diff options
| -rw-r--r-- | src/theory/arith/partial_model.cpp | 44 | ||||
| -rw-r--r-- | src/theory/arith/partial_model.h | 7 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 262 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 16 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fuzz_3.smt | 46 |
6 files changed, 302 insertions, 76 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 4b113257c..33c690276 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -27,21 +27,28 @@ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); if(d_savingAssignments){ - d_history.push_back(make_pair(x,r)); + DeltaRational current = getAssignment(x); + d_history.push_back(make_pair(x,current)); } - DeltaRational* c; - if(x.getAttribute(partial_model::Assignment(), c)){ - *c = r; - Debug("partial_model") << "pm: updating the assignment to" << x - << " now " << r <<endl; - }else{ - Debug("partial_model") << "pm: constructing an assignment for " << x - << " initially " << r <<endl; + Assert(x.hasAttribute(partial_model::Assignment())); - c = new DeltaRational(r); - x.setAttribute(partial_model::Assignment(), c); - } + DeltaRational* c = x.getAttribute(partial_model::Assignment()); + *c = r; + Debug("partial_model") << "pm: updating the assignment to" << x + << " now " << r <<endl; +} + +void ArithPartialModel::initialize(TNode x, const DeltaRational& r){ + Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + + + Assert(!x.hasAttribute(partial_model::Assignment())); + DeltaRational* c = new DeltaRational(r); + x.setAttribute(partial_model::Assignment(), c); + + Debug("partial_model") << "pm: constructing an assignment for " << x + << " initially " << (*c) <<endl; } /** Must know that the bound exists both calling this! */ @@ -72,6 +79,19 @@ DeltaRational ArithPartialModel::getAssignment(TNode x) const{ return *assign; } +DeltaRational ArithPartialModel::getSavedAssignment(TNode x) const{ + Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + if(d_savingAssignments){ + for(HistoryStack::const_iterator i = d_history.begin(); i != d_history.end(); ++i){ + pair<TNode, DeltaRational> curr = *i; + if(curr.first == x){ + return DeltaRational(curr.second); + } + } + } + return getAssignment(x); +} + void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 01db59855..57996a510 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -115,7 +115,7 @@ public: /* */ void stopRecordingAssignments(bool revert); - + bool isRecording() { return d_savingAssignments; } void setUpperBound(TNode x, const DeltaRational& r); void setLowerBound(TNode x, const DeltaRational& r); @@ -144,6 +144,11 @@ public: bool assignmentIsConsistent(TNode x); void printModel(TNode x); + + void initialize(TNode x, const DeltaRational& r); + + DeltaRational getSavedAssignment(TNode x) const; + }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1dbf818b3..3ca3245dd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -43,6 +43,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : { uint64_t ass_id = partial_model::Assignment::getId(); Debug("arithsetup") << "Assignment: " << ass_id << std::endl; + + d_partialModel.beginRecordingAssignments(); } TheoryArith::~TheoryArith(){ for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ @@ -66,11 +68,17 @@ void TheoryArith::preRegisterTerm(TNode n) { d_splits.push_back(eagerSplit); + n.setAttribute(EagerlySplitUpon(), true); d_out->augmentingLemma(eagerSplit); } } + if(n.getMetaKind() == metakind::VARIABLE){ + + setupVariable(n); + } + Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm(" << n << ")" << endl; } @@ -90,18 +98,6 @@ bool isBasicSum(TNode n){ return true; } -Kind multKind(Kind k){ - switch(k){ - case LT: return GT; - case LEQ: return GEQ; - case EQUAL: return EQUAL; - case GEQ: return LEQ; - case GT: return LT; - default: - Unhandled(); - } - return NULL_EXPR; -} void registerAtom(TNode rel){ @@ -110,6 +106,72 @@ void registerAtom(TNode rel){ } +/* Requirements: + * Variable must have been set to be basic. + * For basic variables the row must have been added to the tableau. + */ +void TheoryArith::setupVariable(TNode x){ + Assert(x.getMetaKind() == kind::metakind::VARIABLE); + d_variables.push_back(Node(x)); + + if(!isBasic(x)){ + d_partialModel.initialize(x,d_constants.d_ZERO_DELTA); + }else{ + //If the variable is basic, assertions may have already happened and updates + //may have occured before setting this variable up. + + //This can go away if the tableau creation is done at preregister + //time instead of register + + DeltaRational q = computeRowValueUsingSavedAssignment(x); + if(!(q == d_constants.d_ZERO_DELTA)){ + Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl; + } + d_partialModel.initialize(x,q); + + q = computeRowValueUsingAssignment(x); + if(!(q == d_constants.d_ZERO_DELTA)){ + Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl; + } + d_partialModel.setAssignment(x,q); + } + Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl; +}; + +/** + * Computes the value of a basic variable using the current assignment. + */ +DeltaRational TheoryArith::computeRowValueUsingAssignment(TNode x){ + Assert(isBasic(x)); + DeltaRational sum = d_constants.d_ZERO_DELTA; + + Row* row = d_tableau.lookup(x); + for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){ + TNode nonbasic = *i; + Rational& coeff = row->lookup(nonbasic); + DeltaRational assignment = d_partialModel.getAssignment(nonbasic); + sum = sum + (assignment * coeff); + } + return sum; +} + +/** + * Computes the value of a basic variable using the current assignment. + */ +DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ + Assert(isBasic(x)); + DeltaRational sum = d_constants.d_ZERO_DELTA; + + Row* row = d_tableau.lookup(x); + for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){ + TNode nonbasic = *i; + Rational& coeff = row->lookup(nonbasic); + DeltaRational assignment = d_partialModel.getSavedAssignment(nonbasic); + sum = sum + (assignment * coeff); + } + return sum; +} + Node TheoryArith::rewrite(TNode n){ Debug("arith") << "rewrite(" << n << ")" << endl; @@ -126,10 +188,6 @@ void TheoryArith::registerTerm(TNode tn){ if(tn.getKind() == kind::BUILTIN) return; - if(tn.getMetaKind() == metakind::VARIABLE){ - - setupVariable(tn); - } //TODO is an atom if(isRelationOperator(tn.getKind())){ @@ -152,11 +210,11 @@ void TheoryArith::registerTerm(TNode tn){ TypeNode real_type = NodeManager::currentNM()->realType(); slack = NodeManager::currentNM()->mkVar(real_type); - setupVariable(slack); - left.setAttribute(Slack(), slack); makeBasic(slack); + + Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); slackEqLeft.setAttribute(TheoryArithPropagated(), true); //TODO this has to be wrong no? YES (dejan) @@ -166,6 +224,8 @@ void TheoryArith::registerTerm(TNode tn){ d_tableau.addRow(slackEqLeft); + setupVariable(slack); + Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right); registerAtom(rewritten); }else{ @@ -182,7 +242,7 @@ void TheoryArith::registerTerm(TNode tn){ } /* procedure AssertUpper( x_i <= c_i) */ -void TheoryArith::AssertUpper(TNode n, TNode original){ +bool TheoryArith::AssertUpper(TNode n, TNode original){ TNode x_i = n[0]; Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind()))); DeltaRational c_i(n[1].getConst<Rational>(), dcoeff); @@ -192,12 +252,14 @@ void TheoryArith::AssertUpper(TNode n, TNode original){ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ - return; //sat + return false; //sat } if(d_partialModel.belowLowerBound(x_i, c_i, true)){ - Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getLowerConstraint(x_i), original); + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; d_out->conflict(conflict); - return; + return true; } d_partialModel.setUpperConstraint(x_i,original); @@ -208,10 +270,12 @@ void TheoryArith::AssertUpper(TNode n, TNode original){ update(x_i, c_i); } } + d_partialModel.printModel(x_i); + return false; } /* procedure AssertLower( x_i >= c_i ) */ -void TheoryArith::AssertLower(TNode n, TNode orig){ +bool TheoryArith::AssertLower(TNode n, TNode original){ TNode x_i = n[0]; Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind()))); DeltaRational c_i(n[1].getConst<Rational>(),dcoeff); @@ -219,15 +283,17 @@ void TheoryArith::AssertLower(TNode n, TNode orig){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; if(d_partialModel.belowLowerBound(x_i, c_i, false)){ - return; //sat + return false; //sat } if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ - Node conflict = NodeManager::currentNM()->mkNode(AND, d_partialModel.getUpperConstraint(x_i), orig); + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); d_out->conflict(conflict); - return; + Debug("arith") << "AssertLower conflict " << conflict << endl; + return true; } - d_partialModel.setLowerConstraint(x_i,orig); + d_partialModel.setLowerConstraint(x_i,original); d_partialModel.setLowerBound(x_i, c_i); if(!isBasic(x_i)){ @@ -235,6 +301,9 @@ void TheoryArith::AssertLower(TNode n, TNode orig){ update(x_i, c_i); } } + //d_partialModel.printModel(x_i); + + return false; } void TheoryArith::update(TNode x_i, DeltaRational& v){ @@ -261,9 +330,15 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ } d_partialModel.setAssignment(x_i, v); + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } } void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ + Assert(x_i != x_j); + Row* row_i = d_tableau.lookup(x_i); Rational& a_ij = row_i->lookup(x_j); @@ -293,7 +368,10 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ } d_tableau.pivot(x_i, x_j); - d_tableau.printTableau(); + + if(debugTagIsOn("tableau")){ + d_tableau.printTableau(); + } } TNode TheoryArith::selectSmallestInconsistentVar(){ @@ -352,13 +430,30 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 Debug("arith") << "updateInconsistentVars" << endl; - d_partialModel.beginRecordingAssignments(); + while(true){ + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + TNode x_i = selectSmallestInconsistentVar(); Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == Node::null()){ Debug("arith_update") << "No inconsistent variables" << endl; + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + d_partialModel.stopRecordingAssignments(false); + d_partialModel.beginRecordingAssignments(); + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + + + return Node::null(); //sat } DeltaRational beta_i = d_partialModel.getAssignment(x_i); @@ -367,21 +462,41 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational l_i = d_partialModel.getLowerBound(x_i); TNode x_j = selectSlackBelow(x_i); if(x_j == TNode::null() ){ + Debug("arith_update") << "conflict below" << endl; + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + d_partialModel.stopRecordingAssignments(true); + d_partialModel.beginRecordingAssignments(); + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + return generateConflictBelow(x_i); //unsat } - d_partialModel.printModel(x_i); - d_partialModel.printModel(x_j); pivotAndUpdate(x_i, x_j, l_i); + }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ DeltaRational u_i = d_partialModel.getUpperBound(x_i); TNode x_j = selectSlackAbove(x_i); if(x_j == TNode::null() ){ + Debug("arith_update") << "conflict above" << endl; + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } + d_partialModel.stopRecordingAssignments(true); + d_partialModel.beginRecordingAssignments(); + + if(debugTagIsOn("paranoid:check_tableau")){ + checkTableau(); + } return generateConflictAbove(x_i); //unsat } - d_partialModel.printModel(x_i); - d_partialModel.printModel(x_j); pivotAndUpdate(x_i, x_j, u_i); } } @@ -395,6 +510,7 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ Debug("arith") << "generateConflictAbove " << "conflictVar " << conflictVar + << " " << d_partialModel.getAssignment(conflictVar) << " " << bound << endl; nb << bound; @@ -409,11 +525,13 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ if(a_ij < d_constants.d_ZERO){ bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "below 0 "<< nonbasic << " " << bound << endl; + Debug("arith") << "below 0 " << nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " " << bound << endl; nb << bound; }else{ bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << " above 0 "<< nonbasic << " " << bound << endl; + Debug("arith") << " above 0 " << nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " " << bound << endl; nb << bound; } } @@ -429,6 +547,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ Debug("arith") << "generateConflictBelow " << "conflictVar " << conflictVar + << d_partialModel.getAssignment(conflictVar) << " " << " " << bound << endl; nb << bound; @@ -442,12 +561,14 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ if(a_ij < d_constants.d_ZERO){ TNode bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << "Lower "<< nonbasic << " " << bound << endl; + Debug("arith") << "Lower "<< nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl; nb << bound; }else{ TNode bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "Upper "<< nonbasic << " " << bound << endl; + Debug("arith") << "Upper "<< nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl; nb << bound; } @@ -503,11 +624,14 @@ Node TheoryArith::simulatePreprocessing(TNode n){ void TheoryArith::check(Effort level){ Debug("arith") << "TheoryArith::check begun" << std::endl; + bool conflictDuringAnAssert = false; + while(!done()){ + //checkTableau(); Node original = get(); Node assertion = simulatePreprocessing(original); Debug("arith_assertions") << "arith assertion(" << original - << " \\-> " << assertion << ")" << std::endl; + << " \\-> " << assertion << ")" << std::endl; d_preprocessed.push_back(assertion); @@ -516,14 +640,14 @@ void TheoryArith::check(Effort level){ Warning() << "No bools should be reached dagnabbit" << endl; break; case LEQ: - AssertUpper(assertion, original); + conflictDuringAnAssert = AssertUpper(assertion, original); break; case GEQ: - AssertLower(assertion, original); + conflictDuringAnAssert = AssertLower(assertion, original); break; case EQUAL: - AssertUpper(assertion, original); - AssertLower(assertion, original); + conflictDuringAnAssert = AssertUpper(assertion, original); + conflictDuringAnAssert |= AssertLower(assertion, original); break; case NOT: { @@ -532,13 +656,13 @@ void TheoryArith::check(Effort level){ case LEQ: //(not (LEQ x c)) <=> (GT x c) { Node pushedin = pushInNegation(assertion); - AssertLower(pushedin,original); + conflictDuringAnAssert = AssertLower(pushedin,original); break; } case GEQ: //(not (GEQ x c) <=> (LT x c) { Node pushedin = pushInNegation(assertion); - AssertUpper(pushedin,original); + conflictDuringAnAssert = AssertUpper(pushedin,original); break; } case EQUAL: @@ -556,11 +680,20 @@ void TheoryArith::check(Effort level){ Unhandled(); } } + if(conflictDuringAnAssert){ + //clear the queue; + while(!done()) { + get(); + } + //return + return; + } if(fullEffort(level)){ Node possibleConflict = updateInconsistentVars(); if(possibleConflict != Node::null()){ - Debug("arith_conflict") << "Found a conflict " << possibleConflict << endl; + Debug("arith_conflict") << "Found a conflict " + << possibleConflict << endl; d_out->conflict(possibleConflict); }else{ Debug("arith_conflict") << "No conflict found" << endl; @@ -598,15 +731,38 @@ void TheoryArith::check(Effort level){ //Warning() << "Outstanding case split in theory arith" << endl; } } - if(debugTagIsOn("model")){ - for(vector<Node>::iterator i=d_variables.begin(); - i!= d_variables.end(); - ++i){ - Node var = *i; - d_partialModel.printModel(var); - } - } Debug("arith") << "TheoryArith::check end" << std::endl; } + +/** + * This check is quite expensive. + * It should be wrapped in a debugTagIsOn guard. + * if(debugTagIsOn("paranoid:check_tableau")){ + * checkTableau(); + * } + */ +void TheoryArith::checkTableau(){ + + for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + basicIter != d_tableau.end(); ++basicIter){ + TNode basic = *basicIter; + Row* row_k = d_tableau.lookup(basic); + DeltaRational sum; + Debug("paranoid:check_tableau") << "starting row" << basic << endl; + for(std::set<TNode>::iterator nonbasicIter = row_k->begin(); + nonbasicIter != row_k->end(); + ++nonbasicIter){ + TNode nonbasic = *nonbasicIter; + Rational& coeff = row_k->lookup(nonbasic); + DeltaRational beta = d_partialModel.getAssignment(nonbasic); + Debug("paranoid:check_tableau") << nonbasic << beta << coeff<<endl; + sum = sum + (beta*coeff); + } + DeltaRational shouldBe = d_partialModel.getAssignment(basic); + Debug("paranoid:check_tableau") << "ending row" << sum << "," << shouldBe << endl; + + Assert(sum == shouldBe); + } +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1d6cca5cc..ade63b6c9 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -76,8 +76,8 @@ public: void explain(TNode n, Effort e) { Unimplemented(); } private: - void AssertLower(TNode n, TNode orig); - void AssertUpper(TNode n, TNode orig); + bool AssertLower(TNode n, TNode orig); + bool AssertUpper(TNode n, TNode orig); void update(TNode x_i, DeltaRational& v); void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v); @@ -90,15 +90,13 @@ private: Node generateConflictAbove(TNode conflictVar); Node generateConflictBelow(TNode conflictVar); + void setupVariable(TNode x); + DeltaRational computeRowValueUsingAssignment(TNode x); + DeltaRational computeRowValueUsingSavedAssignment(TNode x); + void checkTableau(); + //TODO get rid of this! Node simulatePreprocessing(TNode n); - void setupVariable(TNode x){ - Assert(x.getMetaKind() == kind::metakind::VARIABLE); - d_partialModel.setAssignment(x,d_constants.d_ZERO_DELTA); - d_variables.push_back(Node(x)); - - Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl; - }; }; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 515d496f5..0b8a60495 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ wiki.18.cvc \ wiki.19.cvc \ wiki.20.cvc \ - wiki.21.cvc + wiki.21.cvc \ + fuzz_3.smt if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/fuzz_3.smt b/test/regress/regress0/fuzz_3.smt new file mode 100644 index 000000000..e1c53d2c3 --- /dev/null +++ b/test/regress/regress0/fuzz_3.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_LRA +:extrafuns ((v0 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v1 Real)) +:status sat +:formula +(let (?n1 2) +(let (?n2 (* ?n1 ?n1)) +(let (?n3 (~ v0)) +(let (?n4 (* ?n1 ?n3)) +(let (?n5 (- ?n1 ?n1)) +(let (?n6 (- ?n5 v0)) +(let (?n7 (- ?n4 ?n6)) +(flet ($n8 (= ?n2 ?n7)) +(flet ($n9 false) +(let (?n10 (ite $n9 ?n1 v1)) +(let (?n11 (+ ?n1 v2)) +(flet ($n12 (<= ?n10 ?n11)) +(let (?n13 (ite $n9 v0 ?n2)) +(let (?n14 (~ ?n1)) +(let (?n15 (ite $n9 ?n14 ?n1)) +(flet ($n16 (< ?n13 ?n15)) +(flet ($n17 (= ?n1 ?n7)) +(let (?n18 (+ ?n1 ?n1)) +(flet ($n19 (= v2 ?n18)) +(let (?n20 (ite $n19 v2 ?n1)) +(let (?n21 (ite $n17 ?n18 ?n20)) +(flet ($n22 (>= ?n21 ?n2)) +(let (?n23 (ite $n9 ?n21 ?n2)) +(flet ($n24 (<= ?n23 ?n1)) +(flet ($n25 (> ?n7 ?n2)) +(flet ($n26 (iff $n24 $n25)) +(let (?n27 (~ ?n7)) +(flet ($n28 (<= ?n27 ?n1)) +(let (?n29 (ite $n28 ?n1 ?n1)) +(flet ($n30 (< ?n1 ?n29)) +(flet ($n31 (implies $n26 $n30)) +(flet ($n32 (implies $n9 $n9)) +(flet ($n33 (if_then_else $n22 $n31 $n32)) +(flet ($n34 (and $n9 $n33)) +(flet ($n35 (if_then_else $n16 $n34 $n9)) +(flet ($n36 (iff $n12 $n35)) +(flet ($n37 (and $n8 $n36)) +$n37 +)))))))))))))))))))))))))))))))))))))) |