summaryrefslogtreecommitdiffstats
path: root/src/sat/psat/m114p.h
blob: 5050cb4bd925b968fe0ec6d64db703dbb4950448 (plain)
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