1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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
|
