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) {
182  DebugAssert(d_theoryCore->d_theoryMap.count(*k) == 0,
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));
198  d_theoryCore->d_theoryMap.erase(*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 {
254  DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
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();
265  DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
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();
289  DebugAssert(d_theoryCore->d_theoryMap.count(kind) > 0,
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 }
virtual Theorem simplify(const Expr &e)
Simplify a term e and return a Theorem(e==e')
Definition: theory.cpp:119
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
Definition: theory.cpp:519
int arity() const
Definition: expr.h:1201
bool isNull() const
Definition: expr.h:1223
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
bool leavesAreSimp(const Expr &e)
Test if all i-leaves of e are simplified.
Definition: theory.cpp:557
_hash_table::iterator iterator
Definition: hash_map.h:106
void clear()
Definition: expr_map.h:175
Data structure of expressions in CVC3.
Definition: expr.h:133
const Theorem & getFind() const
Definition: expr.h:1237
Theorem typePred(const Expr &e)
Return BOOLEAN type.
Definition: theory.cpp:918
void addSplitter(const Expr &e, int priority=0)
Suggest a splitter to the SearchEngine.
Definition: theory.cpp:148
bool isLeafIn(const Expr &e1, const Expr &e2)
Test if e1 is an i-leaf in e2.
Definition: theory.cpp:546
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
bool isLeaf(const Expr &e)
Test if e is an i-leaf term for the current theory.
Definition: theory.h:556
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
Definition: theory.cpp:142
virtual void setInconsistent(const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
Definition: theory.cpp:103
virtual void setIncomplete(const std::string &reason)
Mark the current decision branch as possibly incomplete.
Definition: theory.cpp:112
const CLFlags & getFlags() const
Definition: theory_core.h:350
void enqueueFact(const Theorem &e)
Enqueue a new fact.
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
Definition: theory.cpp:459
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 addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
Definition: expr.cpp:517
bool isSkolem() const
Definition: expr.h:432
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
Definition: expr_map.h:194
Definition: kinds.h:227
static int boundVarCount
Definition: theory.cpp:706
Expr newSymbolExpr(const std::string &s, int kind)
Definition: expr_manager.h:481
Definition: kinds.h:84
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
Definition: theory.cpp:816
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
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
void setFind(const Theorem &e) const
Set the find attribute to e.
Definition: expr.h:1405
MS C++ specific settings.
Definition: type.h:42
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Definition: theory.cpp:128
Base class for theories.
Definition: theory.h:64
virtual void addLemma(const Theorem &thm, int priority=0, bool atBottomScope=false)=0
Add a new lemma derived by theory core.
Definition: kinds.h:85
virtual Theorem rewriteAnd(const Expr &e)=0
==> AND(e1,e2) IFF [simplified expr]
ExprMap< Expr > d_tccCache
Cache for tcc's.
Definition: theory_core.h:122
virtual void enqueueSE(const Theorem &e)
Check if the current context is inconsistent.
Definition: theory.cpp:134
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Definition: expr.h:1265
bool isBool() const
Definition: type.h:60
void unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver)
Unregister a theory.
Definition: theory.cpp:224
void enqueueSE(const Theorem &thm)
Check if the current context is inconsistent.
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
Expr parseExpr(const Expr &e)
Parse the generic expression.
virtual bool check(const Expr &e)=0
Check the validity of e in the current context.
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isType() const
Expr represents a type.
Definition: expr.h:1020
Definition: kinds.h:56
bool inconsistent()
Check if the current context is inconsistent.
Definition: theory_core.h:422
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
bool hasFind() const
Definition: expr.h:1232
void registerKinds(Theory *theory, std::vector< int > &kinds)
Register new kinds with the given theory.
Definition: theory.cpp:177
void setRep(const Theorem &e) const
Definition: expr.h:1589
void setSig(const Theorem &e) const
Definition: expr.h:1578
void setUsesCC() const
Definition: expr.h:1483
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
virtual Theorem rewriteIteFalse(const Expr &e)=0
==> ITE(FALSE, e1, e2) == e2
virtual ~Theory(void)
Destructor.
Definition: theory.cpp:44
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
Theorem renameExpr(const Expr &e)
Derived rule to create a new name for an expression.
Definition: theory.cpp:935
const Expr & getExpr() const
Definition: type.h:52
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
Definition: theory.cpp:162
bool isNot() const
Definition: expr.h:420
std::map< std::string, Expr > d_globals
Database of declared identifiers.
Definition: theory_core.h:107
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
Definition: kinds.h:242
std::hash_map< int, Theory * > d_theoryMap
Array mapping kinds to theories.
Definition: theory_core.h:128
Type lookupTypeExpr(const std::string &name)
Lookup type by name. Return Null if no such type exists.
Definition: theory.cpp:805
Op newFunction(const std::string &name, const Type &type, bool computeTransClosure)
Create a new uninterpreted function.
Definition: theory.cpp:647
Definition: kinds.h:44
void addGlobalLemma(const Theorem &thm, int priority=0)
Add a global lemma.
Definition: theory.cpp:157
bool empty() const
Definition: expr_map.h:170
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.
virtual void addSplitter(const Expr &e, int priority)=0
Suggest a splitter to the Sat engine.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory.cpp:81
int arity() const
Definition: type.h:55
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
Definition: theorem.h:404
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Definition: theory_core.h:120
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:512
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Expr newVar(const std::string &name, const Type &type)
Create a new variable given its name and type.
Definition: theory.cpp:569
void unregisterKinds(Theory *theory, std::vector< int > &kinds)
Unregister kinds for a theory.
Definition: theory.cpp:190
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
const Theorem & getSig() const
Definition: expr.h:1560
virtual Theorem rewriteIteSame(const Expr &e)=0
==> ITE(c, e, e) == e
Definition: kinds.h:193
const Theorem & getRep() const
Definition: expr.h:1569
CoreSatAPI * d_coreSatAPI
Definition: theory_core.h:240
Definition: kinds.h:88
bool isBoolConst() const
Definition: expr.h:357
int getKind() const
Definition: expr.h:1168
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
Expr simplifyExpr(const Expr &e)
Simplify a term e w.r.t. the current context.
Definition: theory.h:430
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
const Theorem & findRef(const Expr &e)
Return the find as a reference: expr must have a find.
Definition: theory.cpp:295
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Definition: theory.cpp:541
Definition: kinds.h:58
bool isNull() const
Definition: type.h:59
Type newTypeExpr(const std::string &name)
Create a new uninterpreted type with the given name.
Definition: theory.cpp:790
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
#define IF_DEBUG(code)
Definition: debug.h:406
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
virtual Type computeBaseType(const Type &tp)
Compute the base type of the top-level operator of an arbitrary type.
Definition: theory.h:265
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
Definition: theory_core.h:111
virtual Theorem rewriteIteTrue(const Expr &e)=0
==> ITE(TRUE, e1, e2) == e1
void installID(const std::string &name, const Expr &e)
Install name as a new identifier associated with Expr e.
Definition: theory.cpp:910
bool isNull() const
Definition: theorem.h:164
bool isApply() const
Definition: expr.h:1014
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
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
void setInconsistent(const Theorem &e)
Theorem updateHelper(const Expr &e)
Update the children of the term e.
Definition: theory.cpp:417
Op lookupFunction(const std::string &name, Type *type)
Look up a function by name.
Definition: theory.cpp:697
void setType(const Type &t) const
Set the cached type.
Definition: expr.h:1427
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
Definition: theory.cpp:383
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
Definition: theory.cpp:473
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
Theorem findReduce(const Expr &e)
Return find-reduced version of e.
Definition: theory.cpp:327
int getNumTheories()
Return the number of registered theories.
Definition: theory.cpp:241
virtual bool inconsistent()
Check if the current context is inconsistent.
Definition: theory.cpp:97
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Definition: theory.cpp:47
bool isVar() const
Definition: expr.h:1005
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.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
ExprManager * d_em
Definition: theory.h:67
bool isRefl() const
Definition: theorem.h:171
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
Expr newVarExpr(const std::string &s)
Definition: expr_manager.h:478
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
virtual void registerAtom(const Expr &e, const Theorem &thm)
Definition: theory.cpp:91
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
Theorem reflexivityRule(const Expr &a)
==> a == a
Definition: theory.h:673
CommonProofRules * d_commonRules
Commonly used proof rules.
Definition: theory.h:69
Definition: kinds.h:99
Expr lookupVar(const std::string &name, Type *type)
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Definition: theory.cpp:776
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 isLambda() const
Definition: expr.h:1011
bool isRewrite() const
Definition: theorem.cpp:224
bool isFunction() const
Definition: type.h:62
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
Definition: theory.cpp:310
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
ExprMap< Expr > d_parseCacheOther
Alternative cache for parser when not at top-level.
Definition: theory_core.h:118
Theory(void)
Private default constructor.
Definition: theory.cpp:33
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Definition: theory.h:677
iterator end() const
End iterator.
Definition: expr.h:1217