CVC3  2.4.1
search_impl_base.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_impl_base.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
6  *
7  * Created: Fri Jan 17 14:19:54 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "search_impl_base.h"
23 #include "theory.h"
24 #include "eval_exception.h"
25 #include "search_rules.h"
26 #include "variable.h"
27 #include "command_line_flags.h"
28 #include "statistics.h"
29 #include "theorem_manager.h"
30 #include "expr_transform.h"
31 #include "assumptions.h"
32 
33 
34 using namespace std;
35 
36 
37 namespace CVC3 {
38 
39 
42  public:
44  virtual ~CoreSatAPI_implBase() {}
45  virtual void addLemma(const Theorem& thm, int priority, bool atBottomScope)
46  { d_se->addFact(thm); }
47  virtual Theorem addAssumption(const Expr& assump)
48  { return d_se->newIntAssumption(assump); }
49  virtual void addSplitter(const Expr& e, int priority)
50  { d_se->addSplitter(e, priority); }
51  virtual bool check(const Expr& e);
52  };
53 
54 bool CoreSatAPI_implBase::check(const Expr& e)
55 {
56  Theorem thm;
57  int scope = d_se->theoryCore()->getCM()->scopeLevel();
58  d_se->theoryCore()->getCM()->push();
59  QueryResult res = d_se->checkValid(e, thm);
60  d_se->theoryCore()->getCM()->popto(scope);
61  return res == VALID;
62 }
63 
64 
65 
66 }
67 
68 
69 using namespace CVC3;
70 
71 
72 // class SearchImplBase::Splitter methods
73 
74 // Constructor
75 SearchImplBase::Splitter::Splitter(const Literal& lit): d_lit(lit) {
76 d_lit.count()++;
77  TRACE("Splitter", "Splitter(", d_lit, ")");
78 }
79 
80 // Copy constructor
82  : d_lit(s.d_lit) {
83  d_lit.count()++;
84  TRACE("Splitter", "Splitter[copy](", d_lit, ")");
85 }
86 
87 // Assignment
90  if(this == &s) return *this; // Self-assignment
91  d_lit.count()--;
92  d_lit = s.d_lit;
93  d_lit.count()++;
94  TRACE("Splitter", "Splitter[assign](", d_lit, ")");
95  return *this;
96 }
97 
98 // Destructor
100  d_lit.count()--;
101  TRACE("Splitter", "~Splitter(", d_lit, ")");
102 }
103 
104 
105 
106 //! Constructor
108  : SearchEngine(core),
109  d_bottomScope(core->getCM()->getCurrentContext()),
110  d_dpSplitters(core->getCM()->getCurrentContext()),
111  d_lastValid(d_commonRules->trueTheorem()),
112  d_assumptions(core->getCM()->getCurrentContext()),
113  d_cnfCache(core->getCM()->getCurrentContext()),
114  d_cnfVars(core->getCM()->getCurrentContext()),
115  d_cnfOption(&(core->getFlags()["cnf"].getBool())),
116  d_ifLiftOption(&(core->getFlags()["iflift"].getBool())),
117  d_ignoreCnfVarsOption(&(core->getFlags()["ignore-cnf-vars"].getBool())),
118  d_origFormulaOption(&(core->getFlags()["orig-formula"].getBool())),
119  d_enqueueCNFCache(core->getCM()->getCurrentContext()),
120  d_applyCNFRulesCache(core->getCM()->getCurrentContext()),
121  d_replaceITECache(core->getCM()->getCurrentContext())
122 {
123  d_vm = new VariableManager(core->getCM(), d_rules,
124  core->getFlags()["mm"].getString());
125  IF_DEBUG(d_assumptions.setName("CDList[SearchImplBase::d_assumptions]");)
128 }
129 
130 
131 //! Destructor
133 {
134  delete d_coreSatAPI_implBase;
135  delete d_vm;
136 }
137 
138 
139 // Returns a new theorem if e has not already been asserted, otherwise returns
140 // a NULL theorem.
142  Theorem thm;
144  IF_DEBUG(if(debugger.trace("search verbose")) {
145  ostream& os(debugger.getOS());
146  os << "d_assumptions = [";
148  iend=d_assumptions.end(); i!=iend; ++i) {
149  debugger.getOS() << "(" << (*i).first << " => " << (*i).second << "), ";
150  }
151  os << "]" << endl;
152  })
153  if(i!=d_assumptions.end()) {
154  TRACE("search verbose", "newUserAssumption(", e,
155  "): assumption already exists");
156  } else {
157  thm = d_commonRules->assumpRule(e);
158  d_assumptions[e] = thm;
159  e.setUserAssumption();
160  TRACE("search verbose", "newUserAssumption(", thm,
161  "): created new assumption");
162  }
163  if (!thm.isNull()) d_core->addFact(d_core->getExprTrans()->preprocess(thm));
164  return thm;
165 }
166 
167 
168 // Same as newUserAssertion, except it's an error to assert something that's
169 // already been asserted.
171  Theorem thm = d_commonRules->assumpRule(e);
172  Expr atom = e.isNot() ? e[0] : e;
173  thm.setQuantLevel(theoryCore()->getQuantLevelForTerm(atom));
174  newIntAssumption(thm);
175  return thm;
176 }
177 
178 
180  DebugAssert(!d_assumptions.count(thm.getExpr()),
181  "newIntAssumption: repeated assertion: "+thm.getExpr().toString());
182  d_assumptions[thm.getExpr()] = thm;
183  thm.getExpr().setIntAssumption();
184  TRACE("search verbose", "newIntAssumption(", thm,
185  "): new assumption");
186 }
187 
188 
189 void SearchImplBase::getUserAssumptions(vector<Expr>& assumptions)
190 {
192  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
193  if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
194 }
195 
196 
197 void SearchImplBase::getInternalAssumptions(std::vector<Expr>& assumptions)
198 {
200  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
201  if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
202 }
203 
204 
205 void SearchImplBase::getAssumptions(std::vector<Expr>& assumptions)
206 {
208  iend=d_assumptions.orderedEnd(); i!=iend; ++i)
209  assumptions.push_back((*i).first);
210 }
211 
212 
214  return d_assumptions.count(e) > 0;
215 }
216 
217 
218 void SearchImplBase::addCNFFact(const Theorem& thm, bool fromCore) {
219  TRACE("addCNFFact", "addCNFFact(", thm.getExpr(), ") {");
220  if(thm.isAbsLiteral()) {
221  addLiteralFact(thm);
222  // These literals are derived, and should also be reported to the core.
223  if(!fromCore) d_core->enqueueFact(thm);
224  } else {
225  addNonLiteralFact(thm);
226  }
227  TRACE_MSG("addCNFFact", "addCNFFact => }");
228 }
229 
230 
232  TRACE("search addFact", "SearchImplBase::addFact(", thm.getExpr(), ") {");
233  if(*d_cnfOption)
234  enqueueCNF(thm);
235  else
236  addCNFFact(thm, true);
237  TRACE_MSG("search addFact", "SearchImplBase::addFact => }");
238 }
239 
240 
241 void SearchImplBase::addSplitter(const Expr& e, int priority) {
242  DebugAssert(e.isAbsLiteral(), "SearchImplBase::addSplitter("+e.toString()+")");
243  d_dpSplitters.push_back(Splitter(newLiteral(e)));
244 }
245 
246 
247 void SearchImplBase::getCounterExample(vector<Expr>& assertions, bool inOrder)
248 {
249  if(!d_core->getTM()->withAssumptions())
250  throw EvalException
251  ("Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"
252  " without assumptions activated");
253  if(!d_lastValid.isNull())
254  throw EvalException
255  ("Method getCounterExample() (or command COUNTEREXAMPLE)\n"
256  " must be called only after failed QUERY");
257  getInternalAssumptions(assertions);
258  /*
259 
260  if(!d_lastCounterExample.empty()) {
261  if (inOrder) {
262  for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
263  iend=d_assumptions.orderedEnd(); i!=iend; ++i) {
264  if (d_lastCounterExample.find((*i).first) != d_lastCounterExample.end()) {
265  assertions.push_back((*i).first);
266  }
267  }
268  DebugAssert(assertions.size()==d_lastCounterExample.size(),
269  "getCounterExample: missing assertion");
270  }
271  else {
272  ExprHashMap<bool>::iterator i=d_lastCounterExample.begin(),
273  iend = d_lastCounterExample.end();
274  for(; i!=iend; ++i) assertions.push_back((*i).first);
275  }
276  }
277  */
278 }
279 
280 
281 Proof
283 {
284  if(!d_core->getTM()->withProof())
285  throw EvalException
286  ("DUMP_PROOF cannot be used without proofs activated");
287  if(d_lastValid.isNull())
288  throw EvalException
289  ("DUMP_PROOF must be called only after successful QUERY");
290  // Double-check for optimized version
291  if(d_lastValid.isNull()) return Proof();
292  return d_lastValid.getProof();
293 }
294 
295 
296 const Assumptions&
298 {
299  if(!d_core->getTM()->withAssumptions())
300  throw EvalException
301  ("DUMP_ASSUMPTIONS cannot be used without assumptions activated");
302  if(d_lastValid.isNull())
303  throw EvalException
304  ("DUMP_ASSUMPTIONS must be called only after successful QUERY");
305  // Double-check for optimized version
308 }
309 
310 /*!
311  * Given a proof of FALSE ('res') from an assumption 'e', derive the
312  * proof of the inverse of e.
313  *
314  * \param res is a proof of FALSE
315  * \param e is the assumption used in the above proof
316  */
317 void SearchImplBase::processResult(const Theorem& res, const Expr& e)
318 {
319  // Result must be either Null (== SAT) or false (== unSAT)
320  DebugAssert(res.isNull() || res.getExpr().isFalse(),
321  "processResult: bad input"
322  + res.toString());
323  if(res.isNull()) {
324  // Didn't prove valid (if CVC-lite is complete, it means invalid).
325  // The assumptions for the counterexample must have been already
326  // set by checkSAT().
327  d_lastValid = Theorem(); // Reset last proof
328  // Remove !e, keep just the counterexample
330  if (e.isNot()) d_lastCounterExample.erase(e[0]);
331  } else {
332  // Proved valid
333  Theorem res2 =
335  if(e.isNot())
336  d_lastValid = d_rules->negIntro(e, res2);
337  else
339  d_lastCounterExample.clear(); // Reset counterexample
340  }
341 }
342 
343 
347  result = d_lastValid;
348  return qres;
349 }
350 
351 
353  QueryResult qres = restartInternal(e);
354  result = d_lastValid;
355  return qres;
356 }
357 
358 
359 void
361  TRACE("mycnf", "enqueueCNF(", beta, ") {");
363  addCNFFact(beta);
364 
365  enqueueCNFrec(beta);
366  TRACE_MSG("mycnf", "enqueueCNF => }");
367 }
368 
369 
370 void
372  Theorem theta = beta;
373 
374  TRACE("mycnf","enqueueCNFrec(", theta.getExpr(), ") { ");
375  TRACE("cnf-clauses", "enqueueCNF call", theta.getExpr(), "");
376  // The theorem scope shouldn't be higher than current
377  DebugAssert(theta.getScope() <= scopeLevel(),
378  "\n theta.getScope()="+int2string(theta.getScope())
379  +"\n scopeLevel="+int2string(scopeLevel())
380  +"\n e = "+theta.getExpr().toString());
381 
382  Expr thetaExpr = theta.getExpr();
383 
384  if(d_enqueueCNFCache.count(thetaExpr) > 0) {
385  TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
386  return;
387  }
388 
389  d_enqueueCNFCache[thetaExpr] = true;
390 
391  // // Strip double negations first
392  while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
393  theta = d_commonRules->notNotElim(theta);
394  thetaExpr = theta.getExpr();
395  // Cache all the derived theorems too
396  d_enqueueCNFCache[thetaExpr] = true;
397  }
398 
399  // Check for a propositional literal
400  if(thetaExpr.isPropLiteral()) {
401  theta = d_commonRules->iffMP(theta, replaceITE(thetaExpr));
403  "Must be a literal: theta = "
404  +theta.getExpr().toString());
405  addCNFFact(theta);
406  TRACE_MSG("mycnf", "enqueueCNFrec[literal] => }");
407  TRACE("cnf-clauses", "literal with proofs(", theta.getExpr(), ")");
408  return;
409  }
410 
411  thetaExpr = theta.getExpr();
412  // Obvious optimizations for AND and OR
413  switch(thetaExpr.getKind()) {
414  case AND:
415  // Split up the top-level conjunction and translate individually
416  for(int i=0; i<thetaExpr.arity(); i++)
417  enqueueCNFrec(d_commonRules->andElim(theta, i));
418  TRACE_MSG("mycnf", "enqueueCNFrec[AND] => }");
419  return;
420  case OR: {
421  // Check if we are already in CNF (ignoring ITEs in the terms),
422  // and if we are, translate term ITEs on the way
423  bool cnf(true);
424  TRACE("bv mycnf", "enqueueCNFrec[OR] ( ", theta.getExpr().toString(), ")");
425  for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
426  i!=iend && cnf; i++) {
427  if(!(*i).isPropLiteral())
428  cnf = false;
429  }
430  if(cnf) {
431  vector<Theorem> thms;
432  vector<unsigned int> changed;
433  unsigned int cc=0;
434  for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
435  i!=iend; i++,cc++) {
436  Theorem thm = replaceITE(*i);
437  if(thm.getLHS() != thm.getRHS()) {
438  thms.push_back(thm);
439  changed.push_back(cc);
440  }
441  }
442  if(changed.size() > 0) {
443  Theorem rewrite =
444  d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
445  theta = d_commonRules->iffMP(theta, rewrite);
446  }
447  addCNFFact(theta);
448  TRACE_MSG("mycnf", "enqueueCNFrec[cnf] => }");
449  return;
450  }
451  break;
452  }
453  case IFF: { // Check for "var <=> phi" and "phi <=> var"
454  const Expr& t0 = thetaExpr[0];
455  const Expr& t1 = thetaExpr[1];
456  if(t1.isPropLiteral()) {
457  if(!t1.isAbsLiteral())
458  theta = d_commonRules->transitivityRule(theta, replaceITE(t1));
459  applyCNFRules(theta);
460  return;
461  } else if(thetaExpr[0].isPropLiteral()) {
462  theta = d_commonRules->symmetryRule(theta);
463  if(!t0.isAbsLiteral())
464  theta = d_commonRules->transitivityRule(theta, replaceITE(t0));
465  applyCNFRules(theta);
466  return;
467  }
468  break;
469  }
470  case ITE:
471  if(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
472  && thetaExpr[2].isPropLiteral()) {
473  // Replace ITEs
474  vector<Theorem> thms;
475  vector<unsigned int> changed;
476  for(int c=0, cend=thetaExpr.arity(); c<cend; ++c) {
477  Theorem thm = replaceITE(thetaExpr[c]);
478  if(thm.getLHS() != thm.getRHS()) {
480  "thm = "+thm.getExpr().toString());
481  thms.push_back(thm);
482  changed.push_back(c);
483  }
484  }
485  if(changed.size() > 0) {
486  Theorem rewrite =
487  d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
488  theta = d_commonRules->iffMP(theta, rewrite);
489  }
490  // Convert to clauses
491  Theorem thm = d_rules->iteToClauses(theta);
492  DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
493  "enqueueCNFrec [ITE over literals]\n thm = "
494  +thm.getExpr().toString());
495  addCNFFact(d_commonRules->andElim(thm, 0));
496  addCNFFact(d_commonRules->andElim(thm, 1));
497  return;
498  }
499  break;
500  default:
501  break;
502  }
503 
504  // Now do the real work
505  Theorem res = findInCNFCache(theta.getExpr());
506  if(!res.isNull()) {
507  Theorem thm = d_commonRules->iffMP(theta, res);
508  DebugAssert(thm.isAbsLiteral(), "thm = "+thm.getExpr().toString());
509  addCNFFact(thm);
510  TRACE("cnf-clauses", "enqueueCNFrec call[cache hit]:(",
511  thm.getExpr(), ")");
512  applyCNFRules(res);
513  TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
514  return;
515  }
516 
517  // std::vector<Theorem> clauses;
518  Theorem result;
519  // (\phi <==> v)
520  result = d_commonRules->varIntroSkolem(theta.getExpr());
521 
522  TRACE("mycnf", "enqueueCNFrec: varIntroSkolem => ", result.getExpr(),
523  " @ "+int2string(result.getScope())
524  +" (current="+int2string(scopeLevel())+")");
525 
526  //result = skolemize(result, false);
527 
528  TRACE("mycnf", "enqueueCNFrec: skolemize => ", result.getExpr(),
529  " @ "+int2string(result.getScope())
530  +" (current="+int2string(scopeLevel())+")");
531  DebugAssert(result.isRewrite(),
532  "SearchImplBase::CNF(): result = "+result.toString());
533  DebugAssert(!result.getLHS().isPropLiteral() &&
534  result.getRHS().isPropLiteral(),
535  "SearchImplBase::CNF(): result = "+result.toString());
536  DebugAssert(result.getLHS() == theta.getExpr(),
537  "SearchImplBase::CNF(): result = "+result.toString()
538  +"\n theta = "+theta.toString());
539 
540  //enqueue v
541  Theorem var(d_commonRules->iffMP(theta, result));
542  // Add variable to the set of CNF vars
543  d_cnfVars[var.getExpr()] = true;
544  TRACE("mycnf", "enqueueCNFrec: theta = ", theta.getExpr(),
545  " @ "+int2string(theta.getScope())
546  +" (current="+int2string(scopeLevel())+")");
547  TRACE("mycnf", "enqueueCNFrec: var = ", var.getExpr(),
548  " @ "+int2string(var.getScope())
549  +" (current="+int2string(scopeLevel())+")");
550  DebugAssert(var.isAbsLiteral(), "var = "+var.getExpr().toString());
551  addCNFFact(var);
552  // phi <=> v
553  addToCNFCache(result);
554  applyCNFRules(result);
555  TRACE_MSG("mycnf", "enqueueCNFrec => }");
556 }
557 
558 
559 /*!
560  * \param thm is the input of the form phi <=> v
561  */
562 void
564  TRACE("mycnf", "applyCNFRules(", thm.getExpr(), ") { ");
565 
566  Theorem result = thm;
567  DebugAssert(result.isRewrite(),
568  "SearchImplBase::applyCNFRules: input must be an iff: " +
569  result.getExpr().toString());
570  Expr lhs = result.getLHS();
571  Expr rhs = result.getRHS();
573  "SearchImplBase::applyCNFRules: rhs of input must be literal: " +
574  result.getExpr().toString());
575 
576  // Eliminate negation first
577  while(result.getLHS().isNot())
578  result = d_commonRules->iffContrapositive(result);
579  lhs = result.getLHS();
580  rhs = result.getRHS();
581 
583  if(it == d_applyCNFRulesCache.end())
584  d_applyCNFRulesCache[lhs] = true;
585  else {
586  TRACE_MSG("mycnf","applyCNFRules[temp cache] => }");
587  return;
588  }
589 
590  // Catch the trivial case v1 <=> v2
591  if(lhs.isPropLiteral()) {
592  if(!lhs.isAbsLiteral()) {
593  Theorem replaced = d_commonRules->symmetryRule(replaceITE(lhs));
594  result = d_commonRules->transitivityRule(replaced, result);
595  lhs = result.getLHS();
596  DebugAssert(rhs == result.getRHS(),
597  "applyCNFRules [literal lhs]\n result = "
598  +result.getExpr().toString()
599  +"\n rhs = "+rhs.toString());
600  }
601  Theorem thm = d_rules->iffToClauses(result);
602  DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
603  "applyCNFRules [literal lhs]\n thm = "
604  +thm.getExpr().toString());
605  addCNFFact(d_commonRules->andElim(thm, 0));
606  addCNFFact(d_commonRules->andElim(thm, 1));
607  return;
608  }
609 
610  // Check the kids in e[0], replace them with cache[e[0][i]], rebuild thm
611  vector<unsigned> changed;
612  vector<Theorem> substitutions;
613  int c=0;
614  for(Expr::iterator j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
615  const Expr& phi = *j;
616  if(!phi.isPropLiteral()) {
617  Theorem phiIffVar = findInCNFCache(phi);
618  if(phiIffVar.isNull()) {
619  // Create a new variable for this child
620  phiIffVar = d_commonRules->varIntroSkolem(phi);
621  addToCNFCache(phiIffVar);
622  }
623  DebugAssert(phiIffVar.isRewrite(),
624  "SearchImplBase::applyCNFRules: result = " +
625  result.toString());
626  DebugAssert(phi == phiIffVar.getLHS(),
627  "SearchImplBase::applyCNFRules:\n phi = " +
628  phi.toString()
629  + "\n\n phiIffVar = " + phiIffVar.toString());
630  DebugAssert(phiIffVar.getRHS().isAbsLiteral(),
631  "SearchImplBase::applyCNFRules: phiIffVar = " +
632  phiIffVar.toString());
633  changed.push_back(c);
634  substitutions.push_back(phiIffVar);
635  applyCNFRules(phiIffVar);
636  }
637  }
638  if(changed.size() > 0) {
639  Theorem subst =
640  d_commonRules->substitutivityRule(lhs, changed, substitutions);
641  subst = d_commonRules->symmetryRule(subst);
642  result = d_commonRules->transitivityRule(subst, result);
643  }
644 
645  switch(result.getLHS().getKind()) {
646  case AND:
647  result = d_rules->andCNFRule(result);
648  break;
649  case OR:
650  result = d_rules->orCNFRule(result);
651  break;
652  case IFF:
653  result = d_rules->iffCNFRule(result);
654  break;
655  case IMPLIES:
656  result = d_rules->impCNFRule(result);
657  break;
658  case ITE:
659  result = d_rules->iteCNFRule(result);
660  break;
661  default:
662  DebugAssert(false,
663  "SearchImplBase::applyCNFRules: "
664  "the input operator must be and|or|iff|imp|ite\n result = " +
665  result.getLHS().toString());
666  break;
667  }
668 
669  // FIXME: eliminate this once debugged
670  Theorem clauses(result);
671 
672  // Enqueue the clauses
673  DebugAssert(!clauses.isNull(), "Oops!..");
674  DebugAssert(clauses.getExpr().isAnd(), "clauses = "
675  +clauses.getExpr().toString());
676 
677  // The clauses may containt term ITEs, and we need to translate those
678 
679  for(int i=0, iend=clauses.getExpr().arity(); i<iend; ++i) {
680  Theorem clause(d_commonRules->andElim(clauses,i));
681  addCNFFact(clause);
682  }
683  TRACE_MSG("mycnf","applyCNFRules => }");
684 }
685 
686 
688  if(e.isAbsLiteral()) return true;
689  if(!e.isOr()) return false;
690 
691  bool cnf(true);
692  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
693  cnf = (*i).isAbsLiteral();
694  return cnf;
695 }
696 
697 
698 bool
700  if(e.isPropLiteral()) return true;
701  if(!e.isOr()) return false;
702 
703  bool cnf(true);
704  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
705  cnf = (*i).isPropLiteral();
706  return cnf;
707 }
708 
709 
710 bool
712  if(!*d_ignoreCnfVarsOption) return true;
713  TRACE("isGoodSplitter", "isGoodSplitter(", e, ") {");
714  // Check for var being an auxiliary CNF variable
715  const Expr& var = e.isNot()? e[0] : e;
716  bool res(!isCNFVar(var));
717  TRACE("isGoodSplitter", "isGoodSplitter => ", res? "true" : "false", " }");
718  return res;
719 }
720 
721 
722 void
724  TRACE("mycnf", "addToCNFCache(", thm.getExpr(), ")");
725 
726  d_core->getStatistics().counter("CNF New Vars")++;
727 
728  Theorem result = thm;
729  DebugAssert(result.isRewrite(),
730  "SearchImplBase::addToCNFCache: input must be an iff: " +
731  result.getExpr().toString());
732  // Record the CNF variable
733  d_cnfVars[thm.getRHS()] = true;
734 
735  Theorem t(thm);
736  Expr phi = thm.getLHS();
737  while(phi.isNot()) {
739  phi = phi[0];
740  }
741  DebugAssert(d_cnfCache.count(phi) == 0,
742  "thm = "+thm.getExpr().toString() +
743  "\n t = "+ t.getExpr().toString());
744  //d_cnfCache.insert(phi, t);
745  d_cnfCache.insert(phi, t, d_bottomScope);
746 }
747 
748 
749 Theorem
751  TRACE("mycnf", "findInCNFCache(", e, ") { ");
752  Expr phi(e);
753 
754  int numNegs(0);
755  // Strip all the top-level negations from e
756  while(phi.isNot()) {
757  phi = phi[0]; numNegs++;
758  }
760  if(it != d_cnfCache.end()) {
761  // IF_DEBUG(debugger.counter("CNF cache hits")++;)
762  d_core->getStatistics().counter("CNF cache hits")++;
763  Theorem thm = (*it).second;
764 
765  DebugAssert(thm.isRewrite() && thm.getLHS() == phi,
766  "SearchImplBase::findInCNFCache: thm must be an iff: " +
767  thm.getExpr().toString());
768 
769  // Now put all the negations back. If the number of negations is
770  // odd, first transform phi<=>v into !phi<=>!v. Then apply
771  // !!phi<=>phi rewrite as many times as needed.
772  if(numNegs % 2 != 0) {
773  thm = d_commonRules->iffContrapositive(thm);
774  numNegs--;
775  }
776  for(; numNegs > 0; numNegs-=2) {
777  Theorem t = d_commonRules->rewriteNotNot(!!(thm.getLHS()));
778  thm = d_commonRules->transitivityRule(t,thm);
779  }
780 
781  DebugAssert(numNegs == 0, "numNegs = "+int2string(numNegs));
782  TRACE("mycnf", "findInCNFCache => ", thm.getExpr(), " }");
783  return thm;
784  }
785  TRACE_MSG("mycnf", "findInCNFCache => null }");
786  return Theorem();
787 }
788 
789 /*!
790  * Strategy:
791  *
792  * For a given atomic formula phi(ite(c, t1, t2)) which depends on a
793  * term ITE, generate an equisatisfiable formula:
794  *
795  * phi(x) & ite(c, t1=x, t2=x),
796  *
797  * where x is a new variable.
798  *
799  * The phi(x) part will be generated by the caller, and our job is to
800  * assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem
801  * phi(ite(c, t1, t2)) <=> phi(x).
802  */
803 Theorem
805  TRACE("replaceITE","replaceITE(", e, ") { ");
806  Theorem res;
807 
809  iend=d_replaceITECache.end();
810  if(i!=iend) {
811  TRACE("replaceITE", "replaceITE[cached] => ", (*i).second, " }");
812  return (*i).second;
813  }
814 
815  if(e.isAbsLiteral())
816  res = d_core->rewriteLiteral(e);
817  else
818  res = d_commonRules->reflexivityRule(e);
819 
820 
821  // If 'res' is e<=>phi, and the resulting formula phi is not a
822  // literal, introduce a new variable x, enqueue phi<=>x, and return
823  // e<=>x.
824  if(!res.getRHS().isPropLiteral()) {
825  Theorem varThm(findInCNFCache(res.getRHS()));
826  if(varThm.isNull()) {
827  varThm = d_commonRules->varIntroSkolem(res.getRHS());
828  Theorem var;
829  if(res.isRewrite())
830  var = d_commonRules->transitivityRule(res,varThm);
831  else
832  var = d_commonRules->iffMP(res,varThm);
833  //d_cnfVars[var.getExpr()] = true;
834  //addCNFFact(var);
835  addToCNFCache(varThm);
836  }
837  applyCNFRules(varThm);
838  //enqueueCNFrec(varThm);
839  res = d_commonRules->transitivityRule(res, varThm);
840  }
841 
842  d_replaceITECache[e] = res;
843 
844  TRACE("replaceITE", "replaceITE => ", res, " }");
845  return res;
846 }
int arity() const
Definition: expr.h:1201
iterator begin() const
Begin iterator.
Definition: expr.h:1211
API to to a generic proof search engine.
Definition: search.h:50
virtual Theorem andCNFRule(const Theorem &thm)=0
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem negIntro(const Expr &not_a, const Theorem &pfFalse)=0
Negation introduction: .
TheoremManager * getTM() const
Definition: theory_core.h:349
virtual Theorem impCNFRule(const Theorem &thm)=0
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Representation of a DP-suggested splitter.
unsigned & count()
Definition: variable.h:166
QueryResult
Definition: queryresult.h:32
void erase(const Expr &e)
Definition: expr_map.h:313
const CLFlags & getFlags() const
Definition: theory_core.h:350
void enqueueFact(const Theorem &e)
Enqueue a new fact.
TheoryCore::CoreSatAPI * d_coreSatAPI_implBase
virtual Theorem iteCNFRule(const Theorem &thm)=0
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
CDO< int > d_bottomScope
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid)...
CDMap< Expr, bool > d_applyCNFRulesCache
Cache for applyCNFRules()
void getUserAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
void registerCoreSatAPI(CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
Definition: theory_core.h:340
Literal newLiteral(const Expr &e)
Construct a Literal out of an Expr or return an existing one.
Theorem d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
virtual bool isAssumption(const Expr &e)
Check if the formula has been assumed.
virtual QueryResult checkValidInternal(const Expr &e)=0
Checks the validity of a formula in the current context.
bool isFalse() const
Definition: expr.h:355
virtual Theorem assumpRule(const Expr &a, int scope=-1)=0
STL namespace.
Generally Useful Expression Transformations.
virtual Proof getProof()
Returns the proof term for the last proven query.
void setUserAssumption(int scope=-1) const
Definition: expr.h:1498
virtual Theorem reflexivityRule(const Expr &a)=0
#define DebugAssert(cond, str)
Definition: debug.h:408
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
Description: Counters and flags for collecting run-time statistics.
Theorem findInCNFCache(const Expr &e)
Find a theorem phi <=> v by phi, where v is a literal.
int getScope() const
Definition: theorem.cpp:486
VariableManager * d_vm
Variable manager for classes Variable and Literal.
CommonProofRules * d_commonRules
Common proof rules.
Definition: search.h:61
bool isOr() const
Definition: expr.h:422
virtual void addLemma(const Theorem &thm, int priority, bool atBottomScope)
Add a new lemma derived by theory core.
CDMap< Expr, bool > d_enqueueCNFCache
Cache for enqueueCNF()
virtual Theorem rewriteNotNot(const Expr &e)=0
==> NOT NOT e IFF e, takes !!e
Theorem replaceITE(const Expr &e)
Replaces ITE subexpressions in e with variables.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
CDMap< Expr, Theorem > d_cnfCache
Backtracking cache for the CNF generator.
bool isPropClause(const Expr &e)
Check if e is a propositional clause.
SearchEngineRules * d_rules
Proof rules for the search engine.
Definition: search.h:64
Abstract proof rules interface to the simple search engine.
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
bool isNot() const
Definition: expr.h:420
Abstract API to the proof search engine.
virtual void addNonLiteralFact(const Theorem &thm)=0
Notify the search engine about a new non-literal fact.
void applyCNFRules(const Theorem &e)
FIXME: write a comment.
virtual Theorem addAssumption(const Expr &assump)
Add an assumption to the set of assumptions in the current context.
void getInternalAssumptions(std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual QueryResult restartInternal(const Expr &e)=0
Reruns last check with e as an additional assumption.
ExprTransform * getExprTrans() const
Definition: theory_core.h:352
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
Definition: theorem.cpp:504
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
Definition: theorem.h:404
CDMap< Expr, Theorem > d_assumptions
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
virtual Theorem iffToClauses(const Theorem &iff)=0
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
virtual Theorem orCNFRule(const Theorem &thm)=0
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual std::vector< Theorem > & getSkolemAxioms()=0
virtual void addSplitter(const Expr &e, int priority)
Suggest a splitter to the Sat engine.
virtual Theorem newIntAssumption(const Expr &e)
Add a new internal asserion.
bool isCNFVar(const Expr &e)
Check whether e is a fresh variable introduced by the CNF converter.
StatCounter counter(const std::string &name)
Definition: statistics.h:163
bool isGoodSplitter(const Expr &e)
Check if a splitter is required for completeness.
ExprHashMap< bool > d_lastCounterExample
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
virtual void addLiteralFact(const Theorem &thm)=0
Notify the search engine about a new literal fact.
Theorem newUserAssumption(const Expr &e)
Generate and add a new assertion to the set of assertions in the current context. This should only be...
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
Definition: kinds.h:68
std::string int2string(int n)
Definition: cvc_util.h:46
const bool * d_ifLiftOption
Flag: whether to convert term ITEs into CNF.
void addToCNFCache(const Theorem &thm)
Cache a theorem phi <=> v by phi, where v is a literal.
const Expr & getRHS() const
Definition: theorem.cpp:246
bool isAbsLiteral() const
Check if the theorem is a literal.
Definition: theorem.cpp:482
virtual Theorem iffCNFRule(const Theorem &thm)=0
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Interface class for callbacks to SAT from Core.
Definition: theory_core.h:219
#define IF_DEBUG(code)
Definition: debug.h:406
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
void enqueueCNFrec(const Theorem &theta)
Recursive version of enqueueCNF()
void processResult(const Theorem &res, const Expr &e)
Process result of checkValid.
Definition: kinds.h:71
Expr getExpr() const
Definition: theorem.cpp:230
int scopeLevel()
Return the current scope level (for convenience)
virtual void clearSkolemAxioms()=0
bool isNull() const
Definition: theorem.h:164
Splitter & operator=(const Splitter &s)
Assignment.
bool isPropLiteral() const
PropAtom or negation of PropAtom.
Definition: expr.h:413
virtual Theorem iteToClauses(const Theorem &ite)=0
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual QueryResult restart(const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
void addCNFFact(const Theorem &thm, bool fromCore=false)
Add a new fact to the search engine bypassing CNF converter.
ContextManager * getCM() const
Definition: theory_core.h:348
void enqueueCNF(const Theorem &theta)
Translate theta to CNF and enqueue the new clauses.
virtual ~SearchImplBase()
Destructor.
Generic API for Theories plus methods commonly used by theories.
Theorem preprocess(const Expr &e)
API to to a generic proof search engine (a.k.a. SAT solver)
TheoryCore * theoryCore()
Accessor for TheoryCore.
Definition: search.h:87
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
CoreSatAPI_implBase(SearchImplBase *se)
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)=0
Proof by contradiction: .
CDMap< Expr, bool > d_cnfVars
Backtracking set of new variables generated by CNF translator.
const Expr & getLHS() const
Definition: theorem.cpp:240
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
void addFact(const Theorem &thm)
Add a new fact to the search engine from the core.
CDList< Splitter > d_dpSplitters
Backtracking ordered set of DP-suggested splitters.
Definition: kinds.h:81
const bool * d_origFormulaOption
Flag: Preserve the original formula with +cnf (for splitter heuristics)
void setIntAssumption() const
Definition: expr.h:1508
CDMap< Expr, Theorem > d_replaceITECache
Cache for replaceITE()
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)=0
virtual Theorem notNotElim(const Theorem &not_not_e)=0
const bool * d_cnfOption
Command line flag whether to convert to CNF.
bool isClause(const Expr &e)
Check if e is a clause (a literal, or a disjunction of literals)
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
Definition: expr.cpp:35
Definition: kinds.h:99
const bool * d_ignoreCnfVarsOption
Flag: ignore auxiliary CNF variables when searching for a splitter.
bool isRewrite() const
Definition: theorem.cpp:224
virtual void addSplitter(const Expr &e, int priority)
Suggest a splitter to the SearchEngine.
virtual const Assumptions & getAssumptionsUsed()
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
SearchImplBase(TheoryCore *core)
Constructor.
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
Definition: kinds.h:67
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
Splitter(const Literal &lit)
Constructor.
virtual Theorem andElim(const Theorem &e, int i)=0
TheoryCore * d_core
Access to theory reasoning.
Definition: search.h:58
Statistics & getStatistics() const
Definition: theory_core.h:351
Definition: kinds.h:70
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Similar to checkValidInternal(), only returns Theorem(e) or Null.
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421