CVC3
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