diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 20:01:00 -0800 |
commit | 0c6505a26a537dc911b6566f82d759521e527c08 (patch) | |
tree | f2687995efd4943fe3b1307fce7ef5942d0a57b3 /src/sat/msat/msat.h | |
parent | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (diff) | |
download | abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.gz abc-0c6505a26a537dc911b6566f82d759521e527c08.tar.bz2 abc-0c6505a26a537dc911b6566f82d759521e527c08.zip |
Version abc80130_2
Diffstat (limited to 'src/sat/msat/msat.h')
-rw-r--r-- | src/sat/msat/msat.h | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 21ddcb81..53353ba6 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -21,6 +21,10 @@ #ifndef __MSAT_H__ #define __MSAT_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -65,7 +69,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// MACRO DEFITIONS /// +/// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// @@ -76,10 +80,10 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t; 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_SolverAddVar( Msat_Solver_t * p, int Level ); 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 ); +extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); // printing stats, assignments, and clauses extern void Msat_SolverPrintStats( Msat_Solver_t * p ); extern void Msat_SolverPrintAssignment( Msat_Solver_t * p ); @@ -87,17 +91,20 @@ 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_SolverReadClauseNum( 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 int Msat_SolverReadInspects( 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 ); +extern float * Msat_SolverReadFactors( 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 ); @@ -153,8 +160,13 @@ 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 ); + +#ifdef __cplusplus +} +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#endif |