From 2581001b96a64e1d11d826cf554d378ac522bbe2 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 14 Jun 2012 19:29:25 +0000 Subject: Fixed arithmetic consistency issue. The simplex conflict variable had to be reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled. --- src/theory/arith/arith_priority_queue.h | 5 ++ src/theory/arith/simplex.cpp | 5 ++ src/theory/arith/simplex.h | 6 ++ src/theory/arith/theory_arith.cpp | 109 +++++++++++++++++++++++--------- src/theory/arith/theory_arith.h | 1 + 5 files changed, 95 insertions(+), 31 deletions(-) (limited to 'src/theory') diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index a4f30e18b..fb80e599e 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -217,6 +217,11 @@ public: void clear(); + bool collectionModeContains(ArithVar v) const { + Assert(inCollectionMode()); + return d_varSet.isMember(v); + } + class const_iterator { private: Mode d_mode; diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index ee71dea74..63bb42e7a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -241,6 +241,7 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_conflictVariable == ARITHVAR_SENTINEL); + Assert(d_queue.inCollectionMode()); if(d_queue.empty()){ return Result::SAT; @@ -352,6 +353,10 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){ d_pivotsInRound.purge(); + // ensure that the conflict variable is still in the queue. + if(d_conflictVariable != ARITHVAR_SENTINEL){ + d_queue.enqueueIfInconsistent(d_conflictVariable); + } d_conflictVariable = ARITHVAR_SENTINEL; d_queue.transitionToCollectionMode(); diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index d260ff9b4..a1c69548c 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -224,6 +224,12 @@ public: d_queue.clear(); } + + bool debugIsInCollectionQueue(ArithVar var) const{ + Assert(d_queue.inCollectionMode()); + return d_queue.collectionModeContains(var); + } + private: /** Reports a conflict to on the output channel. */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index a48a13720..4bc066e08 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -678,7 +678,7 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst Assert(elim == Rewriter::rewrite(elim)); - static const int MAX_SUB_SIZE = 20; + static const unsigned MAX_SUB_SIZE = 20; if(false && right.size() > MAX_SUB_SIZE){ Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl; Debug("simplify") << right.size() << endl; @@ -1384,7 +1384,13 @@ void TheoryArith::check(Effort effortLevel){ Debug("effortlevel") << "TheoryArith::check " << effortLevel << std::endl; Debug("arith") << "TheoryArith::check begun " << effortLevel << std::endl; + if(Debug.isOn("arith::consistency")){ + Assert(unenqueuedVariablesAreConsistent()); + } + bool newFacts = !done(); + //If previous == SAT, then reverts on conflicts are safe + //Otherwise, they are not and must be committed. Result::Sat previous = d_qflraStatus; if(newFacts){ d_qflraStatus = Result::SAT_UNKNOWN; @@ -1397,28 +1403,36 @@ void TheoryArith::check(Effort effortLevel){ bool res = assertionCases(curr); Assert(!res || inConflict()); } - if(inConflict()){ - revertOutOfConflict(); - outputConflicts(); - d_qflraStatus = Result::UNSAT; - return; + if(inConflict()){ break; } + } + if(!inConflict()){ + 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()){ break; } } } - 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()){ + d_qflraStatus = Result::UNSAT; + if(previous == Result::SAT){ + ++d_statistics.d_revertsOnConflicts; + revertOutOfConflict(); + d_simplex.clearQueue(); + }else{ + ++d_statistics.d_commitsOnConflicts; - if(inConflict()){ - d_qflraStatus = Result::UNSAT; + d_partialModel.commitAssignmentChanges(); revertOutOfConflict(); - outputConflicts(); - return; } + outputConflicts(); + return; } @@ -1427,8 +1441,6 @@ void TheoryArith::check(Effort effortLevel){ } bool emmittedConflictOrSplit = false; - - Assert(d_conflicts.empty()); d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel)); @@ -1439,6 +1451,9 @@ void TheoryArith::check(Effort effortLevel){ } d_partialModel.commitAssignmentChanges(); d_unknownsInARow = 0; + if(Debug.isOn("arith::consistency")){ + Assert(entireStateIsConsistent()); + } break; case Result::SAT_UNKNOWN: ++d_unknownsInARow; @@ -1451,7 +1466,6 @@ void TheoryArith::check(Effort effortLevel){ d_unknownsInARow = 0; if(previous == Result::SAT){ ++d_statistics.d_revertsOnConflicts; - revertOutOfConflict(); d_simplex.clearQueue(); }else{ @@ -1515,8 +1529,9 @@ void TheoryArith::check(Effort effortLevel){ if(inConflict()){ Debug("arith::unate") << "unate conflict" << endl; revertOutOfConflict(); + d_qflraStatus = Result::UNSAT; outputConflicts(); - return; + emmittedConflictOrSplit = true; } }else{ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); @@ -1720,15 +1735,15 @@ void TheoryArith::propagate(Effort e) { while(d_constraintDatabase.hasMorePropagations()){ Constraint c = d_constraintDatabase.nextPropagation(); + Debug("arith::prop") << "next prop" << getSatContext()->getLevel() << ": " << c << endl; if(c->negationHasProof()){ - Node conflict = ConstraintValue::explainConflict(c, c->getNegation()); - Message() << "tears " << conflict << endl; - Debug("arith::prop") << "propagate conflict" << conflict << endl; - d_out->conflict(conflict); - return; - }else if(!c->assertedToTheTheory()){ + Debug("arith::prop") << "negation has proof " << c->getNegation() << endl + << c->getNegation()->explainForConflict() << endl; + } + Assert(!c->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true. Contact Tim now!"); + if(!c->assertedToTheTheory()){ Node literal = c->getLiteral(); Debug("arith::prop") << "propagating @" << getSatContext()->getLevel() << " " << literal << endl; @@ -1845,6 +1860,8 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { Node TheoryArith::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); + Assert(d_qflraStatus == Result::SAT); + switch(n.getKind()) { case kind::VARIABLE: { ArithVar var = d_arithvarNodeMap.asArithVar(n); @@ -1946,15 +1963,40 @@ void TheoryArith::notifyRestart(){ bool TheoryArith::entireStateIsConsistent(){ typedef std::vector::const_iterator VarIter; + bool result = true; for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ ArithVar var = d_arithvarNodeMap.asArithVar(*i); if(!d_partialModel.assignmentIsConsistent(var)){ d_partialModel.printModel(var); - Warning() << "Assignment is not consistent for " << var << *i << endl; - return false; + Warning() << "Assignment is not consistent for " << var << *i; + if(d_tableau.isBasic(var)){ + Warning() << " (basic)"; + } + Warning() << endl; + result = false; } } - return true; + return result; +} + +bool TheoryArith::unenqueuedVariablesAreConsistent(){ + typedef std::vector::const_iterator VarIter; + bool result = true; + for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ + ArithVar var = d_arithvarNodeMap.asArithVar(*i); + if(!d_partialModel.assignmentIsConsistent(var) && + !d_simplex.debugIsInCollectionQueue(var)){ + + d_partialModel.printModel(var); + Warning() << "Unenqueued var is not consistent for " << var << *i; + if(d_tableau.isBasic(var)){ + Warning() << " (basic)"; + } + Warning() << endl; + result = false; + } + } + return result; } void TheoryArith::presolve(){ @@ -2066,12 +2108,17 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ bool hasProof = bestImplied->hasProof(); Debug("arith::prop") << "arith::prop" << basic - //<< " " << assertedValuation << " " << assertedToTheTheory << " " << canBePropagated << " " << hasProof << endl; + if(bestImplied->negationHasProof()){ + Warning() << "the negation of " << bestImplied << " : " << endl + << "has proof " << bestImplied->getNegation() << endl + << bestImplied->getNegation()->explainForConflict() << endl; + } + if(!assertedToTheTheory && canBePropagated && !hasProof ){ if(upperBound){ Assert(bestImplied != d_partialModel.getUpperBoundConstraint(basic)); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 556495c97..4983b0557 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -460,6 +460,7 @@ private: * Returns true iff every variable is consistent in the partial model. */ bool entireStateIsConsistent(); + bool unenqueuedVariablesAreConsistent(); bool isImpliedUpperBound(ArithVar var, Node exp); bool isImpliedLowerBound(ArithVar var, Node exp); -- cgit v1.2.3