37 : d_em(theoryCore->getEM()),
38 d_theoryCore(theoryCore),
39 d_commonRules(theoryCore->getTM()->getRules()),
40 d_name(name), d_theoryUsed(false) {
48 TRACE(
"model",
"Theory::computeModelTerm(", e,
"): is a variable");
63 vector<Theorem> newChildrenThm;
64 vector<unsigned> changed;
65 for(
int k = 0; k < ar; ++k) {
69 newChildrenThm.push_back(thm);
73 if(changed.size() > 0)
84 kids.push_back(
getTCC(*i));
85 return (kids.size() == 0) ?
trueExpr() :
86 (kids.size() == 1) ? kids[0] :
107 IF_DEBUG(debugger.counter(
"conflicts from DPs")++;)
149 TRACE(
"facts assertFact",
"addSplitter[" +
getName() +
"->](", e,
163 TRACE(
"facts assertFact",
"assignValue["+
getName()+
"](", t,
", "+
166 TRACE(
"facts assertFact",
"assignValue[",
getName(),
"] => }");
171 TRACE(
"facts assertFact",
"assignValue["+
getName()+
"](", thm,
") {");
173 TRACE(
"facts assertFact",
"assignValue[",
getName(),
"] => }");
179 vector<int>::const_iterator k;
180 vector<int>::const_iterator kEnd;
181 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
192 vector<int>::const_iterator k;
193 vector<int>::const_iterator kEnd;
194 for (k = kinds.begin(), kEnd = kinds.end(); k != kEnd; ++k) {
196 "kind not registered: "+
getEM()->getKindName(*k)
299 if (thm1.isRefl())
return thm1;
300 const Expr& e1 = thm1.getRHS();
314 if (thm1.
isRefl())
return thm1;
316 if (e1 == e || !e1.
hasFind() ||
339 vector<Theorem> newChildrenThm;
340 vector<unsigned> changed;
341 for(
int k = 0; k < ar; ++k) {
345 newChildrenThm.push_back(thm);
346 changed.push_back(k);
349 if(changed.size() > 0)
372 return (*itccCache).second;
375 TRACE(
"tccs",
"computeTCC["+i->
getName()+
"](", e,
") {");
378 TRACE(
"tccs",
"computeTCC["+i->
getName()+
"] => ", tcc,
" }");
395 if(!res.isNull())
return res;
398 "Theory::getBaseType(): No theory for the type: "
440 vector<Theorem> newChildrenThm;
441 vector<unsigned> changed;
442 for (
int k = 0; k < ar; ++k) {
445 newChildrenThm.push_back(thm);
446 changed.push_back(k);
449 if (changed.size() > 0)
461 for (
int k = 0; k < e.
arity(); ++k) {
476 int k, ar(d.
arity());
478 if (!dEQdsig.isNull()) {
479 const Expr& dsig = dEQdsig.getRHS();
482 if (sigNew == dsig) {
488 if (!repEQsigNew.
isNull()) {
497 for (k = 0; k < ar; ++k) {
498 if (sigNew[k] != dsig[k]) {
530 TRACE(
"model",
"computeModelTerm["+i->
getName()+
"](", e,
") {");
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()
549 if (e1 == e2)
return true;
550 if (
theoryOf(e2) !=
this)
return false;
562 for (
int k = 0; k < e.
arity(); ++k) {
579 (
"incompatible redefinition of variable "+name+
":\n "
580 "already defined with type: "+t.
toString()
581 +
"\n the new type is: "+type.
toString());
600 throw Exception(
"newVar: expected non-function type");
602 if( !res.lookupType().isNull() ) {
603 throw Exception(
"newVarExpr: redefining a variable " + name);
617 (
"Redefinition of variable "+name+
":\n "
618 "This variable is already defined.");
624 while(t.getExpr().getKind() ==
TYPEDEF) {
625 DebugAssert(t.arity() == 2,
"Bad TYPEDEF: "+t.toString());
633 " is declared with type:\n "
635 +
"\nBut the type of definition is\n "
648 bool computeTransClosure) {
655 (
"Redefinition of variable "+name+
":\n "
656 "already defined with type: "+t.
toString()
657 +
"\n the new type is: "+type.
toString());
671 if (computeTransClosure &&
673 res.setComputeTransClosure();
686 (
"Redefinition of name "+name+
":\n "
687 "already defined with type: "+t.
toString()
688 +
"\n the new type is: "+type.
toString());
701 if ((*type).isNull())
return Op();
712 Expr v(
getEM()->newBoundVarExpr(name, ss.str(), type));
715 "Parse cache invariant violated");
718 "Expected empty cache");
722 "Parse cache invariant violated 2");
729 (*iBoundVarMap).second =
Expr(
RAW_LIST, v, (*iBoundVarMap).second);
733 TRACE(
"vars",
"addBoundVar("+name+
", ", type,
") => "+v.
toString());
749 getEM()->newBoundVarExpr(name, ss.str(), type), def);
753 "Parse cache invariant violated");
756 "Expected empty cache");
760 "Parse cache invariant violated 2");
767 (*iBoundVarMap).second =
Expr(
RAW_LIST, res, (*iBoundVarMap).second);
770 TRACE(
"vars",
"addBoundVar("+name+
", "+type.
toString()+
", ", def,
783 if ((*type).isNull())
return Expr();
795 (
"Redefinition of type variable "+name+
":\n "
796 "This variable is already defined.");
819 if(!predTp.isFunction() || predTp.arity() != 2)
821 (
"Expected unary predicate in the predicate subtype:\n\n "
823 +
"\n\nThe predicate is:\n\n "
825 if(!predTp[1].isBool())
827 (
"Range is not BOOLEAN in the predicate subtype:\n\n "
829 +
"\n\nThe predicate is:\n\n "
844 (
"Subtype predicate could not be proved total in the following type:\n\n "
846 +
"\n\nThe failed TCC is:\n\n "
862 (
"Unable to prove witness for subtype:\n\n "
864 +
"\n\nThe failed condition is:\n\n "
877 (
"Redefinition of type variable "+name+
":\n "
878 "This variable is already defined.");
893 res = (*iBoundVarMap).second;
913 "installID called on existing identifier");