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