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   // converts cvc clause into MiniSat clause with the given id.
00150   // returns NULL on permanently satisfied clause, i.e. clause containing 'true'
00151   Clause* cvcToMiniSat(const SAT::Clause& clause, int id);
00152 
00153 
00154 
00155 
00156 
00157 
00158 
00159 
00160 
00161 
00162 //=================================================================================================
00163 // MiniSat -- the main class:
00164 
00165 
00166 struct SolverStats {
00167   int64_t   starts, decisions, propagations, conflicts, theory_conflicts, max_level;
00168   int64_t   clauses_literals, learnts_literals, max_literals,
00169     del_clauses, del_lemmas, db_simpl, lm_simpl,
00170     debug;
00171   SolverStats() : starts(0), decisions(0), propagations(0), conflicts(0), theory_conflicts(0), max_level(0),
00172       clauses_literals(0), learnts_literals(0), max_literals(0),
00173       del_clauses(0), del_lemmas(0), db_simpl(0), lm_simpl(0), debug(0) { }
00174 };
00175 
00176 
00177 // solver state at a push, needed so that a pop can revert to that state
00178 struct PushEntry {
00179   // the highest id of all clauses known -
00180   // clauses with higher id must have been added after the push
00181   int d_clauseID;
00182   // size of d_trail
00183   size_type d_trailSize;
00184   size_type d_qhead;
00185   size_type d_thead;
00186 
00187   PushEntry(int clauseID, size_type trailSize, size_type qhead, size_type thead) :
00188     d_clauseID(clauseID), d_trailSize(trailSize),
00189     d_qhead(qhead), d_thead(thead)
00190   {}
00191 };
00192 
00193 
00194 struct SearchParams {
00195     double var_decay, clause_decay, random_var_freq;    // (reasonable values are: 0.95, 0.999, 0.02)    
00196     SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { }
00197 };
00198 
00199 
00200 
00201 class Solver {
00202 
00203   /// variables
00204 protected:
00205   // level before first decision
00206   static const int d_rootLevel = 0;       
00207 
00208   /// status
00209   
00210   // a search() has been started
00211   bool d_inSearch;
00212 
00213   // if false, then the clause set is unsatisfiable.
00214   bool d_ok;       
00215 
00216   // this clause is conflicting with the current context
00217   //
00218   // it is not necessary to store more than one conflicting clause.
00219   // if there are several conflicting clauses,
00220   // they must all have been become conflicting at the same decision level,
00221   // as in a conflicting state no decision is made.
00222   //
00223   // after backtracking on any of these conflicting clauses,
00224   // the others are also not conflicting anymore,
00225   // if the conflict really was due to the current decision level.
00226   //
00227   // this is only not the case if theory clauses are involved.
00228   // i) a conflicting theory clause is added to d_pendingClauses instead of the clause set.
00229   // it will be only moved to the clause set if it is not conflicting,
00230   // otherwise it (or some other conflicting clause) will be used for backtracking.
00231   // ii) progapations based on new theory clauses may actually be already valid
00232   // in a previous level, not only in the current decision level.
00233   // on backtracking this will be kept in the part of the trail which has to be propagated,
00234   // and be propagated again after backtracking,
00235   // thus the conflict will be computed again.
00236   //
00237   // this scheme also allows to stop the propagation as soon as one conflict clause is found,
00238   // and backtrack only in this one, instead of searching for all conflicting clauses.
00239   //
00240   // the only attempt at picking a good conflict clause is to pick the shortest one.
00241   // looking at the lowest backjumping level is probably(?) too expensive.
00242   Clause* d_conflict;
00243 
00244 
00245   /// variable assignments, and pending propagations
00246 
00247   // mapping from literals to clauses in which a literal is watched,
00248   // literal.index() is used as the index
00249   std::vector<std::vector<Clause*> > d_watches;
00250 
00251   // The current assignments (lbool:s stored as char:s), indexed by var
00252   std::vector<char> d_assigns;
00253 
00254   // Assignment stack; stores all assigments made in the order they were made.
00255   // as theory clause and theory implications can add propagations
00256   // which are valid at earlier levels this list is _not_ necessarily ordered by level.
00257   std::vector<Lit> d_trail;
00258 
00259   // Separator indices for different decision levels in 'trail',
00260   // i.e. d_trail[trail_lim[i]] is the i.th decision
00261   std::vector<int> d_trail_lim;
00262 
00263   // 'd_trail_pos[var]' is the variable's position in 'trail[]'
00264   // used for proof logging
00265   std::vector<size_type> d_trail_pos;
00266 
00267   // head of propagation queue as index into the trail:
00268   // the context is the trail up to trail[qhead - 1],
00269   // the propagation queue is trail[qhead] to its end.
00270   size_type d_qhead;
00271 
00272   // like d_qhead for theories:
00273   // only the literals up to trail[thead - 1] have been asserted to the theories.
00274   size_type d_thead;
00275 
00276   // 'reason[var]' is the clause that implied the variables current value,
00277   // or Clause::Decision() for a decision ,
00278   // resp. (Clause::TheoryImplication()) for a theory implication with lazy explanation retrieval
00279   std::vector<Clause*> d_reason;
00280 
00281   // 'level[var]' is the decision level at which assignment was made.
00282   // except when the literal is a theory implication and the explanation
00283   // has not been retrieved yet. Then, this is the level of the literal's
00284   // assertion, and its real level will be computed during conflict analysis.
00285   std::vector<int> d_level;
00286 
00287 
00288   // Variables
00289 
00290   // the variables registered before the first push
00291   // and at each push level (with registerVar),
00292   // i.e. the variables occurring in the clauses at each push level.
00293   // cumulative, i.e. the variables registered in a push level
00294   // are the union of the variables registered at it and any previous level.
00295   std::vector<Hash::hash_set<Var> > d_registeredVars;
00296 
00297 
00298   /// Clauses
00299 
00300   // clause id counter
00301   int d_clauseIDCounter;
00302 
00303   // problem clauses (input clauses, theory clauses, explanations of theory implications).
00304   std::vector<Clause*> d_clauses;
00305 
00306   // learnt clauses (conflict clauses)
00307   std::vector<Clause*> d_learnts;
00308 
00309 
00310   /// Temporary clauses
00311 
00312   // these are clauses which were already conflicting when added.
00313   // so, first the solver has to backtrack,
00314   // then they can be added in a consistent state.
00315   std::queue<Clause*> d_pendingClauses;
00316 
00317   // these clauses are explanations for theory propagations which have been
00318   // retrieved to regress a conflict. they are gathered for the regression
00319   // in analyze, and then deleted on backtracking in backtrack.
00320   std::stack<std::pair<int, Clause*> > d_theoryExplanations;
00321 
00322 
00323   /// Push / Pop
00324 
00325   // pushes
00326   std::vector<PushEntry> d_pushes;
00327 
00328   // lemmas kept after a pop, to add with the next push
00329   std::vector<Clause*> d_popLemmas;
00330 
00331   // for each variable the highest pushID of the clauses used for its implication.
00332   // for a decision or theory implication with unknown explanation this is max_int,
00333   // for a unit clause as the reason it is the clauses pushID,
00334   // for any other reason it is the max of the d_pushIDs of the literals
00335   // falsifying the literals of the reason clause
00336   //
00337   // thus, an approximation for checking if a clause literal is permanently
00338   // falsified/satisfied even after pops (as long as the clause is not popped itself),
00339   // is that the implication level of the literal it the root level,
00340   // and that clauses' pushID is <= the d_pushIDs value of the literal.
00341   //
00342   // this can be used for simplifcation of clauses, lemma minimization,
00343   // and keeping propagated literals after a pop.
00344   std::vector<int> d_pushIDs;
00345 
00346   // :TODO: unify var -> x arrays into one with a varInfo data structure:
00347   // d_assigns, d_reason, d_level, d_pushIDs, d_activity
00348   // probably not: d_trail_pos, d_analyze_seen
00349 
00350   // number of queued pop requests
00351   uint d_popRequests;
00352 
00353 
00354 
00355   /// heuristics
00356 
00357   // heuristics for keeping lemmas
00358 
00359   // Amount to bump next clause with.
00360   double d_cla_inc;
00361   // INVERSE decay factor for clause activity: stores 1/decay.
00362   double d_cla_decay;
00363 
00364   // heuristics for variable decisions
00365 
00366   // A heuristic measurement of the activity of a variable.
00367   std::vector<double> d_activity;
00368   // Amount to bump next variable with.
00369   double d_var_inc;
00370   // INVERSE decay factor for variable activity: stores 1/decay.
00371   // Use negative value for static variable order.
00372   double d_var_decay;
00373   // Keeps track of the decision variable order.
00374   VarOrder d_order;
00375 
00376   // heuristics for clause/lemma database cleanup
00377 
00378   // Number of top-level assignments since last execution of 'simplifyDB()'.
00379   int d_simpDB_assigns;
00380   // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
00381   int64_t d_simpDB_props;
00382   // Number of lemmas after last execution of 'reduceDB()'.
00383   int d_simpRD_learnts;
00384 
00385 
00386   /// CVC interface
00387 
00388   // CVC theory API
00389   SAT::DPLLT::TheoryAPI* d_theoryAPI;
00390 
00391   // CVC decision heuristic
00392   SAT::DPLLT::Decider* d_decider;
00393 
00394 
00395   /// proof logging
00396 
00397   // log derivation, to create a resolution proof from a closed derivation tree proof
00398   Derivation* d_derivation;
00399   
00400 
00401   /// Mode of operation:
00402   
00403   // Restart frequency etc.
00404   SearchParams d_default_params;
00405 
00406   // Controls conflict clause minimization. true by default.
00407   bool d_expensive_ccmin;
00408 
00409 
00410   /// Temporaries (to reduce allocation overhead).
00411   // Each variable is prefixed by the method in which is used:
00412 
00413   std::vector<char> d_analyze_seen;
00414   std::vector<Lit> d_analyze_stack;
00415   std::vector<Lit> d_analyze_redundant;
00416 
00417   // solver statistics
00418   SolverStats d_stats;
00419 
00420 
00421 protected:
00422   /// Search:
00423 
00424   // the current decision level
00425   int decisionLevel() const { return (int)d_trail_lim.size(); }
00426 
00427   // decision on p
00428   bool assume(Lit p);
00429 
00430   // queue a literal for propagation, at decisionLevel implied by reason
00431   bool enqueue(Lit fact, int decisionLevel, Clause* reason);
00432 
00433   // propagate a literal (the head of the propagation queue)
00434   void propagate();
00435 
00436   // perform a lookahead on the best split literals.
00437   // this is done on the propositional level only, without involving theories.
00438   void propLookahead(const SearchParams& params);
00439 
00440   /// Conflict handling
00441 
00442   // conflict analysis: returns conflict clause and level to backtrack to
00443   // clause implies its first literal in level out_btlevel
00444   Clause* analyze(int& out_btlevel);
00445 
00446   // conflict analysis: conflict clause minimization (helper method for 'analyze()')
00447   void analyze_minimize(std::vector<Lit>& out_learnt, Inference* inference, int& pushID);
00448 
00449   // conflict analysis: conflict clause minimization (helper method for 'analyze()')
00450   bool analyze_removable(Lit p, uint min_level, int pushID);
00451 
00452   // backtrack to level, add conflict clause
00453   void backtrack(int level, Clause* clause);
00454 
00455   // is the current state conflicting, i.e. is there a conflicting clause?
00456   bool isConflicting() const;
00457 
00458   // mark this clause as conflicting
00459   void updateConflict(Clause* clause);
00460 
00461   // returns the level in which this clause implies its first literal.
00462   // precondition: all clause literals except for the first must be falsified.
00463   int getImplicationLevel(const Clause& clause) const;
00464 
00465   // returns the level in which this clause became falsified
00466   // (or at least fully assigned).
00467   // precondition: no clause literal is undefined.
00468   int getConflictLevel(const Clause& clause) const;
00469 
00470   // if this literal is a theory implied literal and its explanation has not been retrieved,
00471   // then this is done now and the literal's reason is updated.
00472   // precondition: literal must be a propagated literal
00473   void resolveTheoryImplication(Lit literal);
00474 
00475 
00476   /// unit propagation
00477 
00478   // return the watched clauses for a literal
00479   std::vector<Clause*>& getWatches(Lit literal) { return d_watches[literal.index()]; };
00480 
00481   // return the watched clauses for a literal
00482   const std::vector<Clause*>& getWatches(Lit literal) const { return d_watches[literal.index()]; };
00483 
00484   // adds a watch to a clause literal
00485   // precondition: literal must be one of the first two literals in clause
00486   void addWatch(Lit literal, Clause* clause) { getWatches(literal).push_back(clause); };
00487 
00488   // removes the clause from the list of watched clauses
00489   void removeWatch(std::vector<Clause*>& ws, Clause* elem);
00490 
00491 
00492   /// Operations on clauses:
00493 
00494   // registers a variable - any variable has to be registered before it is used in the search.
00495   void registerVar(Var var);
00496 
00497   // checks if a variable is already registered (pop can remove a variable)
00498   bool isRegistered(Var var);
00499 
00500   // creates/adds a clause or a lemma and returns it; registers all variables,
00501   // used by all other addClause methods
00502   void addClause(std::vector<Lit>& literals, int clauseID);
00503 
00504   // adds a clause or a lemma to the solver, watched lists, and checks if it is unit/conflicting
00505   // clause activity heuristics are updated.
00506   // precondition: all variables are registered
00507   // precondition: a lemma is propagating its first literal
00508   void insertClause(Clause* clause);
00509 
00510   // add a lemma which has not been computed just now (see push(), createFrom()),
00511   // so it is not necessary propagating (which is assumed by insertClause())
00512   void insertLemma(const Clause* lemma, int clauseID, int pushID);
00513 
00514   // simplify clause based on root level assignment
00515   // precondition: all variables are registered
00516   bool simplifyClause(std::vector<Lit>& literals, int clausePushID) const;
00517 
00518   // order a clause such that it is consistent with the current assignment,
00519   // i.e. the two first literals can be taken as the watched literals.
00520   // precondition: all variables are registered
00521   void orderClause(std::vector<Lit>& literals) const;
00522 
00523   // deallocate a clause, and removes it from watches if just_dealloc is false
00524   void remove(Clause* c, bool just_dealloc = false);
00525 
00526   // assuming that the literal is implied at the root level:
00527   // will the literal be assigned as long as the clause exists, even over pops?
00528   bool isImpliedAt(Lit lit, int clausePushID) const;
00529 
00530   // is this clause permanently satisfied?
00531   bool isPermSatisfied(Clause* c) const;
00532 
00533 
00534   // Push / Pop
00535 
00536   // sets the d_pushIDs entry of var implied by from
00537   void setPushID(Var var, Clause* from);
00538 
00539   // returns the d_pushIDs entry of a var
00540   // makes only sense for a var with a defined value
00541   int getPushID(Var var) const { return d_pushIDs[var]; }
00542   int getPushID(Lit lit) const { return getPushID(lit.var()); }
00543 
00544   // pop the most recent push
00545   void pop();
00546   void popClauses(const PushEntry& pushEntry, std::vector<Clause*>& clauses);
00547 
00548   
00549   /// Activity:
00550   
00551   void varBumpActivity(Lit p) {
00552     if (d_var_decay < 0) return;     // (negative decay means static variable order -- don't bump)
00553     if ( (d_activity[p.var()] += d_var_inc) > 1e100 ) varRescaleActivity();
00554     d_order.update(p.var()); }
00555   void varDecayActivity () { if (d_var_decay >= 0) d_var_inc *= d_var_decay; }
00556   void varRescaleActivity();
00557   void claDecayActivity() { d_cla_inc *= d_cla_decay; }
00558   void claRescaleActivity() ;
00559   void claBumpActivity (Clause* c) { if ( (c->activity() += (float)d_cla_inc) > 1e20 ) claRescaleActivity(); }
00560   
00561 
00562 
00563   /// debugging
00564 
00565   // checks that the first two literals of a clause are watched
00566   void checkWatched(const Clause& clause) const;
00567   void checkWatched() const;
00568 
00569   // checks that for each clause one of these holds:
00570   // 1) the first two literals are undefined
00571   // 2) one of the first two literals is satisfied
00572   // 3) the first literal is undefined and all other literals are falsified
00573   // 4) all literals are falsified
00574   void checkClause(const Clause& clause) const;
00575   void checkClauses() const;
00576 
00577   // checks that each literal in the context(trail) is either
00578   // 1) a decision
00579   // 2) or implied by previous context literals
00580   void checkTrail() const;
00581 
00582   // print the current propagation step
00583   void protocolPropagation() const;
00584 
00585 
00586 public:
00587   /// Initialization
00588 
00589   // assumes that this is the SAT solver in control of CVC theories,
00590   // so it immediately pushs a new theory context.
00591   // uses MiniSat's internal decision heuristics if decider is NULL
00592   Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider);
00593 
00594   // copies clauses, assignment as unit clauses, and lemmas
00595   // will be in root level
00596   static Solver* createFrom(const Solver* solver);
00597 
00598   // releases all memory, but does not pop theories.
00599   // this is according to the semantics expected by CVC:
00600   // is the solver detects unsatisfiability, it pops all theory levels.
00601   // otherwise the caller is responsible for resetting the theory levels.
00602   ~Solver();
00603 
00604 
00605   /// problem specification
00606 
00607   // adds a unit clause given as a literal
00608   void addClause(Lit p);
00609 
00610   // adds a (copy of) clause, uses original clause id if wished
00611   void addClause(const Clause& clause, bool keepClauseID);
00612 
00613   // adds a CVC clause
00614   void addClause(const SAT::Clause& clause, bool isTheoryClause);
00615 
00616   // adds a CVC formula
00617   void addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause);
00618 
00619   // returns a unique id for a new clause
00620   // (addClause will then use the negation for theory clauses)
00621   int nextClauseID() {
00622     FatalAssert(d_clauseIDCounter >= 0, "MiniSat::Solver::nextClauseID: overflow");
00623     return d_clauseIDCounter++;
00624   };
00625 
00626   // removes permanently satisfied clauses
00627   void simplifyDB();
00628 
00629   // removes 'bad' lemmas
00630   void reduceDB();
00631 
00632 
00633   /// search
00634 
00635   // (continue) search with current clause set and context
00636   // until model is found (in d_trail), or unsatisfiability detected.
00637   // 
00638   // between two calls clauses may be added,
00639   // but everything else (including the theories) should remain untouched.
00640   //
00641   // the prover becomes essentially unusable if unsatisfiability is detected,
00642   // only data may be retrieved (clauses, statistics, proof, ...)
00643   CVC3::QueryResult search();
00644 
00645   // is the solver currently in a search state?
00646   // i.e. search() has been called and not been undone by a pop request.
00647   bool inSearch() const { return d_inSearch && d_popRequests == 0; }
00648 
00649   // is the solver in a consistent state?
00650   bool isConsistent() const { return !isConflicting(); }
00651 
00652 
00653 
00654   /// Push / Pop
00655 
00656   // push the current solver state
00657   // can only be done when solver is not already in a search (inSearch()).
00658   void push();
00659 
00660   // pop all theory levels pushed by the solver,
00661   // i.e. all (current) decision levels of the solver.
00662   void popTheories();
00663 
00664   // request to pop theories - all request are done when doPops is called
00665   void requestPop();
00666 
00667   // perform all pop requests (calls to requestPop)
00668   void doPops();
00669 
00670   // has there been a push which hasn't been (requested to be) undone yet?
00671   bool inPush() const { return d_pushes.size() > d_popRequests; }
00672 
00673 
00674 
00675   /// clauses / assignment
00676 
00677   // get the current value of a variable/literal
00678   lbool getValue(Var x) const { return toLbool(d_assigns[x]); }
00679   lbool getValue(Lit p) const { return p.sign() ? getValue(p.var()) : ~getValue(p.var()); }
00680 
00681   // get the assignment level of a variable/literal (which should have a value)
00682   int getLevel(Var var) const { return d_level[var]; };
00683   int getLevel(Lit lit) const { return getLevel(lit.var()); };
00684 
00685   // set the assignment level of a variable/literal
00686   void setLevel(Var var, int level) { d_level[var] = level; };
00687   void setLevel(Lit lit, int level) { setLevel(lit.var(), level); };
00688 
00689   // this clause is the reason for a propagation and thus can't be removed
00690   // precondition: the first literal of the reason clause must be the propagated literal
00691   bool isReason(const Clause* c) const { return c->size() > 0 && d_reason[((*c)[0]).var()] == c; }
00692 
00693   // returns the implication reason of a variable (its value must be defined)
00694   Clause* getReason(Var var) const { return d_reason[var]; };
00695 
00696   // like getReason, but if resolveTheoryImplication is true,
00697   // then additionaly if literal is a theory implication resolveTheoryImplication() is called.
00698   Clause* getReason(Lit literal, bool resolveTheoryImplication = true);
00699 
00700   // the current clause set
00701   const std::vector<Clause*>& getClauses() const { return d_clauses; }
00702 
00703   // the current lemma set
00704   const std::vector<Clause*>& getLemmas() const { return d_learnts; }
00705 
00706   // the current variable assignments
00707   const std::vector<Lit>& getTrail() const { return d_trail; }
00708 
00709   // the derivation, logged if != NULL
00710   Derivation* getDerivation() { return d_derivation; }
00711 
00712 
00713   /// Statistics
00714 
00715   // derivation statistics
00716   const SolverStats& getStats() const { return d_stats; }
00717 
00718   // number of assigned variabels (context size)
00719   int nAssigns() const { return d_trail.size(); }
00720 
00721   // number of stored clauses (does not include clauses removed by simplifyDB)
00722   int nClauses() const { return d_clauses.size(); }
00723 
00724   // number of stored lemmas (forgotten lemmas are not counted)
00725   int nLearnts() const { return d_learnts.size(); }
00726 
00727   // variable with the highest id + 1
00728   // not necessaribly the number of variables, if they are not enumerated without gap
00729   int nVars() const { return d_assigns.size(); }
00730 
00731 
00732   /// String representation:
00733 
00734   // literal id, sign, current assignment as string
00735   std::string toString(Lit literal, bool showAssignment) const;
00736 
00737   // clause as string, showAssignment true -> show current assignment of each literal
00738   std::string toString(const std::vector<Lit>& clause, bool showAssignment) const;
00739 
00740   // clause as string, showAssignment true -> show current assignment of each literal
00741   std::string toString(const Clause& clause, bool showAssignment) const;
00742 
00743   // prints lemmas, clauses, assignment to cout
00744   void printState() const;
00745 
00746   // output the clause set and context in DIMACS format
00747   void printDIMACS() const;
00748 };
00749 
00750 }
00751 
00752 
00753 
00754 
00755 //=================================================================================================
00756 #endif

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