From 0e2f84754dd44baa14206780b93f84dd5002a509 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 May 2022 16:58:14 -0500 Subject: [PATCH] Make arith msum utility agnostic to Int (#8694) This utility should continue to assume arithmetic subtypes. Fixes #8691. --- src/theory/arith/arith_msum.cpp | 13 ++++++------- src/theory/arith/arith_msum.h | 10 +++++++--- src/theory/arith/arith_rewriter.cpp | 2 +- test/regress/cli/CMakeLists.txt | 2 ++ .../cli/regress0/nl/issue8691-3-msum-subtypes.smt2 | 5 +++++ .../cli/regress0/nl/issue8691-msum-subtypes.smt2 | 8 ++++++++ 6 files changed, 29 insertions(+), 11 deletions(-) create mode 100644 test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 create mode 100644 test/regress/cli/regress0/nl/issue8691-msum-subtypes.smt2 diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 12d7a8360..f96374127 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -97,7 +97,6 @@ bool ArithMSum::getMonomialSumLit(Node lit, std::map& msum) NodeManager* nm = NodeManager::currentNM(); if (getMonomialSum(lit[1], msum2)) { - TypeNode tn = lit[0].getType(); for (std::map::iterator it = msum2.begin(); it != msum2.end(); ++it) @@ -111,14 +110,14 @@ bool ArithMSum::getMonomialSumLit(Node lit, std::map& msum) Rational r2 = it->second.isNull() ? Rational(1) : it->second.getConst(); - msum[it->first] = nm->mkConstRealOrInt(tn, r1 - r2); + msum[it->first] = nm->mkConstRealOrInt(r1 - r2); } else { msum[it->first] = it->second.isNull() - ? nm->mkConstRealOrInt(tn, Rational(-1)) + ? nm->mkConstInt(Rational(-1)) : nm->mkConstRealOrInt( - tn, -it->second.getConst()); + -it->second.getConst()); } } return true; @@ -129,7 +128,7 @@ bool ArithMSum::getMonomialSumLit(Node lit, std::map& msum) return false; } -Node ArithMSum::mkNode(TypeNode tn, const std::map& msum) +Node ArithMSum::mkNode(const std::map& msum) { NodeManager* nm = NodeManager::currentNM(); std::vector children; @@ -151,7 +150,7 @@ Node ArithMSum::mkNode(TypeNode tn, const std::map& msum) return children.size() > 1 ? nm->mkNode(ADD, children) : (children.size() == 1 ? children[0] - : nm->mkConstRealOrInt(tn, Rational(0))); + : nm->mkConstInt(Rational(0))); } int ArithMSum::isolate( @@ -286,7 +285,7 @@ bool ArithMSum::decompose(Node n, Node v, Node& coeff, Node& rem) { coeff = it->second; msum.erase(v); - rem = mkNode(n.getType(), msum); + rem = mkNode(msum); return true; } } diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index 989f9bc3e..237395b3a 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -104,12 +104,13 @@ class ArithMSum * Make the Node corresponding to the interpretation of msum, [msum], where: * [msum] = sum_{( v, c ) \in msum } [c]*[v] * - * @param tn The type of the node to return, which is used only if msum is - * empty * @param msum The monomial sum * @return The node corresponding to the monomial sum + * + * Note this utility is agnostic to types, it will return the integer 0 if + * msum is empty. */ - static Node mkNode(TypeNode tn, const std::map& msum); + static Node mkNode(const std::map& msum); /** make coefficent term * @@ -164,6 +165,9 @@ class ArithMSum * This function may return false if lit does not contain v, * or if lit is an integer equality with a coefficent on v, * e.g. 3*v = 7. + * + * Note this utility is agnostic to types, the returned term may be Int when + * v is Real. */ static Node solveEqualityFor(Node lit, Node v); diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 804e476fb..be0a35736 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -988,7 +988,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) msum.erase(pi); if (!msum.empty()) { - rem = ArithMSum::mkNode(t[0].getType(), msum); + rem = ArithMSum::mkNode(msum); } } } diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 174d448ee..183c90049 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -809,6 +809,8 @@ set(regress_0_tests regress0/nl/issue8515-cov-iand.smt2 regress0/nl/issue8516-cov-sin.smt2 regress0/nl/issue8638-cov-resultants.smt2 + regress0/nl/issue8691-msum-subtypes.smt2 + regress0/nl/issue8691-3-msum-subtypes.smt2 regress0/nl/lazard-spurious-root.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 diff --git a/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 b/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 new file mode 100644 index 000000000..09170bead --- /dev/null +++ b/test/regress/cli/regress0/nl/issue8691-3-msum-subtypes.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(assert (distinct 0 (/ a (+ 0.5 a)))) +(check-sat) diff --git a/test/regress/cli/regress0/nl/issue8691-msum-subtypes.smt2 b/test/regress/cli/regress0/nl/issue8691-msum-subtypes.smt2 new file mode 100644 index 000000000..6679cf6fa --- /dev/null +++ b/test/regress/cli/regress0/nl/issue8691-msum-subtypes.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_NIRA) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (> b 0)) +(assert (> 0 (/ (to_real (+ a a)) (to_real b)))) +(assert (= 0 (+ b a))) +(check-sat) -- 2.30.2