diff options
| -rw-r--r-- | src/theory/arith/bound_inference.cpp | 3 | ||||
| -rw-r--r-- | src/theory/arith/inference_id.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/inference_manager.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/nl/icp/icp_solver.cpp | 12 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 | 8 |
6 files changed, 20 insertions, 8 deletions
diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 5a1c30966..7cae40bbb 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -15,6 +15,7 @@ #include "theory/arith/bound_inference.h" #include "theory/arith/normal_form.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { @@ -95,7 +96,7 @@ const std::map<Node, Bounds>& BoundInference::get() const { return d_bounds; } bool BoundInference::add(const Node& n) { // Parse the node as a comparison - auto comp = Comparison::parseNormalForm(n); + auto comp = Comparison::parseNormalForm(Rewriter::rewrite(n)); auto dec = comp.decompose(true); if (std::get<0>(dec).isVariable()) { diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp index d984e09f2..a0dc19d81 100644 --- a/src/theory/arith/inference_id.cpp +++ b/src/theory/arith/inference_id.cpp @@ -42,6 +42,8 @@ const char* toString(InferenceId i) case InferenceId::NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; case InferenceId::NL_CAD_CONFLICT: return "CAD_CONFLICT"; case InferenceId::NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; + case InferenceId::NL_ICP_CONFLICT: return "ICP_CONFLICT"; + case InferenceId::NL_ICP_PROPAGATION: return "ICP_PROPAGATION"; default: return "?"; } } diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 77f042d4d..656b5ed0d 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -95,7 +95,7 @@ void InferenceManager::addConflict(const Node& conf, InferenceId inftype) { Trace("arith::infman") << "Adding conflict: " << inftype << " " << conf << std::endl; - conflict(Rewriter::rewrite(conf)); + conflict(conf); } bool InferenceManager::hasUsed() const diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 43905d802..7f97d51b6 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -77,7 +77,8 @@ std::vector<Node> ICPSolver::collectVariables(const Node& n) const std::vector<Candidate> ICPSolver::constructCandidates(const Node& n) { - auto comp = Comparison::parseNormalForm(n).decompose(false); + auto comp = + Comparison::parseNormalForm(Rewriter::rewrite(n)).decompose(false); Kind k = std::get<1>(comp); if (k == Kind::DISTINCT) { @@ -305,13 +306,12 @@ void ICPSolver::reset(const std::vector<Node>& assertions) d_state.reset(); for (const auto& n : assertions) { - Node tmp = Rewriter::rewrite(n); - Trace("nl-icp") << "Adding " << tmp << std::endl; - if (tmp.getKind() != Kind::CONST_BOOLEAN) + Trace("nl-icp") << "Adding " << n << std::endl; + if (n.getKind() != Kind::CONST_BOOLEAN) { - if (!d_state.d_bounds.add(tmp)) + if (!d_state.d_bounds.add(n)) { - addCandidate(tmp); + addCandidate(n); } } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5d4501309..cc5c911ff 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -49,6 +49,7 @@ set(regress_0_tests regress0/arith/issue3683.smt2 regress0/arith/issue4367.smt2 regress0/arith/issue4525.smt2 + regress0/arith/issue5219-conflict-rewrite.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc diff --git a/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 new file mode 100644 index 000000000..3c8a949ad --- /dev/null +++ b/test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 @@ -0,0 +1,8 @@ +; REQUIRES: poly +; COMMAND-LINE: --theoryof-mode=term --nl-ext --nl-icp +; EXPECT: unknown +(set-logic QF_NRA) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (and (< 1 y) (= y (+ x (* x x))))) +(check-sat) |