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