CVC3

minisat_solver.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_solver.h
00004  *\brief Adaptation of MiniSat to DPLL(T)
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 /****************************************************************************************[Solver.h]
00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
00023 
00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00025 associated documentation files (the "Software"), to deal in the Software without restriction,
00026 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00028 furnished to do so, subject to the following conditions:
00029 
00030 The above copyright notice and this permission notice shall be included in all copies or
00031 substantial portions of the Software.
00032 
00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00038 **************************************************************************************************/
00039 
00040 #ifndef _cvc3__minisat_h_
00041 #define _cvc3__minisat_h_
00042 
00043 #include "minisat_types.h"
00044 #include "minisat_varorder.h"
00045 #include "minisat_derivation.h"
00046 #include "dpllt.h"
00047 #include <queue>
00048 #include <stack>
00049 #include <vector>
00050 #include <limits>
00051 #include "hash_set.h"
00052 
00053 
00054 // changes to MiniSat for CVC integration:
00055 // 1) Decision heuristics
00056 // 2) Theory clauses
00057 // 3) Theory conflicts
00058 // 4) Theory implications
00059 // 5) binary clause trick
00060 //
00061 // in more detail:
00062 // 1) Decision heuristics
00063 // if a CVC decider is given (d_decider),
00064 // it is used instead of MiniSat's decision heuristics
00065 // to choose the next decision literal.
00066 //
00067 // 2) Theory clauses
00068 // any number of clauses can be added at any decision level.
00069 // see explanations for d_conflict and d_pendingClauses
00070 //
00071 // 3) Theory conflicts
00072 // theory conflicts are just treated as conflicting theory clauses
00073 //
00074 // 4) Theory implications
00075 // can be treated just as theory clauses if their explanation is retrieved immediately.
00076 // otherwise, Clause::TheoryImplication() is used as a reason
00077 // and the computation level is assumed to be the decision level,
00078 // until the explanation is retrieved (see d_theoryExplanations).
00079 
00080 
00081 // other changes:
00082 // - binary clause trick
00083 // MiniSat sometimes (watched literal, implication reason)
00084 // used a pointer to a clause to represent a unary clause.
00085 // the lowest bit was used to distinguish between a pointer,
00086 // and the integer representing the literal of the unit clause.
00087 // this saved memory and a pointer derefence.
00088 // while this is reported to increase the performance by about 10%-20%,
00089 // it also complicated the code. removing it didn't show any
00090 // worse performance, so this trick was dropped.
00091 //
00092 // - store all clauses
00093 // MiniSat stored unit and binary clauses only implicitly,
00094 // in the context and the watched literal data.
00095 // without the binary clause trick binary clauses have to be stored explicitly in d_clauses anyway.
00096 // mostly for consistency and simplicity unary clauses are stored expicitly as well.
00097 // not-so-convincing reasons are that this makes it also simpler to handle conflicting
00098 // theory unit clauses (see insertClause()) by giving the reason
00099 // (although one could use NULL instead,
00100 //  but this would then complicate proof logging which is based on clause ids),
00101 // and that it helps to retrieve the clause set independently of the assignment.
00102 // (currently this is neither needed for DPLLT::checkSat nor DPLLT::continueCheck,
00103 // the two operations in DPLLTMiniSat which use MiniSat)
00104 // trying this out didn't show too much of an improvement, so it's not done.
00105 
00106 namespace MiniSat {
00107 
00108 // assume that all stl containers use the same size type
00109 // and define it here once and for all
00110 typedef std::vector<int>::size_type size_type;
00111 
00112   //
00113   /// conversions between MiniSat and CVC data types:
00114   ///
00115 
00116   // both MiniSat and CVC use integers for variables and literals.
00117   // CVC uses the integer's sign as the literals sign,
00118   // while MiniSat doubles the id and uses only positive numbers
00119   // (to be able to use them as array indizes).
00120   // e.g, for the variable p with the number 2,
00121   // CVC represents +p as 3 and -p as -3,
00122   // while MiniSat represents +p as 5 and -p as 4.
00123   //
00124   // unifying this representation is probably not worth doing,
00125   // as, first, conversion happens only at the interface level,
00126   // and second, no memory can be saved as a literal is just an integer.
00127   
00128   inline Var cvcToMiniSat(const SAT::Var& var) {
00129     return var.getIndex();  
00130   }
00131 
00132   inline SAT::Var miniSatToCVC(Var var) {
00133     return SAT::Var(var);
00134   }
00135 
00136 
00137   inline Lit cvcToMiniSat(const SAT::Lit& literal) {
00138     return MiniSat::Lit(cvcToMiniSat(literal.getVar()), literal.isPositive());  
00139   }
00140 
00141   inline SAT::Lit miniSatToCVC(Lit literal) {
00142     return SAT::Lit(miniSatToCVC(literal.var()), literal.sign());
00143   }
00144   
00145   // converts cvc clause into MiniSat literal list
00146   // returns true on permanently satisfied clause, i.e. clause containing 'true'
00147   bool cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals);
00148 
00149 
00150 
00151 
00152 
00153 
00154 
00155 
00156 
00157 
00158 //=================================================================================================
00159 // MiniSat -- the main class:
00160 
00161 
00162 struct SolverStats {
00163   int64_t   starts, decisions, propagations, conflicts, theory_conflicts, max_level;
00164   int64_t   clauses_literals, learnts_literals, max_literals,
00165     del_clauses, del_lemmas, db_simpl, lm_simpl,
00166     debug;
00167   SolverStats() : starts(0), decisions(0), propagations(0), conflicts(0), theory_conflicts(0), max_level(0),
00168       clauses_literals(0), learnts_literals(0), max_literals(0),
00169       del_clauses(0), del_lemmas(0), db_simpl(0), lm_simpl(0), debug(0) { }
00170 };
00171 
00172 
00173 // solver state at a push, needed so that a pop can revert to that state
00174 struct PushEntry {
00175   // the highest id of all clauses known -
00176   // clauses with higher id must have been added after the push
00177   int d_clauseID;
00178   // size of d_trail
00179   size_type d_trailSize;
00180   size_type d_qhead;
00181   size_type d_thead;
00182   // conflict detected in initial propagation phase of push
00183   bool d_ok;
00184 
00185 PushEntry(int clauseID, size_type trailSize, size_type qhead, size_type thead, bool ok) :
00186   d_clauseID(clauseID),
00187   d_trailSize(trailSize), d_qhead(qhead), d_thead(thead),
00188   d_ok(ok)
00189   {}
00190 };
00191 
00192 
00193 struct SearchParams {
00194     double var_decay, clause_decay, random_var_freq;    // (reasonable values are: 0.95, 0.999, 0.02)    
00195     SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { }
00196 };
00197 
00198 
00199 
00200 class Solver {
00201 
00202   /// variables
00203 protected:
00204   // level before first decision
00205   static const int d_rootLevel = 0;       
00206 
00207   /// status
00208   
00209   // a search() has been started
00210   bool d_inSearch;
00211 
00212   // if false, then the clause set is unsatisfiable.
00213   bool d_ok;       
00214 
00215   // this clause is conflicting with the current context
00216   //
00217   // it is not necessary to store more than one conflicting clause.
00218   // if there are several conflicting clauses,
00219   // they must all have been become conflicting at the same decision level,
00220   // as in a conflicting state no decision is made.
00221   //
00222   // after backtracking on any of these conflicting clauses,
00223   // the others are also not conflicting anymore,
00224   // if the conflict really was due to the current decision level.
00225   //
00226   // this is only not the case if theory clauses are involved.
00227   // i) a conflicting theory clause is added to d_pendingClauses instead of the clause set.
00228   // it will be only moved to the clause set if it is not conflicting,
00229   // otherwise it (or some other conflicting clause) will be used for backtracking.
00230   // ii) progapations based on new theory clauses may actually be already valid
00231   // in a previous level, not only in the current decision level.
00232   // on backtracking this will be kept in the part of the trail which has to be propagated,
00233   // and be propagated again after backtracking,
00234   // thus the conflict will be computed again.
00235   //
00236   // this scheme also allows to stop the propagation as soon as one conflict clause is found,
00237   // and backtrack only in this one, instead of searching for all conflicting clauses.
00238   //
00239   // the only attempt at picking a good conflict clause is to pick the shortest one.
00240   // looking at the lowest backjumping level is probably(?) too expensive.
00241   Clause* d_conflict;
00242 
00243 
00244   /// variable assignments, and pending propagations
00245 
00246   // mapping from literals to clauses in which a literal is watched,
00247   // literal.index() is used as the index
00248   std::vector<std::vector<Clause*> > d_watches;
00249 
00250   // The current assignments (lbool:s stored as char:s), indexed by var
00251   std::vector<signed char> d_assigns;
00252 
00253   // Assignment stack; stores all assigments made in the order they were made.
00254   // as theory clause and theory implications can add propagations
00255   // which are valid at earlier levels this list is _not_ necessarily ordered by level.
00256   std::vector<Lit> d_trail;
00257 
00258   // Separator indices for different decision levels in 'trail',
00259   // i.e. d_trail[trail_lim[i]] is the i.th decision
00260   std::vector<int> d_trail_lim;
00261 
00262   // 'd_trail_pos[var]' is the variable's position in 'trail[]'
00263   // used for proof logging
00264   std::vector<size_type> d_trail_pos;
00265 
00266   // head of propagation queue as index into the trail:
00267   // the context is the trail up to trail[qhead - 1],
00268   // the propagation queue is trail[qhead] to its end.
00269   size_type d_qhead;
00270 
00271   // like d_qhead for theories:
00272   // only the literals up to trail[thead - 1] have been asserted to the theories.
00273   size_type d_thead;
00274 
00275   // 'reason[var]' is the clause that implied the variables current value,
00276   // or Clause::Decision() for a decision ,
00277   // resp. (Clause::TheoryImplication()) for a theory implication with lazy explanation retrieval
00278   std::vector<Clause*> d_reason;
00279 
00280   // 'level[var]' is the decision level at which assignment was made.
00281   // except when the literal is a theory implication and the explanation
00282   // has not been retrieved yet. Then, this is the level of the literal's
00283   // assertion, and its real level will be computed during conflict analysis.
00284   std::vector<int> d_level;
00285 
00286 
00287   // Variables
00288 
00289   // the variables registered before the first push
00290   // and at each push level (with registerVar),
00291   // i.e. the variables occurring in the clauses at each push level.
00292   // cumulative, i.e. the variables registered in a push level
00293   // are the union of the variables registered at it and any previous level.
00294   std::vector<Hash::hash_set<Var> > d_registeredVars;
00295 
00296 
00297   /// Clauses
00298 
00299   // clause id counter
00300   int d_clauseIDCounter;
00301 
00302   // problem clauses (input clauses, theory clauses, explanations of theory implications).
00303   std::vector<Clause*> d_clauses;
00304 
00305   // learnt clauses (conflict clauses)
00306   std::vector<Clause*> d_learnts;
00307 
00308 
00309   /// Temporary clauses
00310 
00311   // these are clauses which were already conflicting when added.
00312   // so, first the solver has to backtrack,
00313   // then they can be added in a consistent state.
00314   std::queue<Clause*> d_pendingClauses;
00315 
00316   // these clauses are explanations for theory propagations which have been
00317   // retrieved to regress a conflict. they are gathered for the regression
00318   // in analyze, and then deleted on backtracking in backtrack.
00319   std::stack<std::pair<int, Clause*> > d_theoryExplanations;
00320 
00321 
00322   /// Push / Pop
00323 
00324   // pushes
00325   std::vector<PushEntry> d_pushes;
00326 
00327   // lemmas kept after a pop, to add with the next push
00328   std::vector<Clause*> d_popLemmas;
00329 
00330   // for each variable the highest pushID of the clauses used for its implication.
00331   // for a decision or theory implication with unknown explanation this is max_int,
00332   // for a unit clause as the reason it is the clauses pushID,
00333   // for any other reason it is the max of the d_pushIDs of the literals
00334   // falsifying the literals of the reason clause
00335   //
00336   // thus, an approximation for checking if a clause literal is permanently
00337   // falsified/satisfied even after pops (as long as the clause is not popped itself),
00338   // is that the implication level of the literal it the root level,
00339   // and that clauses' pushID is <= the d_pushIDs value of the literal.
00340   //
00341   // this can be used for simplifcation of clauses, lemma minimization,
00342   // and keeping propagated literals after a pop.
00343   std::vector<int> d_pushIDs;
00344 
00345   // :TODO: unify var -> x arrays into one with a varInfo data structure:
00346   // d_assigns, d_reason, d_level, d_pushIDs, d_activity
00347   // probably not: d_trail_pos, d_analyze_seen
00348 
00349   // number of queued pop requests
00350   unsigned int d_popRequests;
00351 
00352 
00353 
00354   /// heuristics
00355 
00356   // heuristics for keeping lemmas
00357 
00358   // Amount to bump next clause with.
00359   double d_cla_inc;
00360   // INVERSE decay factor for clause activity: stores 1/decay.
00361   double d_cla_decay;
00362 
00363   // heuristics for variable decisions
00364 
00365   // A heuristic measurement of the activity of a variable.
00366   std::vector<double> d_activity;
00367   // Amount to bump next variable with.
00368   double d_var_inc;
00369   // INVERSE decay factor for variable activity: stores 1/decay.
00370   // Use negative value for static variable order.
00371   double d_var_decay;
00372   // Keeps track of the decision variable order.
00373   VarOrder d_order;
00374 
00375   // heuristics for clause/lemma database cleanup
00376 
00377   // Number of top-level assignments since last execution of 'simplifyDB()'.
00378   int d_simpDB_assigns;
00379   // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
00380   int64_t d_simpDB_props;
00381   // Number of lemmas after last execution of 'reduceDB()'.
00382   int d_simpRD_learnts;
00383 
00384 
00385   /// CVC interface
00386 
00387   // CVC theory API
00388   SAT::DPLLT::TheoryAPI* d_theoryAPI;
00389 
00390   // CVC decision heuristic
00391   SAT::DPLLT::Decider* d_decider;
00392 
00393 
00394   /// proof logging
00395 
00396   // log derivation, to create a resolution proof from a closed derivation tree proof
00397   Derivation* d_derivation;
00398   
00399 
00400   /// Mode of operation:
00401   
00402   // Restart frequency etc.
00403   SearchParams d_default_params;
00404 
00405   // Controls conflict clause minimization. true by default.
00406   bool d_expensive_ccmin;
00407 
00408 
00409   /// Temporaries (to reduce allocation overhead).
00410   // Each variable is prefixed by the method in which is used:
00411 
00412   std::vector<char> d_analyze_seen;
00413   std::vector<Lit> d_analyze_stack;
00414   std::vector<Lit> d_analyze_redundant;
00415 
00416   // solver statistics
00417   SolverStats d_stats;
00418 
00419 
00420 protected:
00421   /// Search:
00422 
00423   // the current decision level
00424   int decisionLevel() const { return (int)d_trail_lim.size(); }
00425 
00426   // decision on p
00427   bool assume(Lit p);
00428 
00429   // queue a literal for propagation, at decisionLevel implied by reason
00430   bool enqueue(Lit fact, int decisionLevel, Clause* reason);
00431 
00432   // propagate a literal (the head of the propagation queue)
00433   void propagate();
00434 
00435   // perform a lookahead on the best split literals.
00436   // this is done on the propositional level only, without involving theories.
00437   void propLookahead(const SearchParams& params);
00438 
00439   /// Conflict handling
00440 
00441   // conflict analysis: returns conflict clause and level to backtrack to
00442   // clause implies its first literal in level out_btlevel
00443   Clause* analyze(int& out_btlevel);
00444 
00445   // conflict analysis: conflict clause minimization (helper method for 'analyze()')
00446   void analyze_minimize(std::vector<Lit>& out_learnt, Inference* inference, int& pushID);
00447 
00448   // conflict analysis: conflict clause minimization (helper method for 'analyze()')
00449   bool analyze_removable(Lit p, unsigned int min_level, int pushID);
00450 
00451   // backtrack to level, add conflict clause
00452   void backtrack(int level, Clause* clause);
00453 
00454   // is the current state conflicting, i.e. is there a conflicting clause?
00455   bool isConflicting() const;
00456 
00457   // mark this clause as conflicting
00458   void updateConflict(Clause* clause);
00459 
00460   // returns the level in which this clause implies its first literal.
00461   // precondition: all clause literals except for the first must be falsified.
00462   int getImplicationLevel(const Clause& clause) const;
00463 
00464   // returns the level in which this clause became falsified
00465   // (or at least fully assigned).
00466   // precondition: no clause literal is undefined.
00467   int getConflictLevel(const Clause& clause) const;
00468 
00469   // if this literal is a theory implied literal and its explanation has not been retrieved,
00470   // then this is done now and the literal's reason is updated.
00471   // precondition: literal must be a propagated literal
00472   void resolveTheoryImplication(Lit literal);
00473 
00474 
00475   /// unit propagation
00476 
00477   // return the watched clauses for a literal
00478   std::vector<Clause*>& getWatches(Lit literal) { return d_watches[literal.index()]; };
00479 
00480   // return the watched clauses for a literal
00481   const std::vector<Clause*>& getWatches(Lit literal) const { return d_watches[literal.index()]; };
00482 
00483   // adds a watch to a clause literal
00484   // precondition: literal must be one of the first two literals in clause
00485   void addWatch(Lit literal, Clause* clause) { getWatches(literal).push_back(clause); };
00486 
00487   // removes the clause from the list of watched clauses
00488   void removeWatch(std::vector<Clause*>& ws, Clause* elem);
00489 
00490 
00491   /// Operations on clauses:
00492 
00493   // registers a variable - any variable has to be registered before it is used in the search.
00494   void registerVar(Var var);
00495 
00496   // checks if a variable is already registered (pop can remove a variable)
00497   bool isRegistered(Var var);
00498 
00499   // creates/adds a clause or a lemma and returns it; registers all variables,
00500   // used by all other addClause methods
00501   void addClause(std::vector<Lit>& literals, CVC3::Theorem theorem, int clauseID);
00502 
00503   // adds a clause or a lemma to the solver, watched lists, and checks if it is unit/conflicting
00504   // clause activity heuristics are updated.
00505   // precondition: all variables are registered
00506   // precondition: a lemma is propagating its first literal
00507   void insertClause(Clause* clause);
00508 
00509   // add a lemma which has not been computed just now (see push(), createFrom()),
00510   // so it is not necessary propagating (which is assumed by insertClause())
00511   void insertLemma(const Clause* lemma, int clauseID, int pushID);
00512 
00513   // simplify clause based on root level assignment
00514   // precondition: all variables are registered
00515   bool simplifyClause(std::vector<Lit>& literals, int clausePushID) const;
00516 
00517   // order a clause such that it is consistent with the current assignment,
00518   // i.e. the two first literals can be taken as the watched literals.
00519   // precondition: all variables are registered
00520   void orderClause(std::vector<Lit>& literals) const;
00521 
00522   // deallocate a clause, and removes it from watches if just_dealloc is false
00523   void remove(Clause* c, bool just_dealloc = false);
00524 
00525   // assuming that the literal is implied at the root level:
00526   // will the literal be assigned as long as the clause exists, even over pops?
00527   bool isImpliedAt(Lit lit, int clausePushID) const;
00528 
00529   // is this clause permanently satisfied?
00530   bool isPermSatisfied(Clause* c) const;
00531 
00532 
00533   // Push / Pop
00534 
00535   // sets the d_pushIDs entry of var implied by from
00536   void setPushID(Var var, Clause* from);
00537 
00538   // returns the d_pushIDs entry of a var
00539   // makes only sense for a var with a defined value
00540   int getPushID(Var var) const { return d_pushIDs[var]; }
00541   int getPushID(Lit lit) const { return getPushID(lit.var()); }
00542 
00543   // pop the most recent push
00544   void pop();
00545   void popClauses(const PushEntry& pushEntry, std::vector<Clause*>& clauses);
00546 
00547   
00548   /// Activity:
00549   
00550   void varBumpActivity(Lit p) {
00551     if (d_var_decay < 0) return;     // (negative decay means static variable order -- don't bump)
00552     if ( (d_activity[p.var()] += d_var_inc) > 1e100 ) varRescaleActivity();
00553     d_order.update(p.var()); }
00554   void varDecayActivity () { if (d_var_decay >= 0) d_var_inc *= d_var_decay; }
00555   void varRescaleActivity();
00556   void claDecayActivity() { d_cla_inc *= d_cla_decay; }
00557   void claRescaleActivity() ;
00558   void claBumpActivity (Clause* c) {
00559     float act = c->activity() + (float)d_cla_inc;
00560     c->setActivity(act);
00561     if (act > 1e20) claRescaleActivity();
00562   }
00563   
00564 
00565 
00566   /// debugging
00567 
00568   // are all clauses (excluding lemmas) satisfied?
00569   bool allClausesSatisfied();
00570 
00571   // checks that the first two literals of a clause are watched
00572   void checkWatched(const Clause& clause) const;
00573   void checkWatched() const;
00574 
00575   // checks that for each clause one of these holds:
00576   // 1) the first two literals are undefined
00577   // 2) one of the first two literals is satisfied
00578   // 3) the first literal is undefined and all other literals are falsified
00579   // 4) all literals are falsified
00580   void checkClause(const Clause& clause) const;
00581   void checkClauses() const;
00582 
00583   // checks that each literal in the context(trail) is either
00584   // 1) a decision
00585   // 2) or implied by previous context literals
00586   void checkTrail() const;
00587 
00588   // print the current propagation step
00589   void protocolPropagation() const;
00590 
00591 
00592 public:
00593   /// Initialization
00594 
00595   // assumes that this is the SAT solver in control of CVC theories,
00596   // so it immediately pushs a new theory context.
00597   //
00598   // uses MiniSat's internal decision heuristics if decider is NULL
00599   //
00600   // if logDerivation then the derivation will be logged in getDerivation(),
00601   // which provides a prove if the empty clause is derived.
00602   Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider,
00603    bool logDerivation);
00604 
00605   // copies clauses, assignment as unit clauses, and lemmas
00606   // will be in root level
00607   static Solver* createFrom(const Solver* solver);
00608 
00609   // releases all memory, but does not pop theories.
00610   // this is according to the semantics expected by CVC:
00611   // is the solver detects unsatisfiability, it pops all theory levels.
00612   // otherwise the caller is responsible for resetting the theory levels.
00613   ~Solver();
00614 
00615 
00616   /// problem specification
00617 
00618   // converts cvc clause into MiniSat clause with the given id.
00619   // returns NULL on permanently satisfied clause, i.e. clause containing 'true'
00620   Clause* cvcToMiniSat(const SAT::Clause& clause, int id);
00621 
00622   // adds a unit clause given as a literal
00623   void addClause(Lit p, CVC3::Theorem theorem);
00624 
00625   // adds a (copy of) clause, uses original clause id if wished
00626   void addClause(const Clause& clause, bool keepClauseID);
00627 
00628   // adds a CVC clause
00629   void addClause(const SAT::Clause& clause, bool isTheoryClause);
00630 
00631   // adds a CVC formula
00632   void addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause);
00633 
00634   // returns a unique id for a new clause
00635   // (addClause will then use the negation for theory clauses)
00636   int nextClauseID() {
00637     FatalAssert(d_clauseIDCounter >= 0, "MiniSat::Solver::nextClauseID: overflow");
00638     return d_clauseIDCounter++;
00639   };
00640 
00641   // removes permanently satisfied clauses
00642   void simplifyDB();
00643 
00644   // removes 'bad' lemmas
00645   void reduceDB();
00646 
00647 
00648   /// search
00649 
00650   // (continue) search with current clause set and context
00651   // until model is found (in d_trail), or unsatisfiability detected.
00652   // 
00653   // between two calls clauses may be added,
00654   // but everything else (including the theories) should remain untouched.
00655   //
00656   // the prover becomes essentially unusable if unsatisfiability is detected,
00657   // only data may be retrieved (clauses, statistics, proof, ...)
00658   CVC3::QueryResult search();
00659 
00660   // returns a resolution proof for unsatisfiability if
00661   // - createProof was true in the call to the constructor
00662   // - the last call to search returned status UNSATISFIABLE
00663   // returns NULL otherwise
00664   Derivation* getProof();
00665 
00666   // is the solver currently in a search state?
00667   // i.e. search() has been called and not been undone by a pop request.
00668   bool inSearch() const { return d_inSearch && d_popRequests == 0; }
00669 
00670   // is the solver in a consistent state?
00671   bool isConsistent() const { return !isConflicting(); }
00672 
00673 
00674 
00675   /// Push / Pop
00676 
00677   // push the current solver state
00678   // can only be done when solver is not already in a search (inSearch()).
00679   void push();
00680 
00681   // pop all theory levels pushed by the solver,
00682   // i.e. all (current) decision levels of the solver.
00683   void popTheories();
00684 
00685   // request to pop theories - all request are done when doPops is called
00686   void requestPop();
00687 
00688   // perform all pop requests (calls to requestPop)
00689   void doPops();
00690 
00691   // has there been a push which hasn't been (requested to be) undone yet?
00692   bool inPush() const { return d_pushes.size() > d_popRequests; }
00693 
00694 
00695 
00696   /// clauses / assignment
00697 
00698   // get the current value of a variable/literal
00699   lbool getValue(Var x) const { return toLbool(d_assigns[x]); }
00700   lbool getValue(Lit p) const { return p.sign() ? getValue(p.var()) : ~getValue(p.var()); }
00701 
00702   // get the assignment level of a variable/literal (which should have a value)
00703   int getLevel(Var var) const { return d_level[var]; };
00704   int getLevel(Lit lit) const { return getLevel(lit.var()); };
00705 
00706   // set the assignment level of a variable/literal
00707   void setLevel(Var var, int level) { d_level[var] = level; };
00708   void setLevel(Lit lit, int level) { setLevel(lit.var(), level); };
00709 
00710   // this clause is the reason for a propagation and thus can't be removed
00711   // precondition: the first literal of the reason clause must be the propagated literal
00712   bool isReason(const Clause* c) const { return c->size() > 0 && d_reason[((*c)[0]).var()] == c; }
00713 
00714   // returns the implication reason of a variable (its value must be defined)
00715   Clause* getReason(Var var) const { return d_reason[var]; };
00716 
00717   // like getReason, but if resolveTheoryImplication is true,
00718   // then additionaly if literal is a theory implication resolveTheoryImplication() is called.
00719   Clause* getReason(Lit literal, bool resolveTheoryImplication = true);
00720 
00721   // the current clause set
00722   const std::vector<Clause*>& getClauses() const { return d_clauses; }
00723 
00724   // the current lemma set
00725   const std::vector<Clause*>& getLemmas() const { return d_learnts; }
00726 
00727   // the current variable assignments
00728   const std::vector<Lit>& getTrail() const { return d_trail; }
00729 
00730   // the derivation, logged if != NULL
00731   Derivation* getDerivation() { return d_derivation; }
00732 
00733   /// Statistics
00734 
00735   // derivation statistics
00736   const SolverStats& getStats() const { return d_stats; }
00737 
00738   // number of assigned variabels (context size)
00739   int nAssigns() const { return d_trail.size(); }
00740 
00741   // number of stored clauses (does not include clauses removed by simplifyDB)
00742   int nClauses() const { return d_clauses.size(); }
00743 
00744   // number of stored lemmas (forgotten lemmas are not counted)
00745   int nLearnts() const { return d_learnts.size(); }
00746 
00747   // variable with the highest id + 1
00748   // not necessaribly the number of variables, if they are not enumerated without gap
00749   int nVars() const { return d_assigns.size(); }
00750 
00751 
00752   /// String representation:
00753 
00754   // literal id, sign, current assignment as string
00755   std::string toString(Lit literal, bool showAssignment) const;
00756 
00757   // clause as string, showAssignment true -> show current assignment of each literal
00758   std::string toString(const std::vector<Lit>& clause, bool showAssignment) const;
00759 
00760   // clause as string, showAssignment true -> show current assignment of each literal
00761   std::string toString(const Clause& clause, bool showAssignment) const;
00762 
00763   // prints lemmas, clauses, assignment to cout
00764   void printState() const;
00765 
00766   // output the clause set and context in DIMACS format
00767   void printDIMACS() const;
00768 
00769   std::vector<SAT::Lit> curAssigns() ;
00770   std::vector<std::vector<SAT::Lit> > curClauses();
00771 };
00772 
00773 }
00774 
00775 
00776 
00777 
00778 //=================================================================================================
00779 #endif