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 | |
| parent | d63a0cbbfd3979bb1423946fd1853411fbc66210 (diff) | |
| download | abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.tar.gz abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.tar.bz2 abc-13f52980dae9821b3d7bec9ff6a0fa4e544607d7.zip | |
Version abc80718
Diffstat (limited to 'src/sat/psat')
| -rw-r--r-- | src/sat/psat/m114p.h | 39 | ||||
| -rw-r--r-- | src/sat/psat/m114p_types.h | 9 | ||||
| -rw-r--r-- | src/sat/psat/module.make | 1 |
3 files changed, 49 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 diff --git a/src/sat/psat/m114p_types.h b/src/sat/psat/m114p_types.h new file mode 100644 index 00000000..54a20c5c --- /dev/null +++ b/src/sat/psat/m114p_types.h @@ -0,0 +1,9 @@ +// C-language header for MiniSat 1.14p + +#ifndef m114p_types_h +#define m114p_types_h + +typedef int M114p_Solver_t; +typedef int lit; + +#endif
\ No newline at end of file diff --git a/src/sat/psat/module.make b/src/sat/psat/module.make new file mode 100644 index 00000000..d6d908e7 --- /dev/null +++ b/src/sat/psat/module.make @@ -0,0 +1 @@ +SRC += |