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 "proof.h"
00026 #include "cnf_manager.h"
00027 #include <stack>
00028 
00029 
00030 // forward declaration of the minisat solver
00031 namespace MiniSat {
00032   class Solver;
00033 }
00034 
00035 namespace SAT {
00036 
00037 class SatProof;
00038 
00039 // an implementation of the DPLLT interface using an adapted MiniSat SAT solver
00040 class DPLLTMiniSat : public DPLLT {
00041 public:
00042 
00043 protected:
00044   // determines if the derivation statistic of the solver
00045   // is printed after the derivation terminates.
00046   // can only be set with the constructor
00047   bool d_printStats;
00048 
00049   // if true then minisat will create a derivation
00050   // of the empty clause for an unsatisfiable problem.
00051   // see getProof().
00052   bool d_createProof;
00053 
00054   // if d_createProof, then the proof of the last unsatisfiable search
00055   SatProof* d_proof;
00056 
00057   // the dpllt interface operates in a stack fashion via checkSat and push.
00058   // each stack's data is stored in a level, which is just an instance of MiniSat.
00059   // whenever a checkSat or push is done on a solver that is already in a search,
00060   // a new solver is created and pushed.
00061   std::stack<MiniSat::Solver*> d_solvers;
00062 
00063   // returnes the currently active MiniSat instance
00064   //
00065   // must not be called when there is no active MiniSat instance,
00066   // i.e. d_solvers is empty.
00067   MiniSat::Solver* getActiveSolver();
00068 
00069   // creates a solver as an extension of the previous solver
00070   // (i.e. takes clauses/assignments/lemmas)
00071   // and pushes it on d_solvers
00072   void pushSolver();
00073 
00074   // called by checkSat and continueCheck to initiate a search
00075   // with a SAT solver
00076   CVC3::QueryResult search();
00077 
00078 
00079 
00080 public:
00081   DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider,
00082          bool printStats = false, bool createProof = false);
00083   virtual ~DPLLTMiniSat();
00084 
00085 
00086   // Implementation of the DPLLT interface
00087   virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf);
00088   virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
00089   virtual void push();
00090   virtual void pop();
00091   virtual void addAssertion(const CNF_Formula& cnf);
00092   virtual std::vector<SAT::Lit> getCurAssignments() ;
00093   virtual std::vector<std::vector<SAT::Lit> > getCurClauses();
00094   virtual Var::Val getValue(Var v);
00095 
00096   // if createProof was given returns a proof of the last unsatisfiable search,
00097   // otherwise (or if there was no unsatisfiable search) NULL
00098   // ownership remains with DPLLTMiniSat
00099   SatProof* getProof() { 
00100     DebugAssert((d_proof != NULL), "null proof foound") ;
00101     return d_proof; 
00102   };
00103 
00104   CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) ;
00105 };
00106 
00107 }
00108 
00109 #endif

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2