From: Tim King Date: Fri, 22 Oct 2010 20:22:39 +0000 (+0000) Subject: Code cleanup for TheoryArith. X-Git-Tag: cvc5-1.0.0~8790 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6dee1d9817d8e9209f0a681b7c601ec6b4b5014d;p=cvc5.git Code cleanup for TheoryArith. --- diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index f099e77b9..c764d0d2e 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -206,6 +206,41 @@ inline int deltaCoeff(Kind k){ } } +/** + * Given a rewritten predicate to TheoryArith return a single kind to + * to indicate its underlying structure. + * The function returns the following in each case: + * - (K left right) -> K where is a wildcard for EQUAL, LEQ, or GEQ: + * - (NOT (EQUAL left right)) -> DISTINCT + * - (NOT (LEQ left right)) -> GT + * - (NOT (GEQ left right)) -> LT + * If none of these match, it returns UNDEFINED_KIND. + */ + inline Kind simplifiedKind(TNode assertion){ + switch(assertion.getKind()){ + case kind::LEQ: + case kind::GEQ: + case kind::EQUAL: + return assertion.getKind(); + case kind::NOT: + { + TNode atom = assertion[0]; + switch(atom.getKind()){ + case kind::LEQ: //(not (LEQ x c)) <=> (GT x c) + return kind::GT; + case kind::GEQ: //(not (GEQ x c) <=> (LT x c) + return kind::LT; + case kind::EQUAL: + return kind::DISTINCT; + default: + return kind::UNDEFINED_KIND; + } + } + default: + return kind::UNDEFINED_KIND; + } +} + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index bee24aa39..39685a2a1 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -50,6 +50,8 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){ d_hasSafeAssignment[x] = true; d_history.push_back(x); } + + d_deltaIsSafe = false; d_assignment[x] = r; } void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){ @@ -65,6 +67,8 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con d_history.push_back(x); } } + + d_deltaIsSafe = false; d_assignment[x] = r; } @@ -101,14 +105,14 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){ /** Must know that the bound exists both calling this! */ const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) { Assert(inMaps(x)); - Assert(!d_upperConstraint[x].isNull()); + Assert(hasUpperBound(x)); return d_upperBound[x]; } const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) { Assert(inMaps(x)); - Assert(!d_lowerConstraint[x].isNull()); + Assert(hasLowerBound(x)); return d_lowerBound[x]; } @@ -122,6 +126,15 @@ const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{ } } +const DeltaRational& ArithPartialModel::getAssignment(ArithVar x, bool safe) const{ + Assert(inMaps(x)); + if(safe && d_hasSafeAssignment[x]){ + return d_safeAssignment[x]; + }else{ + return d_assignment[x]; + } +} + const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{ Assert(inMaps(x)); return d_assignment[x]; @@ -146,20 +159,20 @@ void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){ TNode ArithPartialModel::getLowerConstraint(ArithVar x){ Assert(inMaps(x)); - Assert(!d_lowerConstraint[x].isNull()); + Assert(hasLowerBound(x)); return d_lowerConstraint[x]; } TNode ArithPartialModel::getUpperConstraint(ArithVar x){ Assert(inMaps(x)); - Assert(!d_upperConstraint[x].isNull()); + Assert(hasUpperBound(x)); return d_upperConstraint[x]; } bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ - if(d_lowerConstraint[x].isNull()){ + if(!hasLowerBound(x)){ // l = -\intfy // ? c < -\infty |- _|_ return false; @@ -172,7 +185,7 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool } bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ - if(d_upperConstraint[x].isNull()){ + if(!hasUpperBound(x)){ // u = \intfy // ? c > \infty |- _|_ return false; @@ -183,14 +196,13 @@ bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool return c >= d_upperBound[x]; } } - -bool ArithPartialModel::hasBounds(ArithVar x){ - return !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull(); +bool ArithPartialModel::hasEitherBound(ArithVar x){ + return hasLowerBound(x) || hasUpperBound(x); } bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){ Assert(inMaps(x)); - if(d_upperConstraint[x].isNull()){ // u = \infty + if(!hasUpperBound(x)){ // u = \infty return true; } return d_assignment[x] < d_upperBound[x]; @@ -198,7 +210,7 @@ bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ Assert(inMaps(x)); - if(d_lowerConstraint[x].isNull()){ // l = -\infty + if(!hasLowerBound(x)){ // l = -\infty return true; } return d_lowerBound[x] < d_assignment[x]; @@ -224,6 +236,10 @@ void ArithPartialModel::clearSafeAssignments(bool revert){ } } + if(revert && !d_history.empty()){ + d_deltaIsSafe = true; + } + d_history.clear(); } @@ -236,13 +252,13 @@ void ArithPartialModel::commitAssignmentChanges(){ void ArithPartialModel::printModel(ArithVar x){ Debug("model") << "model" << x << ":"<< getAssignment(x) << " "; - if(d_lowerConstraint[x].isNull()){ + if(!hasLowerBound(x)){ Debug("model") << "no lb "; }else{ Debug("model") << getLowerBound(x) << " "; Debug("model") << getLowerConstraint(x) << " "; } - if(d_upperConstraint[x].isNull()){ + if(!hasUpperBound(x)){ Debug("model") << "no ub "; }else{ Debug("model") << getUpperBound(x) << " "; @@ -270,11 +286,11 @@ void ArithPartialModel::computeDelta(){ for(ArithVar x = 0; x < d_mapSize; ++x){ const DeltaRational& a = getAssignment(x); - if(!d_lowerConstraint[x].isNull()){ + if(hasLowerBound(x)){ const DeltaRational& l = getLowerBound(x); deltaIsSmallerThan(l,a); } - if(!d_upperConstraint[x].isNull()){ + if(hasUpperBound(x)){ const DeltaRational& u = getUpperBound(x); deltaIsSmallerThan(a,u); } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 518d59fbd..2edfdebca 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -88,6 +88,7 @@ public: /* Gets the last assignment to a variable that is known to be conistent. */ const DeltaRational& getSafeAssignment(ArithVar x) const; + const DeltaRational& getAssignment(ArithVar x, bool safe) const; /* Reverts all variable assignments to their safe values. */ void revertAssignmentChanges(); @@ -131,7 +132,13 @@ public: void printModel(ArithVar x); /** returns true iff x has both a lower and upper bound. */ - bool hasBounds(ArithVar x); + bool hasEitherBound(ArithVar x); + inline bool hasLowerBound(ArithVar x){ + return !d_lowerConstraint[x].isNull(); + } + inline bool hasUpperBound(ArithVar x){ + return !d_upperConstraint[x].isNull(); + } bool hasEverHadABound(ArithVar var){ return d_hasHadABound[var]; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9458ab153..f913eda93 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -127,7 +127,7 @@ bool isNormalAtom(TNode n){ bool TheoryArith::shouldEject(ArithVar var){ - if(d_partialModel.hasBounds(var)){ + if(d_partialModel.hasEitherBound(var)){ return false; }else if(d_tableau.isEjected(var)) { return false; @@ -171,8 +171,8 @@ void TheoryArith::reinjectVariable(ArithVar x){ d_tableau.reinjectBasic(x); - DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x); - DeltaRational assignment = computeRowValueUsingAssignment(x); + DeltaRational safeAssignment = computeRowValue(x, true); + DeltaRational assignment = computeRowValue(x, false); d_partialModel.setAssignment(x,safeAssignment,assignment); } @@ -307,8 +307,8 @@ void TheoryArith::setupInitialValue(ArithVar x){ //This can go away if the tableau creation is done at preregister //time instead of register - DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x); - DeltaRational assignment = computeRowValueUsingAssignment(x); + DeltaRational safeAssignment = computeRowValue(x, true); + DeltaRational assignment = computeRowValue(x, false); d_partialModel.initialize(x,safeAssignment); d_partialModel.setAssignment(x,assignment); @@ -317,10 +317,6 @@ void TheoryArith::setupInitialValue(ArithVar x){ //lower bound. This is done to strongly enforce the notion that basic //variables should not be changed without begin checked. - //Strictly speaking checking x is unnessecary as it cannot have an upper or - //lower bound. This is done to strongly enforce the notion that basic - //variables should not be changed without begin checked. - } Debug("arithgc") << "setupVariable("<begin(); i != row->end();++i){ ArithVar nonbasic = i->first; const Rational& coeff = i->second; - const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic); - sum = sum + (assignment * coeff); - } - return sum; -} - -/** - * Computes the value of a basic variable using the current assignment. - */ -DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(ArithVar x){ - Assert(d_basicManager.isBasic(x)); - DeltaRational sum = d_constants.d_ZERO_DELTA; - Row* row = d_tableau.lookup(x); - for(Row::iterator i = row->begin(); i != row->end();++i){ - ArithVar nonbasic = i->first; - const Rational& coeff = i->second; - const DeltaRational& assignment = d_partialModel.getSafeAssignment(nonbasic); + const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); sum = sum + (assignment * coeff); } return sum; } + RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { return d_nextRewriter.preRewrite(n); } @@ -368,12 +349,7 @@ void TheoryArith::registerTerm(TNode tn){ } /* procedure AssertUpper( x_i <= c_i) */ -bool TheoryArith::AssertUpper(TNode n, TNode original){ - TNode nodeX_i = n[0]; - ArithVar x_i = asArithVar(nodeX_i); - Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind()))); - DeltaRational c_i(n[1].getConst(), dcoeff); - +bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){ @@ -409,12 +385,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ } /* procedure AssertLower( x_i >= c_i ) */ -bool TheoryArith::AssertLower(TNode n, TNode original){ - TNode nodeX_i = n[0]; - ArithVar x_i = asArithVar(nodeX_i); - Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind()))); - DeltaRational c_i(n[1].getConst(),dcoeff); - +bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){ @@ -449,11 +420,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ } /* procedure AssertLower( x_i == c_i ) */ -bool TheoryArith::AssertEquality(TNode n, TNode original){ - Assert(n.getKind() == EQUAL); - TNode nodeX_i = n[0]; - ArithVar x_i = asArithVar(nodeX_i); - DeltaRational c_i(n[1].getConst()); +bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; @@ -501,7 +468,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ return false; } -void TheoryArith::update(ArithVar x_i, DeltaRational& v){ +void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ Assert(!d_basicManager.isBasic(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); ++(d_statistics.d_statUpdates); @@ -757,61 +724,66 @@ Node TheoryArith::generateConflictBelow(ArithVar conflictVar){ return conflict; } +template +TNode getSide(TNode assertion, Kind simpleKind){ + switch(simpleKind){ + case LT: + case GT: + case DISTINCT: + return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; + case LEQ: + case GEQ: + case EQUAL: + return selectLeft ? assertion[0] : assertion[1]; + default: + Unreachable(); + return TNode::null(); + } +} -//TODO get rid of this! -Node TheoryArith::simulatePreprocessing(TNode n){ - if(n.getKind() == NOT){ - Node sub = simulatePreprocessing(n[0]); - Assert(sub.getKind() != NOT); - return NodeManager::currentNM()->mkNode(NOT,sub); +ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){ + TNode left = getSide(assertion, simpleKind); + if(isTheoryLeaf(left)){ + return asArithVar(left); }else{ - Assert(isNormalAtom(n)); - Kind k = n.getKind(); - - Assert(isRelationOperator(k)); - if(n[0].getMetaKind() == metakind::VARIABLE){ - return n; - }else { - TNode left = n[0]; - TNode right = n[1]; - Assert(left.hasAttribute(Slack())); - Node slack = left.getAttribute(Slack()); - return NodeManager::currentNM()->mkNode(k,slack,right); - } + Assert(left.hasAttribute(Slack())); + TNode slack = left.getAttribute(Slack()); + return asArithVar(slack); } } -bool TheoryArith::assertionCases(TNode original, TNode assertion){ - switch(assertion.getKind()){ +DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ + TNode right = getSide(assertion, simpleKind); + + Assert(right.getKind() == CONST_RATIONAL); + const Rational& noninf = right.getConst(); + + Rational inf = Rational(Integer(deltaCoeff(simpleKind))); + return DeltaRational(noninf, inf); +} + +bool TheoryArith::assertionCases(TNode assertion){ + Kind simpKind = simplifiedKind(assertion); + Assert(simpKind != UNDEFINED_KIND); + ArithVar x_i = determineLeftVariable(assertion, simpKind); + DeltaRational c_i = determineRightConstant(assertion, simpKind); + + Debug("arith_assertions") << "arith assertion(" << assertion + << " \\-> " + < (GT x c) - { - Node pushedin = pushInNegation(assertion); - return AssertLower(pushedin,original); - } - case GEQ: //(not (GEQ x c) <=> (LT x c) - { - Node pushedin = pushInNegation(assertion); - return AssertUpper(pushedin,original); - } - case EQUAL: - d_diseq.push_back(assertion); - return false; - default: - Unreachable(); - return false; - } - } + return AssertEquality(x_i, c_i, assertion); + case DISTINCT: + d_diseq.push_back(assertion); + return false; default: Unreachable(); return false; @@ -823,14 +795,10 @@ void TheoryArith::check(Effort level){ while(!done()){ - Node original = get(); - Node assertion = simulatePreprocessing(original); - Debug("arith_assertions") << "arith assertion(" << original - << " \\-> " << assertion << ")" << std::endl; - - d_propagator.assertLiteral(original); - bool conflictDuringAnAssert = assertionCases(original, assertion); + Node assertion = get(); + d_propagator.assertLiteral(assertion); + bool conflictDuringAnAssert = assertionCases(assertion); if(conflictDuringAnAssert){ d_partialModel.revertAssignmentChanges(); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 26dcc9825..5d00c4cc8 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -153,16 +153,18 @@ private: * * returns true if a conflict was asserted. */ - bool AssertLower(TNode n, TNode orig); - bool AssertUpper(TNode n, TNode orig); + bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig); + bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig); + bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig); + + ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); - bool AssertEquality(TNode n, TNode orig); /** * Updates the assignment of a nonbasic variable x_i to v. * Also updates the assignment of basic variables accordingly. */ - void update(ArithVar x_i, DeltaRational& v); + void update(ArithVar x_i, const DeltaRational& v); /** * Updates the value of a basic variable x_i to v, @@ -233,12 +235,14 @@ private: /** Initial (not context dependent) sets up for a new slack variable.*/ void setupSlack(TNode left); - - /** Computes the value of a row in the tableau using the current assignment.*/ - DeltaRational computeRowValueUsingAssignment(ArithVar x); - - /** Computes the value of a row in the tableau using the safe assignment.*/ - DeltaRational computeRowValueUsingSavedAssignment(ArithVar x); + /** + * Computes the value of a basic variable using the assignments + * of the values of the variables in the basic variable's row tableau. + * This can compute the value using either: + * - the the current assignment (useSafe=false) or + * - the safe assignment (useSafe = true). + */ + DeltaRational computeRowValue(ArithVar x, bool useSafe); /** Checks to make sure the assignment is consistent with the tableau. */ void checkTableau(); @@ -250,16 +254,13 @@ private: * Handles the case splitting for check() for a new assertion. * returns true if their is a conflict. */ - bool assertionCases(TNode original, TNode assertion); + bool assertionCases(TNode assertion); ArithVar findBasicRow(ArithVar variable); bool shouldEject(ArithVar var); void ejectInactiveVariables(); void reinjectVariable(ArithVar x); - //TODO get rid of this! - Node simulatePreprocessing(TNode n); - void asVectors(Polynomial& p, std::vector& coeffs, std::vector& variables) const;