diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-18 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-18 08:01:00 -0700 |
| commit | 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 (patch) | |
| tree | 5f5e5ce0f792bf41c6081ec77b0437a11380b696 /src/sat/psat/m114p.h | |
| parent | d63a0cbbfd3979bb1423946fd1853411fbc66210 (diff) | |
| download | abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.tar.gz abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.tar.bz2 abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.zip | |
Version abc80718
Diffstat (limited to 'src/sat/psat/m114p.h')
| -rw-r--r-- | src/sat/psat/m114p.h | 39 |
1 files changed, 39 insertions, 0 deletions
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 |