diff options
Diffstat (limited to 'src/theory/arith/constraint.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 64 |
1 files changed, 54 insertions, 10 deletions
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); |