diff options
Diffstat (limited to 'src/sat/msat/msat.h')
| -rw-r--r-- | src/sat/msat/msat.h | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h new file mode 100644 index 00000000..21ddcb81 --- /dev/null +++ b/src/sat/msat/msat.h @@ -0,0 +1,160 @@ +/**CFile**************************************************************** + + FileName [msat.h] + + PackageName [A C version of SAT solver MINISAT, originally developed + in C++ by Niklas Een and Niklas Sorensson, Chalmers University of + Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] + + Synopsis [External definitions of the solver.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $] + +***********************************************************************/ + +#ifndef __MSAT_H__ +#define __MSAT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef bool +#undef bool +#endif + +#ifndef __MVTYPES_H__ +typedef int bool; +#endif + +typedef struct Msat_Solver_t_ Msat_Solver_t; + +// the vector of intergers and of clauses +typedef struct Msat_IntVec_t_ Msat_IntVec_t; +typedef struct Msat_ClauseVec_t_ Msat_ClauseVec_t; +typedef struct Msat_VarHeap_t_ Msat_VarHeap_t; + +// the return value of the solver +typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; + +// representation of variables and literals +// the literal (l) is the variable (v) and the sign (s) +// s = 0 the variable is positive +// s = 1 the variable is negative +#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) +#define MSAT_LITNOT(l) ((l)^1) +#define MSAT_LITSIGN(l) ((l)&1) +#define MSAT_LIT2VAR(l) ((l)>>1) + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== satRead.c ============================================================*/ +extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose ); +/*=== satSolver.c ===========================================================*/ +// adding vars, clauses, simplifying the database, and solving +extern bool Msat_SolverAddVar( Msat_Solver_t * p ); +extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); +extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p ); +extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit ); +// printing stats, assignments, and clauses +extern void Msat_SolverPrintStats( Msat_Solver_t * p ); +extern void Msat_SolverPrintAssignment( Msat_Solver_t * p ); +extern void Msat_SolverPrintClauses( Msat_Solver_t * p ); +extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ); +// access to the solver internal data +extern int Msat_SolverReadVarNum( Msat_Solver_t * p ); +extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ); +extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ); +extern int * Msat_SolverReadModelArray( Msat_Solver_t * p ); +extern unsigned Msat_SolverReadTruth( Msat_Solver_t * p ); +extern int Msat_SolverReadBackTracks( Msat_Solver_t * p ); +extern void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ); +extern void Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof ); +extern void Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var ); +extern void Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap ); +extern void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ); +extern void Msat_SolverMarkClausesStart( Msat_Solver_t * p ); +// returns the solution after incremental solving +extern int Msat_SolverReadSolutions( Msat_Solver_t * p ); +extern int * Msat_SolverReadSolutionsArray( Msat_Solver_t * p ); +extern Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p ); +extern Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p ); +extern Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p ); +/*=== satSolverSearch.c ===========================================================*/ +extern void Msat_SolverRemoveLearned( Msat_Solver_t * p ); +extern void Msat_SolverRemoveMarked( Msat_Solver_t * p ); +/*=== satSolverApi.c ===========================================================*/ +// allocation, cleaning, and freeing the solver +extern Msat_Solver_t * Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose ); +extern void Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc ); +extern void Msat_SolverClean( Msat_Solver_t * p, int nVars ); +extern void Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars ); +extern void Msat_SolverFree( Msat_Solver_t * p ); +/*=== satVec.c ===========================================================*/ +extern Msat_IntVec_t * Msat_IntVecAlloc( int nCap ); +extern Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize ); +extern Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize ); +extern Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec ); +extern Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec ); +extern void Msat_IntVecFree( Msat_IntVec_t * p ); +extern void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry ); +extern int * Msat_IntVecReleaseArray( Msat_IntVec_t * p ); +extern int * Msat_IntVecReadArray( Msat_IntVec_t * p ); +extern int Msat_IntVecReadSize( Msat_IntVec_t * p ); +extern int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i ); +extern int Msat_IntVecReadEntryLast( Msat_IntVec_t * p ); +extern void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry ); +extern void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin ); +extern void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew ); +extern void Msat_IntVecClear( Msat_IntVec_t * p ); +extern void Msat_IntVecPush( Msat_IntVec_t * p, int Entry ); +extern int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry ); +extern void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease ); +extern int Msat_IntVecPop( Msat_IntVec_t * p ); +extern void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse ); +/*=== satHeap.c ===========================================================*/ +extern Msat_VarHeap_t * Msat_VarHeapAlloc(); +extern void Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity ); +extern void Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc ); +extern void Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize ); +extern void Msat_VarHeapStop( Msat_VarHeap_t * p ); +extern void Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p ); +extern void Msat_VarHeapCheck( Msat_VarHeap_t * p ); +extern void Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar ); +extern int Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar ); +extern void Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar ); +extern void Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar ); +extern void Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar ); +extern double Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p ); +extern int Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit ); +extern int Msat_VarHeapReadMax( Msat_VarHeap_t * p ); +extern int Msat_VarHeapGetMax( Msat_VarHeap_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +#endif |