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 
34   CVC3::ContextManager* d_cm;
35 
36   bool d_ready;
37   SatSolver* d_mng;
38   CNF_Formula_Impl* d_cnf;
39   CD_CNF_Formula* d_assertions;
40 
41   std::vector<SatSolver*> d_mngStack;
42   std::vector<CNF_Formula_Impl*> d_cnfStack;
43   std::vector<CD_CNF_Formula*> d_assertionsStack;
44   bool d_printStats;
45 
46   CVC3::CDO<unsigned> d_pushLevel;
47   CVC3::CDO<bool> d_readyPrev;
48   CVC3::CDO<unsigned> d_prevStackSize;
49   CVC3::CDO<unsigned> d_prevAStackSize;
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:
57   DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, CVC3::ContextManager* cm,
58 	     bool printStats = false);
59   virtual ~DPLLTBasic();
60 
61   void addNewClause(const Clause& c);
62   void addNewClauses(CNF_Formula_Impl& cnf);
63 
cvc2SAT(Lit l)64   SatSolver::Lit cvc2SAT(Lit l)
65   { return l.isNull() ? SatSolver::Lit() :
66       d_mng->MakeLit(d_mng->GetVar(l.getVar()), l.isPositive() ? 0 : 1); }
67 
SAT2cvc(SatSolver::Lit l)68   Lit SAT2cvc(SatSolver::Lit l)
69   { return l.IsNull() ? Lit() :
70                         Lit(d_mng->GetVarIndex(d_mng->GetVarFromLit(l)),
71                             d_mng->GetPhaseFromLit(l) == 0); }
72 
satSolver()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 
83   CVC3::QueryResult checkSat(const CNF_Formula& cnf);
84   CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
getValue(Var v)85   Var::Val getValue(Var v) { return Var::Val(d_mng->GetVarAssignment(d_mng->GetVar(v))); }
86 
87   CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*);
88 
89 };
90 
91 }
92 
93 #endif
94