lingeling/code/lglib.h

   1 /*-------------------------------------------------------------------------*/
   2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
   3 /*-------------------------------------------------------------------------*/
   4
   5 #ifndef lglib_h_INCLUDED
   6 #define lglib_h_INCLUDED
   7
   8 #include <stdio.h>                              // for 'FILE'
   9 #include <stdlib.h>                             // for 'int64_t'
  10
  11 //--------------------------------------------------------------------------
  12
  13 #define LGL_UNKNOWN 0
  14 #define LGL_SATISFIABLE 10
  15 #define LGL_UNSATISFIABLE 20
  16
  17 //--------------------------------------------------------------------------
  18
  19 typedef struct LGL LGL;
  20
  21 //--------------------------------------------------------------------------
  22
  23 LGL * lglinit (void);                           // constructor
  24 void lglrelease (LGL *);                        // destructor
  25
  26 // externally provided memory manager ...
  27
  28 typedef void * (*lglalloc) (void*mem, size_t);
  29 typedef void (*lgldealloc) (void*mem, void*, size_t);
  30 typedef void * (*lglrealloc) (void*mem, void *ptr, size_t old, size_t);
  31
  32 LGL * lglminit (void *mem, lglalloc, lglrealloc, lgldealloc);
  33
  34 // 'Cloning' produces identicaly behaving solvers.
  35
  36 LGL * lglclone (LGL *);
  37 LGL * lglmclone (LGL *, void *mem, lglalloc, lglrealloc, lgldealloc);
  38
  39 int lglunclone (LGL * dst, LGL * src);          // does not release 'src'
  40
  41 // 'Forking' copies only irredundant clauses and also uses internal variable
  42 // indices of the parent as external variable indices.  Thus 'parent' and
  43 // the forked off 'child' do neither exactly work the same way, nor do they
  44 // use from the API point of view the same set of variables.  They are
  45 // satisfiability equivalent.  If the child becomes unsatisfiable the parent
  46 // can be assumed to be unsatisfiable too and thus 'lgljoin' would just add
  47 // the empty clause to the parent.  If the child produces a satisfying
  48 // assignment, this assignment is turned into an assignment of the parent by
  49 // 'lgljoin'.  Parents can be forked multiple times.  A child has exactly
  50 // one parent.  Parents and children can be released independently.  Between
  51 // 'lglfork' and 'lgljoin' no other operations but further 'lglfork' are
  52 // allowed.  The effect ot multiple 'lgljoin' with the same parent is
  53 // unclear at this point.  The same memory manager is use for the child and
  54 // the parent. Options, prefix, output file and the callbacks for 'getime'
  55 // and 'onabort' are copied too (if set).
  56
  57 LGL * lglfork (LGL * parent);
  58 int lgljoin (LGL * parent, LGL * child);        // does not release 'child'
  59
  60 // Both 'Cloning' and 'Forking' can be used to implement 'Push & Pop', but
  61 // the asymmetric forking is more similar to the classical way of
  62 // implementing it, needs less resources since for instance eliminated
  63 // variables do not occupy any memory in the children, but requires lifting
  64 // back satisfying assignments explicitly (through the whole parent chain).
  65 // If these full satisfying assignments are really needed actually cloning
  66 // could be more space efficient too.  Assume you want to split the solver
  67 // into two instances, one with a literal set to false, the other one to
  68 // true. Then cloning allows you to produce two independent branches, while
  69 // for forking you need three, since the root / top solver still has to be
  70 // kept for lifting back a potential assignment.
  71
  72 //--------------------------------------------------------------------------
  73
  74 const char * lglversion ();
  75
  76 void lglbnr (const char * name,
  77              const char * prefix,
  78              FILE * file);                      // ... banner
  79
  80 void lglusage (LGL *);                          // print usage "-h"
  81 void lglopts (LGL *, const char * prefix, int); // ... defaults "-d" | "-e"
  82 void lglrgopts (LGL *);                         // ... option ranges "-r"
  83 void lglpcs (LGL *, int mixed);                 // ... PCS file
  84 void lglsizes (LGL *);                          // ... data structure sizes
  85
  86 //--------------------------------------------------------------------------
  87 // setters and getters for options
  88
  89 void lglsetout (LGL *, FILE*);                  // output file for report
  90 void lglsetprefix (LGL *, const char*);         // prefix for messages
  91
  92 FILE * lglgetout (LGL *);
  93 const char * lglgetprefix (LGL *);
  94
  95 void lglsetopt (LGL *, const char *, int);      // set option value
  96 int lglreadopts (LGL *, FILE *);                // read and set options
  97 int lglgetopt (LGL *, const char *);            // get option value
  98 int lglhasopt (LGL *, const char *);            // exists option?
  99
 100 int lglgetoptminmax (LGL *, const char *, int * minptr, int * maxptr);
 101
 102 void * lglfirstopt (LGL *);                     // option iterator: first
 103
 104 void * lglnextopt (LGL *,                       // option iterator: next
 105                    void * iterator,
 106                    const char ** nameptr,
 107                    int *valptr, int *minptr, int *maxptr);
 108
 109 // individual ids for logging and statistics:
 110
 111 void lglsetid (LGL *, int tid, int tids);
 112
 113 // Set default phase of a literal.  Any decision on this literal will always
 114 // try this phase.  Note, that this function does not have any effect on
 115 // eliminated variables.  Further equivalent variables share the same forced
 116 // phase and thus if they are set to different default phases, only the last
 117 // set operation will be kept.
 118
 119 void lglsetphase (LGL *, int lit);
 120 void lglresetphase (LGL *, int lit);    // Stop forcing phase in decisions.
 121
 122 // Assume the solver is in the SATISFIABLE state (after 'lglsat' or
 123 // 'lglsimp'), then calling 'lglsetphases' will copy the current assignment
 124 // as default phases.
 125
 126 void lglsetphases (LGL *);
 127
 128 //--------------------------------------------------------------------------
 129 // call back for abort
 130
 131 void lglonabort (LGL *, void * state, void (*callback)(void* state));
 132
 133 //--------------------------------------------------------------------------
 134 // write and read API trace
 135
 136 void lglwtrapi (LGL *, FILE *);
 137 void lglrtrapi (LGL *, FILE *);
 138
 139 //--------------------------------------------------------------------------
 140 // traverse units, equivalences, remaining clauses, or all clauses:
 141
 142 void lglutrav (LGL *, void * state, void (*trav)(void *, int unit));
 143 void lgletrav (LGL *, void * state, void (*trav)(void *, int lit, int repr));
 144 void lglctrav (LGL *, void * state, void (*trav)(void *, int lit));
 145 void lgltravall (LGL *, void * state, void (*trav)(void *state, int lit));
 146
 147 //--------------------------------------------------------------------------
 148
 149 void lglprint (LGL *, FILE *);                  // remaining in DIMACS format
 150 void lglprintall (LGL *, FILE *);               // including units & equivs
 151
 152 //--------------------------------------------------------------------------
 153 // main interface as in PicoSAT (see 'picosat.h' for more information)
 154
 155 int lglmaxvar (LGL *);
 156 int lglincvar (LGL *);
 157
 158 void lgladd (LGL *, int lit);
 159 void lglassume (LGL *, int lit);                // assume single units
 160
 161 void lglcassume (LGL *, int lit);               // assume clause
 162                                                 // (at most one)
 163
 164 void lglfixate (LGL *);                         // add assumptions as units
 165
 166 int lglsat (LGL *);
 167 int lglsimp (LGL *, int iterations);
 168
 169 int lglderef (LGL *, int lit);                  // neg=false, pos=true
 170 int lglfixed (LGL *, int lit);                  // ditto but toplevel
 171
 172 int lglfailed (LGL *, int lit);                 // ditto for assumptions
 173 int lglinconsistent (LGL *);                    // contains empty clause?
 174 int lglchanged (LGL *);                         // model changed
 175
 176 void lglreducecache (LGL *);                    // reset cache size
 177 void lglflushcache (LGL *);                     // flush all learned clauses
 178
 179 /*------------------------------------------------------------------------*/
 180
 181 /* Return representative from equivalence class if literal is not top-level
 182  * assigned nor eliminated.
 183  */
 184 int lglrepr (LGL *, int lit);
 185
 186 /* Set 'startptr' and 'toptr' to the 'start' and 'top' of the reconstruction
 187  * stack, which is used in BCE, BVE and CCE for reconstructing a solution
 188  * after eliminating variables or clauses.  These pointers are only valid
 189  * until the next 'lglsat/lglsimp' call.
 190  */
 191 void lglreconstk (LGL * lgl, int ** startptr, int ** toptr);
 192
 193 //--------------------------------------------------------------------------
 194 // Multiple-Objective SAT tries to solve multiple objectives at the same
 195 // time.  If a target can be satisfied or falsified the user is notified via
 196 // a callback function of type 'lglnotify'. The argument is an abstract
 197 // state (of the user), the target literal and as last argument the value
 198 // (-1 = unsatisfiable, 1 = satisfiable).  If the notification callback
 199 // returns 1 the 'lglmosat' procedure continues, otherwise it stops.  It
 200 // returns a non zero value iff only all targets have been either proved to
 201 // be satisfiable or unsatisfiable.  Even if 'val' given to the notification
 202 // function is '1', it can not assume that the current assignment is
 203 // complete, e.g. satisfies the formula.
 204 //
 205 typedef int (*lglnotify)(void *state, int target, int val);
 206
 207 int lglmosat (LGL *, void * state, lglnotify, int * targets);
 208
 209 //--------------------------------------------------------------------------
 210 // Incremental interface provides reference counting for indices, i.e.
 211 // unfrozen indices become invalid after next 'lglsat' (or 'lglsimp').
 212 // This is actually a reference counter for variable indices still in use
 213 // after the next 'lglsat' or 'lglsimp' call.  It is actually variable based
 214 // and only applies to literals in new clauses or used as assumptions,
 215 // e.g. in calls to 'lgladd' and 'lglassume'.
 216 //
 217 // The following example is actually compilable and used for explaining
 218 // all the details of this rather complicated incremental API contract:
 219
 220 /***** start of incremental example ***************************************
 221
 222 #include "lglib.h"
 223
 224 #ifdef NDEBUG
 225 #undef NDEBUG
 226 #endif
 227
 228 #include <assert.h>
 229
 230 int main () {
 231   LGL * lgl = lglinit ();
 232   int res;
 233   lgladd (lgl, -14); lgladd (lgl, 2); lgladd (lgl, 0);  // binary clause
 234   lgladd (lgl, 14); lgladd (lgl, -1); lgladd (lgl, 0);  // binary clause
 235   lglassume (lgl, 1);                                   // assume '1'
 236   lglfreeze (lgl, 1);                                   // will use '1' below
 237   lglfreeze (lgl, 14);                                  // will use '14 too
 238   assert (lglfrozen (lgl, 1));
 239   assert (lglfrozen (lgl, 14));
 240   res = lglsat (lgl);
 241   assert (res == 10);
 242   (void) lglderef (lgl, 1);                             // fine
 243   (void) lglderef (lgl, 2);                             // fine
 244   (void) lglderef (lgl, 3);                             // fine !
 245   (void) lglderef (lgl, 14);                            // fine
 246   assert (!lglusable (lgl, 2));
 247   // lgladd (lgl, 2);                                   // ILLEGAL
 248   // lglassume (lgl, 2);                                // ILLEGAL
 249   assert (lglusable (lgl, 15));                         // '15' not used yet!
 250   lgladd (lgl, -14); lgladd (lgl, 1); lgladd (lgl, 0);  // binary clause
 251   lgladd (lgl, 15); lgladd (lgl, 0);                    // fine!
 252   lglmelt (lgl, 14);                                    // '1' discarded
 253   res = lglsat (lgl);
 254   assert (res == 10);
 255   assert (lglfrozen (lgl, 1));
 256   (void) lglderef (lgl, 1);                             // fine
 257   (void) lglderef (lgl, 2);                             // fine
 258   (void) lglderef (lgl, 3);                             // fine
 259   (void) lglderef (lgl, 14);                            // fine
 260   (void) lglderef (lgl, 15);                            // fine
 261   assert (!lglusable (lgl, 2));
 262   assert (!lglusable (lgl, 14));
 263   // lglassume (lgl, 2);                                // ILLEGAL
 264   // lglassume (lgl, 14);                               // ILLEGAL
 265   lgladd (lgl, 1);                                      // still frozen
 266   lglmelt (lgl, 1);
 267   lgladd (lgl, 0);
 268   res = lglsat (lgl);
 269   // none frozen
 270   assert (!lglusable (lgl, 1));
 271   // lgladd(lgl, 1);                                    // ILLEGAL
 272   lglsetopt (lgl, "plain", 1);                          // disable BCE ...
 273   lgladd (lgl, 8); lgladd (lgl, -9); lgladd (lgl, 0);
 274   res = lglsat (lgl);
 275   assert (res == 10);
 276   assert (!lglusable (lgl, 8));
 277   assert (!lglusable (lgl, -9));
 278   assert (lglreusable (lgl, 8));
 279   assert (lglreusable (lgl, -9));
 280   lglreuse (lgl, 8);
 281   lgladd (lgl, -8); lgladd (lgl, 0);
 282   lglsetopt (lgl, "plain", 0);                          // enable BCE ...
 283   res = lglsat (lgl);
 284   assert (res);
 285   return res;
 286 }
 287
 288 ****** end of incremental example ****************************************/
 289
 290 void lglfreeze (LGL *, int lit);
 291 int lglfrozen (LGL *, int lit);
 292
 293 void lglmelt (LGL *, int lit);
 294 void lglmeltall (LGL *);                                // melt all literals
 295
 296 // If a literal was not frozen at the last call to 'lglsat' (or 'lglsimp')
 297 // it becomes 'unusable' after the next call even though it might not
 298 // have been used as blocking literal etc.  This
 299
 300 int lglusable (LGL *, int lit);
 301 int lglreusable (LGL *, int lit);
 302 void lglreuse (LGL *, int lit);
 303
 304 //--------------------------------------------------------------------------
 305 // Returns a good look ahead literal or zero if all potential literals have
 306 // been eliminated or have been used as blocking literals in blocked clause
 307 // elimination.  Zero is also returned if the formula is already
 308 // inconsistent.  The lookahead literal is made usable again, for instance
 309 // if it was not frozen during a previous SAT call and thus implicitly
 310 // became melted.  Therefore it can be added in a unit clause.
 311
 312 int lglookahead (LGL *);
 313
 314 //--------------------------------------------------------------------------
 315 // stats:
 316
 317 void lglflushtimers (LGL *lgl);                 // after interrupt etc.
 318
 319 void lglstats (LGL *);
 320 int64_t lglgetconfs (LGL *);
 321 int64_t lglgetdecs (LGL *);
 322 int64_t lglgetprops (LGL *);
 323 size_t lglbytes (LGL *);
 324 int lglnvars (LGL *);
 325 int lglnclauses (LGL *);
 326 double lglmb (LGL *);
 327 double lglmaxmb (LGL *);
 328 double lglsec (LGL *);
 329 double lglprocesstime (void);
 330
 331 //--------------------------------------------------------------------------
 332 // low-level parallel support through call backs
 333
 334 void lglseterm (LGL *, int (*term)(void*), void*);
 335
 336 void lglsetproduceunit (LGL *, void (*produce)(void*, int), void*);
 337 void lglsetconsumeunits (LGL *, void (*consume)(void*,int**,int**), void*);
 338 void lglsetconsumedunits (LGL *, void (*consumed)(void*,int), void*);
 339
 340 void lglsetproducecls (LGL*, void(*produce)(void*,int*,int glue),void*);
 341 void lglsetconsumecls (LGL*,void(*consume)(void*,int**,int *glueptr),void*);
 342 void lglsetconsumedcls (LGL *, void (*consumed)(void*,int), void*);
 343
 344 void lglsetlockeq (LGL *, int * (*lock)(void*), void *);
 345 void lglsetunlockeq (LGL *, void (*unlock)(void*,int cons,int prod), void *);
 346
 347 void lglsetmsglock (LGL *, void (*lock)(void*), void (*unlock)(void*), void*);
 348 void lglsetime (LGL *, double (*time)(void));
 349
 350 #endif