CVC3  2.4.1
theory_core.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_core.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh (CNF converter)
6  *
7  * Created: Thu Jan 30 16:57:52 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 #include <locale>
22 #include <cctype>
23 #include <ctime>
24 #include "command_line_flags.h"
25 #include "expr.h"
26 #include "notifylist.h"
27 #include "pretty_printer.h"
28 #include "common_proof_rules.h"
29 #include "parser_exception.h"
30 #include "typecheck_exception.h"
31 #include "smtlib_exception.h"
32 #include "eval_exception.h"
33 #include "theory_core.h"
34 #include "expr_transform.h"
35 #include "core_proof_rules.h"
36 #include "theorem_manager.h"
37 #include "translator.h"
38 #include "theory_arith.h" // for isReal() tester
39 
40 using namespace std;
41 
42 
43 namespace CVC3 {
44 
45 
46  //! Implementation of PrettyPrinter class
47  /*! \ingroup PrettyPrinting */
49  private:
51  //! Disable the default constructor
53  public:
54  //! Constructor
55  PrettyPrinterCore(TheoryCore* core): d_core(core) { }
56  ExprStream& print(ExprStream& os, const Expr& e)
57  {
58  if(e.isString())
59  return e.print(os);
60  else if (e.isApply())
61  return d_core->theoryOf(e)->print(os, e);
62  else if(d_core->hasTheory(e.getKind()))
63  return d_core->theoryOf(e.getKind())->print(os, e);
64  else
65  return e.print(os);
66  }
67  };
68 
69 
72  public:
73  TypeComputerCore(TheoryCore* core): d_core(core) { }
74  void computeType(const Expr& e)
75  {
76  DebugAssert(!e.isVar(), "Variables should have a type: "+e.toString());
77  Theory* i = d_core->theoryOf(e.getKind());
78  if (e.isApply()) i = d_core->theoryOf(e);
79  i->computeType(e);
80  DebugAssert(!e.lookupType().getExpr().isNull(), "Type not set by computeType");
81  }
82  void checkType(const Expr& e)
83  {
84  if (!e.isType()) throw Exception
85  ("Tried to use non-type as a type: "+e.toString());
86  d_core->theoryOf(e)->checkType(e);
87  e.setValidType();
88  }
90  bool enumerate, bool computeSize)
91  {
92  DebugAssert(e.isType(), "finiteTypeInfo called on non-type");
93  return d_core->theoryOf(e)->finiteTypeInfo(e, n, enumerate, computeSize);
94  }
95  };
96 
97 
98  ostream& operator<<(ostream& os, const NotifyList& l)
99  {
100  os << "NotifyList(\n";
101  for(size_t i=0,iend=l.size(); i<iend; ++i) {
102  os << "[" << l.getTheory(i)->getName() << ", " << l.getExpr(i) << "]\n";
103  }
104  return os << ")";
105  }
106 
107 
108 }
109 
110 
111 using namespace CVC3;
112 
113 
114 /*****************************************************************************/
115 /*
116  * Private helper functions
117  */
118 /*****************************************************************************/
119 
120 
121 bool TheoryCore::processFactQueue(EffortLevel effort)
122 {
123  Theorem thm;
124  vector<Theory*>::iterator i, iend = d_theories.end();
125  bool lemmasAdded = false;
126  do {
127  processUpdates();
128  while (!d_queue.empty() && !d_inconsistent && !timeLimitReached()) {
129  thm = d_queue.front();
130  d_queue.pop();
131  assertFactCore(thm);
132  processUpdates();
133  };
134 
135  if (d_inconsistent) break;
136 
137  while (!d_queueSE.empty() && !timeLimitReached()) {
138  // Copy a Theorem by value, to guarantee valid reference down
139  // the call chain
140  lemmasAdded = true;
141  Theorem thm(d_queueSE.back());
142  d_queueSE.pop_back();
143  d_coreSatAPI->addLemma(thm);
144  }
145 
146  if (effort > LOW) {
147  for(i = d_theories.begin(); d_update_thms.empty() && d_queue.empty() && i != iend && !d_inconsistent && !timeLimitReached(); ++i) {
148  (*i)->checkSat(effort == FULL && !lemmasAdded);
149  }
150  }
151  } while ((!d_queue.empty() || !d_update_thms.empty()) && !d_inconsistent && !timeLimitReached());
152 
153  if (d_inconsistent) {
154  d_update_thms.clear();
155  d_update_data.clear();
156  while(d_queue.size()) d_queue.pop();
157  d_queueSE.clear();
158  return false;
159  }
160 
161  if (timeLimitReached()) {
162  // clear all work queues to satisfy invariants
163  d_update_thms.clear();
164  d_update_data.clear();
165  while (!d_queue.empty()) d_queue.pop();
166  d_queueSE.clear();
167  }
168 
169  return lemmasAdded;
170 }
171 
172 
173 void TheoryCore::processNotify(const Theorem& e, NotifyList *L)
174 {
175  ++d_inUpdate;
176  DebugAssert(L, "Expected non-NULL notify list");
177  for(unsigned k = 0; k < L->size() && !d_inconsistent; ++k) {
178  L->getTheory(k)->update(e, L->getExpr(k));
179  }
180  --d_inUpdate;
181 }
182 
183 
184 Theorem TheoryCore::simplify(const Expr& e)
185 {
186  DebugAssert(d_simpStack.count(e) == 0, "TheoryCore::simplify: loop detected over e =\n"
187  +e.toString());
188  DebugAssert(d_simpStack.size() < 10000,
189  "TheoryCore::simplify: too deep recursion depth");
190  IF_DEBUG(d_simpStack[e] = true;)
191 
192  // Normally, if an expr has a find, we don't need to simplify, just return the find.
193  // However, if we are in the middle of an update, the find may not yet be updated, so
194  // we should do a full simplify. The exception is expressions like
195  // uninterp. functions or reads that use a congruence closure algorithm that
196  // relies on not simplifying inside of expressions that have finds.
197  if (e.hasFind()) {
198  DebugAssert((find(e).getRHS().hasFind() && find(e).getRHS().isTerm())
199  || find(e).getRHS().isTrue()
200  || find(e).getRHS().isFalse(), "Unexpected find pointer");
201  if (d_inUpdate) {
202  if (e.usesCC()) {
203  Theorem thm = find(e);
204  if (!thm.isRefl()) {
205  thm = transitivityRule(thm, simplify(thm.getRHS()));
206  }
207  IF_DEBUG(d_simpStack.erase(e);)
208  return thm;
209  }
210  }
211  else {
212  IF_DEBUG(d_simpStack.erase(e);)
213  return find(e);
214  }
215  }
216 
217  if(e.validSimpCache()) {
218  IF_DEBUG(d_simpStack.erase(e);)
219  return e.getSimpCache();
220  }
221 
222  Theorem thm;
223  if (e.isVar()) {
224  thm = rewriteCore(e);
225  }
226  else {
227  thm = rewriteCore(theoryOf(e.getOpKind())->simplifyOp(e));
228  }
229 
230  const Expr& e2 = thm.getRHS();
231 #ifdef _CVC3_DEBUG_MODE
232  if (!e2.usesCC()) { //2.isTerm() || !e2.hasFind()) {
233  // The rewriter should guarantee that all of its children are simplified.
234  for (int k=0; k<e2.arity(); ++k) {
235  Expr simplified(simplify(e2[k]).getRHS());
236  DebugAssert(e2[k]==simplified,"Simplify Error 1:\n e2[k="+int2string(k)
237  +"] = "
238  +e2[k].toString() + "\nSimplified = "
239  +simplified.toString()
240  +"\ne2 = "+e2.toString());
241  }
242  }
243  Expr rewritten(rewriteCore(e2).getRHS());
244  DebugAssert(e2==rewritten,"Simplify Error 2: e2 = \n"
245  +e2.toString() + "\nSimplified rewritten = \n"
246  +rewritten.toString());
247 #endif
248  e.setSimpCache(thm);
249  if (e != e2 && !e2.hasFind()) {
250  e2.setSimpCache(reflexivityRule(e2));
251  }
252  IF_DEBUG(d_simpStack.erase(e);)
253  return thm;
254 }
255 
256 
257 Theorem TheoryCore::rewriteCore(const Theorem& e)
258 {
260  "rewriteCore(thm): not equality or iff:\n " + e.toString());
261  return transitivityRule(e, rewriteCore(e.getRHS()));
262 }
263 
264 
265 /* Recurse through s looking for atomic formulas (or terms in the case of
266  * then/else branches of ite's) and use the notifylist mechanism to indicate
267  * that the atomic formula e depends on these atomic formulas and terms. Used
268  * by registerAtom. */
269 void TheoryCore::setupSubFormulas(const Expr& s, const Expr& e,
270  const Theorem& thm)
271 {
272  if (s.isAtomic()) {
273  setupTerm(s, theoryOf(s), thm);
274  s.addToNotify(this, e);
275  }
276  else if (s.isAbsAtomicFormula()) {
277  setupTerm(s, theoryOf(s), thm);
278  for (int i = 0; i < s.arity(); ++i) {
279  s[i].addToNotify(this, e);
280  }
281  if (s != e) s.addToNotify(this, e);
282  }
283  else {
284  for (int i = 0; i < s.arity(); ++i) {
285  setupSubFormulas(s[i], e, thm);
286  }
287  }
288 }
289 
290 
291 void TheoryCore::processUpdates()
292 {
293  Theorem e;
294  Expr d;
295  DebugAssert(d_update_thms.size() == d_update_data.size(),
296  "Expected same size");
297  while (!d_inconsistent && !d_update_thms.empty()) {
298  e = d_update_thms.back();
299  d_update_thms.pop_back();
300  d = d_update_data.back();
301  d_update_data.pop_back();
302 
303  DebugAssert(d.isAbsAtomicFormula(), "Expected atomic formula");
304  Theorem thm = simplify(d);
305  if (thm.getRHS().isTrue()) {
306  setFindLiteral(d_commonRules->iffTrueElim(thm));
307  }
308  else if (thm.getRHS().isFalse()) {
309  setFindLiteral(d_commonRules->iffFalseElim(thm));
310  }
311  else {
312  DebugAssert(e.isRewrite(), "Unexpected theorem in TheoryCore::update");
313  if (e.getRHS().getType().isBool()) continue;
314  find(e.getRHS()).getRHS().addToNotify(this, d);
315  if (thm.getRHS().isAbsAtomicFormula()) thm.getRHS().addToNotify(this, d);
316  }
317  }
318 }
319 
320 
321 void TheoryCore::assertFactCore(const Theorem& e)
322 {
323  IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
324  TRACE("assertFactCore", indentStr, "AssertFactCore: ", e.getExpr().toString(PRESENTATION_LANG));
325 
326  Theorem estarThm(e);
327  Expr estar = e.getExpr();
328  IF_DEBUG(Expr e2 = estar;)
329  Theorem equiv = simplify(estar);
330  if (!equiv.isRefl()) {
331  estarThm = iffMP(e, equiv);
332  // Make sure originally asserted atomic formulas have a find pointer
333  if (!estar.isTrue() && estar.isAbsLiteral()) {
334  setFindLiteral(e);
335  }
336  estar = estarThm.getExpr();
337  }
338  if (estar.isAbsLiteral()) {
339  if (estar.isEq()) {
340  Theorem solvedThm(solve(estarThm));
341  if(estar != solvedThm.getExpr()) setFindLiteral(estarThm);
342  if (!solvedThm.getExpr().isTrue())
343  assertEqualities(solvedThm);
344  }
345  else if (estar.isFalse()) {
346  IF_DEBUG(debugger.counter("conflicts from simplifier")++;)
347  setInconsistent(estarThm);
348  }
349  else if (!estar.isTrue()) {
350  assertFormula(estarThm);
351  }
352  else {
353  // estar is true, nothing will be done
354  // Make sure equivalence classes of equations between two terms with finds get merged
355  // We skip this check for now because unsolvable nonlinear equations bring up this kind of
356  // problems, i.e. x^2 + y^2 = z^2 is not solved, it is true, but the find of LHS and RHS are
357  // different
358  if (!incomplete() && e.isRewrite() &&
359  e.getLHS().hasFind() && e.getRHS().hasFind() &&
360  find(e.getLHS()).getRHS() != find(e.getRHS()).getRHS()) {
361  TRACE("assertFactCore", "Problem (LHS of): ", e.getExpr(), "");
362  TRACE("assertFactCore", find(e.getLHS()).getRHS(), " vs ", find(e.getRHS()).getRHS());
363  IF_DEBUG(cerr << "Warning: Equivalence classes didn't get merged" << endl;)
364  }
365  }
366  } else if (estar.isAnd()) {
367  for(int i=0,iend=estar.arity(); i<iend && !d_inconsistent; ++i)
368  assertFactCore(d_commonRules->andElim(estarThm, i));
369  return;
370  }
371  else {
372  // Notify the search engine
373  enqueueSE(estarThm);
374  }
375 
376  DebugAssert(!e2.isAbsLiteral() || e2.hasFind()
377  || (e2.isNot() && e2[0].hasFind()),
378  "assertFactCore: e2 = "+e2.toString());
379  DebugAssert(!estar.isAbsLiteral() || estar.hasFind()
380  || (estar.isNot() && estar[0].hasFind()),
381  "assertFactCore: estar = "+estar.toString());
382 }
383 
384 
385 void TheoryCore::assertFormula(const Theorem& thm)
386 {
387  const Expr& e = thm.getExpr();
388  DebugAssert(e.isAbsLiteral(),"assertFormula: nonliteral asserted:\n "
389  +thm.toString());
390  IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
391  TRACE("assertFormula",indentStr,"AssertFormula: ", e.toString(PRESENTATION_LANG));
392 
393  Theory* i = theoryOf(e);
394  Theory* i2 = i;
395 
396  // Recursively set up terms in this formula
397  setupTerm(e,i,thm);
398 
399  // Use find to force af to rewrite to TRUE and NOT af to rewrite to FALSE,
400  // where af is an atomic formula. If af is an equality, make sure its lhs
401  // is greater than its rhs so the simplifier will be able to use the find.
402  DebugAssert(!e.isNot() || (!e.hasFind() && !e[0].hasFind()),
403  "Expected negated argument to assertFormula to not have find");
404  setFindLiteral(thm);
405 
406  // Special processing for existentials, equalities, disequalities
407  switch (e.getKind()) {
408  case EXISTS:
409  // Do not send existential quantifiers to DPs; instead, skolemize them
410  enqueueFact(d_commonRules->skolemize(thm));
411  return;
412  case NOT:
413  if (e[0].isEq()) {
414 
415  // Save the disequality for later processing
416  e[0][0].addToNotify(this, e);
417  e[0][1].addToNotify(this, e);
418  i2 = theoryOf(getBaseType(e[0][0]));
419  DebugAssert(e[0][0] > e[0][1], "Expected lhs of diseq to be greater");
420 // if(e[0][0] < e[0][1]) {
421 // Expr e2 = e[0][1].eqExpr(e[0][0]);
422 // DebugAssert(!e2.hasFind(), "already has find");
423 // thm2 = transitivityRule(d_commonRules->rewriteUsingSymmetry(e2),
424 // d_commonRules->notToIff(thm));
425 // setFindLiteral(d_commonRules->iffFalseElim(thm2));
426 // }
427  }
428  break;
429  case EQ:
430  i2 = theoryOf(getBaseType(e[0]));
431  if (e[0] < e[1]) {
432  // this can happen because of the solver
433  Expr e2 = e[1].eqExpr(e[0]);
434  if (!e2.hasFind()) {
435  Theorem thm2 =
436  transitivityRule(d_commonRules->rewriteUsingSymmetry(e2),
437  d_commonRules->iffTrue(thm));
438  setFindLiteral(d_commonRules->iffTrueElim(thm2));
439  }
440  }
441  break;
442  default:
443  break;
444  }
445 
446  // Send formula to the appropriate DP
447  i->assertFact(thm);
448 
449  // Equalities and disequalities are also asserted to the theories of
450  // their types
451  if (i != i2) i2->assertFact(thm);
452 }
453 
454 
456 {
457  // Normally, if an expr has a find, we don't need to rewrite, just return the find.
458  // However, if we are in the middle of an update, the find may not yet be updated, so
459  // we should simplify the result.
460  if (e.hasFind()) {
461  Theorem thm = find(e);
462  if (d_inUpdate && !thm.isRefl()) {
463  thm = transitivityRule(thm, simplify(thm.getRHS()));
464  }
465  return thm;
466  }
467 
468  if (e.isRewriteNormal()) {
469  IF_DEBUG(
470  // Check that the RewriteNormal flag is set properly. Note that we
471  // assume theory-specific rewrites are idempotent
472  e.clearRewriteNormal();
473  Expr rewritten(rewriteCore(e).getRHS());
474  e.setRewriteNormal(); // Restore the flag
475  DebugAssert(rewritten == e,
476  "Expected no change: e = " + e.toString()
477  +"\n rewriteCore(e) = "+rewritten.toString());
478  )
479  return reflexivityRule(e);
480  }
481  switch (e.getKind()) {
482  case EQ:
483  if (e[0] < e[1])
484  return rewriteCore(d_commonRules->rewriteUsingSymmetry(e));
485  else if (e[0] == e[1])
486  return d_commonRules->rewriteReflexivity(e);
487  break;
488  case NOT:
489  if (e[0].isNot())
490  return rewriteCore(d_commonRules->rewriteNotNot(e));
491  break;
492  default:
493  break;
494  }
495  Theorem thm = theoryOf(e)->rewrite(e);
496  const Expr& e2 = thm.getRHS();
497 
498  // Theory-specific rewrites for equality should ensure that lhs >= rhs, or
499  // there is danger of an infinite loop.
500  DebugAssert(!e2.isEq() || e2[0] >= e2[1],
501  "theory-specific rewrites for equality should ensure lhs >= rhs");
502  if (e != e2) {
503  thm = rewriteCore(thm);
504  }
505  return thm;
506 }
507 
508 
509 void TheoryCore::setFindLiteral(const Theorem& thm)
510 {
511  const Expr& e = thm.getExpr();
512  NotifyList* L;
513  if (e.isNot()) {
514  const Expr& e0 = e[0];
515  if (!e0.hasFind()) {
516  IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
517  TRACE("setFindLiteral", indentStr, "SFL: ", e.toString(PRESENTATION_LANG));
518  Theorem findThm = d_commonRules->notToIff(thm);
519  e0.setFind(findThm);
520  if (e0.isRegisteredAtom()) {
521  DebugAssert(!e.isImpliedLiteral(), "Should be new implied lit");
522  e.setImpliedLiteral();
523  d_impliedLiterals.push_back(thm);
524  }
525  d_em->invalidateSimpCache();
526  L = e0.getNotify();
527  if (L) processNotify(findThm, L);
528  }
529  else {
530  Theorem findThm = find(e0);
531  if (findThm.getRHS().isTrue()) {
532  setInconsistent(iffMP(d_commonRules->iffTrueElim(findThm),
533  d_commonRules->notToIff(thm)));
534  }
535  }
536  }
537  else if (!e.hasFind()) {
538  IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
539  TRACE("setFindLiteral", indentStr, "SFL: ", e.toString(PRESENTATION_LANG));
540  Theorem findThm = d_commonRules->iffTrue(thm);
541  e.setFind(findThm);
542  if (e.isRegisteredAtom()) {
543  DebugAssert(!e.isImpliedLiteral(), "Should be new implied lit");
544  e.setImpliedLiteral();
545  d_impliedLiterals.push_back(thm);
546  }
547  d_em->invalidateSimpCache();
548  L = e.getNotify();
549  if (L) processNotify(findThm, L);
550  }
551  else {
552  Theorem findThm = find(e);
553  if (findThm.getRHS().isFalse()) {
554  setInconsistent(iffMP(thm, findThm));
555  }
556  }
557 }
558 
559 
560 Theorem TheoryCore::rewriteLitCore(const Expr& e)
561 {
562  switch (e.getKind()) {
563  case EQ:
564  if (e[0] == e[1])
565  return d_commonRules->rewriteReflexivity(e);
566  else if (e[0] < e[1])
567  return d_commonRules->rewriteUsingSymmetry(e);
568  break;
569  case NOT:
570  if (e[0].isTrue())
571  return d_commonRules->rewriteNotTrue(e);
572  else if (e[0].isFalse())
573  return d_commonRules->rewriteNotFalse(e);
574  else if (e[0].isNot())
575  return d_commonRules->rewriteNotNot(e);
576  break;
577  default:
578  DebugAssert(false,
579  "TheoryCore::rewriteLitCore("
580  + e.toString()
581  + "): Not implemented");
582  break;
583  }
584  return reflexivityRule(e);
585 }
586 
587 
588 void TheoryCore::enqueueSE(const Theorem& thm)
589 {
590  DebugAssert(okToEnqueue(), "enqueueSE()");
591  d_queueSE.push_back(thm);
592 }
593 
594 
595 Theorem TheoryCore::getModelValue(const Expr& e)
596 {
597  ExprHashMap<Theorem>::iterator i=d_varAssignments.find(e),
598  iend=d_varAssignments.end();
599  if(i!=iend) return (*i).second;
600  else return find(e);
601 }
602 
603 
604 //! An auxiliary recursive function to process COND expressions into ITE
605 Expr TheoryCore::processCond(const Expr& e, int i)
606 {
607  DebugAssert(i < e.arity()-1, "e = "+e.toString()+", i = "+int2string(i));
608  if(i == e.arity()-2) {
609  if(e[i].getKind() == RAW_LIST && e[i].arity() == 2
610  && e[i+1].getKind() == RAW_LIST && e[i+1].arity() == 2
611  && e[i+1][0].getKind() == ID && e[i+1][0][0].getString() == "_ELSE") {
612  Expr c(parseExpr(e[i][0]));
613  Expr e1(parseExpr(e[i][1]));
614  Expr e2(parseExpr(e[i+1][1]));
615  return c.iteExpr(e1,e2);
616  }
617  } else {
618  if(e[i].getKind() == RAW_LIST && e[i].arity() == 2
619  && e[i+1].getKind() == RAW_LIST && e[i+1].arity() == 2) {
620  Expr c(parseExpr(e[i][0]));
621  Expr e1(parseExpr(e[i][1]));
622  Expr e2(processCond(e, i+1));
623  return c.iteExpr(e1,e2);
624  }
625  }
626  throw ParserException("Parse Error: bad COND expression: "+e.toString());
627 }
628 
629 
630 bool TheoryCore::isBasicKind(int kind)
631 {
632  switch (kind) {
633  case VARDECLS:
634  case LETDECLS:
635  case HELP:
636  case GET_VALUE:
637  case GET_ASSIGNMENT:
638  case DUMP_PROOF:
639  case DUMP_ASSUMPTIONS:
640  case DUMP_SIG:
641  case DUMP_TCC:
643  case DUMP_TCC_PROOF:
644  case DUMP_CLOSURE:
645  case DUMP_CLOSURE_PROOF:
646  case WHERE:
647  case ASSERTIONS:
648  case ASSUMPTIONS:
649  case COUNTEREXAMPLE:
650  case COUNTERMODEL:
651  case ASSERT:
652  case PRINT:
653  case QUERY:
654  case CHECKSAT:
655  case CONTINUE:
656  case RESTART:
657  case TRACE:
658  case ECHO:
659  case UNTRACE:
660  case VARLIST:
661  case FORGET:
662  case GET_TYPE:
663  case IFF:
664  case IMPLIES:
665  case TYPEDEF:
666  case OPTION:
667  case AND:
668  case OR:
669  case XOR:
670  case NOT:
671  case DISTINCT:
672  case CALL:
673  case TRANSFORM:
674  case CHECK_TYPE:
675  case VARDECL:
676  case GET_CHILD:
677  case SUBSTITUTE:
678  case SEQ:
679  case DBG:
680  case PUSH:
681  case POP:
682  case POPTO:
683  case PUSH_SCOPE:
684  case POP_SCOPE:
685  case POPTO_SCOPE:
686  case RESET:
687  case LETDECL:
688  case ELSE:
689  case CONTEXT:
690  return true;
691  default:
692  break;
693  }
694  return false;
695 }
696 
697 
698 TheoryCore::TheoryCore(ContextManager* cm,
699  ExprManager* em,
700  TheoremManager* tm,
701  Translator* translator,
702  const CLFlags& flags,
703  Statistics& statistics)
704  : Theory(), d_cm(cm), d_tm(tm), d_flags(flags), d_statistics(statistics),
705  d_translator(translator),
706  d_inconsistent(cm->getCurrentContext(), false, 0),
707  d_incomplete(cm->getCurrentContext()),
708  d_incThm(cm->getCurrentContext()),
709  d_terms(cm->getCurrentContext()),
710  // d_termTheorems(cm->getCurrentContext()),
711  d_predicates(cm->getCurrentContext()),
712  d_solver(NULL),
713  d_simplifyInPlace(false),
714  d_currentRecursiveSimplifier(NULL),
715  d_resourceLimit(0),
716  d_timeBase(0),
717  d_timeLimit(0),
718  d_inCheckSATCore(false), d_inAddFact(false),
719  d_inRegisterAtom(false), d_inPP(false),
720  d_notifyObj(this, cm->getCurrentContext()),
721  d_impliedLiterals(cm->getCurrentContext()),
722  d_impliedLiteralsIdx(cm->getCurrentContext(), 0, 0),
723  d_notifyEq(cm->getCurrentContext()),
724  d_inUpdate(0),
725  d_coreSatAPI(NULL)
726 {
727  d_em = em;
728  // Since we are in the middle of creating TheoryCore, we set the pointer to
729  // TheoryCore in the Theory base class ourselves.
730  d_theoryCore = this;
731  d_commonRules = tm->getRules();
732  d_name = "Core";
733  d_theoryUsed = false;
734 
736  d_printer = new PrettyPrinterCore(this);
737  d_typeComputer = new TypeComputerCore(this);
739  d_exprTrans = new ExprTransform(this);
740 
741  // Register the pretty-printer
743 
744  // for (int i = 0; i < LAST_KIND; ++i) d_theoryMap[i] = NULL;
745 
746  vector<int> kinds;
747  kinds.push_back(RAW_LIST);
748  kinds.push_back(BOOLEAN);
749  kinds.push_back(ANY_TYPE);
750  kinds.push_back(SUBTYPE);
751  kinds.push_back(STRING_EXPR);
752  kinds.push_back(ID);
753  kinds.push_back(TRUE_EXPR);
754  kinds.push_back(FALSE_EXPR);
755  kinds.push_back(UCONST);
756  kinds.push_back(BOUND_VAR);
757  kinds.push_back(SKOLEM_VAR);
758  kinds.push_back(EQ);
759  kinds.push_back(NEQ);
760  kinds.push_back(DISTINCT);
761  kinds.push_back(ECHO);
762  kinds.push_back(DBG);
763  kinds.push_back(TRACE);
764  kinds.push_back(UNTRACE);
765  kinds.push_back(OPTION);
766  kinds.push_back(HELP);
767  kinds.push_back(AND);
768  kinds.push_back(OR);
769  kinds.push_back(IFTHEN);
770  kinds.push_back(IF);
771  kinds.push_back(ELSE);
772  kinds.push_back(COND);
773  kinds.push_back(XOR);
774  kinds.push_back(NOT);
775  kinds.push_back(ITE);
776  kinds.push_back(IFF);
777  kinds.push_back(IMPLIES);
778  kinds.push_back(APPLY);
779  // For printing LET expressions (in DAG printing mode)
780  kinds.push_back(LET);
781  kinds.push_back(LETDECLS);
782  kinds.push_back(LETDECL);
783  // For printing raw parsed quantifier expressions
784  kinds.push_back(VARLIST);
785  kinds.push_back(VARDECLS);
786  kinds.push_back(VARDECL);
787 
788  // Type declarations and definitions
789  kinds.push_back(TYPE);
790  // For printing type declarations (or definitions)
791  kinds.push_back(CONST);
792 
793  kinds.push_back(TYPEDEF);
794  kinds.push_back(DEFUN);
795  // Printing proofs
796  kinds.push_back(PF_APPLY);
797  kinds.push_back(PF_HOLE);
798  // Register commands for pretty-printing. Currently, only ASSERT
799  // needs to be printed.
800  kinds.push_back(ASSERT);
801  kinds.push_back(QUERY);
802  kinds.push_back(PRINT);
803 
804  kinds.push_back(GET_VALUE);
805  kinds.push_back(GET_ASSIGNMENT);
806  kinds.push_back(DUMP_PROOF);
807  kinds.push_back(DUMP_ASSUMPTIONS);
808  kinds.push_back(DUMP_SIG);
809  kinds.push_back(DUMP_TCC);
810  kinds.push_back(DUMP_TCC_ASSUMPTIONS);
811  kinds.push_back(DUMP_TCC_PROOF);
812  kinds.push_back(DUMP_CLOSURE);
813  kinds.push_back(DUMP_CLOSURE_PROOF);
814  kinds.push_back(TRANSFORM);
815  kinds.push_back(CALL);
816  kinds.push_back(WHERE);
817  kinds.push_back(ASSERTIONS);
818  kinds.push_back(ASSUMPTIONS);
819  kinds.push_back(COUNTEREXAMPLE);
820  kinds.push_back(COUNTERMODEL);
821  kinds.push_back(PUSH);
822  kinds.push_back(POP);
823  kinds.push_back(POPTO);
824  kinds.push_back(PUSH_SCOPE);
825  kinds.push_back(POP_SCOPE);
826  kinds.push_back(POPTO_SCOPE);
827  kinds.push_back(RESET);
828  kinds.push_back(CONTEXT);
829  kinds.push_back(FORGET);
830  kinds.push_back(GET_TYPE);
831  kinds.push_back(CHECK_TYPE);
832  kinds.push_back(GET_CHILD);
833  kinds.push_back(SUBSTITUTE);
834  kinds.push_back(SEQ);
835  kinds.push_back(ARITH_VAR_ORDER);
836  kinds.push_back(ANNOTATION);
837  kinds.push_back(THEOREM_KIND);
838 
839  kinds.push_back(AND_R);
840  kinds.push_back(IFF_R);
841  kinds.push_back(ITE_R);
842 
843  registerTheory(this, kinds);
844 }
845 
846 
848 {
849  delete d_exprTrans;
850  delete d_rules;
851  delete d_typeComputer;
853  delete d_printer;
854 }
855 
856 
858 {
859  Theorem thm = reflexivityRule(e);
860  for(unsigned i=1; i<d_theories.size(); ++i) {
861  thm = transitivityRule(thm, d_theories[i]->theoryPreprocess(thm.getRHS()));
862  }
864  return thm;
865 }
866 
867 
869 
870 // <<<<<<< theory_core_sat.cpp
871 // // DebugAssert(e.hasFind(), "getTheoremForTerm called on term without find");
872 // CDMap<Expr, Theorem>::iterator i = d_termTheorems.find(e);
873 // if( i == d_termTheorems.end()){
874 // TRACE("quantlevel", "getTheoremForTerm: no theorem found: ", e , "");
875 // Theorem nul;
876 // return nul;
877 // }
878 // // DebugAssert(i != d_termTheorems.end(), "getTheoremForTerm: no theorem found");
879 // =======
880 // DebugAssert(e.hasFind() || e.isStoredPredicate(), "getTheoremForTerm called on invalid term");
881 
883  // yeting, I think we should use CDMap here, but a static map works better.
884  // CDMap<Expr, Theorem>::iterator i = d_termTheorems.find(e);
885 
886  // DebugAssert(i != d_termTheorems.end(), "getTheoremForTerm: no theorem found");
887 
888  if(i != d_termTheorems.end()){
889  return (*i).second;
890  }
891  else{
892  TRACE("quantlevel", "getTheoremForTerm: no theorem found: ", e , "");
893  Theorem x;
894  return x;
895  }
896 }
897 
898 #ifdef _CVC3_DEBUG_MODE
900  return theoryOf(FORALL)->help(1);
901 }
902 #endif
903 
905 {
906 
907 
908 /*
909  if (!e.hasFind() && !e.isStoredPredicate()) {
910  TRACE("quantlevel", "get 0 ", e , "");
911  return 0;
912  }
913 */
914  TRACE("quantlevel", "trying get level for (" + e.toString() + ") with index ", "", e.getIndex());
915  Theorem thm = getTheoremForTerm(e);
916  if (thm.isNull()) {
917  if(e.isNot()){
918  thm = getTheoremForTerm(e[0]);
919  }
920  }
921 
922  if(thm.isNull()){
923  if (e.inUserAssumption()) {
924  return 0 ;
925  }
926  else{
927  TRACE("quantlevel", "expr get null :", e.getIndex(), "" );
928  if( ! (e.isNot() || e.isIff())){
929  TRACE("quantlevel", "cannot find expr: " , e, "");
930  }
931  return 0;
932  }
933  }
934 
935  TRACE("quantlevel", "expr get level:", thm.getQuantLevel(), "");
936 
937  /*
938  if(thm.getQuantLevel() != thm.getQuantLevelDebug()){
939  cout << "theorem: " << thm.getExpr().toString() <<endl;
940  cout << "quant level : " << thm.getQuantLevel()<<endl;
941  cout << "debug quant level : " << thm.getQuantLevelDebug() <<endl;
942  cout << "the proof is " << thm.getProof() << endl;
943  }
944  */
945 
946  return thm.getQuantLevel();
947  /*
948  unsigned ql = thm.getQuantLevel();
949  unsigned qld = thm.getQuantLevelDebug();
950  return (ql > qld ? ql : qld);
951  */
952 }
953 
954 
955 ///////////////////////////////////////////////////////////////////////////////
956 // Theory interface implementaion //
957 ///////////////////////////////////////////////////////////////////////////////
958 
959 
961 {
963  e.getExpr().unnegate().getKind() == UCONST,
964  "TheoryCore::assertFact("+e.toString()+")");
965 }
966 
967 
969 {
970  Theorem thm;
971  switch (e.getKind()) {
972  case TRUE_EXPR:
973  case FALSE_EXPR:
974  case UCONST:
975  case BOUND_VAR:
976  case SKOLEM_VAR:
977  thm = reflexivityRule(e);
978  break; // do not rewrite
979  case LETDECL:
980  // Replace LETDECL with its definition. The
981  // typechecker makes sure it's type-safe to do so.
982  thm = d_rules->rewriteLetDecl(e);
983  break;
984  case APPLY:
985  //TODO: this is a bit of a hack
986  if (e.getOpKind() == LAMBDA)
987  thm = theoryOf(LAMBDA)->rewrite(e);
988  else thm = reflexivityRule(e);
989  break;
990  case EQ:
991  case NOT:
992  thm = rewriteLitCore(e);
993  break;
994  case DISTINCT: {
995  Theorem thm1 = d_rules->rewriteDistinct(e);
996  thm = transitivityRule(thm1, simplify(thm1.getRHS()));
997  break;
998  }
999  case IMPLIES: {
1000  thm = d_rules->rewriteImplies(e);
1001  const Expr& rhs = thm.getRHS();
1002  // rhs = OR(!e1, e2). Rewrite !e1, then top-level OR().
1003  DebugAssert(rhs.isOr() && rhs.arity() == 2,
1004  "TheoryCore::rewrite[IMPLIES]: rhs = "+rhs.toString());
1005  Theorem rw = rewriteCore(rhs[0]);
1006  if (!rw.isRefl()) {
1007  vector<unsigned> changed;
1008  vector<Theorem> thms;
1009  changed.push_back(0);
1010  thms.push_back(rw);
1011  rw = substitutivityRule(rhs, changed, thms);
1012  // Simplify to the find pointer of the result
1013  rw = transitivityRule(rw, find(rw.getRHS()));
1014  // Now rw = Theorem(rhs = rhs')
1015  rw = transitivityRule(rw, rewrite(rw.getRHS()));
1016  } else
1017  rw = rewrite(rhs);
1018  thm = transitivityRule(thm, rw);
1019  // thm = transitivityRule(thm, simplify(thm.getRHS()));
1020  break;
1021  }
1022  case XOR: {
1023  thm = d_commonRules->xorToIff(e);
1024  thm = transitivityRule(thm, simplify(thm.getRHS()));
1025  break;
1026  }
1027  case IFF: {
1028  thm = d_commonRules->rewriteIff(e);
1029  Expr e1 = thm.getRHS();
1030  // The only time we need to rewrite the result (e1) is when
1031  // e==(FALSE<=>e[1]) or (e[1]<=>FALSE), so e1==!e[1].
1032  if (e != e1 && e1.isNot())
1033  thm = transitivityRule(thm, rewriteCore(e1));
1034  break;
1035  }
1036  case ITE:
1037  thm = rewriteIte(e);
1038  if (!thm.isRefl()) break;
1039  else if (getFlags()["un-ite-ify"].getBool()) {
1040  // undo the rewriting of Boolean connectives to ITEs.
1041  // helpful for examples converted from SVC.
1042  // must rewrite again because we might create expressions
1043  // that can be further rewritten, and we must normalize.
1044  if (e[1].isFalse() && e[2].isTrue())
1045  thm = rewriteCore(d_rules->rewriteIteToNot(e));
1046  else if (e[1].isTrue())
1047  thm = rewriteCore(d_rules->rewriteIteToOr(e));
1048  else if (e[2].isFalse())
1049  thm = rewriteCore(d_rules->rewriteIteToAnd(e));
1050  else if (e[2].isTrue())
1051  thm = rewriteCore(d_rules->rewriteIteToImp(e));
1052  else if (e[1] == e[2].negate())
1053  thm = rewriteCore(d_rules->rewriteIteToIff(e));
1054  else thm = reflexivityRule(e);
1055  }
1056  else if(getFlags()["ite-cond-simp"].getBool()) {
1057  thm = d_rules->rewriteIteCond(e);
1058  if (!thm.isRefl()) {
1059  thm = transitivityRule(thm, simplify(thm.getRHS()));
1060  }
1061  }
1062  else thm = reflexivityRule(e);
1063  break;
1064  case AND: {
1065  thm = rewriteAnd(e);
1066  Expr ee = thm.getRHS();
1067  break;
1068  }
1069  case OR: {
1070  thm = rewriteOr(e);
1071  Expr ee = thm.getRHS();
1072  break;
1073  }
1074  // Quantifiers
1075  case FORALL:
1076  case EXISTS:
1077  thm = d_commonRules->reflexivityRule(e);
1078  break;
1079  // don't need to rewrite these
1080  case AND_R:
1081  case IFF_R:
1082  case ITE_R:
1083  thm = reflexivityRule(e);
1084  break;
1085  default:
1086  DebugAssert(false,
1087  "TheoryCore::rewrite("
1088  + e.toString() + " : " + e.getType().toString()
1089  + "): Not implemented");
1090  break;
1091  }
1092 
1093  DebugAssert(thm.getLHS() == e, "TheoryCore::rewrite("+e.toString()
1094  +") = "+thm.getExpr().toString());
1095 
1096  Expr rhs = thm.getRHS();
1097  // Advanced Boolean rewrites
1098  switch(rhs.getKind()) {
1099  case AND:
1100  if(getFlags()["simp-and"].getBool()) {
1101  Theorem tmp(reflexivityRule(rhs));
1102  for(int i=0, iend=rhs.arity(); i<iend; ++i) {
1103  tmp = transitivityRule
1104  (tmp, d_rules->rewriteAndSubterms(tmp.getRHS(), i));
1105  }
1106  if(tmp.getRHS() != rhs) { // Something changed: simplify recursively
1107  thm = transitivityRule(thm, tmp);
1108  thm = transitivityRule(thm, simplify(thm.getRHS()));
1109  rhs = thm.getRHS();
1110  }
1111  }
1112  break;
1113  case OR:
1114  if(getFlags()["simp-or"].getBool()) {
1115  Theorem tmp(reflexivityRule(rhs));
1116  for(int i=0, iend=rhs.arity(); i<iend; ++i) {
1117  tmp = transitivityRule
1118  (tmp, d_rules->rewriteOrSubterms(tmp.getRHS(), i));
1119  }
1120  if(tmp.getRHS() != rhs) { // Something changed: simplify recursively
1121  thm = transitivityRule(thm, tmp);
1122  thm = transitivityRule(thm, simplify(thm.getRHS()));
1123  rhs = thm.getRHS();
1124  }
1125  }
1126  break;
1127  default:
1128  break;
1129  }
1130  if (theoryOf(rhs) == this) {
1131  // Core rewrites are idempotent (FIXME: are they, still?)
1132  rhs.setRewriteNormal();
1133  }
1134  return thm;
1135 }
1136 
1137 
1138 /*! We use the update method of theory core to track registered atomic
1139  * formulas. Updates are recorded and then processed by calling processUpdates
1140  * once all equalities have been processed. */
1141 void TheoryCore::update(const Theorem& e, const Expr& d)
1142 {
1143  // Disequalities
1144  if (d.isNot()) {
1145  const Expr& eq = d[0];
1146  DebugAssert(eq.isEq(), "Expected equality");
1147  Theorem thm1(find(eq[0]));
1148  Theorem thm2(find(eq[1]));
1149  const Expr& newlhs = thm1.getRHS();
1150  const Expr& newrhs = thm2.getRHS();
1151  if (newlhs == newrhs) {
1152  Theorem thm = find(eq);
1153  DebugAssert(thm.getRHS().isFalse(), "Expected disequality");
1154  Theorem leftEqRight = transitivityRule(thm1, symmetryRule(thm2));
1155  setInconsistent(iffMP(leftEqRight, thm));
1156  }
1157  else {
1158  e.getRHS().addToNotify(this, d);
1159  // propagate new disequality
1160  Theorem thm = d_commonRules->substitutivityRule(eq, thm1, thm2);
1161  if (newlhs < newrhs) {
1163  }
1164  const Expr& newEq = thm.getRHS();
1165  if (newEq.hasFind()) {
1166  Theorem thm2 = find(newEq);
1167  if (thm2.getRHS().isTrue()) {
1168  thm2 = transitivityRule(thm, thm2);
1169  thm = find(eq);
1170  DebugAssert(thm.getRHS().isFalse(), "Expected disequality");
1171  thm = transitivityRule(symmetryRule(thm), thm2);
1173  }
1174  // else if thm2.getRHS().isFalse(), nothing to do
1175  }
1176  else {
1177  Theorem thm2 = find(eq);
1178  DebugAssert(thm2.getRHS().isFalse(), "Expected disequality");
1179  thm2 = transitivityRule(symmetryRule(thm),thm2);
1181  }
1182  }
1183  }
1184  // Registered atoms
1185  else {
1186  DebugAssert(d.isRegisteredAtom(), "Expected registered atom");
1187  if (!d.isImpliedLiteral()) {
1188  d_update_thms.push_back(e);
1189  d_update_data.push_back(d);
1190  }
1191  }
1192 }
1193 
1194 
1196 {
1197  Expr e2 = thm.getExpr();
1198  DebugAssert(e2.isEq(), "Expected equation");
1199  Expr solved;
1200  if (d_solver) {
1201  solved = d_solver->solve(thm).getExpr();
1202  DebugAssert(solved == e2, "e2 = "+e2.toString()
1203  +"\nsolved = "+solved.toString());
1204  }
1205  Theory* i = theoryOf(e2);
1206  if (d_solver != i) {
1207  solved = i->solve(thm).getExpr();
1208  DebugAssert(solved == e2, "e2 = "+e2.toString()
1209  +"\nsolved = "+solved.toString());
1210  }
1211  Theory* j = theoryOf(e2[0].getType());
1212  if (d_solver != j && i != j) {
1213  solved = j->solve(thm).getExpr();
1214  DebugAssert(solved == e2, "e2 = "+e2.toString()
1215  +"\nsolved = "+solved.toString());
1216  }
1217 }
1218 
1219 
1221 {
1222  Expr e2 = thm.getExpr();
1223  if (e2.isAnd()) {
1224  for (int index = 0; index < e2.arity(); ++index) {
1225  checkEquation(d_commonRules->andElim(thm, index));
1226  }
1227  }
1228  else if (!e2.isBoolConst()) checkEquation(thm);
1229 }
1230 
1231 
1232 /*****************************************************************************/
1233 /*!
1234  * Function: TheoryCore::solve
1235  *
1236  * Author: Clark Barrett
1237  *
1238  * Created: Wed Feb 26 16:17:54 2003
1239  *
1240  * This is a generalization of what's in my thesis. The goal is to rewrite e
1241  * into an equisatisfiable conjunction of equations such that the left-hand
1242  * side of each equation is a variable which does not appear as an i-leaf of
1243  * the rhs, where i is the theory of the primary solver. Any solution which
1244  * satisfies this is fine. "Solvers" from other theories can do whatever they
1245  * want as long as we eventually reach this form.
1246  */
1247 /*****************************************************************************/
1249 {
1250  const Expr& e = eThm.getExpr();
1251  Theorem thm;
1252  Expr e2;
1253 
1254  DebugAssert(eThm.isRewrite() && eThm.getLHS().isTerm(), "Expected equation");
1255 
1256  // Invoke the primary solver
1257  if (d_solver) {
1258  thm = d_solver->solve(eThm);
1259  e2 = thm.getExpr();
1260  if (e2.isBoolConst() || e2.isAnd()) {
1261  // We expect a conjunction of equations, each of which is terminally solved
1262  IF_DEBUG(checkSolved(thm));
1263  return thm;
1264  }
1265  }
1266  else {
1267  thm = eThm;
1268  e2 = e;
1269  }
1270 
1271  // Invoke solver based on owner of equation
1272  DebugAssert(e2.isEq(), "Expected equation");
1273  Theory* i = theoryOf(e2);
1274  if (d_solver != i) thm = i->solve(thm);
1275  e2 = thm.getExpr();
1276  if (e2.isBoolConst() || e2.isAnd()) {
1277  // We expect a conjunction of equations, each of which is solved
1278  IF_DEBUG(checkSolved(thm));
1279  return thm;
1280  }
1281 
1282  // Invoke solver based on type of terms in equation
1283  DebugAssert(e2.isEq(), "Expected equation");
1284  Theory* j = theoryOf(getBaseType(e2[0]));
1285  if (d_solver != j && i != j) thm = j->solve(thm);
1286 
1287  IF_DEBUG(checkSolved(thm));
1288  return thm;
1289 }
1290 
1291 
1293 {
1294  int kind(e.getKind());
1295 
1296  switch(kind) {
1297  case EQ:
1298  case IFF:
1299  if(e[0]==e[1]) {
1300  IF_DEBUG(debugger.counter("simplified x=x")++;)
1301  return d_commonRules->iffTrue(reflexivityRule(e[0]));
1302  }
1303  return Theory::simplifyOp(e);
1304  case AND:
1305  case OR: {
1306  // Stop when a child has this kind
1307  int endKind = (kind==AND)? FALSE_EXPR : TRUE_EXPR;
1308  int ar = e.arity();
1309  // Optimization: before simplifying anything recursively, check if
1310  // any kid is already TRUE or FALSE, and just return at that point
1311  int l(0);
1312  for(; l<ar && e[l].getKind() != endKind; ++l);
1313  if(l < ar) { // Found TRUE or FALSE: e simplifies to a const
1314  IF_DEBUG(debugger.counter("simplified AND/OR topdown")++;)
1315  if(kind==AND)
1316  return rewriteAnd(e);
1317  else
1318  return rewriteOr(e);
1319  }
1320  vector<Theorem> newChildrenThm;
1321  vector<unsigned> changed;
1322  for(int k = 0; k < ar; ++k) {
1323  // Recursively simplify the kids
1324  Theorem thm = simplify(e[k]);
1325  if (!thm.isRefl()) {
1326  if (thm.getRHS().getKind() == endKind) {
1327  newChildrenThm.clear();
1328  changed.clear();
1329  newChildrenThm.push_back(thm);
1330  changed.push_back(k);
1331  thm = substitutivityRule(e, changed, newChildrenThm);
1332  // Simplify to TRUE or FALSE
1333  if(kind==AND)
1334  thm = transitivityRule(thm, rewriteAnd(thm.getRHS()));
1335  else
1336  thm = transitivityRule(thm, rewriteOr(thm.getRHS()));
1337  IF_DEBUG(debugger.counter("simplified AND/OR: skipped kids")
1338  += ar-k-1;)
1339  return thm;
1340  } else { // Child simplified to something else
1341  newChildrenThm.push_back(thm);
1342  changed.push_back(k);
1343  }
1344  }
1345  }
1346  if(changed.size() > 0)
1347  return substitutivityRule(e, changed, newChildrenThm);
1348  break;
1349  }
1350  case ITE: {
1351  DebugAssert(e.arity()==3, "Bad ITE in TheoryCore::simplify(e="
1352  +e.toString()+")");
1353  // Optimization: check if the two branches are the same, so we
1354  // don't have to simplify the condition
1355  if(e[1]==e[2]) {
1356  IF_DEBUG(debugger.counter("simplified ITE(c,e,e)")++;)
1358  return transitivityRule(res, simplify(res.getRHS()));
1359  }
1360 
1361  // First, simplify the conditional
1362  vector<Theorem> newChildrenThm;
1363  vector<unsigned> changed;
1364  Theorem thm = simplify(e[0]);
1365  if (!thm.isRefl()) {
1366  newChildrenThm.push_back(thm);
1367  changed.push_back(0);
1368  }
1369  Expr cond = thm.getRHS();
1370 
1371  for(int k=1; k<=2; ++k) {
1372  // If condition value is known, only the appropriate branch
1373  // needs to be simplified
1374  if (cond.isBoolConst()) {
1375  if((k==1 && cond.isFalse()) || (k==2 && cond.isTrue())) {
1376  IF_DEBUG(debugger.counter("simplified ITE: skiped one branch")++;)
1377  continue;
1378  }
1379  }
1380  thm = simplify(e[k]);
1381  if (!thm.isRefl()) {
1382  newChildrenThm.push_back(thm);
1383  changed.push_back(k);
1384  }
1385  }
1386  if(changed.size() > 0)
1387  return substitutivityRule(e, changed, newChildrenThm);
1388  break;
1389  }
1390  case NOT: {
1391  Theorem res = simplify(e[0]);
1392  if (!res.isRefl()) {
1393  return d_commonRules->substitutivityRule(e, res);
1394  }
1395  break;
1396  }
1397  case IMPLIES: {
1398  Theorem res = d_rules->rewriteImplies(e);
1399  return transitivityRule(res, simplifyOp(res.getRHS()));
1400  }
1401  default:
1402  return Theory::simplifyOp(e);
1403  }
1404  return reflexivityRule(e);
1405 }
1406 
1407 
1409 {
1410  switch (e.getKind()) {
1411  case BOOLEAN:
1412  if (e.arity() > 0) {
1413  throw Exception("Ill-formed Boolean type:\n\n"+e.toString());
1414  }
1415  break;
1416  case SUBTYPE: {
1417  if (e.arity() != 1)
1418  throw Exception("Ill-formed SUBTYPE expression:\n\n"+e.toString());
1419  Type t = e[0].getType();
1420  if (!t.isFunction())
1421  throw Exception
1422  ("Non-function argument to SUBTYPE:\n\n"
1423  +e.toString());
1424  if (!t[1].isBool())
1425  throw Exception
1426  ("Non-predicate argument to SUBTYPE:\n\n"
1427  +e.toString());
1428  }
1429  break;
1430  case ANY_TYPE: {
1431  if (e.arity() != 0) {
1432  throw Exception("Expected no children: "+e.toString());
1433  }
1434  break;
1435  }
1436  default:
1437  FatalAssert(false, "Unexpected kind in TheoryCore::checkType"
1438  +getEM()->getKindName(e.getKind()));
1439  }
1440 }
1441 
1442 
1444  bool enumerate, bool computeSize)
1445 {
1446  Cardinality card = CARD_INFINITE;
1447  switch (e.getKind()) {
1448  case BOOLEAN:
1449  card = CARD_FINITE;
1450  if (enumerate) {
1451  e = (n == 0) ? falseExpr() : (n == 1) ? trueExpr() : Expr();
1452  }
1453  if (computeSize) {
1454  n = 2;
1455  }
1456  break;
1457  case SUBTYPE:
1458  card = CARD_UNKNOWN;
1459  break;
1460  case ANY_TYPE:
1461  card = CARD_UNKNOWN;
1462  break;
1463  default:
1464  FatalAssert(false, "Unexpected kind in TheoryCore::finiteTypeInfo"
1465  +getEM()->getKindName(e.getKind()));
1466  }
1467  return card;
1468 }
1469 
1470 
1472 {
1473  switch (e.getKind()) {
1474  case ITE: {
1475  Type t1(getBaseType(e[1])), t2(getBaseType(e[2]));
1476  if (e[0].getType() != boolType())
1477  throw TypecheckException
1478  ("The conditional in IF-THEN-ELSE must be BOOLEAN, but is:\n\n"
1479  +e[0].getType().toString()
1480  +"\n\nIn the expression:\n\n "
1481  +e.toString());
1482  if(t1 != t2) {
1483  throw TypecheckException
1484  ("The types of the IF-THEN-ELSE branches do not match.\n"
1485  "THEN branch has the type:\n\n "
1486  +e[1].getType().toString()
1487  +"\n\nELSE branch has the type:\n\n "
1488  +e[2].getType().toString()
1489  +"\n\nIn expression:\n\n "+e.toString());
1490  }
1491  Type res(e[1].getType());
1492  // If the precise types match in both branches, use it as the
1493  // result type.
1494  if(res == e[2].getType()) {
1495  e.setType(res);
1496  }
1497  else
1498  // Note: setting the base type, since e[1] and e[2] have
1499  // different exact types, and the base type is a conservative
1500  // approximation we can easily compute.
1501  e.setType(t1);
1502  }
1503  break;
1504  case EQ: {
1505  Type t0(getBaseType(e[0])), t1(getBaseType(e[1]));
1506  if (t0.isBool() || t1.isBool()) {
1507  throw TypecheckException
1508  ("Cannot use EQ ('=') for BOOLEAN type; use IFF ('<=>') instead.\n"
1509  "Error in the following expression:\n"+e.toString());
1510  }
1511  if (t0 != t1) {
1512  throw TypecheckException
1513  ("Type mismatch in equality:\n\n LHS type:\n"+t0.toString()
1514  +"\n\n RHS type: \n"+t1.toString()
1515  +"\n\n in expression: \n"+e.toString());
1516  }
1517  e.setType(boolType());
1518  break;
1519  }
1520  case DISTINCT: {
1521  Type t0(getBaseType(e[0]));
1522  for (int i = 1; i < e.arity(); ++i) {
1523  if (t0 != getBaseType(e[i])) {
1524  throw TypecheckException
1525  ("Type mismatch in distinct:\n\n types:\n"+t0.toString()
1526  +"\n\n and type: \n"+getBaseType(e[i]).toString()
1527  +"\n\n in expression: \n"+e.toString());
1528  }
1529  }
1530  e.setType(boolType());
1531  break;
1532  }
1533  case NOT:
1534  case AND:
1535  case OR:
1536  case XOR:
1537  case IFF:
1538  case IMPLIES:
1539 
1540  case AND_R:
1541  case IFF_R:
1542  case ITE_R:
1543 
1544  for (int k = 0; k < e.arity(); ++k) {
1545  if (e[k].getType() != boolType()) {
1546  throw TypecheckException(e.toString());
1547  }
1548  }
1549  if((e.getKind() == NOT && e.arity() != 1) ||
1550  (e.getKind() == IFF && e.arity() != 2) ||
1551  (e.getKind() == IMPLIES && e.arity() != 2)) {
1552  throw TypecheckException("Wrong arity ("+int2string(e.arity())+") for operator: "+e.toString());
1553  }
1554  e.setType(boolType());
1555  break;
1556  case LETDECL: {
1557  Type varTp(getBaseType(e[0]));
1558  Type valTp(getBaseType(e[1]));
1559  if(valTp != varTp) {
1560  throw TypecheckException("Type mismatch for "+e[0].toString()+":"
1561  +"\n declared: "
1562  + varTp.toString()
1563  +"\n derived: "+ valTp.toString());
1564  }
1565  e.setType(e[0].getType());
1566  }
1567  break;
1568  case APPLY:
1569  {
1570  DebugAssert(e.isApply(), "Should be application");
1571  DebugAssert(e.arity() > 0, "Expected non-zero arity in APPLY");
1572  Expr funExpr = e.getOpExpr();
1573  Type funType = funExpr.getType();
1574 
1575  if(!funType.isFunction()) {
1576  throw TypecheckException
1577  ("Expected function type for:\n\n"
1578  + funExpr.toString() + "\n\n but got this: "
1579  +funType.getExpr().toString()
1580  +"\n\n in function application:\n\n"+e.toString());
1581  }
1582 
1583  if(funType.arity() != e.arity()+1)
1584  throw TypecheckException("Type mismatch for expression:\n\n "
1585  + e.toString()
1586  + "\n\nFunction \""+funExpr.toString()
1587  +"\" expects "+int2string(funType.arity()-1)
1588  +" argument"
1589  +string((funType.arity()==2)? "" : "s")
1590  +", but received "
1591  +int2string(e.arity())+".");
1592 
1593  for (int k = 0; k < e.arity(); ++k) {
1594  Type valType(getBaseType(e[k]));
1595  if (funType[k] != Type::anyType(d_em) && !(valType == getBaseType(funType[k]) || valType == Type::anyType(d_em)) ) {
1596  throw TypecheckException("Type mismatch for expression:\n\n "
1597  + e[k].toString()
1598  + "\n\nhas the following type:\n\n "
1599  + e[k].getType().toString()
1600  + "\n\nbut the expected type is:\n\n "
1601  + funType[k].getExpr().toString()
1602  + "\n\nin function application:\n\n "
1603  + e.toString());
1604  }
1605  }
1606  e.setType(funType[funType.arity()-1]);
1607  break;
1608  }
1609  case RAW_LIST:
1610  throw TypecheckException("computeType called on RAW_LIST");
1611  break;
1612  default:
1613  DebugAssert(false,"TheoryCore::computeType(" + e.toString()
1614  + "):\nNot implemented");
1615  break;
1616  }
1617 }
1618 
1619 
1621 {
1622  const Expr& e = tp.getExpr();
1623  Type res;
1624  switch(e.getKind()) {
1625  case SUBTYPE: {
1626  DebugAssert(e.arity() == 1, "Expr::computeBaseType(): "+e.toString());
1627  Type lambdaTp = e[0].getType();
1628  Type lambdaBaseTp = getBaseType(lambdaTp);
1629  DebugAssert(lambdaBaseTp.isFunction(),
1630  "Expr::computeBaseType(): lambdaBaseTp = "
1631  +lambdaBaseTp.toString()+" in e = "+e.toString());
1632  res = lambdaBaseTp[0];
1633  break;
1634  }
1635  case BOOLEAN:
1636  case ANY_TYPE:
1637  res = tp;
1638  break;
1639  case TYPEDEF: // Compute the base type of the definition
1640  res = getBaseType(Type(e[1]));
1641  break;
1642  default:
1643  DebugAssert(false, "TheoryCore::computeBaseType("+tp.toString()+")");
1644  res = tp;
1645  }
1646  return res;
1647 }
1648 
1649 
1651 {
1652  Expr res;
1653  switch (e.getKind()) {
1654  case NOT:
1655  res = getTCC(e[0]);
1656  break;
1657  case AND: {
1658  // ( (tcc(e1) & !e1) \/ ... \/ (tcc(en) & !en) \/ (tcc(e1)&...&tcc(en))
1659  vector<Expr> tccs;
1660  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
1661  tccs.push_back(getTCC(*i));
1662  vector<Expr> pairs;
1663  pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS());
1664  for(size_t i=0, iend=tccs.size(); i<iend; ++i)
1665  pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i].negate())).getRHS());
1666  res = rewriteOr(orExpr(pairs)).getRHS();
1667  break;
1668  }
1669  case OR: {
1670  // ( (tcc(e1) & e1) \/ ... \/ (tcc(en) & en) \/ (tcc(e1)&...&tcc(en))
1671  vector<Expr> tccs;
1672  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
1673  tccs.push_back(getTCC(*i));
1674  vector<Expr> pairs;
1675  pairs.push_back(rewriteAnd(andExpr(tccs)).getRHS());
1676  for(size_t i=0, iend=tccs.size(); i<iend; ++i)
1677  pairs.push_back(rewriteAnd(tccs[i].andExpr(e[i])).getRHS());
1678  res = rewriteOr(orExpr(pairs)).getRHS();
1679  break;
1680  }
1681  case ITE: {
1682  Expr tcc1(getTCC(e[1])), tcc2(getTCC(e[2]));
1683  // Optimize: if TCCs on both branches are the same, skip the ITE
1684  Expr tccITE((tcc1 == tcc2)? tcc1 : e[0].iteExpr(tcc1, tcc2));
1685  res = rewriteAnd(getTCC(e[0]).andExpr(tccITE)).getRHS();
1686  break;
1687  }
1688  case IMPLIES:
1689  res = getTCC(e[0].negate().orExpr(e[1]));
1690  break;
1691  case APPLY: {
1692  Theory* i = theoryOf(e);
1693  if (i != this) return i->computeTCC(e);
1694  // fall through
1695  }
1696  default: // All the other operators are strict
1697  res = Theory::computeTCC(e);
1698  break;
1699  }
1700  return res;
1701 }
1702 
1703 
1705 {
1706  Expr tExpr = t.getExpr();
1707  switch(tExpr.getKind()) {
1708  case SUBTYPE: {
1709  Expr pred = tExpr[0];
1710  const Type& argTp = pred.lookupType()[0];
1711  return Expr(pred.mkOp(), e).andExpr(getTypePred(argTp, e));
1712  }
1713  case APPLY: {
1714  Theory* i = theoryOf(e);
1715  if (i != this) return i->computeTypePred(t, e);
1716  // fall through
1717  }
1718  default:
1719  return e.getEM()->trueExpr();
1720  }
1721 }
1722 
1723 
1725 {
1726  // If the expression is not a list, it must have been already
1727  // parsed, so just return it as is.
1728  switch(e.getKind()) {
1729  case ID: {
1730  int kind = getEM()->getKind(e[0].getString());
1731  switch(kind) {
1732  case NULL_KIND: return e; // nothing to do
1733  case TRUE_EXPR:
1734  case FALSE_EXPR:
1735  case TYPE:
1736  case BOOLEAN: return getEM()->newLeafExpr(kind);
1737  default:
1738  DebugAssert(false, "Bad use of bare keyword: "+e.toString());
1739  return e;
1740  }
1741  }
1742  case RAW_LIST: break; // break out of switch, do the work
1743  default:
1744  return e;
1745  }
1746  DebugAssert(e.getKind()==RAW_LIST && e.arity() > 0 && e[0].getKind()==ID,
1747  "TheoryCore::parseExprOp:\n e = "+e.toString());
1748  TRACE("parse", "TheoryCore::parseExprOp:\n e = ", e.toString(), "");
1749  /* The first element of the list (e[0] is an ID of the operator.
1750  ID string values are the dirst element of the expression */
1751  const Expr& c1 = e[0][0];
1752  int kind = getEM()->getKind(c1.getString());
1753 
1754  if (isBasicKind(kind)) {
1755  vector<Expr> operatorStack;
1756  vector<Expr> operandStack;
1757  vector<int> childStack;
1758  Expr e2;
1759 
1760  operatorStack.push_back(e);
1761  childStack.push_back(1);
1762 
1763  while (!operatorStack.empty()) {
1764  DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated");
1765 
1766  if (childStack.back() < operatorStack.back().arity()) {
1767 
1768  e2 = operatorStack.back()[childStack.back()++];
1769 
1770  ExprMap<Expr>::iterator iParseCache = d_parseCache->find(e2);
1771  if (iParseCache != d_parseCache->end()) {
1772  operandStack.push_back((*iParseCache).second);
1773  }
1774  else if (e2.getKind() == RAW_LIST &&
1775  e2.arity() > 0 &&
1776  e2[0].getKind() == ID &&
1777  isBasicKind(getEM()->getKind(e2[0][0].getString()))) {
1778  operatorStack.push_back(e2);
1779  childStack.push_back(1);
1780  }
1781  else {
1782  operandStack.push_back(parseExpr(e2));
1783  }
1784  }
1785  else {
1786  e2 = operatorStack.back();
1787  operatorStack.pop_back();
1788  childStack.pop_back();
1789  vector<Expr> children;
1790  vector<Expr>::iterator childStart = operandStack.end() - (e2.arity() - 1);
1791  children.insert(children.begin(), childStart, operandStack.end());
1792  operandStack.erase(childStart, operandStack.end());
1793  kind = getEM()->getKind(e2[0][0].getString());
1794  operandStack.push_back(Expr(kind, children, e2.getEM()));
1795  (*d_parseCache)[e2] = operandStack.back();
1796  if (!getEM()->isTypeKind(operandStack.back().getKind())) {
1797  operandStack.back().getType();
1798  }
1799  }
1800  }
1801  DebugAssert(childStack.empty(), "Invariant violated");
1802  DebugAssert(operandStack.size() == 1, "Expected single operand left");
1803  return operandStack.back();
1804  }
1805 
1806  switch(kind) {
1807  case SUBTYPE:
1808  if (e.arity() <= 3) {
1809  Expr witness;
1810  if (e.arity() == 3) {
1811  witness = parseExpr(e[2]);
1812  }
1813  return newSubtypeExpr(parseExpr(e[1]), witness).getExpr();
1814  }
1815  else {
1816  throw ParserException("Expected one or two arguments to SUBTYPE");
1817  }
1818  case EQ:
1819  if(e.arity()==3) {
1820  Expr e1 = parseExpr(e[1]);
1821  Expr e2 = parseExpr(e[2]);
1822  if (e1.getType() == boolType() &&
1823  getFlags()["convert-eq-iff"].getBool()) {
1824  return e1.iffExpr(e2);
1825  }
1826  else {
1827  return e1.eqExpr(e2);
1828  }
1829  }
1830  else
1831  throw ParserException("Equality requires exactly two arguments: "
1832  +e.toString());
1833  break;
1834 
1835  case NEQ:
1836  if(e.arity()==3)
1837  return !(parseExpr(e[1]).eqExpr(parseExpr(e[2])));
1838  else
1839  throw ParserException("Disequality requires exactly two arguments: "
1840  +e.toString());
1841  break;
1842  case TYPE: {
1843  if(e.arity()==2) {
1844  const Expr& types = e[1];
1845  if(types.getKind() == RAW_LIST) {
1846  vector<Expr> names;
1847  for(Expr::iterator i=types.begin(), iend=types.end(); i!=iend; ++i)
1848  names.push_back(*i);
1849  return Expr(TYPEDECL, names, getEM());
1850  }
1851  }
1852  else if(e.arity() == 3 && e[1].getKind() == ID)
1853  return Expr(TYPEDEF, e[1], parseExpr(e[2]));
1854  throw ParserException("Bad TYPE declaration: "+e.toString());
1855  break;
1856  }
1857  //TODO: Is IF still used?
1858  case IF:
1859  if(e.arity() == 4) {
1860  Expr c(parseExpr(e[1]));
1861  Expr e1(parseExpr(e[2]));
1862  Expr e2(parseExpr(e[3]));
1863  return c.iteExpr(e1, e2);
1864  } else
1865  throw ParserException("Bad IF-THEN-ELSE expression: "
1866  +e.toString());
1867  case COND: {
1868  if(e.arity() >= 3)
1869  return processCond(e, 1);
1870  else
1871  throw ParserException("Bad COND expression: "+e.toString());
1872  break;
1873  }
1874  case LET: { // (LET ((v1 e1) (v2 e2) ... ) body)
1875  Expr e2(e);
1876  while (true) {
1877  if(!(e2.arity() == 3 && e2[1].getKind() == RAW_LIST && e2[1].arity() > 0))
1878  throw ParserException("Bad LET expression: "+e2.toString());
1879 
1880  // Iterate through the bound variables
1881  for(Expr::iterator i=e2[1].begin(), iend=e2[1].end(); i!=iend; ++i) {
1882  const Expr& decl = *i;
1883  if (decl.getKind() != RAW_LIST || decl.arity() != 2)
1884  throw ParserException("Bad variable declaration block in LET "
1885  "expression: "+decl.toString()+
1886  "\n e2 = "+e2.toString());
1887  if (decl[0].getKind() != ID)
1888  throw ParserException("Variable must be an identifier in LET "
1889  "expression: "+decl[0].toString()+
1890  "\n e2 = "+e2.toString());
1891  addBoundVar(decl[0][0].getString(), Type(), parseExpr(decl[1]));
1892  }
1893  // Optimization for nested LETs:
1894  if (e2[2].getKind()==RAW_LIST && e2[2].arity() > 0 &&
1895  e2[2][0].getKind()==ID && getEM()->getKind(e2[2][0][0].getString()) == LET) {
1896  e2 = e2[2];
1897  } else break;
1898  }
1899  // Parse the body recursively and return it (nuke the LET)
1900  return parseExpr(e2[2]);
1901  }
1902  case TRUE_EXPR: { return e.getEM()->trueExpr(); }
1903  case FALSE_EXPR: { return e.getEM()->falseExpr();}
1904  case BOOLEAN: { return e.getEM()->boolExpr(); }
1905  break;
1906  default:
1907  DebugAssert(false,
1908  "TheoryCore::parseExprOp: invalid command or expression: "
1909  + e.toString());
1910  break;
1911  }
1912  return e;
1913 }
1914 
1916  DebugAssert(os.lang() == SMTLIB_LANG || os.lang() == SMTLIB_V2_LANG,
1917  "Invalid state in printSmtLibShared" );
1918  switch(e.getKind()) {
1919  case TRUE_EXPR: os << "true"; break;
1920  case FALSE_EXPR: os << "false"; break;
1921  case UCONST: os << d_translator->escapeSymbol(d_translator->fixConstName(e.getName())); break;
1922  case BOOLEAN: e.printAST(os); break;
1923  case STRING_EXPR: e.print(os); break;
1924  case SUBTYPE:
1925  throw SmtlibException("TheoryCore::print: SMTLIB: SUBTYPE not implemented");
1926  break;
1927  case TYPEDEF: {
1928  throw SmtlibException("TheoryCore::print: SMTLIB: TYPEDEF not implemented");
1929  break;
1930  }
1931  case EQ:
1932  os << "(" << push << "=" << space << e[0]
1933  << space << e[1] << push << ")";
1934  break;
1935  case DISTINCT: {
1936  int i=0, iend=e.arity();
1937  os << "(" << push << "distinct";
1938  for(; i!=iend; ++i) os << space << e[i];
1939  os << push << ")";
1940  break;
1941  }
1942  case NOT:
1943  os << "(" << push << "not" << space << e[0] << push << ")";
1944  break;
1945  case AND: {
1946  int i=0, iend=e.arity();
1947  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
1948  os << e[0];
1949  } else {
1950  os << "(" << push << "and";
1951  for(; i!=iend; ++i) os << space << e[i];
1952  os << push << ")";
1953  }
1954  break;
1955  }
1956  case OR: {
1957  int i=0, iend=e.arity();
1958  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
1959  os << e[0];
1960  } else {
1961  os << "(" << push << "or";
1962  for(; i!=iend; ++i) os << space << e[i];
1963  os << push << ")";
1964  }
1965  break;
1966  }
1967  case XOR: {
1968  int i=0, iend=e.arity();
1969  if(iend == 1 && os.lang() == SMTLIB_V2_LANG) {
1970  os << e[0];
1971  } else {
1972  os << "(" << push << "xor";
1973  for(; i!=iend; ++i) os << space << e[i];
1974  os << push << ")";
1975  }
1976  break;
1977  }
1978 
1979  case TRANSFORM:
1980  throw SmtlibException("TheoryCore::print: SMTLIB: TRANSFORM not implemented");
1981  os << "(" << push << "TRANSFORM" << space << e[0] << push << ")";
1982  break;
1983 
1984  case LETDECL:
1985  // throw SmtlibException("TheoryCore::print: SMTLIB: LETDECL not implemented");
1986  if(e.arity() == 2) os << e[1];
1987  else e.printAST(os);
1988  break;
1989 
1990 
1991  case PF_APPLY: {
1992  DebugAssert(e.arity() > 0, "TheoryCore::print(): "
1993  "Proof rule application must have at "
1994  "least one argument (rule name):\n "+e.toString());
1995  // os << e[0]; by yeting
1996  os << e[0] << "\n" ;
1997  if(e.arity() > 1) { // Print the arguments
1998  os << push << "(" << push;
1999  bool first(true);
2000  for(int i=1; i<e.arity(); i++) {
2001  if(first) first=false;
2002  else os << push << "," << pop << space;
2003  // os << e[i]; by yeting
2004  os << e[i] << "\n";
2005  }
2006  os << push << ")";
2007  }
2008  break;
2009  }
2010  case RAW_LIST: {
2011  os << "(" << push;
2012  bool firstTime(true);
2013  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2014  if(firstTime) firstTime = false;
2015  else os << space;
2016  os << *i;
2017  }
2018  os << push << ")";
2019  break;
2020  }
2021  case ANY_TYPE:
2022  os << "ANY_TYPE";
2023  break;
2024 
2025  case PF_HOLE: // FIXME: implement this (now fall through to default)
2026  default:
2027  throw SmtlibException("TheoryCore::print: SMTLIB_LANG: Unexpected expression: "
2028  +getEM()->getKindName(e.getKind()));
2029  }
2030  return os;
2031 }
2032 
2033 static bool containsRec(const Expr& def, ExprHashMap<bool>& defs, ExprHashMap<bool>& visited) {
2034  ExprHashMap<bool>::iterator it = visited.find(def);
2035  if (it != visited.end()) return false;
2036  it = defs.find(def);
2037  if (it != defs.end()) return true;
2038  for(Expr::iterator i = def.begin(), iend=def.end(); i != iend; ++i) {
2039  if (containsRec(*i,defs,visited)) return true;
2040  }
2041  // [MGD] Closure exprs (LAMBDAs and quantifiers) don't have children,
2042  // they have bodies.
2043  if(def.isClosure()) {
2044  if (containsRec(def.getBody(),defs,visited)) return true;
2045  }
2046  visited[def] = true;
2047  return false;
2048 }
2049 
2050 static bool contains(const Expr& def, ExprHashMap<bool>& defs) {
2051  ExprHashMap<bool> visited;
2052  return containsRec(def, defs, visited);
2053 }
2054 
2056 {
2057  switch(os.lang()) {
2058  case SPASS_LANG:
2059  switch(e.getKind()) {
2060  case TRUE_EXPR: os << "true"; break;
2061  case FALSE_EXPR: os << "false"; break;
2062  case UCONST:
2063  if(isReal(getBaseType(e.getType()))) {
2064  // SPASS guys want "np" prefix on arith vars
2065  os << "np";
2066  }
2067  os << e.getName();
2068  break;
2069  case BOOLEAN: e.printAST(os); break;
2070  case STRING_EXPR: e.print(os); break;
2071  case TYPE:
2072  throw SmtlibException("TheoryCore::print: SPASS_LANG: TYPE should have been handled by Translator::finish()");
2073  case ID:
2074  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
2075  else e.printAST(os);
2076  break;
2077  case CONST:
2078  throw SmtlibException("TheoryCore::print: SPASS_LANG: CONST should have been handled by Translator::finish()");
2079  case SUBTYPE:
2080  throw SmtlibException("TheoryCore::print: SPASS_LANG: SUBTYPE not implemented");
2081  break;
2082  case TYPEDEF: {
2083  throw SmtlibException("TheoryCore::print: SPASS_LANG: TYPEDEF not implemented");
2084  break;
2085  }
2086  case EQ:
2087  os << push << "equal(" << e[0]
2088  << "," << space << e[1] << push << ")";
2089  break;
2090  case DISTINCT: {
2091  throw SmtlibException("TheoryCore::print: SPASS_LANG: SUBTYPE not implemented");
2092  break;
2093  }
2094  case NOT:
2095  os << push << "not(" << e[0] << push << ")";
2096  break;
2097  case AND: {
2098  int i=0, iend=e.arity();
2099  os << push << "and(" << e[i];
2100  while(++i != iend) os << "," << space << e[i];
2101  os << push << ")";
2102  break;
2103  }
2104  case OR: {
2105  int i=0, iend=e.arity();
2106  os << push << "or(" << e[i];
2107  while(++i != iend) os << "," << space << e[i];
2108  os << push << ")";
2109  break;
2110  }
2111  case XOR: {
2112  if(e.arity() != 2) {
2113  throw SmtlibException("TheoryCore::print: SPASS_LANG: XOR not supported when arity != 2 !");
2114  }
2115  os << push << "or(and(" << e[0] << "," << space << "not(" << e[1] << ")),"
2116  << space << "and(not(" << e[0] << ")," << space << e[1] << ")"
2117  << push << ")";
2118  break;
2119  }
2120  case ITE:
2121  if (e.getType().isBool()) {
2122  os << push << "and(" << space
2123  << push << "implies(" << space
2124  << e[0] << "," << space << e[1]
2125  << push << ")" << "," << space
2126  << push << "implies(" << space
2127  << e[0].negate() << "," << space << e[2]
2128  << push << ")"
2129  << push << ")";
2130  } else {
2131  os << push << "if_then_else("
2132  << e[0] << "," << space
2133  << e[1] << "," << space
2134  << e[2] << push << ")";
2135  }
2136  break;
2137  case IFF:
2138  os << push << "equiv(" << space
2139  << e[0] << space << "," << space << e[1] << push << ")";
2140  break;
2141  case IMPLIES:
2142  os << push << "implies(" << space
2143  << e[0] << space << "," << space << e[1] << push << ")";
2144  break;
2145  case ASSERT:
2146  // SPASS guys don't want formula(false) etc: comment them out
2147  if(e[0] == d_em->trueExpr() ||
2148  e[0] == d_em->falseExpr().notExpr()) {
2149  os << "% ";
2150  }
2151  os << "formula(" << space << push << e[0].negate() << space << ").";
2152  break;
2153  case TRANSFORM:
2154  throw SmtlibException("TheoryCore::print: SPASS: TRANSFORM not implemented");
2155  break;
2156  case QUERY:
2157  // SPASS guys don't want formula(false) etc: comment them out
2158  if(e[0].negate() == d_em->trueExpr() ||
2159  e[0].negate() == d_em->falseExpr().notExpr()) {
2160  os << "% ";
2161  }
2162  os << "formula(" << space << push << e[0] << space << ").";
2163  break;
2164  case LETDECL:
2165  throw SmtlibException("TheoryCore::print: SPASS_LANG: LETDECL not implemented");
2166  case LET:
2167  throw SmtlibException("TheoryCore::print: SPASS_LANG: LET should have been handled in Translator::finish()");
2168  case BOUND_VAR:
2169  if(isReal(getBaseType(e.getType()))) {
2170  // SPASS guys want "np" prefix on arith vars
2171  os << "np";
2172  }
2173  os << e.getName();
2174  break;
2175  case SKOLEM_VAR:
2176  os << push << "SKOLEM_" + int2string((int)e.getIndex());
2177  break;
2178  case PF_APPLY:
2179  throw SmtlibException("TheoryCore::print: SPASS_LANG: PF_APPLY not implemented");
2180  case ANNOTATION:
2181  throw SmtlibException("TheoryCore::print: SPASS_LANG: ANNOTATION should have been handled by Translator::finish()");
2182 
2183  case RAW_LIST:
2184  case ANY_TYPE:
2185  case WHERE:
2186  case ASSERTIONS:
2187  case ASSUMPTIONS:
2188  case COUNTEREXAMPLE:
2189  case COUNTERMODEL:
2190  case PUSH:
2191  case POP:
2192  case POPTO:
2193  case PUSH_SCOPE:
2194  case POP_SCOPE:
2195  case POPTO_SCOPE:
2196  case RESET:
2197  case PF_HOLE:
2198  default:
2199  throw SmtlibException("TheoryCore::print: SPASS_LANG: Unexpected expression: "
2200  +getEM()->getKindName(e.getKind()));
2201  }
2202  break; // end of case SPASS_LANG
2203 
2204  case SIMPLIFY_LANG:
2205  switch(e.getKind()) {
2206  case TRUE_EXPR: os << "TRUE"; break;
2207  case FALSE_EXPR: os << "FALSE"; break;
2208  case TYPE:
2209  break; // no type for Simplify
2210  case ID:
2211  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
2212  else e.print(os);
2213  break;
2214  case CONST:
2215  // os << "ERROR:const to be supported\n"; simplify do not need this
2216  break;
2217  case SUBTYPE:
2218  break;
2219  case TYPEDEF: {
2220  break;
2221  }
2222  case EQ:
2223  os << "(EQ " << e[0] << " " << e[1] << ")";
2224  break;
2225  case NOT: os << "(NOT " << e[0] << ")"; break;
2226  case AND: {
2227  int i=0, iend=e.arity();
2228  os << "(AND ";
2229  if(i!=iend) { os << e[i]; ++i; }
2230  for(; i!=iend; ++i) os << " " << e[i];
2231  os << ")";
2232  }
2233  break;
2234  case OR: {
2235  int i=0, iend=e.arity();
2236  os << "(OR ";
2237  if(i!=iend) { os << e[i]; ++i; }
2238  for(; i!=iend; ++i) os << " " << e[i];
2239  os << ")";
2240  }
2241  break;
2242  case ITE:
2243  os<<"ERROR:ITE:not supported yet\n";
2244  break;
2245  case IFF:
2246  if(e.arity() == 2)
2247  os << "(IFF " << e[0] << " " << e[1] << ")";
2248  else
2249  e.print(os);
2250  break;
2251  case IMPLIES:
2252  os << "(IMPLIES " <<e[0] << " " << e[1] << ")";
2253  break;
2254  // Commands
2255  case ASSERT:
2256  os << "(BG_PUSH " << e[0] << ")\n";
2257  break;
2258  case TRANSFORM:
2259  os << "ERROR:TRANSFORM:not supported in Simplify " << push << e[0] << push << "\n";
2260  break;
2261  case QUERY:
2262  os << e[0] <<"\n";
2263  break;
2264  case WHERE:
2265  os << "ERROR:WHERE:not supported in Simplify\n";
2266  break;
2267  case ASSERTIONS:
2268  os << "ERROR:ASSERTIONS:not supported in Simplify\n";
2269  break;
2270  case ASSUMPTIONS:
2271  os << "ERROR:ASSUMPTIONS:not supported in Simplify\n";
2272  break;
2273  case COUNTEREXAMPLE:
2274  os << "ERROR:COUNTEREXAMPLE:not supported in Simplify\n";
2275  break;
2276  case COUNTERMODEL:
2277  os << "ERROR:COUNTERMODEL:not supported in Simplify\n";
2278  break;
2279  case PUSH:
2280  case POP:
2281  case POPTO:
2282  case PUSH_SCOPE:
2283  case POP_SCOPE:
2284  case POPTO_SCOPE:
2285  case RESET:
2286  os << "ERROR:PUSH and POP:not supported in Simplify\n";
2287  break;
2288  // case CONSTDEF:
2289  case LETDECL:
2290  os << "LETDECL not supported in Simplify\n";
2291  break;
2292  case LET: {
2293  // (LET (LETDECLS (LETDECL var [ type ] val) .... ) body)
2294  /* bool first(true);
2295  os << "(" << push << "LET" << space << push;
2296  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2297  if(!first) os << push << "," << pop << endl;
2298  else first = false;
2299  if(i->arity() == 3) {
2300  os << (*i)[0] << ":" << space << push << (*i)[1]
2301  << space << "= " << push << nodag << (*i)[2] << pop << pop;
2302  } else {
2303  os << (*i)[0];
2304  Type tp((*i)[0].lookupType());
2305  if(!tp.isNull()) os << ":" << space << push << tp.getExpr();
2306  else os << push;
2307  os << space << "= " << push << nodag << (*i)[1] << pop << pop;
2308  }
2309  }
2310  os << pop << endl << "IN" << space << push << e[1] << push << ")";
2311  */
2312  os << "LET not supported in Simplify\n";
2313  break;
2314 
2315  }
2316  case BOUND_VAR:
2317  // os << e.getName()+"_"+e.getUid(); // by yeting for a neat output
2318  os << e.getName();
2319  break;
2320  case SKOLEM_VAR:
2321  os << "SKOLEM_" + int2string((int)e.getIndex());
2322  break;
2323  case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory
2324  /* DebugAssert(e.arity() > 0, "TheoryCore::print(): "
2325  "Proof rule application must have at "
2326  "least one argument (rule name):\n "+e.toString());
2327  os << e[0];
2328  if(e.arity() > 1) { // Print the arguments
2329  os << push << "(" << push;
2330  bool first(true);
2331  for(int i=1; i<e.arity(); i++) {
2332  if(first) first=false;
2333  else os << push << "," << pop << space;
2334  os << e[i];
2335  }
2336  os << push << ")";
2337  }*/
2338 
2339  os << "PR_APPLY not supported in Simplify\n";
2340  break;
2341  case RAW_LIST: {
2342  /* os << "[" << push;
2343  bool firstTime(true);
2344  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2345  if(firstTime) firstTime = false;
2346  else os << push << "," << pop << space;
2347  os << *i;
2348  }
2349  os << push << "]";*/
2350  os << "RAW_LIST not supported in Simplify\n";
2351  break;
2352  }
2353  case PF_HOLE: // FIXME: implement this (now fall through to default)
2354  default:
2355  // Print the top node in the default LISP format, continue with
2356  // pretty-printing for children.
2357  e.print(os);
2358  }
2359  break; // end of case simplify_LANG
2360 
2361  case TPTP_LANG: {
2362  static int axiom_counter =0;
2363  switch(e.getKind()) {
2364  case TRUE_EXPR: os << "$true"; break;
2365  case FALSE_EXPR: os << "$false"; break;
2366  case TYPE:
2367  break;
2368  if(e.arity() == 0) os << "TYPE";
2369  else if(e.arity() == 1) {
2370  for (int i=0; i < e[0].arity(); ++i) {
2371  if (i != 0) os << endl;
2372  os << e[0][i] << ": TYPE;";
2373  }
2374  }
2375  else if(e.arity() == 2)
2376  os << e[0] << ":" << push << " TYPE = " << e[1] << push << ";";
2377  else e.printAST(os);
2378  break;
2379  case ID:
2380  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
2381  else e.print(os);
2382  break;
2383  case CONST:
2384  if(e.arity() == 2) {
2385  string ename = to_lower(e[0].toString());
2386  os << "tff(" << ename << "_type, type,\n " << ename;
2387  os << ": " << e[1] << "). \n";
2388  }
2389  else {
2390  os << "ERROR: CONST's arity > 2";
2391  }
2392  break;
2393 
2394  case SUBTYPE:
2395  break;
2396  case TYPEDEF: {
2397  break;
2398  }
2399  case EQ:
2400  os << e[0] << " = " << e[1];
2401  break;
2402 
2403  case DISTINCT: {
2404  int i=0, iend=e.arity();
2405  os << "$distinct(" ;
2406  os << e[i] ;
2407  i++;
2408  for(; i!=iend; ++i) os << ", " << e[i] ;
2409  os << ")";
2410  break;
2411  }
2412 
2413  case NOT:
2414  os << "~(" << e[0]<<")" ;
2415  break;
2416 
2417  case AND: {
2418  int i=0, iend=e.arity();
2419  if(iend == 1) {
2420  os << e[i];
2421  }
2422 
2423  else if(iend > 1) {
2424  for(i=0 ; i < iend-1; i++) {
2425  os << "(" << e[i] << " \n& " ;
2426  }
2427  os << e[iend-1];
2428  for(i=0 ; i < iend-1; i++) {
2429  os << ")";
2430  }
2431  }
2432  else{
2433  os <<"ERROR:AND has less than 1 parameter\n";
2434  }
2435  break;
2436  }
2437  case OR: {
2438  int i=0, iend=e.arity();
2439  if(iend == 1) {
2440  os << e[i];
2441  }
2442 
2443  else if(iend > 1) {
2444  for(i=0 ; i < iend-1; i++) {
2445  os << "(" << e[i] << " \n| " ;
2446  }
2447  os << e[iend-1];
2448  for(i=0 ; i < iend-1; i++) {
2449  os << ")";
2450  }
2451  }
2452  else{
2453  os <<"ERROR:OR has less than 1 parameter\n";
2454  }
2455  break;
2456  }
2457  case ITE:
2458  os<<"ERROR:ITE:not supported in TPTP yet\n";
2459  /* os << "(AND (IMPLIES "<< e[0] << " " << e[1]<<")"
2460  << "(IMPLIES (NOT " <<e[0] << ")" << e[2] <<"))";
2461  */
2462  break;
2463  case IFF:
2464  if(e.arity() == 2)
2465  os << "(" << e[0] << " \n<=> " << e[1] << ")" ;
2466  else
2467  e.print(os);
2468  break;
2469  case IMPLIES:
2470  os << "(" << e[0] << " \n=> " << e[1] << ")" ;
2471  break;
2472  // Commands
2473  case ASSERT:
2474  os << "tff(" << axiom_counter++ << ", axiom, \n " <<e[0] << ").\n";
2475 
2476  break;
2477  case TRANSFORM:
2478  os << "ERROR:TRANSFORM:not supported in TPTP " << push << e[0] << push << "\n";
2479  break;
2480  case QUERY:
2481  if(getFlags()["negate-query"].getBool() == true){
2482  if (e[0].isNot()){
2483  os << "tff(" << axiom_counter++ << ", conjecture, \n " <<e[0][0] << ").\n";
2484  }
2485  else{
2486  os << "tff(" << axiom_counter++ << ", conjecture, \n ~(" << e[0] << ")).\n";
2487  }
2488  }
2489  else{
2490  os << "tff(" << axiom_counter++ << ", conjecture, \n " <<e[0] << ").\n";
2491  }
2492  break;
2493  case WHERE:
2494  os << "ERROR:WHERE:not supported in TPTP\n";
2495  break;
2496  case ASSERTIONS:
2497  os << "ERROR:ASSERTIONS:not supported in TPTP\n";
2498  break;
2499  case ASSUMPTIONS:
2500  os << "ERROR:ASSUMPTIONS:not supported in TPTP\n";
2501  break;
2502  case COUNTEREXAMPLE:
2503  os << "ERROR:COUNTEREXAMPLE:not supported in TPTP\n";
2504  break;
2505  case COUNTERMODEL:
2506  os << "ERROR:COUNTERMODEL:not supported in TPTP\n";
2507  break;
2508  case PUSH:
2509  case POP:
2510  case POPTO:
2511  case PUSH_SCOPE:
2512  case POP_SCOPE:
2513  case POPTO_SCOPE:
2514  case RESET:
2515  os << "ERROR:PUSH and POP:not supported in TPTP\n";
2516  break;
2517  // case CONSTDEF:
2518  case LETDECL:
2519  os << "LETDECL not supported in Simplify\n";
2520  break;
2521  case LET: {
2522  bool first(true);
2523  os << " := [" ;
2524  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2525  if(!first) os << " , " ;
2526  else first = false;
2527  if(i->arity() == 3) {
2528  os << (*i)[0] << ":" << (*i)[1]
2529  << " ERROR= " << nodag << (*i)[2] ;
2530  } else {
2531  os << (*i)[0];
2532  os << " := " << nodag << (*i)[1] ;
2533  }
2534  os <<endl;
2535  }
2536  os << "] : " << endl << "(" << e[1] << ")";
2537  break;
2538 
2539  }
2540 
2541  case BOUND_VAR:{
2542  // os << e.getName()+"_"+e.getUid() ; // by yeting
2543  os<< to_upper(e.getName());
2544  break;
2545  }
2546  case SKOLEM_VAR:
2547  os << "SKOLEM_VAR is not supported in TPTP\n";
2548  break;
2549 
2550  case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory
2551  /* DebugAssert(e.arity() > 0, "TheoryCore::print(): "
2552  "Proof rule application must have at "
2553  "least one argument (rule name):\n "+e.toString());
2554  os << e[0];
2555  if(e.arity() > 1) { // Print the arguments
2556  os << push << "(" << push;
2557  bool first(true);
2558  for(int i=1; i<e.arity(); i++) {
2559  if(first) first=false;
2560  else os << push << "," << pop << space;
2561  os << e[i];
2562  }
2563  os << push << ")";
2564  }*/
2565 
2566  os << "PR_APPLY not supported in TPTP\n";
2567  break;
2568  case RAW_LIST: {
2569  /* os << "[" << push;
2570  bool firstTime(true);
2571  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2572  if(firstTime) firstTime = false;
2573  else os << push << "," << pop << space;
2574  os << *i;
2575  }
2576  os << push << "]";*/
2577  os << "RAW_LIST not supported in TPTP\n";
2578  break;
2579  }
2580  case PF_HOLE:
2581  os << "PF_HOLE not supported in TPTP\n";
2582  break;
2583  case UCONST:
2584  {string name = e.getName();
2585  if(name.length() >= 5){
2586  if ('C' == name[0] && 'V' == name[1] && 'C' == name[2] && '_' == name[3] && isdigit(name[4])){
2587  os << to_upper(name);
2588  }
2589  else {
2590  os << to_lower(name);
2591  }
2592  }
2593  else {
2594  os<<to_lower(name);
2595  }
2596  //
2597  // e.print(os); break;
2598  break;
2599  }
2600  case STRING_EXPR:
2601  os <<"ERROR:STRING_EXPR is not suppoerted in TPTP\n";
2602  e.print(os); break;
2603  case BOOLEAN:
2604  os << "$o";
2605  break;
2606  default:
2607  // Print the top node in the default LISP format, continue with
2608  // pretty-printing for children.
2609  os<<"unknown ";
2610  // cout<<e.toString(PRESENTATION_LANG)<<endl;
2611  // cout<<getEM()->getKindName(e.getKind())<<endl;
2612  e.print(os);
2613  }
2614  break; // end of case TPTP_LANG
2615  }
2616 
2617 
2618  case PRESENTATION_LANG:
2619  switch(e.getKind()) {
2620  case TRUE_EXPR:
2621  os << "TRUE";
2622  break;
2623  case FALSE_EXPR:
2624  os << "FALSE";
2625  break;
2626  case BOOLEAN:
2627  os << "BOOLEAN";
2628  break;
2629  case UCONST:
2630  case STRING_EXPR:
2631  e.print(os); break;
2632  case TYPE:
2633  if(e.arity() == 0) os << "TYPE";
2634  else if(e.arity() == 1) {
2635  for (int i=0; i < e[0].arity(); ++i) {
2636  if (i != 0) os << endl;
2637  os << e[0][i] << ": TYPE;";
2638  }
2639  }
2640  else if(e.arity() == 2)
2641  os << e[0] << ":" << push << " TYPE = " << e[1] << push << ";";
2642  else e.printAST(os);
2643  break;
2644  case ID:
2645  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
2646  else e.printAST(os);
2647  break;
2648  case CONST:
2649  if(e.arity() == 2) {
2650  if(e[0].getKind() == RAW_LIST) {
2651  bool first(true);
2652  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2653  if(first) first = false;
2654  else os << push << "," << pop << space;
2655  os << (*i);
2656  }
2657  }
2658  else
2659  os << e[0];
2660  os << ":" << push << space << e[1] << push << ";";
2661  } else if(e.arity() == 3)
2662  os << e[0] << ":" << push << space << e[1]
2663  << space << "=" << space << push << e[2] << push << ";";
2664  else
2665  e.printAST(os);
2666  break;
2667  case SUBTYPE:
2668  os << "SUBTYPE(" << push << e[0] << push << ")";
2669  break;
2670  case TYPEDEF: {
2671  // This is used when dumping declarations to file. Print just
2672  // the name of the type, unless it's a messed-up expression.
2673  if(e.arity() != 2) e.printAST(os);
2674  else if(e[0].isString()) os << e[0].getString();
2675  else e[0].print(os);
2676  break;
2677  }
2678  case EQ:
2679  // When a separator starts with a space (like " = "), add the
2680  // leading space with 'space' modifier. If this separator goes
2681  // to the next line, the leading spaces must be eaten up to get
2682  // the indentation right; 'space' will tell the indentation
2683  // engine that it is a space that can be eaten. A space in a
2684  // string (like " ") will never be eaten.
2685  os << "(" << push << e[0] << space << "= " << e[1] << push << ")";
2686  break;
2687  case DISTINCT: {
2688  os << "DISTINCT(" << push;
2689  bool first(true);
2690  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2691  if (!first) os << push << "," << pop << space;
2692  else first = false;
2693  os << (*i);
2694  }
2695  os << push << ")";
2696  }
2697  break;
2698  case NOT: os << "NOT " << e[0]; break;
2699  case AND: {
2700  int i=0, iend=e.arity();
2701  os << "(" << push;
2702  if(i!=iend) { os << e[i]; ++i; }
2703  for(; i!=iend; ++i) os << space << "AND " << e[i];
2704  os << push << ")";
2705  }
2706  break;
2707  case OR: {
2708  int i=0, iend=e.arity();
2709  os << "(" << push;
2710  if(i!=iend) { os << e[i]; ++i; }
2711  for(; i!=iend; ++i) os << space << "OR " << e[i];
2712  os << push << ")";
2713  }
2714  break;
2715  case XOR: {
2716  int i=0, iend=e.arity();
2717  os << "(" << push;
2718  if(i!=iend) { os << e[i]; ++i; }
2719  for(; i!=iend; ++i) os << space << "XOR " << e[i];
2720  os << push << ")";
2721  }
2722  break;
2723  case ITE:
2724  os << push << "IF " << push << e[0] << popSave
2725  << space << "THEN " << pushRestore << e[1] << popSave
2726  << space << "ELSE " << pushRestore << e[2] << pop
2727  << space << "ENDIF";
2728  break;
2729  case IFF:
2730  if(e.arity() == 2)
2731  os << "(" << push << e[0] << space << "<=> " << e[1] << push << ")";
2732  else
2733  e.printAST(os);
2734  break;
2735  case IMPLIES:
2736  os << "(" << push << e[0] << space << "=> " << e[1] << push << ")";
2737  break;
2738  // Commands
2739  case ASSERT:
2740  os << "ASSERT " << push << e[0] << push << ";";
2741  break;
2742  case TRANSFORM:
2743  os << "TRANSFORM " << push << e[0] << push << ";";
2744  break;
2745  case QUERY:
2746  os << "QUERY " << push << e[0] << push << ";";
2747  break;
2748  case WHERE:
2749  os << "WHERE;";
2750  break;
2751  case ASSERTIONS:
2752  os << "ASSERTIONS;";
2753  break;
2754  case ASSUMPTIONS:
2755  os << "ASSUMPTIONS;";
2756  break;
2757  case COUNTEREXAMPLE:
2758  os << "COUNTEREXAMPLE;";
2759  break;
2760  case COUNTERMODEL:
2761  os << "COUNTERMODEL;";
2762  break;
2763  case PUSH:
2764  if(e.arity()==0)
2765  os << "PUSH;";
2766  else
2767  os << "PUSH" << space << e[0] << push << ";";
2768  break;
2769  case POP:
2770  if(e.arity()==0)
2771  os << "POP;";
2772  else
2773  os << "POP" << space << e[0] << push << ";";
2774  break;
2775  case POPTO:
2776  os << "POPTO" << space << e[0] << push << ";"; break;
2777  case PUSH_SCOPE:
2778  if(e.arity()==0)
2779  os << "PUSH_SCOPE;";
2780  else
2781  os << "PUSH_SCOPE" << space << e[0] << push << ";";
2782  break;
2783  case POP_SCOPE:
2784  if(e.arity()==0)
2785  os << "POP_SCOPE;";
2786  else
2787  os << "POP_SCOPE" << space << e[0] << push << ";";
2788  break;
2789  case POPTO_SCOPE:
2790  os << "POPTO_SCOPE" << space << e[0] << push << ";"; break;
2791  case RESET:
2792  os << "RESET;";
2793  break;
2794  case LETDECL:
2795  if(e.arity() == 2) os << e[1];
2796  else e.printAST(os);
2797  break;
2798  case LET: {
2799  // (LET (LETDECLS (LETDECL var [ type ] val) .... ) body)
2800  bool first(true);
2801  os << "(" << push << "LET" << space << push;
2802  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2803  if(!first) os << push << "," << pop << endl;
2804  else first = false;
2805  if(i->arity() == 3) {
2806  os << (*i)[0] << ":" << space << push << (*i)[1]
2807  << space << "= " << push << nodag << (*i)[2] << pop << pop;
2808  } else {
2809  os << (*i)[0];
2810  Type tp((*i)[0].lookupType());
2811  if(!tp.isNull()) os << ":" << space << push << tp.getExpr();
2812  else os << push;
2813  os << space << "= " << push << nodag << (*i)[1] << pop << pop;
2814  }
2815  }
2816  os << pop << endl << "IN" << space << push << e[1] << push << ")";
2817  break;
2818  }
2819  case BOUND_VAR:
2820  // os << e.getName()+"_"+e.getUid();
2821 
2822  //by yeting, as requested by Sascha Boehme for proofs
2823  if(getFlags()["print-var-type"].getBool()) {
2824  os << e.getName() << "(" << e.getType() << ")";
2825  }
2826  else {
2827  os << e.getName(); //for better support of proof translation yeting
2828  }
2829  break;
2830  case SKOLEM_VAR:
2831  os << "SKOLEM_" + int2string((int)e.getIndex());
2832  break;
2833  case PF_APPLY: // FIXME: this will eventually go to the "symsim" theory
2834  DebugAssert(e.arity() > 0, "TheoryCore::print(): "
2835  "Proof rule application must have at "
2836  "least one argument (rule name):\n "+e.toString());
2837  // os << e[0]; by yeting
2838  os << e[0] << "\n" ;
2839  if(e.arity() > 1) { // Print the arguments
2840  os << push << "(" << push;
2841  bool first(true);
2842  for(int i=1; i<e.arity(); i++) {
2843  if(first) first=false;
2844  else os << push << "," << pop << space;
2845  // os << e[i]; by yeting
2846  os << e[i] << "\n";
2847  }
2848  os << push << ")";
2849  }
2850  break;
2851  case RAW_LIST: {
2852  os << "[" << push;
2853  bool firstTime(true);
2854  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2855  if(firstTime) firstTime = false;
2856  else os << push << "," << pop << space;
2857  os << *i;
2858  }
2859  os << push << "]";
2860  break;
2861  }
2862  case ANY_TYPE:
2863  os << "ANY_TYPE";
2864  break;
2865  case ARITH_VAR_ORDER: {
2866  os << "ARITH_VAR_ORDER(" << push;
2867  bool firstTime(true);
2868  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
2869  if(firstTime) firstTime = false;
2870  else os << push << "," << pop << space;
2871  os << *i;
2872  }
2873  os << push << ");";
2874  break;
2875  }
2876  case ANNOTATION: {
2877  os << "%% ";
2878  os << e[0];
2879  if (e.arity() > 1) {
2880  os << ": " << e[1];
2881  }
2882  }
2883  case PF_HOLE: // FIXME: implement this (now fall through to default)
2884  default:
2885  // Print the top node in the default LISP format, continue with
2886  // pretty-printing for children.
2887  e.printAST(os);
2888  }
2889  break; // end of case PRESENTATION_LANG
2890 
2891  /* There's a lot of overlap between SMT-LIB v1 and v2, so we'll only handle
2892  * v1-specific stuff here, then goto (!) then end of the v2 block below.
2893  */
2894  case SMTLIB_LANG:
2895  switch(e.getKind()) {
2896  case TYPE:
2897  if (e.arity() == 1) {
2898  os << " :extrasorts (";
2899  for (int i=0; i < e[0].arity(); ++i) {
2900  if (i != 0) os << push << space;
2901  os << push << e[0][i];
2902  }
2903  os << push << ")";
2904  }
2905  else if (e.arity() == 2) {
2906  break;
2907  }
2908  else {
2909  throw SmtlibException("TheoryCore::print: SMTLIB: Unexpected TYPE expression");
2910  }
2911  break;
2912 
2913  case CONST:
2914  if(e.arity() == 2) {
2915  if (e[1].getKind() == BOOLEAN) {
2916  os << " :extrapreds ((" << push << d_translator->fixConstName(e[0][0].getString())
2917  << push << "))";
2918  }
2919  else if (e[1].getKind() == ARROW && e[1][e[1].arity()-1].getKind() == BOOLEAN) {
2920  os << " :extrapreds ((" << push << d_translator->fixConstName(e[0][0].getString())
2921  << space << nodag << e[1] << push << "))";
2922  }
2923  else {
2924  os << " :extrafuns ((" << push << d_translator->fixConstName(e[0][0].getString())
2925  << space << nodag << e[1] << push << "))";
2926  }
2927  }
2928  else if (e.arity() == 0) e.printAST(os);
2929  else {
2930  throw SmtlibException("TheoryCore::print: SMTLIB: CONST not implemented");
2931  }
2932  break;
2933 
2934  case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs
2935  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
2936  else e.printAST(os);
2937  break;
2938 
2939  case IMPLIES:
2940  os << "(" << push << "implies" << space
2941  << e[0] << space << e[1] << push << ")";
2942  break;
2943 
2944  case IFF:
2945  os << "(" << push << "iff" << space
2946  << e[0] << space << e[1] << push << ")";
2947  break;
2948 
2949  case ITE:
2950  os << "(" << push;
2951  if (e.getType().isBool()) os << "if_then_else";
2952  else os << "ite";
2953  os << space << e[0]
2954  << space << e[1] << space << e[2] << push << ")";
2955  break;
2956 
2957  // Commands
2958  case ASSERT:
2959  os << " :assumption" << space << push << e[0];
2960  break;
2961 
2962  case QUERY:
2963  os << " :formula" << space << push << e[0].negate();
2964  break;
2965 
2966  case LET: {
2967  // (LET ((var [ type ] val) .... ) body)
2968  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2969  os << "(" << push;
2970  Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType());
2971  DebugAssert(!tp.isNull(), "Unexpected Null type");
2972  if (tp.getExpr().getKind() == BOOLEAN) {
2973  os << "flet" << space << "(" << push;
2974  }
2975  else {
2976  os << "let" << space << "(" << push;
2977  }
2978  if(i->arity() == 3) {
2979  os << (*i)[0] << space << nodag << (*i)[2];
2980  } else {
2981  os << (*i)[0] << space << nodag << (*i)[1];
2982  }
2983  os << push << ")" << pop << pop << space;
2984  }
2985  os << e[1] << push;
2986  for (int j = 0; j < e[0].arity(); ++j)
2987  os << ")";
2988  break;
2989  }
2990 
2991  case BOUND_VAR: {
2992  // os << push << "?" << e.getName()+"_"+e.getUid();
2993  string str = e.getName();
2994  if (str[0] == '_') str[0] = '?';
2995  os << push << str;
2996  break;
2997  }
2998  case SKOLEM_VAR:
2999  os << push << "SKOLEM_" + int2string((int)e.getIndex());
3000  break;
3001 
3002  case WHERE:
3003  os << " :cvc_command \"WHERE\"";
3004  break;
3005  case ASSERTIONS:
3006  os << " :cvc_command \"ASSERTIONS\"";
3007  break;
3008  case ASSUMPTIONS:
3009  os << " :cvc_command \"ASSUMPTIONS\"";
3010  break;
3011  case COUNTEREXAMPLE:
3012  os << " :cvc_command \"COUNTEREXAMPLE\"";
3013  break;
3014  case COUNTERMODEL:
3015  os << " :cvc_command \"COUNTERMODEL\"";
3016  break;
3017  case PUSH:
3018  os << " :cvc_command" << space;
3019  if(e.arity()==0)
3020  os << "\"PUSH\"";
3021  else
3022  os << "\"PUSH" << space << e[0] << push << "\"";
3023  break;
3024  case POP:
3025  os << " :cvc_command" << space;
3026  if(e.arity()==0)
3027  os << "\"POP\"";
3028  else
3029  os << "\"POP" << space << e[0] << push << "\"";
3030  break;
3031  case POPTO:
3032  os << " :cvc_command" << space;
3033  os << "\"POPTO" << space << e[0] << push << "\""; break;
3034  case PUSH_SCOPE:
3035  os << " :cvc_command" << space;
3036  if(e.arity()==0)
3037  os << "\"PUSH_SCOPE\"";
3038  else
3039  os << "\"PUSH_SCOPE" << space << e[0] << push << "\"";
3040  break;
3041  case POP_SCOPE:
3042  os << " :cvc_command" << space;
3043  if(e.arity()==0)
3044  os << "\"POP_SCOPE\"";
3045  else
3046  os << "\"POP_SCOPE" << space << e[0] << push << "\"";
3047  break;
3048  case POPTO_SCOPE:
3049  os << " :cvc_command" << space;
3050  os << "\"POPTO_SCOPE" << space << e[0] << push << "\""; break;
3051  break;
3052  case RESET:
3053  os << " :cvc_command" << space;
3054  os << "\"RESET\""; break;
3055  break;
3056  case ANNOTATION: {
3057  os << " :" << e[0].getString();
3058  if (e[0].getString() == "notes") {
3059  os << space << e[1];
3060  }
3061  else if (e.arity() > 1) {
3062  os << space << "{" << e[1].getString() << "}";
3063  }
3064  break;
3065  }
3066 
3067  default: /* Must be shared, jump to the end of SMT-LIB v2 symbols */
3068  printSmtLibShared(os,e);
3069  }
3070  break;
3071 
3072  case SMTLIB_V2_LANG:
3073 
3074  switch(e.getKind()) {
3075  case TYPE:
3076  if (e.arity() == 1) {
3077  for (int i=0; i < e[0].arity(); ++i) {
3078  if( i!=0 ) {
3079  os << endl;
3080  }
3081  os << "(declare-sort" << space
3082  << push << nodag << e[0][i] << " 0)" << pop;
3083  }
3084  } else if (e.arity() == 2) {
3085  break;
3086  } else {
3087  throw SmtlibException("TheoryCore::print: SMTLIB: Unexpected TYPE expression");
3088  }
3089  break;
3090 
3091  case BOOLEAN:
3092  os << "Bool";
3093  break;
3094 
3095  case CONST:
3096  if(e.arity() == 2) {
3097  os << "(declare-fun" << space << push
3099  << space;
3100  if( e[1].getKind() == ARROW ) {
3101  os << nodag << e[1];
3102  } else {
3103  os << "()" << space << nodag << e[1];
3104  }
3105  os << ")" << pop;
3106  }
3107  else if (e.arity() == 0) e.printAST(os);
3108  else {
3109  throw SmtlibException("TheoryCore::print: SMTLIB: CONST not implemented");
3110  }
3111  break;
3112 
3113  case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs
3114  if(e.arity() == 1 && e[0].isString()) os << d_translator->escapeSymbol(e[0].getString());
3115  else e.printAST(os);
3116  break;
3117 
3118  case IMPLIES:
3119  os << "(" << push << "=>" << space
3120  << e[0] << space << e[1] << push << ")";
3121  break;
3122 
3123  case IFF:
3124  os << "(" << push << "=" << space
3125  << e[0] << space << e[1] << push << ")";
3126  break;
3127 
3128  case ITE:
3129  os << "(" << push << "ite";
3130  os << space << e[0]
3131  << space << e[1] << space << e[2] << push << ")";
3132  break;
3133 
3134  // Commands
3135  case ASSERT:
3136  os << "(assert" << space << push << e[0] << ")" << pop;
3137  break;
3138 
3139  case QUERY:
3140  if (e[0] != falseExpr() && e[0].negate() != trueExpr()) {
3141  os << push << "(assert" << space << push << e[0].negate() << pop << ")" << pop << endl;
3142  }
3143  os << "(check-sat)";
3144  break;
3145 
3146  case LET: {
3147  // (LET ((var [ type ] val) .... ) body)
3148  Expr var, def;
3149  bool first = true;
3150  int letCount = 0;
3151  ExprHashMap<bool> defs;
3152  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
3153  Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType());
3154  DebugAssert(!tp.isNull(), "Unexpected Null type");
3155  var = (*i)[0];
3156  if(i->arity() == 3) {
3157  def = (*i)[2];
3158  }
3159  else {
3160  def = (*i)[1];
3161  }
3162  if (first || contains(def, defs)) {
3163  if (!first) {
3164  os << push << ")" << pop << pop << space;
3165  defs.clear();
3166  }
3167  os << "(" << push << "let" << space << "(" << push;
3168  ++letCount;
3169  first = false;
3170  }
3171  else {
3172  os << space;
3173  }
3174  defs[def] = true;
3175  os << "(" << push << var << space << nodag << def << ")" << pop;
3176  }
3177  DebugAssert(!first, "Expected at least one child");
3178  os << push << ")" << pop << pop << space << e[1];
3179  for (int j = 0; j < letCount; ++j)
3180  os << ")" << pop;
3181  break;
3182  }
3183  case BOUND_VAR: {
3184  string str = e.getName();
3185  if (str[0] == '_') str[0] = '?';
3186  os << push << d_translator->escapeSymbol(str);
3187  break;
3188  }
3189  case SKOLEM_VAR:
3190  os << "SKOLEM_" + int2string((int)e.getIndex());
3191  break;
3192 
3193  case WHERE:
3194  case ASSERTIONS:
3195  case ASSUMPTIONS:
3196  os << "(get-assertions)";
3197  break;
3198  case COUNTEREXAMPLE:
3199  os << "(get-unsat-core)";
3200  break;
3201  case COUNTERMODEL:
3202  os << "(get-model)";
3203  break;
3204  case PUSH:
3205  case PUSH_SCOPE:
3206  if(e.arity()==0)
3207  os << "(push 1)";
3208  else
3209  os << "(push" << space << push << e[0] << ")" << pop;
3210  break;
3211  case POP:
3212  case POP_SCOPE:
3213  if(e.arity()==0)
3214  os << "(pop 1)";
3215  else
3216  os << "(pop" << space << push << e[0] << ")" << pop;
3217  break;
3218  case POPTO:
3219  os << " :cvc_command" << space
3220  << "\"POPTO" << space << e[0] << push << "\""; break;
3221  case POPTO_SCOPE:
3222  os << " :cvc_command" << space
3223  << "\"POPTO_SCOPE" << space << push << e[0] << "\"" << pop;
3224  break;
3225  case RESET:
3226  os << " :cvc_command" << space;
3227  os << "\"RESET\""; break;
3228  break;
3229  case ANNOTATION: {
3230  os << "(set-info :" << e[0].getString();
3231  if (e.arity() > 1)
3232  os << space << d_translator->quoteAnnotation(e[1].getString());
3233  os << ")";
3234  break;
3235  }
3236 
3237  default: // fall-through to shared symbols
3238  printSmtLibShared(os,e);
3239  }
3240  break;
3241 
3242  case LISP_LANG:
3243  switch(e.getKind()) {
3244  case TRUE_EXPR:
3245  case FALSE_EXPR:
3246  case UCONST:
3247  e.print(os); break;
3248  case TYPE:
3249  if(e.arity() == 0) os << "TYPE";
3250  else if(e.arity() == 1)
3251  os << "(" << push << "TYPE" << space << e[0] << push << ")";
3252  else if(e.arity() == 2)
3253  os << "(" << push << "TYPE" << space << e[0]
3254  << space << e[1] << push << ")";
3255  else e.printAST(os);
3256  break;
3257  case ID: // FIXME: when lisp becomes case-insensitive, fix printing of IDs
3258  if(e.arity() == 1 && e[0].isString()) os << e[0].getString();
3259  else e.printAST(os);
3260  break;
3261  case CONST:
3262  if(e.arity() == 2)
3263  os << "(" << push << "CONST" << space << e[0]
3264  << space << e[1] << push << ")";
3265  else
3266  e.printAST(os);
3267  break;
3268  case SUBTYPE:
3269  os << "SUBTYPE(" << push << e[0] << push << ")";
3270  break;
3271  case TYPEDEF: {
3272  // This is used when dumping declarations to file. Print just
3273  // the name of the type, unless it's a messed-up expression.
3274  if(e.arity() != 2) e.printAST(os);
3275  else if(e[0].isString()) os << e[0].getString();
3276  else e[0].print(os);
3277  break;
3278  }
3279  case EQ:
3280  // When a separator starts with a space (like " = "), add the
3281  // leading space with 'space' modifier. If this separator goes
3282  // to the next line, the leading spaces must be eaten up to get
3283  // the indentation right; 'space' will tell the indentation
3284  // engine that it is a space that can be eaten. A space in a
3285  // string (like " ") will never be eaten.
3286  os << "(" << push << "=" << space << e[0]
3287  << space << e[1] << push << ")";
3288  break;
3289  case NOT:
3290  os << "(" << push << "NOT" << space << e[0] << push << ")";
3291  break;
3292  case AND: {
3293  int i=0, iend=e.arity();
3294  os << "(" << push << "AND";
3295  for(; i!=iend; ++i) os << space << e[i];
3296  os << push << ")";
3297  }
3298  break;
3299  case OR: {
3300  int i=0, iend=e.arity();
3301  os << "(" << push << "OR";
3302  for(; i!=iend; ++i) os << space << e[i] << space;
3303  os << push << ")";
3304  }
3305  break;
3306  case ITE:
3307  os << "(" << push << "IF" << space << e[0]
3308  << space << e[1] << space << e[2] << push << ")";
3309  break;
3310  case IFF:
3311  os << "(" << push << "<=>" << space
3312  << e[0] << space << e[1] << push << ")";
3313  break;
3314  case IMPLIES:
3315  os << "(" << push << "=>" << space
3316  << e[0] << space << e[1] << push << ")";
3317  break;
3318  // Commands
3319  case ASSERT:
3320  os << "(" << push << "ASSERT" << space << e[0] << push << ")";
3321  break;
3322  case TRANSFORM:
3323  os << "(" << push << "TRANSFORM" << space << e[0] << push << ")";
3324  break;
3325  case QUERY:
3326  os << "(" << push << "QUERY" << space << e[0] << push << ")";
3327  break;
3328  case PUSH:
3329  os << "(PUSH)"; break;
3330  case POP:
3331  os << "(POP)"; break;
3332  case POPTO:
3333  os << "(" << push << "POPTO" << space << e[0] << push << ")"; break;
3334  case RESET:
3335  os << "(" << push << "RESET" << push << ")"; break;
3336  case LETDECL:
3337  if(e.arity() == 2) os << e[1];
3338  else if(e.arity()==3) // It's a declaration of a named Expr
3339  os << e[0] << push << ":" << space << push << e[1] << push << " ="
3340  << pop << pop << space << e[2];
3341  else e.printAST(os);
3342  break;
3343  case LET: {
3344  // (LET ((var [ type ] val) .... ) body)
3345  bool first(true);
3346  os << "(" << push << "LET" << space << "(" << push;
3347  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
3348  if(!first) os << space;
3349  else first = false;
3350  os << "(" << push;
3351  if(i->arity() == 3) {
3352  os << (*i)[0] << space << (*i)[1]
3353  << space << nodag << (*i)[2];
3354  } else {
3355  os << (*i)[0];
3356  Type tp((*i)[0].lookupType());
3357  if(!tp.isNull()) os << space << tp.getExpr();
3358  os << space << nodag << (*i)[1];
3359  }
3360  os << push << ")" << pop << pop;
3361  }
3362  os << push << ")" << pop << pop << space << e[1] << push << ")";
3363  break;
3364  }
3365  case BOUND_VAR:
3366  // os << e.getName()+"_"+e.getUid(); by yeting
3367  os << e.getName();
3368  break;
3369  case SKOLEM_VAR:
3370  os << "SKOLEM_" + int2string((int)e.getIndex());
3371  break;
3372  case PF_APPLY: {// FIXME: this will eventually go to the "symsim" theory
3373  DebugAssert(e.arity() > 0, "TheoryCore::print(): "
3374  "Proof rule application must have at "
3375  "least one argument (rule name):\n "+e.toString());
3376  os << push << "(" << push;
3377  bool first(true);
3378  for(int i=0; i<e.arity(); i++) {
3379  if(first) first=false;
3380  else os << space;
3381  os << e[i];
3382  }
3383  os << push << ")";
3384  break;
3385  }
3386  case RAW_LIST: {
3387  os << "(" << push;
3388  bool firstTime(true);
3389  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
3390  if(firstTime) firstTime = false;
3391  else os << space;
3392  os << *i;
3393  }
3394  os << push << ")";
3395  break;
3396  }
3397  case ANY_TYPE:
3398  os << "ANY_TYPE";
3399  break;
3400  case PF_HOLE: // FIXME: implement this (now fall through to default)
3401  default:
3402  // Print the top node in the default LISP format, continue with
3403  // pretty-printing for children.
3404  e.printAST(os);
3405  }
3406  break; // end of case LISP_LANGUAGE
3407  default:
3408  // Print the top node in the default LISP format, continue with
3409  // pretty-printing for children.
3410  e.printAST(os);
3411  }
3412  return os;
3413 }
3414 
3416 {
3417  // Theory 0 is TheoryCore, skip it
3418  for(int i = 1; i<getNumTheories(); i++) {
3419  if(d_theories[i] != this)
3420  d_theories[i]->refineCounterExample();
3421  if(inconsistent()) {
3422  thm = inconsistentThm();
3423  return false;
3424  }
3425  }
3426  return true;
3427 }
3428 
3430 {
3431  // Theory 0 is TheoryCore, skip it
3432  for(int i = 1; i<getNumTheories(); i++) {
3433  if(d_theories[i] != this)
3434  d_theories[i]->refineCounterExample();
3435  if(inconsistent()) {
3436  vector<Expr> assump;
3438  Expr a = Expr(RAW_LIST, assump, d_em);
3439  throw EvalException("Theory["+d_theories[i]->getName()
3440  +"]: Model Creation failed due "
3441  "to the following assumptions:\n\n"
3442  +a.toString()
3443  +"\n\nYou might be using an incomplete logical fragment.");
3444  }
3445  }
3446 }
3447 
3448 
3449 void TheoryCore::computeModelBasic(const vector<Expr>& v) {
3450  for(vector<Expr>::const_iterator i=v.begin(), iend=v.end(); i!=iend; ++i) {
3451  TRACE("model", "Model var "+i->toString()+" = ", find(*i).getRHS(), "");
3452  DebugAssert((*i).getType().isBool(), "TheoryCore::computeModel: *i = "
3453  +(*i).toString());
3454  Expr val = find(*i).getRHS();
3455  if(!val.isBoolConst()) val = d_em->trueExpr();
3456  assignValue(*i, val);
3457  }
3458 }
3459 
3460 
3461 /*****************************************************************************/
3462 /*
3463  * User-level API methods
3464  */
3465 /*****************************************************************************/
3466 
3467 
3469 {
3470  //<<<<<<< theory_core_sat.cpp
3471  // cout<<"theory_core_sat.cpp asserted fact:"<<e<<endl;
3472  // IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
3473  // TRACE("addFact", indentStr, "Assert: ", e.getExpr().toString(PRESENTATION_LANG));
3474  //=======
3475  IF_DEBUG(string indentStr(getCM()->scopeLevel(), ' ');)
3476  TRACE("addFact", indentStr, "Assert: ", e.getExpr().toString(PRESENTATION_LANG));
3477  //>>>>>>> 1.7
3478  DebugAssert(!d_inAddFact, "Recursive call to addFact() is not allowed");
3479  DebugAssert(d_queue.empty(), "addFact[start]: Expected empty queue");
3480  // DebugAssert(d_queueSE.empty(), "addFact[start]: Expected empty queue");
3481  DebugAssert(d_update_thms.empty() && d_update_data.empty(),
3482  "addFact[start]: Expected empty update list");
3484 
3485  if(!d_inconsistent && !outOfResources()) {
3486  getResource();
3487  d_queue.push(e);
3488 
3489  // cout<<"queue pushed" <<e<<endl;
3490  // cout<<"queue pushed id" <<e.getQuantLevel()<<endl;
3491 
3492  if (outOfResources()) {
3493  // No more resources: ignore all the remaining facts and fail
3494  // gracefully
3495  setIncomplete("Exhausted user-specified resource");
3496  }
3497  processFactQueue();
3498  }
3499 
3500  DebugAssert(d_queue.empty(), "addFact[end]: Expected empty queue");
3501  DebugAssert(d_queueSE.empty(), "addFact[end]: Expected empty queue");
3502  DebugAssert(d_update_thms.empty() && d_update_data.empty(),
3503  "addFact[end]: Expected empty update list");
3504 }
3505 
3506 
3508 {
3509  DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue");
3510  DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue");
3511  DebugAssert(!d_inCheckSATCore, "Recursive call to checkSATCore is not allowed!");
3513  IF_DEBUG(debugger.counter("DP checkSAT(fullEffort) calls")++;)
3514  DebugAssert(d_update_thms.empty() && d_update_data.empty(),
3515  "addFact[start]: Expected empty update list");
3516 
3517  bool lemmas = processFactQueue(FULL);
3518 
3519  DebugAssert(d_queue.empty(), "checkSATCore[start]: Expected empty queue");
3520  DebugAssert(d_queueSE.empty(), "checkSATCore[start]: Expected empty queue");
3521  DebugAssert(d_update_thms.empty() && d_update_data.empty(),
3522  "addFact[end]: Expected empty update list");
3523 
3524  return !lemmas;
3525 }
3526 
3527 
3528 bool TheoryCore::incomplete(vector<string>& reasons)
3529 {
3530  if(d_incomplete.size() > 0) {
3532  iend=d_incomplete.end(); i!=iend; ++i)
3533  reasons.push_back((*i).first);
3534  return true;
3535  }
3536  else
3537  return false;
3538 }
3539 
3540 
3541 void TheoryCore::registerAtom(const Expr& e, const Theorem& thm)
3542 {
3543  DebugAssert(!e.isEq() || e[0] != e[1], "expected non-reflexive");
3544  DebugAssert(!e.isRegisteredAtom(), "atom registered more than once");
3545  // if (e.isQuantifier()) return;
3546  e.setRegisteredAtom();
3547  if(d_termTheorems.find(e) != d_termTheorems.end()){
3548  // cout<<"found this before 1 : "<<e<<endl;
3549  }
3550  // cout<<"#1# get into "<<e<<endl;
3551  d_termTheorems[e] = thm;
3552  DebugAssert(e.isAbsAtomicFormula(), "Expected atomic formula");
3554  Theorem thm2 = simplify(e);
3555  if (thm2.getRHS().isTrue()) {
3557  }
3558  else if (thm2.getRHS().isFalse()) {
3560  }
3561  else {
3562  //TODO: why does arith need thm2.getRHS() instead of e?
3563  // theoryOf(e)->registerAtom(e);
3564  theoryOf(thm2.getRHS())->registerAtom(thm2.getRHS());
3565  setupSubFormulas(thm2.getRHS(), e, thm);
3566  }
3568 }
3569 
3570 
3572 {
3573  Theorem res;
3574  if (d_impliedLiteralsIdx < d_impliedLiterals.size()) {
3577  }
3578  return res;
3579 }
3580 
3581 
3583 {
3584  DebugAssert(index < d_impliedLiterals.size(), "index out of bounds");
3585  return d_impliedLiterals[index];
3586 }
3587 
3588 
3590 {
3591  // check cache
3592  ExprMap<Expr>::iterator iParseCache = d_parseCache->find(e);
3593  if (iParseCache != d_parseCache->end()) {
3594  return (*iParseCache).second;
3595  }
3596  // Remember the current size of the bound variable stack
3597  size_t boundVarSize = d_boundVarStack.size();
3598 
3599  // Compute the kind to determine what to do with the expression
3600  int kind = NULL_KIND;
3601  Expr res;
3602 
3603  switch(e.getKind()) {
3604  case ID: {
3605  const Expr c1 = e[0];
3606  kind = getEM()->getKind(c1.getString());
3607  if(kind == NULL_KIND) { // It's an identifier; try to resolve it
3608  res = resolveID(e[0].getString());
3609  if(res.isNull())
3610  throw ParserException("cannot resolve an identifier: "
3611  +e[0].toString());
3612  else {
3613  DebugAssert(!e.isApply(), "Unexpected apply function");
3614  }
3615  }
3616  // Otherwise exit the switch and use DP-specific parsing
3617  break;
3618  }
3619  case RAW_LIST: {
3620  if(e.arity() == 0)
3621  throw ParserException("Empty list is not an expression!");
3622  const Expr& op = e[0];
3623  // First, resolve the operator
3624  switch(op.getKind()) {
3625  case ID: { // The operator in the list is ID: is it keyword or variable?
3626  kind = getEM()->getKind(op[0].getString());
3627  if(kind == NULL_KIND) {
3628  // It's a named function application. Resolve the ID.
3629  res = resolveID(op[0].getString());
3630  if(res.isNull()){
3631  // cout<<"stop here: " << e << endl;
3632  // cout<<"stop here op: " << op << endl;
3633  // cout<<"stop here op[0]: " << op[0] << endl;
3634  throw ParserException("cannot resolve an identifier: "
3635  +op[0].toString());
3636  }
3637  if(e.arity() < 2)
3638  throw ParserException("Bad function application: "+e.toString());
3639  Expr::iterator i=e.begin(), iend=e.end();
3640  ++i;
3641  vector<Expr> args;
3642  for(; i!=iend; ++i) args.push_back(parseExpr(*i));
3643  res = Expr(res.mkOp(), args);
3644  }
3645  // Proceed to DP-specific parsing
3646  break;
3647  }
3648  case RAW_LIST:
3649  // This can only be a lambda expression application.
3650  kind = LAMBDA;
3651  break;
3652  case STRING_EXPR: {
3653  vector<Expr> assignmentVars;
3654  if(op.getString() == "_ANNOTATION") {
3655  for(int i = 0; i < e[2].arity(); ++i) {
3656  if(e[2][i][0][0].getString() == ":named") {
3657  FatalAssert(e[2][i].arity() == 2 && e[2][i][1].getKind() == ID,
3658  ":named annotation must take a name");
3659  assignmentVars.push_back(e[2][i][1]);
3660  }
3661  }
3662  Expr parsed = parseExpr(e[1]);
3663  for(unsigned i = 0; i < assignmentVars.size(); ++i) {
3664  d_assignment.push_back(make_pair(assignmentVars[i], parsed));
3665  }
3666  // Return rather than break; nothing more to do with the
3667  // annotation expr itself; it is stripped away.
3668  return parsed;
3669  }
3670  /* else fall through... */
3671  }
3672  default:
3673  throw ParserException("Bad operator in "+e.toString());
3674  }
3675  break; // Exit the top-level switch, proceed to DP-specific parsing
3676  }
3677  default: // Can only be a string or a number.
3678  res = e;
3679  }
3680 
3681  // DP-specific parsing
3682  if(res.isNull()) {
3683  if (hasTheory(kind)) {
3684  res = theoryOf(kind)->parseExprOp(e);
3685  // Restore the bound variable stack
3686  if (d_boundVarStack.size() > boundVarSize) {
3687  d_parseCache->clear();
3688  if (boundVarSize == 0) {
3690  }
3691  while(d_boundVarStack.size() > boundVarSize) {
3692  pair<string,Expr>& bv = d_boundVarStack.back();
3693  hash_map<string,Expr>::iterator iBoundVarMap = d_boundVarMap.find(bv.first);
3694  DebugAssert(iBoundVarMap != d_boundVarMap.end(), "Expected bv in map");
3695  if ((*iBoundVarMap).second.getKind() == RAW_LIST) {
3696  (*iBoundVarMap).second = (*iBoundVarMap).second[1];
3697  }
3698  else d_boundVarMap.erase(bv.first);
3699  d_boundVarStack.pop_back();
3700  }
3701  }
3702  }
3703  else {
3704  res = e;
3705  }
3706  }
3707  (*d_parseCache)[e] = res;
3708  if (!getEM()->isTypeKind(res.getOpKind())) res.getType();
3709  return res;
3710 }
3711 
3712 
3713 void TheoryCore::assignValue(const Expr& t, const Expr& val)
3714 {
3715  DebugAssert(d_varAssignments.count(t) == 0
3716  || d_varAssignments[t].getRHS() == val,
3717  "TheoryCore::assignValue("+t.toString()+" := "+val.toString()
3718  +")\n variable already has a different value");
3719  // Check if the assignment theorem can be derived from the find of t
3720  Theorem thm(find(t));
3721  Expr t2 = thm.getRHS();
3722 
3723  if(t2!=val) {
3724  bool isBool(t2.getType().isBool());
3725  Expr assump = (isBool)? t2.iffExpr(val) : t2.eqExpr(val);
3726  Theorem assertThm = d_coreSatAPI->addAssumption(assump);
3727  addFact(assertThm);
3728  thm = transitivityRule(thm, assertThm);
3729  }
3730  d_varAssignments[t] = thm;
3731 }
3732 
3733 
3735 {
3736  DebugAssert(thm.isRewrite(), "TheoryCore::assignValue("+thm.toString()+")");
3737  const Expr& t = thm.getLHS();
3738  const Expr& val = thm.getRHS();
3739  DebugAssert(d_varAssignments.count(t) == 0
3740  || d_varAssignments[t].getRHS() == val,
3741  "TheoryCore::assignValue("+thm.getExpr().toString()
3742  +")\n variable already has a different value:\n "
3743  +d_varAssignments[t].getExpr().toString());
3744  d_varAssignments[t] = thm;
3745  // Check if the assignment theorem can be derived from the find of t
3746  Theorem findThm(find(t));
3747  const Expr& t2 = findThm.getRHS();
3748 
3749  if(t2!=val) {
3750  Theorem thm2 = transitivityRule(symmetryRule(findThm), thm);
3751  addFact(thm2);
3752  }
3753 }
3754 
3755 
3757 {
3758  TRACE("model", "TheoryCore::addToVarDB(", e, ")");
3759  d_vars.push_back(e);
3760 }
3761 
3762 
3764 {
3765  TRACE_MSG("model", "collectBasicVars() {");
3766  // Clear caches
3767  d_varModelMap.clear();
3768  d_varAssignments.clear();
3769  d_basicModelVars.clear();
3770  d_simplifiedModelVars.clear();
3771  // Current stack of variables to process
3772  vector<Expr> stack(d_vars.begin(), d_vars.end());
3773  size_t lastSize(0);
3774  while(stack.size() > 0) {
3775  Expr var(stack.back());
3776  stack.pop_back();
3777  if(d_varModelMap.count(var) > 0) continue; // Already processed
3778  Theorem findThm(find(var));
3779  if(findThm.getRHS()!=var) { // Replace var with its find
3780  d_simplifiedModelVars[var] = findThm;
3781  stack.push_back(findThm.getRHS());
3782  TRACE("model", "collectBasicVars: simplified var: ", findThm.getExpr(), "");
3783  continue; // Recycle to the beginning of the loop
3784  }
3785  lastSize = stack.size();
3786  TRACE("model", "getModelTerm(", var, ") {");
3787  getModelTerm(var, stack);
3788  TRACE("model", "getModelTerm => ",
3789  Expr(RAW_LIST, stack, getEM()), " }");
3790  if(stack.size() == lastSize) {
3791  // Add a primitive variable
3792  TRACE("model", "collectBasicVars: adding primitive var: ", var, "");
3793  d_basicModelVars.push_back(var);
3794  if(var.isTerm()) {
3795  Theory* t1 = theoryOf(var);
3796  Theory* t2 = theoryOf(getBaseType(var).getExpr().getKind());
3797  if(t1 != t2) {
3798  TRACE("model", "collectBasicVars: adding shared var: ", var, "");
3799  t1->addSharedTerm(var);
3800  t2->addSharedTerm(var);
3801  }
3802  }
3803  } else { // Record the descendants of var
3804  vector<Expr>& kids = d_varModelMap[var];
3805  for(size_t i=lastSize; i<stack.size(); ++i) {
3806  DebugAssert(stack[i] != var, "Primitive var was pushed on "
3807  "the stack in computeModelTerm(): "+var.toString());
3808  kids.push_back(stack[i]);
3809  }
3810  TRACE("model", "collectBasicVars: var="+var.toString()
3811  +" maps into vars=", Expr(RAW_LIST, kids, getEM()), "");
3812  }
3813  }
3814  TRACE_MSG("model", "collectBasicVars() => }");
3815 }
3816 
3818 {
3819  size_t numTheories = getNumTheories();
3820  // Use STL set to prune duplicate variables in theories
3821  vector<set<Expr> > theoryExprs(numTheories+1);
3822 
3823  // Sort out model vars by theories
3824  for(size_t j = 0 ; j<d_basicModelVars.size() ; j++) {
3825  const Expr& var = d_basicModelVars[j];
3826  Theorem findThm(find(var));
3827  if(findThm.getRHS()!=var) { // Replace var with its find and skip it
3828  TRACE("model", "buildModel: replace var="+var.toString(), " with find(var)=", findThm.getRHS());
3829  d_simplifiedModelVars[var] = findThm;
3830  continue;
3831  }
3832 
3833  Theory *th = theoryOf(getBaseType(var).getExpr().getKind());
3834  size_t i=0;
3835  for(; i<numTheories && d_theories[i] != th; ++i);
3836  DebugAssert(i<numTheories && d_theories[i] == th, "TheoryCore::buildModel: cannot find the theory [" +th->getName()+"] for the variable: " +var.toString());
3837  theoryExprs[i].insert(var);
3838  TRACE("model", "buildModel: adding ", var, " to theory "+d_theories[i]->getName());
3839  }
3840 
3841  // Build a model for the basic-type variables
3842  for(int i=0; i<getNumTheories(); i++) {
3843  if(theoryExprs[i].size() > 0) {
3844  TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] {");
3845  // Copy the corresponding variables into a vector
3846  vector<Expr> vars;
3847  vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end());
3848  d_theories[i]->computeModelBasic(vars);
3849  TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] => }");
3850  if(inconsistent()) {
3851  vector<Expr> assump;
3852  thm = inconsistentThm();
3853  return false;
3854  }
3855  }
3856  }
3857 
3858  return true;
3859 }
3860 
3861 
3863 {
3864  TRACE_MSG("model", "buildModel() {");
3865 
3866  size_t numTheories = getNumTheories();
3867  // Use STL set to prune duplicate variables in theories
3868  vector<set<Expr> > theoryExprs(numTheories+1);
3869  // Sort out model vars by theories
3870  for(size_t j = 0 ; j<d_basicModelVars.size() ; j++) {
3871  const Expr& var = d_basicModelVars[j];
3872  Theorem findThm(find(var));
3873  if(findThm.getRHS()!=var) { // Replace var with its find and skip it
3874  TRACE("model", "buildModel: replace var="+var.toString(),
3875  " with find(var)=", findThm.getRHS());
3876  d_simplifiedModelVars[var] = findThm;
3877  continue;
3878  }
3879 
3880  Theory *th = theoryOf(getBaseType(var).getExpr().getKind());
3881  size_t i=0;
3882  for(; i<numTheories && d_theories[i] != th; ++i);
3883  DebugAssert(i<numTheories && d_theories[i] == th,
3884  "TheoryCore::buildModel: cannot find the theory ["
3885  +th->getName()+"] for the variable: "
3886  +var.toString());
3887  theoryExprs[i].insert(var);
3888  TRACE("model", "buildModel: adding ", var,
3889  " to theory "+d_theories[i]->getName());
3890  }
3891  // Build a model for the basic-type variables
3892  for(int i=0; i<getNumTheories(); i++) {
3893  if(theoryExprs[i].size() > 0) {
3894  TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] {");
3895  // Copy the corresponding variables into a vector
3896  vector<Expr> vars;
3897  vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end());
3898  d_theories[i]->computeModelBasic(vars);
3899  TRACE("model", "computeModelBasic[", d_theories[i]->getName(), "] => }");
3900  if(inconsistent()) {
3901  vector<Expr> assump;
3903  Expr a = Expr(RAW_LIST, assump, d_em);
3904  throw EvalException
3905  ("Model Creation failed in Theory["
3906  +d_theories[i]->getName()
3907  +"] due to the following assumptions:\n\n"
3908  +a.toString()
3909  +"\n\nYou might be using an incomplete logical fragment.");
3910  }
3911  }
3912  }
3913  // Recombine the values for the compound-type variables
3915  for(vector<Expr>::const_iterator i=d_vars.begin(), iend=d_vars.end(); i!=iend; ++i) {
3916  Expr var(*i);
3917  TRACE("model", "buildModel: recombining var=", var, "");
3918  k=d_simplifiedModelVars.find(var);
3919  Theorem simp; // Null by default
3920  if(k!=kend) { // This var is simplified
3921  simp = k->second;
3922  TRACE("model", "buildModel: simplified var="+var.toString()+" to ",
3923  simp.getRHS(), "");
3924  var = simp.getRHS();
3925  }
3926  collectModelValues(var, m);
3927  if(d_varAssignments.count(var) > 0) {
3928  if(!simp.isNull()) {
3929  Theorem thm(transitivityRule(simp, d_varAssignments[var]));
3930  assignValue(thm);
3931  DebugAssert(thm.getLHS() == *i, "");
3932  m[*i] = thm.getRHS();
3933  } else
3934  m[*i] = d_varAssignments[var].getRHS();
3935  }
3936 // else if(simp.isNull())
3937 // m[*i] = *i;
3938 // else
3939 // m[*i] = simp.getRHS();
3940  }
3941  TRACE_MSG("model", "buildModel => }");
3942 }
3943 
3944 
3945 // Recursively build a compound-type variable assignment for e
3946 /*! Not all theories may implement aggregation of compound values. If
3947  * a compound variable is not assigned by a theory, add the more
3948  * primitive variable assignments to 'm'.
3949  *
3950  * Some variables may simplify to something else (simplifiedVars map).
3951  * INVARIANT: e is always simplified (it's not in simplifiedVars map).
3952  * Also, if v simplifies to e, and e is assigned, then v must be assigned.
3953  */
3955 {
3956  TRACE("model", "collectModelValues(", e, ") {");
3957  if(d_varAssignments.count(e) > 0) {
3958  TRACE("model", "collectModelValues[cached] => ",
3959  d_varAssignments[e].getRHS(), " }");
3960  return; // Got it already
3961  }
3963  k=d_simplifiedModelVars.find(e);
3964  if(k!=kend) {
3965  const Theorem& findThm = k->second;
3966  const Expr& ee = findThm.getRHS();
3967  collectModelValues(ee, m);
3968  if(d_varAssignments.count(ee) > 0) {
3969  Theorem thm = transitivityRule(findThm, d_varAssignments[ee]);
3970  assignValue(thm);
3971  }
3972  TRACE("model", "collectModelValues[simplified] => ",
3973  d_varAssignments[e].getRHS(), " }");
3974  return;
3975  }
3976  if(d_varModelMap.count(e) == 0) { // Consider it a value of itself
3978  TRACE("model", "collectModelValues[e=e] => ", e, " }");
3979  return; // Got it already
3980  }
3981  // Get the vector of more primitive vars
3982  const vector<Expr>& vars = d_varModelMap[e];
3983  // Recurse
3984  bool gotAll(true); // Whether we got all the values
3985  for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
3986  Expr var(*i);
3987 // k=d_simplifiedModelVars.find(var);
3988 // Theorem simp; // Null by default
3989 // if(k!=kend) { // This var is simplified
3990 // simp = k->second;
3991 // var = simp.getRHS();
3992 // }
3993  collectModelValues(var, m);
3994  if(d_varAssignments.count(var) == 0) {
3995  gotAll = false;
3996  }
3997 // else if(!simp.isNull()) {
3998 // Theorem thm(transitivityRule(simp, d_varAssignments[var]));
3999 // DebugAssert(thm.getLHS() == *i, "");
4000 // assignValue(thm);
4001 // }
4002  }
4003  IF_DEBUG(vector<Expr> res;)
4004  if(gotAll) {
4005  vector<Expr> assigned; // What DP actually assigns
4006  Theory* th = theoryOf(getBaseType(e).getExpr());
4007  TRACE("model", "computeModel["+th->getName()+"](", e, ") {");
4008  th->computeModel(e, assigned);
4009  TRACE("model", "computeModel["+th->getName()+"] => ",
4010  Expr(RAW_LIST, assigned, getEM()), " }");
4011  // Check if the assigned vars are different from e
4012  if(!(assigned.size()==1 && assigned[0]==e)) {
4013  // if(d_varAssignments.count(e) == 0) {
4014  for(vector<Expr>::iterator i=assigned.begin(), iend=assigned.end();
4015  i!=iend; ++i) {
4016  if(*i == e) continue; // Skip the original var
4017  m[*i] = getModelValue(*i).getRHS();
4018  IF_DEBUG(res.push_back(getModelValue(*i).getExpr());)
4019  }
4020  } else {
4021  IF_DEBUG(res.push_back(getModelValue(e).getExpr());)
4022  }
4023  }
4024  TRACE("model", "collectModelValues => ",
4025  Expr(RAW_LIST, res, getEM()), " }");
4026 }
4027 
4028 
4030  DebugAssert(e.isAbsLiteral(), "rewriteLiteral("+e.toString()
4031  +")\nExpected a literal.");
4032  Theorem res;
4033  //Theory* i = theoryOf(getBaseType(e).getExpr());
4034  bool neg(e.isNot());
4035  const Expr a = neg? e[0] : e;
4036  Theory * i;
4037  if(a.isEq())
4038  i = theoryOf(getBaseType(a[0]).getExpr());
4039  else if (a.arity() > 1)
4040  i = theoryOf(getBaseType(a[0]).getExpr());
4041  else
4042  i = theoryOf(a);
4043  res = i->rewriteAtomic(a);
4044  if(neg) res = d_commonRules->iffContrapositive(res);
4045  return res;
4046 }
4047 
4048 
4049 
4050 
4051 
4052 
4053 void TheoryCore::setTimeLimit(unsigned limit) {
4054  initTimeLimit();
4055  d_timeLimit = limit;
4056 }
4057 
4059  d_timeBase = clock() / (CLOCKS_PER_SEC / 10);
4060 }
4061 
4063  if (d_timeLimit > 0
4064  && d_timeLimit < (unsigned)(clock() / (CLOCKS_PER_SEC / 10)) - d_timeBase) {
4065  setIncomplete("Exhausted user-specified time limit");
4066  return true;
4067  } else {
4068  return false;
4069  }
4070 }
4071 
4072 
4073 
4074 /*****************************************************************************/
4075 /*
4076  * Methods provided for benefit of theories
4077  */
4078 /*****************************************************************************/
4079 
4080 
4081 /*!
4082  * Invariants:
4083  * - The input theorem e is either an equality or a conjunction of
4084  * equalities;
4085  * - In each equality e1=e2, the RHS e2 i-leaf-simplified;
4086  * - At the time of calling update(), all equalities in the queue are
4087  * processed by assertFormula() and the equivalence classes are merged
4088  * in the union-find database.
4089  *
4090  * In other words, the entire equality queue is processed "in parallel".
4091  */
4092 
4094 {
4095  IF_DEBUG(
4096  string indentStr(getCM()->scopeLevel(), ' ');
4097  TRACE("facts", indentStr, "assertEqualities: ", e);
4099  )
4100  TRACE("quant update", "equs in core ", e.getExpr(), "");
4101 
4102  // fast case
4103  if (e.isRewrite()) {
4104  const Expr& lhs = e.getLHS();
4105  const Expr& rhs = e.getRHS();
4106  DebugAssert(lhs.isTerm(), "term expected");
4107  DebugAssert(findReduced(lhs) &&
4108  findReduced(rhs), "should be find-reduced");
4109  DebugAssert(lhs != rhs, "expected different lhs and rhs");
4110  assertFormula(e);
4111  lhs.setFind(e);
4112  Theorem tmp = lhs.getEqNext();
4113  lhs.setEqNext(transitivityRule(e, rhs.getEqNext()));
4114  rhs.setEqNext(transitivityRule(symmetryRule(e), tmp));
4116  NotifyList *L;
4117  L = lhs.getNotify();
4118  if (L) processNotify(e, L);
4120  }
4121  else if (e.getExpr().isFalse()) {
4122  setInconsistent(e);
4123  }
4124  else {
4125  Expr conj = e.getExpr();
4126  DebugAssert(conj.isAnd(), "Expected conjunction");
4127  vector<Theorem> eqs;
4128  Theorem t;
4129  int index;
4130 
4131  for (index = 0; index < conj.arity(); ++index) {
4132  t = d_commonRules->andElim(e, index);
4133  eqs.push_back(t);
4134  if (t.getExpr().isFalse()) {
4135  setInconsistent(t);
4136  return;
4137  }
4138  DebugAssert(t.isRewrite(), "Expected rewrite");
4139  DebugAssert(t.getLHS().isTerm(), "term expected");
4141  findReduced(t.getRHS()), "should be find-reduced");
4142  assertFormula(t);
4143  if (d_inconsistent) return;
4144  }
4145 
4146  // Merge the equivalence classes
4147  vector<Theorem>::iterator i = eqs.begin(), iend = eqs.end();
4148  for(; i!=iend; ++i) {
4149  const Theorem& thm = *i;
4150  const Expr& lhs = thm.getLHS();
4151  const Expr& rhs = thm.getRHS();
4152  DebugAssert(find(lhs).getRHS() == lhs,
4153  "find error: thm = "+thm.getExpr().toString()
4154  +"\n\n find(lhs) = "
4155  +find(lhs).getRHS().toString());
4156  DebugAssert(find(rhs).getRHS() == rhs,
4157  "find error: thm = "+thm.getExpr().toString()
4158  +"\n\n find(rhs) = "
4159  +find(rhs).getRHS().toString());
4160  lhs.setFind(thm);
4161  Theorem tmp = lhs.getEqNext();
4162  lhs.setEqNext(transitivityRule(thm, rhs.getEqNext()));
4163  rhs.setEqNext(transitivityRule(symmetryRule(thm), tmp));
4164  }
4165 
4167 
4168  // Call the update() functions (process NotifyLists).
4169 
4170  for(i=eqs.begin(); i!=iend && !d_inconsistent; ++i) {
4171  const Theorem& thm = *i;
4172  NotifyList *L = thm.getLHS().getNotify();
4173  if (L) processNotify(thm, L);
4174  processNotify(thm, &d_notifyEq);
4175  }
4176  }
4177 }
4178 
4179 
4180 void TheoryCore::setIncomplete(const string& reason)
4181 {
4182  d_incomplete.insert(reason, true);
4183 }
4184 
4185 
4187 {
4188  return d_rules->typePred(e);
4189 }
4190 
4191 
4192 static bool hasBoundVarRec(const Expr& e)
4193 {
4194  if (e.getFlag()) return false;
4195  if (e.isQuantifier()) return false;
4196  if (e.getKind() == BOUND_VAR) return true;
4197  for (int i = 0, ar = e.arity(); i < ar; ++i) {
4198  if (hasBoundVarRec(e[i])) return true;
4199  }
4200  e.setFlag();
4201  return false;
4202 }
4203 
4205 static bool hasBoundVar(const Expr& e)
4206 {
4207  e.getEM()->clearFlags();
4208  return hasBoundVarRec(e);
4209 }
4210 )
4211 
4212 
4213 void TheoryCore::enqueueFact(const Theorem& e)
4214 {
4215  // The theorem scope shouldn't be higher than current
4216  DebugAssert(e.getScope() <= d_cm->scopeLevel(),
4217  "\n e.getScope()="+int2string(e.getScope())
4218  +"\n scopeLevel="+int2string(d_cm->scopeLevel())
4219  +"\n e = "+e.getExpr().toString());
4221  "enqueueFact() is called outside of addFact()"
4222  " or checkSATCore() or registerAtom() or preprocess");
4223  DebugAssert((e.isRewrite() && !hasBoundVar(e.getLHS())
4224  && !hasBoundVar(e.getRHS())) ||
4225  (!e.isRewrite() && !hasBoundVar(e.getExpr())),
4226  "Bound vars shouldn't be free: " + e.toString());
4227 
4228  // No need to enqueue when already inconsistent or out of resources
4229  if (d_inconsistent || outOfResources()) return;
4230 
4231  if (!e.isRewrite() && e.getExpr().isFalse()) {
4232  setInconsistent(e);
4233  } else {
4234  getResource();
4235  d_queue.push(e);
4236  if (outOfResources()) {
4237  // No more resources: ignore all the remaining facts and fail
4238  // gracefully
4239  setIncomplete("Exhausted user-specified resource");
4240  }
4241  }
4242 }
4243 
4244 
4246 {
4247  DebugAssert(e.getExpr() == falseExpr(), "Expected proof of false");
4248  d_inconsistent = true; d_incThm = e;
4249  // if(!d_queueSE.empty()){
4250  // cout<<"before SAT 1"<<endl;
4251  // }
4252  d_queueSE.clear();
4253  // Theory 0 is TheoryCore, skip it
4254  for(unsigned i=1; i < d_theories.size(); ++i) {
4255  d_theories[i]->notifyInconsistent(e);
4256  }
4257 }
4258 
4259 
4260 void TheoryCore::setupTerm(const Expr& t, Theory* i, const Theorem& thm)
4261 {
4262  int k;
4263  // Atomic formulas (non-terms) may have find pointers without the
4264  // subterms being setup. Recurse down to the terms before checking
4265  // for find pointers.
4266  if (!t.isTerm()) {
4267  if (!t.isStoredPredicate()) {
4268  DebugAssert(t.isAbsLiteral(), "Expected absliteral");
4269  for (k = 0; k < t.arity(); ++k) {
4270  setupTerm(t[k], i, thm);
4271  }
4272  t.setStoredPredicate();
4274  d_termTheorems[t] = thm;
4275  theoryOf(t)->setup(t);
4276  TRACE("quantlevel", "==========\npushed pred | ", t.getIndex(), "|" + t.toString()+"because : "+thm.toString() );
4277  TRACE("quant","pushed pred ",t,thm);
4278  }
4279  return;
4280  }
4281 
4282  // Even if t is already setup, it may become shared with another theory
4283  Theory* j = theoryOf(t);
4284  if(i != j) {
4285  j->addSharedTerm(t);
4286  i->addSharedTerm(t);
4287  }
4288 
4289  // If already setup, nothing else to do
4290  if (t.hasFind()) return;
4291 
4292  // Proceed with the setup
4293 
4294  // Add the term into the set of all terms
4295  d_terms.push_back(t);
4296  d_termTheorems[t] = thm;
4297  TRACE("quantlevel","=========\npushed term ("+t.toString(), ") with quantlevel: ", thm.getQuantLevel());
4298 
4299  for (k = 0; k < t.arity(); ++k) {
4300  setupTerm(t[k], j, thm);
4301  }
4302  t.setFind(reflexivityRule(t));
4303  t.setEqNext(reflexivityRule(t));
4304  j->setup(t);
4305 
4306  // Assert the subtyping predicate AFTER the setup is complete
4307  Theorem pred = d_rules->typePred(t);
4308  pred = iffMP(pred, simplify(pred.getExpr()));
4309  const Expr& predExpr = pred.getExpr();
4310  if(predExpr.isFalse()) {
4311  IF_DEBUG(debugger.counter("conflicts from type predicate")++;)
4312  setInconsistent(pred);
4313  }
4314  else if(!predExpr.isTrue()) {
4315  Theory* k = theoryOf(t.getType().getExpr());
4316  k->assertTypePred(t, pred);
4317  }
4318 }
4319 
4321  vector<Expr> v;
4322  for(unsigned i = 0; i < d_assignment.size(); ++i) {
4323  Theorem res = d_exprTrans->preprocess(d_assignment[i].second);
4324  Theorem simpThm = d_theoryCore->simplify(res.getRHS());
4325  vector<Expr> pr;
4326  pr.push_back(d_assignment[i].first);
4327  pr.push_back(simpThm.getRHS());
4328  v.push_back(Expr(RAW_LIST, pr, getEM()));
4329  }
4330  return Expr(RAW_LIST, v, getEM());
4331 }
4332 
4334  Theorem res = d_exprTrans->preprocess(e);
4335  Theorem simpThm = d_theoryCore->simplify(res.getRHS());
4336  return simpThm.getRHS();
4337 }
4338 
CDO< bool > d_inconsistent
Inconsistent flag.
Definition: theory_core.h:89
Definition: kinds.h:48
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
ExprStream & popSave(ExprStream &os)
Remember the current indentation and pop to the previous position.
ExprStream & pop(ExprStream &os)
Restore the indentation.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
bool isNull() const
Definition: expr.h:1223
for output in SPASS format
Definition: lang.h:49
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin() const
Begin iterator.
Definition: expr.h:1211
Theory * d_solver
The theory which has the solver (if any)
Definition: theory_core.h:131
TheoryCore * d_theoryCore
Provides the core functionality.
Definition: theory.h:68
bool isEq() const
Definition: expr.h:419
Definition: kinds.h:104
ExprStream & nodag(ExprStream &os)
Definition: kinds.h:214
virtual Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
Definition: theory.h:365
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
Definition: expr.cpp:400
std::hash_map< Expr, Theorem > d_termTheorems
Map from active terms to theorems that introduced those terms.
Definition: theory_core.h:99
Definition: kinds.h:118
EffortLevel
Effort level for processFactQueue.
Definition: theory_core.h:258
static bool containsRec(const Expr &def, ExprHashMap< bool > &defs, ExprHashMap< bool > &visited)
_hash_table::iterator iterator
Definition: hash_map.h:106
void setRewriteNormal() const
Definition: expr.h:1457
void setFlag() const
Set the generic flag.
Definition: expr.h:1395
const std::string fixConstName(const std::string &s)
iterator end() const
Definition: cdmap.h:258
CDList< Expr > d_terms
List of all active terms in the system (for quantifier instantiation)
Definition: theory_core.h:96
void clear()
Definition: expr_map.h:175
Data structure of expressions in CVC3.
Definition: expr.h:133
void assertFormula(const Theorem &e)
Process a newly derived formula.
void computeType(const Expr &e)
Compute and store the type of e.
ExprHashMap< Theorem > d_varAssignments
Mapping of intermediate variables to their values.
Definition: theory_core.h:136
ExprManager * getEM() const
Definition: expr.h:1156
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Definition: kinds.h:75
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
CoreProofRules * createProofRules(TheoremManager *tm)
Private method to get a new theorem producer.
An exception thrown by the parser.
PrettyPrinterCore(TheoryCore *core)
Constructor.
Definition: theory_core.cpp:55
static bool contains(const Expr &def, ExprHashMap< bool > &defs)
unsigned d_timeBase
Time limit (0==unlimited, >0==total available cpu time in seconds).
Definition: theory_core.h:163
Expr processCond(const Expr &e, int i)
An auxiliary recursive function to process COND expressions into ITE.
const CLFlags & getFlags() const
Definition: theory_core.h:350
void enqueueFact(const Theorem &e)
Enqueue a new fact.
bool isTrue() const
Definition: expr.h:356
CoreProofRules * d_rules
Core proof rules.
Definition: theory_core.h:63
void computeType(const Expr &e)
Compute the type of e.
Definition: theory_core.cpp:74
void addToVarDB(const Expr &e)
Adds expression to var database.
bool hasTheory(int kind)
Test whether a kind maps to any theory.
Definition: theory.cpp:247
void setStoredPredicate() const
Set the Stored Predicate flag for this Expr.
Definition: expr.h:1538
Definition: kinds.h:241
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
Definition: expr.cpp:517
virtual Theorem rewriteIteToIff(const Expr &e)=0
==> ITE(a, b, !b) IFF IFF(a, b)
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
Definition: expr_map.h:194
Definition: kinds.h:227
Definition: kinds.h:105
unsigned size() const
Definition: notifylist.h:39
Definition: kinds.h:225
bool isStoredPredicate() const
Definition: expr.h:1386
const Expr & boolExpr()
BOOLEAN Expr.
Definition: expr_manager.h:276
Definition: kinds.h:84
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
Definition: theorem.cpp:274
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
Definition: theory.cpp:816
std::string d_name
Name of the theory (for debugging)
Definition: theory.h:70
ExprStream & print(ExprStream &os, const Expr &e)
The pretty-printer which subclasses must implement.
Definition: theory_core.cpp:56
bool isFalse() const
Definition: expr.h:355
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
Definition: theory.cpp:887
virtual Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
Definition: theory.h:275
Definition: kinds.h:136
void setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)
Helper for registerAtom.
bool isImpliedLiteral() const
Definition: expr.h:1350
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
virtual Theorem rewriteIteCond(const Expr &e)=0
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
void setFind(const Theorem &e) const
Set the find attribute to e.
Definition: expr.h:1405
for output in TPTP format
Definition: lang.h:46
void insert(const Key &k, const Data &d, int scope=-1)
Definition: cdmap.h:190
void unregisterPrettyPrinter()
Tell ExprManager that the printer is no longer valid.
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
SMT-LIB v2 format.
Definition: lang.h:52
ContextManager * d_cm
Context manager.
Definition: theory_core.h:57
STL namespace.
Definition: kinds.h:85
CDList< Theorem > d_impliedLiterals
List of implied literals, based on registered atomic formulas of interest.
Definition: theory_core.h:186
void initTimeLimit()
Initialize base time used for !setTimeLimit.
virtual Theorem iffFalseElim(const Theorem &e)=0
Lisp-like format for automatically generated specs.
Definition: lang.h:36
Definition: kinds.h:66
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Definition: expr.h:1265
Generally Useful Expression Transformations.
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
Expr getExpr(int i) const
Definition: notifylist.h:42
virtual Theorem rewriteIteToAnd(const Expr &e)=0
==> ITE(a, b, FALSE) IFF AND(a, b)
bool isBool() const
Definition: type.h:60
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Definition: theory.h:252
Theory * getTheory(int i) const
Definition: notifylist.h:41
Definition: kinds.h:123
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Definition: kinds.h:212
Definition: kinds.h:100
Definition: kinds.h:240
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Definition: expr.h:398
Definition: kinds.h:51
std::vector< std::pair< std::string, Expr > > d_boundVarStack
Bound variable stack: a vector of pairs
Definition: theory_core.h:109
virtual Theorem reflexivityRule(const Expr &a)=0
void registerPrettyPrinter(PrettyPrinter &printer)
Register the pretty-printer (can only do it if none registered)
bool incomplete()
Check if the current decision branch is marked as incomplete.
Definition: theory_core.h:435
Expr parseExpr(const Expr &e)
Parse the generic expression.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
Definition: theory.h:719
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
bool inUserAssumption() const
Definition: expr.h:1358
bool isType() const
Expr represents a type.
Definition: expr.h:1020
Definition: kinds.h:56
Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool inconsistent()
Check if the current context is inconsistent.
Definition: theory_core.h:422
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
bool hasFind() const
Definition: expr.h:1232
int getScope() const
Definition: theorem.cpp:486
unsigned getQuantLevelForTerm(const Expr &e)
Get quantification level at which this term was introduced.
Definition: kinds.h:96
void registerTypeComputer(TypeComputer *typeComputer)
Register type computer.
Definition: expr_manager.h:344
bool isOr() const
Definition: expr.h:422
Theorem callTheoryPreprocess(const Expr &e)
Call theory-specific preprocess routines.
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
IF_DEBUG(static bool hasBoundVar(const Expr &e){e.getEM() ->clearFlags();return hasBoundVarRec(e);}) void TheoryCore
iterator find(const key_type &key)
operations
Definition: hash_map.h:171
CDMap< std::string, bool > d_incomplete
The set of reasons for incompleteness (empty when we are complete)
Definition: theory_core.h:91
Definition: kinds.h:97
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Definition: theory.h:172
virtual void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: theory.h:236
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Definition: theory.cpp:203
std::vector< Theory * > d_theories
Array of registered theories.
Definition: theory_core.h:125
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
void setValidType() const
Definition: expr.h:1438
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
TypeComputerCore(TheoryCore *core)
Definition: theory_core.cpp:73
const Expr & getExpr() const
Definition: type.h:52
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
Definition: theory.h:714
Definition: kinds.h:130
bool checkSATCore()
To be called by SearchEngine when it believes the context is satisfiable.
bool isNot() const
Definition: expr.h:420
ExprTransform * d_exprTrans
Expr Transformer.
Definition: theory_core.h:78
bool isClosure() const
Definition: expr.h:1007
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
Definition: kinds.h:242
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem getImpliedLiteralByIndex(unsigned index)
Return an implied literal by index.
void getResource()
Request a unit of resource.
Definition: theory_core.h:334
Implementation of PrettyPrinter class.
Definition: theory_core.cpp:48
std::vector< Theorem > d_update_thms
List of theorems from calls to update()
Definition: theory_core.h:194
virtual Theorem rewriteIteToOr(const Expr &e)=0
==> ITE(a, TRUE, b) IFF OR(a, b)
virtual Theorem iffTrue(const Theorem &e)=0
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Definition: kinds.h:44
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
NotifyList d_notifyEq
Notify list that gets processed on every equality.
Definition: theory_core.h:200
ExprHashMap< Theorem > d_simplifiedModelVars
Mapping of basic variables to simplified expressions (temp. storage)
Definition: theory_core.h:145
void assignValue(const Expr &t, const Expr &val)
Assign t a concrete value val. Used in model generation.
Theorem simplify(const Expr &e)
Top-level simplifier.
bool d_theoryUsed
Definition: theory.h:79
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
int arity() const
Definition: type.h:55
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
CommonProofRules * getRules() const
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
Definition: kinds.h:76
std::string toString() const
Definition: theorem.h:404
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Definition: theory_core.h:120
Abstract class for computing expr type.
Definition: expr_manager.h:183
bool isString() const
Definition: expr.h:1006
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Definition: theory.h:334
virtual Theorem rewriteIteToNot(const Expr &e)=0
==> ITE(e, FALSE, TRUE) IFF NOT(e)
ExprStream & pushRestore(ExprStream &os)
Set the indentation to the position saved by popSave()
Expr getAssignment()
Get the value of all :named terms.
virtual void computeType(const Expr &e)
Compute and store the type of e.
Definition: theory.h:263
Definition: kinds.h:145
Definition: kinds.h:101
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
void setImpliedLiteral() const
Definition: expr.h:1493
bool validSimpCache() const
Return true if there is a valid cached value for calling simplify on this Expr.
Definition: expr.h:1294
virtual Theorem rewriteIteSame(const Expr &e)=0
==> ITE(c, e, e) == e
virtual void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Definition: theory.h:127
static bool hasBoundVarRec(const Expr &e)
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Definition: theory.h:292
const Theorem & getEqNext() const
Definition: expr.h:1247
Definition: kinds.h:102
unsigned getQuantLevel() const
Return quantification level for this theorem.
Definition: theorem.cpp:491
Definition: kinds.h:193
const Theorem & getSimpCache() const
Definition: expr.h:1298
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
CoreSatAPI * d_coreSatAPI
Definition: theory_core.h:240
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
ExprManager::TypeComputer * d_typeComputer
Type Computer.
Definition: theory_core.h:75
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
virtual Theorem rewriteIteToImp(const Expr &e)=0
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Expr negate() const
Definition: expr.h:937
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Definition: kinds.h:68
bool isBoolConst() const
Definition: expr.h:357
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
const Expr & unnegate() const
Remove leading NOT if any.
Definition: expr.h:506
virtual Theorem typePred(const Expr &e)=0
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
void collectModelValues(const Expr &e, ExprMap< Expr > &m)
Recursively build a compound-type variable assignment for e.
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
void clearRewriteNormal() const
Definition: expr.h:1543
std::string int2string(int n)
Definition: cvc_util.h:46
virtual Theorem rewriteAndSubterms(const Expr &e, int idx)=0
(a & b) <=> a & b[a/true]; takes the index of a
CDO< Theorem > d_incThm
Proof of inconsistent.
Definition: theory_core.h:94
const Expr & getRHS() const
Definition: theorem.cpp:246
const std::string & getName() const
Get the name of the theory (for debugging purposes)
Definition: theory.h:99
size_t size() const
Definition: cdmap.h:171
Definition: kinds.h:58
Theorem rewriteCore(const Theorem &e)
Transitive composition of other rewrites with the above.
bool isNull() const
Definition: type.h:59
Definition: kinds.h:98
Definition: kinds.h:131
void collectBasicVars()
Split compound vars into basic type variables.
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
Definition: theory.cpp:406
std::string toString() const
Definition: type.h:80
void setRegisteredAtom() const
Set the RegisteredAtom flag for this Expr.
Definition: expr.h:1528
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
const Expr & falseExpr()
Return FALSE Expr.
Definition: theory.h:579
Definition: kinds.h:62
const Expr & trueExpr()
Return TRUE Expr.
Definition: theory.h:582
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
Definition: theory.cpp:709
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
virtual ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Definition: theory.h:302
void clearFlags()
Clears the generic Expr flag in all Exprs.
Definition: expr_manager.h:272
Expression Manager.
Definition: expr_manager.h:58
Expr notExpr() const
Definition: expr.h:933
Definition: kinds.h:71
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
Definition: theory_core.h:111
virtual void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
Definition: theory.h:350
bool usesCC() const
Definition: expr.h:1342
Expr getExpr() const
Definition: theorem.cpp:230
void setSimpCache(const Theorem &e) const
Definition: expr.h:1432
bool isNull() const
Definition: theorem.h:164
const std::string quoteAnnotation(const std::string &s)
bool isApply() const
Definition: expr.h:1014
std::vector< Expr > d_basicModelVars
List of basic variables (temporary storage for model generation)
Definition: theory_core.h:138
NotifyList * getNotify() const
Definition: expr.h:1254
bool getFlag() const
Check if the generic flag is set.
Definition: expr.h:1390
static Type anyType(ExprManager *em)
Definition: type.h:74
virtual Theorem rewriteDistinct(const Expr &e)=0
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
void checkEquation(const Theorem &thm)
Helper check functions for solve.
Definition: kinds.h:90
CDO< unsigned > d_impliedLiteralsIdx
Next index in d_impliedLiterals that has not yet been fetched.
Definition: theory_core.h:189
Expr getValue(Expr e)
Get the value of an arbitrary formula or term.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: kinds.h:69
void getModelTerm(const Expr &e, std::vector< Expr > &v)
Calls the correct theory to get all of the terms that need to be assigned values in the concrete mode...
Definition: theory.cpp:527
const std::string & getName() const
Definition: expr.h:1050
void setInconsistent(const Theorem &e)
Definition: kinds.h:94
bool processFactQueue(EffortLevel effort=NORMAL)
A helper function for addFact()
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
virtual Theorem rewriteLetDecl(const Expr &e)=0
Replace LETDECL with its definition.
virtual Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Definition: theory.h:159
virtual Theorem solve(const Theorem &e)
An optional solver.
Definition: theory.h:204
ContextManager * getCM() const
Definition: theory_core.h:348
unsigned d_timeLimit
Definition: theory_core.h:164
virtual void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
Definition: theory.h:206
Translator * d_translator
Translator.
Definition: theory_core.h:81
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
Definition: kinds.h:77
bool isRegisteredAtom() const
Definition: expr.h:1378
Definition: kinds.h:246
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
PrettyPrinterCore()
Disable the default constructor.
Definition: theory_core.cpp:52
bool isQuantifier() const
Definition: expr.h:1008
Theorem preprocess(const Expr &e)
virtual Theorem xorToIff(const Expr &e)=0
virtual Theorem simplifyOp(const Expr &e)
Recursive simplification step.
Definition: theory.cpp:53
bool findReduced(const Expr &e)
Return true iff e is find-reduced.
Definition: theory.cpp:357
int getNumTheories()
Return the number of registered theories.
Definition: theory.cpp:241
Definition: kinds.h:276
Type boolType()
Return BOOLEAN type.
Definition: theory.h:576
bool isVar() const
Definition: expr.h:1005
Theorem getTheoremForTerm(const Expr &e)
Get theorem which was responsible for introducing this term.
std::string to_lower(const std::string &src)
Definition: cvc_util.h:38
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
std::string to_upper(const std::string &src)
Definition: cvc_util.h:30
ExprHashMap< std::vector< Expr > > d_varModelMap
Mapping of compound type variables to simpler types (model generation)
Definition: theory_core.h:134
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Definition: theory.h:189
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
Definition: kinds.h:95
An exception to be thrown by the smtlib translator.
iterator find(const Expr &e)
Definition: expr_map.h:329
An exception to be thrown by the smtlib translator.
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
Theorem typePred(const Expr &e)
Return a theorem for the type predicate of e.
SMT-LIB format.
Definition: lang.h:34
Definition: kinds.h:125
Proof rules used by theory_core.
bool outOfResources()
Return true if resources are exhausted.
Definition: theory_core.h:492
Definition of the API to expression package. See class Expr for details.
const std::string escapeSymbol(const std::string &s)
ExprManager * d_em
Definition: theory.h:67
virtual Theorem rewriteIff(const Expr &e)=0
==> (e1 <=> e2) <=> [simplified expr]
bool isRefl() const
Definition: theorem.h:171
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
Definition: theory_core.h:425
void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: theory_core.cpp:82
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
void assertEqualities(const Theorem &e)
Assert a system of equations (1 or more).
Op mkOp() const
Make the expr into an operator.
Definition: expr.h:1178
const Expr & getLHS() const
Definition: theorem.cpp:240
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
Definition: expr.h:1416
ExprMap< Expr > d_parseCacheTop
Top-level cache for parser.
Definition: theory_core.h:114
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
Definition: theory.cpp:367
Definition: kinds.h:93
Definition: kinds.h:53
bool isRewriteNormal() const
Definition: expr.h:1322
Definition: kinds.h:81
Definition: kinds.h:63
std::vector< Theorem > d_queueSE
Queue of facts to be sent to the SearchEngine.
Definition: theory_core.h:86
virtual Theorem rewriteOrSubterms(const Expr &e, int idx)=0
(a | b) <=> a | b[a/false]; takes the index of a
iterator begin() const
Definition: cdmap.h:257
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
Definition: theory.cpp:923
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
Definition: expr_manager.h:341
virtual Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
Definition: theory.h:164
Definition: kinds.h:61
CDList< Expr > d_predicates
List of all active non-equality atomic formulas in the system (for quantifier instantiation) ...
Definition: theory_core.h:103
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.
Definition: theory_core.cpp:89
std::queue< Theorem > d_queue
Assertion queue.
Definition: theory_core.h:84
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Definition: theory.h:724
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition: theory.h:686
CommonProofRules * d_commonRules
Commonly used proof rules.
Definition: theory.h:69
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Definition: kinds.h:213
void processNotify(const Theorem &e, NotifyList *L)
Process a notify list triggered as a result of new theorem e.
ExprIndex getIndex() const
Definition: expr.h:1173
PrettyPrinter * d_printer
PrettyPrinter (we own it)
Definition: theory_core.h:72
Definition: kinds.h:124
bool okToEnqueue()
Whether its OK to add new facts (for use in rewrites)
Definition: theory_core.h:377
bool isReal(Type t)
Definition: theory_arith.h:173
const std::string & getString() const
Definition: expr.h:1055
Definition: kinds.h:50
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Definition: kinds.h:129
Definition: expr.cpp:35
Definition: kinds.h:99
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Definition: theory.cpp:252
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isRewrite() const
Definition: theorem.cpp:224
InputLanguage lang() const
Get the current output language.
Definition: expr_stream.h:165
bool isFunction() const
Definition: type.h:62
void setFindLiteral(const Theorem &thm)
Set the find pointer of an atomic formula and notify SearchEngine.
Definition: kinds.h:217
Definition: kinds.h:229
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
~TheoryCore()
Destructor.
std::vector< Expr > d_vars
List of variables that were created up to this point.
Definition: theory_core.h:105
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;...
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
void update(const Theorem &e, const Expr &d)
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Definition: kinds.h:67
Theorem solve(const Theorem &e)
std::vector< std::pair< Expr, Expr > > d_assignment
The set of named expressions to evaluate on a GET_ASSIGNMENT request.
Definition: theory_core.h:206
for output into Simplify format
Definition: lang.h:43
virtual Theorem andElim(const Theorem &e, int i)=0
virtual Theorem addAssumption(const Expr &assump)=0
Add an assumption to the set of assumptions in the current context.
std::vector< Expr > d_update_data
List of data accompanying above theorems from calls to update()
Definition: theory_core.h:197
Abstract API to a pretty-printer for Expr.
Definition: kinds.h:106
A class which sets a boolean value to true when created, and resets to false when deleted...
Definition: cvc_util.h:108
virtual Theorem rewriteImplies(const Expr &e)=0
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
bool isBasicKind(int kind)
Return true if no special parsing is required for this kind.
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.
Definition: kinds.h:70
Nice SAL-like language for manually written specs.
Definition: lang.h:32
virtual Theorem iffTrueElim(const Theorem &e)=0
Theorem rewriteLitCore(const Expr &e)
Core rewrites for literals (NOT and EQ)
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
iterator end()
Definition: hash_map.h:257
void checkSolved(const Theorem &thm)
Helper check functions for solve.
iterator end()
Definition: expr_map.h:326
void setTimeLimit(unsigned limit)
Set the time limit in seconds (0==unlimited).
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421