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
Theory(void)33 Theory::Theory(void) : d_theoryCore(NULL) { }
34
35
Theory(TheoryCore * theoryCore,const string & name)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
~Theory(void)44 Theory::~Theory(void) { }
45
46
computeModelTerm(const Expr & e,vector<Expr> & v)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
simplifyOp(const Expr & e)53 Theorem Theory::simplifyOp(const Expr& e) {
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
computeTCC(const Expr & e)81 Expr Theory::computeTCC(const Expr& e) {
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] :
87 d_commonRules->rewriteAnd(andExpr(kids)).getRHS();
88 }
89
90
registerAtom(const Expr & e,const Theorem & thm)91 void Theory::registerAtom(const Expr& e, const Theorem& thm)
92 {
93 d_theoryCore->registerAtom(e, thm);
94 }
95
96
inconsistent()97 bool Theory::inconsistent()
98 {
99 return d_theoryCore->inconsistent();
100 }
101
102
setInconsistent(const Theorem & e)103 void Theory::setInconsistent(const Theorem& e)
104 {
105 // TRACE("facts assertFact", ("setInconsistent[" + getName() + "->]("), e, ")");
106 // TRACE("conflict", ("setInconsistent[" + getName() + "->]("), e, ")");
107 IF_DEBUG(debugger.counter("conflicts from DPs")++;)
108 d_theoryCore->setInconsistent(e);
109 }
110
111
setIncomplete(const string & reason)112 void Theory::setIncomplete(const string& reason)
113 {
114 // TRACE("facts assertFact", "setIncomplete["+getName()+"](", reason, ")");
115 d_theoryCore->setIncomplete(reason);
116 }
117
118
simplify(const Expr & e)119 Theorem Theory::simplify(const Expr& e)
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
enqueueFact(const Theorem & e)128 void Theory::enqueueFact(const Theorem& e)
129 {
130 // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
131 d_theoryCore->enqueueFact(e);
132 }
133
enqueueSE(const Theorem & e)134 void Theory::enqueueSE(const Theorem& e)
135 {
136 // TRACE("facts assertFact", ("enqueueFact[" + getName() + "->]("), e, ")");
137 d_theoryCore->enqueueSE(e);
138 }
139
140
141
assertEqualities(const Theorem & e)142 void Theory::assertEqualities(const Theorem& e)
143 {
144 d_theoryCore->assertEqualities(e);
145 }
146
147
addSplitter(const Expr & e,int priority)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
addGlobalLemma(const Theorem & thm,int priority)157 void Theory::addGlobalLemma(const Theorem& thm, int priority) {
158 d_theoryCore->d_coreSatAPI->addLemma(thm, priority, true);
159 }
160
161
assignValue(const Expr & t,const Expr & val)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
assignValue(const Theorem & thm)170 void Theory::assignValue(const Theorem& thm) {
171 TRACE("facts assertFact", "assignValue["+getName()+"](", thm, ") {");
172 d_theoryCore->assignValue(thm);
173 TRACE("facts assertFact", "assignValue[", getName(), "] => }");
174 }
175
176
registerKinds(Theory * theory,vector<int> & kinds)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
unregisterKinds(Theory * theory,vector<int> & kinds)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
registerTheory(Theory * theory,vector<int> & kinds,bool hasSolver)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
unregisterTheory(Theory * theory,vector<int> & kinds,bool hasSolver)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
getNumTheories()241 int Theory::getNumTheories()
242 {
243 return d_theoryCore->d_theories.size();
244 }
245
246
hasTheory(int kind)247 bool Theory::hasTheory(int kind) {
248 return (d_theoryCore->d_theoryMap.count(kind) > 0);
249 }
250
251
theoryOf(int kind)252 Theory* Theory::theoryOf(int kind)
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
theoryOf(const Type & e)260 Theory* Theory::theoryOf(const Type& e)
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
theoryOf(const Expr & e)271 Theory* Theory::theoryOf(const Expr& e)
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
findRef(const Expr & e)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
find(const Expr & e)310 Theorem Theory::find(const Expr& e)
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
findReduce(const Expr & e)327 Theorem Theory::findReduce(const Expr& e)
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
findReduced(const Expr & e)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
getTCC(const Expr & e)367 Expr Theory::getTCC(const Expr& e)
368 {
369 if(e.isVar()) return trueExpr();
370 ExprMap<Expr>::iterator itccCache = d_theoryCore->d_tccCache.find(e);
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
getBaseType(const Expr & e)383 Type Theory::getBaseType(const Expr& e)
384 {
385 return getBaseType(e.getType());
386 }
387
388
getBaseType(const Type & tp)389 Type Theory::getBaseType(const Type& tp)
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
getTypePred(const Type & t,const Expr & e)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
updateHelper(const Expr & e)417 Theorem Theory::updateHelper(const Expr& e)
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)
setupCC(const Expr & e)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())
updateCC(const Theorem & e,const Expr & d)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);
504 getEM()->invalidateSimpCache();
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())
rewriteCC(const Expr & e)512 Theorem Theory::rewriteCC(const Expr& e) {
513 const Theorem& rep = e.getRep();
514 if (rep.isNull()) return reflexivityRule(e);
515 else return symmetryRule(rep);
516 }
517
518
parseExpr(const Expr & e)519 Expr Theory::parseExpr(const Expr& e) {
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
getModelTerm(const Expr & e,vector<Expr> & v)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
getModelValue(const Expr & e)541 Theorem Theory::getModelValue(const Expr& e) {
542 return d_theoryCore->getModelValue(e);
543 }
544
545
isLeafIn(const Expr & e1,const Expr & e2)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
leavesAreSimp(const Expr & e)557 bool Theory::leavesAreSimp(const Expr& e)
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
newVar(const string & name,const Type & type)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
newVar(const string & name,const Type & type,const Expr & def)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
newFunction(const string & name,const Type & type,bool computeTransClosure)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
newFunction(const string & name,const Type & type,const Expr & def)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
lookupFunction(const string & name,Type * type)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
addBoundVar(const string & name,const Type & type)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) {
714 DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheTop,
715 "Parse cache invariant violated");
716 d_theoryCore->d_parseCache = &d_theoryCore->d_parseCacheOther;
717 DebugAssert(d_theoryCore->d_parseCache->empty(),
718 "Expected empty cache");
719 }
720 else {
721 DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheOther,
722 "Parse cache invariant violated 2");
723 d_theoryCore->d_parseCache->clear();
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");
727 hash_map<string, Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
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
addBoundVar(const string & name,const Type & type,const Expr & def)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) {
752 DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheTop,
753 "Parse cache invariant violated");
754 d_theoryCore->d_parseCache = &d_theoryCore->d_parseCacheOther;
755 DebugAssert(d_theoryCore->d_parseCache->empty(),
756 "Expected empty cache");
757 }
758 else {
759 DebugAssert(d_theoryCore->d_parseCache == &d_theoryCore->d_parseCacheOther,
760 "Parse cache invariant violated 2");
761 d_theoryCore->d_parseCache->clear();
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");
765 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
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
lookupVar(const string & name,Type * type)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
newTypeExpr(const string & name)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
lookupTypeExpr(const string & name)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
newSubtypeExpr(const Expr & pred,const Expr & witness)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
newTypeExpr(const string & name,const Type & def)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
resolveID(const string & name)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
891 hash_map<string,Expr>::iterator iBoundVarMap = d_theoryCore->d_boundVarMap.find(name);
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
installID(const string & name,const Expr & e)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
typePred(const Expr & e)918 Theorem Theory::typePred(const Expr& e) {
919 return d_theoryCore->typePred(e);
920 }
921
922
rewriteIte(const Expr & e)923 Theorem Theory::rewriteIte(const Expr& e)
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
renameExpr(const Expr & e)935 Theorem Theory::renameExpr(const Expr& e) {
936 Theorem thm = d_commonRules->varIntroSkolem(e);
937 DebugAssert(thm.isRewrite() && thm.getRHS().isSkolem(),
938 "thm = "+thm.toString());
939 d_theoryCore->addToVarDB(thm.getRHS());
940 return thm;
941 }
942