CVC3  2.4.1
theory.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Jan 30 15:11:55 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "theory_core.h"
23 #include "common_proof_rules.h"
24 #include "typecheck_exception.h"
25 #include "theorem_manager.h"
26 #include "command_line_flags.h"
27 
28 
29 using namespace CVC3;
30 using namespace std;
31 
32 
33 Theory::Theory(void) : d_theoryCore(NULL) { }
34 
35 
36 Theory::Theory(TheoryCore* theoryCore, const string& name)
37  : d_em(theoryCore->getEM()),
38  d_theoryCore(theoryCore),
39  d_commonRules(theoryCore->getTM()->getRules()),
40  d_name(name), d_theoryUsed(false) {
41 }
42 
43 
44 Theory::~Theory(void) { }
45 
46 
47 void Theory::computeModelTerm(const Expr& e, vector<Expr>& v) {
48  TRACE("model", "Theory::computeModelTerm(", e, "): is a variable");
49  // v.push_back(e);
50 }
51 
52 
54  int ar = e.arity();
55  if (ar > 0) {
56  if (ar == 1) {
57  Theorem res = d_theoryCore->simplify(e[0]);
58  if (!res.isRefl()) {
59  return d_commonRules->substitutivityRule(e, res);
60  }
61  }
62  else {
63  vector<Theorem> newChildrenThm;
64  vector<unsigned> changed;
65  for(int k = 0; k < ar; ++k) {
66  // Recursively simplify the kids
67  Theorem thm = d_theoryCore->simplify(e[k]);
68  if (!thm.isRefl()) {
69  newChildrenThm.push_back(thm);
70  changed.push_back(k);
71  }
72  }
73  if(changed.size() > 0)
74  return d_commonRules->substitutivityRule(e, changed, newChildrenThm);
75  }
76  }
77  return reflexivityRule(e);
78 }
79 
80 
82  vector<Expr> kids;
83  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
84  kids.push_back(getTCC(*i));
85  return (kids.size() == 0) ? trueExpr() :
86  (kids.size() == 1) ? kids[0] :
88 }
89 
90 
91 void Theory::registerAtom(const Expr& e, const Theorem& thm)
92 {
93  d_theoryCore->registerAtom(e, thm);
94 }
95 
96 
98 {
99  return d_theoryCore->inconsistent();
100 }
101 
102 
104 {
105  // TRACE("facts assertFact", ("setInconsistent[" + getName() + "->]("), e, ")");
106  // TRACE("conflict", ("setInconsistent[" + getName() + "->]("), e, ")");
107  IF_DEBUG(debugger.counter("conflicts from DPs")++;)
109 }
110 
111 
112 void Theory::setIncomplete(const string& reason)
113 {
114  // TRACE("facts assertFact", "setIncomplete["+getName()+"](", reason, ")");
115  d_theoryCore->setIncomplete(reason);
116 }
117 
118 
120 {
121  // TRACE("simplify", ("simplify[" + getName() + "->]("), e, ") {");
122  Theorem res(d_theoryCore->simplify(e));
123  // TRACE("simplify", "simplify[" + getName() + "] => ", res, "}");
124  return res;
125 }
126 
127 
129 {
130  // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
132 }
133 
135 {
136  // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
138 }
139 
140 
141 
143 {
145 }
146 
147 
148 void Theory::addSplitter(const Expr& e, int priority) {
149  TRACE("facts assertFact", "addSplitter[" + getName() + "->](", e,
150  ", pri="+int2string(priority)+")");
151  // DebugAssert(simplifyExpr(e) == e, "Expected splitter to be simplified");
152  DebugAssert(e.isAbsLiteral() && !e.isBoolConst(), "Expected literal");
153  d_theoryCore->d_coreSatAPI->addSplitter(e, priority);
154 }
155 
156 
157 void Theory::addGlobalLemma(const Theorem& thm, int priority) {
158  d_theoryCore->d_coreSatAPI->addLemma(thm, priority, true);
159 }
160 
161 
162 void Theory::assignValue(const Expr& t, const Expr& val) {
163  TRACE("facts assertFact", "assignValue["+getName()+"](", t, ", "+
164  val.toString()+") {");
165  d_theoryCore->assignValue(t, val);
166  TRACE("facts assertFact", "assignValue[", getName(), "] => }");
167 }
168 
169 
170 void Theory::assignValue(const Theorem& thm) {
171  TRACE("facts assertFact", "assignValue["+getName()+"](", thm, ") {");
173  TRACE("facts assertFact", "assignValue[", getName(), "] => }");
174 }
175 
176 
177 void Theory::registerKinds(Theory* theory, vector<int>& kinds)
178 {
179  vector<int>::const_iterator k;
180  vector<int>::const_iterator kEnd;
181  for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
183  "kind already registered: "+getEM()->getKindName(*k)
184  +" = "+int2string(*k));
185  d_theoryCore->d_theoryMap[*k] = theory;
186  }
187 }
188 
189 
190 void Theory::unregisterKinds(Theory* theory, vector<int>& kinds)
191 {
192  vector<int>::const_iterator k;
193  vector<int>::const_iterator kEnd;
194  for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
195  DebugAssert(d_theoryCore->d_theoryMap[*k] == theory,
196  "kind not registered: "+getEM()->getKindName(*k)
197  +" = "+int2string(*k));
199  }
200 }
201 
202 
203 void Theory::registerTheory(Theory* theory, vector<int>& kinds,
204  bool hasSolver)
205 {
206  registerKinds(theory, kinds);
207  unsigned i = 0;
208  for (; i < d_theoryCore->d_theories.size(); ++i) {
209  if (d_theoryCore->d_theories[i] == NULL) {
210  d_theoryCore->d_theories[i] = theory;
211  break;
212  }
213  }
214  if (i == d_theoryCore->d_theories.size()) {
215  d_theoryCore->d_theories.push_back(theory);
216  }
217  if (hasSolver) {
218  DebugAssert(!d_theoryCore->d_solver,"Solver already registered");
219  d_theoryCore->d_solver = theory;
220  }
221 }
222 
223 
224 void Theory::unregisterTheory(Theory* theory, vector<int>& kinds,
225  bool hasSolver)
226 {
227  unregisterKinds(theory, kinds);
228  unsigned i = 0;
229  for (; i < d_theoryCore->d_theories.size(); ++i) {
230  if (d_theoryCore->d_theories[i] == theory) {
231  d_theoryCore->d_theories[i] = NULL;
232  }
233  }
234  if (hasSolver) {
235  DebugAssert(d_theoryCore->d_solver == theory, "Solver not registered");
236  d_theoryCore->d_solver = NULL;
237  }
238 }
239 
240 
242 {
243  return d_theoryCore->d_theories.size();
244 }
245 
246 
247 bool Theory::hasTheory(int kind) {
248  return (d_theoryCore->d_theoryMap.count(kind) > 0);
249 }
250 
251 
253 {
255  "Unknown operator: " + getEM()->getKindName(kind));
256  return d_theoryCore->d_theoryMap[kind];
257 }
258 
259 
261 {
262  const Expr& typeExpr = getBaseType(e).getExpr();
263  DebugAssert(!typeExpr.isNull(),"Null type");
264  int kind = typeExpr.getOpKind();
266  "Unknown operator: " + getEM()->getKindName(kind));
267  return d_theoryCore->d_theoryMap[kind];
268 }
269 
270 
272 {
273  Expr e2(e);
274  while (e2.isNot() || e2.isEq()) {
275  e2 = e2[0];
276  }
277  if (e2.isApply()) {
278  return d_theoryCore->d_theoryMap[e2.getOpKind()];
279  }
280  if (!e2.isVar()) {
281  return d_theoryCore->d_theoryMap[e2.getKind()];
282  }
283  // Theory of a var is determined by its *base* type, since SUBTYPE
284  // may have different base types, but SUBTYPE itself belongs to
285  // TheoryCore.
286  const Expr& typeExpr = getBaseType(e2).getExpr();
287  DebugAssert(!typeExpr.isNull(),"Null type");
288  int kind = typeExpr.getOpKind();
290  "Unknown operator: " + getEM()->getKindName(kind));
291  return d_theoryCore->d_theoryMap[kind];
292 }
293 
294 
295 const Theorem& Theory::findRef(const Expr& e)
296 {
297  DebugAssert(e.hasFind(), "expected find");
298  const Theorem& thm1 = e.getFind();
299  if (thm1.isRefl()) return thm1;
300  const Expr& e1 = thm1.getRHS();
301  if (!e1.hasFind() || e1.getFind().getRHS() == e1) return thm1;
302  const Theorem& thm2 = findRef(e1);
303  DebugAssert(thm2.getLHS()==e1,"");
304  DebugAssert(thm2.getLHS() != thm2.getRHS(),"");
305  e.setFind(transitivityRule(thm1,thm2));
306  return e.getFind();
307 }
308 
309 
311 {
312  if (!e.hasFind()) return reflexivityRule(e);
313  const Theorem& thm1 = e.getFind();
314  if (thm1.isRefl()) return thm1;
315  const Expr& e1 = thm1.getRHS();
316  if (e1 == e || !e1.hasFind() ||
317  e1.getFind().getRHS() == e1) return thm1;
318  Theorem thm2 = find(e1);
319  DebugAssert(thm2.getLHS()==e1,"");
320  DebugAssert(thm2.getLHS() != thm2.getRHS(),"");
321  thm2 = transitivityRule(thm1,thm2);
322  e.setFind(thm2);
323  return thm2;
324 }
325 
326 
328 {
329  if (e.hasFind()) return find(e);
330  int ar = e.arity();
331  if (ar > 0) {
332  if (ar == 1) {
333  Theorem res = findReduce(e[0]);
334  if (!res.isRefl()) {
335  return d_commonRules->substitutivityRule(e, res);
336  }
337  }
338  else {
339  vector<Theorem> newChildrenThm;
340  vector<unsigned> changed;
341  for(int k = 0; k < ar; ++k) {
342  // Recursively reduce the kids
343  Theorem thm = findReduce(e[k]);
344  if (!thm.isRefl()) {
345  newChildrenThm.push_back(thm);
346  changed.push_back(k);
347  }
348  }
349  if(changed.size() > 0)
350  return d_commonRules->substitutivityRule(e, changed, newChildrenThm);
351  }
352  }
353  return reflexivityRule(e);
354 }
355 
356 
357 bool Theory::findReduced(const Expr& e)
358 {
359  if (e.hasFind())
360  return e.getFind().getRHS() == e;
361  for (Expr::iterator i = e.begin(), iend = e.end(); i != iend; ++i)
362  if (!findReduced(*i)) return false;
363  return true;
364 }
365 
366 
368 {
369  if(e.isVar()) return trueExpr();
371  if (itccCache != d_theoryCore->d_tccCache.end()) {
372  return (*itccCache).second;
373  }
374  Theory* i = theoryOf(e.getKind());
375  TRACE("tccs", "computeTCC["+i->getName()+"](", e, ") {");
376  Expr tcc = i->computeTCC(e);
377  d_theoryCore->d_tccCache[e] = tcc;
378  TRACE("tccs", "computeTCC["+i->getName()+"] => ", tcc, " }");
379  return tcc;
380 }
381 
382 
384 {
385  return getBaseType(e.getType());
386 }
387 
388 
390 {
391  const Expr& e = tp.getExpr();
392  DebugAssert(!e.isNull(), "Theory::getBaseType(Type(Null))");
393  // See if we have it cached
394  Type res(e.lookupType());
395  if(!res.isNull()) return res;
396 
397  DebugAssert(theoryOf(e) != NULL,
398  "Theory::getBaseType(): No theory for the type: "
399  +tp.toString());
400  res= theoryOf(e)->computeBaseType(tp);
401  e.setType(res);
402  return res;
403 }
404 
405 
406 Expr Theory::getTypePred(const Type& t, const Expr& e)
407 {
408  Expr pred;
409  Theory *i = theoryOf(t.getExpr().getKind());
410  // TRACE("typePred", "computeTypePred["+i->getName()+"]("+t.toString()+", ", e, ") {");
411  pred = i->computeTypePred(t, e);
412  // TRACE("typePred", "computeTypePred["+i->getName()+"] => ", pred, " }");
413  return pred;
414 }
415 
416 
418 {
419  int ar = e.arity();
420  switch (ar) {
421  case 0:
422  break;
423  case 1: {
424  const Theorem& res = findRef(e[0]);
425  if (res.getLHS() != res.getRHS()) {
426  return d_commonRules->substitutivityRule(e, res);
427  }
428  break;
429  }
430  case 2: {
431  const Theorem thm0 = findRef(e[0]);
432  const Theorem thm1 = findRef(e[1]);
433  if (thm0.getLHS() != thm0.getRHS() ||
434  thm1.getLHS() != thm1.getRHS()) {
435  return d_commonRules->substitutivityRule(e, thm0, thm1);
436  }
437  break;
438  }
439  default: {
440  vector<Theorem> newChildrenThm;
441  vector<unsigned> changed;
442  for (int k = 0; k < ar; ++k) {
443  const Theorem& thm = findRef(e[k]);
444  if (thm.getLHS() != thm.getRHS()) {
445  newChildrenThm.push_back(thm);
446  changed.push_back(k);
447  }
448  }
449  if (changed.size() > 0)
450  return d_commonRules->substitutivityRule(e, changed, newChildrenThm);
451  break;
452  }
453  }
454  return reflexivityRule(e);
455 }
456 
457 
458 //! Setup a term for congruence closure (must have sig and rep attributes)
459 void Theory::setupCC(const Expr& e) {
460  // TRACE("facts setup", "setupCC["+getName()+"](", e, ") {");
461  for (int k = 0; k < e.arity(); ++k) {
462  e[k].addToNotify(this, e);
463  }
464  Theorem thm = reflexivityRule(e);
465  e.setSig(thm);
466  e.setRep(thm);
467  e.setUsesCC();
468  // TRACE_MSG("facts setup", "setupCC["+getName()+"]() => }");
469 }
470 
471 
472 //! Update a term w.r.t. congruence closure (must be setup with setupCC())
473 void Theory::updateCC(const Theorem& e, const Expr& d) {
474  // TRACE("facts update", "updateCC["+getName()+"]("+e.getExpr().toString()+", ",
475  // d, ") {");
476  int k, ar(d.arity());
477  const Theorem& dEQdsig = d.getSig();
478  if (!dEQdsig.isNull()) {
479  const Expr& dsig = dEQdsig.getRHS();
480  Theorem thm = updateHelper(d);
481  const Expr& sigNew = thm.getRHS();
482  if (sigNew == dsig) {
483  // TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
484  return;
485  }
486  dsig.setRep(Theorem());
487  const Theorem& repEQsigNew = sigNew.getRep();
488  if (!repEQsigNew.isNull()) {
489  d.setSig(Theorem());
490  enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
491  }
492  else if (d.getType().isBool()) {
493  d.setSig(Theorem());
494  enqueueFact(thm);
495  }
496  else {
497  for (k = 0; k < ar; ++k) {
498  if (sigNew[k] != dsig[k]) {
499  sigNew[k].addToNotify(this, d);
500  }
501  }
502  d.setSig(thm);
503  sigNew.setRep(thm);
505  }
506  }
507  // TRACE_MSG("facts update", "updateCC["+getName()+"]() => }");
508 }
509 
510 
511 //! Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
513  const Theorem& rep = e.getRep();
514  if (rep.isNull()) return reflexivityRule(e);
515  else return symmetryRule(rep);
516 }
517 
518 
520  // TRACE("facts parseExpr", "parseExpr(", e, ") {");
521  Expr res(d_theoryCore->parseExpr(e));
522  // TRACE("facts parseExpr", "parseExpr => ", res, " }");
523  return res;
524 }
525 
526 
527 void Theory::getModelTerm(const Expr& e, vector<Expr>& v)
528 {
529  Theory *i = theoryOf(getBaseType(e).getExpr());
530  TRACE("model", "computeModelTerm["+i->getName()+"](", e, ") {");
531  IF_DEBUG(unsigned size = v.size();)
532  i->computeModelTerm(e, v);
533  TRACE("model", "computeModelTerm[", i->getName(), "] => }");
534  DebugAssert(v.size() <= size || v.back() != e, "Primitive var was pushed on "
535  "the stack in computeModelTerm["+i->getName()
536  +"]: "+e.toString());
537 
538 }
539 
540 
542  return d_theoryCore->getModelValue(e);
543 }
544 
545 
546 bool Theory::isLeafIn(const Expr& e1, const Expr& e2)
547 {
548  DebugAssert(isLeaf(e1),"Expected leaf");
549  if (e1 == e2) return true;
550  if (theoryOf(e2) != this) return false;
551  for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i)
552  if (isLeafIn(e1, *i)) return true;
553  return false;
554 }
555 
556 
558 {
559  if (isLeaf(e)) {
560  return !e.hasFind() || e.getFind().getRHS() == e;
561  }
562  for (int k = 0; k < e.arity(); ++k) {
563  if (!leavesAreSimp(e[k])) return false;
564  }
565  return true;
566 }
567 
568 
569 Expr Theory::newVar(const string& name, const Type& type)
570 {
571  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
572  Expr res = resolveID(name);
573  Type t;
574 // Expr res = lookupVar(name, &t);
575  if (!res.isNull()) {
576  t = res.getType();
577  if (t != type) {
578  throw TypecheckException
579  ("incompatible redefinition of variable "+name+":\n "
580  "already defined with type: "+t.toString()
581  +"\n the new type is: "+type.toString());
582  }
583  return res;
584  }
585  // Replace TYPEDEF with its definition
586  t = type;
587  while(t.getExpr().getKind() == TYPEDEF) {
588  DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
589  t = t[1];
590  }
591  if (type.isBool()) res = d_em->newSymbolExpr(name, UCONST);
592  else res = getEM()->newVarExpr(name);
593 
594  // Add the variable for constructing a concrete model
595  d_theoryCore->addToVarDB(res);
596  // Add the new global declaration
597  installID(name, res);
598 
599  if( type.isFunction() ) {
600  throw Exception("newVar: expected non-function type");
601  }
602  if( !res.lookupType().isNull() ) {
603  throw Exception("newVarExpr: redefining a variable " + name);
604  }
605  res.setType(type);
606  return res;
607 }
608 
609 
610 Expr Theory::newVar(const string& name, const Type& type, const Expr& def)
611 {
612  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
613  Type t;
614  Expr res = resolveID(name);
615  if (!res.isNull()) {
616  throw TypecheckException
617  ("Redefinition of variable "+name+":\n "
618  "This variable is already defined.");
619  }
620  Expr v;
621 
622  // Replace TYPEDEF with its definition
623  t = type;
624  while(t.getExpr().getKind() == TYPEDEF) {
625  DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
626  t = t[1];
627  }
628 
629  // Typecheck
630  if(getBaseType(def) != getBaseType(t)) {
631  throw TypecheckException("Type mismatch in constant definition:\n"
632  "Constant "+name+
633  " is declared with type:\n "
634  +t.toString()
635  +"\nBut the type of definition is\n "
636  +def.getType().toString());
637  }
638  DebugAssert(t.getExpr().getKind() != ARROW,"");
639 
640  // Add the new global declaration
641  installID(name, def);
642 
643  return def;
644 }
645 
646 
647 Op Theory::newFunction(const string& name, const Type& type,
648  bool computeTransClosure) {
649  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
650  Expr res = resolveID(name);
651  Type t;
652  if (!res.isNull()) {
653  t = res.getType();
654  throw TypecheckException
655  ("Redefinition of variable "+name+":\n "
656  "already defined with type: "+t.toString()
657  +"\n the new type is: "+type.toString());
658  }
659  res = getEM()->newSymbolExpr(name, UFUNC);
660  // Replace TYPEDEF with its definition
661  t = type;
662  while(t.getExpr().getKind() == TYPEDEF) {
663  DebugAssert(t.arity() == 2, "Bad TYPEDEF: "+t.toString());
664  t = t[1];
665  }
666  res.setType(t);
667  // Add it to the database of variables for concrete model generation
668  d_theoryCore->addToVarDB(res);
669  // Add the new global declaration
670  installID(name, res);
671  if (computeTransClosure &&
672  t.isFunction() && t.arity() == 3 && t[2].isBool())
673  res.setComputeTransClosure();
674  return res.mkOp();
675 }
676 
677 
678 Op Theory::newFunction(const string& name, const Type& type,
679  const Expr& def) {
680  DebugAssert(!type.isNull(), "Error: defining a variable of NULL type");
681  Expr res = resolveID(name);
682  Type t;
683  if (!res.isNull()) {
684  t = res.getType();
685  throw TypecheckException
686  ("Redefinition of name "+name+":\n "
687  "already defined with type: "+t.toString()
688  +"\n the new type is: "+type.toString());
689  }
690 
691  // Add the new global declaration
692  installID(name, def);
693  return def.mkOp();
694 }
695 
696 
697 Op Theory::lookupFunction(const string& name, Type* type)
698 {
699  Expr e = getEM()->newSymbolExpr(name, UFUNC);
700  *type = e.lookupType();
701  if ((*type).isNull()) return Op();
702  return e.mkOp();
703 }
704 
705 
706 static int boundVarCount = 0;
707 
708 
709 Expr Theory::addBoundVar(const string& name, const Type& type) {
710  ostringstream ss;
711  ss << boundVarCount++;
712  Expr v(getEM()->newBoundVarExpr(name, ss.str(), type));
713  if (d_theoryCore->d_boundVarStack.size() == 0) {
715  "Parse cache invariant violated");
718  "Expected empty cache");
719  }
720  else {
722  "Parse cache invariant violated 2");
724  }
725  d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,v));
726  DebugAssert(v.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
728  if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
729  (*iBoundVarMap).second = Expr(RAW_LIST, v, (*iBoundVarMap).second);
730  }
731  else d_theoryCore->d_boundVarMap[name] = v;
732 
733  TRACE("vars", "addBoundVar("+name+", ", type, ") => "+v.toString());
734  return v;
735 }
736 
737 
738 Expr Theory::addBoundVar(const string& name, const Type& type,
739  const Expr& def) {
740  Expr res;
741  // Without the type, just replace the bound variable with the definition
742  if(type.isNull())
743  res = def;
744  else {
745  // When type is given, construct (LETDECL var, def) for the typechecker
746  ostringstream ss;
747  ss << boundVarCount++;
748  res = Expr(LETDECL,
749  getEM()->newBoundVarExpr(name, ss.str(), type), def);
750  }
751  if (d_theoryCore->d_boundVarStack.size() == 0) {
753  "Parse cache invariant violated");
756  "Expected empty cache");
757  }
758  else {
760  "Parse cache invariant violated 2");
762  }
763  d_theoryCore->d_boundVarStack.push_back(pair<string,Expr>(name,res));
764  DebugAssert(res.getKind() != RAW_LIST, "Bound vars cannot be bound to RAW_LIST");
766  if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
767  (*iBoundVarMap).second = Expr(RAW_LIST, res, (*iBoundVarMap).second);
768  }
769  else d_theoryCore->d_boundVarMap[name] = res;
770  TRACE("vars", "addBoundVar("+name+", "+type.toString()+", ", def,
771  ") => "+res.toString());
772  return res;
773 }
774 
775 
776 Expr Theory::lookupVar(const string& name, Type* type)
777 {
778  Expr e = getEM()->newVarExpr(name);
779  *type = e.lookupType();
780 // if ((*type).isNull()) {
781 // e = newApplyExpr(Op(UFUNC, e));
782 // *type = e.lookupType();
783  if ((*type).isNull()) return Expr();
784 // }
785  return e;
786 }
787 
788 
789 // TODO: reconcile this with parser-driven new type expressions
790 Type Theory::newTypeExpr(const string& name)
791 {
792  Expr res = resolveID(name);
793  if (!res.isNull()) {
794  throw TypecheckException
795  ("Redefinition of type variable "+name+":\n "
796  "This variable is already defined.");
797  }
798  res = Expr(TYPEDECL, getEM()->newStringExpr(name));
799  // Add the new global declaration
800  installID(name, res);
801  return Type(res);
802 }
803 
804 
805 Type Theory::lookupTypeExpr(const string& name)
806 {
807  Expr res = resolveID(name);
808  if (res.isNull() ||
809  (res.getKind() != TYPEDECL && !res.isType())) {
810  return Type();
811  }
812  return Type(res);
813 }
814 
815 
816 Type Theory::newSubtypeExpr(const Expr& pred, const Expr& witness)
817 {
818  Type predTp(pred.getType());
819  if(!predTp.isFunction() || predTp.arity() != 2)
820  throw TypecheckException
821  ("Expected unary predicate in the predicate subtype:\n\n "
822  +predTp.toString()
823  +"\n\nThe predicate is:\n\n "
824  +pred.toString());
825  if(!predTp[1].isBool())
826  throw TypecheckException
827  ("Range is not BOOLEAN in the predicate subtype:\n\n "
828  +predTp.toString()
829  +"\n\nThe predicate is:\n\n "
830  +pred.toString());
831  Expr p(simplifyExpr(pred));
832  // Make sure that the supplied predicate is total: construct
833  //
834  // FORALL (x: domType): getTCC(pred(x))
835  //
836  // This only needs to be done for LAMBDA-expressions, since
837  // uninterpreted predicates are defined for all the arguments
838  // of correct (exact) types.
839  if (pred.isLambda() && d_theoryCore->getFlags()["tcc"].getBool()) {
840  Expr quant = d_em->newClosureExpr(FORALL, p.getVars(),
841  d_theoryCore->getTCC(p.getBody()));
842  if (!d_theoryCore->d_coreSatAPI->check(quant)) {
843  throw TypecheckException
844  ("Subtype predicate could not be proved total in the following type:\n\n "
845  +Expr(SUBTYPE, p).toString()
846  +"\n\nThe failed TCC is:\n\n "
847  +quant.toString());
848  }
849  }
850  // We require that there exists an object of this type (otherwise there is an inherent inconsistency)
851  Expr q;
852  if (witness.isNull()) {
853  vector<Expr> vec;
854  vec.push_back(d_em->newBoundVarExpr(predTp[0]));
855  q = d_em->newClosureExpr(EXISTS, vec, simplifyExpr(Expr(pred.mkOp(), vec.back())));
856  }
857  else {
858  q = Expr(pred.mkOp(), witness);
859  }
860  if (!d_theoryCore->d_coreSatAPI->check(q)) {
861  throw TypecheckException
862  ("Unable to prove witness for subtype:\n\n "
863  +Expr(SUBTYPE, p).toString()
864  +"\n\nThe failed condition is:\n\n "
865  +q.toString());
866  }
867  return Type(Expr(SUBTYPE, p));
868 }
869 
870 
871 //! Create a new type abbreviation with the given name
872 Type Theory::newTypeExpr(const string& name, const Type& def)
873 {
874  Expr res = resolveID(name);
875  if (!res.isNull()) {
876  throw TypecheckException
877  ("Redefinition of type variable "+name+":\n "
878  "This variable is already defined.");
879  }
880  res = def.getExpr();
881  // Add the new global declaration
882  installID(name, res);
883  return Type(res);
884 }
885 
886 
887 Expr Theory::resolveID(const string& name) {
888  // TRACE("vars", "resolveID(", name, ") {");
889  Expr res; // Result is Null by default
890  // First, look up the bound variable stack
892  if (iBoundVarMap != d_theoryCore->d_boundVarMap.end()) {
893  res = (*iBoundVarMap).second;
894  if (res.getKind() == RAW_LIST) {
895  res = res[0];
896  }
897  }
898  else {
899  // Next, check in the globals
900  map<string,Expr>::iterator i=d_theoryCore->d_globals.find(name),
901  iend=d_theoryCore->d_globals.end();
902  if(i!=iend)
903  res = i->second;
904  }
905  // TRACE("vars", "resolveID => ", res, " }");
906  return res;
907 }
908 
909 
910 void Theory::installID(const string& name, const Expr& e)
911 {
912  DebugAssert(resolveID(name).isNull(),
913  "installID called on existing identifier");
914  d_theoryCore->d_globals[name] = e;
915 }
916 
917 
919  return d_theoryCore->typePred(e);
920 }
921 
922 
924 {
925  if (e[0].isTrue())
926  return d_commonRules->rewriteIteTrue(e);
927  if (e[0].isFalse())
928  return d_commonRules->rewriteIteFalse(e);
929  if (e[1] == e[2])
930  return d_commonRules->rewriteIteSame(e);
931  return reflexivityRule(e);
932 }
933 
934 
937  DebugAssert(thm.isRewrite() && thm.getRHS().isSkolem(),
938  "thm = "+thm.toString());
940  return thm;
941 }