Make arith msum utility agnostic to Int (#8694)

This utility should continue to assume arithmetic subtypes.

Fixes #8691.

diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 12d7a8360424f57019eacb5ba7dc9915669db46d..f963741277ef32720da6f0ffcc77f6a7b9bd30fc 100644 (file)
--- 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<Node, Node>& msum)
         NodeManager* nm = NodeManager::currentNM();
         if (getMonomialSum(lit[1], msum2))
         {
-          TypeNode tn = lit[0].getType();
           for (std::map<Node, Node>::iterator it = msum2.begin();
                it != msum2.end();
                ++it)
@@ -111,14 +110,14 @@ bool ArithMSum::getMonomialSumLit(Node lit, std::map<Node, Node>& msum)
               Rational r2 = it->second.isNull()
                                 ? Rational(1)
                                 : it->second.getConst<Rational>();
-              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<Rational>());
+                                          -it->second.getConst<Rational>());
             }
           }
           return true;
@@ -129,7 +128,7 @@ bool ArithMSum::getMonomialSumLit(Node lit, std::map<Node, Node>& msum)
   return false;
 }
 
-Node ArithMSum::mkNode(TypeNode tn, const std::map<Node, Node>& msum)
+Node ArithMSum::mkNode(const std::map<Node, Node>& msum)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> children;
@@ -151,7 +150,7 @@ Node ArithMSum::mkNode(TypeNode tn, const std::map<Node, Node>& 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 989f9bc3e179531ba0dffb10e7905c67b961f058..237395b3a51b27af2fda22f1c2ca4819bd48dbe0 100644 (file)
--- 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<Node, Node>& msum);
+  static Node mkNode(const std::map<Node, Node>& 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 804e476fbbd71b85558d91c6d5cdf013c5783b8b..be0a3573670f70ea414c311534db92cf0d4a1a05 100644 (file)
--- 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 174d448eed1d3529d9e374e1665a16bb155c19c0..183c90049cc38c1686f508095a9997d984f5b457 100644 (file)
--- 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 (file)
index 0000000..09170be
--- /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 (file)
index 0000000..6679cf6
--- /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)