1 // C-language header for MiniSat 1.14p 2 3 #ifndef ABC__sat__psat__m114p_h 4 #define ABC__sat__psat__m114p_h 5 6 7 #include "m114p_types.h" 8 9 ABC_NAMESPACE_HEADER_START 10 11 12 // SAT solver APIs 13 extern M114p_Solver_t M114p_SolverNew( int fRecordProof ); 14 extern void M114p_SolverDelete( M114p_Solver_t s ); 15 extern void M114p_SolverPrintStats( M114p_Solver_t s, double Time ); 16 extern void M114p_SolverSetVarNum( M114p_Solver_t s, int nVars ); 17 extern int M114p_SolverAddClause( M114p_Solver_t s, lit* begin, lit* end ); 18 extern int M114p_SolverSimplify( M114p_Solver_t s ); 19 extern int M114p_SolverSolve( M114p_Solver_t s, lit* begin, lit* end, int nConfLimit ); 20 extern int M114p_SolverGetConflictNum( M114p_Solver_t s ); 21 22 // proof status APIs 23 extern int M114p_SolverProofIsReady( M114p_Solver_t s ); 24 extern void M114p_SolverProofSave( M114p_Solver_t s, char * pFileName ); 25 extern int M114p_SolverProofClauseNum( M114p_Solver_t s ); 26 27 // proof traversal APIs 28 extern int M114p_SolverGetFirstRoot( M114p_Solver_t s, int ** ppLits ); 29 extern int M114p_SolverGetNextRoot( M114p_Solver_t s, int ** ppLits ); 30 extern int M114p_SolverGetFirstChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); 31 extern int M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); 32 33 // iterator over the root clauses (should be called first) 34 #define M114p_SolverForEachRoot( s, ppLits, nLits, i ) \ 35 for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits; \ 36 i++, nLits = M114p_SolverGetNextRoot(s, ppLits) ) 37 38 // iterator over the learned clauses (should be called after iterating over roots) 39 #define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i ) \ 40 for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \ 41 i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) ) 42 43 44 45 ABC_NAMESPACE_HEADER_END 46 47 #endif