From 9da04b35ddb44761285af21519023d88f3adf1b5 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 6 Jun 2010 17:06:07 +0000 Subject: [PATCH] Some assorted fixes and local optimizations for theory arith. --- src/theory/arith/partial_model.cpp | 52 +++---- src/theory/arith/partial_model.h | 56 ++++---- src/theory/arith/tableau.h | 25 +++- src/theory/arith/theory_arith.cpp | 209 ++++++++++------------------- src/theory/arith/theory_arith.h | 4 + 5 files changed, 144 insertions(+), 202 deletions(-) diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index d4be75559..bb2864cf9 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -44,19 +44,16 @@ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - Assert(x.hasAttribute(partial_model::Assignment())); + Assert(x.hasAttribute(partial_model::SafeAssignment())); DeltaRational* curr = x.getAttribute(partial_model::Assignment()); - if(d_unsafeMode){ - Assert(x.hasAttribute(partial_model::SafeAssignment())); - DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment()); - if(saved == NULL){ - saved = new DeltaRational(*curr); - x.setAttribute(partial_model::SafeAssignment(), saved); - d_history.push_back(x); - } + DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment()); + if(saved == NULL){ + saved = new DeltaRational(*curr); + x.setAttribute(partial_model::SafeAssignment(), saved); + d_history.push_back(x); } *curr = r; @@ -99,14 +96,14 @@ DeltaRational ArithPartialModel::getLowerBound(TNode x) const{ DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - if(d_unsafeMode){ - Assert( x.hasAttribute(partial_model::SafeAssignment())); - DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment()); - if(safeAssignment != NULL){ - return *safeAssignment; - } + Assert( x.hasAttribute(SafeAssignment())); + + DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); + if(safeAssignment != NULL){ + return *safeAssignment; + }else{ + return getAssignment(x); //The current assignment is safe. } - return getAssignment(x); } const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{ @@ -238,34 +235,19 @@ bool ArithPartialModel::assignmentIsConsistent(TNode x){ return above_li && below_ui; } -void ArithPartialModel::turnOnUnsafeMode(){ - Assert(!d_unsafeMode); - Assert(d_history.empty()); - - d_unsafeMode = true; -} - -void ArithPartialModel::turnOffUnsafeMode(){ - Assert(d_unsafeMode); - Assert(d_history.empty()); - - d_unsafeMode = false; -} void ArithPartialModel::clearSafeAssignments(bool revert){ - Assert(d_unsafeMode); for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){ TNode x = *i; - Assert(x.hasAttribute(partial_model::SafeAssignment())); + Assert(x.hasAttribute(SafeAssignment())); + Assert(x.hasAttribute(Assignment())); - DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment()); + DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); if(revert){ - Assert(x.hasAttribute(partial_model::Assignment())); - - DeltaRational* assign = x.getAttribute(partial_model::Assignment()); + DeltaRational* assign = x.getAttribute(Assignment()); *assign = *safeAssignment; } x.setAttribute(partial_model::SafeAssignment(), NULL); diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index d04d8dd8c..26f9a135b 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -60,12 +60,13 @@ typedef expr::Attribute CDDRationalMap; -/* Side disucssion for why new tables are introduced instead of using the attribute - * framework. - * It comes down to that the obvious ways to use the current attribute framework do - * do not provide a terribly satisfying answer. +/* Side disucssion for why new tables are introduced instead of using the + * attribute framework. + * It comes down to that the obvious ways to use the current attribute + * framework do not provide a terribly satisfying answer. * - Suppose the type of the attribute is CD and maps to type DeltaRational. - * Well it can't map to a DeltaRational, and it thus it will be a DeltaRational* + * Well it can't map to a DeltaRational, and it thus it will be a + * DeltaRational* * However being context dependent means givening up cleanup functions. * So this leaks memory. * - Suppose the type of the attribute is CD and the type mapped to @@ -74,22 +75,23 @@ typedef context::CDMap CDDRationalMap; * Inefficiency: Every lookup and comparison will require going through the * massaging in between a node and the constant being wrapped. Every update * requires going through the additional expense of creating at least 1 node. - * The Uglyness: If this was chosen it would also suggest using comparisons against - * DeltaRationals for the tracking the constraints for conflict analysis. - * This seems to invite misuse and introducing Nodes that should probably not escape - * arith. - * - Suppose that the of the attribute was not CD and mapped to a CDO - * or similarly a ContextObj that wraps a DeltaRational*. + * The Uglyness: If this was chosen it would also suggest using comparisons + * against DeltaRationals for the tracking the constraints for conflict + * analysis. This seems to invite misuse and introducing Nodes that should + * probably not escape arith. + * - Suppose that the of the attribute was not CD and mapped to a + * CDO or similarly a ContextObj that wraps a DeltaRational*. * This is currently rejected just because this is difficult to get right, - * and maintain. However with enough effort this the best solution is probably of - * this form. + * and maintain. However with enough effort this the best solution is + * probably of this form. */ /** * This is the literal that was asserted in the current context to the theory * that asserted the tightest lower bound on a variable. - * For example: for a variable x this could be the constraint (>= x 4) or (not (<= x 50)) + * For example: for a variable x this could be the constraint + * (>= x 4) or (not (<= x 50)) * Note the strong correspondence between this and LowerBoundMap. * This is used during conflict analysis. */ @@ -117,18 +119,18 @@ private: partial_model::CDDRationalMap d_UpperBoundMap; + /** + * List contains all of the variables that have an unsafe assignment. + */ typedef std::vector HistoryList; HistoryList d_history; - bool d_unsafeMode; - public: ArithPartialModel(context::Context* c): d_LowerBoundMap(c), d_UpperBoundMap(c), - d_history(), - d_unsafeMode(false) + d_history() { } void setLowerConstraint(TNode x, TNode constraint); @@ -138,23 +140,24 @@ public: + /* Initializes a variable to a safe value.*/ void initialize(TNode x, const DeltaRational& r); + /* Gets the last assignment to a variable that is known to be conistent. */ DeltaRational getSafeAssignment(TNode x) const; - bool isInUnsafeMode() { return d_unsafeMode; } - - void turnOnUnsafeMode(); - void turnOffUnsafeMode(); - + /* Reverts all variable assignments to their safe values. */ void revertAssignmentChanges(); - void commitAssignmentChanges(); + /* Commits all variables assignments as safe.*/ + void commitAssignmentChanges(); void setUpperBound(TNode x, const DeltaRational& r); void setLowerBound(TNode x, const DeltaRational& r); + + /* Sets an unsafe variable assignment */ void setAssignment(TNode x, const DeltaRational& r); /** Must know that the bound exists before calling this! */ @@ -182,6 +185,11 @@ public: void printModel(TNode x); private: + + /** + * This function implements the mostly identical: + * revertAssignmentChanges() and commitAssignmentChanges(). + */ void clearSafeAssignments(bool revert); }; diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index e43b48c66..a5499db08 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -55,7 +55,6 @@ public: //TODO Assert(d_x_i.getType() == REAL); Assert(sum.getKind() == PLUS); - Rational zero(0,1); for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){ TNode pair = *iter; @@ -68,10 +67,9 @@ public: //TODO Assert(var_i.getKind() == REAL); Assert(!has(var_i)); d_nonbasic.insert(var_i); - Rational q = coeff.getConst(); - d_coeffs[var_i] = q; - Assert(q != zero); - Assert(d_coeffs[var_i] != zero); + d_coeffs[var_i] = coeff.getConst(); + Assert(coeff.getConst() != Rational(0,1)); + Assert(d_coeffs[var_i] != Rational(0,1)); } } @@ -134,7 +132,21 @@ public: iter != row_s.d_nonbasic.end(); ++iter){ TNode x_j = *iter; - Rational a_sj = a_rs * row_s.lookup(x_j); + Rational a_sj = row_s.lookup(x_j); + a_sj *= a_rs; + CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j); + + if(coeff_iter != d_coeffs.end()){ + coeff_iter->second += a_sj; + if(coeff_iter->second == zero){ + d_coeffs.erase(coeff_iter); + d_nonbasic.erase(x_j); + } + }else{ + d_nonbasic.insert(x_j); + d_coeffs.insert(make_pair(x_j,a_sj)); + } + /* if(has(x_j)){ d_coeffs[x_j] = d_coeffs[x_j] + a_sj; if(d_coeffs[x_j] == zero){ @@ -145,6 +157,7 @@ public: d_nonbasic.insert(x_j); d_coeffs[x_j] = a_sj; } + */ } } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 92781e0ba..6c6a61adf 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -30,7 +30,6 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" -//#include "theory/arith/normal.h" #include "theory/arith/slack.h" #include "theory/arith/basic.h" @@ -87,7 +86,7 @@ bool isBasicSum(TNode n){ } bool isNormalAtom(TNode n){ - + if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){ return false; } @@ -109,6 +108,7 @@ void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm(" << n << ")" << endl; + Kind k = n.getKind(); if(n.getKind() == EQUAL){ if(!n.getAttribute(EagerlySplitUpon())){ TNode left = n[0]; @@ -131,47 +131,20 @@ void TheoryArith::preRegisterTerm(TNode n) { setupVariable(n); } - //TODO is an atom - if(isRelationOperator(n.getKind())){ + //TODO is an atom + if(isRelationOperator(k)){ Assert(isNormalAtom(n)); - Node normalForm(n); - - if(normalForm.getKind() == NOT){ - normalForm = pushInNegation(normalForm); - } - Kind k = normalForm.getKind(); - - if(k != kind::CONST_BOOLEAN){ - Assert(isRelationOperator(k)); - TNode left = normalForm[0]; - TNode right = normalForm[1]; - if(left.getKind() == PLUS){ - //We may need to introduce a slack variable. - Assert(left.getNumChildren() >= 2); - Assert(isBasicSum(left)); - Node slack; - if(!left.getAttribute(Slack(), slack)){ - //TODO - TypeNode real_type = NodeManager::currentNM()->realType(); - slack = NodeManager::currentNM()->mkVar(real_type); - - left.setAttribute(Slack(), slack); - makeBasic(slack); - - Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); - slackEqLeft.setAttribute(TheoryArithPropagated(), true); - //TODO this has to be wrong no? YES (dejan) - // d_out->lemma(slackEqLeft); - - Debug("slack") << "slack " << slackEqLeft << endl; - - d_tableau.addRow(slackEqLeft); - - setupVariable(slack); - } + TNode left = n[0]; + TNode right = n[1]; + if(left.getKind() == PLUS){ + //We may need to introduce a slack variable. + Assert(left.getNumChildren() >= 2); + Assert(isBasicSum(left)); + if(!left.hasAttribute(Slack())){ + setupSlack(left); } } } @@ -180,7 +153,23 @@ void TheoryArith::preRegisterTerm(TNode n) { << n << ")" << endl; } +void TheoryArith::setupSlack(TNode left){ + //TODO + TypeNode real_type = NodeManager::currentNM()->realType(); + Node slack = NodeManager::currentNM()->mkVar(real_type); + + left.setAttribute(Slack(), slack); + makeBasic(slack); + + Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left); + slackEqLeft.setAttribute(TheoryArithPropagated(), true); + + Debug("slack") << "slack " << slackEqLeft << endl; + d_tableau.addRow(slackEqLeft); + + setupVariable(slack); +} void TheoryArith::checkBasicVariable(TNode basic){ @@ -491,31 +480,13 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 Debug("arith") << "updateInconsistentVars" << endl; - d_partialModel.turnOnUnsafeMode(); - while(true){ - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } TNode x_i = selectSmallestInconsistentVar(); Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == Node::null()){ Debug("arith_update") << "No inconsistent variables" << endl; - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } - - d_partialModel.commitAssignmentChanges(); - d_partialModel.turnOffUnsafeMode(); - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } - - - return Node::null(); //sat } DeltaRational beta_i = d_partialModel.getAssignment(x_i); @@ -524,21 +495,6 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational l_i = d_partialModel.getLowerBound(x_i); TNode x_j = selectSlackBelow(x_i); if(x_j == TNode::null() ){ - Debug("arith_update") << "conflict below" << endl; - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } - - d_partialModel.revertAssignmentChanges(); - d_partialModel.turnOffUnsafeMode(); - //d_partialModel.stopRecordingAssignments(true); - //d_partialModel.beginRecordingAssignments(); - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } - return generateConflictBelow(x_i); //unsat } pivotAndUpdate(x_i, x_j, l_i); @@ -547,20 +503,6 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational u_i = d_partialModel.getUpperBound(x_i); TNode x_j = selectSlackAbove(x_i); if(x_j == TNode::null() ){ - Debug("arith_update") << "conflict above" << endl; - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } - - d_partialModel.revertAssignmentChanges(); - d_partialModel.turnOffUnsafeMode(); - //d_partialModel.stopRecordingAssignments(true); - //d_partialModel.beginRecordingAssignments(); - - if(debugTagIsOn("paranoid:check_tableau")){ - checkTableau(); - } return generateConflictAbove(x_i); //unsat } pivotAndUpdate(x_i, x_j, u_i); @@ -592,12 +534,14 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){ if(a_ij < d_constants.d_ZERO){ bound = d_partialModel.getUpperConstraint(nonbasic); Debug("arith") << "below 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " << bound << endl; + << d_partialModel.getAssignment(nonbasic) + << " " << bound << endl; nb << bound; }else{ bound = d_partialModel.getLowerConstraint(nonbasic); Debug("arith") << " above 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " << bound << endl; + << d_partialModel.getAssignment(nonbasic) + << " " << bound << endl; nb << bound; } } @@ -628,13 +572,15 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){ if(a_ij < d_constants.d_ZERO){ TNode bound = d_partialModel.getLowerConstraint(nonbasic); Debug("arith") << "Lower "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl; + << d_partialModel.getAssignment(nonbasic) << " " + << bound << endl; nb << bound; }else{ TNode bound = d_partialModel.getUpperConstraint(nonbasic); Debug("arith") << "Upper "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " "<< bound << endl; + << d_partialModel.getAssignment(nonbasic) << " " + << bound << endl; nb << bound; } @@ -655,37 +601,17 @@ Node TheoryArith::simulatePreprocessing(TNode n){ } }else{ Assert(isNormalAtom(n)); - Node rewritten = n; - Kind k = rewritten.getKind(); - -// if(rewritten.getKind() == NOT){ -// Node sub = simulatePreprocessing(rewritten[0]); -// if(sub.getKind() == NOT){ -// return sub[0]; -// }else{ -// return NodeManager::currentNM()->mkNode(NOT,sub); -// } -// } else - if(!isRelationOperator(k)){ - if(rewritten.getKind() == CONST_BOOLEAN){ - Warning() << "How did I get a const boolean here" << endl; - Warning() << "offending node has id " << n.getId() << endl; - Warning() << "offending node is "<< n << endl; - return rewritten; - }else{ - Unreachable("Unexpected type!"); - } - }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){ - return rewritten; + Kind k = n.getKind(); + + Assert(isRelationOperator(k)); + if(n[0].getMetaKind() == metakind::VARIABLE){ + return n; }else { - TNode left = rewritten[0]; - TNode right = rewritten[1]; - Node slack; - if(!left.getAttribute(Slack(), slack)){ - Unreachable("Slack must be have been created!"); - }else{ - return NodeManager::currentNM()->mkNode(k,slack,right); - } + TNode left = n[0]; + TNode right = n[1]; + Assert(left.hasAttribute(Slack())); + Node slack = left.getAttribute(Slack()); + return NodeManager::currentNM()->mkNode(k,slack,right); } } } @@ -693,6 +619,7 @@ Node TheoryArith::simulatePreprocessing(TNode n){ void TheoryArith::check(Effort level){ Debug("arith") << "TheoryArith::check begun" << std::endl; + bool conflictDuringAnAssert = false; while(!done()){ @@ -705,17 +632,14 @@ void TheoryArith::check(Effort level){ d_preprocessed.push_back(assertion); switch(assertion.getKind()){ - case CONST_BOOLEAN: - Warning() << "No bools should be reached dagnabbit" << endl; - break; case LEQ: - conflictDuringAnAssert = AssertUpper(assertion, original); + conflictDuringAnAssert |= AssertUpper(assertion, original); break; case GEQ: - conflictDuringAnAssert = AssertLower(assertion, original); + conflictDuringAnAssert |= AssertLower(assertion, original); break; case EQUAL: - conflictDuringAnAssert = AssertUpper(assertion, original); + conflictDuringAnAssert |= AssertUpper(assertion, original); conflictDuringAnAssert |= AssertLower(assertion, original); break; case NOT: @@ -725,21 +649,18 @@ void TheoryArith::check(Effort level){ case LEQ: //(not (LEQ x c)) <=> (GT x c) { Node pushedin = pushInNegation(assertion); - conflictDuringAnAssert = AssertLower(pushedin,original); + conflictDuringAnAssert |= AssertLower(pushedin,original); break; } case GEQ: //(not (GEQ x c) <=> (LT x c) { Node pushedin = pushInNegation(assertion); - conflictDuringAnAssert = AssertUpper(pushedin,original); + conflictDuringAnAssert |= AssertUpper(pushedin,original); break; } case EQUAL: d_diseq.push_back(assertion); break; - case CONST_BOOLEAN: - Warning() << "No bools should be reached dagnabbit" << endl; - break; default: Unhandled(); } @@ -750,10 +671,10 @@ void TheoryArith::check(Effort level){ } } if(conflictDuringAnAssert){ - //clear the queue; - while(!done()) { - get(); - } + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + d_partialModel.revertAssignmentChanges(); + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + //return return; } @@ -761,10 +682,24 @@ void TheoryArith::check(Effort level){ if(fullEffort(level)){ Node possibleConflict = updateInconsistentVars(); if(possibleConflict != Node::null()){ + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + + d_partialModel.revertAssignmentChanges(); + + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + + d_out->conflict(possibleConflict, true); + + Debug("arith_conflict") << "Found a conflict " << possibleConflict << endl; - d_out->conflict(possibleConflict); }else{ + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + + d_partialModel.commitAssignmentChanges(); + + if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } + Debug("arith_conflict") << "No conflict found" << endl; } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index cdd73782e..e54f273e9 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -97,12 +97,16 @@ private: Node generateConflictBelow(TNode conflictVar); void setupVariable(TNode x); + void setupSlack(TNode left); + DeltaRational computeRowValueUsingAssignment(TNode x); DeltaRational computeRowValueUsingSavedAssignment(TNode x); void checkTableau(); void checkBasicVariable(TNode basic); + + //TODO get rid of this! Node simulatePreprocessing(TNode n); -- 2.30.2