diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-08 23:54:18 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-08 23:54:18 +0000 |
commit | 2979089be3bc655d8bdd6245e193f356b4f7c93c (patch) | |
tree | ddb51fd7df95a39e7c67c3c08a3c6cbd3cc9ff42 /src/theory/arith | |
parent | 44ac537312dcba8fc179f5ea9489e8cd7266f71c (diff) |
Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 136 |
1 files changed, 5 insertions, 131 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3ea8b9550..4ce1113a4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1008,7 +1008,7 @@ Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){ Polynomial rp = Polynomial::parsePolynomial(r); Polynomial qp = Polynomial::parsePolynomial(q); - Node abs_d = (n.isConstant()) ? + Node abs_d = (n.isConstant()) ? d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$"); Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode(); @@ -1016,9 +1016,7 @@ Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){ Node leq1 = currNM->mkNode(LT, r, abs_d); Node andE = currNM->mkNode(AND, eq, leq0, leq1); - Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE); - Node lem = abs_d.getMetaKind () == metakind::VARIABLE ? defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode; @@ -1469,130 +1467,6 @@ bool TheoryArith::assertionCases(Constraint constraint){ 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. @@ -2281,11 +2155,11 @@ void TheoryArith::notifyRestart(){ }else if(d_tableauResetDensity * copySize <= currSize){ d_simplex.reduceQueue(); if(safeToReset()){ - Debug("arith::reset") << "resetting " << d_restartsCounter << endl; - ++d_statistics.d_currSetToSmaller; - d_tableau = d_smallTableauCopy; + Debug("arith::reset") << "resetting " << d_restartsCounter << endl; + ++d_statistics.d_currSetToSmaller; + d_tableau = d_smallTableauCopy; }else{ - Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl; + Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl; } } } |