// 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