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 5163a145d9a396652f1aa64f4c71455d2defffcf..f412abe6bf280429aedebb98907a944e94a9caed 100644 (file)
--- 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 ac7acb4be68d8cceaa5bd07d06d05e5ec0ac4378..ff2c7a145b375d592d2502447ad0a3fb584916bc 100644 (file)
--- 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 f1d1de2e809d92c24516aa189a4ca7efdab2a1de..ea5bc37cdc6883a6ce724177e4d9f2e0a8772ee2 100644 (file)
--- 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 (file)
index 0000000..59fdf1d
--- /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)