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);