abc70930: src/sat/msat/msat.h Source File

00001 
00021 #ifndef __MSAT_H__
00022 #define __MSAT_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif
00027 
00031 
00035 
00039 
00040 #ifdef bool
00041 #undef bool
00042 #endif
00043 
00044 #ifndef __MVTYPES_H__
00045 typedef int  bool;
00046 #endif
00047 
00048 typedef struct Msat_Solver_t_      Msat_Solver_t;
00049 
00050 // the vector of intergers and of clauses
00051 typedef struct Msat_IntVec_t_      Msat_IntVec_t;
00052 typedef struct Msat_ClauseVec_t_   Msat_ClauseVec_t;
00053 typedef struct Msat_VarHeap_t_     Msat_VarHeap_t;
00054 
00055 // the return value of the solver
00056 typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
00057 
00058 // representation of variables and literals
00059 // the literal (l) is the variable (v) and the sign (s)
00060 // s = 0 the variable is positive
00061 // s = 1 the variable is negative
00062 #define MSAT_VAR2LIT(v,s) (2*(v)+(s)) 
00063 #define MSAT_LITNOT(l)    ((l)^1)
00064 #define MSAT_LITSIGN(l)   ((l)&1)     
00065 #define MSAT_LIT2VAR(l)   ((l)>>1)
00066 
00070 
00074 
00078 
00079 /*=== satRead.c ============================================================*/
00080 extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
00081 /*=== satSolver.c ===========================================================*/
00082 // adding vars, clauses, simplifying the database, and solving
00083 extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
00084 extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
00085 extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
00086 extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
00087 // printing stats, assignments, and clauses
00088 extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
00089 extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
00090 extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
00091 extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
00092 // access to the solver internal data
00093 extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
00094 extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
00095 extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
00096 extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
00097 extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
00098 extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
00099 extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
00100 extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
00101 extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
00102 extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
00103 extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
00104 extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
00105 extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
00106 extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
00107 extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
00108 // returns the solution after incremental solving
00109 extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
00110 extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
00111 extern Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p );
00112 extern Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p );
00113 extern Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p );
00114 /*=== satSolverSearch.c ===========================================================*/
00115 extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
00116 extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
00117 /*=== satSolverApi.c ===========================================================*/
00118 // allocation, cleaning, and freeing the solver
00119 extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose );
00120 extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
00121 extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
00122 extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
00123 extern void             Msat_SolverFree( Msat_Solver_t * p );
00124 /*=== satVec.c ===========================================================*/
00125 extern Msat_IntVec_t *  Msat_IntVecAlloc( int nCap );
00126 extern Msat_IntVec_t *  Msat_IntVecAllocArray( int * pArray, int nSize );
00127 extern Msat_IntVec_t *  Msat_IntVecAllocArrayCopy( int * pArray, int nSize );
00128 extern Msat_IntVec_t *  Msat_IntVecDup( Msat_IntVec_t * pVec );
00129 extern Msat_IntVec_t *  Msat_IntVecDupArray( Msat_IntVec_t * pVec );
00130 extern void             Msat_IntVecFree( Msat_IntVec_t * p );
00131 extern void             Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry );
00132 extern int *            Msat_IntVecReleaseArray( Msat_IntVec_t * p );
00133 extern int *            Msat_IntVecReadArray( Msat_IntVec_t * p );
00134 extern int              Msat_IntVecReadSize( Msat_IntVec_t * p );
00135 extern int              Msat_IntVecReadEntry( Msat_IntVec_t * p, int i );
00136 extern int              Msat_IntVecReadEntryLast( Msat_IntVec_t * p );
00137 extern void             Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry );
00138 extern void             Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin );
00139 extern void             Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew );
00140 extern void             Msat_IntVecClear( Msat_IntVec_t * p );
00141 extern void             Msat_IntVecPush( Msat_IntVec_t * p, int Entry );
00142 extern int              Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry );
00143 extern void             Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease );
00144 extern int              Msat_IntVecPop( Msat_IntVec_t * p );
00145 extern void             Msat_IntVecSort( Msat_IntVec_t * p, int fReverse );
00146 /*=== satHeap.c ===========================================================*/
00147 extern Msat_VarHeap_t * Msat_VarHeapAlloc();
00148 extern void             Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity );
00149 extern void             Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
00150 extern void             Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize );
00151 extern void             Msat_VarHeapStop( Msat_VarHeap_t * p );
00152 extern void             Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p );
00153 extern void             Msat_VarHeapCheck( Msat_VarHeap_t * p );
00154 extern void             Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar );
00155 extern int              Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar );
00156 extern void             Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar );  
00157 extern void             Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar );  
00158 extern void             Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar );  
00159 extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
00160 extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
00161 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
00162 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
00163  
00164 #ifdef __cplusplus
00165 }
00166 #endif
00167 
00168 #endif
00169