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