From: Gereon Kremer Date: Tue, 20 Oct 2020 15:01:30 +0000 (+0200) Subject: Handle rewrite to bool in BoundInference (#5311) X-Git-Tag: cvc5-1.0.0~2687 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e714e365dbbd51bbf04305867c4bcdc3d5a4d83;p=cvc5.git Handle rewrite to bool in BoundInference (#5311) The BoundInference class did not properly handle rewrites that yield constant Booleans. This PR fixes this issue by explicitly checking for this case. --- diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 7cae40bbb..92e71bf14 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -95,8 +95,13 @@ Bounds BoundInference::get(const Node& v) const const std::map& BoundInference::get() const { return d_bounds; } bool BoundInference::add(const Node& n) { + Node tmp = Rewriter::rewrite(n); + if (tmp.getKind() == Kind::CONST_BOOLEAN) + { + return false; + } // Parse the node as a comparison - auto comp = Comparison::parseNormalForm(Rewriter::rewrite(n)); + auto comp = Comparison::parseNormalForm(tmp); auto dec = comp.decompose(true); if (std::get<0>(dec).isVariable()) { diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 7f97d51b6..4ec33c360 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -77,8 +77,12 @@ std::vector ICPSolver::collectVariables(const Node& n) const std::vector ICPSolver::constructCandidates(const Node& n) { - auto comp = - Comparison::parseNormalForm(Rewriter::rewrite(n)).decompose(false); + Node tmp = Rewriter::rewrite(n); + if (tmp.isConst()) + { + return {}; + } + auto comp = Comparison::parseNormalForm(tmp).decompose(false); Kind k = std::get<1>(comp); if (k == Kind::DISTINCT) {