CVC3  2.4.1
dpllt_basic.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file dpllt_basic.h
4  *\brief Basic implementation of dpllt module
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Mon Dec 12 19:06:58 2005
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_basic_h_
22 #define _cvc3__sat__dpllt_basic_h_
23 
24 #include "dpllt.h"
25 #include "sat_api.h"
26 #include "cdo.h"
27 #include "proof.h"
28 #include "cnf_manager.h"
29 
30 namespace SAT {
31 
32 class DPLLTBasic :public DPLLT {
33 
35 
36  bool d_ready;
40 
41  std::vector<SatSolver*> d_mngStack;
42  std::vector<CNF_Formula_Impl*> d_cnfStack;
43  std::vector<CD_CNF_Formula*> d_assertionsStack;
45 
50 
51  void createManager();
52  void generate_CDB (CNF_Formula_Impl& cnf);
53  void handle_result(SatSolver::SATStatus outcome);
54  void verify_solution();
55 
56 public:
58  bool printStats = false);
59  virtual ~DPLLTBasic();
60 
61  void addNewClause(const Clause& c);
63 
65  { return l.isNull() ? SatSolver::Lit() :
66  d_mng->MakeLit(d_mng->GetVar(l.getVar()), l.isPositive() ? 0 : 1); }
67 
69  { return l.IsNull() ? Lit() :
71  d_mng->GetPhaseFromLit(l) == 0); }
72 
73  SatSolver* satSolver() { return d_mng; }
74 
75  // Implementation of virtual DPLLT methods
76 
77  void push();
78  void pop();
79  void addAssertion(const CNF_Formula& cnf);
80  virtual std::vector<SAT::Lit> getCurAssignments() ;
81  virtual std::vector<std::vector<SAT::Lit> > getCurClauses();
82 
86 
88 
89 };
90 
91 }
92 
93 #endif
virtual int GetVarAssignment(Var var)=0
void handle_result(SatSolver::SATStatus outcome)
bool IsNull()
Definition: sat_api.h:63
virtual Lit MakeLit(Var var, int phase)=0
virtual ~DPLLTBasic()
virtual Var GetVarFromLit(Lit lit)=0
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
std::vector< CD_CNF_Formula * > d_assertionsStack
Definition: dpllt_basic.h:43
CVC3::CDO< bool > d_readyPrev
Definition: dpllt_basic.h:47
CVC3::CDO< unsigned > d_prevStackSize
Definition: dpllt_basic.h:48
CVC3::CDO< unsigned > d_pushLevel
Definition: dpllt_basic.h:46
bool isNull() const
Definition: cnf.h:63
CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
void generate_CDB(CNF_Formula_Impl &cnf)
void addNewClauses(CNF_Formula_Impl &cnf)
virtual std::vector< SAT::Lit > getCurAssignments()
CVC3::CDO< unsigned > d_prevAStackSize
Definition: dpllt_basic.h:49
SatSolver::Lit cvc2SAT(Lit l)
Definition: dpllt_basic.h:64
CVC3::ContextManager * d_cm
Definition: dpllt_basic.h:34
void addNewClause(const Clause &c)
Decider * decider()
Definition: dpllt.h:118
Val
Definition: cnf.h:37
std::vector< CNF_Formula_Impl * > d_cnfStack
Definition: dpllt_basic.h:42
Definition: cnf.h:51
virtual Var GetVar(int varIndex)=0
Generic DPLL(T) module.
Manager for conversion to and traversal of CNF formulas.
CNF_Formula_Impl * d_cnf
Definition: dpllt_basic.h:38
void pop()
Restore checkpoint.
std::vector< SatSolver * > d_mngStack
Definition: dpllt_basic.h:41
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
Lit SAT2cvc(SatSolver::Lit l)
Definition: dpllt_basic.h:68
SatSolver * satSolver()
Definition: dpllt_basic.h:73
SatSolver * d_mng
Definition: dpllt_basic.h:37
DPLLTBasic(TheoryAPI *theoryAPI, Decider *decider, CVC3::ContextManager *cm, bool printStats=false)
Var getVar() const
Definition: cnf.h:70
TheoryAPI * theoryAPI()
Definition: dpllt.h:117
Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
Definition: dpllt_basic.h:85
bool isPositive() const
Definition: cnf.h:64
CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
void verify_solution()
void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
virtual int GetPhaseFromLit(Lit lit)=0
Definition: cnf.h:34
CD_CNF_Formula * d_assertions
Definition: dpllt_basic.h:39
virtual int GetVarIndex(Var v)=0
void push()
Set a checkpoint for backtracking.