61 return d_core->theoryOf(e)->print(os, e);
62 else if(d_core->hasTheory(e.
getKind()))
63 return d_core->theoryOf(e.
getKind())->print(os, e);
85 (
"Tried to use non-type as a type: "+e.
toString());
86 d_core->theoryOf(e)->checkType(e);
90 bool enumerate,
bool computeSize)
93 return d_core->theoryOf(e)->finiteTypeInfo(e, n, enumerate, computeSize);
100 os <<
"NotifyList(\n";
101 for(
size_t i=0,iend=l.
size(); i<iend; ++i) {
111 using namespace CVC3;
124 vector<Theory*>::iterator i, iend = d_theories.end();
125 bool lemmasAdded =
false;
128 while (!d_queue.empty() && !d_inconsistent && !timeLimitReached()) {
129 thm = d_queue.front();
135 if (d_inconsistent)
break;
137 while (!d_queueSE.empty() && !timeLimitReached()) {
142 d_queueSE.pop_back();
143 d_coreSatAPI->addLemma(thm);
147 for(i = d_theories.begin(); d_update_thms.empty() && d_queue.empty() && i != iend && !d_inconsistent && !timeLimitReached(); ++i) {
148 (*i)->checkSat(effort == FULL && !lemmasAdded);
151 }
while ((!d_queue.empty() || !d_update_thms.empty()) && !d_inconsistent && !timeLimitReached());
153 if (d_inconsistent) {
154 d_update_thms.clear();
155 d_update_data.clear();
156 while(d_queue.size()) d_queue.pop();
161 if (timeLimitReached()) {
163 d_update_thms.clear();
164 d_update_data.clear();
165 while (!d_queue.empty()) d_queue.pop();
177 for(
unsigned k = 0; k < L->
size() && !d_inconsistent; ++k) {
186 DebugAssert(d_simpStack.count(e) == 0,
"TheoryCore::simplify: loop detected over e =\n"
189 "TheoryCore::simplify: too deep recursion depth");
198 DebugAssert((find(e).getRHS().hasFind() && find(e).getRHS().isTerm())
199 || find(e).getRHS().isTrue()
200 || find(e).getRHS().isFalse(),
"Unexpected find pointer");
205 thm = transitivityRule(thm, simplify(thm.
getRHS()));
224 thm = rewriteCore(e);
227 thm = rewriteCore(theoryOf(e.
getOpKind())->simplifyOp(e));
231 #ifdef _CVC3_DEBUG_MODE
234 for (
int k=0; k<e2.
arity(); ++k) {
235 Expr simplified(simplify(e2[k]).getRHS());
238 +e2[k].toString() +
"\nSimplified = "
243 Expr rewritten(rewriteCore(e2).getRHS());
244 DebugAssert(e2==rewritten,
"Simplify Error 2: e2 = \n"
245 +e2.
toString() +
"\nSimplified rewritten = \n"
249 if (e != e2 && !e2.
hasFind()) {
260 "rewriteCore(thm): not equality or iff:\n " + e.
toString());
261 return transitivityRule(e, rewriteCore(e.
getRHS()));
269 void TheoryCore::setupSubFormulas(
const Expr& s,
const Expr& e,
273 setupTerm(s, theoryOf(s), thm);
277 setupTerm(s, theoryOf(s), thm);
278 for (
int i = 0; i < s.
arity(); ++i) {
284 for (
int i = 0; i < s.
arity(); ++i) {
285 setupSubFormulas(s[i], e, thm);
291 void TheoryCore::processUpdates()
295 DebugAssert(d_update_thms.size() == d_update_data.size(),
296 "Expected same size");
297 while (!d_inconsistent && !d_update_thms.empty()) {
298 e = d_update_thms.back();
299 d_update_thms.pop_back();
300 d = d_update_data.back();
301 d_update_data.pop_back();
305 if (thm.getRHS().isTrue()) {
306 setFindLiteral(d_commonRules->iffTrueElim(thm));
308 else if (thm.getRHS().isFalse()) {
309 setFindLiteral(d_commonRules->iffFalseElim(thm));
314 find(e.
getRHS()).getRHS().addToNotify(
this, d);
315 if (thm.getRHS().isAbsAtomicFormula()) thm.getRHS().addToNotify(
this, d);
321 void TheoryCore::assertFactCore(
const Theorem& e)
323 IF_DEBUG(
string indentStr(getCM()->scopeLevel(),
' ');)
329 Theorem equiv = simplify(estar);
330 if (!equiv.isRefl()) {
331 estarThm = iffMP(e, equiv);
336 estar = estarThm.getExpr();
340 Theorem solvedThm(solve(estarThm));
341 if(estar != solvedThm.
getExpr()) setFindLiteral(estarThm);
343 assertEqualities(solvedThm);
346 IF_DEBUG(debugger.counter(
"conflicts from simplifier")++;)
347 setInconsistent(estarThm);
349 else if (!estar.
isTrue()) {
350 assertFormula(estarThm);
360 find(e.
getLHS()).getRHS() != find(e.
getRHS()).getRHS()) {
361 TRACE(
"assertFactCore",
"Problem (LHS of): ", e.
getExpr(),
"");
362 TRACE(
"assertFactCore", find(e.
getLHS()).getRHS(),
" vs ", find(e.
getRHS()).getRHS());
363 IF_DEBUG(cerr <<
"Warning: Equivalence classes didn't get merged" <<
endl;)
366 }
else if (estar.
isAnd()) {
367 for(
int i=0,iend=estar.
arity(); i<iend && !d_inconsistent; ++i)
368 assertFactCore(d_commonRules->andElim(estarThm, i));
377 || (e2.isNot() && e2[0].hasFind()),
378 "assertFactCore: e2 = "+e2.toString());
381 "assertFactCore: estar = "+estar.
toString());
385 void TheoryCore::assertFormula(
const Theorem& thm)
390 IF_DEBUG(
string indentStr(getCM()->scopeLevel(),
' ');)
403 "Expected negated argument to assertFormula to not have find");
410 enqueueFact(d_commonRules->skolemize(thm));
418 i2 = theoryOf(getBaseType(e[0][0]));
419 DebugAssert(e[0][0] > e[0][1],
"Expected lhs of diseq to be greater");
430 i2 = theoryOf(getBaseType(e[0]));
436 transitivityRule(d_commonRules->rewriteUsingSymmetry(e2),
437 d_commonRules->iffTrue(thm));
438 setFindLiteral(d_commonRules->iffTrueElim(thm2));
462 if (d_inUpdate && !thm.
isRefl()) {
463 thm = transitivityRule(thm, simplify(thm.
getRHS()));
473 Expr rewritten(rewriteCore(e).getRHS());
476 "Expected no change: e = " + e.
toString()
477 +
"\n rewriteCore(e) = "+rewritten.
toString());
479 return reflexivityRule(e);
484 return rewriteCore(d_commonRules->rewriteUsingSymmetry(e));
485 else if (e[0] == e[1])
486 return d_commonRules->rewriteReflexivity(e);
490 return rewriteCore(d_commonRules->rewriteNotNot(e));
495 Theorem thm = theoryOf(e)->rewrite(e);
501 "theory-specific rewrites for equality should ensure lhs >= rhs");
503 thm = rewriteCore(thm);
509 void TheoryCore::setFindLiteral(
const Theorem& thm)
514 const Expr& e0 = e[0];
516 IF_DEBUG(
string indentStr(getCM()->scopeLevel(),
' ');)
518 Theorem findThm = d_commonRules->notToIff(thm);
523 d_impliedLiterals.push_back(thm);
525 d_em->invalidateSimpCache();
527 if (L) processNotify(findThm, L);
532 setInconsistent(iffMP(d_commonRules->iffTrueElim(findThm),
533 d_commonRules->notToIff(thm)));
538 IF_DEBUG(
string indentStr(getCM()->scopeLevel(),
' ');)
540 Theorem findThm = d_commonRules->iffTrue(thm);
545 d_impliedLiterals.push_back(thm);
547 d_em->invalidateSimpCache();
549 if (L) processNotify(findThm, L);
554 setInconsistent(iffMP(thm, findThm));
565 return d_commonRules->rewriteReflexivity(e);
566 else if (e[0] < e[1])
567 return d_commonRules->rewriteUsingSymmetry(e);
571 return d_commonRules->rewriteNotTrue(e);
572 else if (e[0].isFalse())
573 return d_commonRules->rewriteNotFalse(e);
574 else if (e[0].isNot())
575 return d_commonRules->rewriteNotNot(e);
579 "TheoryCore::rewriteLitCore("
581 +
"): Not implemented");
584 return reflexivityRule(e);
588 void TheoryCore::enqueueSE(
const Theorem& thm)
591 d_queueSE.push_back(thm);
598 iend=d_varAssignments.end();
599 if(i!=iend)
return (*i).second;
608 if(i == e.
arity()-2) {
612 Expr c(parseExpr(e[i][0]));
613 Expr e1(parseExpr(e[i][1]));
614 Expr e2(parseExpr(e[i+1][1]));
618 if(e[i].getKind() ==
RAW_LIST && e[i].arity() == 2
619 && e[i+1].getKind() ==
RAW_LIST && e[i+1].arity() == 2) {
620 Expr c(parseExpr(e[i][0]));
621 Expr e1(parseExpr(e[i][1]));
622 Expr e2(processCond(e, i+1));
630 bool TheoryCore::isBasicKind(
int kind)
704 :
Theory(), d_cm(cm), d_tm(tm), d_flags(flags), d_statistics(statistics),
705 d_translator(translator),
706 d_inconsistent(cm->getCurrentContext(), false, 0),
707 d_incomplete(cm->getCurrentContext()),
708 d_incThm(cm->getCurrentContext()),
709 d_terms(cm->getCurrentContext()),
711 d_predicates(cm->getCurrentContext()),
713 d_simplifyInPlace(false),
714 d_currentRecursiveSimplifier(NULL),
718 d_inCheckSATCore(false), d_inAddFact(false),
719 d_inRegisterAtom(false), d_inPP(false),
720 d_notifyObj(this, cm->getCurrentContext()),
721 d_impliedLiterals(cm->getCurrentContext()),
722 d_impliedLiteralsIdx(cm->getCurrentContext(), 0, 0),
723 d_notifyEq(cm->getCurrentContext()),
759 kinds.push_back(
NEQ);
761 kinds.push_back(
ECHO);
762 kinds.push_back(
DBG);
763 kinds.push_back(
TRACE);
766 kinds.push_back(
HELP);
767 kinds.push_back(
AND);
771 kinds.push_back(
ELSE);
772 kinds.push_back(
COND);
773 kinds.push_back(
XOR);
774 kinds.push_back(
NOT);
775 kinds.push_back(
ITE);
776 kinds.push_back(
IFF);
778 kinds.push_back(
APPLY);
780 kinds.push_back(
LET);
789 kinds.push_back(
TYPE);
791 kinds.push_back(
CONST);
794 kinds.push_back(
DEFUN);
801 kinds.push_back(
QUERY);
802 kinds.push_back(
PRINT);
815 kinds.push_back(
CALL);
816 kinds.push_back(
WHERE);
821 kinds.push_back(
PUSH);
822 kinds.push_back(
POP);
823 kinds.push_back(
POPTO);
827 kinds.push_back(
RESET);
834 kinds.push_back(
SEQ);
839 kinds.push_back(
AND_R);
840 kinds.push_back(
IFF_R);
841 kinds.push_back(
ITE_R);
892 TRACE(
"quantlevel",
"getTheoremForTerm: no theorem found: ", e ,
"");
898 #ifdef _CVC3_DEBUG_MODE
929 TRACE(
"quantlevel",
"cannot find expr: " , e,
"");
935 TRACE(
"quantlevel",
"expr get level:", thm.getQuantLevel(),
"");
946 return thm.getQuantLevel();
964 "TheoryCore::assertFact("+e.
toString()+
")");
1004 "TheoryCore::rewrite[IMPLIES]: rhs = "+rhs.
toString());
1007 vector<unsigned> changed;
1008 vector<Theorem> thms;
1009 changed.push_back(0);
1032 if (e != e1 && e1.
isNot())
1038 if (!thm.
isRefl())
break;
1039 else if (
getFlags()[
"un-ite-ify"].getBool()) {
1044 if (e[1].isFalse() && e[2].
isTrue())
1046 else if (e[1].isTrue())
1048 else if (e[2].isFalse())
1050 else if (e[2].isTrue())
1052 else if (e[1] == e[2].negate())
1056 else if(
getFlags()[
"ite-cond-simp"].getBool()) {
1087 "TheoryCore::rewrite("
1089 +
"): Not implemented");
1098 switch(rhs.getKind()) {
1100 if(
getFlags()[
"simp-and"].getBool()) {
1102 for(
int i=0, iend=rhs.arity(); i<iend; ++i) {
1106 if(tmp.
getRHS() != rhs) {
1114 if(
getFlags()[
"simp-or"].getBool()) {
1116 for(
int i=0, iend=rhs.arity(); i<iend; ++i) {
1120 if(tmp.
getRHS() != rhs) {
1145 const Expr& eq = d[0];
1149 const Expr& newlhs = thm1.getRHS();
1151 if (newlhs == newrhs) {
1161 if (newlhs < newrhs) {
1203 +
"\nsolved = "+solved.toString());
1209 +
"\nsolved = "+solved.toString());
1215 +
"\nsolved = "+solved.toString());
1224 for (
int index = 0; index < e2.
arity(); ++index) {
1274 if (
d_solver != i) thm = i->solve(thm);
1285 if (
d_solver != j && i != j) thm = j->solve(thm);
1300 IF_DEBUG(debugger.counter(
"simplified x=x")++;)
1312 for(; l<ar && e[l].
getKind() != endKind; ++l);
1314 IF_DEBUG(debugger.counter(
"simplified AND/OR topdown")++;)
1320 vector<Theorem> newChildrenThm;
1321 vector<unsigned> changed;
1322 for(
int k = 0; k < ar; ++k) {
1327 newChildrenThm.clear();
1329 newChildrenThm.push_back(thm);
1330 changed.push_back(k);
1337 IF_DEBUG(debugger.counter(
"simplified AND/OR: skipped kids")
1341 newChildrenThm.push_back(thm);
1342 changed.push_back(k);
1346 if(changed.size() > 0)
1356 IF_DEBUG(debugger.counter(
"simplified ITE(c,e,e)")++;)
1362 vector<Theorem> newChildrenThm;
1363 vector<unsigned> changed;
1366 newChildrenThm.push_back(thm);
1367 changed.push_back(0);
1371 for(
int k=1; k<=2; ++k) {
1376 IF_DEBUG(debugger.counter(
"simplified ITE: skiped one branch")++;)
1382 newChildrenThm.push_back(thm);
1383 changed.push_back(k);
1386 if(changed.size() > 0)
1412 if (e.
arity() > 0) {
1422 (
"Non-function argument to SUBTYPE:\n\n"
1426 (
"Non-predicate argument to SUBTYPE:\n\n"
1431 if (e.
arity() != 0) {
1437 FatalAssert(
false,
"Unexpected kind in TheoryCore::checkType"
1444 bool enumerate,
bool computeSize)
1464 FatalAssert(
false,
"Unexpected kind in TheoryCore::finiteTypeInfo"
1478 (
"The conditional in IF-THEN-ELSE must be BOOLEAN, but is:\n\n"
1479 +e[0].getType().toString()
1480 +
"\n\nIn the expression:\n\n "
1484 (
"The types of the IF-THEN-ELSE branches do not match.\n"
1485 "THEN branch has the type:\n\n "
1486 +e[1].getType().toString()
1487 +
"\n\nELSE branch has the type:\n\n "
1488 +e[2].getType().toString()
1489 +
"\n\nIn expression:\n\n "+e.
toString());
1491 Type res(e[1].getType());
1494 if(res == e[2].getType()) {
1506 if (t0.isBool() || t1.
isBool()) {
1508 (
"Cannot use EQ ('=') for BOOLEAN type; use IFF ('<=>') instead.\n"
1509 "Error in the following expression:\n"+e.
toString());
1513 (
"Type mismatch in equality:\n\n LHS type:\n"+t0.toString()
1515 +
"\n\n in expression: \n"+e.
toString());
1522 for (
int i = 1; i < e.
arity(); ++i) {
1525 (
"Type mismatch in distinct:\n\n types:\n"+t0.
toString()
1527 +
"\n\n in expression: \n"+e.
toString());
1544 for (
int k = 0; k < e.
arity(); ++k) {
1545 if (e[k].getType() !=
boolType()) {
1559 if(valTp != varTp) {
1563 +
"\n derived: "+ valTp.
toString());
1573 Type funType = funExpr.getType();
1577 (
"Expected function type for:\n\n"
1578 + funExpr.toString() +
"\n\n but got this: "
1580 +
"\n\n in function application:\n\n"+e.
toString());
1586 +
"\n\nFunction \""+funExpr.toString()
1589 +
string((funType.
arity()==2)?
"" :
"s")
1593 for (
int k = 0; k < e.
arity(); ++k) {
1598 +
"\n\nhas the following type:\n\n "
1599 + e[k].getType().toString()
1600 +
"\n\nbut the expected type is:\n\n "
1601 + funType[k].getExpr().toString()
1602 +
"\n\nin function application:\n\n "
1614 +
"):\nNot implemented");
1630 "Expr::computeBaseType(): lambdaBaseTp = "
1632 res = lambdaBaseTp[0];
1661 tccs.push_back(
getTCC(*i));
1664 for(
size_t i=0, iend=tccs.size(); i<iend; ++i)
1673 tccs.push_back(
getTCC(*i));
1676 for(
size_t i=0, iend=tccs.size(); i<iend; ++i)
1684 Expr tccITE((tcc1 == tcc2)? tcc1 : e[0].iteExpr(tcc1, tcc2));
1709 Expr pred = tExpr[0];
1747 "TheoryCore::parseExprOp:\n e = "+e.
toString());
1748 TRACE(
"parse",
"TheoryCore::parseExprOp:\n e = ", e.
toString(),
"");
1751 const Expr& c1 = e[0][0];
1755 vector<Expr> operatorStack;
1756 vector<Expr> operandStack;
1757 vector<int> childStack;
1760 operatorStack.push_back(e);
1761 childStack.push_back(1);
1763 while (!operatorStack.empty()) {
1764 DebugAssert(operatorStack.size() == childStack.size(),
"Invariant violated");
1766 if (childStack.back() < operatorStack.back().arity()) {
1768 e2 = operatorStack.back()[childStack.back()++];
1772 operandStack.push_back((*iParseCache).second);
1778 operatorStack.push_back(e2);
1779 childStack.push_back(1);
1786 e2 = operatorStack.back();
1787 operatorStack.pop_back();
1788 childStack.pop_back();
1789 vector<Expr> children;
1790 vector<Expr>::iterator childStart = operandStack.end() - (e2.
arity() - 1);
1791 children.insert(children.begin(), childStart, operandStack.end());
1792 operandStack.erase(childStart, operandStack.end());
1794 operandStack.push_back(
Expr(kind, children, e2.
getEM()));
1795 (*d_parseCache)[e2] = operandStack.back();
1796 if (!
getEM()->isTypeKind(operandStack.back().getKind())) {
1797 operandStack.back().getType();
1801 DebugAssert(childStack.empty(),
"Invariant violated");
1802 DebugAssert(operandStack.size() == 1,
"Expected single operand left");
1803 return operandStack.back();
1808 if (e.
arity() <= 3) {
1810 if (e.
arity() == 3) {
1823 getFlags()[
"convert-eq-iff"].getBool()) {
1844 const Expr& types = e[1];
1848 names.push_back(*i);
1859 if(e.
arity() == 4) {
1882 const Expr& decl = *i;
1887 if (decl[0].getKind() !=
ID)
1889 "expression: "+decl[0].toString()+
1894 if (e2[2].getKind()==
RAW_LIST && e2[2].arity() > 0 &&
1895 e2[2][0].getKind()==
ID &&
getEM()->getKind(e2[2][0][0].getString()) ==
LET) {
1908 "TheoryCore::parseExprOp: invalid command or expression: "
1917 "Invalid state in printSmtLibShared" );
1925 throw SmtlibException(
"TheoryCore::print: SMTLIB: SUBTYPE not implemented");
1928 throw SmtlibException(
"TheoryCore::print: SMTLIB: TYPEDEF not implemented");
1932 os <<
"(" <<
push <<
"=" <<
space << e[0]
1936 int i=0, iend=e.
arity();
1937 os <<
"(" << push <<
"distinct";
1938 for(; i!=iend; ++i) os <<
space << e[i];
1943 os <<
"(" << push <<
"not" <<
space << e[0] << push <<
")";
1946 int i=0, iend=e.
arity();
1950 os <<
"(" << push <<
"and";
1951 for(; i!=iend; ++i) os <<
space << e[i];
1957 int i=0, iend=e.
arity();
1961 os <<
"(" << push <<
"or";
1962 for(; i!=iend; ++i) os <<
space << e[i];
1968 int i=0, iend=e.
arity();
1972 os <<
"(" << push <<
"xor";
1973 for(; i!=iend; ++i) os <<
space << e[i];
1980 throw SmtlibException(
"TheoryCore::print: SMTLIB: TRANSFORM not implemented");
1981 os <<
"(" << push <<
"TRANSFORM" <<
space << e[0] << push <<
")";
1986 if(e.
arity() == 2) os << e[1];
1993 "Proof rule application must have at "
1994 "least one argument (rule name):\n "+e.
toString());
1996 os << e[0] <<
"\n" ;
1998 os << push <<
"(" <<
push;
2000 for(
int i=1; i<e.arity(); i++) {
2001 if(first) first=
false;
2002 else os << push <<
"," <<
pop <<
space;
2012 bool firstTime(
true);
2014 if(firstTime) firstTime =
false;
2027 throw SmtlibException(
"TheoryCore::print: SMTLIB_LANG: Unexpected expression: "
2035 if (it != visited.
end())
return false;
2036 it = defs.
find(def);
2037 if (it != defs.
end())
return true;
2046 visited[def] =
true;
2072 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: TYPE should have been handled by Translator::finish()");
2074 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
2078 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: CONST should have been handled by Translator::finish()");
2080 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: SUBTYPE not implemented");
2083 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: TYPEDEF not implemented");
2087 os <<
push <<
"equal(" << e[0]
2091 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: SUBTYPE not implemented");
2095 os << push <<
"not(" << e[0] << push <<
")";
2098 int i=0, iend=e.
arity();
2099 os << push <<
"and(" << e[i];
2100 while(++i != iend) os <<
"," <<
space << e[i];
2105 int i=0, iend=e.
arity();
2106 os << push <<
"or(" << e[i];
2107 while(++i != iend) os <<
"," <<
space << e[i];
2112 if(e.
arity() != 2) {
2113 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: XOR not supported when arity != 2 !");
2115 os << push <<
"or(and(" << e[0] <<
"," <<
space <<
"not(" << e[1] <<
")),"
2116 <<
space <<
"and(not(" << e[0] <<
")," <<
space << e[1] <<
")"
2122 os << push <<
"and(" <<
space
2123 << push <<
"implies(" <<
space
2124 << e[0] <<
"," <<
space << e[1]
2125 << push <<
")" <<
"," <<
space
2126 << push <<
"implies(" <<
space
2131 os << push <<
"if_then_else("
2132 << e[0] <<
"," <<
space
2133 << e[1] <<
"," <<
space
2134 << e[2] << push <<
")";
2138 os << push <<
"equiv(" <<
space
2139 << e[0] <<
space <<
"," <<
space << e[1] << push <<
")";
2142 os << push <<
"implies(" <<
space
2143 << e[0] <<
space <<
"," <<
space << e[1] << push <<
")";
2154 throw SmtlibException(
"TheoryCore::print: SPASS: TRANSFORM not implemented");
2162 os <<
"formula(" <<
space << push << e[0] <<
space <<
").";
2165 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: LETDECL not implemented");
2167 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: LET should have been handled in Translator::finish()");
2179 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: PF_APPLY not implemented");
2181 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: ANNOTATION should have been handled by Translator::finish()");
2199 throw SmtlibException(
"TheoryCore::print: SPASS_LANG: Unexpected expression: "
2211 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
2223 os <<
"(EQ " << e[0] <<
" " << e[1] <<
")";
2225 case NOT: os <<
"(NOT " << e[0] <<
")";
break;
2227 int i=0, iend=e.arity();
2229 if(i!=iend) { os << e[i]; ++i; }
2230 for(; i!=iend; ++i) os <<
" " << e[i];
2235 int i=0, iend=e.arity();
2237 if(i!=iend) { os << e[i]; ++i; }
2238 for(; i!=iend; ++i) os <<
" " << e[i];
2243 os<<
"ERROR:ITE:not supported yet\n";
2247 os <<
"(IFF " << e[0] <<
" " << e[1] <<
")";
2252 os <<
"(IMPLIES " <<e[0] <<
" " << e[1] <<
")";
2256 os <<
"(BG_PUSH " << e[0] <<
")\n";
2259 os <<
"ERROR:TRANSFORM:not supported in Simplify " <<
push << e[0] <<
push <<
"\n";
2265 os <<
"ERROR:WHERE:not supported in Simplify\n";
2268 os <<
"ERROR:ASSERTIONS:not supported in Simplify\n";
2271 os <<
"ERROR:ASSUMPTIONS:not supported in Simplify\n";
2274 os <<
"ERROR:COUNTEREXAMPLE:not supported in Simplify\n";
2277 os <<
"ERROR:COUNTERMODEL:not supported in Simplify\n";
2286 os <<
"ERROR:PUSH and POP:not supported in Simplify\n";
2290 os <<
"LETDECL not supported in Simplify\n";
2312 os <<
"LET not supported in Simplify\n";
2321 os <<
"SKOLEM_" +
int2string((
int)e.getIndex());
2339 os <<
"PR_APPLY not supported in Simplify\n";
2350 os <<
"RAW_LIST not supported in Simplify\n";
2362 static int axiom_counter =0;
2368 if(e.
arity() == 0) os <<
"TYPE";
2369 else if(e.
arity() == 1) {
2370 for (
int i=0; i < e[0].
arity(); ++i) {
2371 if (i != 0) os <<
endl;
2372 os << e[0][i] <<
": TYPE;";
2375 else if(e.
arity() == 2)
2376 os << e[0] <<
":" <<
push <<
" TYPE = " << e[1] <<
push <<
";";
2380 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
2384 if(e.
arity() == 2) {
2385 string ename =
to_lower(e[0].toString());
2386 os <<
"tff(" << ename <<
"_type, type,\n " << ename;
2387 os <<
": " << e[1] <<
"). \n";
2390 os <<
"ERROR: CONST's arity > 2";
2400 os << e[0] <<
" = " << e[1];
2404 int i=0, iend=e.arity();
2405 os <<
"$distinct(" ;
2408 for(; i!=iend; ++i) os <<
", " << e[i] ;
2414 os <<
"~(" << e[0]<<
")" ;
2418 int i=0, iend=e.arity();
2424 for(i=0 ; i < iend-1; i++) {
2425 os <<
"(" << e[i] <<
" \n& " ;
2428 for(i=0 ; i < iend-1; i++) {
2433 os <<
"ERROR:AND has less than 1 parameter\n";
2438 int i=0, iend=e.arity();
2444 for(i=0 ; i < iend-1; i++) {
2445 os <<
"(" << e[i] <<
" \n| " ;
2448 for(i=0 ; i < iend-1; i++) {
2453 os <<
"ERROR:OR has less than 1 parameter\n";
2458 os<<
"ERROR:ITE:not supported in TPTP yet\n";
2465 os <<
"(" << e[0] <<
" \n<=> " << e[1] <<
")" ;
2470 os <<
"(" << e[0] <<
" \n=> " << e[1] <<
")" ;
2474 os <<
"tff(" << axiom_counter++ <<
", axiom, \n " <<e[0] <<
").\n";
2478 os <<
"ERROR:TRANSFORM:not supported in TPTP " <<
push << e[0] <<
push <<
"\n";
2481 if(
getFlags()[
"negate-query"].getBool() ==
true){
2483 os <<
"tff(" << axiom_counter++ <<
", conjecture, \n " <<e[0][0] <<
").\n";
2486 os <<
"tff(" << axiom_counter++ <<
", conjecture, \n ~(" << e[0] <<
")).\n";
2490 os <<
"tff(" << axiom_counter++ <<
", conjecture, \n " <<e[0] <<
").\n";
2494 os <<
"ERROR:WHERE:not supported in TPTP\n";
2497 os <<
"ERROR:ASSERTIONS:not supported in TPTP\n";
2500 os <<
"ERROR:ASSUMPTIONS:not supported in TPTP\n";
2503 os <<
"ERROR:COUNTEREXAMPLE:not supported in TPTP\n";
2506 os <<
"ERROR:COUNTERMODEL:not supported in TPTP\n";
2515 os <<
"ERROR:PUSH and POP:not supported in TPTP\n";
2519 os <<
"LETDECL not supported in Simplify\n";
2524 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2525 if(!first) os <<
" , " ;
2527 if(i->arity() == 3) {
2528 os << (*i)[0] <<
":" << (*i)[1]
2529 <<
" ERROR= " <<
nodag << (*i)[2] ;
2532 os <<
" := " <<
nodag << (*i)[1] ;
2536 os <<
"] : " <<
endl <<
"(" << e[1] <<
")";
2547 os <<
"SKOLEM_VAR is not supported in TPTP\n";
2566 os <<
"PR_APPLY not supported in TPTP\n";
2577 os <<
"RAW_LIST not supported in TPTP\n";
2581 os <<
"PF_HOLE not supported in TPTP\n";
2584 {
string name = e.getName();
2585 if(name.length() >= 5){
2586 if (
'C' == name[0] &&
'V' == name[1] &&
'C' == name[2] &&
'_' == name[3] && isdigit(name[4])){
2601 os <<
"ERROR:STRING_EXPR is not suppoerted in TPTP\n";
2633 if(e.
arity() == 0) os <<
"TYPE";
2634 else if(e.
arity() == 1) {
2635 for (
int i=0; i < e[0].
arity(); ++i) {
2636 if (i != 0) os <<
endl;
2637 os << e[0][i] <<
": TYPE;";
2640 else if(e.
arity() == 2)
2641 os << e[0] <<
":" <<
push <<
" TYPE = " << e[1] <<
push <<
";";
2645 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
2649 if(e.
arity() == 2) {
2652 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2653 if(first) first =
false;
2661 }
else if(e.
arity() == 3)
2662 os << e[0] <<
":" <<
push <<
space << e[1]
2668 os <<
"SUBTYPE(" <<
push << e[0] <<
push <<
")";
2674 else if(e[0].isString()) os << e[0].
getString();
2675 else e[0].
print(os);
2685 os <<
"(" << push << e[0] <<
space <<
"= " << e[1] << push <<
")";
2688 os <<
"DISTINCT(" <<
push;
2691 if (!first) os << push <<
"," <<
pop <<
space;
2698 case NOT: os <<
"NOT " << e[0];
break;
2700 int i=0, iend=e.arity();
2702 if(i!=iend) { os << e[i]; ++i; }
2703 for(; i!=iend; ++i) os <<
space <<
"AND " << e[i];
2708 int i=0, iend=e.arity();
2710 if(i!=iend) { os << e[i]; ++i; }
2711 for(; i!=iend; ++i) os <<
space <<
"OR " << e[i];
2716 int i=0, iend=e.arity();
2718 if(i!=iend) { os << e[i]; ++i; }
2719 for(; i!=iend; ++i) os <<
space <<
"XOR " << e[i];
2724 os << push <<
"IF " << push << e[0] <<
popSave
2727 <<
space <<
"ENDIF";
2731 os <<
"(" << push << e[0] << space <<
"<=> " << e[1] << push <<
")";
2736 os <<
"(" << push << e[0] << space <<
"=> " << e[1] << push <<
")";
2740 os <<
"ASSERT " << push << e[0] << push <<
";";
2743 os <<
"TRANSFORM " << push << e[0] << push <<
";";
2746 os <<
"QUERY " << push << e[0] << push <<
";";
2752 os <<
"ASSERTIONS;";
2755 os <<
"ASSUMPTIONS;";
2758 os <<
"COUNTEREXAMPLE;";
2761 os <<
"COUNTERMODEL;";
2767 os <<
"PUSH" << space << e[0] << push <<
";";
2773 os <<
"POP" << space << e[0] << push <<
";";
2776 os <<
"POPTO" << space << e[0] << push <<
";";
break;
2779 os <<
"PUSH_SCOPE;";
2781 os <<
"PUSH_SCOPE" << space << e[0] << push <<
";";
2787 os <<
"POP_SCOPE" << space << e[0] << push <<
";";
2790 os <<
"POPTO_SCOPE" << space << e[0] << push <<
";";
break;
2795 if(e.arity() == 2) os << e[1];
2796 else e.printAST(os);
2801 os <<
"(" << push <<
"LET" << space <<
push;
2802 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2803 if(!first) os << push <<
"," <<
pop <<
endl;
2805 if(i->arity() == 3) {
2806 os << (*i)[0] <<
":" << space << push << (*i)[1]
2807 << space <<
"= " << push <<
nodag << (*i)[2] <<
pop <<
pop;
2810 Type tp((*i)[0].lookupType());
2811 if(!tp.
isNull()) os <<
":" << space << push << tp.
getExpr();
2813 os << space <<
"= " << push <<
nodag << (*i)[1] <<
pop <<
pop;
2816 os <<
pop <<
endl <<
"IN" << space << push << e[1] << push <<
")";
2823 if(
getFlags()[
"print-var-type"].getBool()) {
2824 os << e.getName() <<
"(" << e.getType() <<
")";
2831 os <<
"SKOLEM_" +
int2string((
int)e.getIndex());
2834 DebugAssert(e.arity() > 0,
"TheoryCore::print(): "
2835 "Proof rule application must have at "
2836 "least one argument (rule name):\n "+e.toString());
2838 os << e[0] <<
"\n" ;
2840 os << push <<
"(" <<
push;
2842 for(
int i=1; i<e.arity(); i++) {
2843 if(first) first=
false;
2844 else os << push <<
"," <<
pop <<
space;
2853 bool firstTime(
true);
2855 if(firstTime) firstTime =
false;
2856 else os << push <<
"," <<
pop <<
space;
2866 os <<
"ARITH_VAR_ORDER(" <<
push;
2867 bool firstTime(
true);
2869 if(firstTime) firstTime =
false;
2870 else os << push <<
"," <<
pop <<
space;
2879 if (e.arity() > 1) {
2897 if (e.
arity() == 1) {
2898 os <<
" :extrasorts (";
2899 for (
int i=0; i < e[0].
arity(); ++i) {
2901 os <<
push << e[0][i];
2905 else if (e.
arity() == 2) {
2909 throw SmtlibException(
"TheoryCore::print: SMTLIB: Unexpected TYPE expression");
2914 if(e.
arity() == 2) {
2915 if (e[1].getKind() ==
BOOLEAN) {
2919 else if (e[1].getKind() ==
ARROW && e[1][e[1].arity()-1].getKind() ==
BOOLEAN) {
2930 throw SmtlibException(
"TheoryCore::print: SMTLIB: CONST not implemented");
2935 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
2941 << e[0] <<
space << e[1] <<
push <<
")";
2945 os <<
"(" << push <<
"iff" <<
space
2946 << e[0] <<
space << e[1] << push <<
")";
2954 <<
space << e[1] <<
space << e[2] << push <<
")";
2959 os <<
" :assumption" <<
space << push << e[0];
2963 os <<
" :formula" <<
space << push << e[0].negate();
2968 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
2970 Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType());
2971 DebugAssert(!tp.isNull(),
"Unexpected Null type");
2972 if (tp.getExpr().getKind() ==
BOOLEAN) {
2978 if(i->arity() == 3) {
2986 for (
int j = 0; j < e[0].arity(); ++j)
2993 string str = e.getName();
2994 if (str[0] ==
'_') str[0] =
'?';
2999 os << push <<
"SKOLEM_" +
int2string((
int)e.getIndex());
3003 os <<
" :cvc_command \"WHERE\"";
3006 os <<
" :cvc_command \"ASSERTIONS\"";
3009 os <<
" :cvc_command \"ASSUMPTIONS\"";
3012 os <<
" :cvc_command \"COUNTEREXAMPLE\"";
3015 os <<
" :cvc_command \"COUNTERMODEL\"";
3018 os <<
" :cvc_command" <<
space;
3022 os <<
"\"PUSH" << space << e[0] << push <<
"\"";
3025 os <<
" :cvc_command" <<
space;
3029 os <<
"\"POP" << space << e[0] << push <<
"\"";
3032 os <<
" :cvc_command" <<
space;
3033 os <<
"\"POPTO" << space << e[0] << push <<
"\"";
break;
3035 os <<
" :cvc_command" <<
space;
3037 os <<
"\"PUSH_SCOPE\"";
3039 os <<
"\"PUSH_SCOPE" << space << e[0] << push <<
"\"";
3042 os <<
" :cvc_command" <<
space;
3044 os <<
"\"POP_SCOPE\"";
3046 os <<
"\"POP_SCOPE" << space << e[0] << push <<
"\"";
3049 os <<
" :cvc_command" <<
space;
3050 os <<
"\"POPTO_SCOPE" << space << e[0] << push <<
"\"";
break;
3053 os <<
" :cvc_command" <<
space;
3054 os <<
"\"RESET\"";
break;
3057 os <<
" :" << e[0].getString();
3058 if (e[0].getString() ==
"notes") {
3059 os << space << e[1];
3061 else if (e.arity() > 1) {
3062 os << space <<
"{" << e[1].getString() <<
"}";
3076 if (e.
arity() == 1) {
3077 for (
int i=0; i < e[0].
arity(); ++i) {
3081 os <<
"(declare-sort" <<
space
3084 }
else if (e.
arity() == 2) {
3087 throw SmtlibException(
"TheoryCore::print: SMTLIB: Unexpected TYPE expression");
3096 if(e.
arity() == 2) {
3100 if( e[1].getKind() ==
ARROW ) {
3101 os <<
nodag << e[1];
3109 throw SmtlibException(
"TheoryCore::print: SMTLIB: CONST not implemented");
3120 << e[0] <<
space << e[1] <<
push <<
")";
3124 os <<
"(" << push <<
"=" <<
space
3125 << e[0] <<
space << e[1] << push <<
")";
3129 os <<
"(" << push <<
"ite";
3131 <<
space << e[1] <<
space << e[2] << push <<
")";
3136 os <<
"(assert" <<
space << push << e[0] <<
")" <<
pop;
3141 os << push <<
"(assert" <<
space << push << e[0].
negate() << pop <<
")" << pop <<
endl;
3143 os <<
"(check-sat)";
3152 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
3153 Type tp(i->arity() == 3 ? (*i)[2].getType() : (*i)[1].getType());
3154 DebugAssert(!tp.isNull(),
"Unexpected Null type");
3156 if(i->arity() == 3) {
3162 if (first ||
contains(def, defs)) {
3164 os << push <<
")" << pop << pop <<
space;
3167 os <<
"(" << push <<
"let" <<
space <<
"(" <<
push;
3175 os <<
"(" << push << var <<
space <<
nodag << def <<
")" <<
pop;
3177 DebugAssert(!first,
"Expected at least one child");
3178 os << push <<
")" << pop << pop <<
space << e[1];
3179 for (
int j = 0; j < letCount; ++j)
3185 if (str[0] ==
'_') str[0] =
'?';
3196 os <<
"(get-assertions)";
3199 os <<
"(get-unsat-core)";
3202 os <<
"(get-model)";
3209 os <<
"(push" <<
space << push << e[0] <<
")" <<
pop;
3216 os <<
"(pop" <<
space << push << e[0] <<
")" <<
pop;
3219 os <<
" :cvc_command" <<
space
3220 <<
"\"POPTO" <<
space << e[0] << push <<
"\"";
break;
3222 os <<
" :cvc_command" <<
space
3223 <<
"\"POPTO_SCOPE" <<
space << push << e[0] <<
"\"" <<
pop;
3226 os <<
" :cvc_command" <<
space;
3227 os <<
"\"RESET\"";
break;
3230 os <<
"(set-info :" << e[0].
getString();
3249 if(e.
arity() == 0) os <<
"TYPE";
3250 else if(e.
arity() == 1)
3251 os <<
"(" <<
push <<
"TYPE" <<
space << e[0] <<
push <<
")";
3252 else if(e.
arity() == 2)
3253 os <<
"(" <<
push <<
"TYPE" <<
space << e[0]
3258 if(e.
arity() == 1 && e[0].
isString()) os << e[0].getString();
3263 os <<
"(" <<
push <<
"CONST" <<
space << e[0]
3269 os <<
"SUBTYPE(" <<
push << e[0] <<
push <<
")";
3275 else if(e[0].isString()) os << e[0].
getString();
3276 else e[0].
print(os);
3286 os <<
"(" << push <<
"=" <<
space << e[0]
3287 <<
space << e[1] << push <<
")";
3290 os <<
"(" << push <<
"NOT" <<
space << e[0] << push <<
")";
3293 int i=0, iend=e.
arity();
3294 os <<
"(" << push <<
"AND";
3295 for(; i!=iend; ++i) os <<
space << e[i];
3300 int i=0, iend=e.
arity();
3301 os <<
"(" << push <<
"OR";
3302 for(; i!=iend; ++i) os <<
space << e[i] <<
space;
3307 os <<
"(" << push <<
"IF" <<
space << e[0]
3308 <<
space << e[1] <<
space << e[2] << push <<
")";
3311 os <<
"(" << push <<
"<=>" <<
space
3312 << e[0] <<
space << e[1] << push <<
")";
3315 os <<
"(" << push <<
"=>" <<
space
3316 << e[0] <<
space << e[1] << push <<
")";
3320 os <<
"(" << push <<
"ASSERT" <<
space << e[0] << push <<
")";
3323 os <<
"(" << push <<
"TRANSFORM" <<
space << e[0] << push <<
")";
3326 os <<
"(" << push <<
"QUERY" <<
space << e[0] << push <<
")";
3329 os <<
"(PUSH)";
break;
3331 os <<
"(POP)";
break;
3333 os <<
"(" << push <<
"POPTO" <<
space << e[0] << push <<
")";
break;
3335 os <<
"(" << push <<
"RESET" << push <<
")";
break;
3337 if(e.
arity() == 2) os << e[1];
3338 else if(e.
arity()==3)
3339 os << e[0] << push <<
":" <<
space << push << e[1] << push <<
" ="
3346 os <<
"(" << push <<
"LET" <<
space <<
"(" <<
push;
3347 for(
Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i) {
3348 if(!first) os <<
space;
3351 if(i->arity() == 3) {
3352 os << (*i)[0] << space << (*i)[1]
3353 << space <<
nodag << (*i)[2];
3356 Type tp((*i)[0].lookupType());
3358 os << space <<
nodag << (*i)[1];
3360 os << push <<
")" <<
pop <<
pop;
3362 os << push <<
")" <<
pop <<
pop <<
space << e[1] << push <<
")";
3374 "Proof rule application must have at "
3375 "least one argument (rule name):\n "+e.
toString());
3376 os << push <<
"(" <<
push;
3378 for(
int i=0; i<e.
arity(); i++) {
3379 if(first) first=
false;
3388 bool firstTime(
true);
3390 if(firstTime) firstTime =
false;
3436 vector<Expr> assump;
3440 +
"]: Model Creation failed due "
3441 "to the following assumptions:\n\n"
3443 +
"\n\nYou might be using an incomplete logical fragment.");
3450 for(vector<Expr>::const_iterator i=v.begin(), iend=v.end(); i!=iend; ++i) {
3451 TRACE(
"model",
"Model var "+i->toString()+
" = ",
find(*i).
getRHS(),
"");
3452 DebugAssert((*i).getType().isBool(),
"TheoryCore::computeModel: *i = "
3482 "addFact[start]: Expected empty update list");
3503 "addFact[end]: Expected empty update list");
3513 IF_DEBUG(debugger.counter(
"DP checkSAT(fullEffort) calls")++;)
3515 "addFact[start]: Expected empty update list");
3522 "addFact[end]: Expected empty update list");
3533 reasons.push_back((*i).first);
3594 return (*iParseCache).second;
3605 const Expr c1 = e[0];
3622 const Expr& op = e[0];
3642 for(; i!=iend; ++i) args.push_back(
parseExpr(*i));
3653 vector<Expr> assignmentVars;
3655 for(
int i = 0; i < e[2].
arity(); ++i) {
3656 if(e[2][i][0][0].getString() ==
":named") {
3657 FatalAssert(e[2][i].arity() == 2 && e[2][i][1].getKind() ==
ID,
3658 ":named annotation must take a name");
3659 assignmentVars.push_back(e[2][i][1]);
3663 for(
unsigned i = 0; i < assignmentVars.size(); ++i) {
3664 d_assignment.push_back(make_pair(assignmentVars[i], parsed));
3688 if (boundVarSize == 0) {
3695 if ((*iBoundVarMap).second.getKind() ==
RAW_LIST) {
3696 (*iBoundVarMap).second = (*iBoundVarMap).second[1];
3707 (*d_parseCache)[e] = res;
3718 +
")\n variable already has a different value");
3721 Expr t2 = thm.getRHS();
3742 +
")\n variable already has a different value:\n "
3758 TRACE(
"model",
"TheoryCore::addToVarDB(", e,
")");
3765 TRACE_MSG(
"model",
"collectBasicVars() {");
3774 while(stack.size() > 0) {
3775 Expr var(stack.back());
3779 if(findThm.
getRHS()!=var) {
3781 stack.push_back(findThm.
getRHS());
3782 TRACE(
"model",
"collectBasicVars: simplified var: ", findThm.
getExpr(),
"");
3785 lastSize = stack.size();
3786 TRACE(
"model",
"getModelTerm(", var,
") {");
3788 TRACE(
"model",
"getModelTerm => ",
3790 if(stack.size() == lastSize) {
3792 TRACE(
"model",
"collectBasicVars: adding primitive var: ", var,
"");
3798 TRACE(
"model",
"collectBasicVars: adding shared var: ", var,
"");
3805 for(
size_t i=lastSize; i<stack.size(); ++i) {
3806 DebugAssert(stack[i] != var,
"Primitive var was pushed on "
3807 "the stack in computeModelTerm(): "+var.toString());
3808 kids.push_back(stack[i]);
3810 TRACE(
"model",
"collectBasicVars: var="+var.toString()
3814 TRACE_MSG(
"model",
"collectBasicVars() => }");
3821 vector<set<Expr> > theoryExprs(numTheories+1);
3827 if(findThm.
getRHS()!=var) {
3828 TRACE(
"model",
"buildModel: replace var="+var.
toString(),
" with find(var)=", findThm.
getRHS());
3835 for(; i<numTheories &&
d_theories[i] != th; ++i);
3837 theoryExprs[i].insert(var);
3843 if(theoryExprs[i].size() > 0) {
3847 vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end());
3851 vector<Expr> assump;
3868 vector<set<Expr> > theoryExprs(numTheories+1);
3873 if(findThm.
getRHS()!=var) {
3875 " with find(var)=", findThm.
getRHS());
3882 for(; i<numTheories &&
d_theories[i] != th; ++i);
3884 "TheoryCore::buildModel: cannot find the theory ["
3885 +th->
getName()+
"] for the variable: "
3887 theoryExprs[i].insert(var);
3888 TRACE(
"model",
"buildModel: adding ", var,
3893 if(theoryExprs[i].size() > 0) {
3897 vars.insert(vars.end(), theoryExprs[i].begin(), theoryExprs[i].end());
3901 vector<Expr> assump;
3905 (
"Model Creation failed in Theory["
3907 +
"] due to the following assumptions:\n\n"
3909 +
"\n\nYou might be using an incomplete logical fragment.");
3915 for(vector<Expr>::const_iterator i=
d_vars.begin(), iend=
d_vars.end(); i!=iend; ++i) {
3917 TRACE(
"model",
"buildModel: recombining var=", var,
"");
3922 TRACE(
"model",
"buildModel: simplified var="+var.
toString()+
" to ",
3956 TRACE(
"model",
"collectModelValues(", e,
") {");
3958 TRACE(
"model",
"collectModelValues[cached] => ",
3965 const Theorem& findThm = k->second;
3972 TRACE(
"model",
"collectModelValues[simplified] => ",
3978 TRACE(
"model",
"collectModelValues[e=e] => ", e,
" }");
3985 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
4005 vector<Expr> assigned;
4007 TRACE(
"model",
"computeModel["+th->
getName()+
"](", e,
") {");
4012 if(!(assigned.size()==1 && assigned[0]==e)) {
4014 for(vector<Expr>::iterator i=assigned.begin(), iend=assigned.end();
4016 if(*i == e)
continue;
4024 TRACE(
"model",
"collectModelValues => ",
4031 +
")\nExpected a literal.");
4034 bool neg(e.
isNot());
4035 const Expr a = neg? e[0] : e;
4039 else if (a.arity() > 1)
4059 d_timeBase = clock() / (CLOCKS_PER_SEC / 10);
4096 string indentStr(
getCM()->scopeLevel(),
' ');
4097 TRACE(
"facts", indentStr,
"assertEqualities: ", e);
4100 TRACE(
"quant update",
"equs in core ", e.
getExpr(),
"");
4109 DebugAssert(lhs != rhs,
"expected different lhs and rhs");
4127 vector<Theorem> eqs;
4131 for (index = 0; index < conj.
arity(); ++index) {
4147 vector<Theorem>::iterator i = eqs.begin(), iend = eqs.end();
4148 for(; i!=iend; ++i) {
4154 +
"\n\n find(lhs) = "
4158 +
"\n\n find(rhs) = "
4194 if (e.
getFlag())
return false;
4197 for (
int i = 0, ar = e.
arity(); i < ar; ++i) {
4205 static bool hasBoundVar(
const Expr& e)
4221 "enqueueFact() is called outside of addFact()"
4222 " or checkSATCore() or registerAtom() or preprocess");
4224 && !hasBoundVar(e.
getRHS())) ||
4226 "Bound vars shouldn't be free: " + e.
toString());
4254 for(
unsigned i=1; i <
d_theories.size(); ++i) {
4269 for (k = 0; k < t.
arity(); ++k) {
4277 TRACE(
"quant",
"pushed pred ",t,thm);
4299 for (k = 0; k < t.
arity(); ++k) {
4311 IF_DEBUG(debugger.counter(
"conflicts from type predicate")++;)
4314 else if(!predExpr.
isTrue()) {
4327 pr.push_back(simpThm.
getRHS());