spot: Add Picosat to Spot library & Update satsolver class

* Makefile.am: Add picosat to subdirs.
* configure.ac: Add picosat/Makefile to AC_CONFIG_FILES.
* README: Add picosat/ in the list of directories.
* debian/copyright: Add picosat licence and details.
* picosat/Makefile.am: Implement Makefile.am in picosat directory.
* spot/Makefile.am: Tell the compiler to add libpico.la into libspot.la.
* picosat/LICENSE: Add picosat licence.
* picosat/NEWS: Add picosat NEWS.
* picosat/VERSION: Add picosat VERSION.
* picosat/picosat.c: Add picosat c file.
* picosat/picosat.h: Add picosat header file.
* spot/misc/satsolver.cc: Update functions.
* spot/misc/satsolver.hh: Add documentation, clean code, change
some functions visibility and separate templates functions.
* spot/twaalgos/dtbasat.cc: Update dtba_to_sat function.
* spot/twaalgos/dtwasat.cc: Update dtwa_to_sat function.

Makefile.am

@@ -32,7 +32,8 @@ if USE_PYTHON
   PYTHON_SUBDIR = python
 endif
 
-SUBDIRS = buddy lib ltdl spot bin tests $(PYTHON_SUBDIR) doc $(NEVER_SUBDIRS)
+SUBDIRS = picosat buddy lib ltdl spot bin tests $(PYTHON_SUBDIR) doc \
+					$(NEVER_SUBDIRS)
 
 UTF8 = utf8/doc/ReleaseNotes utf8/doc/utf8cpp.html utf8/utf8.h	\
   utf8/utf8/checked.h utf8/utf8/core.h utf8/utf8/unchecked.h

README

@@ -218,6 +218,7 @@ ltdl/             Libtool's portable dlopen() wrapper library.
 lib/              Gnulib's portability modules.
 utf8/             Nemanja Trifunovic's utf-8 routines.
 elisp/		  Related emacs modes, used for building the documentation.
+picosat/          A distribution of PicoSAT 965 (a satsolver library).
 
 Build-system stuff
 ------------------

configure.ac

@@ -261,6 +261,7 @@ AC_CONFIG_FILES([
   doc/org/init.el
   elisp/Makefile
   lib/Makefile
+  picosat/Makefile
   spot/graph/Makefile
   spot/kripke/Makefile
   spot/ltsmin/Makefile

debian/copyright

@@ -162,3 +162,24 @@ License: GPL-3+
  .
  On Debian systems, the complete text of the GNU General
  Public License version 3 can be found in "/usr/share/common-licenses/GPL-3".
+
+Files: picosat/*
+Copyright: 2006 - 2015, Armin Biere, Johannes Kepler University.
+License: MIT style
+ Permission is hereby granted, free of charge, to any person obtaining a copy
+ of this software and associated documentation files (the "Software"), to
+ deal in the Software without restriction, including without limitation the
+ rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+ sell copies of the Software, and to permit persons to whom the Software is
+ furnished to do so, subject to the following conditions:
+
+ The above copyright notice and this permission notice shall be included in
+ all copies or substantial portions of the Software.
+
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+ IN THE SOFTWARE.

picosat/LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to
+deal in the Software without restriction, including without limitation the
+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.
+

picosat/Makefile.am

@@ -0,0 +1,7 @@
+noinst_LTLIBRARIES = libpico.la
+
+libpico_la_SOURCES = picosat.c picosat.h
+
+# Force -DNDEBUG regardless of the Spot settings
+libpico_la_CPPFLAGS = -DNDEBUG -DNGETRUSAGE
+EXTRA_DIST = LICENSE NEWS VERSION

picosat/NEWS

@@ -0,0 +1,162 @@
+news for release 965 since 959
+------------------------------
+
+* ADC code works again (spotted by Himanshu Jain)
+* include into R projects (with Christoph Muessel) (--rcode)
+* fixed 'undefined' + 'ptrdiff_' issues (thanks to Christoph Muessel)
+* added 'picosat_set_interrupt' and '-a <alarm>' command line option
+* fixed various issues pointed out by Stefan Hengelein:
+  - fixed incremental usage of 'picosat_adjust'
+  - added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups)
+  - removed redundant explicit set to zero on reset
+* fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein)
+* removed '-fno-strict-aliasing' (thanks to Jerry James)
+
+news for release 959 since 953
+------------------------------
+
+* fixed header comments
+
+* fixed minor compilation issues
+
+* fixed unitialized memory access problem for 'picosat_deref_partial'
+  and another issue with partial models
+
+* added 'picosat_add_arg' and 'picosat_add_lits'
+
+* '--plain' and 'picosat_set_plain' to disable failed literal probing
+
+* new '#define PICOSAT_REENTRANT_API' in 'picosat.h'
+
+* added manager so no more global variables
+  (allows multiple instances, requires manager object)
+
+news for release 951 since 941
+------------------------------
+
+* cleaned up code (based on comments by Donald Knuth)
+
+* lreduce=O(conflicts^.5)
+
+* added 'picosat_visits' and 'picosat_decisions'
+
+* added '--partial' command line option
+
+* added 'picosat_deref_partial' and 'picosat_save_original_clauses'
+
+* added 'picomcs' as example for MSS computation
+
+news for release 941 since 936
+------------------------------
+
+* added 'picogcnf'
+
+* added All-SAT mode ('--all' command line option)
+
+* statistics include time spent in failed literal preprocessing (probing)
+
+* 'picosat_failed_context' for 'push & pop'
+   (and tested failed assumptions for 'push & pop')
+
+* 'picosat_simplify' for forced garbage collection
+
+* undefined NFL, defined NADC (= failed literals on, ADC's off)
+
+* 'picosat_push' and 'picosat_pop' (beta version)
+
+* fixed some issues related to binary clause handling and 
+  generating list of failed assumptions
+
+news for release 936 since 935
+------------------------------
+
+* simple minimal unsatisfiable core (MUS) extractor 'picomus'
+  (example for using 'picosat_mus_assumptions' and 'picosat_coreclause')
+
+* added 'picosat_mus_assumptions'
+
+* added 'picosat_{set_}propagations'
+
+* new 'int' return value for 'picosat_enable_trace_generation' to
+  check for trace code being compiled
+
+news for release 935 since 926
+------------------------------
+
+* added 'picosat_failed_assumptions' (plural)
+
+* new '-A <failedlits>' command line option
+
+* fixed failed assumption issues
+
+* added 'picosat_remove_learned'
+
+* added 'picosat_reset_{phases,scores}'
+
+* added 'picosat_set_less_important_lit'
+
+* added 'picosat_res'
+
+news for release 926 since 846
+------------------------------
+
+* random initial phase (API of 'picosat_set_default_phase' changed)
+
+* fixed accumulative failed assumption (multiple times)
+
+* fixed missing original clause in core generation with assumptions
+
+* fixed debugging code for memory allocation
+
+* shared library in addition to static library
+
+* removed potential UNKNOWN result without decision limit
+
+* added picosat_set_more_important_lit
+
+* added picosat_coreclause
+
+* propagation of binary clauses until completion
+
+* fixed API usage 'assume;sat;sat'
+
+* literals move to front (LMTF) during traversal of visited clauses
+
+* switched from inner/outer to Luby style restart scheduling
+
+* less agressive reduce schedule
+
+* replaced watched literals with head and tail pointers
+
+* add 'picosat_failed_assumption', which allows to avoid tracing and core
+  generation, if one is only interested in assumptions in the core
+
+* fixed a BUG in the generic iterator code of clauses
+  (should rarely happen unless you use a very sophisticated malloc lib)
+
+news for release 846 since 632
+------------------------------
+
+* cleaned up assumption handling (actually removed buggy optimization)
+
+* incremental core generation 
+
+* experimental 'all different constraint' handling as in our FMCAD'08 paper
+
+* new API calls: 
+
+  - picosat_add_ado_lit       (add all different object literal)
+  - picosat_deref_top_level   (deref top level assignment)
+  - picosat_changed           (check whether extension was possible)
+  - picosat_measure_all_calls (per default do not measure adding time)
+  - picosat_set_prefix        (set prefix for messages)
+
+* 64 bit port (and compilation options)
+
+* optional NVSIDS visualization code
+
+* resource controlled failed literal implementation
+
+* disconnect long clauses satisfied at lower decision level
+
+* controlling restarts

picosat/VERSION

@@ -0,0 +1 @@
+965

picosat/picosat.h

@@ -0,0 +1,665 @@
+/****************************************************************************
+Copyright (c) 2006 - 2015, Armin Biere, Johannes Kepler University.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to
+deal in the Software without restriction, including without limitation the
+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.
+****************************************************************************/
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifndef picosat_h_INCLUDED
+#define picosat_h_INCLUDED
+/*------------------------------------------------------------------------*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <stddef.h>
+
+/*------------------------------------------------------------------------*/
+/* The following macros allows for users to distiguish between different
+ * versions of the API.  The first 'PICOSAT_REENTRANT_API' is defined for
+ * the new reentrant API which allows to generate multiple instances of
+ * PicoSAT in one process.  The second 'PICOSAT_API_VERSION' defines the
+ * (smallest) version of PicoSAT to which this API conforms.
+ */
+#define PICOSAT_REENTRANT_API
+#define PICOSAT_API_VERSION 953		/* API version */
+
+/*------------------------------------------------------------------------*/
+/* These are the return values for 'picosat_sat' as for instance
+ * standardized by the output format of the SAT competition.
+ */
+#define PICOSAT_UNKNOWN         0
+#define PICOSAT_SATISFIABLE     10
+#define PICOSAT_UNSATISFIABLE   20
+
+/*------------------------------------------------------------------------*/
+struct PicoSAT; //forward declaration
+typedef struct PicoSAT PicoSAT;
+
+/*------------------------------------------------------------------------*/
+
+const char *picosat_version (void);
+const char *picosat_config (void);
+const char *picosat_copyright (void);
+
+/*------------------------------------------------------------------------*/
+/* You can make PicoSAT use an external memory manager instead of the one
+ * provided by LIBC. But then you need to call these three function before
+ * 'picosat_init'.  The memory manager functions here all have an additional
+ * first argument which is a pointer to the memory manager, but otherwise
+ * are supposed to work as their LIBC counter parts 'malloc', 'realloc' and
+ * 'free'.  As exception the 'resize' and 'delete' function have as third
+ * argument the number of bytes of the block given as second argument.
+ */
+
+typedef void * (*picosat_malloc)(void *, size_t);
+typedef void * (*picosat_realloc)(void*, void *, size_t, size_t);
+typedef void (*picosat_free)(void*, void*, size_t);
+
+/*------------------------------------------------------------------------*/
+
+PicoSAT * picosat_init (void);          /* constructor */
+
+PicoSAT * picosat_minit (void * state,
+			 picosat_malloc,
+			 picosat_realloc,
+			 picosat_free);
+
+void picosat_reset (PicoSAT *);         /* destructor */
+
+/*------------------------------------------------------------------------*/
+/* The following five functions are essentially parameters to 'init', and
+ * thus should be called right after 'picosat_init' before doing anything
+ * else.  You should not call any of them after adding a literal.
+ */
+
+/* Set output file, default is 'stdout'.
+ */
+void picosat_set_output (PicoSAT *, FILE *);
+
+/* Measure all time spent in all calls in the solver.  By default only the
+ * time spent in 'picosat_sat' is measured.  Enabling this function might
+ * for instance triple the time needed to add large CNFs, since every call
+ * to 'picosat_add' will trigger a call to 'getrusage'.
+ */
+void picosat_measure_all_calls (PicoSAT *);
+
+/* Set the prefix used for printing verbose messages and statistics.
+ * Default is "c ".
+ */
+void picosat_set_prefix (PicoSAT *, const char *);
+
+/* Set verbosity level.  A verbosity level of 1 and above prints more and
+ * more detailed progress reports on the output file, set by
+ * 'picosat_set_output'.  Verbose messages are prefixed with the string set
+ * by 'picosat_set_prefix'.
+ */
+void picosat_set_verbosity (PicoSAT *, int new_verbosity_level);
+
+/* Disable/Enable all pre-processing, currently only failed literal probing.
+ *
+ *  new_plain_value != 0    only 'plain' solving, so no preprocessing
+ *  new_plain_value == 0    allow preprocessing
+ */
+void picosat_set_plain (PicoSAT *, int new_plain_value);
+
+/* Set default initial phase:
+ *
+ *   0 = false
+ *   1 = true
+ *   2 = Jeroslow-Wang (default)
+ *   3 = random initial phase
+ *
+ * After a variable has been assigned the first time, it will always
+ * be assigned the previous value if it is picked as decision variable.
+ * The initial assignment can be chosen with this function.
+ */
+void picosat_set_global_default_phase (PicoSAT *, int);
+
+/* Set next/initial phase of a particular variable if picked as decision
+ * variable.  Second argument 'phase' has the following meaning:
+ *
+ *   negative = next value if picked as decision variable is false
+ *
+ *   positive = next value if picked as decision variable is true
+ *
+ *   0        = use global default phase as next value and
+ *              assume 'lit' was never assigned
+ *
+ * Again if 'lit' is assigned afterwards through a forced assignment,
+ * then this forced assignment is the next phase if this variable is
+ * used as decision variable.
+ */
+void picosat_set_default_phase_lit (PicoSAT *, int lit, int phase);
+
+/* You can reset all phases by the following function.
+ */
+void picosat_reset_phases (PicoSAT *);
+
+/* Scores can be erased as well.  Note, however, that even after erasing
+ * scores and phases, learned clauses are kept.  In addition head tail
+ * pointers for literals are not moved either.  So expect a difference
+ * between calling the solver in incremental mode or with a fresh copy of
+ * the CNF.
+ */
+void picosat_reset_scores (PicoSAT *);
+
+/* Reset assignment if in SAT state and then remove the given percentage of
+ * less active (large) learned clauses.  If you specify 100% all large
+ * learned clauses are removed.
+ */
+void picosat_remove_learned (PicoSAT *, unsigned percentage);
+
+/* Set some variables to be more important than others.  These variables are
+ * always used as decisions before other variables are used.  Dually there
+ * is a set of variables that is used last.  The default is
+ * to mark all variables as being indifferent only.
+ */
+void picosat_set_more_important_lit (PicoSAT *, int lit);
+void picosat_set_less_important_lit (PicoSAT *, int lit);
+
+/* Allows to print to internal 'out' file from client.
+ */
+void picosat_message (PicoSAT *, int verbosity_level, const char * fmt, ...);
+
+/* Set a seed for the random number generator.  The random number generator
+ * is currently just used for generating random decisions.  In our
+ * experiments having random decisions did not really help on industrial
+ * examples, but was rather helpful to randomize the solver in order to
+ * do proper benchmarking of different internal parameter sets.
+ */
+void picosat_set_seed (PicoSAT *, unsigned random_number_generator_seed);
+
+/* If you ever want to extract cores or proof traces with the current
+ * instance of PicoSAT initialized with 'picosat_init', then make sure to
+ * call 'picosat_enable_trace_generation' right after 'picosat_init'.   This
+ * is not necessary if you only use 'picosat_set_incremental_rup_file'.
+ *
+ * NOTE, trace generation code is not necessarily included, e.g. if you
+ * configure PicoSAT with full optimzation as './configure.sh -O' or with
+
+ * you do not get any results by trying to generate traces.
+ *
+ * The return value is non-zero if code for generating traces is included
+ * and it is zero if traces can not be generated.
+ */
+int picosat_enable_trace_generation (PicoSAT *);
+
+/* You can dump proof traces in RUP format incrementally even without
+ * keeping the proof trace in memory.  The advantage is a reduction of
+ * memory usage, but the dumped clauses do not necessarily belong to the
+ * clausal core.  Beside the file the additional parameters denotes the
+ * maximal number of variables and the number of original clauses.
+ */
+void picosat_set_incremental_rup_file (PicoSAT *, FILE * file, int m, int n);
+
+/* Save original clauses for 'picosat_deref_partial'.  See comments to that
+ * function further down.
+ */
+void picosat_save_original_clauses (PicoSAT *);
+
+/* Add a call back which is checked regularly to notify the SAT solver
+ * to terminate earlier.  This is useful for setting external time limits
+ * or terminate early in say a portfolio style parallel SAT solver.
+ */
+void picosat_set_interrupt (PicoSAT *,
+                            void * external_state,
+			    int (*interrupted)(void * external_state));
+
+/*------------------------------------------------------------------------*/
+/* This function returns the next available unused variable index and
+ * allocates a variable for it even though this variable does not occur as
+ * assumption, nor in a clause or any other constraints.  In future calls to
+ * 'picosat_sat', 'picosat_deref' and particularly for 'picosat_changed',
+ * this variable is treated as if it had been used.
+ */
+int picosat_inc_max_var (PicoSAT *);
+
+/*------------------------------------------------------------------------*/
+/* Push and pop semantics for PicoSAT.   'picosat_push' opens up a new
+ * context.  All clauses added in this context are attached to it and
+ * discarded when the context is closed with 'picosat_pop'.  It is also
+ * possible to nest contexts.
+ *
+ * The current implementation uses a new internal variable for each context.
+ * However, the indices for these internal variables are shared with
+ * ordinary external variables.  This means that after any call to
+ * 'picosat_push', new variable indices should be obtained with
+ * 'picosat_inc_max_var' and not just by incrementing the largest variable
+ * index used so far.
+ *
+ * The return value is the index of the literal that assumes this context.
+ * This literal can only be used for 'picosat_failed_context' otherwise
+ * it will lead to an API usage error.
+ */
+int picosat_push (PicoSAT *);
+
+/* This is as 'picosat_failed_assumption', but only for internal variables
+ * generated by 'picosat_push'.
+ */
+int picosat_failed_context (PicoSAT *, int lit);
+
+/* Returns the literal that assumes the current context or zero if the
+ * outer context has been reached.
+ */
+int picosat_context (PicoSAT *);
+
+/* Closes the current context and recycles the literal generated for
+ * assuming this context.  The return value is the literal for the new
+ * outer context or zero if the outer most context has been reached.
+ */
+int picosat_pop (PicoSAT *);
+
+/* Force immmediate removal of all satisfied clauses and clauses that are
+ * added or generated in closed contexts.  This function is called
+ * internally if enough units are learned or after a certain number of
+ * contexts have been closed.  This number is fixed at compile time
+ * and defined as MAXCILS in 'picosat.c'.
+ *
+ * Note that learned clauses which only involve outer contexts are kept.
+ */
+void picosat_simplify (PicoSAT *);
+
+/*------------------------------------------------------------------------*/
+/* If you know a good estimate on how many variables you are going to use
+ * then calling this function before adding literals will result in less
+ * resizing of the variable table.  But this is just a minor optimization.
+ * Beside exactly allocating enough variables it has the same effect as
+ * calling 'picosat_inc_max_var'.
+ */
+void picosat_adjust (PicoSAT *, int max_idx);
+
+/*------------------------------------------------------------------------*/
+/* Statistics.
+ */
+int picosat_variables (PicoSAT *);                      /* p cnf <m> n */
+int picosat_added_original_clauses (PicoSAT *);         /* p cnf m <n> */
+size_t picosat_max_bytes_allocated (PicoSAT *);
+double picosat_time_stamp (void);                       /* ... in process */
+void picosat_stats (PicoSAT *);                         /* > output file */
+unsigned long long picosat_propagations (PicoSAT *);	/* #propagations */
+unsigned long long picosat_decisions (PicoSAT *);	/* #decisions */
+unsigned long long picosat_visits (PicoSAT *);		/* #visits */
+
+/* The time spent in calls to the library or in 'picosat_sat' respectively.
+ * The former is returned if, right after initialization
+ * 'picosat_measure_all_calls' is called.
+ */
+double picosat_seconds (PicoSAT *);
+
+/*------------------------------------------------------------------------*/
+/* Add a literal of the next clause.  A zero terminates the clause.  The
+ * solver is incremental.  Adding a new literal will reset the previous
+ * assignment.   The return value is the original clause index to which
+ * this literal respectively the trailing zero belong starting at 0.
+ */
+int picosat_add (PicoSAT *, int lit);
+
+/* As the previous function, but allows to add a full clause at once with an
+ * at compiled time known size.  The list of argument literals has to be
+ * terminated with a zero literal.  Literals beyond the first zero literal
+ * are discarded.
+ */
+int picosat_add_arg (PicoSAT *, ...);
+
+/* As the previous function but with an at compile time unknown size.
+ */
+int picosat_add_lits (PicoSAT *, int * lits);
+
+/* Print the CNF to the given file in DIMACS format.
+ */
+void picosat_print (PicoSAT *, FILE *);
+
+/* You can add arbitrary many assumptions before the next 'picosat_sat'
+ * call.  This is similar to the using assumptions in MiniSAT, except that
+ * for PicoSAT you do not have to collect all your assumptions in a vector
+ * yourself.  In PicoSAT you can add one after the other, to be used in the
+ * next call to 'picosat_sat'.
+ *
+ * These assumptions can be interpreted as adding unit clauses with those
+ * assumptions as literals.  However these assumption clauses are only valid
+ * for exactly the next call to 'picosat_sat', and will be removed
+ * afterwards, e.g. in following future calls to 'picosat_sat' after the
+ * next 'picosat_sat' call, unless they are assumed again trough
+ * 'picosat_assume'.
+ *
+ * More precisely, assumptions actually remain valid even after the next
+ * call to 'picosat_sat' has returned.  Valid means they remain 'assumed'
+ * internally until a call to 'picosat_add', 'picosat_assume', or a second
+ * 'picosat_sat', following the first 'picosat_sat'.  The reason for keeping
+ * them valid is to allow 'picosat_failed_assumption' to return correct
+ * values.
+ *
+ * Example:
+ *
+ *   picosat_assume (1);        // assume unit clause '1 0'
+ *   picosat_assume (-2);       // additionally assume clause '-2 0'
+ *   res = picosat_sat (1000);  // assumes 1 and -2 to hold
+ *                              // 1000 decisions max.
+ *
+ *   if (res == PICOSAT_UNSATISFIABLE)
+ *     {
+ *       if (picosat_failed_assumption (1))
+ *         // unit clause '1 0' was necessary to derive UNSAT
+ *
+ *       if (picosat_failed_assumption (-2))
+ *         // unit clause '-2 0' was necessary to derive UNSAT
+ *
+ *       // at least one but also both could be necessary
+ *
+ *       picosat_assume (17);  // previous assumptions are removed
+ *                             // now assume unit clause '17 0' for
+ *                             // the next call to 'picosat_sat'
+ *
+ *       // adding a new clause, actually the first literal of
+ *       // a clause would also make the assumptions used in the previous
+ *       // call to 'picosat_sat' invalid.
+ *
+ *       // The first two assumptions above are not assumed anymore.  Only
+ *       // the assumptions, since the last call to 'picosat_sat' returned
+ *       // are assumed, e.g. the unit clause '17 0'.
+ *
+ *       res = picosat_sat (-1);
+ *     }
+ *   else if (res == PICOSAT_SATISFIABLE)
+ *     {
+ *       // now the assignment is valid and we can call 'picosat_deref'
+ *
+ *       assert (picosat_deref (1) == 1));
+ *       assert (picosat_deref (-2) == 1));
+ *
+ *       val = picosat_deref (15);
+ *
+ *       // previous two assumptions are still valid
+ *
+ *       // would become invalid if 'picosat_add' or 'picosat_assume' is
+ *       // called here, but we immediately call 'picosat_sat'.  Now when
+ *       // entering 'picosat_sat' the solver knows that the previous call
+ *       // returned SAT and it can safely reset the previous assumptions
+ *
+ *       res = picosat_sat (-1);
+ *     }
+ *   else
+ *     {
+ *       assert (res == PICOSAT_UNKNOWN);
+ *
+ *       // assumptions valid, but assignment invalid
+ *       // except for top level assigned literals which
+ *       // necessarily need to have this value if the formula is SAT
+ *
+ *       // as above the solver nows that the previous call returned UNKWOWN
+ *       // and will before doing anything else reset assumptions
+ *
+ *       picosat_sat (-1);
+ *     }
+ */
+void picosat_assume (PicoSAT *, int lit);
+
+/*------------------------------------------------------------------------*/
+/* This is an experimental feature for handling 'all different constraints'
+ * (ADC).  Currently only one global ADC can be handled.  The bit-width of
+ * all the bit-vectors entered in this ADC (stored in 'all different
+ * objects' or ADOs) has to be identical.
+ *
+ * TODO: also handle top level assigned literals here.
+ */
+void picosat_add_ado_lit (PicoSAT *, int);
+
+/*------------------------------------------------------------------------*/
+/* Call the main SAT routine.  A negative decision limit sets no limit on
+ * the number of decisions.  The return values are as above, e.g.
+ * 'PICOSAT_UNSATISFIABLE', 'PICOSAT_SATISFIABLE', or 'PICOSAT_UNKNOWN'.
+ */
+int picosat_sat (PicoSAT *, int decision_limit);
+
+/* As alternative to a decision limit you can use the number of propagations
+ * as limit.  This is more linearly related to execution time. This has to
+ * be called after 'picosat_init' and before 'picosat_sat'.
+ */
+void picosat_set_propagation_limit (PicoSAT *, unsigned long long limit);
+
+/* Return last result of calling 'picosat_sat' or '0' if not called.
+ */
+int picosat_res (PicoSAT *);
+
+/* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then
+ * the satisfying assignment can be obtained by 'dereferencing' literals.
+ * The value of the literal is return as '1' for 'true',  '-1' for 'false'
+ * and '0' for an unknown value.
+ */
+int picosat_deref (PicoSAT *, int lit);
+
+/* Same as before but just returns true resp. false if the literals is
+ * forced to this assignment at the top level.  This function does not
+ * require that 'picosat_sat' was called and also does not internally reset
+ * incremental usage.
+ */
+int picosat_deref_toplevel (PicoSAT *, int lit);
+
+/* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE' a
+ * partial satisfying assignment can be obtained as well.  It satisfies all
+ * original clauses.  The value of the literal is return as '1' for 'true',
+ * '-1' for 'false' and '0' for an unknown value.  In order to make this
+ * work all original clauses have to be saved internally, which has to be
+ * enabled by 'picosat_save_original_clauses' right after initialization.
+ */
+int picosat_deref_partial (PicoSAT *, int lit);
+
+/* Returns non zero if the CNF is unsatisfiable because an empty clause was
+ * added or derived.
+ */
+int picosat_inconsistent  (PicoSAT *);
+
+/* Returns non zero if the literal is a failed assumption, which is defined
+ * as an assumption used to derive unsatisfiability.  This is as accurate as
+ * generating core literals, but still of course is an overapproximation of
+ * the set of assumptions really necessary.  The technique does not need
+ * clausal core generation nor tracing to be enabled and thus can be much
+ * more effective.  The function can only be called as long the current
+ * assumptions are valid.  See 'picosat_assume' for more details.
+ */
+int picosat_failed_assumption (PicoSAT *, int lit);
+
+/* Returns a zero terminated list of failed assumption in the last call to
+ * 'picosat_sat'.  The pointer is valid until the next call to
+ * 'picosat_sat' or 'picosat_failed_assumptions'.  It only makes sense if the
+ * last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'.
+ */
+const int * picosat_failed_assumptions (PicoSAT *);
+
+/* Returns a zero terminated minimized list of failed assumption for the last
+ * call to 'picosat_sat'.  The pointer is valid until the next call to this
+ * function or 'picosat_sat' or 'picosat_mus_assumptions'.  It only makes sense
+ * if the last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'.
+ *
+ * The call back function is called for all successful simplification
+ * attempts.  The first argument of the call back function is the state
+ * given as first argument to 'picosat_mus_assumptions'.  The second
+ * argument to the call back function is the new reduced list of failed
+ * assumptions.
+ *
+ * This function will call 'picosat_assume' and 'picosat_sat' internally but
+ * before returning reestablish a proper UNSAT state, e.g.
+ * 'picosat_failed_assumption' will work afterwards as expected.
+ *
+ * The last argument if non zero fixes assumptions.  In particular, if an
+ * assumption can not be removed it is permanently assigned true, otherwise
+ * if it turns out to be redundant it is permanently assumed to be false.
+ */
+const int * picosat_mus_assumptions (PicoSAT *, void *,
+                                     void(*)(void*,const int*),int);
+
+/* Compute one maximal subset of satisfiable assumptions.  You need to set
+ * the assumptions, call 'picosat_sat' and check for 'picosat_inconsistent',
+ * before calling this function.  The result is a zero terminated array of
+ * assumptions that consistently can be asserted at the same time.  Before
+ * returing the library 'reassumes' all assumptions.
+ *
+ * It could be beneficial to set the default phase of assumptions
+ * to true (positive).  This can speed up the computation.
+ */
+const int * picosat_maximal_satisfiable_subset_of_assumptions (PicoSAT *);
+
+/* This function assumes that you have set up all assumptions with
+ * 'picosat_assume'.  Then it calls 'picosat_sat' internally unless the
+ * formula is already inconsistent without assumptions, i.e.  it contains
+ * the empty clause.  After that it extracts a maximal satisfiable subset of
+ * assumptions.
+ *
+ * The result is a zero terminated maximal subset of consistent assumptions
+ * or a zero pointer if the formula contains the empty clause and thus no
+ * more maximal consistent subsets of assumptions can be extracted.  In the
+ * first case, before returning, a blocking clause is added, that rules out
+ * the result for the next call.
+ *
+ * NOTE: adding the blocking clause changes the CNF.
+ *
+ * So the following idiom
+ *
+ * const int * mss;
+ * picosat_assume (a1);
+ * picosat_assume (a2);
+ * picosat_assume (a3);
+ * picosat_assume (a4);
+ * while ((mss = picosat_next_maximal_satisfiable_subset_of_assumptions ()))
+ *   process_mss (mss);
+ *
+ * can be used to iterate over all maximal consistent subsets of
+ * the set of assumptions {a1,a2,a3,a4}.
+ *
+ * It could be beneficial to set the default phase of assumptions
+ * to true (positive).  This might speed up the computation.
+ */
+const int *
+picosat_next_maximal_satisfiable_subset_of_assumptions (PicoSAT *);
+
+/* Similarly we can iterate over all minimal correcting assumption sets.
+ * See the CAMUS literature [M. Liffiton, K. Sakallah JAR 2008].
+ *
+ * The result contains each assumed literal only once, even if it
+ * was assumed multiple times (in contrast to the maximal consistent
+ * subset functions above).
+ *
+ * It could be beneficial to set the default phase of assumptions
+ * to true (positive).  This might speed up the computation.
+ */
+const int *
+picosat_next_minimal_correcting_subset_of_assumptions (PicoSAT *);
+
+/* Compute the union of all minmal correcting sets, which is called
+ * the 'high level union of all minimal unsatisfiable subset sets'
+ * or 'HUMUS' in our papers.
+ *
+ * It uses 'picosat_next_minimal_correcting_subset_of_assumptions' and
+ * the same notes and advices apply.  In particular, this implies that
+ * after calling the function once, the current CNF becomes inconsistent,
+ * and PicoSAT has to be reset.  So even this function internally uses
+ * PicoSAT incrementally, it can not be used incrementally itself at this
+ * point.
+ *
+ * The 'callback' can be used for progress logging and is called after
+ * each extracted minimal correcting set if non zero.  The 'nhumus'
+ * parameter of 'callback' denotes the number of assumptions found to be
+ * part of the HUMUS sofar.
+ */
+const int *
+picosat_humus (PicoSAT *,
+               void (*callback)(void * state, int nmcs, int nhumus),
+	       void * state);
+
+/*------------------------------------------------------------------------*/
+/* Assume that a previous call to 'picosat_sat' in incremental usage,
+ * returned 'SATISFIABLE'.  Then a couple of clauses and optionally new
+ * variables were added (a new variable is a variable that has an index
+ * larger then the maximum variable added so far).  The next call to
+ * 'picosat_sat' also returns 'SATISFIABLE'. If this function
+ * 'picosat_changed' returns '0', then the assignment to the old variables
+ * is guaranteed to not have changed.  Otherwise it might have changed.
+ *
+ * The return value to this function is only valid until new clauses are
+ * added through 'picosat_add', an assumption is made through
+ * 'picosat_assume', or again 'picosat_sat' is called.  This is the same
+ * assumption as for 'picosat_deref'.
+ *
+ * TODO currently this function might also return a non zero value even if
+ * the old assignment did not change, because it only checks whether the
+ * assignment of at least one old variable was flipped at least once during
+ * the search.  In principle it should be possible to be exact in the other
+ * direction as well by using a counter of variables that have an odd number
+ * of flips.  But this is not implemented yet.
+ */
+int picosat_changed (PicoSAT *);
+
+/*------------------------------------------------------------------------*/
+/* The following six functions internally extract the variable and clausal
+ * core and thus require trace generation to be enabled with
+ * 'picosat_enable_trace_generation' right after calling 'picosat_init'.
+ *
+ * TODO: using these functions in incremental mode with failed assumptions
+ * has only been tested for 'picosat_corelit' thoroughly.  The others
+ * probably only work in non-incremental mode or without using
+ * 'picosat_assume'.
+ */
+
+/* This function determines whether the i'th added original clause is in the
+ * core.  The 'i' is the return value of 'picosat_add', which starts at zero
+ * and is incremented by one after a original clause is added (that is after
+ * 'picosat_add (0)').  For the index 'i' the following has to hold:
+ *
+ *   0 <= i < picosat_added_original_clauses ()
+ */
+int picosat_coreclause (PicoSAT *, int i);
+
+/* This function gives access to the variable core, which is made up of the
+ * variables that were resolved in deriving the empty clause.
+ */
+int picosat_corelit (PicoSAT *, int lit);
+
+/* Write the clauses that were used in deriving the empty clause to a file
+ * in DIMACS format.
+ */
+void picosat_write_clausal_core (PicoSAT *, FILE * core_file);
+
+/* Write a proof trace in TraceCheck format to a file.
+ */
+void picosat_write_compact_trace (PicoSAT *, FILE * trace_file);
+void picosat_write_extended_trace (PicoSAT *, FILE * trace_file);
+
+/* Write a RUP trace to a file.  This trace file contains only the learned
+ * core clauses while this is not necessarily the case for the RUP file
+ * obtained with 'picosat_set_incremental_rup_file'.
+ */
+void picosat_write_rup_trace (PicoSAT *, FILE * trace_file);
+
+/*------------------------------------------------------------------------*/
+/* Keeping the proof trace around is not necessary if an over-approximation
+ * of the core is enough.  A literal is 'used' if it was involved in a
+ * resolution to derive a learned clause.  The core literals are necessarily
+ * a subset of the 'used' literals.
+ */
+
+int picosat_usedlit (PicoSAT *, int lit);
+/*------------------------------------------------------------------------*/
+#endif
+
+#ifdef __cplusplus
+}
+#endif

spot/Makefile.am

@@ -42,7 +42,8 @@ libspot_la_LIBADD =  \
   tl/libtl.la \
   twaalgos/libtwaalgos.la \
   twa/libtwa.la \
-  ../lib/libgnu.la
+  ../lib/libgnu.la \
+  ../picosat/libpico.la
 
 # Dummy C++ source to cause C++ linking.
 nodist_EXTRA_libspot_la_SOURCES = _.cc

spot/misc/satsolver.cc

@@ -23,66 +23,13 @@
 #include <sstream>
 #include <stdexcept>
 #include <spot/misc/satsolver.hh>
+#include <picosat/picosat.h>
 #include <fstream>
 #include <limits>
 #include <sys/wait.h>
 
 namespace spot
 {
-  namespace
-  {
-    struct satsolver_command: formater
-    {
-      const char* satsolver;
-
-      satsolver_command()
-      {
-        satsolver = getenv("SPOT_SATSOLVER");
-        if (!satsolver)
-          {
-            satsolver = "glucose -verb=0 -model %I >%O";
-            return;
-          }
-        prime(satsolver);
-        if (!has('I'))
-          throw std::runtime_error("SPOT_SATSOLVER should contain %I to "
-                                   "indicate how to use the input filename.");
-        if (!has('O'))
-          throw std::runtime_error("SPOT_SATSOLVER should contain %O to "
-                                   "indicate how to use the output filename.");
-      }
-
-      int
-      run(printable* in, printable* out)
-      {
-        declare('I', in);
-        declare('O', out);
-        std::ostringstream s;
-        format(s, satsolver);
-        int res = system(s.str().c_str());
-        if (res < 0 || (WIFEXITED(res) && WEXITSTATUS(res) == 127))
-          {
-            s << ": failed to execute";
-            throw std::runtime_error(s.str());
-          }
-        // For POSIX shells, "The exit status of a command that
-        // terminated because it received a signal shall be reported
-        // as greater than 128."
-        if (WIFEXITED(res) && WEXITSTATUS(res) >= 128)
-          {
-            s << ": terminated by signal";
-            throw std::runtime_error(s.str());
-          }
-        if (WIFSIGNALED(res))
-          {
-            s << ": terminated by signal " << WTERMSIG(res);
-            throw std::runtime_error(s.str());
-          }
-        return res;
-      }
-    };
-  }
-
   satsolver::solution
   satsolver_get_solution(const char* filename)
   {
@@ -122,17 +69,35 @@ namespace spot
     return sol;
   }
 
+  // In other functions, command_given() won't be called anymore as it is more
+  // easy to check if psat_ was initialized or not.
   satsolver::satsolver()
-    : cnf_tmp_(nullptr), cnf_stream_(nullptr)
+    : cnf_tmp_(nullptr), cnf_stream_(nullptr), nclauses_(0), nvars_(0),
+      psat_(nullptr)
   {
-    start();
+    if (cmd_.command_given())
+    {
+      start();
+    }
+    else
+    {
+      psat_ = picosat_init();
+      picosat_set_seed(psat_, 0);
+    }
   }
 
   satsolver::~satsolver()
   {
-    delete cnf_tmp_;
+    if (psat_)
-    delete cnf_stream_;
+    {
-    delete nclauses_;
+      picosat_reset(psat_);
+      psat_ = nullptr;
+    }
+    else
+    {
+      delete cnf_tmp_;
+      delete cnf_stream_;
+    }
   }
 
   void satsolver::start()
@@ -140,70 +105,192 @@ namespace spot
     cnf_tmp_ = create_tmpfile("sat-", ".cnf");
     cnf_stream_ = new std::ofstream(cnf_tmp_->name(), std::ios_base::trunc);
     cnf_stream_->exceptions(std::ofstream::failbit | std::ofstream::badbit);
-    nclauses_ = new clause_counter();
 
     // Add empty line for the header
     *cnf_stream_ << "                                                 \n";
   }
 
+  // Must be called only when SPOT_SATSOLVER is given
   void satsolver::end_clause()
   {
     *cnf_stream_ << '\n';
-    *nclauses_ += 1;
+    nclauses_ += 1;
+    if (nclauses_ < 0)
+      throw std::runtime_error("too many SAT clauses (more than INT_MAX)");
+  }
+
+  void satsolver::adjust_nvars(int nvars)
+  {
+    if (nvars < 0)
+      throw std::runtime_error("variable number must be at least 0");
+
+    if (psat_)
+    {
+      picosat_adjust(psat_, nvars);
+    }
+    else
+    {
+      if (nvars < nvars_)
+      {
+        throw std::runtime_error(
+            "wrong number of variables, a bigger one was already added");
+      }
+      nvars_ = nvars;
+    }
   }
 
   void satsolver::add(std::initializer_list<int> values)
   {
     for (auto& v : values)
     {
-      *cnf_stream_ << v << ' ';
+      if (psat_)
-      if (!v) // ..., 0)
+      {
-        end_clause();
+        picosat_add(psat_, v);
+      }
+      else
+      {
+        *cnf_stream_ << v << ' ';
+        if (!v) // ..., 0)
+          end_clause();
+
+        if (nvars_ < v)
+          nvars_ = v;
+      }
     }
   }
 
   void satsolver::add(int v)
   {
-    *cnf_stream_ << v << ' ';
+    if (psat_)
-    if (!v) // 0
+    {
-      end_clause();
+      picosat_add(psat_, v);
+    }
+    else
+    {
+      *cnf_stream_ << v << ' ';
+      if (!v) // 0
+        end_clause();
+
+      if (v && nvars_ < v)
+        nvars_ = v;
+    }
   }
 
   int satsolver::get_nb_clauses() const
   {
-    return nclauses_->nb_clauses();
+    if (psat_)
+      return picosat_added_original_clauses(psat_);
+    return nclauses_;
   }
 
-  std::pair<int, int> satsolver::stats(int nvars)
+  int satsolver::get_nb_vars() const
   {
-    int nclaus = nclauses_->nb_clauses();
+    if (psat_)
-    cnf_stream_->seekp(0);
+      return picosat_variables(psat_);
-    *cnf_stream_ << "p cnf " << nvars << ' ' << nclaus;
+    return nvars_;
-    return std::make_pair(nvars, nclaus);
   }
 
   std::pair<int, int> satsolver::stats()
   {
-    *cnf_stream_ << "p cnf 1 2\n-1 0\n1 0\n";
+    return std::make_pair(get_nb_vars(), get_nb_clauses());
-    return std::make_pair(1, 2);
+  }
+
+  satsolver::solution
+  satsolver::picosat_get_solution(int res)
+  {
+    satsolver::solution sol;
+    if (res == PICOSAT_SATISFIABLE)
+    {
+      int nvars = get_nb_vars();
+      for (int lit = 1; lit <= nvars; ++lit)
+      {
+        if (picosat_deref(psat_, lit) > 0)
+          sol.push_back(lit);
+        else
+          sol.push_back(-lit);
+      }
+    }
+    return sol;
   }
 
   satsolver::solution_pair
   satsolver::get_solution()
   {
-    delete cnf_stream_;                // Close the file.
-    cnf_stream_ = nullptr;
-
-    temporary_file* output = create_tmpfile("sat-", ".out");
     solution_pair p;
+    if (psat_)
+    {
+      p.first = 0; // A subprocess was not executed so nothing failed.
+      int res = picosat_sat(psat_, -1); // -1: no limit (number of decisions).
+      p.second = picosat_get_solution(res);
+    }
+    else
+    {
+      // Update header
+      cnf_stream_->seekp(0);
+      *cnf_stream_ << "p cnf " << get_nb_vars() << ' ' << get_nb_clauses();
+      cnf_stream_->seekp(0, std::ios_base::end);
+      if (!*cnf_stream_)
+        throw std::runtime_error("Failed to update cnf header");
 
-    // Make this static, so the SPOT_SATSOLVER lookup is done only on
+      temporary_file* output = create_tmpfile("sat-", ".out");
-    // the first call to run_sat().
+      p.first = cmd_.run(cnf_tmp_, output);
-    static satsolver_command cmd;
+      p.second = satsolver_get_solution(output->name());
-
+      delete output;
-    p.first = cmd.run(cnf_tmp_, output);
+    }
-    p.second = satsolver_get_solution(output->name());
-    delete output;
     return p;
   }
+
+  satsolver_command::satsolver_command() : satsolver(nullptr)
+  {
+    satsolver = getenv("SPOT_SATSOLVER");
+    if (!satsolver)
+      return;
+
+    prime(satsolver);
+    if (!has('I'))
+      throw std::runtime_error("SPOT_SATSOLVER should contain %I to "
+          "indicate how to use the input filename.");
+    if (!has('O'))
+      throw std::runtime_error("SPOT_SATSOLVER should contain %O to "
+          "indicate how to use the output filename.");
+  }
+
+  bool
+  satsolver_command::command_given()
+  {
+    return satsolver != nullptr;
+  }
+
+  int
+  satsolver_command::run(printable* in, printable* out)
+  {
+    declare('I', in);
+    declare('O', out);
+    std::ostringstream s;
+    format(s, satsolver);
+
+    int res = system(s.str().c_str());
+    if (res < 0 || (WIFEXITED(res) && WEXITSTATUS(res) == 127))
+    {
+      s << ": failed to execute";
+      throw std::runtime_error(s.str());
+    }
+
+    // For POSIX shells, "The exit status of a command that
+    // terminated because it received a signal shall be reported
+    // as greater than 128."
+    if (WIFEXITED(res) && WEXITSTATUS(res) >= 128)
+    {
+      s << ": terminated by signal";
+      throw std::runtime_error(s.str());
+    }
+
+    if (WIFSIGNALED(res))
+    {
+      s << ": terminated by signal " << WTERMSIG(res);
+      throw std::runtime_error(s.str());
+    }
+
+    return res;
+  }
 }

spot/misc/satsolver.hh

@@ -26,68 +26,58 @@
 #include <iosfwd>
 #include <initializer_list>
 
+struct PicoSAT; // forward
+
 namespace spot
 {
   class printable;
 
-  class clause_counter
+  /// \brief Interface with a given sat solver.
+  ///
+  /// When created, it checks if SPOT_SATSOLVER env var is set. If so,
+  /// its value is parsed and saved internally. The env variable musb be set
+  /// like this: "<satsolver> [its_options] %I > %O"
+  /// where %I and %O are replaced by input and output files.
+  ///
+  /// The run method permits of course to run the given sat solver.
+  class satsolver_command: formater
   {
   private:
-    int count_;
+    const char* satsolver;
 
   public:
-    clause_counter()
+    satsolver_command();
-      : count_(0)
-    {
-    }
 
-    void check() const
+    /// \brief Return true if a satsolver is given, false otherwise.
-    {
+    bool command_given();
-      if (count_ < 0)
-        throw std::runtime_error("too many SAT clauses (more than INT_MAX)");
-    }
 
-    clause_counter& operator++()
+    /// \brief Run the given satsolver.
-    {
+    int run(printable* in, printable* out);
-      ++count_;
-      check();
-      return *this;
-    }
 
-    clause_counter& operator+=(int n)
-    {
-      count_ += n;
-      check();
-      return *this;
-    }
-
-    int nb_clauses() const
-    {
-      return count_;
-    }
   };
 
   /// \brief Interface with a SAT solver.
   ///
-  /// Call start() to initialize the cnf file. This class provides the
+  /// This class provides the necessary functions to add clauses, comments.
-  /// necessary functions to handle the cnf file, add clauses, count them,
+  /// Depending on SPOT_SATSOLVER, it will use either picosat solver (default)
-  /// update the header, add some comments...
+  /// or the given satsolver.
-  /// It is not possible to write in the file without having to call these
-  /// functions.
-  ///
-  /// The satsolver called can be configured via the
-  /// <code>SPOT_SATSOLVER</code> environment variable. It must be this set
-  /// following this: "satsolver -verb=0 %I >%O".
   ///
+  /// Now that spot is distributed with a satsolver (PicoSAT), it is used by
+  /// default. But another satsolver can be configured via the
+  /// <code>SPOT_SATSOLVER</code> environment variable. It must be set following
+  /// this: "satsolver [options] %I > %O"
   /// where %I and %O are replaced by input and output files.
   class SPOT_API satsolver
   {
   public:
+    /// \brief Construct the sat solver and itinialize variables.
+    /// If no satsolver is provided through SPOT_SATSOLVER env var, a
+    /// distributed version of PicoSAT will be used.
     satsolver();
     ~satsolver();
 
-    /// \brief Initialize private attributes
+    /// \brief Adjust the number of variables used in the cnf formula.
-    void start();
+    void adjust_nvars(int nvars);
 
     /// \brief Add a list of lit. to the current clause.
     void add(std::initializer_list<int> values);
@@ -98,58 +88,109 @@ namespace spot
     /// \breif Get the current number of clauses.
     int get_nb_clauses() const;
 
-    /// \breif Update cnf_file's header with the correct stats.
+    /// \brief Get the current number of variables.
-    std::pair<int, int> stats(int nvars);
+    int get_nb_vars() const;
 
-    /// \breif Create an unsatisfiable cnf_file, return stats about it.
+    /// \brief Returns std::pair<nvars, nclauses>;
     std::pair<int, int> stats();
 
-    /// \breif Add a comment in cnf file.
+    /// \brief Add a comment.
+    /// It should be used only in debug mode after providing a satsolver.
     template<typename T>
-    void comment_rec(T single)
+    void comment_rec(T single);
-    {
-      *cnf_stream_ << single << ' ';
-    }
 
-    /// \breif Add a comment in cnf_file.
+    /// \brief Add comments.
+    /// It should be used only in debug mode after providing a satsolver.
     template<typename T, typename... Args>
-    void comment_rec(T first, Args... args)
+    void comment_rec(T first, Args... args);
-    {
-      *cnf_stream_ << first << ' ';
-      comment_rec(args...);
-    }
 
-    /// \breif Add a comment in the cnf_file, starting with 'c'.
+    /// \brief Add a comment. It will start with "c ".
+    /// It should be used only in debug mode after providing a satsolver.
     template<typename T>
-    void comment(T single)
+    void comment(T single);
-    {
-      *cnf_stream_ << "c " << single << ' ';
-    }
 
-    /// \breif Add comment in the cnf_file, starting with 'c'.
+    /// \brief Add comments. It will start with "c ".
+    /// It should be used only in debug mode after providing a satsolver.
     template<typename T, typename... Args>
-    void comment(T first, Args... args)
+    void comment(T first, Args... args);
-    {
-      *cnf_stream_ << "c " << first << ' ';
-      comment_rec(args...);
-    }
 
     typedef std::vector<int> solution;
     typedef std::pair<int, solution> solution_pair;
+
+    /// \brief Return std::vector<solving_return_code, solution>.
     solution_pair get_solution();
 
-  private:
+  private:  // methods
-    /// \breif End the current clause and increment the counter.
+    /// \brief Initialize cnf streams attributes.
+    void start();
+
+    /// \brief End the current clause and increment the counter.
     void end_clause();
 
-  private:
+    /// \brief Extract the solution of Picosat output.
+    /// Must be called only if SPOT_SATSOLVER env variable is not set.
+    satsolver::solution
+    picosat_get_solution(int res);
+
+  private:  // variables
+    /// \brief A satsolver_command. Check if SPOT_SATSOLVER is given.
+    satsolver_command cmd_;
+
+    // cnf streams and associated clause counter.
+    // The next 2 pointers will be != nullptr if SPOT_SATSOLVER is given.
     temporary_file* cnf_tmp_;
     std::ostream* cnf_stream_;
-    clause_counter* nclauses_;
+    int nclauses_;
+    int nvars_;
 
+    /// \brief Picosat satsolver instance.
+    PicoSAT* psat_;
   };
 
   /// \brief Extract the solution of a SAT solver output.
   SPOT_API satsolver::solution
   satsolver_get_solution(const char* filename);
+
+}
+
+namespace spot
+{
+  template<typename T>
+  void
+  satsolver::comment_rec(T single)
+  {
+    if (!psat_)
+      *cnf_stream_ << ' ' << single;
+  }
+
+  template<typename T, typename... Args>
+  void
+  satsolver::comment_rec(T first, Args... args)
+  {
+    if (!psat_)
+    {
+      *cnf_stream_ << ' ' << first;
+      comment_rec(args...);
+    }
+  }
+
+  template<typename T>
+  void
+  satsolver::comment(T single)
+  {
+    if (!psat_)
+      *cnf_stream_ << "c " << single;
+  }
+
+  template<typename T, typename... Args>
+  void
+  satsolver::comment(T first, Args... args)
+  {
+    if (!psat_)
+    {
+      *cnf_stream_ << "c " << first;
+      comment_rec(args...);
+    }
+  }
+
 }

spot/twaalgos/dtbasat.cc

@@ -296,7 +296,7 @@ namespace spot
     typedef std::pair<int, int> sat_stats;
 
     static
-    sat_stats dtba_to_sat(satsolver solver,
+    sat_stats dtba_to_sat(satsolver& solver,
                           const const_twa_graph_ptr& ref,
                           dict& d, bool state_based)
     {
@@ -322,9 +322,11 @@ namespace spot
       // Number all the SAT variables we may need.
       unsigned ref_size = declare_vars(ref, d, ap, state_based, sm);
 
+      // Tell the satsolver the number of variables
+      solver.adjust_nvars(d.nvars);
+
       // empty automaton is impossible
-      if (d.cand_size == 0)
+      assert(d.cand_size > 0);
-        return solver.stats();
 
 #if DEBUG
       debug_dict = ref->get_dict();
@@ -602,7 +604,7 @@ namespace spot
                   }
             }
         }
-      return solver.stats(d.nvars);
+      return solver.stats();
     }
 
     static twa_graph_ptr

spot/twaalgos/dtwasat.cc

@@ -598,7 +598,7 @@ namespace spot
     typedef std::pair<int, int> sat_stats;
 
     static
-    sat_stats dtwa_to_sat(satsolver solver, const_twa_graph_ptr ref,
+    sat_stats dtwa_to_sat(satsolver& solver, const_twa_graph_ptr ref,
                            dict& d, bool state_based, bool colored)
     {
 #if DEBUG
@@ -628,9 +628,11 @@ namespace spot
       // Number all the SAT variables we may need.
       unsigned ref_size = declare_vars(ref, d, ap, state_based, sm);
 
+      // Tell the satsolver the number of variables
+      solver.adjust_nvars(d.nvars);
+
       // empty automaton is impossible
-      if (d.cand_size == 0)
+      assert(d.cand_size > 0);
-          return solver.stats();
 
 #if DEBUG
       debug_ref_acc = &ref->acc();
@@ -995,7 +997,7 @@ namespace spot
                   }
             }
         }
-      return solver.stats(d.nvars);
+      return solver.stats();
     }
 
     static twa_graph_ptr