CVC3  2.4.1
dpllt_minisat.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file dpllt_minisat.h
4  *\brief Implementation of dpllt module based on minisat
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__sat__dpllt_minisat_h_
22 #define _cvc3__sat__dpllt_minisat_h_
23 
24 #include "dpllt.h"
25 #include "proof.h"
26 #include "cnf_manager.h"
27 #include <stack>
28 
29 
30 // forward declaration of the minisat solver
31 namespace MiniSat {
32  class Solver;
33 }
34 
35 namespace SAT {
36 
37 class SatProof;
38 
39 // an implementation of the DPLLT interface using an adapted MiniSat SAT solver
40 class DPLLTMiniSat : public DPLLT {
41 public:
42 
43 protected:
44  // determines if the derivation statistic of the solver
45  // is printed after the derivation terminates.
46  // can only be set with the constructor
48 
49  // if true then minisat will create a derivation
50  // of the empty clause for an unsatisfiable problem.
51  // see getProof().
53 
54  // if d_createProof, then the proof of the last unsatisfiable search
56 
57  // the dpllt interface operates in a stack fashion via checkSat and push.
58  // each stack's data is stored in a level, which is just an instance of MiniSat.
59  // whenever a checkSat or push is done on a solver that is already in a search,
60  // a new solver is created and pushed.
61  std::stack<MiniSat::Solver*> d_solvers;
62 
63  // returnes the currently active MiniSat instance
64  //
65  // must not be called when there is no active MiniSat instance,
66  // i.e. d_solvers is empty.
68 
69  // creates a solver as an extension of the previous solver
70  // (i.e. takes clauses/assignments/lemmas)
71  // and pushes it on d_solvers
72  void pushSolver();
73 
74  // called by checkSat and continueCheck to initiate a search
75  // with a SAT solver
77 
78 
79 
80 public:
82  bool printStats = false, bool createProof = false);
83  virtual ~DPLLTMiniSat();
84 
85 
86  // Implementation of the DPLLT interface
87  virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf);
88  virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
89  virtual void push();
90  virtual void pop();
91  virtual void addAssertion(const CNF_Formula& cnf);
92  virtual std::vector<SAT::Lit> getCurAssignments() ;
93  virtual std::vector<std::vector<SAT::Lit> > getCurClauses();
94  virtual Var::Val getValue(Var v);
95 
96  // if createProof was given returns a proof of the last unsatisfiable search,
97  // otherwise (or if there was no unsatisfiable search) NULL
98  // ownership remains with DPLLTMiniSat
100  DebugAssert((d_proof != NULL), "null proof foound") ;
101  return d_proof;
102  };
103 
105 };
106 
107 }
108 
109 #endif
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
QueryResult
Definition: queryresult.h:32
CVC3::QueryResult search()
DPLLTMiniSat(TheoryAPI *theoryAPI, Decider *decider, bool printStats=false, bool createProof=false)
virtual ~DPLLTMiniSat()
#define DebugAssert(cond, str)
Definition: debug.h:408
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
SatProof * getProof()
Definition: dpllt_minisat.h:99
virtual void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
Decider * decider()
Definition: dpllt.h:118
Val
Definition: cnf.h:37
virtual std::vector< SAT::Lit > getCurAssignments()
Generic DPLL(T) module.
Manager for conversion to and traversal of CNF formulas.
virtual CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
virtual void push()
Set a checkpoint for backtracking.
virtual void pop()
Restore checkpoint.
virtual Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
TheoryAPI * theoryAPI()
Definition: dpllt.h:117
SatProof * d_proof
Definition: dpllt_minisat.h:55
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
MiniSat::Solver * getActiveSolver()
std::stack< MiniSat::Solver * > d_solvers
Definition: dpllt_minisat.h:61
Definition: cnf.h:34