From 811e5c602c1445a4a64aa8a90d9b52a769611ebe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Feb 2022 15:11:10 -0600 Subject: [PATCH] Missing ids for arith conflicts (#8108) Fixes #8097. --- src/theory/arith/constraint.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 30 ++++++------------- src/theory/inference_id.cpp | 7 +++++ src/theory/inference_id.h | 10 +++++++ test/regress/CMakeLists.txt | 1 + .../regress/regress0/arith/issue8097-iid.smt2 | 11 +++++++ 6 files changed, 39 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress0/arith/issue8097-iid.smt2 diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 806079f62..fcb6740f1 100644 --- 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 a4864c4e4..c540aa384 100644 --- 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 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 e1a5260e3..745f6d35b 100644 --- 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 19dd1d3ea..ef63c224c 100644 --- 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 3cdb878df..48f26f9d2 100644 --- 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 index 000000000..1db1e5e9c --- /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) -- 2.30.2