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());
CDO< bool > d_inconsistent
Inconsistent flag.
ExprStream & popSave(ExprStream &os)
Remember the current indentation and pop to the previous position.
ExprStream & pop(ExprStream &os)
Restore the indentation.
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
for output in SPASS format
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin() const
Begin iterator.
Theory * d_solver
The theory which has the solver (if any)
TheoryCore * d_theoryCore
Provides the core functionality.
ExprStream & nodag(ExprStream &os)
virtual Theorem rewriteAtomic(const Expr &e)
Theory-specific rewrites for atomic formulas.
bool isAtomic() const
Test if e is atomic.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
std::hash_map< Expr, Theorem > d_termTheorems
Map from active terms to theorems that introduced those terms.
EffortLevel
Effort level for processFactQueue.
static bool containsRec(const Expr &def, ExprHashMap< bool > &defs, ExprHashMap< bool > &visited)
_hash_table::iterator iterator
void setRewriteNormal() const
void setFlag() const
Set the generic flag.
const std::string fixConstName(const std::string &s)
CDList< Expr > d_terms
List of all active terms in the system (for quantifier instantiation)
Data structure of expressions in CVC3.
void assertFormula(const Theorem &e)
Process a newly derived formula.
void computeType(const Expr &e)
Compute and store the type of e.
ExprHashMap< Theorem > d_varAssignments
Mapping of intermediate variables to their values.
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
CoreProofRules * createProofRules(TheoremManager *tm)
Private method to get a new theorem producer.
An exception thrown by the parser.
PrettyPrinterCore(TheoryCore *core)
Constructor.
static bool contains(const Expr &def, ExprHashMap< bool > &defs)
unsigned d_timeBase
Time limit (0==unlimited, >0==total available cpu time in seconds).
Expr processCond(const Expr &e, int i)
An auxiliary recursive function to process COND expressions into ITE.
const CLFlags & getFlags() const
void enqueueFact(const Theorem &e)
Enqueue a new fact.
CoreProofRules * d_rules
Core proof rules.
void computeType(const Expr &e)
Compute the type of e.
void addToVarDB(const Expr &e)
Adds expression to var database.
bool hasTheory(int kind)
Test whether a kind maps to any theory.
void setStoredPredicate() const
Set the Stored Predicate flag for this Expr.
void addToNotify(Theory *i, const Expr &e) const
Add (e,i) to the notify list of this expression.
virtual Theorem rewriteIteToIff(const Expr &e)=0
==> ITE(a, b, !b) IFF IFF(a, b)
ostream & operator<<(ostream &os, const Expr &e)
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
bool isStoredPredicate() const
const Expr & boolExpr()
BOOLEAN Expr.
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
Type newSubtypeExpr(const Expr &pred, const Expr &witness)
Create a new subtype expression.
std::string d_name
Name of the theory (for debugging)
ExprStream & print(ExprStream &os, const Expr &e)
The pretty-printer which subclasses must implement.
Expr resolveID(const std::string &name)
Resolve an identifier, for use in parseExprOp()
virtual Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void setupSubFormulas(const Expr &s, const Expr &e, const Theorem &thm)
Helper for registerAtom.
bool isImpliedLiteral() const
void setIncomplete(const std::string &reason)
Mark the branch as incomplete.
virtual Theorem rewriteIteCond(const Expr &e)=0
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
void setFind(const Theorem &e) const
Set the find attribute to e.
for output in TPTP format
void insert(const Key &k, const Data &d, int scope=-1)
void unregisterPrettyPrinter()
Tell ExprManager that the printer is no longer valid.
MS C++ specific settings.
ContextManager * d_cm
Context manager.
CDList< Theorem > d_impliedLiterals
List of implied literals, based on registered atomic formulas of interest.
void initTimeLimit()
Initialize base time used for !setTimeLimit.
virtual Theorem iffFalseElim(const Theorem &e)=0
Lisp-like format for automatically generated specs.
Type lookupType() const
Look up the current type. Do not recursively compute (i.e. may be NULL)
Expr eqExpr(const Expr &right) const
Expr getExpr(int i) const
virtual Theorem rewriteIteToAnd(const Expr &e)=0
==> ITE(a, b, FALSE) IFF AND(a, b)
Theory * getTheory(int i) const
ExprStream & space(ExprStream &os)
Insert a single white space separator.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
std::vector< std::pair< std::string, Expr > > d_boundVarStack
Bound variable stack: a vector of pairs
virtual Theorem reflexivityRule(const Expr &a)=0
void registerPrettyPrinter(PrettyPrinter &printer)
Register the pretty-printer (can only do it if none registered)
bool incomplete()
Check if the current decision branch is marked as incomplete.
Expr parseExpr(const Expr &e)
Parse the generic expression.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
#define DebugAssert(cond, str)
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
bool inUserAssumption() const
bool isType() const
Expr represents a type.
Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool inconsistent()
Check if the current context is inconsistent.
Theorem rewriteLiteral(const Expr &e)
Called by search engine.
unsigned getQuantLevelForTerm(const Expr &e)
Get quantification level at which this term was introduced.
void registerTypeComputer(TypeComputer *typeComputer)
Register type computer.
Theorem callTheoryPreprocess(const Expr &e)
Call theory-specific preprocess routines.
T & push_back(const T &data, int scope=-1)
IF_DEBUG(static bool hasBoundVar(const Expr &e){e.getEM() ->clearFlags();return hasBoundVarRec(e);}) void TheoryCore
iterator find(const key_type &key)
operations
CDMap< std::string, bool > d_incomplete
The set of reasons for incompleteness (empty when we are complete)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
std::vector< Theory * > d_theories
Array of registered theories.
Expr orExpr(const std::vector< Expr > &children)
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
void setValidType() const
#define TRACE_MSG(flag, msg)
TypeComputerCore(TheoryCore *core)
const Expr & getExpr() const
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
e1 AND (e1 IFF e2) ==> e2
bool checkSATCore()
To be called by SearchEngine when it believes the context is satisfiable.
ExprTransform * d_exprTrans
Expr Transformer.
Theorem getModelValue(const Expr &e)
Enqueue a fact to be sent to the SearchEngine.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Theorem getImpliedLiteralByIndex(unsigned index)
Return an implied literal by index.
void getResource()
Request a unit of resource.
Implementation of PrettyPrinter class.
std::vector< Theorem > d_update_thms
List of theorems from calls to update()
virtual Theorem rewriteIteToOr(const Expr &e)=0
==> ITE(a, TRUE, b) IFF OR(a, b)
virtual Theorem iffTrue(const Theorem &e)=0
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
NotifyList d_notifyEq
Notify list that gets processed on every equality.
ExprHashMap< Theorem > d_simplifiedModelVars
Mapping of basic variables to simplified expressions (temp. storage)
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 Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Identifier is (ID (STRING_EXPR "name"))
void refineCounterExample()
Calls for other theories to add facts to refine a coutnerexample.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
CommonProofRules * getRules() const
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
ExprMap< Expr > * d_parseCache
Current cache being used for parser.
Abstract class for computing expr type.
std::string toString() const
Print the expression to a string.
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
virtual Theorem rewriteIteToNot(const Expr &e)=0
==> ITE(e, FALSE, TRUE) IFF NOT(e)
ExprStream & pushRestore(ExprStream &os)
Set the indentation to the position saved by popSave()
Expr getAssignment()
Get the value of all :named terms.
virtual void computeType(const Expr &e)
Compute and store the type of e.
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
void setImpliedLiteral() const
bool validSimpCache() const
Return true if there is a valid cached value for calling simplify on this Expr.
virtual Theorem rewriteIteSame(const Expr &e)=0
==> ITE(c, e, e) == e
virtual void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
static bool hasBoundVarRec(const Expr &e)
Expr iffExpr(const Expr &right) const
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const Theorem & getEqNext() const
unsigned getQuantLevel() const
Return quantification level for this theorem.
const Theorem & getSimpCache() const
const Expr & falseExpr()
FALSE Expr.
CoreSatAPI * d_coreSatAPI
Expr newLeafExpr(const Op &op)
ExprManager::TypeComputer * d_typeComputer
Type Computer.
Theorem getImpliedLiteral(void)
Return the next implied literal (NULL Theorem if none)
virtual Theorem rewriteIteToImp(const Expr &e)=0
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
const Expr & unnegate() const
Remove leading NOT if any.
virtual Theorem typePred(const Expr &e)=0
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
void collectModelValues(const Expr &e, ExprMap< Expr > &m)
Recursively build a compound-type variable assignment for e.
const Expr & getBody() const
Get the body of the closure Expr.
void clearRewriteNormal() const
std::string int2string(int n)
virtual Theorem rewriteAndSubterms(const Expr &e, int idx)=0
(a & b) <=> a & b[a/true]; takes the index of a
CDO< Theorem > d_incThm
Proof of inconsistent.
const Expr & getRHS() const
const std::string & getName() const
Get the name of the theory (for debugging purposes)
Theorem rewriteCore(const Theorem &e)
Transitive composition of other rewrites with the above.
void collectBasicVars()
Split compound vars into basic type variables.
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
std::string toString() const
void setRegisteredAtom() const
Set the RegisteredAtom flag for this Expr.
const Expr & trueExpr()
TRUE Expr.
const Expr & falseExpr()
Return FALSE Expr.
const Expr & trueExpr()
Return TRUE Expr.
Expr addBoundVar(const std::string &name, const Type &type)
Create and add a new bound variable to the stack, for parseExprOp().
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void clearFlags()
Clears the generic Expr flag in all Exprs.
std::hash_map< std::string, Expr > d_boundVarMap
Map for bound vars.
virtual void assertTypePred(const Expr &e, const Theorem &pred)
Receives all the type predicates for the types of the given theory.
void setSimpCache(const Theorem &e) const
const std::string quoteAnnotation(const std::string &s)
std::vector< Expr > d_basicModelVars
List of basic variables (temporary storage for model generation)
NotifyList * getNotify() const
bool getFlag() const
Check if the generic flag is set.
static Type anyType(ExprManager *em)
virtual Theorem rewriteDistinct(const Expr &e)=0
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
ExprManager * getEM()
Access to ExprManager.
void checkEquation(const Theorem &thm)
Helper check functions for solve.
CDO< unsigned > d_impliedLiteralsIdx
Next index in d_impliedLiterals that has not yet been fetched.
Expr getValue(Expr e)
Get the value of an arbitrary formula or term.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
void checkType(const Expr &e)
Check that e is a valid Type expr.
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...
const std::string & getName() const
void setInconsistent(const Theorem &e)
bool processFactQueue(EffortLevel effort=NORMAL)
A helper function for addFact()
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
virtual Theorem rewriteLetDecl(const Expr &e)=0
Replace LETDECL with its definition.
virtual Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
virtual Theorem solve(const Theorem &e)
An optional solver.
ContextManager * getCM() const
virtual void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
Translator * d_translator
Translator.
ExprStream & printSmtLibShared(ExprStream &os, const Expr &e)
bool isRegisteredAtom() const
void setType(const Type &t) const
Set the cached type.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
PrettyPrinterCore()
Disable the default constructor.
bool isQuantifier() const
virtual Theorem xorToIff(const Expr &e)=0
virtual Theorem simplifyOp(const Expr &e)
Recursive simplification step.
bool findReduced(const Expr &e)
Return true iff e is find-reduced.
int getNumTheories()
Return the number of registered theories.
Type boolType()
Return BOOLEAN type.
Theorem getTheoremForTerm(const Expr &e)
Get theorem which was responsible for introducing this term.
std::string to_lower(const std::string &src)
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
std::string to_upper(const std::string &src)
ExprHashMap< std::vector< Expr > > d_varModelMap
Mapping of compound type variables to simpler types (model generation)
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
virtual Theorem iffContrapositive(const Theorem &thm)=0
e1 <=> e2 ==> ~e1 <=> ~e2
An exception to be thrown by the smtlib translator.
iterator find(const Expr &e)
An exception to be thrown by the smtlib translator.
bool isAbsLiteral() const
Test if e is an abstract literal.
Theorem typePred(const Expr &e)
Return a theorem for the type predicate of e.
Proof rules used by theory_core.
bool outOfResources()
Return true if resources are exhausted.
Definition of the API to expression package. See class Expr for details.
const std::string escapeSymbol(const std::string &s)
virtual Theorem rewriteIff(const Expr &e)=0
==> (e1 <=> e2) <=> [simplified expr]
Theorem inconsistentThm()
Get the proof of inconsistency for the current context.
void checkType(const Expr &e)
Check that e is a valid Type expr.
virtual Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)=0
void assertEqualities(const Theorem &e)
Assert a system of equations (1 or more).
Op mkOp() const
Make the expr into an operator.
const Expr & getLHS() const
void setEqNext(const Theorem &e) const
Set the eqNext attribute to e.
ExprMap< Expr > d_parseCacheTop
Top-level cache for parser.
Expr getTCC(const Expr &e)
Compute the TCC of e, or the subtyping predicate, if e is a type.
bool isRewriteNormal() const
std::vector< Theorem > d_queueSE
Queue of facts to be sent to the SearchEngine.
virtual Theorem rewriteOrSubterms(const Expr &e, int idx)=0
(a | b) <=> a | b[a/false]; takes the index of a
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem rewriteIte(const Expr &e)
Derived rule for rewriting ITE.
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
virtual Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
CDList< Expr > d_predicates
List of all active non-equality atomic formulas in the system (for quantifier instantiation) ...
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.
std::queue< Theorem > d_queue
Assertion queue.
Theorem reflexivityRule(const Expr &a)
==> a == a
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
CommonProofRules * d_commonRules
Commonly used proof rules.
Cardinality
Enum for cardinality of types.
void processNotify(const Theorem &e, NotifyList *L)
Process a notify list triggered as a result of new theorem e.
ExprIndex getIndex() const
PrettyPrinter * d_printer
PrettyPrinter (we own it)
bool okToEnqueue()
Whether its OK to add new facts (for use in rewrites)
const std::string & getString() const
Manager for multiple contexts. Also holds current context.
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
InputLanguage lang() const
Get the current output language.
void setFindLiteral(const Theorem &thm)
Set the find pointer of an atomic formula and notify SearchEngine.
Expr andExpr(const std::vector< Expr > &children)
std::vector< Expr > d_vars
List of variables that were created up to this point.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
void update(const Theorem &e, const Expr &d)
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
std::vector< std::pair< Expr, Expr > > d_assignment
The set of named expressions to evaluate on a GET_ASSIGNMENT request.
for output into Simplify format
virtual Theorem andElim(const Theorem &e, int i)=0
virtual Theorem addAssumption(const Expr &assump)=0
Add an assumption to the set of assumptions in the current context.
std::vector< Expr > d_update_data
List of data accompanying above theorems from calls to update()
Abstract API to a pretty-printer for Expr.
A class which sets a boolean value to true when created, and resets to false when deleted...
virtual Theorem rewriteImplies(const Expr &e)=0
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
bool isBasicKind(int kind)
Return true if no special parsing is required for this kind.
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
void buildModel(ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.
Nice SAL-like language for manually written specs.
virtual Theorem iffTrueElim(const Theorem &e)=0
Theorem rewriteLitCore(const Expr &e)
Core rewrites for literals (NOT and EQ)
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
void checkSolved(const Theorem &thm)
Helper check functions for solve.
void setTimeLimit(unsigned limit)
Set the time limit in seconds (0==unlimited).
iterator end() const
End iterator.