diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 18 | ||||
-rw-r--r-- | src/theory/arith/constraint.cpp | 64 | ||||
-rw-r--r-- | src/theory/arith/constraint.h | 9 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 436 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 26 |
6 files changed, 408 insertions, 154 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 649e34134..14d2370ab 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -7,8 +7,9 @@ namespace CVC4 { namespace theory { namespace arith { -ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node) - : d_conflict(c), +ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict) + : d_inConflict(c), + d_raiseConflict(raiseConflict), d_notify(*this), d_keepAlive(c), d_propagatations(c), @@ -112,7 +113,7 @@ bool ArithCongruenceManager::propagate(TNode x){ ++(d_statistics.d_conflicts); Node conf = flattenAnd(explainInternal(x)); - d_conflict.set(conf); + raiseConflict(conf); Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl; return false; } @@ -141,7 +142,7 @@ bool ArithCongruenceManager::propagate(TNode x){ Node final = flattenAnd(conf); ++(d_statistics.d_conflicts); - d_conflict.set(final); + raiseConflict(final); Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl; return false; } diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 63a370f9a..1864bc89e 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -25,7 +25,8 @@ namespace arith { class ArithCongruenceManager { private: - context::CDMaybe<Node> d_conflict; + context::CDRaised d_inConflict; + NodeCallBack& d_raiseConflict; /** * The set of ArithVars equivalent to a pair of terms. @@ -101,17 +102,18 @@ private: eq::EqualityEngine d_ee; + void raiseConflict(Node conflict){ + Assert(!inConflict()); + Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl; + d_inConflict.raise(); + d_raiseConflict(conflict); + } public: bool inConflict() const{ - return d_conflict.isSet(); + return d_inConflict.isRaised(); }; - Node conflict() const{ - Assert(inConflict()); - return d_conflict.get(); - } - bool hasMorePropagations() const { return !d_propagatations.empty(); } @@ -182,7 +184,7 @@ private: public: - ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&); + ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack& setLiteral, const ArithVarNodeMap&, NodeCallBack& raiseConflict); Node explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d451e9597..bedb91756 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -448,7 +448,7 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm) +ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm, NodeCallBack& raiseConflict) : d_varDatabases(), d_toPropagate(satContext), d_proofs(satContext, false), @@ -456,7 +456,8 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_av2nodeMap(av2nodeMap), d_congruenceManager(cm), d_satContext(satContext), - d_satAllocationLevel(d_satContext->getLevel()) + d_satAllocationLevel(d_satContext->getLevel()), + d_raiseConflict(raiseConflict) { d_selfExplainingProof = d_proofs.size(); d_proofs.push_back(NullConstraint); @@ -1153,6 +1154,20 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas) } } +void ConstraintDatabase::raiseUnateConflict(Constraint ant, Constraint cons){ + Assert(ant->hasProof()); + Constraint negCons = cons->getNegation(); + Assert(negCons->hasProof()); + + Debug("arith::unate::conf") << ant << "implies " << cons << endl; + Debug("arith::unate::conf") << negCons << " is true." << endl; + + + Node conf = ConstraintValue::explainConflict(ant, negCons); + Debug("arith::unate::conf") << conf << std::endl; + d_raiseConflict(conf); +} + void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl; Assert(curr != prev); @@ -1186,17 +1201,25 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){ //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ Constraint lb = vc.getLowerBound(); - if(!lb->isTrue()){ + if(lb->negationHasProof()){ + raiseUnateConflict(curr, lb); + return; + }else if(!lb->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl; + lb->impliedBy(curr); } } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); } } @@ -1229,7 +1252,10 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ Constraint ub = vc.getUpperBound(); - if(!ub->isTrue()){ + if(ub->negationHasProof()){ + raiseUnateConflict(curr, ub); + return; + }else if(!ub->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl; ub->impliedBy(curr); @@ -1237,9 +1263,13 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){ } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; ++d_statistics.d_unatePropagateImplications; + dis->impliedBy(curr); } } @@ -1279,7 +1309,10 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //These should all be handled by propagating the LowerBounds! if(vc.hasLowerBound()){ Constraint lb = vc.getLowerBound(); - if(!lb->isTrue()){ + if(lb->negationHasProof()){ + raiseUnateConflict(curr, lb); + return; + }else if(!lb->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl; lb->impliedBy(curr); @@ -1287,9 +1320,13 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl; + dis->impliedBy(curr); } } @@ -1307,15 +1344,22 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C //These should all be handled by propagating the UpperBounds! if(vc.hasUpperBound()){ Constraint ub = vc.getUpperBound(); - if(!ub->isTrue()){ + if(ub->negationHasProof()){ + raiseUnateConflict(curr, ub); + return; + }else if(!ub->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl; + ub->impliedBy(curr); } } if(vc.hasDisequality()){ Constraint dis = vc.getDisequality(); - if(!dis->isTrue()){ + if(dis->negationHasProof()){ + raiseUnateConflict(curr, dis); + return; + }else if(!dis->isTrue()){ ++d_statistics.d_unatePropagateImplications; Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl; dis->impliedBy(curr); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 5b49dd54d..dcc3bf8bb 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -762,6 +762,8 @@ private: const context::Context * const d_satContext; const int d_satAllocationLevel; + NodeCallBack& d_raiseConflict; + friend class ConstraintValue; public: @@ -769,12 +771,13 @@ public: ConstraintDatabase( context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, - ArithCongruenceManager& dm); + ArithCongruenceManager& dm, + NodeCallBack& conflictCallBack); ~ConstraintDatabase(); + /** Adds a literal to the database. */ Constraint addLiteral(TNode lit); - //Constraint addAtom(TNode atom); /** * If hasLiteral() is true, returns the constraint. @@ -852,6 +855,8 @@ public: void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB); private: + void raiseUnateConflict(Constraint ant, Constraint cons); + class Statistics { public: IntStat d_unatePropagateCalls; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index be24e43ba..faf0e3563 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -61,6 +61,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), d_diseqQueue(c, false), + d_currentPropagationList(), + d_learnedBounds(c), d_partialModel(c), d_tableau(), d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack), @@ -71,10 +73,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_conflicts(c), - d_conflictCallBack(d_conflicts), - d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap), - d_simplex(d_linEq, d_conflictCallBack), - d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager), + d_raiseConflict(d_conflicts), + d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict), + d_simplex(d_linEq, d_raiseConflict), + d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict), d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() @@ -181,7 +183,7 @@ void TheoryArith::zeroDifferenceDetected(ArithVar x){ } /* procedure AssertLower( x_i >= c_i ) */ -Node TheoryArith::AssertLower(Constraint constraint){ +bool TheoryArith::AssertLower(Constraint constraint){ Assert(constraint != NullConstraint); Assert(constraint->isLowerBound()); @@ -194,7 +196,7 @@ Node TheoryArith::AssertLower(Constraint constraint){ //TODO Relax to less than? if(d_partialModel.lessThanLowerBound(x_i, c_i)){ - return Node::null(); + return false; //sat } int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i); @@ -203,7 +205,8 @@ Node TheoryArith::AssertLower(Constraint constraint){ Node conflict = ConstraintValue::explainConflict(ubc, constraint); Debug("arith") << "AssertLower conflict " << conflict << endl; ++(d_statistics.d_statAssertLowerConflicts); - return conflict; + d_raiseConflict(conflict); + return true; }else if(cmpToUB == 0){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); @@ -229,10 +232,33 @@ Node TheoryArith::AssertLower(Constraint constraint){ ++(d_statistics.d_statDisequalityConflicts); Debug("eq") << " assert lower conflict " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; }else if(!eq->isTrue()){ Debug("eq") << "lb == ub, propagate eq" << eq << endl; eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i)); + // do not need to add to d_learnedBounds + } + } + }else{ + Assert(cmpToUB < 0); + const ValueCollection& vc = constraint->getValueCollection(); + if(vc.hasDisequality() && vc.hasUpperBound()){ + const Constraint diseq = vc.getDisequality(); + if(diseq->isTrue()){ + const Constraint ub = vc.getUpperBound(); + if(ub->hasProof()){ + Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint); + Debug("eq") << " assert upper conflict " << conflict << endl; + d_raiseConflict(conflict); + return true; + }else if(!ub->negationHasProof()){ + Constraint negUb = ub->getNegation(); + negUb->impliedBy(constraint, diseq); + //if(!negUb->canBePropagated()){ + d_learnedBounds.push_back(negUb); + //}//otherwise let this be propagated/asserted later + } } } } @@ -263,11 +289,11 @@ Node TheoryArith::AssertLower(Constraint constraint){ if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - return Node::null(); + return false; //sat } /* procedure AssertUpper( x_i <= c_i) */ -Node TheoryArith::AssertUpper(Constraint constraint){ +bool TheoryArith::AssertUpper(Constraint constraint){ ArithVar x_i = constraint->getVariable(); const DeltaRational& c_i = constraint->getValue(); @@ -283,7 +309,7 @@ Node TheoryArith::AssertUpper(Constraint constraint){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i - return Node::null(); //sat + return false; //sat } // cmpToLb = \lowerbound(x_i).cmp(c_i) @@ -293,7 +319,8 @@ Node TheoryArith::AssertUpper(Constraint constraint){ Node conflict = ConstraintValue::explainConflict(lbc, constraint); Debug("arith") << "AssertUpper conflict " << conflict << endl; ++(d_statistics.d_statAssertUpperConflicts); - return conflict; + d_raiseConflict(conflict); + return true; }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); @@ -315,13 +342,34 @@ Node TheoryArith::AssertUpper(Constraint constraint){ if(diseq->isTrue()){ Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint); Debug("eq") << " assert upper conflict " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; }else if(!eq->isTrue()){ Debug("eq") << "lb == ub, propagate eq" << eq << endl; eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i)); + //do not bother to add to d_learnedBounds + } + } + }else if(cmpToLB > 0){ + const ValueCollection& vc = constraint->getValueCollection(); + if(vc.hasDisequality() && vc.hasLowerBound()){ + const Constraint diseq = vc.getDisequality(); + if(diseq->isTrue()){ + const Constraint lb = vc.getLowerBound(); + if(lb->hasProof()){ + Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint); + Debug("eq") << " assert upper conflict " << conflict << endl; + d_raiseConflict(conflict); + return true; + }else if(!lb->negationHasProof()){ + Constraint negLb = lb->getNegation(); + negLb->impliedBy(constraint, diseq); + //if(!negLb->canBePropagated()){ + d_learnedBounds.push_back(negLb); + //}//otherwise let this be propagated/asserted later + } } } - } d_currentPropagationList.push_back(constraint); @@ -351,12 +399,12 @@ Node TheoryArith::AssertUpper(Constraint constraint){ if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - return Node::null(); + return false; //sat } /* procedure AssertEquality( x_i == c_i ) */ -Node TheoryArith::AssertEquality(Constraint constraint){ +bool TheoryArith::AssertEquality(Constraint constraint){ AssertArgument(constraint != NullConstraint, "AssertUpper() called on a NullConstraint."); @@ -374,21 +422,23 @@ Node TheoryArith::AssertEquality(Constraint constraint){ // u_i <= c_i <= l_i // This can happen if both c_i <= x_i and x_i <= c_i are in the system. if(cmpToUB >= 0 && cmpToLB <= 0){ - return Node::null(); //sat + return false; //sat } if(cmpToUB > 0){ Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i); Node conflict = ConstraintValue::explainConflict(ubc, constraint); Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; } if(cmpToLB < 0){ Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i); Node conflict = ConstraintValue::explainConflict(lbc, constraint); Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return true; } Assert(cmpToUB <= 0); @@ -431,12 +481,12 @@ Node TheoryArith::AssertEquality(Constraint constraint){ }else{ d_simplex.updateBasic(x_i); } - return Node::null(); + return false; } /* procedure AssertDisequality( x_i != c_i ) */ -Node TheoryArith::AssertDisequality(Constraint constraint){ +bool TheoryArith::AssertDisequality(Constraint constraint){ AssertArgument(constraint != NullConstraint, "AssertUpper() called on a NullConstraint."); @@ -457,7 +507,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ if(constraint->isSplit()){ Debug("eq") << "skipping already split " << constraint << endl; - return Node::null(); + return false; } const ValueCollection& vc = constraint->getValueCollection(); @@ -468,18 +518,25 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ //in conflict Debug("eq") << "explaining" << endl; ++(d_statistics.d_statDisequalityConflicts); - return ConstraintValue::explainConflict(constraint, lb, ub); + Node conflict = ConstraintValue::explainConflict(constraint, lb, ub); + d_raiseConflict(conflict); + return true; + }else if(lb->isTrue()){ Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl; const Constraint negUb = ub->getNegation(); if(!negUb->isTrue()){ negUb->impliedBy(constraint, lb); + d_learnedBounds.push_back(negUb); } }else if(ub->isTrue()){ Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl; const Constraint negLb = lb->getNegation(); if(!negLb->isTrue()){ negLb->impliedBy(constraint, ub); + //if(!negLb->canBePropagated()){ + d_learnedBounds.push_back(negLb); + //} } } } @@ -488,7 +545,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ if(c_i == d_partialModel.getAssignment(x_i)){ Debug("eq") << "lemma now! " << constraint << endl; d_out->lemma(constraint->split()); - return Node::null(); + return false; }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ Debug("eq") << "can drop as less than lb" << constraint << endl; }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){ @@ -497,7 +554,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){ Debug("eq") << "push back" << constraint << endl; d_diseqQueue.push(constraint); } - return Node::null(); + return false; } @@ -1006,23 +1063,48 @@ Node TheoryArith::callDioSolver(){ return d_diosolver.processEquationsForConflict(); } -Node TheoryArith::assertionCases(TNode assertion){ - Constraint constraint = d_constraintDatabase.lookup(assertion); +Constraint TheoryArith::constraintFromFactQueue(){ + Assert(!done()); + TNode assertion = get(); Kind simpleKind = Comparison::comparisonKind(assertion); - Assert(simpleKind != UNDEFINED_KIND); - Assert(constraint != NullConstraint || - simpleKind == EQUAL || - simpleKind == DISTINCT ); - if(simpleKind == EQUAL || simpleKind == DISTINCT){ + Constraint constraint = d_constraintDatabase.lookup(assertion); + if(constraint == NullConstraint){ + Assert(simpleKind == EQUAL || simpleKind == DISTINCT ); + bool isDistinct = 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(!isSetup(eq)); + Node reEq = Rewriter::rewrite(eq); + if(reEq.getKind() == CONST_BOOLEAN){ + if(reEq.getConst<bool>() != isDistinct){ + Assert((reEq.getConst<bool>() && isDistinct) || + (!reEq.getConst<bool>() && !isDistinct)); + d_raiseConflict(assertion); + } + return NullConstraint; } - } + Assert(reEq.getKind() != CONST_BOOLEAN); + if(!isSetup(reEq)){ + setupAtom(reEq); + } + Node reAssertion = isDistinct ? reEq.notNode() : reEq; + constraint = d_constraintDatabase.lookup(reAssertion); + } + + // 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()){ @@ -1031,8 +1113,6 @@ Node TheoryArith::assertionCases(TNode assertion){ 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; @@ -1042,94 +1122,202 @@ Node TheoryArith::assertionCases(TNode assertion){ negation->explainForConflict(nb); Node conflict = nb; Debug("arith::eq") << "conflict" << conflict << endl; - return conflict; + d_raiseConflict(conflict); + return NullConstraint; } 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; - + return NullConstraint; + }else{ + Debug("arith::constraint") << "arith constraint " << constraint << std::endl; + constraint->setAssertedToTheTheory(); - 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; + } - 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; + return constraint; } +} + +bool TheoryArith::assertionCases(Constraint constraint){ + Assert(constraint->hasProof()); + Assert(!constraint->negationHasProof()); - Assert(!isInteger(x_i) || - simpleKind == EQUAL || - simpleKind == DISTINCT || - simpleKind == GEQ || - simpleKind == LT); + ArithVar x_i = constraint->getVariable(); switch(constraint->getType()){ case UpperBound: - if(simpleKind == LT && isInteger(x_i)){ + if(isInteger(x_i) && constraint->isStrictUpperBound()){ Constraint floorConstraint = constraint->getFloor(); if(!floorConstraint->isTrue()){ if(floorConstraint->negationHasProof()){ - return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation()); + Node conf = ConstraintValue::explainConflict(constraint, floorConstraint->getNegation()); + d_raiseConflict(conf); + return true; }else{ floorConstraint->impliedBy(constraint); + // Do not need to add to d_learnedBounds } } - //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)){ + if(isInteger(x_i) && constraint->isStrictLowerBound()){ Constraint ceilingConstraint = constraint->getCeiling(); if(!ceilingConstraint->isTrue()){ if(ceilingConstraint->negationHasProof()){ - - return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation()); + Node conf = ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation()); + d_raiseConflict(conf); + return true; } ceilingConstraint->impliedBy(constraint); + // Do not need to add to learnedBounds } - //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(); + 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. @@ -1154,6 +1342,15 @@ bool TheoryArith::hasIntegerModel(){ return true; } +/** Outputs conflicts to the output channel. */ +void TheoryArith::outputConflicts(){ + Assert(!d_conflicts.empty()); + for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ + Node conflict = d_conflicts[i]; + Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl; + d_out->conflict(conflict); + } +} void TheoryArith::check(Effort effortLevel){ Assert(d_currentPropagationList.empty()); @@ -1161,22 +1358,29 @@ void TheoryArith::check(Effort effortLevel){ d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done(); while(!done()){ - - Node assertion = get(); - Node possibleConflict = assertionCases(assertion); - - if(!possibleConflict.isNull()){ + Constraint curr = constraintFromFactQueue(); + if(curr != NullConstraint){ + bool res = assertionCases(curr); + Assert(!res || inConflict()); + } + if(inConflict()){ revertOutOfConflict(); - - Debug("arith::conflict") << "conflict " << possibleConflict << endl; - d_out->conflict(possibleConflict); + outputConflicts(); return; } - if(d_congruenceManager.inConflict()){ - Node c = d_congruenceManager.conflict(); + } + 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()){ revertOutOfConflict(); - Debug("arith::conflict") << "difference manager conflict " << c << endl; - d_out->conflict(c); + outputConflicts(); return; } } @@ -1191,13 +1395,7 @@ void TheoryArith::check(Effort effortLevel){ bool foundConflict = d_simplex.findModel(); if(foundConflict){ revertOutOfConflict(); - - Assert(!d_conflicts.empty()); - for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ - Node conflict = d_conflicts[i]; - Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl; - d_out->conflict(conflict); - } + outputConflicts(); emmittedConflictOrSplit = true; }else{ d_partialModel.commitAssignmentChanges(); @@ -1208,7 +1406,7 @@ void TheoryArith::check(Effort effortLevel){ Options::current()->arithPropagationMode == Options::BOTH_PROP)){ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); - while(!d_currentPropagationList.empty()){ + while(!d_currentPropagationList.empty() && !inConflict()){ Constraint curr = d_currentPropagationList.front(); d_currentPropagationList.pop_front(); @@ -1244,6 +1442,13 @@ void TheoryArith::check(Effort effortLevel){ Unhandled(curr->getType()); } } + + if(inConflict()){ + Debug("arith::unate") << "unate conflict" << endl; + revertOutOfConflict(); + outputConflicts(); + return; + } }else{ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); d_currentPropagationList.clear(); @@ -1800,25 +2005,10 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic)); d_linEq.propagateNonbasicsLowerBound(basic, bestImplied); } + // I think this can be skipped if canBePropagated is true + //d_learnedBounds.push(bestImplied); return true; } - - // bool asserted = valuationIsAsserted(bestImplied); - // bool propagated = d_theRealPropManager.isPropagated(bestImplied); - // if( !asserted && !propagated){ - - // NodeBuilder<> nb(kind::AND); - // if(upperBound){ - // d_linEq.explainNonbasicsUpperBound(basic, nb); - // }else{ - // d_linEq.explainNonbasicsLowerBound(basic, nb); - // } - // Node explanation = nb; - // d_theRealPropManager.propagate(bestImplied, explanation, false); - // return true; - // }else{ - // Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; - // } } } return false; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1f0120387..e23a9a943 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -184,6 +184,8 @@ private: */ std::deque<Constraint> d_currentPropagationList; + context::CDQueue<Constraint> d_learnedBounds; + /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -245,8 +247,17 @@ private: void operator()(Node n){ d_list.push_back(n); } - }; - PushCallBack d_conflictCallBack; + } d_raiseConflict; + + /** Returns true iff a conflict has been raised. */ + inline bool inConflict() const { + return !d_conflicts.empty(); + } + /** + * Outputs the contents of d_conflicts onto d_out. + * Must be inConflict(). + */ + void outputConflicts(); /** @@ -386,10 +397,10 @@ private: * a node describing this conflict is returned. * If this new bound is not in conflict, Node::null() is returned. */ - Node AssertLower(Constraint constraint); - Node AssertUpper(Constraint constraint); - Node AssertEquality(Constraint constraint); - Node AssertDisequality(Constraint constraint); + bool AssertLower(Constraint constraint); + bool AssertUpper(Constraint constraint); + bool AssertEquality(Constraint constraint); + bool AssertDisequality(Constraint constraint); /** Tracks the bounds that were updated in the current round. */ DenseSet d_updatedBounds; @@ -423,7 +434,8 @@ private: * Returns a conflict if one was found. * Returns Node::null if no conflict was found. */ - Node assertionCases(TNode assertion); + Constraint constraintFromFactQueue(); + bool assertionCases(Constraint c); /** * Returns the basic variable with the shorted row containg a non-basic variable. |