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