dpllt_minisat.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file dpllt_minisat.h
00004  *\brief Implementation of dpllt module based on minisat
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
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_minisat_h_
00022 #define _cvc3__sat__dpllt_minisat_h_
00023 
00024 #include "dpllt.h"
00025 #include <stack>
00026 
00027 
00028 // forward declaration of the minisat solver
00029 namespace MiniSat {
00030   class Solver;
00031 }
00032 
00033 namespace SAT {
00034 
00035 // an implementation of the DPLLT interface using an adapted MiniSat SAT solver
00036 class DPLLTMiniSat : public DPLLT {
00037 public:
00038 
00039 protected:
00040   // determines if the derivation statistic of the solver
00041   // is printed after the derivation terminates.
00042   // can only be set with the constructor
00043   bool d_printStats;
00044 
00045   // the dpllt interface operates in a stack fashion via checkSat and push.
00046   // each stack's data is stored in a level, which is just an instance of MiniSat.
00047   // whenever a checkSat or push is done on a solver that is already in a search,
00048   // a new solver is created and pushed.
00049   std::stack<MiniSat::Solver*> d_solvers;
00050 
00051   // returnes the currently active MiniSat instance
00052   //
00053   // must not be called when there is no active MiniSat instance,
00054   // i.e. d_solvers is empty.
00055   MiniSat::Solver* getActiveSolver();
00056 
00057   // creates a solver as an extension of the previous solver
00058   // (i.e. takes clauses/assignments/lemmas)
00059   // and pushes it on d_solvers
00060   void pushSolver();
00061 
00062   // called by checkSat and continueCheck to initiate a search
00063   // with a SAT solver
00064   CVC3::QueryResult search();
00065 
00066 
00067 
00068 public:
00069   DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider, bool printStats = false);
00070   virtual ~DPLLTMiniSat();
00071 
00072 
00073   // Implementation of the DPLLT interface
00074   virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf);
00075   virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
00076   virtual void push();
00077   virtual void pop();
00078   virtual void addAssertion(const CNF_Formula& cnf);
00079   virtual Var::Val getValue(Var v);
00080 };
00081 
00082 }
00083 
00084 #endif

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