00001 /*****************************************************************************/ 00002 /*! 00003 *\file dpllt_basic.h 00004 *\brief Basic implementation of dpllt module based on xchaff 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Mon Dec 12 19:06:58 2005 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 */ 00019 /*****************************************************************************/ 00020 00021 #ifndef _cvc3__sat__dpllt_basic_h_ 00022 #define _cvc3__sat__dpllt_basic_h_ 00023 00024 #include "dpllt.h" 00025 #include "sat_api.h" 00026 #include "cdo.h" 00027 00028 namespace SAT { 00029 00030 class DPLLTBasic :public DPLLT { 00031 00032 CVC3::ContextManager* d_cm; 00033 00034 bool d_ready; 00035 SatSolver* d_mng; 00036 CNF_Formula_Impl* d_cnf; 00037 CD_CNF_Formula* d_assertions; 00038 00039 std::vector<SatSolver*> d_mngStack; 00040 std::vector<CNF_Formula_Impl*> d_cnfStack; 00041 std::vector<CD_CNF_Formula*> d_assertionsStack; 00042 bool d_printStats; 00043 00044 CVC3::CDO<unsigned> d_pushLevel; 00045 CVC3::CDO<bool> d_readyPrev; 00046 CVC3::CDO<unsigned> d_prevStackSize; 00047 CVC3::CDO<unsigned> d_prevAStackSize; 00048 00049 void createManager(); 00050 void generate_CDB (CNF_Formula_Impl& cnf); 00051 void handle_result(SatSolver::SATStatus outcome); 00052 void verify_solution(); 00053 00054 public: 00055 DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, CVC3::ContextManager* cm, 00056 bool printStats = false); 00057 virtual ~DPLLTBasic(); 00058 00059 void addNewClause(const Clause& c); 00060 void addNewClauses(CNF_Formula_Impl& cnf); 00061 00062 SatSolver::Lit cvc2SAT(Lit l) 00063 { return l.isNull() ? SatSolver::Lit() : 00064 d_mng->MakeLit(d_mng->GetVar(l.getVar()), l.isPositive() ? 0 : 1); } 00065 00066 Lit SAT2cvc(SatSolver::Lit l) 00067 { return l.IsNull() ? Lit() : 00068 Lit(d_mng->GetVarIndex(d_mng->GetVarFromLit(l)), 00069 d_mng->GetPhaseFromLit(l) == 0); } 00070 00071 SatSolver* satSolver() { return d_mng; } 00072 00073 // Implementation of virtual DPLLT methods 00074 00075 void push(); 00076 void pop(); 00077 void addAssertion(const CNF_Formula& cnf); 00078 CVC3::QueryResult checkSat(const CNF_Formula& cnf); 00079 CVC3::QueryResult continueCheck(const CNF_Formula& cnf); 00080 Var::Val getValue(Var v) { return Var::Val(d_mng->GetVarAssignment(d_mng->GetVar(v))); } 00081 00082 }; 00083 00084 } 00085 00086 #endif