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