From: Gereon Kremer Date: Thu, 3 Mar 2022 00:37:05 +0000 (+0100) Subject: Fix rewriting of mixed-integer atoms (#8214) X-Git-Tag: cvc5-1.0.0~337 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91eb86f4f64e29865661bc2edc4fb86317808d16;p=cvc5.git Fix rewriting of mixed-integer atoms (#8214) The sixth input from #8159 revealed a subtle issue in our rewriting of arithmetic atoms. As real and integer atoms are rewritten differently, we check this and then call different functions. However, we check this on the original input, although this property can change during rewriting, e.g., when the only real variable vanishes. This PR fixes this issue. --- diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 91652b7ce..8d634c77a 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -118,6 +118,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom) RewriteResponse ArithRewriter::postRewriteAtom(TNode atom) { Assert(rewriter::isAtom(atom)); + Trace("arith-rewriter") << "postRewriteAtom: " << atom << std::endl; if (atom.getKind() == kind::IS_INTEGER) { @@ -181,8 +182,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom) rewriter::addToSum(sum, left, negate); rewriter::addToSum(sum, right, !negate); - // Now we have (rsum 0) - if (rewriter::isIntegral(atom)) + // Now we have (sum 0) + if (rewriter::isIntegral(sum)) { if (kind == Kind::EQUAL) { diff --git a/src/theory/arith/rewriter/addition.cpp b/src/theory/arith/rewriter/addition.cpp index e8743a43a..dca343e82 100644 --- a/src/theory/arith/rewriter/addition.cpp +++ b/src/theory/arith/rewriter/addition.cpp @@ -139,6 +139,35 @@ Node collectSumWithBase(const Sum& sum, } } +bool isIntegral(const Sum& sum) +{ + std::vector queue; + for (const auto& s: sum) + { + queue.emplace_back(s.first); + } + while (!queue.empty()) + { + TNode cur = queue.back(); + queue.pop_back(); + + if (cur.isConst()) continue; + switch (cur.getKind()) + { + case Kind::ADD: + case Kind::NEG: + case Kind::SUB: + case Kind::MULT: + case Kind::NONLINEAR_MULT: + queue.insert(queue.end(), cur.begin(), cur.end()); + break; + default: + if (!cur.getType().isInteger()) return false; + } + } + return true; +} + void addToSum(Sum& sum, TNode n, bool negate) { if (n.getKind() == Kind::ADD) diff --git a/src/theory/arith/rewriter/addition.h b/src/theory/arith/rewriter/addition.h index fd25a79d3..fa2a75067 100644 --- a/src/theory/arith/rewriter/addition.h +++ b/src/theory/arith/rewriter/addition.h @@ -53,6 +53,14 @@ using Sum = std::map; */ std::ostream& operator<<(std::ostream& os, const Sum& sum); +/** + * Check whether the given sum can be rewritten as an integer expression. This + * differs from checking the node type in a major way: rational + * constants are always integral, as they are rewritten to integers by simple + * multiplication with their denominator. + */ +bool isIntegral(const Sum& sum); + /** * Add the arithmetic term `n` to the given sum. If negate is true, actually add * `-n`. If `n` is itself a sum, it automatically flattens it into `sum` (though diff --git a/src/theory/arith/rewriter/node_utils.cpp b/src/theory/arith/rewriter/node_utils.cpp index 3d1856e0b..69522b237 100644 --- a/src/theory/arith/rewriter/node_utils.cpp +++ b/src/theory/arith/rewriter/node_utils.cpp @@ -23,39 +23,6 @@ namespace theory { namespace arith { namespace rewriter { -bool isIntegral(TNode n) -{ - std::vector queue = {n}; - while (!queue.empty()) - { - TNode cur = queue.back(); - queue.pop_back(); - - if (cur.isConst()) continue; - switch (cur.getKind()) - { - case Kind::LT: - case Kind::LEQ: - case Kind::EQUAL: - case Kind::DISTINCT: - case Kind::GEQ: - case Kind::GT: - queue.emplace_back(n[0]); - queue.emplace_back(n[1]); - break; - case Kind::ADD: - case Kind::NEG: - case Kind::SUB: - case Kind::MULT: - queue.insert(queue.end(), cur.begin(), cur.end()); - break; - default: - if (!cur.getType().isInteger()) return false; - } - } - return true; -} - Node mkMultTerm(const Rational& multiplicity, TNode monomial) { if (monomial.isConst()) diff --git a/src/theory/arith/rewriter/node_utils.h b/src/theory/arith/rewriter/node_utils.h index f8e030386..a6d311b3d 100644 --- a/src/theory/arith/rewriter/node_utils.h +++ b/src/theory/arith/rewriter/node_utils.h @@ -51,15 +51,6 @@ inline bool isAtom(TNode n) } } -/** - * Check whether the given node can be rewritten to an integer node. This - * differs from checking the node type in two major ways: we consider relational - * operators integral if both children are integral in this sense; rational - * constants are always integral, as they are rewritten to integers by simple - * multiplication with their denominator. - */ -bool isIntegral(TNode n); - /** Check whether the node wraps a real algebraic number. */ inline bool isRAN(TNode n) { diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp index e627186f2..5163a145d 100644 --- a/src/theory/arith/rewriter/rewrite_atom.cpp +++ b/src/theory/arith/rewriter/rewrite_atom.cpp @@ -259,6 +259,7 @@ Node buildRelation(Kind kind, Node left, Node right, bool negate) Node buildIntegerEquality(Sum&& sum) { + Trace("arith-rewriter") << "building integer inequality from " << sum << std::endl; normalizeGCDLCM(sum); const auto& constant = *sum.begin(); @@ -289,6 +290,7 @@ Node buildIntegerEquality(Sum&& sum) Node buildRealEquality(Sum&& sum) { + Trace("arith-rewriter") << "building real equality from " << sum << std::endl; auto lterm = removeLTerm(sum); if (isZero(lterm.second)) { @@ -304,6 +306,7 @@ Node buildRealEquality(Sum&& sum) Node buildIntegerInequality(Sum&& sum, Kind k) { + Trace("arith-rewriter") << "building integer equality from " << sum << std::endl; bool negate = normalizeGCDLCM(sum, true); if (negate) @@ -329,6 +332,7 @@ Node buildIntegerInequality(Sum&& sum, Kind k) Node buildRealInequality(Sum&& sum, Kind k) { + Trace("arith-rewriter") << "building real inequality from " << sum << std::endl; normalizeLCoeffAbsOne(sum); Node rhs = mkConst(-removeConstant(sum)); return buildRelation(k, collectSum(sum), rhs); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 67be26f52..807abb4c2 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/issue8097-iid.smt2 + regress0/arith/issue8159-rewrite-intreal.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc.smt2 diff --git a/test/regress/regress0/arith/issue8159-rewrite-intreal.smt2 b/test/regress/regress0/arith/issue8159-rewrite-intreal.smt2 new file mode 100644 index 000000000..a15191115 --- /dev/null +++ b/test/regress/regress0/arith/issue8159-rewrite-intreal.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic QF_LIRA) +(declare-fun a () Real) +(declare-fun b () Int) +(assert (>= a (+ a b))) +(check-sat)