From 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 18 Jul 2008 08:01:00 -0700 Subject: Version abc80718 --- src/sat/psat/m114p.h | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/sat/psat/m114p.h (limited to 'src/sat/psat/m114p.h') diff --git a/src/sat/psat/m114p.h b/src/sat/psat/m114p.h new file mode 100644 index 00000000..5050cb4b --- /dev/null +++ b/src/sat/psat/m114p.h @@ -0,0 +1,39 @@ +// C-language header for MiniSat 1.14p + +#ifndef m114p_h +#define m114p_h + +#include "m114p_types.h" + +// SAT solver APIs +extern M114p_Solver_t M114p_SolverNew( int fRecordProof ); +extern void M114p_SolverDelete( M114p_Solver_t s ); +extern void M114p_SolverPrintStats( M114p_Solver_t s, double Time ); +extern void M114p_SolverSetVarNum( M114p_Solver_t s, int nVars ); +extern int M114p_SolverAddClause( M114p_Solver_t s, lit* begin, lit* end ); +extern int M114p_SolverSimplify( M114p_Solver_t s ); +extern int M114p_SolverSolve( M114p_Solver_t s, lit* begin, lit* end, int nConfLimit ); +extern int M114p_SolverGetConflictNum( M114p_Solver_t s ); + +// proof status APIs +extern int M114p_SolverProofIsReady( M114p_Solver_t s ); +extern void M114p_SolverProofSave( M114p_Solver_t s, char * pFileName ); +extern int M114p_SolverProofClauseNum( M114p_Solver_t s ); + +// proof traversal APIs +extern int M114p_SolverGetFirstRoot( M114p_Solver_t s, int ** ppLits ); +extern int M114p_SolverGetNextRoot( M114p_Solver_t s, int ** ppLits ); +extern int M114p_SolverGetFirstChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); +extern int M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars ); + +// iterator over the root clauses (should be called first) +#define M114p_SolverForEachRoot( s, ppLits, nLits, i ) \ + for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits; \ + i++, nLits = M114p_SolverGetNextRoot(s, ppLits) ) + +// iterator over the learned clauses (should be called after iterating over roots) +#define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i ) \ + for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \ + i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) ) + +#endif \ No newline at end of file -- cgit v1.2.3