From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 4 Mar 2022 22:31:10 +0000 (+0100)
Subject: Remove spurious assertion in linear solver (#8231)
X-Git-Tag: cvc5-1.0.0~321
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39b607b9c93bc14048bbbff543e8d16534c606f0;p=cvc5.git

Remove spurious assertion in linear solver (#8231)

This PR removes a spurious assertion about how integer equality should look like. It actually requires that the coefficients of the leading terms on both sides of the equation are positive, which can't be true in general anyway. Note that the regression failed before we refactored the arithmetic rewriter.

Fixes cvc5/cvc5-projects#469
---

diff --git a/src/theory/arith/rewriter/rewrite_atom.cpp b/src/theory/arith/rewriter/rewrite_atom.cpp
index 5163a145d..f412abe6b 100644
--- a/src/theory/arith/rewriter/rewrite_atom.cpp
+++ b/src/theory/arith/rewriter/rewrite_atom.cpp
@@ -259,20 +259,27 @@ Node buildRelation(Kind kind, Node left, Node right, bool negate)
 
 Node buildIntegerEquality(Sum&& sum)
 {
-  Trace("arith-rewriter") << "building integer inequality from " << sum << std::endl;
+  Trace("arith-rewriter") << "building integer equality from " << sum
+                          << std::endl;
   normalizeGCDLCM(sum);
 
+  Trace("arith-rewriter::debug") << "\tnormalized to " << sum << std::endl;
+
   const auto& constant = *sum.begin();
   if (constant.first.isConst())
   {
     Assert(constant.second.isRational());
     if (!constant.second.toRational().isIntegral())
     {
+      Trace("arith-rewriter::debug")
+          << "\thas non-integer constant, thus false" << std::endl;
       return mkConst(false);
     }
   }
 
   auto minabscoeff = removeMinAbsCoeff(sum);
+  Trace("arith-rewriter::debug") << "\tremoved min abs coeff " << minabscoeff
+                                 << ", left with " << sum << std::endl;
   if (sgn(minabscoeff.second) < 0)
   {
     // move minabscoeff goes to the right and switch lhs and rhs
@@ -285,6 +292,9 @@ Node buildIntegerEquality(Sum&& sum)
   }
   Node left = mkMultTerm(minabscoeff.second, minabscoeff.first);
 
+  Trace("arith-rewriter::debug")
+      << "\tbuilding " << left << " = " << sum << std::endl;
+
   return buildRelation(Kind::EQUAL, left, collectSum(sum));
 }
 
@@ -306,7 +316,8 @@ Node buildRealEquality(Sum&& sum)
 
 Node buildIntegerInequality(Sum&& sum, Kind k)
 {
-  Trace("arith-rewriter") << "building integer equality from " << sum << std::endl;
+  Trace("arith-rewriter") << "building integer inequality from " << sum
+                          << std::endl;
   bool negate = normalizeGCDLCM(sum, true);
 
   if (negate)
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ac7acb4be..ff2c7a145 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4801,7 +4801,6 @@ bool TheoryArithPrivate::decomposeTerm(Node t,
     m *= g;
     poly = poly * Rational(1,g);
     Assert(poly.isIntegral());
-    Assert(poly.leadingCoefficientIsPositive());
   }else{
     Assert(!intVars);
     m = poly.getHead().getConstant().getValue();
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f1d1de2e8..ea5bc37cd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -76,6 +76,7 @@ set(regress_0_tests
   regress0/arith/mod.01.smt2
   regress0/arith/mult.01.smt2
   regress0/arith/non-normal.smt2
+  regress0/arith/projissue469-int-equality.smt2
   regress0/arr1.smt2
   regress0/arr1.smtv1.smt2
   regress0/arr2.smtv1.smt2
diff --git a/test/regress/regress0/arith/projissue469-int-equality.smt2 b/test/regress/regress0/arith/projissue469-int-equality.smt2
new file mode 100644
index 000000000..59fdf1d48
--- /dev/null
+++ b/test/regress/regress0/arith/projissue469-int-equality.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-option :nl-ext-ent-conf true)
+(declare-const x Int)
+(assert (> (* x x) (+ x x)))
+(assert (not (str.is_digit (str.from_code x))))
+(check-sat)