lglib.h

/*-------------------------------------------------------------------------*/
/* Copyright 2010-2020 Armin Biere Johannes Kepler University Linz Austria */
/*-------------------------------------------------------------------------*/

#ifndef lglib_h_INCLUDED
#define lglib_h_INCLUDED

#include <stdio.h>				// for 'FILE'
#include <stdlib.h>				// for 'int64_t'

//--------------------------------------------------------------------------

#define LGL_UNKNOWN 0
#define LGL_SATISFIABLE 10
#define LGL_UNSATISFIABLE 20

//--------------------------------------------------------------------------

typedef struct LGL LGL;

//--------------------------------------------------------------------------

LGL * lglinit (void);				// constructor
void lglrelease (LGL *);			// destructor

// externally provided memory manager ...

typedef void * (*lglalloc) (void*mem, size_t);
typedef void (*lgldealloc) (void*mem, void*, size_t);
typedef void * (*lglrealloc) (void*mem, void *ptr, size_t old, size_t);

LGL * lglminit (void *mem, lglalloc, lglrealloc, lgldealloc);

// 'Cloning' produces identicaly behaving solvers.

LGL * lglclone (LGL *);
LGL * lglmclone (LGL *, void *mem, lglalloc, lglrealloc, lgldealloc);

int lglunclone (LGL * dst, LGL * src);		// does not release 'src'

// 'Forking' copies only irredundant clauses and also uses internal variable
// indices of the parent as external variable indices.  Thus 'parent' and
// the forked off 'child' do neither exactly work the same way, nor do they
// use from the API point of view the same set of variables.  They are
// satisfiability equivalent.  If the child becomes unsatisfiable the parent
// can be assumed to be unsatisfiable too and thus 'lgljoin' would just add
// the empty clause to the parent.  If the child produces a satisfying
// assignment, this assignment is turned into an assignment of the parent by
// 'lgljoin'.  Parents can be forked multiple times.  A child has exactly
// one parent.  Parents and children can be released independently.  Between
// 'lglfork' and 'lgljoin' no other operations but further 'lglfork' are
// allowed.  The effect ot multiple 'lgljoin' with the same parent is
// unclear at this point.  The same memory manager is use for the child and
// the parent. Options, prefix, output file and the callbacks for 'getime'
// and 'onabort' are copied too (if set).

LGL * lglfork (LGL * parent);
int lgljoin (LGL * parent, LGL * child);	// does not release 'child'

// Both 'Cloning' and 'Forking' can be used to implement 'Push & Pop', but
// the asymmetric forking is more similar to the classical way of
// implementing it, needs less resources since for instance eliminated
// variables do not occupy any memory in the children, but requires lifting
// back satisfying assignments explicitly (through the whole parent chain).
// If these full satisfying assignments are really needed actually cloning
// could be more space efficient too.  Assume you want to split the solver
// into two instances, one with a literal set to false, the other one to
// true. Then cloning allows you to produce two independent branches, while
// for forking you need three, since the root / top solver still has to be
// kept for lifting back a potential assignment.

//--------------------------------------------------------------------------

const char * lglparsefile (LGL *, FILE *, int force,
                           int * lineno_ptr, int * max_var_ptr);

const char * lglparsepath (LGL *, const char * path, int force,
                           int * lineno_ptr, int * max_var_ptr);

//--------------------------------------------------------------------------

const char * lglversion ();

void lglbnr (const char * name,
             const char * prefix,
	     FILE * file);			// ... banner

void lglusage (LGL *);				// print usage "-h"
void lglopts (LGL *, const char * prefix, int);	// ... defaults "-d" | "-e"
void lglrgopts (LGL *);				// ... option ranges "-r"
void lglpcs (LGL *, int mixed);			// ... PCS file
void lglsizes (LGL *);				// ... data structure sizes

//--------------------------------------------------------------------------
// setters and getters for options

void lglsetout (LGL *, FILE*);			// output file for report
void lglsetrace (LGL *, FILE*);			// set trace output file
void lglsetprefix (LGL *, const char*);		// prefix for messages

FILE * lglgetout (LGL *);
const char * lglgetprefix (LGL *);

void lglsetopt (LGL *, const char *, int);	// set option value
int lglreadopts (LGL *, FILE *);		// read and set options
int lglgetopt (LGL *, const char *);		// get option value
int lgldefopt (LGL *, const char *);		// get default value
int lglhasopt (LGL *, const char *);		// exists option?

int lglgetoptminmax (LGL *, const char *, int * minptr, int * maxptr);

void * lglfirstopt (LGL *);			// option iterator: first

void * lglnextopt (LGL *, 			// option iterator: next
                   void * iterator, 
                   const char ** nameptr,
		   int *valptr, int *minptr, int *maxptr);

// individual ids for logging and statistics:

void lglsetid (LGL *, int tid, int tids);

// Set default phase of a literal.  Any decision on this literal will always
// try this phase.  Note, that this function does not have any effect on
// eliminated variables.  Further equivalent variables share the same forced 
// phase and thus if they are set to different default phases, only the last
// set operation will be kept.

void lglsetphase (LGL *, int lit);
void lglresetphase (LGL *, int lit);	// Stop forcing phase in decisions.

// Prefer decisions on 'important' variables.

void lglsetimportant (LGL *, int lit);

// Assume the solver is in the SATISFIABLE state (after 'lglsat' or
// 'lglsimp'), then calling 'lglsetphases' will copy the current assignment
// as default phases.

void lglsetphases (LGL *);

//--------------------------------------------------------------------------
// call back for abort

void lglonabort (LGL *, void * state, void (*callback)(void* state));

//--------------------------------------------------------------------------
// write and read API trace

void lglwtrapi (LGL *, FILE *);
void lglrtrapi (LGL *, FILE *);

//--------------------------------------------------------------------------
// traverse units, equivalences, remaining clauses, or all clauses:

void lglutrav (LGL *, void * state, void (*trav)(void *, int unit));
void lgletrav (LGL *, void * state, void (*trav)(void *, int lit, int repr));
void lglctrav (LGL *, void * state, void (*trav)(void *, int lit));
void lgltravall (LGL *, void * state, void (*trav)(void *state, int lit));

//--------------------------------------------------------------------------

void lglprint (LGL *, FILE *);			// remaining in DIMACS format
void lglprintall (LGL *, FILE *);		// including units & equivs

//--------------------------------------------------------------------------
// main interface as in PicoSAT (see 'picosat.h' for more information)

int lglmaxvar (LGL *);
int lglincvar (LGL *);

void lgladd (LGL *, int lit);
void lglassume (LGL *, int lit);		// assume single units

void lglcassume (LGL *, int lit);		// assume clause
						// (at most one)

void lglfixate (LGL *);				// add assumptions as units

int lglsat (LGL *);
int lglsimp (LGL *, int iterations);

int lglderef (LGL *, int lit);			// neg=false, pos=true
int lglfixed (LGL *, int lit);			// ditto but toplevel

int lglfailed (LGL *, int lit);			// ditto for assumptions
int lglinconsistent (LGL *);			// contains empty clause?
int lglchanged (LGL *);				// model changed

void lglreducecache (LGL *);			// reset cache size
void lglflushcache (LGL *);			// flush all learned clauses

/*------------------------------------------------------------------------*/

/* Return representative from equivalence class if literal is not top-level
 * assigned nor eliminated.
 */
int lglrepr (LGL *, int lit);

/* Set 'startptr' and 'toptr' to the 'start' and 'top' of the reconstruction
 * stack, which is used in BCE, BVE and CCE for reconstructing a solution
 * after eliminating variables or clauses.  These pointers are only valid
 * until the next 'lglsat/lglsimp' call.
 */
void lglreconstk (LGL * lgl, int ** startptr, int ** toptr);

//--------------------------------------------------------------------------
// Incremental interface provides reference counting for indices, i.e.
// unfrozen indices become invalid after next 'lglsat' (or 'lglsimp').
// This is actually a reference counter for variable indices still in use
// after the next 'lglsat' or 'lglsimp' call.  It is actually variable based
// and only applies to literals in new clauses or used as assumptions,
// e.g. in calls to 'lgladd' and 'lglassume'.
//
// The following example is actually compilable and used for explaining
// all the details of this rather complicated incremental API contract:

/***** start of incremental example ***************************************

#include "lglib.h"

#ifdef NDEBUG
#undef NDEBUG
#endif

#include <assert.h>

int main () {
  LGL * lgl = lglinit ();
  int res;
  lgladd (lgl, -14); lgladd (lgl, 2); lgladd (lgl, 0);  // binary clause
  lgladd (lgl, 14); lgladd (lgl, -1); lgladd (lgl, 0);  // binary clause
  lglassume (lgl, 1);                                   // assume '1'
  lglfreeze (lgl, 1);                                   // will use '1' below
  lglfreeze (lgl, 14);                                  // will use '14 too
  assert (lglfrozen (lgl, 1));
  assert (lglfrozen (lgl, 14));
  res = lglsat (lgl);
  assert (res == 10);
  (void) lglderef (lgl, 1);                             // fine
  (void) lglderef (lgl, 2);                             // fine
  (void) lglderef (lgl, 3);                             // fine !
  (void) lglderef (lgl, 14);                            // fine
  assert (!lglusable (lgl, 2));
  // lgladd (lgl, 2);                                   // ILLEGAL
  // lglassume (lgl, 2);                                // ILLEGAL
  assert (lglusable (lgl, 15));				// '15' not used yet!
  lgladd (lgl, -14); lgladd (lgl, 1); lgladd (lgl, 0);  // binary clause
  lgladd (lgl, 15); lgladd (lgl, 0);                    // fine!
  lglmelt (lgl, 14);                                    // '1' discarded
  res = lglsat (lgl);
  assert (res == 10);
  assert (lglfrozen (lgl, 1));
  (void) lglderef (lgl, 1);                             // fine
  (void) lglderef (lgl, 2);                             // fine
  (void) lglderef (lgl, 3);                             // fine
  (void) lglderef (lgl, 14);                            // fine
  (void) lglderef (lgl, 15);                            // fine
  assert (!lglusable (lgl, 2));
  assert (!lglusable (lgl, 14));
  // lglassume (lgl, 2);                                // ILLEGAL
  // lglassume (lgl, 14);                               // ILLEGAL
  lgladd (lgl, 1);                                      // still frozen
  lglmelt (lgl, 1);
  lgladd (lgl, 0);
  res = lglsat (lgl);
  assert (res == 10);					// TODO right?
  // none frozen
  assert (!lglusable (lgl, 1));
  // lgladd(lgl, 1);                                    // ILLEGAL
  lglsetopt (lgl, "plain", 1);				// disable BCE ...
  lgladd (lgl, 8); lgladd (lgl, -9); lgladd (lgl, 0);
  res = lglsat (lgl);
  assert (res == 10);
  assert (!lglusable (lgl, 8));
  assert (!lglusable (lgl, -9));
  assert (lglreusable (lgl, 8));
  assert (lglreusable (lgl, -9));
  lglreuse (lgl, 8);
  lgladd (lgl, -8); lgladd (lgl, 0);
  lglsetopt (lgl, "plain", 0);				// enable BCE ...
  res = lglsat (lgl);
  assert (res);
  return res;
}

****** end of incremental example ****************************************/

void lglfreeze (LGL *, int lit);
int lglfrozen (LGL *, int lit);

void lglmelt (LGL *, int lit);
void lglmeltall (LGL *);				// melt all literals

// If a literal was not frozen at the last call to 'lglsat' (or 'lglsimp')
// it becomes 'unusable' after the next call even though it might not
// have been used as blocking literal etc.  This

int lglusable (LGL *, int lit);
int lglreusable (LGL *, int lit);
void lglreuse (LGL *, int lit);

//--------------------------------------------------------------------------
// Returns a good look ahead literal or zero if all potential literals have
// been eliminated or have been used as blocking literals in blocked clause
// elimination.  Zero is also returned if the formula is already
// inconsistent.  The lookahead literal is made usable again, for instance
// if it was not frozen during a previous SAT call and thus implicitly
// became melted.  Therefore it can be added in a unit clause.

int lglookahead (LGL *);

//--------------------------------------------------------------------------
// stats:

void lglflushtimers (LGL *lgl);			// after interrupt etc.

void lglstats (LGL *);
int64_t lglgetconfs (LGL *);
int64_t lglgetdecs (LGL *);
int64_t lglgetprops (LGL *);
size_t lglbytes (LGL *);
int lglnvars (LGL *);
int lglnclauses (LGL *);
double lglmb (LGL *);
double lglmaxmb (LGL *);
double lglsec (LGL *);
double lglprocesstime (void);

//--------------------------------------------------------------------------
// low-level parallel support through call backs

void lglseterm (LGL *, int (*term)(void*), void*);

void lglsetproduceunit (LGL *, void (*produce)(void*, int), void*);
void lglsetconsumeunits (LGL *, void (*consume)(void*,int**,int**), void*);
void lglsetconsumedunits (LGL *, void (*consumed)(void*,int), void*);

void lglsetproducecls (LGL*, void(*produce)(void*,int*,int glue),void*);
void lglsetconsumecls (LGL*,void(*consume)(void*,int**,int *glueptr),void*);
void lglsetconsumedcls (LGL *, void (*consumed)(void*,int), void*);

void lglsetlockeq (LGL *, int * (*lock)(void*), void *);
void lglsetunlockeq (LGL *, void (*unlock)(void*,int cons,int prod), void *);

void lglsetmsglock (LGL *, void (*lock)(void*), void (*unlock)(void*), void*);
void lglsetime (LGL *, double (*time)(void));

#endif