From: Tim King Date: Wed, 13 Jun 2012 20:37:43 +0000 (+0000) Subject: - Added a loop to internally assert constraints that are marked as true. X-Git-Tag: cvc5-1.0.0~8032 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0b33af0cf910ca7adb0357dad13e7e88baedebc;p=cvc5.git - Added a loop to internally assert constraints that are marked as true. - Changes how CongruenceManager reports conflicts. - ConstraintDatabase can now detect and raise conflicts when doing unate propagation. --- diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 649e34134..14d2370ab 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -7,8 +7,9 @@ namespace CVC4 { namespace theory { namespace arith { -ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node) - : d_conflict(c), +ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict) + : d_inConflict(c), + d_raiseConflict(raiseConflict), d_notify(*this), d_keepAlive(c), d_propagatations(c), @@ -112,7 +113,7 @@ bool ArithCongruenceManager::propagate(TNode x){ ++(d_statistics.d_conflicts); Node conf = flattenAnd(explainInternal(x)); - d_conflict.set(conf); + raiseConflict(conf); Debug("arith::congruenceManager") << "rewritten to false "< d_conflict; + context::CDRaised d_inConflict; + NodeCallBack& d_raiseConflict; /** * The set of ArithVars equivalent to a pair of terms. @@ -101,17 +102,18 @@ private: eq::EqualityEngine d_ee; + void raiseConflict(Node conflict){ + Assert(!inConflict()); + Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl; + d_inConflict.raise(); + d_raiseConflict(conflict); + } public: bool inConflict() const{ - return d_conflict.isSet(); + return d_inConflict.isRaised(); }; - Node conflict() const{ - Assert(inConflict()); - return d_conflict.get(); - } - bool hasMorePropagations() const { return !d_propagatations.empty(); } @@ -182,7 +184,7 @@ private: public: - ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&); + ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack& setLiteral, const ArithVarNodeMap&, NodeCallBack& raiseConflict); Node explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d451e9597..bedb91756 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -448,7 +448,7 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm, NodeCallBack& raiseConflict) : d_varDatabases(), d_toPropagate(satContext), d_proofs(satContext, false), @@ -456,7 +456,8 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_av2nodeMap(av2nodeMap), d_congruenceManager(cm), d_satContext(satContext), - d_satAllocationLevel(d_satContext->getLevel()) + d_satAllocationLevel(d_satContext->getLevel()), + d_raiseConflict(raiseConflict) { d_selfExplainingProof = d_proofs.size(); d_proofs.push_back(NullConstraint); @@ -1153,6 +1154,20 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector& lemmas) } } +void ConstraintDatabase::raiseUnateConflict(Constraint ant, Constraint cons){ + Assert(ant->hasProof()); + Constraint negCons = cons->getNegation(); + Assert(negCons->hasProof()); + + Debug("arith::unate::conf") << ant << "implies " << cons << endl; + Debug("arith::unate::conf") << negCons << " is true." << endl; + + + Node conf = ConstraintValue::explainConflict(ant, negCons); + Debug("arith::unate::conf") << conf << std::endl; + d_raiseConflict(conf); +} + void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl; Assert(curr != prev); @@ -1186,17 +1201,25 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ Constraint lb = vc.getLowerBound(); - if(!lb->isTrue()){ + if(lb->negationHasProof()){ + raiseUnateConflict(curr, lb); + return; + }else if(!lb->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl; + lb->impliedBy(curr); } } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); } } @@ -1229,7 +1252,10 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ Constraint ub = vc.getUpperBound(); - if(!ub->isTrue()){ + if(ub->negationHasProof()){ + raiseUnateConflict(curr, ub); + return; + }else if(!ub->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl; ub->impliedBy(curr); @@ -1237,9 +1263,13 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; ++d_statistics.d_unatePropagateImplications; + dis->impliedBy(curr); } } @@ -1279,7 +1309,10 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ Constraint lb = vc.getLowerBound(); - if(!lb->isTrue()){ + if(lb->negationHasProof()){ + raiseUnateConflict(curr, lb); + return; + }else if(!lb->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl; lb->impliedBy(curr); @@ -1287,9 +1320,13 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); } } @@ -1307,15 +1344,22 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ Constraint ub = vc.getUpperBound(); - if(!ub->isTrue()){ + if(ub->negationHasProof()){ + raiseUnateConflict(curr, ub); + return; + }else if(!ub->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl; + ub->impliedBy(curr); } } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl; dis->impliedBy(curr); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 5b49dd54d..dcc3bf8bb 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -762,6 +762,8 @@ private: const context::Context * const d_satContext; const int d_satAllocationLevel; + NodeCallBack& d_raiseConflict; + friend class ConstraintValue; public: @@ -769,12 +771,13 @@ public: ConstraintDatabase( context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - ArithCongruenceManager& dm); + ArithCongruenceManager& dm, + NodeCallBack& conflictCallBack); ~ConstraintDatabase(); + /** Adds a literal to the database. */ Constraint addLiteral(TNode lit); - //Constraint addAtom(TNode atom); /** * If hasLiteral() is true, returns the constraint. @@ -852,6 +855,8 @@ public: void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB); private: + void raiseUnateConflict(Constraint ant, Constraint cons); + class Statistics { public: IntStat d_unatePropagateCalls; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index be24e43ba..faf0e3563 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -61,6 +61,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), d_diseqQueue(c, false), + d_currentPropagationList(), + d_learnedBounds(c), d_partialModel(c), d_tableau(), d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack), @@ -71,10 +73,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_conflicts(c), - d_conflictCallBack(d_conflicts), - d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap), - d_simplex(d_linEq, d_conflictCallBack), - d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager), + d_raiseConflict(d_conflicts), + d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict), + d_simplex(d_linEq, d_raiseConflict), + d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict), d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() @@ -181,7 +183,7 @@ void TheoryArith::zeroDifferenceDetected(ArithVar x){ } /* procedure AssertLower( x_i >= c_i ) */ -Node TheoryArith::AssertLower(Constraint constraint){ +bool TheoryArith::AssertLower(Constraint constraint){ Assert(constraint != NullConstraint); Assert(constraint->isLowerBound()); @@ -194,7 +196,7 @@ Node TheoryArith::AssertLower(Constraint constraint){ //TODO Relax to less than? if(d_partialModel.lessThanLowerBound(x_i, c_i)){ - return Node::null(); + return false; //sat } int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i); @@ -203,7 +205,8 @@ Node TheoryArith::AssertLower(Constraint constraint){ Node conflict = ConstraintValue::explainConflict(ubc, constraint); Debug("arith") << "AssertLower conflict " << conflict << endl; ++(d_statistics.d_statAssertLowerConflicts); - return conflict; + d_raiseConflict(conflict); + return true; }else if(cmpToUB == 0){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); @@ -229,10 +232,33 @@ Node TheoryArith::AssertLower(Constraint constraint){ ++(d_statistics.d_statDisequalityConflicts); Debug("eq") << " assert lower conflict " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; }else if(!eq->isTrue()){ Debug("eq") << "lb == ub, propagate eq" << eq << endl; eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i)); + // do not need to add to d_learnedBounds + } + } + }else{ + Assert(cmpToUB < 0); + const ValueCollection& vc = constraint->getValueCollection(); + if(vc.hasDisequality() && vc.hasUpperBound()){ + const Constraint diseq = vc.getDisequality(); + if(diseq->isTrue()){ + const Constraint ub = vc.getUpperBound(); + if(ub->hasProof()){ + Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint); + Debug("eq") << " assert upper conflict " << conflict << endl; + d_raiseConflict(conflict); + return true; + }else if(!ub->negationHasProof()){ + Constraint negUb = ub->getNegation(); + negUb->impliedBy(constraint, diseq); + //if(!negUb->canBePropagated()){ + d_learnedBounds.push_back(negUb); + //}//otherwise let this be propagated/asserted later + } } } } @@ -263,11 +289,11 @@ Node TheoryArith::AssertLower(Constraint constraint){ if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - return Node::null(); + return false; //sat } /* procedure AssertUpper( x_i <= c_i) */ -Node TheoryArith::AssertUpper(Constraint constraint){ +bool TheoryArith::AssertUpper(Constraint constraint){ ArithVar x_i = constraint->getVariable(); const DeltaRational& c_i = constraint->getValue(); @@ -283,7 +309,7 @@ Node TheoryArith::AssertUpper(Constraint constraint){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i - return Node::null(); //sat + return false; //sat } // cmpToLb = \lowerbound(x_i).cmp(c_i) @@ -293,7 +319,8 @@ Node TheoryArith::AssertUpper(Constraint constraint){ Node conflict = ConstraintValue::explainConflict(lbc, constraint); Debug("arith") << "AssertUpper conflict " << conflict << endl; ++(d_statistics.d_statAssertUpperConflicts); - return conflict; + d_raiseConflict(conflict); + return true; }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); @@ -315,13 +342,34 @@ Node TheoryArith::AssertUpper(Constraint constraint){ if(diseq->isTrue()){ Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint); Debug("eq") << " assert upper conflict " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; }else if(!eq->isTrue()){ Debug("eq") << "lb == ub, propagate eq" << eq << endl; eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i)); + //do not bother to add to d_learnedBounds + } + } + }else if(cmpToLB > 0){ + const ValueCollection& vc = constraint->getValueCollection(); + if(vc.hasDisequality() && vc.hasLowerBound()){ + const Constraint diseq = vc.getDisequality(); + if(diseq->isTrue()){ + const Constraint lb = vc.getLowerBound(); + if(lb->hasProof()){ + Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint); + Debug("eq") << " assert upper conflict " << conflict << endl; + d_raiseConflict(conflict); + return true; + }else if(!lb->negationHasProof()){ + Constraint negLb = lb->getNegation(); + negLb->impliedBy(constraint, diseq); + //if(!negLb->canBePropagated()){ + d_learnedBounds.push_back(negLb); + //}//otherwise let this be propagated/asserted later + } } } - } d_currentPropagationList.push_back(constraint); @@ -351,12 +399,12 @@ Node TheoryArith::AssertUpper(Constraint constraint){ if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - return Node::null(); + return false; //sat } /* procedure AssertEquality( x_i == c_i ) */ -Node TheoryArith::AssertEquality(Constraint constraint){ +bool TheoryArith::AssertEquality(Constraint constraint){ AssertArgument(constraint != NullConstraint, "AssertUpper() called on a NullConstraint."); @@ -374,21 +422,23 @@ Node TheoryArith::AssertEquality(Constraint constraint){ // u_i <= c_i <= l_i // This can happen if both c_i <= x_i and x_i <= c_i are in the system. if(cmpToUB >= 0 && cmpToLB <= 0){ - return Node::null(); //sat + return false; //sat } if(cmpToUB > 0){ Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i); Node conflict = ConstraintValue::explainConflict(ubc, constraint); Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; } if(cmpToLB < 0){ Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i); Node conflict = ConstraintValue::explainConflict(lbc, constraint); Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; } Assert(cmpToUB <= 0); @@ -431,12 +481,12 @@ Node TheoryArith::AssertEquality(Constraint constraint){ }else{ d_simplex.updateBasic(x_i); } - return Node::null(); + return false; } /* procedure AssertDisequality( x_i != c_i ) */ -Node TheoryArith::AssertDisequality(Constraint constraint){ +bool TheoryArith::AssertDisequality(Constraint constraint){ AssertArgument(constraint != NullConstraint, "AssertUpper() called on a NullConstraint."); @@ -457,7 +507,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ if(constraint->isSplit()){ Debug("eq") << "skipping already split " << constraint << endl; - return Node::null(); + return false; } const ValueCollection& vc = constraint->getValueCollection(); @@ -468,18 +518,25 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ //in conflict Debug("eq") << "explaining" << endl; ++(d_statistics.d_statDisequalityConflicts); - return ConstraintValue::explainConflict(constraint, lb, ub); + Node conflict = ConstraintValue::explainConflict(constraint, lb, ub); + d_raiseConflict(conflict); + return true; + }else if(lb->isTrue()){ Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl; const Constraint negUb = ub->getNegation(); if(!negUb->isTrue()){ negUb->impliedBy(constraint, lb); + d_learnedBounds.push_back(negUb); } }else if(ub->isTrue()){ Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl; const Constraint negLb = lb->getNegation(); if(!negLb->isTrue()){ negLb->impliedBy(constraint, ub); + //if(!negLb->canBePropagated()){ + d_learnedBounds.push_back(negLb); + //} } } } @@ -488,7 +545,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ if(c_i == d_partialModel.getAssignment(x_i)){ Debug("eq") << "lemma now! " << constraint << endl; d_out->lemma(constraint->split()); - return Node::null(); + return false; }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ Debug("eq") << "can drop as less than lb" << constraint << endl; }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){ @@ -497,7 +554,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ Debug("eq") << "push back" << constraint << endl; d_diseqQueue.push(constraint); } - return Node::null(); + return false; } @@ -1006,23 +1063,48 @@ Node TheoryArith::callDioSolver(){ return d_diosolver.processEquationsForConflict(); } -Node TheoryArith::assertionCases(TNode assertion){ - Constraint constraint = d_constraintDatabase.lookup(assertion); +Constraint TheoryArith::constraintFromFactQueue(){ + Assert(!done()); + TNode assertion = get(); Kind simpleKind = Comparison::comparisonKind(assertion); - Assert(simpleKind != UNDEFINED_KIND); - Assert(constraint != NullConstraint || - simpleKind == EQUAL || - simpleKind == DISTINCT ); - if(simpleKind == EQUAL || simpleKind == DISTINCT){ + Constraint constraint = d_constraintDatabase.lookup(assertion); + if(constraint == NullConstraint){ + Assert(simpleKind == EQUAL || simpleKind == DISTINCT ); + bool isDistinct = simpleKind == DISTINCT; Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; - - if(!isSetup(eq)){ - //The previous code was equivalent to: - setupAtom(eq); - constraint = d_constraintDatabase.lookup(assertion); + Assert(!isSetup(eq)); + Node reEq = Rewriter::rewrite(eq); + if(reEq.getKind() == CONST_BOOLEAN){ + if(reEq.getConst() != isDistinct){ + Assert((reEq.getConst() && isDistinct) || + (!reEq.getConst() && !isDistinct)); + d_raiseConflict(assertion); + } + return NullConstraint; } - } + Assert(reEq.getKind() != CONST_BOOLEAN); + if(!isSetup(reEq)){ + setupAtom(reEq); + } + Node reAssertion = isDistinct ? reEq.notNode() : reEq; + constraint = d_constraintDatabase.lookup(reAssertion); + } + + // Kind simpleKind = Comparison::comparisonKind(assertion); + // Assert(simpleKind != UNDEFINED_KIND); + // Assert(constraint != NullConstraint || + // simpleKind == EQUAL || + // simpleKind == DISTINCT ); + // if(simpleKind == EQUAL || simpleKind == DISTINCT){ + // Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; + + // if(!isSetup(eq)){ + // //The previous code was equivalent to: + // setupAtom(eq); + // constraint = d_constraintDatabase.lookup(assertion); + // } + // } Assert(constraint != NullConstraint); if(constraint->negationHasProof()){ @@ -1031,8 +1113,6 @@ Node TheoryArith::assertionCases(TNode assertion){ if(Debug.isOn("whytheoryenginewhy")){ debugPrintFacts(); } -// Warning() << "arith: Theory engine is sending me both a literal and its negation?" -// << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl; } Debug("arith::eq") << constraint << endl; Debug("arith::eq") << negation << endl; @@ -1042,94 +1122,202 @@ Node TheoryArith::assertionCases(TNode assertion){ negation->explainForConflict(nb); Node conflict = nb; Debug("arith::eq") << "conflict" << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return NullConstraint; } Assert(!constraint->negationHasProof()); if(constraint->assertedToTheTheory()){ //Do nothing - return Node::null(); - } - Assert(!constraint->assertedToTheTheory()); - constraint->setAssertedToTheTheory(); - - ArithVar x_i = constraint->getVariable(); - //DeltaRational c_i = determineRightConstant(assertion, simpleKind); - - //Assert(constraint->getVariable() == determineLeftVariable(assertion, simpleKind)); - //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind)); - Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion); - - Debug("arith::assertions") << "arith assertion @" << getSatContext()->getLevel() - <<"(" << assertion - << " \\-> " - //<< determineLeftVariable(assertion, simpleKind) - <<" "<< simpleKind <<" " - //<< determineRightConstant(assertion, simpleKind) - << ")" << std::endl; - + return NullConstraint; + }else{ + Debug("arith::constraint") << "arith constraint " << constraint << std::endl; + constraint->setAssertedToTheTheory(); - Debug("arith::constraint") << "arith constraint " << constraint << std::endl; + if(!constraint->hasProof()){ + Debug("arith::constraint") << "marking as constraint as self explaining " << endl; + constraint->selfExplaining(); + }else{ + Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl; + } - if(!constraint->hasProof()){ - Debug("arith::constraint") << "marking as constraint as self explaining " << endl; - constraint->selfExplaining(); - }else{ - Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl; + return constraint; } +} + +bool TheoryArith::assertionCases(Constraint constraint){ + Assert(constraint->hasProof()); + Assert(!constraint->negationHasProof()); - Assert(!isInteger(x_i) || - simpleKind == EQUAL || - simpleKind == DISTINCT || - simpleKind == GEQ || - simpleKind == LT); + ArithVar x_i = constraint->getVariable(); switch(constraint->getType()){ case UpperBound: - if(simpleKind == LT && isInteger(x_i)){ + if(isInteger(x_i) && constraint->isStrictUpperBound()){ Constraint floorConstraint = constraint->getFloor(); if(!floorConstraint->isTrue()){ if(floorConstraint->negationHasProof()){ - return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation()); + Node conf = ConstraintValue::explainConflict(constraint, floorConstraint->getNegation()); + d_raiseConflict(conf); + return true; }else{ floorConstraint->impliedBy(constraint); + // Do not need to add to d_learnedBounds } } - //c_i = DeltaRational(c_i.floor()); - //return AssertUpper(x_i, c_i, assertion, floorConstraint); return AssertUpper(floorConstraint); }else{ return AssertUpper(constraint); } - //return AssertUpper(x_i, c_i, assertion, constraint); case LowerBound: - if(simpleKind == LT && isInteger(x_i)){ + if(isInteger(x_i) && constraint->isStrictLowerBound()){ Constraint ceilingConstraint = constraint->getCeiling(); if(!ceilingConstraint->isTrue()){ if(ceilingConstraint->negationHasProof()){ - - return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation()); + Node conf = ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation()); + d_raiseConflict(conf); + return true; } ceilingConstraint->impliedBy(constraint); + // Do not need to add to learnedBounds } - //c_i = DeltaRational(c_i.ceiling()); - //return AssertLower(x_i, c_i, assertion, ceilingConstraint); return AssertLower(ceilingConstraint); }else{ return AssertLower(constraint); } - //return AssertLower(x_i, c_i, assertion, constraint); case Equality: return AssertEquality(constraint); - //return AssertEquality(x_i, c_i, assertion, constraint); case Disequality: return AssertDisequality(constraint); - //return AssertDisequality(x_i, c_i, assertion, constraint); default: Unreachable(); - return Node::null(); + return false; } } +// Node TheoryArith::assertionCases(TNode assertion){ +// Constraint constraint = d_constraintDatabase.lookup(assertion); + +// Kind simpleKind = Comparison::comparisonKind(assertion); +// Assert(simpleKind != UNDEFINED_KIND); +// Assert(constraint != NullConstraint || +// simpleKind == EQUAL || +// simpleKind == DISTINCT ); +// if(simpleKind == EQUAL || simpleKind == DISTINCT){ +// Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; + +// if(!isSetup(eq)){ +// //The previous code was equivalent to: +// setupAtom(eq); +// constraint = d_constraintDatabase.lookup(assertion); +// } +// } +// Assert(constraint != NullConstraint); + +// if(constraint->negationHasProof()){ +// Constraint negation = constraint->getNegation(); +// if(negation->isSelfExplaining()){ +// if(Debug.isOn("whytheoryenginewhy")){ +// debugPrintFacts(); +// } +// // Warning() << "arith: Theory engine is sending me both a literal and its negation?" +// // << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl; +// } +// Debug("arith::eq") << constraint << endl; +// Debug("arith::eq") << negation << endl; + +// NodeBuilder<> nb(kind::AND); +// nb << assertion; +// negation->explainForConflict(nb); +// Node conflict = nb; +// Debug("arith::eq") << "conflict" << conflict << endl; +// return conflict; +// } +// Assert(!constraint->negationHasProof()); + +// if(constraint->assertedToTheTheory()){ +// //Do nothing +// return Node::null(); +// } +// Assert(!constraint->assertedToTheTheory()); +// constraint->setAssertedToTheTheory(); + +// ArithVar x_i = constraint->getVariable(); +// //DeltaRational c_i = determineRightConstant(assertion, simpleKind); + +// //Assert(constraint->getVariable() == determineLeftVariable(assertion, simpleKind)); +// //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind)); +// Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion); + +// Debug("arith::assertions") << "arith assertion @" << getSatContext()->getLevel() +// <<"(" << assertion +// << " \\-> " +// //<< determineLeftVariable(assertion, simpleKind) +// <<" "<< simpleKind <<" " +// //<< determineRightConstant(assertion, simpleKind) +// << ")" << std::endl; + + +// Debug("arith::constraint") << "arith constraint " << constraint << std::endl; + +// if(!constraint->hasProof()){ +// Debug("arith::constraint") << "marking as constraint as self explaining " << endl; +// constraint->selfExplaining(); +// }else{ +// Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl; +// } + +// Assert(!isInteger(x_i) || +// simpleKind == EQUAL || +// simpleKind == DISTINCT || +// simpleKind == GEQ || +// simpleKind == LT); + +// switch(constraint->getType()){ +// case UpperBound: +// if(simpleKind == LT && isInteger(x_i)){ +// Constraint floorConstraint = constraint->getFloor(); +// if(!floorConstraint->isTrue()){ +// if(floorConstraint->negationHasProof()){ +// return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation()); +// }else{ +// floorConstraint->impliedBy(constraint); +// } +// } +// //c_i = DeltaRational(c_i.floor()); +// //return AssertUpper(x_i, c_i, assertion, floorConstraint); +// return AssertUpper(floorConstraint); +// }else{ +// return AssertUpper(constraint); +// } +// //return AssertUpper(x_i, c_i, assertion, constraint); +// case LowerBound: +// if(simpleKind == LT && isInteger(x_i)){ +// Constraint ceilingConstraint = constraint->getCeiling(); +// if(!ceilingConstraint->isTrue()){ +// if(ceilingConstraint->negationHasProof()){ + +// return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation()); +// } +// ceilingConstraint->impliedBy(constraint); +// } +// //c_i = DeltaRational(c_i.ceiling()); +// //return AssertLower(x_i, c_i, assertion, ceilingConstraint); +// return AssertLower(ceilingConstraint); +// }else{ +// return AssertLower(constraint); +// } +// //return AssertLower(x_i, c_i, assertion, constraint); +// case Equality: +// return AssertEquality(constraint); +// //return AssertEquality(x_i, c_i, assertion, constraint); +// case Disequality: +// return AssertDisequality(constraint); +// //return AssertDisequality(x_i, c_i, assertion, constraint); +// default: +// Unreachable(); +// return Node::null(); +// } +// } /** * Looks for the next integer variable without an integer assignment in a round robin fashion. @@ -1154,6 +1342,15 @@ bool TheoryArith::hasIntegerModel(){ return true; } +/** Outputs conflicts to the output channel. */ +void TheoryArith::outputConflicts(){ + Assert(!d_conflicts.empty()); + for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ + Node conflict = d_conflicts[i]; + Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl; + d_out->conflict(conflict); + } +} void TheoryArith::check(Effort effortLevel){ Assert(d_currentPropagationList.empty()); @@ -1161,22 +1358,29 @@ void TheoryArith::check(Effort effortLevel){ d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done(); while(!done()){ - - Node assertion = get(); - Node possibleConflict = assertionCases(assertion); - - if(!possibleConflict.isNull()){ + Constraint curr = constraintFromFactQueue(); + if(curr != NullConstraint){ + bool res = assertionCases(curr); + Assert(!res || inConflict()); + } + if(inConflict()){ revertOutOfConflict(); - - Debug("arith::conflict") << "conflict " << possibleConflict << endl; - d_out->conflict(possibleConflict); + outputConflicts(); return; } - if(d_congruenceManager.inConflict()){ - Node c = d_congruenceManager.conflict(); + } + while(!d_learnedBounds.empty()){ + // we may attempt some constraints twice. this is okay! + Constraint curr = d_learnedBounds.front(); + d_learnedBounds.pop(); + Debug("arith::learned") << curr << endl; + + bool res = assertionCases(curr); + Assert(!res || inConflict()); + + if(inConflict()){ revertOutOfConflict(); - Debug("arith::conflict") << "difference manager conflict " << c << endl; - d_out->conflict(c); + outputConflicts(); return; } } @@ -1191,13 +1395,7 @@ void TheoryArith::check(Effort effortLevel){ bool foundConflict = d_simplex.findModel(); if(foundConflict){ revertOutOfConflict(); - - Assert(!d_conflicts.empty()); - for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ - Node conflict = d_conflicts[i]; - Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl; - d_out->conflict(conflict); - } + outputConflicts(); emmittedConflictOrSplit = true; }else{ d_partialModel.commitAssignmentChanges(); @@ -1208,7 +1406,7 @@ void TheoryArith::check(Effort effortLevel){ Options::current()->arithPropagationMode == Options::BOTH_PROP)){ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); - while(!d_currentPropagationList.empty()){ + while(!d_currentPropagationList.empty() && !inConflict()){ Constraint curr = d_currentPropagationList.front(); d_currentPropagationList.pop_front(); @@ -1244,6 +1442,13 @@ void TheoryArith::check(Effort effortLevel){ Unhandled(curr->getType()); } } + + if(inConflict()){ + Debug("arith::unate") << "unate conflict" << endl; + revertOutOfConflict(); + outputConflicts(); + return; + } }else{ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); d_currentPropagationList.clear(); @@ -1800,25 +2005,10 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic)); d_linEq.propagateNonbasicsLowerBound(basic, bestImplied); } + // I think this can be skipped if canBePropagated is true + //d_learnedBounds.push(bestImplied); return true; } - - // bool asserted = valuationIsAsserted(bestImplied); - // bool propagated = d_theRealPropManager.isPropagated(bestImplied); - // if( !asserted && !propagated){ - - // NodeBuilder<> nb(kind::AND); - // if(upperBound){ - // d_linEq.explainNonbasicsUpperBound(basic, nb); - // }else{ - // d_linEq.explainNonbasicsLowerBound(basic, nb); - // } - // Node explanation = nb; - // d_theRealPropManager.propagate(bestImplied, explanation, false); - // return true; - // }else{ - // Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; - // } } } return false; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1f0120387..e23a9a943 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -184,6 +184,8 @@ private: */ std::deque d_currentPropagationList; + context::CDQueue d_learnedBounds; + /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -245,8 +247,17 @@ private: void operator()(Node n){ d_list.push_back(n); } - }; - PushCallBack d_conflictCallBack; + } d_raiseConflict; + + /** Returns true iff a conflict has been raised. */ + inline bool inConflict() const { + return !d_conflicts.empty(); + } + /** + * Outputs the contents of d_conflicts onto d_out. + * Must be inConflict(). + */ + void outputConflicts(); /** @@ -386,10 +397,10 @@ private: * a node describing this conflict is returned. * If this new bound is not in conflict, Node::null() is returned. */ - Node AssertLower(Constraint constraint); - Node AssertUpper(Constraint constraint); - Node AssertEquality(Constraint constraint); - Node AssertDisequality(Constraint constraint); + bool AssertLower(Constraint constraint); + bool AssertUpper(Constraint constraint); + bool AssertEquality(Constraint constraint); + bool AssertDisequality(Constraint constraint); /** Tracks the bounds that were updated in the current round. */ DenseSet d_updatedBounds; @@ -423,7 +434,8 @@ private: * Returns a conflict if one was found. * Returns Node::null if no conflict was found. */ - Node assertionCases(TNode assertion); + Constraint constraintFromFactQueue(); + bool assertionCases(Constraint c); /** * Returns the basic variable with the shorted row containg a non-basic variable. diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index bfc13ae16..21479bac5 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -19,6 +19,7 @@ SMT_TESTS = \ xs-09-16-3-4-1-5.delta03.smt \ xs-09-16-3-4-1-5.delta04.smt \ error0.smt2 \ + error1.smt \ error0.delta01.smt \ simple_cyclic2.smt2 \ error30.smt diff --git a/test/regress/regress0/uflia/error1.smt b/test/regress/regress0/uflia/error1.smt new file mode 100644 index 000000000..7afffaa88 --- /dev/null +++ b/test/regress/regress0/uflia/error1.smt @@ -0,0 +1,701 @@ +(benchmark fuzzsmt +:logic QF_UFLIA +:status sat +:extrafuns ((f0 Int Int Int Int)) +:extrafuns ((f1 Int Int)) +:extrapreds ((p0 Int Int)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Int)) +:formula +(let (?e3 1) +(let (?e4 2) +(let (?e5 (f1 v1)) +(let (?e6 (+ v2 v2)) +(let (?e7 (ite (p0 ?e6 v1) 1 0)) +(let (?e8 (ite (p0 ?e5 v1) 1 0)) +(let (?e9 (+ ?e6 ?e8)) +(let (?e10 (ite (p0 v1 ?e6) 1 0)) +(let (?e11 (ite (p0 v2 ?e8) 1 0)) +(let (?e12 (* (~ ?e4) ?e6)) +(let (?e13 (+ v1 ?e5)) +(let (?e14 (* ?e4 ?e12)) +(let (?e15 (f0 v2 ?e5 v0)) +(let (?e16 (ite (p0 ?e5 ?e6) 1 0)) +(let (?e17 (+ ?e7 ?e16)) +(let (?e18 (+ ?e10 ?e12)) +(let (?e19 (- ?e13 ?e12)) +(let (?e20 (* ?e19 (~ ?e4))) +(let (?e21 (+ ?e13 ?e18)) +(let (?e22 (f0 ?e5 ?e17 ?e5)) +(let (?e23 (* ?e17 ?e4)) +(let (?e24 (ite (p0 ?e9 ?e19) 1 0)) +(let (?e25 (~ ?e6)) +(let (?e26 (f1 ?e6)) +(let (?e27 (* ?e25 (~ ?e3))) +(flet ($e28 (< ?e7 ?e6)) +(flet ($e29 (> ?e12 ?e10)) +(flet ($e30 (distinct ?e7 ?e9)) +(flet ($e31 (<= v2 v2)) +(flet ($e32 (>= ?e6 ?e27)) +(flet ($e33 (distinct ?e11 ?e20)) +(flet ($e34 (> ?e25 ?e23)) +(flet ($e35 (< ?e7 ?e22)) +(flet ($e36 (>= ?e24 ?e10)) +(flet ($e37 (>= ?e24 ?e23)) +(flet ($e38 (distinct ?e5 ?e25)) +(flet ($e39 (= ?e16 ?e27)) +(flet ($e40 (> ?e21 ?e16)) +(flet ($e41 (> ?e7 ?e12)) +(flet ($e42 (distinct ?e22 ?e22)) +(flet ($e43 (= v2 ?e16)) +(flet ($e44 (>= ?e23 ?e7)) +(flet ($e45 (= ?e12 ?e8)) +(flet ($e46 (<= ?e13 ?e12)) +(flet ($e47 (< ?e12 ?e24)) +(flet ($e48 (< ?e13 ?e6)) +(flet ($e49 (> ?e15 ?e19)) +(flet ($e50 (> ?e25 ?e18)) +(flet ($e51 (>= ?e15 ?e7)) +(flet ($e52 (distinct ?e8 ?e20)) +(flet ($e53 (= ?e18 ?e5)) +(flet ($e54 (> ?e13 ?e15)) +(flet ($e55 (= ?e14 ?e16)) +(flet ($e56 (>= v0 ?e21)) +(flet ($e57 (= v1 ?e10)) +(flet ($e58 (distinct ?e26 ?e22)) +(flet ($e59 (> ?e18 ?e5)) +(flet ($e60 (< ?e11 ?e10)) +(flet ($e61 (>= ?e8 ?e11)) +(flet ($e62 (distinct ?e23 ?e21)) +(flet ($e63 (p0 v1 ?e20)) +(flet ($e64 (< ?e8 ?e11)) +(flet ($e65 (<= ?e26 ?e12)) +(flet ($e66 (= ?e21 ?e6)) +(flet ($e67 (distinct ?e21 ?e21)) +(flet ($e68 (>= v1 ?e17)) +(let (?e69 (ite $e59 ?e16 ?e12)) +(let (?e70 (ite $e47 ?e9 ?e19)) +(let (?e71 (ite $e64 ?e9 ?e25)) +(let (?e72 (ite $e63 v2 ?e25)) +(let (?e73 (ite $e31 ?e22 ?e15)) +(let (?e74 (ite $e66 ?e23 ?e20)) +(let (?e75 (ite $e57 ?e15 ?e9)) +(let (?e76 (ite $e39 ?e21 ?e75)) +(let (?e77 (ite $e62 v0 ?e11)) +(let (?e78 (ite $e50 ?e17 ?e71)) +(let (?e79 (ite $e38 ?e6 v0)) +(let (?e80 (ite $e62 ?e18 v0)) +(let (?e81 (ite $e29 ?e70 ?e13)) +(let (?e82 (ite $e54 ?e19 ?e20)) +(let (?e83 (ite $e57 ?e19 ?e77)) +(let (?e84 (ite $e41 ?e79 v2)) +(let (?e85 (ite $e56 ?e84 v2)) +(let (?e86 (ite $e47 ?e7 ?e15)) +(let (?e87 (ite $e49 ?e27 ?e27)) +(let (?e88 (ite $e45 ?e14 ?e16)) +(let (?e89 (ite $e42 ?e26 ?e5)) +(let (?e90 (ite $e51 ?e10 ?e12)) +(let (?e91 (ite $e46 ?e26 ?e16)) +(let (?e92 (ite $e35 ?e24 v1)) +(let (?e93 (ite $e32 ?e8 ?e91)) +(let (?e94 (ite $e30 ?e80 ?e15)) +(let (?e95 (ite $e56 ?e75 ?e27)) +(let (?e96 (ite $e64 ?e79 ?e19)) +(let (?e97 (ite $e44 ?e77 ?e84)) +(let (?e98 (ite $e62 ?e25 ?e71)) +(let (?e99 (ite $e65 ?e91 ?e21)) +(let (?e100 (ite $e33 ?e97 ?e14)) +(let (?e101 (ite $e45 ?e90 ?e7)) +(let (?e102 (ite $e41 ?e78 ?e89)) +(let (?e103 (ite $e36 ?e7 ?e81)) +(let (?e104 (ite $e48 ?e74 ?e16)) +(let (?e105 (ite $e31 ?e24 ?e81)) +(let (?e106 (ite $e40 ?e83 ?e71)) +(let (?e107 (ite $e67 ?e11 ?e10)) +(let (?e108 (ite $e52 ?e104 ?e76)) +(let (?e109 (ite $e55 ?e14 ?e14)) +(let (?e110 (ite $e61 ?e102 ?e80)) +(let (?e111 (ite $e34 ?e74 v2)) +(let (?e112 (ite $e54 ?e21 ?e106)) +(let (?e113 (ite $e28 ?e93 ?e20)) +(let (?e114 (ite $e37 ?e8 ?e83)) +(let (?e115 (ite $e55 ?e113 ?e89)) +(let (?e116 (ite $e58 ?e7 ?e25)) +(let (?e117 (ite $e60 ?e7 ?e75)) +(let (?e118 (ite $e43 ?e75 ?e16)) +(let (?e119 (ite $e53 ?e74 ?e26)) +(let (?e120 (ite $e68 ?e76 ?e25)) +(flet ($e121 (< ?e90 ?e9)) +(flet ($e122 (distinct ?e99 v0)) +(flet ($e123 (= ?e116 ?e23)) +(flet ($e124 (= ?e86 ?e99)) +(flet ($e125 (>= ?e78 ?e18)) +(flet ($e126 (> ?e99 ?e75)) +(flet ($e127 (<= ?e84 ?e107)) +(flet ($e128 (>= ?e9 ?e69)) +(flet ($e129 (= ?e95 ?e79)) +(flet ($e130 (p0 ?e103 ?e16)) +(flet ($e131 (<= ?e83 ?e104)) +(flet ($e132 (p0 ?e119 ?e97)) +(flet ($e133 (p0 ?e96 ?e89)) +(flet ($e134 (<= ?e100 ?e21)) +(flet ($e135 (= ?e102 ?e18)) +(flet ($e136 (<= ?e81 ?e16)) +(flet ($e137 (distinct ?e70 ?e94)) +(flet ($e138 (= ?e114 ?e112)) +(flet ($e139 (= ?e107 ?e89)) +(flet ($e140 (p0 ?e110 v2)) +(flet ($e141 (< ?e21 ?e114)) +(flet ($e142 (p0 ?e20 v2)) +(flet ($e143 (< ?e100 ?e94)) +(flet ($e144 (distinct ?e94 ?e26)) +(flet ($e145 (= ?e109 ?e88)) +(flet ($e146 (= ?e16 ?e100)) +(flet ($e147 (= ?e99 ?e87)) +(flet ($e148 (<= ?e87 ?e86)) +(flet ($e149 (p0 ?e73 ?e96)) +(flet ($e150 (> ?e12 ?e94)) +(flet ($e151 (distinct ?e95 ?e71)) +(flet ($e152 (distinct ?e19 ?e101)) +(flet ($e153 (p0 ?e84 ?e96)) +(flet ($e154 (= ?e99 ?e111)) +(flet ($e155 (p0 ?e14 ?e118)) +(flet ($e156 (<= ?e70 ?e25)) +(flet ($e157 (= ?e19 ?e98)) +(flet ($e158 (< ?e99 ?e90)) +(flet ($e159 (>= ?e14 ?e15)) +(flet ($e160 (<= v2 ?e120)) +(flet ($e161 (<= ?e21 ?e75)) +(flet ($e162 (< ?e114 ?e6)) +(flet ($e163 (> ?e99 ?e116)) +(flet ($e164 (<= ?e89 ?e11)) +(flet ($e165 (distinct ?e9 ?e10)) +(flet ($e166 (> ?e27 ?e97)) +(flet ($e167 (< ?e119 ?e10)) +(flet ($e168 (< ?e69 ?e79)) +(flet ($e169 (<= ?e22 ?e7)) +(flet ($e170 (= ?e117 ?e17)) +(flet ($e171 (>= ?e72 ?e16)) +(flet ($e172 (>= ?e12 ?e114)) +(flet ($e173 (distinct ?e119 ?e27)) +(flet ($e174 (<= ?e72 ?e119)) +(flet ($e175 (= ?e119 ?e118)) +(flet ($e176 (distinct ?e80 ?e73)) +(flet ($e177 (> ?e10 ?e18)) +(flet ($e178 (> ?e115 ?e15)) +(flet ($e179 (= ?e13 ?e72)) +(flet ($e180 (>= ?e110 ?e111)) +(flet ($e181 (< v0 ?e87)) +(flet ($e182 (< ?e72 ?e70)) +(flet ($e183 (<= ?e13 ?e9)) +(flet ($e184 (>= ?e7 ?e20)) +(flet ($e185 (<= ?e77 ?e23)) +(flet ($e186 (< ?e105 ?e102)) +(flet ($e187 (<= ?e78 ?e109)) +(flet ($e188 (distinct ?e89 ?e97)) +(flet ($e189 (p0 ?e118 ?e97)) +(flet ($e190 (> ?e81 ?e111)) +(flet ($e191 (> ?e14 ?e78)) +(flet ($e192 (< ?e101 ?e97)) +(flet ($e193 (distinct ?e12 ?e16)) +(flet ($e194 (< ?e113 ?e92)) +(flet ($e195 (>= ?e100 ?e87)) +(flet ($e196 (>= ?e103 ?e12)) +(flet ($e197 (p0 ?e116 ?e13)) +(flet ($e198 (>= ?e85 ?e13)) +(flet ($e199 (p0 ?e107 ?e120)) +(flet ($e200 (> ?e96 ?e74)) +(flet ($e201 (<= ?e113 ?e113)) +(flet ($e202 (>= ?e16 ?e103)) +(flet ($e203 (>= ?e72 ?e11)) +(flet ($e204 (> ?e27 ?e25)) +(flet ($e205 (distinct ?e25 ?e15)) +(flet ($e206 (distinct v1 ?e85)) +(flet ($e207 (p0 ?e95 ?e75)) +(flet ($e208 (< ?e92 ?e84)) +(flet ($e209 (< ?e91 ?e115)) +(flet ($e210 (distinct ?e13 ?e75)) +(flet ($e211 (= ?e91 ?e69)) +(flet ($e212 (p0 ?e13 ?e23)) +(flet ($e213 (>= ?e96 ?e100)) +(flet ($e214 (>= ?e72 ?e111)) +(flet ($e215 (p0 ?e97 ?e112)) +(flet ($e216 (>= ?e78 ?e98)) +(flet ($e217 (= ?e120 ?e101)) +(flet ($e218 (<= ?e72 ?e71)) +(flet ($e219 (p0 ?e90 ?e103)) +(flet ($e220 (< ?e117 ?e113)) +(flet ($e221 (>= ?e118 ?e84)) +(flet ($e222 (> ?e11 ?e104)) +(flet ($e223 (< ?e77 ?e111)) +(flet ($e224 (<= ?e21 ?e7)) +(flet ($e225 (>= ?e16 ?e74)) +(flet ($e226 (<= ?e91 ?e74)) +(flet ($e227 (p0 v2 ?e70)) +(flet ($e228 (p0 ?e101 ?e83)) +(flet ($e229 (>= ?e10 ?e8)) +(flet ($e230 (> ?e110 ?e72)) +(flet ($e231 (< ?e84 ?e20)) +(flet ($e232 (p0 ?e79 ?e26)) +(flet ($e233 (= ?e113 ?e81)) +(flet ($e234 (p0 ?e14 ?e90)) +(flet ($e235 (distinct ?e96 ?e15)) +(flet ($e236 (distinct ?e96 ?e7)) +(flet ($e237 (p0 ?e87 ?e104)) +(flet ($e238 (= ?e110 ?e71)) +(flet ($e239 (< ?e70 ?e7)) +(flet ($e240 (>= ?e13 ?e112)) +(flet ($e241 (p0 ?e24 ?e93)) +(flet ($e242 (<= ?e102 ?e87)) +(flet ($e243 (p0 ?e73 ?e25)) +(flet ($e244 (distinct ?e24 ?e116)) +(flet ($e245 (< ?e84 ?e78)) +(flet ($e246 (<= ?e104 ?e100)) +(flet ($e247 (= ?e18 ?e74)) +(flet ($e248 (< ?e16 ?e8)) +(flet ($e249 (< ?e93 ?e25)) +(flet ($e250 (>= ?e88 ?e81)) +(flet ($e251 (>= ?e98 ?e109)) +(flet ($e252 (>= ?e21 ?e13)) +(flet ($e253 (p0 v2 ?e74)) +(flet ($e254 (distinct ?e24 ?e27)) +(flet ($e255 (>= ?e120 ?e111)) +(flet ($e256 (>= ?e81 ?e14)) +(flet ($e257 (<= ?e87 ?e21)) +(flet ($e258 (p0 ?e74 ?e12)) +(flet ($e259 (distinct ?e5 ?e9)) +(flet ($e260 (>= ?e105 ?e79)) +(flet ($e261 (<= v2 ?e108)) +(flet ($e262 (= ?e96 ?e6)) +(flet ($e263 (= ?e5 ?e77)) +(flet ($e264 (>= v0 ?e23)) +(flet ($e265 (= ?e107 ?e72)) +(flet ($e266 (= ?e110 ?e95)) +(flet ($e267 (< ?e90 ?e117)) +(flet ($e268 (= v2 ?e23)) +(flet ($e269 (<= ?e77 ?e12)) +(flet ($e270 (<= ?e104 ?e111)) +(flet ($e271 (= ?e93 ?e14)) +(flet ($e272 (p0 ?e72 ?e79)) +(flet ($e273 (distinct ?e8 ?e20)) +(flet ($e274 (p0 ?e96 ?e112)) +(flet ($e275 (= ?e92 ?e24)) +(flet ($e276 (>= ?e16 ?e22)) +(flet ($e277 (= ?e19 ?e10)) +(flet ($e278 (<= ?e20 ?e86)) +(flet ($e279 (< ?e116 ?e118)) +(flet ($e280 (>= ?e74 ?e5)) +(flet ($e281 (<= ?e79 ?e105)) +(flet ($e282 (< ?e115 ?e70)) +(flet ($e283 (<= ?e13 ?e103)) +(flet ($e284 (p0 ?e27 ?e87)) +(flet ($e285 (p0 v0 ?e88)) +(flet ($e286 (<= ?e81 ?e104)) +(flet ($e287 (= ?e6 ?e99)) +(flet ($e288 (= ?e114 ?e87)) +(flet ($e289 (distinct ?e77 ?e71)) +(flet ($e290 (distinct ?e15 ?e15)) +(flet ($e291 (< ?e79 ?e72)) +(flet ($e292 (< ?e19 ?e8)) +(flet ($e293 (p0 ?e109 ?e5)) +(flet ($e294 (p0 v1 ?e19)) +(flet ($e295 (p0 ?e75 ?e104)) +(flet ($e296 (>= ?e100 ?e110)) +(flet ($e297 (>= ?e101 ?e23)) +(flet ($e298 (distinct ?e21 ?e107)) +(flet ($e299 (= ?e27 ?e101)) +(flet ($e300 (distinct ?e116 v1)) +(flet ($e301 (> ?e22 ?e5)) +(flet ($e302 (distinct ?e102 ?e80)) +(flet ($e303 (p0 ?e112 ?e84)) +(flet ($e304 (<= ?e111 ?e78)) +(flet ($e305 (= ?e75 ?e9)) +(flet ($e306 (= ?e80 ?e20)) +(flet ($e307 (< ?e80 ?e80)) +(flet ($e308 (distinct ?e13 ?e9)) +(flet ($e309 (p0 ?e6 ?e14)) +(flet ($e310 (> ?e70 ?e91)) +(flet ($e311 (> ?e16 ?e8)) +(flet ($e312 (<= ?e13 ?e95)) +(flet ($e313 (> ?e92 ?e95)) +(flet ($e314 (< ?e96 ?e87)) +(flet ($e315 (= ?e91 ?e92)) +(flet ($e316 (>= ?e120 ?e117)) +(flet ($e317 (p0 ?e13 ?e93)) +(flet ($e318 (distinct ?e120 ?e24)) +(flet ($e319 (>= ?e15 ?e86)) +(flet ($e320 (> ?e94 ?e84)) +(flet ($e321 (> ?e20 ?e99)) +(flet ($e322 (< ?e23 ?e71)) +(flet ($e323 (= ?e119 ?e73)) +(flet ($e324 (<= ?e82 ?e94)) +(flet ($e325 (<= ?e108 ?e107)) +(flet ($e326 (p0 ?e13 ?e80)) +(flet ($e327 (<= ?e87 ?e102)) +(flet ($e328 (<= ?e74 ?e89)) +(flet ($e329 (= ?e73 ?e11)) +(flet ($e330 (distinct ?e15 ?e106)) +(flet ($e331 (<= ?e115 ?e110)) +(flet ($e332 (p0 v0 ?e69)) +(flet ($e333 (>= v1 ?e9)) +(flet ($e334 (> v1 v2)) +(flet ($e335 (< ?e80 ?e95)) +(flet ($e336 (>= ?e114 ?e69)) +(flet ($e337 (distinct ?e80 ?e118)) +(flet ($e338 (p0 ?e16 ?e91)) +(flet ($e339 (p0 ?e100 ?e85)) +(flet ($e340 (= ?e13 ?e73)) +(flet ($e341 (= ?e92 ?e12)) +(flet ($e342 (p0 ?e100 ?e72)) +(flet ($e343 (= ?e26 ?e119)) +(flet ($e344 (< ?e20 ?e20)) +(flet ($e345 (<= ?e100 ?e94)) +(flet ($e346 (> ?e114 ?e116)) +(flet ($e347 (p0 ?e102 ?e19)) +(flet ($e348 (= ?e113 ?e13)) +(flet ($e349 (distinct ?e108 ?e5)) +(flet ($e350 (< ?e14 ?e118)) +(flet ($e351 (< ?e72 ?e110)) +(flet ($e352 (> ?e83 ?e114)) +(flet ($e353 (distinct ?e106 ?e24)) +(flet ($e354 (<= ?e24 ?e83)) +(flet ($e355 (p0 ?e116 ?e101)) +(flet ($e356 (< ?e110 ?e96)) +(flet ($e357 (= ?e12 v0)) +(flet ($e358 (p0 ?e108 ?e113)) +(flet ($e359 (>= ?e27 ?e81)) +(flet ($e360 (<= ?e109 ?e75)) +(flet ($e361 (= ?e102 ?e26)) +(flet ($e362 (distinct ?e108 ?e104)) +(flet ($e363 (<= ?e108 ?e26)) +(flet ($e364 (<= ?e114 ?e69)) +(flet ($e365 (>= ?e113 ?e82)) +(flet ($e366 (= ?e115 v1)) +(flet ($e367 (= ?e25 ?e27)) +(flet ($e368 (p0 ?e27 ?e91)) +(flet ($e369 (<= ?e13 ?e116)) +(flet ($e370 (<= ?e87 ?e114)) +(flet ($e371 (< ?e25 ?e108)) +(flet ($e372 (= ?e108 ?e9)) +(flet ($e373 (p0 ?e89 ?e117)) +(flet ($e374 (<= ?e13 ?e19)) +(flet ($e375 (p0 ?e12 ?e26)) +(flet ($e376 (< ?e20 ?e91)) +(flet ($e377 (distinct ?e107 ?e76)) +(flet ($e378 (if_then_else $e180 $e123 $e342)) +(flet ($e379 (if_then_else $e151 $e330 $e232)) +(flet ($e380 (if_then_else $e136 $e175 $e130)) +(flet ($e381 (if_then_else $e362 $e250 $e56)) +(flet ($e382 (not $e337)) +(flet ($e383 (xor $e194 $e150)) +(flet ($e384 (iff $e44 $e65)) +(flet ($e385 (xor $e300 $e160)) +(flet ($e386 (xor $e158 $e241)) +(flet ($e387 (not $e286)) +(flet ($e388 (and $e168 $e55)) +(flet ($e389 (or $e143 $e153)) +(flet ($e390 (not $e289)) +(flet ($e391 (or $e191 $e235)) +(flet ($e392 (and $e42 $e184)) +(flet ($e393 (not $e170)) +(flet ($e394 (iff $e35 $e356)) +(flet ($e395 (xor $e128 $e207)) +(flet ($e396 (implies $e394 $e208)) +(flet ($e397 (not $e354)) +(flet ($e398 (not $e201)) +(flet ($e399 (if_then_else $e176 $e169 $e331)) +(flet ($e400 (and $e217 $e172)) +(flet ($e401 (and $e324 $e178)) +(flet ($e402 (iff $e387 $e279)) +(flet ($e403 (or $e204 $e374)) +(flet ($e404 (iff $e323 $e334)) +(flet ($e405 (xor $e302 $e247)) +(flet ($e406 (iff $e288 $e125)) +(flet ($e407 (or $e375 $e227)) +(flet ($e408 (and $e127 $e378)) +(flet ($e409 (iff $e58 $e284)) +(flet ($e410 (implies $e181 $e52)) +(flet ($e411 (implies $e166 $e385)) +(flet ($e412 (and $e41 $e306)) +(flet ($e413 (xor $e268 $e361)) +(flet ($e414 (and $e47 $e32)) +(flet ($e415 (iff $e228 $e339)) +(flet ($e416 (implies $e292 $e199)) +(flet ($e417 (implies $e252 $e39)) +(flet ($e418 (or $e37 $e351)) +(flet ($e419 (and $e209 $e49)) +(flet ($e420 (implies $e263 $e197)) +(flet ($e421 (if_then_else $e349 $e312 $e287)) +(flet ($e422 (implies $e353 $e249)) +(flet ($e423 (not $e388)) +(flet ($e424 (and $e296 $e310)) +(flet ($e425 (xor $e309 $e59)) +(flet ($e426 (and $e240 $e242)) +(flet ($e427 (if_then_else $e45 $e163 $e411)) +(flet ($e428 (not $e364)) +(flet ($e429 (if_then_else $e144 $e267 $e293)) +(flet ($e430 (if_then_else $e173 $e238 $e126)) +(flet ($e431 (implies $e338 $e48)) +(flet ($e432 (iff $e156 $e383)) +(flet ($e433 (or $e68 $e391)) +(flet ($e434 (xor $e262 $e304)) +(flet ($e435 (not $e318)) +(flet ($e436 (iff $e29 $e155)) +(flet ($e437 (not $e121)) +(flet ($e438 (implies $e389 $e36)) +(flet ($e439 (iff $e234 $e174)) +(flet ($e440 (iff $e253 $e314)) +(flet ($e441 (if_then_else $e137 $e278 $e355)) +(flet ($e442 (xor $e131 $e64)) +(flet ($e443 (or $e377 $e124)) +(flet ($e444 (implies $e346 $e122)) +(flet ($e445 (iff $e212 $e372)) +(flet ($e446 (implies $e195 $e277)) +(flet ($e447 (not $e430)) +(flet ($e448 (not $e192)) +(flet ($e449 (implies $e196 $e177)) +(flet ($e450 (or $e190 $e257)) +(flet ($e451 (iff $e215 $e412)) +(flet ($e452 (implies $e274 $e418)) +(flet ($e453 (if_then_else $e336 $e322 $e149)) +(flet ($e454 (if_then_else $e447 $e189 $e269)) +(flet ($e455 (not $e218)) +(flet ($e456 (xor $e152 $e224)) +(flet ($e457 (not $e358)) +(flet ($e458 (not $e60)) +(flet ($e459 (not $e424)) +(flet ($e460 (not $e398)) +(flet ($e461 (if_then_else $e380 $e291 $e453)) +(flet ($e462 (iff $e305 $e271)) +(flet ($e463 (if_then_else $e408 $e417 $e148)) +(flet ($e464 (not $e270)) +(flet ($e465 (and $e261 $e51)) +(flet ($e466 (or $e450 $e299)) +(flet ($e467 (iff $e301 $e154)) +(flet ($e468 (iff $e200 $e460)) +(flet ($e469 (and $e343 $e129)) +(flet ($e470 (iff $e313 $e400)) +(flet ($e471 (or $e433 $e347)) +(flet ($e472 (not $e451)) +(flet ($e473 (iff $e266 $e317)) +(flet ($e474 (and $e273 $e390)) +(flet ($e475 (and $e406 $e440)) +(flet ($e476 (implies $e223 $e233)) +(flet ($e477 (if_then_else $e298 $e185 $e344)) +(flet ($e478 (xor $e462 $e426)) +(flet ($e479 (and $e368 $e28)) +(flet ($e480 (implies $e319 $e466)) +(flet ($e481 (not $e348)) +(flet ($e482 (not $e134)) +(flet ($e483 (xor $e145 $e471)) +(flet ($e484 (xor $e439 $e171)) +(flet ($e485 (if_then_else $e369 $e198 $e295)) +(flet ($e486 (xor $e329 $e405)) +(flet ($e487 (iff $e290 $e221)) +(flet ($e488 (if_then_else $e373 $e415 $e219)) +(flet ($e489 (iff $e50 $e244)) +(flet ($e490 (and $e363 $e403)) +(flet ($e491 (or $e402 $e431)) +(flet ($e492 (not $e229)) +(flet ($e493 (implies $e470 $e280)) +(flet ($e494 (or $e489 $e220)) +(flet ($e495 (and $e188 $e67)) +(flet ($e496 (or $e53 $e165)) +(flet ($e497 (and $e427 $e206)) +(flet ($e498 (iff $e307 $e333)) +(flet ($e499 (if_then_else $e186 $e487 $e281)) +(flet ($e500 (iff $e360 $e442)) +(flet ($e501 (iff $e490 $e357)) +(flet ($e502 (iff $e392 $e211)) +(flet ($e503 (xor $e210 $e410)) +(flet ($e504 (iff $e239 $e486)) +(flet ($e505 (implies $e248 $e54)) +(flet ($e506 (implies $e465 $e492)) +(flet ($e507 (and $e494 $e255)) +(flet ($e508 (or $e285 $e352)) +(flet ($e509 (if_then_else $e264 $e399 $e316)) +(flet ($e510 (if_then_else $e34 $e508 $e448)) +(flet ($e511 (not $e203)) +(flet ($e512 (not $e246)) +(flet ($e513 (and $e366 $e371)) +(flet ($e514 (xor $e367 $e311)) +(flet ($e515 (iff $e141 $e226)) +(flet ($e516 (iff $e455 $e484)) +(flet ($e517 (iff $e164 $e62)) +(flet ($e518 (iff $e140 $e294)) +(flet ($e519 (and $e345 $e222)) +(flet ($e520 (xor $e135 $e519)) +(flet ($e521 (implies $e216 $e315)) +(flet ($e522 (or $e260 $e446)) +(flet ($e523 (xor $e520 $e522)) +(flet ($e524 (iff $e407 $e46)) +(flet ($e525 (xor $e275 $e256)) +(flet ($e526 (and $e420 $e423)) +(flet ($e527 (not $e61)) +(flet ($e528 (implies $e297 $e488)) +(flet ($e529 (or $e231 $e332)) +(flet ($e530 (and $e482 $e66)) +(flet ($e531 (and $e518 $e245)) +(flet ($e532 (not $e183)) +(flet ($e533 (and $e382 $e236)) +(flet ($e534 (iff $e456 $e422)) +(flet ($e535 (if_then_else $e413 $e524 $e379)) +(flet ($e536 (and $e436 $e401)) +(flet ($e537 (xor $e475 $e475)) +(flet ($e538 (implies $e437 $e498)) +(flet ($e539 (implies $e485 $e477)) +(flet ($e540 (implies $e504 $e474)) +(flet ($e541 (xor $e272 $e445)) +(flet ($e542 (implies $e393 $e438)) +(flet ($e543 (xor $e139 $e205)) +(flet ($e544 (implies $e414 $e386)) +(flet ($e545 (if_then_else $e214 $e321 $e544)) +(flet ($e546 (xor $e449 $e265)) +(flet ($e547 (and $e533 $e187)) +(flet ($e548 (xor $e530 $e506)) +(flet ($e549 (or $e258 $e283)) +(flet ($e550 (iff $e326 $e500)) +(flet ($e551 (if_then_else $e535 $e359 $e537)) +(flet ($e552 (iff $e479 $e469)) +(flet ($e553 (xor $e531 $e521)) +(flet ($e554 (xor $e435 $e43)) +(flet ($e555 (not $e162)) +(flet ($e556 (and $e525 $e454)) +(flet ($e557 (xor $e501 $e514)) +(flet ($e558 (implies $e179 $e138)) +(flet ($e559 (xor $e404 $e365)) +(flet ($e560 (not $e540)) +(flet ($e561 (xor $e513 $e546)) +(flet ($e562 (implies $e503 $e308)) +(flet ($e563 (if_then_else $e541 $e561 $e434)) +(flet ($e564 (not $e335)) +(flet ($e565 (not $e341)) +(flet ($e566 (if_then_else $e564 $e551 $e511)) +(flet ($e567 (or $e523 $e496)) +(flet ($e568 (and $e534 $e159)) +(flet ($e569 (if_then_else $e555 $e562 $e497)) +(flet ($e570 (xor $e457 $e225)) +(flet ($e571 (or $e161 $e251)) +(flet ($e572 (implies $e556 $e559)) +(flet ($e573 (iff $e483 $e370)) +(flet ($e574 (if_then_else $e237 $e432 $e213)) +(flet ($e575 (and $e147 $e528)) +(flet ($e576 (xor $e376 $e552)) +(flet ($e577 (and $e463 $e542)) +(flet ($e578 (not $e548)) +(flet ($e579 (implies $e468 $e560)) +(flet ($e580 (or $e557 $e495)) +(flet ($e581 (if_then_else $e327 $e478 $e472)) +(flet ($e582 (implies $e254 $e572)) +(flet ($e583 (and $e491 $e543)) +(flet ($e584 (implies $e527 $e243)) +(flet ($e585 (if_then_else $e428 $e142 $e566)) +(flet ($e586 (xor $e429 $e133)) +(flet ($e587 (not $e202)) +(flet ($e588 (iff $e481 $e550)) +(flet ($e589 (iff $e33 $e441)) +(flet ($e590 (or $e547 $e532)) +(flet ($e591 (and $e538 $e57)) +(flet ($e592 (not $e230)) +(flet ($e593 (or $e576 $e592)) +(flet ($e594 (iff $e505 $e578)) +(flet ($e595 (and $e350 $e580)) +(flet ($e596 (or $e443 $e574)) +(flet ($e597 (or $e579 $e575)) +(flet ($e598 (or $e132 $e38)) +(flet ($e599 (implies $e303 $e146)) +(flet ($e600 (if_then_else $e598 $e499 $e419)) +(flet ($e601 (and $e558 $e473)) +(flet ($e602 (or $e590 $e529)) +(flet ($e603 (if_then_else $e591 $e182 $e40)) +(flet ($e604 (iff $e596 $e571)) +(flet ($e605 (iff $e328 $e588)) +(flet ($e606 (and $e397 $e594)) +(flet ($e607 (or $e593 $e502)) +(flet ($e608 (or $e516 $e539)) +(flet ($e609 (iff $e573 $e193)) +(flet ($e610 (not $e549)) +(flet ($e611 (not $e563)) +(flet ($e612 (xor $e30 $e606)) +(flet ($e613 (if_then_else $e467 $e609 $e581)) +(flet ($e614 (not $e526)) +(flet ($e615 (if_then_else $e517 $e602 $e610)) +(flet ($e616 (implies $e464 $e396)) +(flet ($e617 (not $e425)) +(flet ($e618 (or $e452 $e611)) +(flet ($e619 (xor $e416 $e63)) +(flet ($e620 (iff $e545 $e565)) +(flet ($e621 (xor $e603 $e458)) +(flet ($e622 (if_then_else $e536 $e476 $e567)) +(flet ($e623 (or $e515 $e157)) +(flet ($e624 (iff $e510 $e493)) +(flet ($e625 (or $e600 $e599)) +(flet ($e626 (iff $e553 $e619)) +(flet ($e627 (or $e586 $e625)) +(flet ($e628 (not $e621)) +(flet ($e629 (not $e509)) +(flet ($e630 (xor $e617 $e582)) +(flet ($e631 (implies $e480 $e630)) +(flet ($e632 (implies $e421 $e340)) +(flet ($e633 (iff $e577 $e612)) +(flet ($e634 (iff $e512 $e627)) +(flet ($e635 (if_then_else $e632 $e444 $e583)) +(flet ($e636 (not $e569)) +(flet ($e637 (implies $e629 $e276)) +(flet ($e638 (and $e633 $e620)) +(flet ($e639 (and $e461 $e381)) +(flet ($e640 (iff $e597 $e395)) +(flet ($e641 (implies $e637 $e639)) +(flet ($e642 (and $e640 $e320)) +(flet ($e643 (or $e607 $e259)) +(flet ($e644 (if_then_else $e384 $e584 $e325)) +(flet ($e645 (implies $e626 $e608)) +(flet ($e646 (xor $e585 $e631)) +(flet ($e647 (or $e616 $e167)) +(flet ($e648 (or $e568 $e644)) +(flet ($e649 (or $e589 $e614)) +(flet ($e650 (and $e641 $e642)) +(flet ($e651 (xor $e554 $e650)) +(flet ($e652 (implies $e635 $e595)) +(flet ($e653 (or $e618 $e636)) +(flet ($e654 (and $e645 $e282)) +(flet ($e655 (not $e648)) +(flet ($e656 (or $e649 $e652)) +(flet ($e657 (iff $e31 $e409)) +(flet ($e658 (iff $e634 $e651)) +(flet ($e659 (xor $e601 $e605)) +(flet ($e660 (not $e628)) +(flet ($e661 (xor $e587 $e622)) +(flet ($e662 (not $e459)) +(flet ($e663 (or $e656 $e638)) +(flet ($e664 (not $e646)) +(flet ($e665 (or $e623 $e653)) +(flet ($e666 (implies $e663 $e663)) +(flet ($e667 (implies $e570 $e507)) +(flet ($e668 (xor $e647 $e658)) +(flet ($e669 (not $e661)) +(flet ($e670 (iff $e660 $e657)) +(flet ($e671 (not $e655)) +(flet ($e672 (if_then_else $e615 $e615 $e624)) +(flet ($e673 (iff $e665 $e643)) +(flet ($e674 (xor $e662 $e669)) +(flet ($e675 (not $e671)) +(flet ($e676 (and $e674 $e675)) +(flet ($e677 (implies $e670 $e676)) +(flet ($e678 (iff $e668 $e604)) +(flet ($e679 (not $e659)) +(flet ($e680 (or $e672 $e666)) +(flet ($e681 (xor $e679 $e678)) +(flet ($e682 (not $e667)) +(flet ($e683 (and $e677 $e681)) +(flet ($e684 (xor $e680 $e680)) +(flet ($e685 (not $e683)) +(flet ($e686 (if_then_else $e664 $e684 $e685)) +(flet ($e687 (iff $e654 $e686)) +(flet ($e688 (if_then_else $e687 $e613 $e613)) +(flet ($e689 (and $e682 $e688)) +(flet ($e690 (implies $e673 $e689)) +$e690 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index ea707e549..189c96618 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -28,7 +28,8 @@ SMT_TESTS = \ pb_real_10_0200_10_26.smt \ pb_real_10_0200_10_29.smt \ incorrect2.smt \ - incorrect1.smt + incorrect1.smt \ + error1.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/uflra/error1.smt b/test/regress/regress0/uflra/error1.smt new file mode 100644 index 000000000..9b2cabedf --- /dev/null +++ b/test/regress/regress0/uflra/error1.smt @@ -0,0 +1,867 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:status sat +:extrafuns ((f0 Real Real Real)) +:extrafuns ((f1 Real Real)) +:extrapreds ((p0 Real Real)) +:extrafuns ((v0 Real)) +:extrafuns ((v1 Real)) +:extrafuns ((v2 Real)) +:formula +(let (?e3 5) +(let (?e4 15) +(let (?e5 3) +(let (?e6 (+ v1 v1)) +(let (?e7 (~ v1)) +(let (?e8 (/ ?e3 ?e5)) +(let (?e9 (~ ?e7)) +(let (?e10 (* ?e4 ?e8)) +(let (?e11 (~ v1)) +(let (?e12 (- v0 ?e7)) +(let (?e13 (/ ?e4 ?e4)) +(let (?e14 (+ ?e9 v2)) +(let (?e15 (/ ?e4 ?e4)) +(let (?e16 (f0 ?e12 ?e11)) +(let (?e17 (- ?e6 ?e14)) +(let (?e18 (f0 ?e10 ?e13)) +(let (?e19 (+ v1 ?e15)) +(let (?e20 (/ ?e4 ?e5)) +(let (?e21 (f1 ?e19)) +(let (?e22 (~ ?e9)) +(let (?e23 (ite (p0 ?e7 ?e19) 1 0)) +(flet ($e24 (> ?e7 v1)) +(flet ($e25 (>= ?e16 ?e9)) +(flet ($e26 (>= ?e9 ?e9)) +(flet ($e27 (>= ?e14 ?e19)) +(flet ($e28 (<= v2 ?e15)) +(flet ($e29 (< ?e23 ?e11)) +(flet ($e30 (distinct ?e15 ?e6)) +(flet ($e31 (= ?e8 ?e16)) +(flet ($e32 (>= ?e17 ?e8)) +(flet ($e33 (< ?e14 ?e7)) +(flet ($e34 (> ?e18 ?e11)) +(flet ($e35 (>= v2 ?e20)) +(flet ($e36 (= ?e11 ?e8)) +(flet ($e37 (= v2 ?e9)) +(flet ($e38 (>= ?e22 v0)) +(flet ($e39 (= ?e16 ?e15)) +(flet ($e40 (= ?e9 ?e20)) +(flet ($e41 (<= ?e8 ?e14)) +(flet ($e42 (<= ?e9 ?e8)) +(flet ($e43 (>= ?e23 ?e19)) +(flet ($e44 (> ?e22 v0)) +(flet ($e45 (>= ?e14 ?e23)) +(flet ($e46 (> v2 ?e9)) +(flet ($e47 (distinct ?e18 ?e15)) +(flet ($e48 (distinct ?e15 ?e22)) +(flet ($e49 (distinct ?e12 ?e15)) +(flet ($e50 (<= ?e16 v2)) +(flet ($e51 (> v0 ?e17)) +(flet ($e52 (<= ?e14 ?e14)) +(flet ($e53 (< ?e13 ?e17)) +(flet ($e54 (p0 ?e21 ?e17)) +(flet ($e55 (p0 ?e17 ?e14)) +(flet ($e56 (> ?e20 ?e8)) +(flet ($e57 (p0 ?e17 ?e8)) +(flet ($e58 (distinct ?e15 ?e15)) +(flet ($e59 (> ?e8 ?e9)) +(flet ($e60 (<= ?e23 ?e21)) +(flet ($e61 (p0 ?e20 ?e22)) +(flet ($e62 (p0 ?e9 ?e19)) +(flet ($e63 (distinct ?e11 ?e18)) +(flet ($e64 (= ?e9 v2)) +(flet ($e65 (<= ?e7 ?e14)) +(flet ($e66 (< ?e8 v1)) +(flet ($e67 (distinct ?e18 ?e17)) +(flet ($e68 (>= v0 v1)) +(flet ($e69 (= ?e13 ?e9)) +(flet ($e70 (>= ?e23 ?e16)) +(flet ($e71 (p0 ?e20 ?e8)) +(flet ($e72 (> ?e18 ?e23)) +(flet ($e73 (>= ?e14 ?e6)) +(flet ($e74 (>= ?e8 ?e18)) +(flet ($e75 (= ?e19 v0)) +(flet ($e76 (= ?e9 ?e14)) +(flet ($e77 (> ?e9 ?e21)) +(flet ($e78 (distinct ?e14 ?e21)) +(flet ($e79 (distinct ?e15 ?e17)) +(flet ($e80 (p0 ?e12 v2)) +(flet ($e81 (> ?e11 ?e18)) +(flet ($e82 (= ?e9 ?e7)) +(flet ($e83 (>= ?e6 ?e11)) +(flet ($e84 (< ?e22 ?e7)) +(flet ($e85 (> ?e13 ?e9)) +(flet ($e86 (< v2 ?e21)) +(flet ($e87 (< ?e23 ?e9)) +(flet ($e88 (= ?e11 ?e13)) +(flet ($e89 (p0 ?e23 ?e13)) +(flet ($e90 (< ?e12 ?e19)) +(flet ($e91 (= ?e14 ?e19)) +(flet ($e92 (distinct ?e21 ?e8)) +(flet ($e93 (< ?e14 ?e19)) +(flet ($e94 (p0 ?e12 ?e8)) +(flet ($e95 (<= ?e22 ?e18)) +(flet ($e96 (p0 ?e13 v1)) +(flet ($e97 (p0 v1 v1)) +(flet ($e98 (> ?e17 v1)) +(flet ($e99 (<= v2 ?e9)) +(flet ($e100 (<= ?e21 v0)) +(flet ($e101 (distinct ?e7 ?e9)) +(flet ($e102 (p0 ?e19 ?e6)) +(flet ($e103 (<= ?e12 ?e23)) +(flet ($e104 (= ?e14 ?e9)) +(flet ($e105 (>= ?e10 ?e15)) +(let (?e106 (ite $e31 ?e7 ?e11)) +(let (?e107 (ite $e51 ?e12 ?e9)) +(let (?e108 (ite $e72 ?e8 ?e106)) +(let (?e109 (ite $e77 ?e19 ?e10)) +(let (?e110 (ite $e46 ?e21 ?e10)) +(let (?e111 (ite $e25 ?e14 ?e110)) +(let (?e112 (ite $e87 ?e17 ?e107)) +(let (?e113 (ite $e85 ?e23 ?e108)) +(let (?e114 (ite $e66 v0 ?e109)) +(let (?e115 (ite $e78 ?e108 ?e110)) +(let (?e116 (ite $e27 ?e13 ?e21)) +(let (?e117 (ite $e57 ?e18 v2)) +(let (?e118 (ite $e52 ?e20 ?e18)) +(let (?e119 (ite $e102 ?e12 ?e13)) +(let (?e120 (ite $e42 ?e22 ?e119)) +(let (?e121 (ite $e92 v1 ?e11)) +(let (?e122 (ite $e59 ?e16 ?e22)) +(let (?e123 (ite $e30 v1 ?e117)) +(let (?e124 (ite $e55 ?e13 ?e108)) +(let (?e125 (ite $e86 ?e15 ?e21)) +(let (?e126 (ite $e69 ?e6 ?e123)) +(let (?e127 (ite $e63 ?e121 ?e11)) +(let (?e128 (ite $e31 v0 ?e16)) +(let (?e129 (ite $e70 ?e6 ?e23)) +(let (?e130 (ite $e74 ?e17 ?e127)) +(let (?e131 (ite $e95 ?e106 ?e117)) +(let (?e132 (ite $e28 v1 ?e126)) +(let (?e133 (ite $e34 ?e127 ?e22)) +(let (?e134 (ite $e81 ?e133 ?e16)) +(let (?e135 (ite $e97 ?e14 ?e130)) +(let (?e136 (ite $e31 ?e113 ?e9)) +(let (?e137 (ite $e49 v1 ?e135)) +(let (?e138 (ite $e104 ?e18 ?e110)) +(let (?e139 (ite $e49 ?e9 ?e135)) +(let (?e140 (ite $e33 ?e133 ?e117)) +(let (?e141 (ite $e71 ?e124 ?e20)) +(let (?e142 (ite $e40 ?e111 ?e110)) +(let (?e143 (ite $e37 ?e15 ?e11)) +(let (?e144 (ite $e64 ?e127 ?e134)) +(let (?e145 (ite $e39 ?e115 ?e17)) +(let (?e146 (ite $e33 ?e119 ?e134)) +(let (?e147 (ite $e41 ?e20 ?e107)) +(let (?e148 (ite $e60 ?e138 ?e140)) +(let (?e149 (ite $e88 ?e128 ?e20)) +(let (?e150 (ite $e53 ?e136 ?e132)) +(let (?e151 (ite $e60 ?e19 ?e126)) +(let (?e152 (ite $e42 ?e113 ?e145)) +(let (?e153 (ite $e93 ?e150 ?e147)) +(let (?e154 (ite $e60 ?e19 ?e144)) +(let (?e155 (ite $e35 ?e149 v0)) +(let (?e156 (ite $e30 ?e113 ?e113)) +(let (?e157 (ite $e80 ?e11 ?e17)) +(let (?e158 (ite $e47 ?e114 ?e12)) +(let (?e159 (ite $e62 ?e19 ?e123)) +(let (?e160 (ite $e40 ?e151 ?e17)) +(let (?e161 (ite $e105 ?e19 ?e133)) +(let (?e162 (ite $e45 ?e22 ?e142)) +(let (?e163 (ite $e91 ?e112 ?e8)) +(let (?e164 (ite $e26 ?e160 ?e126)) +(let (?e165 (ite $e56 ?e140 ?e126)) +(let (?e166 (ite $e93 ?e9 ?e18)) +(let (?e167 (ite $e76 ?e158 ?e166)) +(let (?e168 (ite $e80 ?e17 ?e146)) +(let (?e169 (ite $e51 ?e132 ?e117)) +(let (?e170 (ite $e89 ?e21 ?e118)) +(let (?e171 (ite $e64 ?e19 ?e120)) +(let (?e172 (ite $e91 ?e142 ?e118)) +(let (?e173 (ite $e90 ?e16 ?e168)) +(let (?e174 (ite $e66 ?e136 ?e157)) +(let (?e175 (ite $e54 ?e143 ?e165)) +(let (?e176 (ite $e74 ?e12 ?e166)) +(let (?e177 (ite $e51 ?e120 ?e8)) +(let (?e178 (ite $e82 ?e7 ?e125)) +(let (?e179 (ite $e58 ?e143 ?e130)) +(let (?e180 (ite $e43 ?e23 v1)) +(let (?e181 (ite $e101 ?e166 ?e173)) +(let (?e182 (ite $e84 ?e135 ?e157)) +(let (?e183 (ite $e89 ?e172 ?e21)) +(let (?e184 (ite $e75 ?e125 ?e19)) +(let (?e185 (ite $e47 ?e165 ?e155)) +(let (?e186 (ite $e100 ?e21 ?e146)) +(let (?e187 (ite $e27 ?e157 ?e185)) +(let (?e188 (ite $e45 ?e130 ?e110)) +(let (?e189 (ite $e96 ?e6 ?e121)) +(let (?e190 (ite $e67 ?e120 ?e133)) +(let (?e191 (ite $e65 ?e18 ?e130)) +(let (?e192 (ite $e29 ?e112 ?e127)) +(let (?e193 (ite $e49 ?e152 ?e179)) +(let (?e194 (ite $e54 ?e121 v1)) +(let (?e195 (ite $e45 ?e137 ?e19)) +(let (?e196 (ite $e79 ?e125 ?e158)) +(let (?e197 (ite $e50 ?e16 ?e124)) +(let (?e198 (ite $e83 ?e168 ?e134)) +(let (?e199 (ite $e84 ?e121 ?e157)) +(let (?e200 (ite $e94 ?e173 ?e149)) +(let (?e201 (ite $e50 ?e132 ?e186)) +(let (?e202 (ite $e96 ?e115 ?e135)) +(let (?e203 (ite $e99 ?e110 ?e182)) +(let (?e204 (ite $e73 ?e185 ?e198)) +(let (?e205 (ite $e36 ?e131 v2)) +(let (?e206 (ite $e39 ?e6 ?e204)) +(let (?e207 (ite $e34 ?e156 ?e7)) +(let (?e208 (ite $e103 ?e124 ?e173)) +(let (?e209 (ite $e63 ?e149 ?e143)) +(let (?e210 (ite $e70 ?e20 ?e130)) +(let (?e211 (ite $e44 ?e112 ?e176)) +(let (?e212 (ite $e62 v2 ?e118)) +(let (?e213 (ite $e33 ?e150 ?e179)) +(let (?e214 (ite $e87 ?e152 ?e175)) +(let (?e215 (ite $e85 ?e196 ?e198)) +(let (?e216 (ite $e61 ?e143 ?e149)) +(let (?e217 (ite $e48 ?e108 ?e166)) +(let (?e218 (ite $e24 ?e18 ?e204)) +(let (?e219 (ite $e38 ?e179 ?e154)) +(let (?e220 (ite $e84 ?e107 ?e189)) +(let (?e221 (ite $e83 ?e119 ?e158)) +(let (?e222 (ite $e98 ?e23 ?e188)) +(let (?e223 (ite $e92 ?e147 ?e112)) +(let (?e224 (ite $e32 ?e215 ?e16)) +(let (?e225 (ite $e68 ?e128 ?e158)) +(flet ($e226 (>= ?e157 ?e198)) +(flet ($e227 (> ?e182 ?e184)) +(flet ($e228 (< ?e139 ?e225)) +(flet ($e229 (> ?e175 ?e211)) +(flet ($e230 (> ?e212 ?e117)) +(flet ($e231 (> ?e173 ?e196)) +(flet ($e232 (p0 ?e116 v2)) +(flet ($e233 (< ?e173 ?e220)) +(flet ($e234 (< ?e129 ?e127)) +(flet ($e235 (distinct ?e175 ?e135)) +(flet ($e236 (<= ?e177 ?e211)) +(flet ($e237 (>= ?e129 ?e154)) +(flet ($e238 (<= ?e133 ?e174)) +(flet ($e239 (<= ?e9 ?e168)) +(flet ($e240 (>= ?e225 ?e11)) +(flet ($e241 (< ?e131 ?e185)) +(flet ($e242 (<= ?e153 ?e107)) +(flet ($e243 (<= ?e197 ?e143)) +(flet ($e244 (<= ?e198 ?e186)) +(flet ($e245 (>= ?e194 ?e129)) +(flet ($e246 (< ?e13 ?e195)) +(flet ($e247 (distinct ?e8 ?e134)) +(flet ($e248 (>= ?e164 ?e118)) +(flet ($e249 (>= ?e208 ?e170)) +(flet ($e250 (= ?e157 ?e19)) +(flet ($e251 (< ?e160 ?e161)) +(flet ($e252 (<= ?e148 ?e15)) +(flet ($e253 (p0 ?e174 ?e167)) +(flet ($e254 (<= ?e167 ?e121)) +(flet ($e255 (< ?e146 ?e174)) +(flet ($e256 (= ?e166 ?e119)) +(flet ($e257 (>= ?e121 ?e129)) +(flet ($e258 (distinct ?e148 ?e190)) +(flet ($e259 (>= ?e8 ?e209)) +(flet ($e260 (= ?e113 ?e218)) +(flet ($e261 (>= ?e146 ?e153)) +(flet ($e262 (= ?e20 ?e215)) +(flet ($e263 (>= ?e213 ?e21)) +(flet ($e264 (p0 ?e216 ?e168)) +(flet ($e265 (< ?e210 ?e162)) +(flet ($e266 (distinct ?e126 ?e127)) +(flet ($e267 (<= ?e131 ?e223)) +(flet ($e268 (p0 ?e179 ?e7)) +(flet ($e269 (< ?e150 ?e13)) +(flet ($e270 (<= ?e160 ?e182)) +(flet ($e271 (<= ?e180 ?e206)) +(flet ($e272 (= ?e191 ?e206)) +(flet ($e273 (p0 ?e155 ?e180)) +(flet ($e274 (distinct ?e116 ?e186)) +(flet ($e275 (>= ?e173 ?e179)) +(flet ($e276 (p0 ?e16 ?e118)) +(flet ($e277 (p0 ?e164 ?e209)) +(flet ($e278 (>= ?e178 ?e182)) +(flet ($e279 (> ?e138 ?e139)) +(flet ($e280 (> ?e8 ?e110)) +(flet ($e281 (p0 ?e113 ?e157)) +(flet ($e282 (< ?e127 ?e167)) +(flet ($e283 (< ?e222 ?e152)) +(flet ($e284 (= ?e205 ?e201)) +(flet ($e285 (distinct ?e141 ?e153)) +(flet ($e286 (p0 ?e211 ?e140)) +(flet ($e287 (distinct ?e21 ?e10)) +(flet ($e288 (>= ?e182 ?e172)) +(flet ($e289 (< ?e224 ?e159)) +(flet ($e290 (distinct ?e134 ?e118)) +(flet ($e291 (>= ?e170 ?e186)) +(flet ($e292 (> ?e206 ?e11)) +(flet ($e293 (<= v1 ?e160)) +(flet ($e294 (> ?e175 ?e132)) +(flet ($e295 (p0 ?e131 ?e11)) +(flet ($e296 (<= ?e173 ?e137)) +(flet ($e297 (distinct ?e182 ?e165)) +(flet ($e298 (distinct ?e22 ?e159)) +(flet ($e299 (>= ?e155 ?e223)) +(flet ($e300 (p0 ?e10 ?e23)) +(flet ($e301 (= ?e219 ?e11)) +(flet ($e302 (>= ?e181 ?e129)) +(flet ($e303 (< ?e132 ?e150)) +(flet ($e304 (>= ?e204 ?e174)) +(flet ($e305 (p0 ?e16 ?e114)) +(flet ($e306 (<= ?e145 ?e120)) +(flet ($e307 (>= ?e138 ?e190)) +(flet ($e308 (<= ?e190 ?e210)) +(flet ($e309 (> ?e166 ?e198)) +(flet ($e310 (= ?e136 ?e128)) +(flet ($e311 (distinct ?e170 ?e189)) +(flet ($e312 (p0 ?e185 ?e208)) +(flet ($e313 (> ?e143 ?e214)) +(flet ($e314 (= ?e125 ?e194)) +(flet ($e315 (distinct ?e204 ?e157)) +(flet ($e316 (<= ?e183 ?e150)) +(flet ($e317 (> ?e112 ?e113)) +(flet ($e318 (= ?e130 ?e123)) +(flet ($e319 (= ?e7 ?e213)) +(flet ($e320 (= v0 ?e174)) +(flet ($e321 (distinct ?e149 ?e171)) +(flet ($e322 (< ?e178 ?e158)) +(flet ($e323 (< ?e129 ?e155)) +(flet ($e324 (> ?e136 v1)) +(flet ($e325 (= ?e200 v0)) +(flet ($e326 (> ?e162 ?e147)) +(flet ($e327 (< ?e196 ?e182)) +(flet ($e328 (> ?e125 ?e132)) +(flet ($e329 (> ?e12 ?e215)) +(flet ($e330 (<= ?e202 ?e177)) +(flet ($e331 (<= ?e120 ?e114)) +(flet ($e332 (distinct ?e203 ?e132)) +(flet ($e333 (< ?e172 ?e190)) +(flet ($e334 (<= ?e193 ?e170)) +(flet ($e335 (>= ?e175 ?e193)) +(flet ($e336 (>= ?e187 ?e209)) +(flet ($e337 (> ?e19 ?e210)) +(flet ($e338 (> ?e18 ?e172)) +(flet ($e339 (distinct ?e210 ?e177)) +(flet ($e340 (distinct ?e19 ?e106)) +(flet ($e341 (= ?e134 ?e175)) +(flet ($e342 (< ?e21 ?e121)) +(flet ($e343 (> ?e199 ?e148)) +(flet ($e344 (<= ?e184 v2)) +(flet ($e345 (p0 ?e199 ?e137)) +(flet ($e346 (>= ?e15 ?e131)) +(flet ($e347 (< ?e131 ?e180)) +(flet ($e348 (< ?e206 ?e12)) +(flet ($e349 (< ?e173 ?e147)) +(flet ($e350 (<= ?e142 ?e115)) +(flet ($e351 (distinct ?e223 v1)) +(flet ($e352 (> ?e217 ?e187)) +(flet ($e353 (> ?e12 ?e163)) +(flet ($e354 (> ?e15 ?e153)) +(flet ($e355 (>= ?e184 ?e163)) +(flet ($e356 (p0 ?e210 ?e212)) +(flet ($e357 (>= ?e193 ?e114)) +(flet ($e358 (> ?e108 ?e187)) +(flet ($e359 (p0 ?e222 ?e224)) +(flet ($e360 (>= ?e128 ?e168)) +(flet ($e361 (distinct ?e186 ?e18)) +(flet ($e362 (< ?e117 ?e179)) +(flet ($e363 (> ?e199 ?e200)) +(flet ($e364 (<= ?e201 ?e179)) +(flet ($e365 (<= ?e120 ?e187)) +(flet ($e366 (p0 ?e151 ?e188)) +(flet ($e367 (> ?e149 ?e135)) +(flet ($e368 (< ?e205 ?e142)) +(flet ($e369 (>= ?e126 ?e220)) +(flet ($e370 (>= ?e151 ?e169)) +(flet ($e371 (p0 ?e115 ?e126)) +(flet ($e372 (<= ?e22 ?e123)) +(flet ($e373 (>= v0 ?e153)) +(flet ($e374 (> ?e14 ?e128)) +(flet ($e375 (= ?e163 ?e118)) +(flet ($e376 (<= ?e204 ?e135)) +(flet ($e377 (p0 ?e210 ?e167)) +(flet ($e378 (= ?e124 ?e213)) +(flet ($e379 (distinct ?e13 ?e194)) +(flet ($e380 (< ?e171 ?e15)) +(flet ($e381 (< ?e15 ?e156)) +(flet ($e382 (= ?e140 ?e206)) +(flet ($e383 (<= ?e123 v1)) +(flet ($e384 (> ?e194 ?e138)) +(flet ($e385 (= ?e107 ?e127)) +(flet ($e386 (> ?e155 ?e142)) +(flet ($e387 (distinct ?e177 ?e153)) +(flet ($e388 (distinct ?e9 ?e23)) +(flet ($e389 (= ?e136 ?e207)) +(flet ($e390 (= ?e151 ?e212)) +(flet ($e391 (distinct ?e192 ?e218)) +(flet ($e392 (= ?e151 ?e222)) +(flet ($e393 (> ?e195 ?e204)) +(flet ($e394 (= ?e214 ?e121)) +(flet ($e395 (= ?e207 ?e157)) +(flet ($e396 (< ?e205 ?e190)) +(flet ($e397 (>= ?e206 ?e215)) +(flet ($e398 (>= ?e178 ?e210)) +(flet ($e399 (= ?e6 ?e136)) +(flet ($e400 (>= ?e7 ?e150)) +(flet ($e401 (= ?e146 ?e174)) +(flet ($e402 (p0 ?e220 ?e207)) +(flet ($e403 (>= ?e20 ?e131)) +(flet ($e404 (< ?e126 ?e211)) +(flet ($e405 (> ?e208 ?e121)) +(flet ($e406 (< ?e131 ?e222)) +(flet ($e407 (= ?e184 ?e168)) +(flet ($e408 (= ?e210 v2)) +(flet ($e409 (p0 ?e215 ?e147)) +(flet ($e410 (distinct ?e195 ?e108)) +(flet ($e411 (p0 ?e140 ?e151)) +(flet ($e412 (p0 ?e125 ?e214)) +(flet ($e413 (distinct ?e218 ?e167)) +(flet ($e414 (= ?e136 ?e206)) +(flet ($e415 (= ?e22 ?e213)) +(flet ($e416 (>= ?e203 ?e155)) +(flet ($e417 (distinct ?e109 ?e120)) +(flet ($e418 (= ?e112 ?e160)) +(flet ($e419 (> ?e17 ?e146)) +(flet ($e420 (>= ?e200 ?e161)) +(flet ($e421 (>= ?e221 ?e171)) +(flet ($e422 (= ?e157 ?e210)) +(flet ($e423 (> ?e120 ?e118)) +(flet ($e424 (< ?e113 ?e165)) +(flet ($e425 (< ?e183 ?e197)) +(flet ($e426 (<= ?e211 ?e197)) +(flet ($e427 (= ?e136 ?e195)) +(flet ($e428 (= ?e216 ?e222)) +(flet ($e429 (p0 ?e178 ?e204)) +(flet ($e430 (<= ?e111 ?e195)) +(flet ($e431 (> ?e13 ?e199)) +(flet ($e432 (p0 ?e195 ?e136)) +(flet ($e433 (> ?e210 ?e109)) +(flet ($e434 (= ?e15 v2)) +(flet ($e435 (>= ?e168 ?e220)) +(flet ($e436 (< ?e108 ?e213)) +(flet ($e437 (distinct ?e155 ?e142)) +(flet ($e438 (>= ?e173 ?e185)) +(flet ($e439 (= ?e196 ?e209)) +(flet ($e440 (p0 ?e124 ?e15)) +(flet ($e441 (>= v1 ?e200)) +(flet ($e442 (<= ?e132 ?e106)) +(flet ($e443 (p0 ?e15 ?e168)) +(flet ($e444 (>= ?e145 ?e139)) +(flet ($e445 (= ?e198 ?e146)) +(flet ($e446 (= ?e119 ?e140)) +(flet ($e447 (>= ?e16 ?e177)) +(flet ($e448 (< ?e221 ?e200)) +(flet ($e449 (= ?e8 ?e18)) +(flet ($e450 (<= ?e132 ?e134)) +(flet ($e451 (p0 ?e164 v0)) +(flet ($e452 (>= ?e123 ?e12)) +(flet ($e453 (distinct ?e214 ?e199)) +(flet ($e454 (< ?e16 ?e195)) +(flet ($e455 (= ?e6 ?e159)) +(flet ($e456 (> v0 ?e196)) +(flet ($e457 (distinct ?e225 ?e221)) +(flet ($e458 (>= ?e163 ?e146)) +(flet ($e459 (distinct ?e225 ?e212)) +(flet ($e460 (= ?e8 ?e218)) +(flet ($e461 (p0 ?e211 ?e205)) +(flet ($e462 (>= ?e118 ?e176)) +(flet ($e463 (distinct ?e156 ?e171)) +(flet ($e464 (> ?e121 ?e191)) +(flet ($e465 (= ?e202 ?e190)) +(flet ($e466 (= ?e141 ?e149)) +(flet ($e467 (= ?e203 ?e143)) +(flet ($e468 (>= ?e213 ?e132)) +(flet ($e469 (p0 ?e16 ?e161)) +(flet ($e470 (distinct ?e116 v0)) +(flet ($e471 (= ?e156 ?e153)) +(flet ($e472 (p0 ?e130 ?e114)) +(flet ($e473 (<= ?e169 ?e161)) +(flet ($e474 (p0 ?e129 ?e203)) +(flet ($e475 (distinct ?e22 ?e119)) +(flet ($e476 (> ?e194 ?e158)) +(flet ($e477 (> ?e173 ?e222)) +(flet ($e478 (>= ?e112 ?e137)) +(flet ($e479 (< ?e219 ?e120)) +(flet ($e480 (p0 ?e109 ?e211)) +(flet ($e481 (< ?e162 ?e18)) +(flet ($e482 (< ?e160 ?e138)) +(flet ($e483 (p0 ?e111 ?e206)) +(flet ($e484 (<= ?e122 ?e17)) +(flet ($e485 (>= ?e144 ?e171)) +(flet ($e486 (implies $e97 $e362)) +(flet ($e487 (or $e47 $e428)) +(flet ($e488 (implies $e401 $e238)) +(flet ($e489 (xor $e308 $e55)) +(flet ($e490 (not $e60)) +(flet ($e491 (xor $e78 $e366)) +(flet ($e492 (not $e283)) +(flet ($e493 (iff $e353 $e404)) +(flet ($e494 (implies $e446 $e228)) +(flet ($e495 (iff $e259 $e386)) +(flet ($e496 (iff $e236 $e226)) +(flet ($e497 (iff $e394 $e322)) +(flet ($e498 (xor $e255 $e290)) +(flet ($e499 (not $e459)) +(flet ($e500 (or $e277 $e306)) +(flet ($e501 (or $e414 $e81)) +(flet ($e502 (if_then_else $e286 $e475 $e243)) +(flet ($e503 (or $e447 $e449)) +(flet ($e504 (xor $e252 $e288)) +(flet ($e505 (iff $e365 $e339)) +(flet ($e506 (or $e390 $e418)) +(flet ($e507 (and $e51 $e317)) +(flet ($e508 (or $e270 $e30)) +(flet ($e509 (or $e332 $e321)) +(flet ($e510 (implies $e361 $e298)) +(flet ($e511 (not $e29)) +(flet ($e512 (or $e346 $e264)) +(flet ($e513 (not $e399)) +(flet ($e514 (if_then_else $e413 $e94 $e327)) +(flet ($e515 (implies $e261 $e42)) +(flet ($e516 (not $e482)) +(flet ($e517 (or $e325 $e280)) +(flet ($e518 (and $e25 $e452)) +(flet ($e519 (iff $e347 $e481)) +(flet ($e520 (implies $e516 $e409)) +(flet ($e521 (not $e457)) +(flet ($e522 (implies $e348 $e388)) +(flet ($e523 (xor $e103 $e241)) +(flet ($e524 (and $e305 $e326)) +(flet ($e525 (iff $e488 $e44)) +(flet ($e526 (and $e387 $e250)) +(flet ($e527 (iff $e389 $e383)) +(flet ($e528 (iff $e382 $e318)) +(flet ($e529 (and $e239 $e511)) +(flet ($e530 (and $e296 $e439)) +(flet ($e531 (or $e292 $e26)) +(flet ($e532 (not $e301)) +(flet ($e533 (implies $e320 $e431)) +(flet ($e534 (not $e262)) +(flet ($e535 (implies $e514 $e456)) +(flet ($e536 (if_then_else $e485 $e468 $e49)) +(flet ($e537 (or $e79 $e479)) +(flet ($e538 (if_then_else $e274 $e460 $e393)) +(flet ($e539 (xor $e343 $e297)) +(flet ($e540 (xor $e265 $e532)) +(flet ($e541 (iff $e340 $e429)) +(flet ($e542 (not $e61)) +(flet ($e543 (if_then_else $e82 $e260 $e46)) +(flet ($e544 (iff $e367 $e465)) +(flet ($e545 (not $e66)) +(flet ($e546 (not $e54)) +(flet ($e547 (or $e237 $e358)) +(flet ($e548 (and $e539 $e400)) +(flet ($e549 (or $e249 $e368)) +(flet ($e550 (if_then_else $e427 $e377 $e526)) +(flet ($e551 (implies $e229 $e287)) +(flet ($e552 (implies $e396 $e518)) +(flet ($e553 (and $e517 $e430)) +(flet ($e554 (and $e331 $e437)) +(flet ($e555 (xor $e553 $e314)) +(flet ($e556 (and $e469 $e263)) +(flet ($e557 (if_then_else $e335 $e461 $e524)) +(flet ($e558 (if_then_else $e24 $e48 $e48)) +(flet ($e559 (implies $e324 $e304)) +(flet ($e560 (xor $e379 $e300)) +(flet ($e561 (not $e455)) +(flet ($e562 (xor $e27 $e59)) +(flet ($e563 (and $e445 $e311)) +(flet ($e564 (implies $e275 $e512)) +(flet ($e565 (iff $e498 $e484)) +(flet ($e566 (if_then_else $e43 $e336 $e282)) +(flet ($e567 (iff $e458 $e513)) +(flet ($e568 (iff $e356 $e315)) +(flet ($e569 (if_then_else $e550 $e235 $e310)) +(flet ($e570 (or $e487 $e422)) +(flet ($e571 (implies $e506 $e534)) +(flet ($e572 (xor $e99 $e547)) +(flet ($e573 (and $e68 $e88)) +(flet ($e574 (iff $e100 $e472)) +(flet ($e575 (iff $e542 $e556)) +(flet ($e576 (or $e385 $e350)) +(flet ($e577 (xor $e90 $e536)) +(flet ($e578 (iff $e505 $e234)) +(flet ($e579 (iff $e360 $e374)) +(flet ($e580 (iff $e391 $e573)) +(flet ($e581 (xor $e65 $e370)) +(flet ($e582 (if_then_else $e490 $e426 $e559)) +(flet ($e583 (not $e71)) +(flet ($e584 (not $e276)) +(flet ($e585 (and $e72 $e502)) +(flet ($e586 (and $e436 $e552)) +(flet ($e587 (and $e375 $e267)) +(flet ($e588 (not $e574)) +(flet ($e589 (not $e434)) +(flet ($e590 (not $e581)) +(flet ($e591 (not $e299)) +(flet ($e592 (and $e411 $e345)) +(flet ($e593 (and $e41 $e486)) +(flet ($e594 (and $e302 $e93)) +(flet ($e595 (not $e543)) +(flet ($e596 (if_then_else $e85 $e395 $e70)) +(flet ($e597 (or $e273 $e36)) +(flet ($e598 (implies $e371 $e525)) +(flet ($e599 (and $e507 $e582)) +(flet ($e600 (not $e403)) +(flet ($e601 (implies $e480 $e594)) +(flet ($e602 (xor $e231 $e271)) +(flet ($e603 (or $e384 $e580)) +(flet ($e604 (implies $e565 $e35)) +(flet ($e605 (or $e546 $e548)) +(flet ($e606 (implies $e92 $e233)) +(flet ($e607 (if_then_else $e601 $e102 $e500)) +(flet ($e608 (if_then_else $e67 $e392 $e52)) +(flet ($e609 (or $e266 $e39)) +(flet ($e610 (implies $e575 $e599)) +(flet ($e611 (xor $e566 $e293)) +(flet ($e612 (if_then_else $e602 $e330 $e529)) +(flet ($e613 (or $e603 $e256)) +(flet ($e614 (and $e590 $e483)) +(flet ($e615 (not $e415)) +(flet ($e616 (if_then_else $e64 $e373 $e352)) +(flet ($e617 (and $e540 $e489)) +(flet ($e618 (and $e560 $e560)) +(flet ($e619 (not $e281)) +(flet ($e620 (if_then_else $e291 $e521 $e451)) +(flet ($e621 (and $e230 $e528)) +(flet ($e622 (or $e519 $e617)) +(flet ($e623 (and $e329 $e577)) +(flet ($e624 (or $e571 $e606)) +(flet ($e625 (or $e610 $e313)) +(flet ($e626 (not $e477)) +(flet ($e627 (xor $e435 $e378)) +(flet ($e628 (and $e530 $e307)) +(flet ($e629 (not $e96)) +(flet ($e630 (not $e76)) +(flet ($e631 (and $e355 $e621)) +(flet ($e632 (implies $e412 $e495)) +(flet ($e633 (not $e31)) +(flet ($e634 (and $e363 $e632)) +(flet ($e635 (not $e440)) +(flet ($e636 (implies $e463 $e607)) +(flet ($e637 (if_then_else $e576 $e309 $e32)) +(flet ($e638 (or $e433 $e557)) +(flet ($e639 (if_then_else $e77 $e568 $e80)) +(flet ($e640 (not $e242)) +(flet ($e641 (iff $e333 $e53)) +(flet ($e642 (or $e541 $e474)) +(flet ($e643 (xor $e470 $e87)) +(flet ($e644 (or $e624 $e269)) +(flet ($e645 (not $e535)) +(flet ($e646 (and $e612 $e407)) +(flet ($e647 (iff $e62 $e316)) +(flet ($e648 (xor $e600 $e45)) +(flet ($e649 (if_then_else $e608 $e627 $e634)) +(flet ($e650 (and $e246 $e372)) +(flet ($e651 (if_then_else $e227 $e626 $e503)) +(flet ($e652 (iff $e337 $e397)) +(flet ($e653 (implies $e645 $e583)) +(flet ($e654 (and $e551 $e398)) +(flet ($e655 (not $e417)) +(flet ($e656 (implies $e527 $e563)) +(flet ($e657 (or $e38 $e636)) +(flet ($e658 (xor $e232 $e448)) +(flet ($e659 (or $e616 $e57)) +(flet ($e660 (iff $e558 $e589)) +(flet ($e661 (not $e442)) +(flet ($e662 (xor $e416 $e649)) +(flet ($e663 (xor $e75 $e578)) +(flet ($e664 (implies $e476 $e258)) +(flet ($e665 (or $e655 $e424)) +(flet ($e666 (not $e295)) +(flet ($e667 (not $e646)) +(flet ($e668 (if_then_else $e462 $e663 $e33)) +(flet ($e669 (iff $e572 $e662)) +(flet ($e670 (not $e357)) +(flet ($e671 (iff $e510 $e254)) +(flet ($e672 (xor $e272 $e641)) +(flet ($e673 (or $e604 $e251)) +(flet ($e674 (implies $e34 $e338)) +(flet ($e675 (if_then_else $e37 $e381 $e303)) +(flet ($e676 (iff $e544 $e253)) +(flet ($e677 (implies $e673 $e654)) +(flet ($e678 (not $e661)) +(flet ($e679 (or $e667 $e95)) +(flet ($e680 (implies $e587 $e319)) +(flet ($e681 (implies $e596 $e471)) +(flet ($e682 (not $e651)) +(flet ($e683 (and $e515 $e656)) +(flet ($e684 (implies $e497 $e501)) +(flet ($e685 (xor $e402 $e478)) +(flet ($e686 (not $e666)) +(flet ($e687 (iff $e450 $e354)) +(flet ($e688 (iff $e623 $e643)) +(flet ($e689 (implies $e376 $e554)) +(flet ($e690 (iff $e342 $e638)) +(flet ($e691 (implies $e671 $e562)) +(flet ($e692 (and $e682 $e630)) +(flet ($e693 (or $e633 $e323)) +(flet ($e694 (and $e650 $e91)) +(flet ($e695 (and $e648 $e56)) +(flet ($e696 (xor $e351 $e441)) +(flet ($e697 (not $e244)) +(flet ($e698 (or $e678 $e499)) +(flet ($e699 (or $e618 $e248)) +(flet ($e700 (or $e586 $e653)) +(flet ($e701 (xor $e597 $e364)) +(flet ($e702 (and $e684 $e278)) +(flet ($e703 (or $e683 $e657)) +(flet ($e704 (and $e408 $e652)) +(flet ($e705 (iff $e28 $e692)) +(flet ($e706 (xor $e454 $e701)) +(flet ($e707 (if_then_else $e672 $e664 $e257)) +(flet ($e708 (if_then_else $e660 $e613 $e588)) +(flet ($e709 (xor $e695 $e659)) +(flet ($e710 (implies $e706 $e593)) +(flet ($e711 (xor $e443 $e537)) +(flet ($e712 (implies $e69 $e591)) +(flet ($e713 (not $e622)) +(flet ($e714 (xor $e545 $e50)) +(flet ($e715 (and $e620 $e40)) +(flet ($e716 (not $e285)) +(flet ($e717 (xor $e523 $e689)) +(flet ($e718 (if_then_else $e665 $e531 $e670)) +(flet ($e719 (implies $e555 $e716)) +(flet ($e720 (xor $e698 $e669)) +(flet ($e721 (or $e585 $e98)) +(flet ($e722 (xor $e561 $e538)) +(flet ($e723 (xor $e492 $e268)) +(flet ($e724 (iff $e509 $e569)) +(flet ($e725 (if_then_else $e675 $e685 $e699)) +(flet ($e726 (xor $e676 $e691)) +(flet ($e727 (implies $e104 $e467)) +(flet ($e728 (xor $e419 $e709)) +(flet ($e729 (if_then_else $e631 $e496 $e640)) +(flet ($e730 (xor $e680 $e284)) +(flet ($e731 (iff $e609 $e609)) +(flet ($e732 (not $e438)) +(flet ($e733 (if_then_else $e567 $e642 $e693)) +(flet ($e734 (or $e637 $e731)) +(flet ($e735 (if_then_else $e101 $e635 $e584)) +(flet ($e736 (not $e679)) +(flet ($e737 (or $e719 $e732)) +(flet ($e738 (implies $e344 $e734)) +(flet ($e739 (or $e406 $e718)) +(flet ($e740 (and $e721 $e453)) +(flet ($e741 (iff $e491 $e58)) +(flet ($e742 (or $e423 $e700)) +(flet ($e743 (and $e724 $e520)) +(flet ($e744 (iff $e294 $e710)) +(flet ($e745 (not $e410)) +(flet ($e746 (iff $e725 $e473)) +(flet ($e747 (implies $e493 $e359)) +(flet ($e748 (implies $e681 $e349)) +(flet ($e749 (xor $e421 $e595)) +(flet ($e750 (implies $e639 $e735)) +(flet ($e751 (or $e712 $e714)) +(flet ($e752 (and $e549 $e508)) +(flet ($e753 (not $e625)) +(flet ($e754 (implies $e598 $e369)) +(flet ($e755 (and $e564 $e728)) +(flet ($e756 (and $e744 $e89)) +(flet ($e757 (not $e105)) +(flet ($e758 (and $e687 $e752)) +(flet ($e759 (or $e707 $e717)) +(flet ($e760 (xor $e240 $e63)) +(flet ($e761 (or $e746 $e754)) +(flet ($e762 (implies $e466 $e380)) +(flet ($e763 (iff $e592 $e644)) +(flet ($e764 (xor $e738 $e83)) +(flet ($e765 (xor $e720 $e751)) +(flet ($e766 (or $e420 $e739)) +(flet ($e767 (implies $e726 $e289)) +(flet ($e768 (iff $e703 $e341)) +(flet ($e769 (if_then_else $e432 $e674 $e764)) +(flet ($e770 (iff $e74 $e658)) +(flet ($e771 (and $e742 $e704)) +(flet ($e772 (if_then_else $e570 $e743 $e84)) +(flet ($e773 (xor $e425 $e748)) +(flet ($e774 (iff $e759 $e668)) +(flet ($e775 (not $e769)) +(flet ($e776 (iff $e775 $e504)) +(flet ($e777 (implies $e768 $e772)) +(flet ($e778 (and $e328 $e708)) +(flet ($e779 (not $e761)) +(flet ($e780 (or $e740 $e686)) +(flet ($e781 (iff $e628 $e711)) +(flet ($e782 (not $e766)) +(flet ($e783 (implies $e757 $e780)) +(flet ($e784 (or $e444 $e779)) +(flet ($e785 (implies $e765 $e729)) +(flet ($e786 (iff $e767 $e756)) +(flet ($e787 (not $e750)) +(flet ($e788 (not $e677)) +(flet ($e789 (if_then_else $e773 $e605 $e705)) +(flet ($e790 (not $e312)) +(flet ($e791 (if_then_else $e749 $e783 $e713)) +(flet ($e792 (iff $e762 $e522)) +(flet ($e793 (xor $e760 $e279)) +(flet ($e794 (or $e755 $e73)) +(flet ($e795 (and $e690 $e776)) +(flet ($e796 (if_then_else $e789 $e247 $e334)) +(flet ($e797 (not $e793)) +(flet ($e798 (if_then_else $e688 $e782 $e727)) +(flet ($e799 (iff $e741 $e614)) +(flet ($e800 (and $e494 $e791)) +(flet ($e801 (if_then_else $e730 $e798 $e781)) +(flet ($e802 (implies $e736 $e777)) +(flet ($e803 (not $e696)) +(flet ($e804 (xor $e533 $e694)) +(flet ($e805 (if_then_else $e615 $e723 $e747)) +(flet ($e806 (iff $e799 $e405)) +(flet ($e807 (not $e805)) +(flet ($e808 (and $e794 $e787)) +(flet ($e809 (implies $e802 $e245)) +(flet ($e810 (not $e808)) +(flet ($e811 (not $e770)) +(flet ($e812 (or $e629 $e745)) +(flet ($e813 (xor $e797 $e812)) +(flet ($e814 (not $e763)) +(flet ($e815 (iff $e806 $e806)) +(flet ($e816 (not $e758)) +(flet ($e817 (and $e737 $e733)) +(flet ($e818 (or $e722 $e792)) +(flet ($e819 (or $e803 $e804)) +(flet ($e820 (or $e611 $e647)) +(flet ($e821 (and $e810 $e702)) +(flet ($e822 (or $e817 $e817)) +(flet ($e823 (or $e821 $e786)) +(flet ($e824 (not $e771)) +(flet ($e825 (if_then_else $e807 $e619 $e809)) +(flet ($e826 (implies $e464 $e790)) +(flet ($e827 (or $e715 $e579)) +(flet ($e828 (if_then_else $e784 $e697 $e818)) +(flet ($e829 (if_then_else $e825 $e814 $e811)) +(flet ($e830 (and $e828 $e800)) +(flet ($e831 (not $e826)) +(flet ($e832 (if_then_else $e830 $e819 $e830)) +(flet ($e833 (iff $e832 $e829)) +(flet ($e834 (xor $e785 $e827)) +(flet ($e835 (implies $e824 $e824)) +(flet ($e836 (not $e778)) +(flet ($e837 (not $e834)) +(flet ($e838 (not $e831)) +(flet ($e839 (xor $e836 $e836)) +(flet ($e840 (or $e820 $e801)) +(flet ($e841 (and $e813 $e815)) +(flet ($e842 (xor $e788 $e837)) +(flet ($e843 (and $e838 $e823)) +(flet ($e844 (xor $e835 $e841)) +(flet ($e845 (implies $e796 $e774)) +(flet ($e846 (and $e816 $e753)) +(flet ($e847 (not $e845)) +(flet ($e848 (or $e842 $e833)) +(flet ($e849 (if_then_else $e847 $e840 $e822)) +(flet ($e850 (and $e846 $e86)) +(flet ($e851 (xor $e849 $e844)) +(flet ($e852 (xor $e795 $e848)) +(flet ($e853 (iff $e843 $e839)) +(flet ($e854 (not $e852)) +(flet ($e855 (or $e853 $e854)) +(flet ($e856 (if_then_else $e851 $e855 $e850)) +$e856 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +