Missing ids for arith conflicts (#8108)

Fixes #8097.

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 806079f62775e85f448db9278bc0d42ec7c1a8e3..fcb6740f194e6943071decc84e95e3f007f84def 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -2263,7 +2263,7 @@ bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
   if(cons->negationHasProof()){
     Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
     cons->impliedByUnate(ant, true);
-    d_raiseConflict.raiseConflict(cons, InferenceId::UNKNOWN);
+    d_raiseConflict.raiseConflict(cons, InferenceId::ARITH_CONF_UNATE_PROP);
     return true;
   }else if(!cons->isTrue()){
     ++d_statistics.d_unatePropagateImplications;

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a4864c4e43575b16511abc552c4665a1a82c6d18..c540aa384955f6bda7b151af5bb7704a7aa78db1 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -378,6 +378,8 @@ bool TheoryArithPrivate::isProofEnabled() const
 
 void TheoryArithPrivate::raiseConflict(ConstraintCP a, InferenceId id){
   Assert(a->inConflict());
+  Assert(id != InferenceId::UNKNOWN)
+      << "Must provide an inference id in TheoryArithPrivate::raiseConflict";
   d_conflicts.push_back(std::make_pair(a, id));
 }
 
@@ -411,21 +413,6 @@ void TheoryArithPrivate::clearUpdates(){
   d_updatedBounds.purge();
 }
 
-// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
-//   ConstraintCPVec v;
-//   v.push_back(a);
-//   v.push_back(b);
-//   d_conflicts.push_back(v);
-// }
-
-// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
-//   ConstraintCPVec v;
-//   v.push_back(a);
-//   v.push_back(b);
-//   v.push_back(c);
-//   d_conflicts.push_back(v);
-// }
-
 void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x){
   if(d_cmEnabled){
     Assert(d_congruenceManager.isWatchedVariable(x));
@@ -1751,8 +1738,9 @@ void TheoryArithPrivate::outputConflicts(){
       Node conflict = trustedConflict.getNode();
 
       ++conflicts;
-      Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
-                               << " has proof: " << hasProof << endl;
+      Debug("arith::conflict")
+          << "d_conflicts[" << i << "] " << conflict
+          << " has proof: " << hasProof << ", id = " << conf.second << endl;
       if(Debug.isOn("arith::normalize::external")){
         conflict = flattenAndSort(conflict);
         Debug("arith::conflict") << "(normalized to) " << conflict << endl;
@@ -1916,7 +1904,7 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
                                      << "  (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
                                      << "  (" << at_j->isTrue() <<") " << at_j << endl;
           neg_at_j->impliedByIntHole(vec, true);
-          raiseConflict(at_j, InferenceId::UNKNOWN);
+          raiseConflict(at_j, InferenceId::ARITH_CONF_REPLAY_LOG);
           break;
         }
       }
@@ -2180,7 +2168,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
     if(!contains(conf, bcneg)){
       Debug("approx::branch") << "reraise " << conf  << endl;
       ConstraintCP conflicting = vectorToIntHoleConflict(conf);
-      raiseConflict(conflicting, InferenceId::UNKNOWN);
+      raiseConflict(conflicting, InferenceId::ARITH_CONF_BRANCH_CUT);
     }else if(!bci.proven()){
       drop(conf, bcneg);
       bci.setExplanation(conf);
@@ -2200,7 +2188,7 @@ void TheoryArithPrivate::replayAssert(ConstraintP c) {
     }
     Debug("approx::replayAssert") << "replayAssertion " << c << endl;
     if(inConflict){
-      raiseConflict(c, InferenceId::UNKNOWN);
+      raiseConflict(c, InferenceId::ARITH_CONF_REPLAY_ASSERT);
     }else{
       assertionCases(c);
     }
@@ -2349,7 +2337,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
             }else {
               con->impliedByIntHole(exp, true);
               Debug("approx::replayLogRec") << "cut into conflict " << con << endl;
-              raiseConflict(con, InferenceId::UNKNOWN);
+              raiseConflict(con, InferenceId::ARITH_CONF_REPLAY_LOG_REC);
             }
           }else{
             ++d_statistics.d_cutsProofFailed;

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index e1a5260e33c13d3cb5b2b46c716aa8809e96e4fc..745f6d35b082448c1e039f8c62cb1c143bed61d1 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -39,6 +39,13 @@ const char* toString(InferenceId i)
     case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX";
     case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX";
     case InferenceId::ARITH_CONF_FACT_QUEUE: return "ARITH_CONF_FACT_QUEUE";
+    case InferenceId::ARITH_CONF_BRANCH_CUT: return "ARITH_CONF_BRANCH_CUT";
+    case InferenceId::ARITH_CONF_REPLAY_ASSERT:
+      return "ARITH_CONF_REPLAY_ASSERT";
+    case InferenceId::ARITH_CONF_REPLAY_LOG: return "ARITH_CONF_REPLAY_LOG";
+    case InferenceId::ARITH_CONF_REPLAY_LOG_REC:
+      return "ARITH_CONF_REPLAY_LOG_REC";
+    case InferenceId::ARITH_CONF_UNATE_PROP: return "ARITH_CONF_UNATE_PROP";
     case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ";
     case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL";
     case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR";

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 19dd1d3eac9710b77237d0340fbdb346f8e828e3..ef63c224cdff63e0af186a11c1e92f8ad4392ed1 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -66,6 +66,16 @@ enum class InferenceId
   ARITH_CONF_SOI_SIMPLEX,
   // conflict when getting constraint from fact queue
   ARITH_CONF_FACT_QUEUE,
+  // conflict in tryBranchCut
+  ARITH_CONF_BRANCH_CUT,
+  // conflict in replayAssert
+  ARITH_CONF_REPLAY_ASSERT,
+  // conflict in replayLog
+  ARITH_CONF_REPLAY_LOG,
+  // conflict in replayLogRec
+  ARITH_CONF_REPLAY_LOG_REC,
+  // conflict from handleUnateProp
+  ARITH_CONF_UNATE_PROP,
   // introduces split on a disequality
   ARITH_SPLIT_DEQ,
   // tighten integer inequalities to ceiling

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3cdb878dfc80206244825409ac2bea523fe7c511..48f26f9d20c7b4692a23cd274221ef66c69e3e32 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -65,6 +65,7 @@ set(regress_0_tests
   regress0/arith/issue5219-conflict-rewrite.smt2
   regress0/arith/issue5761-ppr.smt2
   regress0/arith/issue7984-quant-trans.smt2
+  regress0/arith/issue8097-iid.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc.smt2

diff --git a/test/regress/regress0/arith/issue8097-iid.smt2 b/test/regress/regress0/arith/issue8097-iid.smt2
new file mode 100644 (file)
index 0000000..1db1e5e
--- /dev/null
+++ b/test/regress/regress0/arith/issue8097-iid.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun g () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(assert (and (>= f 0) (>= b 0) (> g 0) (= 1 (* e b)) (= 0 (* c b)) (> 0 (div (* f b) 0)) (> (* f (div (* g b) c)) 0)))
+(check-sat)