diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-07 16:13:41 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-07 09:13:41 -0500 |
| commit | eb4321c5040258ac1ac41eb955aa5b6b5199011e (patch) | |
| tree | 01524ae48f79b8aa0ab60728e29e3a4b80e92e8f /src/theory/arith/nl | |
| parent | 1a97c19443833604d57f1453a1bebfe0714d3d8e (diff) | |
Make sure conflicts are not rewritten (in arithmetic) (#5219)
The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.
Diffstat (limited to 'src/theory/arith/nl')
| -rw-r--r-- | src/theory/arith/nl/icp/icp_solver.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
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); } } } |