CVC3  2.4.1
minisat_solver.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_solver.h
4  *\brief Adaptation of MiniSat to DPLL(T)
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 /****************************************************************************************[Solver.h]
22 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
23 
24 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
25 associated documentation files (the "Software"), to deal in the Software without restriction,
26 including without limitation the rights to use, copy, modify, merge, publish, distribute,
27 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
28 furnished to do so, subject to the following conditions:
29 
30 The above copyright notice and this permission notice shall be included in all copies or
31 substantial portions of the Software.
32 
33 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
34 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
36 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
37 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
38 **************************************************************************************************/
39 
40 #ifndef _cvc3__minisat_h_
41 #define _cvc3__minisat_h_
42 
43 #include "minisat_types.h"
44 #include "minisat_varorder.h"
45 #include "minisat_derivation.h"
46 #include "dpllt.h"
47 #include <queue>
48 #include <stack>
49 #include <vector>
50 #include <limits>
51 #include "hash_set.h"
52 
53 
54 // changes to MiniSat for CVC integration:
55 // 1) Decision heuristics
56 // 2) Theory clauses
57 // 3) Theory conflicts
58 // 4) Theory implications
59 // 5) binary clause trick
60 //
61 // in more detail:
62 // 1) Decision heuristics
63 // if a CVC decider is given (d_decider),
64 // it is used instead of MiniSat's decision heuristics
65 // to choose the next decision literal.
66 //
67 // 2) Theory clauses
68 // any number of clauses can be added at any decision level.
69 // see explanations for d_conflict and d_pendingClauses
70 //
71 // 3) Theory conflicts
72 // theory conflicts are just treated as conflicting theory clauses
73 //
74 // 4) Theory implications
75 // can be treated just as theory clauses if their explanation is retrieved immediately.
76 // otherwise, Clause::TheoryImplication() is used as a reason
77 // and the computation level is assumed to be the decision level,
78 // until the explanation is retrieved (see d_theoryExplanations).
79 
80 
81 // other changes:
82 // - binary clause trick
83 // MiniSat sometimes (watched literal, implication reason)
84 // used a pointer to a clause to represent a unary clause.
85 // the lowest bit was used to distinguish between a pointer,
86 // and the integer representing the literal of the unit clause.
87 // this saved memory and a pointer derefence.
88 // while this is reported to increase the performance by about 10%-20%,
89 // it also complicated the code. removing it didn't show any
90 // worse performance, so this trick was dropped.
91 //
92 // - store all clauses
93 // MiniSat stored unit and binary clauses only implicitly,
94 // in the context and the watched literal data.
95 // without the binary clause trick binary clauses have to be stored explicitly in d_clauses anyway.
96 // mostly for consistency and simplicity unary clauses are stored expicitly as well.
97 // not-so-convincing reasons are that this makes it also simpler to handle conflicting
98 // theory unit clauses (see insertClause()) by giving the reason
99 // (although one could use NULL instead,
100 // but this would then complicate proof logging which is based on clause ids),
101 // and that it helps to retrieve the clause set independently of the assignment.
102 // (currently this is neither needed for DPLLT::checkSat nor DPLLT::continueCheck,
103 // the two operations in DPLLTMiniSat which use MiniSat)
104 // trying this out didn't show too much of an improvement, so it's not done.
105 
106 namespace MiniSat {
107 
108 // assume that all stl containers use the same size type
109 // and define it here once and for all
111 
112  //
113  /// conversions between MiniSat and CVC data types:
114  ///
115 
116  // both MiniSat and CVC use integers for variables and literals.
117  // CVC uses the integer's sign as the literals sign,
118  // while MiniSat doubles the id and uses only positive numbers
119  // (to be able to use them as array indizes).
120  // e.g, for the variable p with the number 2,
121  // CVC represents +p as 3 and -p as -3,
122  // while MiniSat represents +p as 5 and -p as 4.
123  //
124  // unifying this representation is probably not worth doing,
125  // as, first, conversion happens only at the interface level,
126  // and second, no memory can be saved as a literal is just an integer.
127 
128  inline Var cvcToMiniSat(const SAT::Var& var) {
129  return var.getIndex();
130  }
131 
132  inline SAT::Var miniSatToCVC(Var var) {
133  return SAT::Var(var);
134  }
135 
136 
137  inline Lit cvcToMiniSat(const SAT::Lit& literal) {
138  return MiniSat::Lit(cvcToMiniSat(literal.getVar()), literal.isPositive());
139  }
140 
141  inline SAT::Lit miniSatToCVC(Lit literal) {
142  return SAT::Lit(miniSatToCVC(literal.var()), literal.sign());
143  }
144 
145  // converts cvc clause into MiniSat literal list
146  // returns true on permanently satisfied clause, i.e. clause containing 'true'
147  bool cvcToMiniSat(const SAT::Clause& clause, std::vector<Lit>& literals);
148 
149 
150 
151 
152 
153 
154 
155 
156 
157 
158 //=================================================================================================
159 // MiniSat -- the main class:
160 
161 
162 struct SolverStats {
166  debug;
169  del_clauses(0), del_lemmas(0), db_simpl(0), lm_simpl(0), debug(0) { }
170 };
171 
172 
173 // solver state at a push, needed so that a pop can revert to that state
174 struct PushEntry {
175  // the highest id of all clauses known -
176  // clauses with higher id must have been added after the push
178  // size of d_trail
182  // conflict detected in initial propagation phase of push
183  bool d_ok;
184 
185 PushEntry(int clauseID, size_type trailSize, size_type qhead, size_type thead, bool ok) :
186  d_clauseID(clauseID),
187  d_trailSize(trailSize), d_qhead(qhead), d_thead(thead),
188  d_ok(ok)
189  {}
190 };
191 
192 
193 struct SearchParams {
194  double var_decay, clause_decay, random_var_freq; // (reasonable values are: 0.95, 0.999, 0.02)
195  SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { }
196 };
197 
198 
199 
200 class Solver {
201 
202  /// variables
203 protected:
204  // level before first decision
205  static const int d_rootLevel = 0;
206 
207  /// status
208 
209  // a search() has been started
211 
212  // if false, then the clause set is unsatisfiable.
213  bool d_ok;
214 
215  // this clause is conflicting with the current context
216  //
217  // it is not necessary to store more than one conflicting clause.
218  // if there are several conflicting clauses,
219  // they must all have been become conflicting at the same decision level,
220  // as in a conflicting state no decision is made.
221  //
222  // after backtracking on any of these conflicting clauses,
223  // the others are also not conflicting anymore,
224  // if the conflict really was due to the current decision level.
225  //
226  // this is only not the case if theory clauses are involved.
227  // i) a conflicting theory clause is added to d_pendingClauses instead of the clause set.
228  // it will be only moved to the clause set if it is not conflicting,
229  // otherwise it (or some other conflicting clause) will be used for backtracking.
230  // ii) progapations based on new theory clauses may actually be already valid
231  // in a previous level, not only in the current decision level.
232  // on backtracking this will be kept in the part of the trail which has to be propagated,
233  // and be propagated again after backtracking,
234  // thus the conflict will be computed again.
235  //
236  // this scheme also allows to stop the propagation as soon as one conflict clause is found,
237  // and backtrack only in this one, instead of searching for all conflicting clauses.
238  //
239  // the only attempt at picking a good conflict clause is to pick the shortest one.
240  // looking at the lowest backjumping level is probably(?) too expensive.
242 
243 
244  /// variable assignments, and pending propagations
245 
246  // mapping from literals to clauses in which a literal is watched,
247  // literal.index() is used as the index
248  std::vector<std::vector<Clause*> > d_watches;
249 
250  // The current assignments (lbool:s stored as char:s), indexed by var
251  std::vector<signed char> d_assigns;
252 
253  // Assignment stack; stores all assigments made in the order they were made.
254  // as theory clause and theory implications can add propagations
255  // which are valid at earlier levels this list is _not_ necessarily ordered by level.
256  std::vector<Lit> d_trail;
257 
258  // Separator indices for different decision levels in 'trail',
259  // i.e. d_trail[trail_lim[i]] is the i.th decision
260  std::vector<int> d_trail_lim;
261 
262  // 'd_trail_pos[var]' is the variable's position in 'trail[]'
263  // used for proof logging
264  std::vector<size_type> d_trail_pos;
265 
266  // head of propagation queue as index into the trail:
267  // the context is the trail up to trail[qhead - 1],
268  // the propagation queue is trail[qhead] to its end.
270 
271  // like d_qhead for theories:
272  // only the literals up to trail[thead - 1] have been asserted to the theories.
274 
275  // 'reason[var]' is the clause that implied the variables current value,
276  // or Clause::Decision() for a decision ,
277  // resp. (Clause::TheoryImplication()) for a theory implication with lazy explanation retrieval
278  std::vector<Clause*> d_reason;
279 
280  // 'level[var]' is the decision level at which assignment was made.
281  // except when the literal is a theory implication and the explanation
282  // has not been retrieved yet. Then, this is the level of the literal's
283  // assertion, and its real level will be computed during conflict analysis.
284  std::vector<int> d_level;
285 
286 
287  // Variables
288 
289  // the variables registered before the first push
290  // and at each push level (with registerVar),
291  // i.e. the variables occurring in the clauses at each push level.
292  // cumulative, i.e. the variables registered in a push level
293  // are the union of the variables registered at it and any previous level.
294  std::vector<Hash::hash_set<Var> > d_registeredVars;
295 
296 
297  /// Clauses
298 
299  // clause id counter
301 
302  // problem clauses (input clauses, theory clauses, explanations of theory implications).
303  std::vector<Clause*> d_clauses;
304 
305  // learnt clauses (conflict clauses)
306  std::vector<Clause*> d_learnts;
307 
308 
309  /// Temporary clauses
310 
311  // these are clauses which were already conflicting when added.
312  // so, first the solver has to backtrack,
313  // then they can be added in a consistent state.
314  std::queue<Clause*> d_pendingClauses;
315 
316  // these clauses are explanations for theory propagations which have been
317  // retrieved to regress a conflict. they are gathered for the regression
318  // in analyze, and then deleted on backtracking in backtrack.
319  std::stack<std::pair<int, Clause*> > d_theoryExplanations;
320 
321 
322  /// Push / Pop
323 
324  // pushes
325  std::vector<PushEntry> d_pushes;
326 
327  // lemmas kept after a pop, to add with the next push
328  std::vector<Clause*> d_popLemmas;
329 
330  // for each variable the highest pushID of the clauses used for its implication.
331  // for a decision or theory implication with unknown explanation this is max_int,
332  // for a unit clause as the reason it is the clauses pushID,
333  // for any other reason it is the max of the d_pushIDs of the literals
334  // falsifying the literals of the reason clause
335  //
336  // thus, an approximation for checking if a clause literal is permanently
337  // falsified/satisfied even after pops (as long as the clause is not popped itself),
338  // is that the implication level of the literal it the root level,
339  // and that clauses' pushID is <= the d_pushIDs value of the literal.
340  //
341  // this can be used for simplifcation of clauses, lemma minimization,
342  // and keeping propagated literals after a pop.
343  std::vector<int> d_pushIDs;
344 
345  // :TODO: unify var -> x arrays into one with a varInfo data structure:
346  // d_assigns, d_reason, d_level, d_pushIDs, d_activity
347  // probably not: d_trail_pos, d_analyze_seen
348 
349  // number of queued pop requests
350  unsigned int d_popRequests;
351 
352 
353 
354  /// heuristics
355 
356  // heuristics for keeping lemmas
357 
358  // Amount to bump next clause with.
359  double d_cla_inc;
360  // INVERSE decay factor for clause activity: stores 1/decay.
361  double d_cla_decay;
362 
363  // heuristics for variable decisions
364 
365  // A heuristic measurement of the activity of a variable.
366  std::vector<double> d_activity;
367  // Amount to bump next variable with.
368  double d_var_inc;
369  // INVERSE decay factor for variable activity: stores 1/decay.
370  // Use negative value for static variable order.
371  double d_var_decay;
372  // Keeps track of the decision variable order.
374 
375  // heuristics for clause/lemma database cleanup
376 
377  // Number of top-level assignments since last execution of 'simplifyDB()'.
379  // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
380  int64_t d_simpDB_props;
381  // Number of lemmas after last execution of 'reduceDB()'.
383 
384 
385  /// CVC interface
386 
387  // CVC theory API
389 
390  // CVC decision heuristic
392 
393 
394  /// proof logging
395 
396  // log derivation, to create a resolution proof from a closed derivation tree proof
398 
399 
400  /// Mode of operation:
401 
402  // Restart frequency etc.
404 
405  // Controls conflict clause minimization. true by default.
407 
408 
409  /// Temporaries (to reduce allocation overhead).
410  // Each variable is prefixed by the method in which is used:
411 
412  std::vector<char> d_analyze_seen;
413  std::vector<Lit> d_analyze_stack;
414  std::vector<Lit> d_analyze_redundant;
415 
416  // solver statistics
418 
419 
420 protected:
421  /// Search:
422 
423  // the current decision level
424  int decisionLevel() const { return (int)d_trail_lim.size(); }
425 
426  // decision on p
427  bool assume(Lit p);
428 
429  // queue a literal for propagation, at decisionLevel implied by reason
430  bool enqueue(Lit fact, int decisionLevel, Clause* reason);
431 
432  // propagate a literal (the head of the propagation queue)
433  void propagate();
434 
435  // perform a lookahead on the best split literals.
436  // this is done on the propositional level only, without involving theories.
437  void propLookahead(const SearchParams& params);
438 
439  /// Conflict handling
440 
441  // conflict analysis: returns conflict clause and level to backtrack to
442  // clause implies its first literal in level out_btlevel
443  Clause* analyze(int& out_btlevel);
444 
445  // conflict analysis: conflict clause minimization (helper method for 'analyze()')
446  void analyze_minimize(std::vector<Lit>& out_learnt, Inference* inference, int& pushID);
447 
448  // conflict analysis: conflict clause minimization (helper method for 'analyze()')
449  bool analyze_removable(Lit p, unsigned int min_level, int pushID);
450 
451  // backtrack to level, add conflict clause
452  void backtrack(int level, Clause* clause);
453 
454  // is the current state conflicting, i.e. is there a conflicting clause?
455  bool isConflicting() const;
456 
457  // mark this clause as conflicting
458  void updateConflict(Clause* clause);
459 
460  // returns the level in which this clause implies its first literal.
461  // precondition: all clause literals except for the first must be falsified.
462  int getImplicationLevel(const Clause& clause) const;
463 
464  // returns the level in which this clause became falsified
465  // (or at least fully assigned).
466  // precondition: no clause literal is undefined.
467  int getConflictLevel(const Clause& clause) const;
468 
469  // if this literal is a theory implied literal and its explanation has not been retrieved,
470  // then this is done now and the literal's reason is updated.
471  // precondition: literal must be a propagated literal
472  void resolveTheoryImplication(Lit literal);
473 
474 
475  /// unit propagation
476 
477  // return the watched clauses for a literal
478  std::vector<Clause*>& getWatches(Lit literal) { return d_watches[literal.index()]; };
479 
480  // return the watched clauses for a literal
481  const std::vector<Clause*>& getWatches(Lit literal) const { return d_watches[literal.index()]; };
482 
483  // adds a watch to a clause literal
484  // precondition: literal must be one of the first two literals in clause
485  void addWatch(Lit literal, Clause* clause) { getWatches(literal).push_back(clause); };
486 
487  // removes the clause from the list of watched clauses
488  void removeWatch(std::vector<Clause*>& ws, Clause* elem);
489 
490 
491  /// Operations on clauses:
492 
493  // registers a variable - any variable has to be registered before it is used in the search.
494  void registerVar(Var var);
495 
496  // checks if a variable is already registered (pop can remove a variable)
497  bool isRegistered(Var var);
498 
499  // creates/adds a clause or a lemma and returns it; registers all variables,
500  // used by all other addClause methods
501  void addClause(std::vector<Lit>& literals, CVC3::Theorem theorem, int clauseID);
502 
503  // adds a clause or a lemma to the solver, watched lists, and checks if it is unit/conflicting
504  // clause activity heuristics are updated.
505  // precondition: all variables are registered
506  // precondition: a lemma is propagating its first literal
507  void insertClause(Clause* clause);
508 
509  // add a lemma which has not been computed just now (see push(), createFrom()),
510  // so it is not necessary propagating (which is assumed by insertClause())
511  void insertLemma(const Clause* lemma, int clauseID, int pushID);
512 
513  // simplify clause based on root level assignment
514  // precondition: all variables are registered
515  bool simplifyClause(std::vector<Lit>& literals, int clausePushID) const;
516 
517  // order a clause such that it is consistent with the current assignment,
518  // i.e. the two first literals can be taken as the watched literals.
519  // precondition: all variables are registered
520  void orderClause(std::vector<Lit>& literals) const;
521 
522  // deallocate a clause, and removes it from watches if just_dealloc is false
523  void remove(Clause* c, bool just_dealloc = false);
524 
525  // assuming that the literal is implied at the root level:
526  // will the literal be assigned as long as the clause exists, even over pops?
527  bool isImpliedAt(Lit lit, int clausePushID) const;
528 
529  // is this clause permanently satisfied?
530  bool isPermSatisfied(Clause* c) const;
531 
532 
533  // Push / Pop
534 
535  // sets the d_pushIDs entry of var implied by from
536  void setPushID(Var var, Clause* from);
537 
538  // returns the d_pushIDs entry of a var
539  // makes only sense for a var with a defined value
540  int getPushID(Var var) const { return d_pushIDs[var]; }
541  int getPushID(Lit lit) const { return getPushID(lit.var()); }
542 
543  // pop the most recent push
544  void pop();
545  void popClauses(const PushEntry& pushEntry, std::vector<Clause*>& clauses);
546 
547 
548  /// Activity:
549 
551  if (d_var_decay < 0) return; // (negative decay means static variable order -- don't bump)
552  if ( (d_activity[p.var()] += d_var_inc) > 1e100 ) varRescaleActivity();
553  d_order.update(p.var()); }
555  void varRescaleActivity();
557  void claRescaleActivity() ;
559  float act = c->activity() + (float)d_cla_inc;
560  c->setActivity(act);
561  if (act > 1e20) claRescaleActivity();
562  }
563 
564 
565 
566  /// debugging
567 
568  // are all clauses (excluding lemmas) satisfied?
569  bool allClausesSatisfied();
570 
571  // checks that the first two literals of a clause are watched
572  void checkWatched(const Clause& clause) const;
573  void checkWatched() const;
574 
575  // checks that for each clause one of these holds:
576  // 1) the first two literals are undefined
577  // 2) one of the first two literals is satisfied
578  // 3) the first literal is undefined and all other literals are falsified
579  // 4) all literals are falsified
580  void checkClause(const Clause& clause) const;
581  void checkClauses() const;
582 
583  // checks that each literal in the context(trail) is either
584  // 1) a decision
585  // 2) or implied by previous context literals
586  void checkTrail() const;
587 
588  // print the current propagation step
589  void protocolPropagation() const;
590 
591 
592 public:
593  /// Initialization
594 
595  // assumes that this is the SAT solver in control of CVC theories,
596  // so it immediately pushs a new theory context.
597  //
598  // uses MiniSat's internal decision heuristics if decider is NULL
599  //
600  // if logDerivation then the derivation will be logged in getDerivation(),
601  // which provides a prove if the empty clause is derived.
602  Solver(SAT::DPLLT::TheoryAPI* theoryAPI, SAT::DPLLT::Decider* decider,
603  bool logDerivation);
604 
605  // copies clauses, assignment as unit clauses, and lemmas
606  // will be in root level
607  static Solver* createFrom(const Solver* solver);
608 
609  // releases all memory, but does not pop theories.
610  // this is according to the semantics expected by CVC:
611  // is the solver detects unsatisfiability, it pops all theory levels.
612  // otherwise the caller is responsible for resetting the theory levels.
613  ~Solver();
614 
615 
616  /// problem specification
617 
618  // converts cvc clause into MiniSat clause with the given id.
619  // returns NULL on permanently satisfied clause, i.e. clause containing 'true'
620  Clause* cvcToMiniSat(const SAT::Clause& clause, int id);
621 
622  // adds a unit clause given as a literal
623  void addClause(Lit p, CVC3::Theorem theorem);
624 
625  // adds a (copy of) clause, uses original clause id if wished
626  void addClause(const Clause& clause, bool keepClauseID);
627 
628  // adds a CVC clause
629  void addClause(const SAT::Clause& clause, bool isTheoryClause);
630 
631  // adds a CVC formula
632  void addFormula(const SAT::CNF_Formula& cnf, bool isTheoryClause);
633 
634  // returns a unique id for a new clause
635  // (addClause will then use the negation for theory clauses)
636  int nextClauseID() {
637  FatalAssert(d_clauseIDCounter >= 0, "MiniSat::Solver::nextClauseID: overflow");
638  return d_clauseIDCounter++;
639  };
640 
641  // removes permanently satisfied clauses
642  void simplifyDB();
643 
644  // removes 'bad' lemmas
645  void reduceDB();
646 
647 
648  /// search
649 
650  // (continue) search with current clause set and context
651  // until model is found (in d_trail), or unsatisfiability detected.
652  //
653  // between two calls clauses may be added,
654  // but everything else (including the theories) should remain untouched.
655  //
656  // the prover becomes essentially unusable if unsatisfiability is detected,
657  // only data may be retrieved (clauses, statistics, proof, ...)
659 
660  // returns a resolution proof for unsatisfiability if
661  // - createProof was true in the call to the constructor
662  // - the last call to search returned status UNSATISFIABLE
663  // returns NULL otherwise
664  Derivation* getProof();
665 
666  // is the solver currently in a search state?
667  // i.e. search() has been called and not been undone by a pop request.
668  bool inSearch() const { return d_inSearch && d_popRequests == 0; }
669 
670  // is the solver in a consistent state?
671  bool isConsistent() const { return !isConflicting(); }
672 
673 
674 
675  /// Push / Pop
676 
677  // push the current solver state
678  // can only be done when solver is not already in a search (inSearch()).
679  void push();
680 
681  // pop all theory levels pushed by the solver,
682  // i.e. all (current) decision levels of the solver.
683  void popTheories();
684 
685  // request to pop theories - all request are done when doPops is called
686  void requestPop();
687 
688  // perform all pop requests (calls to requestPop)
689  void doPops();
690 
691  // has there been a push which hasn't been (requested to be) undone yet?
692  bool inPush() const { return d_pushes.size() > d_popRequests; }
693 
694 
695 
696  /// clauses / assignment
697 
698  // get the current value of a variable/literal
699  lbool getValue(Var x) const { return toLbool(d_assigns[x]); }
700  lbool getValue(Lit p) const { return p.sign() ? getValue(p.var()) : ~getValue(p.var()); }
701 
702  // get the assignment level of a variable/literal (which should have a value)
703  int getLevel(Var var) const { return d_level[var]; };
704  int getLevel(Lit lit) const { return getLevel(lit.var()); };
705 
706  // set the assignment level of a variable/literal
707  void setLevel(Var var, int level) { d_level[var] = level; };
708  void setLevel(Lit lit, int level) { setLevel(lit.var(), level); };
709 
710  // this clause is the reason for a propagation and thus can't be removed
711  // precondition: the first literal of the reason clause must be the propagated literal
712  bool isReason(const Clause* c) const { return c->size() > 0 && d_reason[((*c)[0]).var()] == c; }
713 
714  // returns the implication reason of a variable (its value must be defined)
715  Clause* getReason(Var var) const { return d_reason[var]; };
716 
717  // like getReason, but if resolveTheoryImplication is true,
718  // then additionaly if literal is a theory implication resolveTheoryImplication() is called.
719  Clause* getReason(Lit literal, bool resolveTheoryImplication = true);
720 
721  // the current clause set
722  const std::vector<Clause*>& getClauses() const { return d_clauses; }
723 
724  // the current lemma set
725  const std::vector<Clause*>& getLemmas() const { return d_learnts; }
726 
727  // the current variable assignments
728  const std::vector<Lit>& getTrail() const { return d_trail; }
729 
730  // the derivation, logged if != NULL
732 
733  /// Statistics
734 
735  // derivation statistics
736  const SolverStats& getStats() const { return d_stats; }
737 
738  // number of assigned variabels (context size)
739  int nAssigns() const { return d_trail.size(); }
740 
741  // number of stored clauses (does not include clauses removed by simplifyDB)
742  int nClauses() const { return d_clauses.size(); }
743 
744  // number of stored lemmas (forgotten lemmas are not counted)
745  int nLearnts() const { return d_learnts.size(); }
746 
747  // variable with the highest id + 1
748  // not necessaribly the number of variables, if they are not enumerated without gap
749  int nVars() const { return d_assigns.size(); }
750 
751 
752  /// String representation:
753 
754  // literal id, sign, current assignment as string
755  std::string toString(Lit literal, bool showAssignment) const;
756 
757  // clause as string, showAssignment true -> show current assignment of each literal
758  std::string toString(const std::vector<Lit>& clause, bool showAssignment) const;
759 
760  // clause as string, showAssignment true -> show current assignment of each literal
761  std::string toString(const Clause& clause, bool showAssignment) const;
762 
763  // prints lemmas, clauses, assignment to cout
764  void printState() const;
765 
766  // output the clause set and context in DIMACS format
767  void printDIMACS() const;
768 
769  std::vector<SAT::Lit> curAssigns() ;
770  std::vector<std::vector<SAT::Lit> > curClauses();
771 };
772 
773 }
774 
775 
776 
777 
778 //=================================================================================================
779 #endif