dpllt_basic.h

Go to the documentation of this file.
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

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1