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 91652b7ce7ce27b9f5561fc4ddd574e3828c5592..8d634c77a2376bd4a2a9c9e31557a7883185bcfd 100644 (file)
--- 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 <kind> 0)
-  if (rewriter::isIntegral(atom))
+  // Now we have (sum <kind> 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 e8743a43aca55c61da5ea1d72a325d1087529f56..dca343e82632e66c2668bb974931335cd6dc38d8 100644 (file)
--- 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<TNode> 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 fd25a79d3fb87ce67d630cc31705784a88d62c45..fa2a7506745cdd1d9c9761a286591237a1e2a923 100644 (file)
--- a/src/theory/arith/rewriter/addition.h
+++ b/src/theory/arith/rewriter/addition.h
@@ -53,6 +53,14 @@ using Sum = std::map<Node, RealAlgebraicNumber, TermComparator>;
  */
 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 3d1856e0b3cebe4cfbc77ba688a147d29a154243..69522b237bcfc1ea016951f9f9b983430af288f3 100644 (file)
--- 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<TNode> 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 f8e030386cf6854792736f9c55f281653f8f4a3e..a6d311b3de0f8cf5026b812370c3183820b825be 100644 (file)
--- 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 e627186f22fc2c69b09c2739c562a57f2e7eb66f..5163a145d9a396652f1aa64f4c71455d2defffcf 100644 (file)
--- 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 67be26f52d936fe0555c4332f6ca4b98b0dc2ee6..807abb4c2507ccf7dee0693e888108cb13835931 100644 (file)
--- 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 (file)
index 0000000..a151911
--- /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)