From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 29 Apr 2022 17:49:05 +0000 (-0500)
Subject: Ensure mkConstInt is used on integral rationals only (#8683)
X-Git-Tag: cvc5-1.0.1~199
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4aa5c467d199e958bd3b0d10ea11fa587e199ae1;p=cvc5.git

Ensure mkConstInt is used on integral rationals only (#8683)

This is work towards using CONST_INTEGER for integer constants.

This corrects a few places that incorrectly assumed that integers were necessary.
---

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 2b1412c21..64f24f89a 100644
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1284,6 +1284,7 @@ Node NodeManager::mkConstReal(const Rational& r)
 Node NodeManager::mkConstInt(const Rational& r)
 {
   // !!!! Note will update to CONST_INTEGER.
+  Assert(r.isIntegral());
   return mkConst(kind::CONST_RATIONAL, r);
 }
 
@@ -1291,11 +1292,11 @@ Node NodeManager::mkConstRealOrInt(const TypeNode& tn, const Rational& r)
 {
   Assert(tn.isRealOrInt()) << "Expected real or int for mkConstRealOrInt, got "
                            << tn;
-  if (tn.isReal())
+  if (tn.isInteger())
   {
-    return mkConstReal(r);
+    return mkConstInt(r);
   }
-  return mkConstInt(r);
+  return mkConstReal(r);
 }
 
 Node NodeManager::mkRealAlgebraicNumber(const RealAlgebraicNumber& ran)
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index b3f780474..c96655a61 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -160,8 +160,7 @@ const char* toString(PfRule id)
     case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
     case PfRule::STRING_INFERENCE: return "STRING_INFERENCE";
     //================================================= Arith rules
-    case PfRule::MACRO_ARITH_SCALE_SUM_UB:
-      return "ARITH_SCALE_SUM_UPPER_BOUNDS";
+    case PfRule::MACRO_ARITH_SCALE_SUM_UB: return "MACRO_ARITH_SCALE_SUM_UB";
     case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
     case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 5337021ef..12d7a8360 100644
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -195,7 +195,7 @@ int ArithMSum::isolate(
       {
         if (vtn.isInteger())
         {
-          veq_c = nm->mkConstInt(r.abs());
+          veq_c = nm->mkConstReal(r.abs());
         }
         else
         {
diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp
index 9ed758f98..d33a40c1d 100644
--- a/src/theory/arith/linear/constraint.cpp
+++ b/src/theory/arith/linear/constraint.cpp
@@ -1808,7 +1808,7 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
           TypeNode type = plit[0].getType();
           for (Rational r : *getFarkasCoefficients())
           {
-            farkasCoeffs.push_back(nm->mkConstRealOrInt(type, Rational(r)));
+            farkasCoeffs.push_back(nm->mkConstReal(Rational(r)));
           }
 
           // Apply the scaled-sum rule.
diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp
index 04ebdeffb..0d31d734f 100644
--- a/src/theory/arith/linear/theory_arith_private.cpp
+++ b/src/theory/arith/linear/theory_arith_private.cpp
@@ -1407,10 +1407,9 @@ TrustNode TheoryArithPrivate::dioCutting()
       Pf pfNotGeq = d_pnm->mkAssume(geq.getNode().negate());
       Pf pfLt =
           d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotGeq}, {lt});
-      Pf pfSum = d_pnm->mkNode(
-          PfRule::MACRO_ARITH_SCALE_SUM_UB,
-          {pfGt, pfLt},
-          {nm->mkConstRealOrInt(type, -1), nm->mkConstRealOrInt(type, 1)});
+      Pf pfSum = d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+                               {pfGt, pfLt},
+                               {nm->mkConstReal(-1), nm->mkConstReal(1)});
       Pf pfBot = d_pnm->mkNode(
           PfRule::MACRO_SR_PRED_TRANSFORM, {pfSum}, {nm->mkConst<bool>(false)});
       std::vector<Node> assumptions = {leq.getNode().negate(),
@@ -3896,8 +3895,20 @@ void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
         const DeltaRational& mod = d_partialModel.getAssignment(v);
         Rational qmodel = mod.substituteDelta(delta);
 
-        Node qNode = nm->mkConstRealOrInt(term.getType(), qmodel);
-        Trace("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
+        Node qNode;
+        if (!qmodel.isIntegral())
+        {
+          // Note that the linear solver may generate non-integer values for
+          // integer variables in rare cases. We construct real in this case;
+          // this will be corrected in TheoryArith::sanityCheckIntegerModel.
+          qNode = nm->mkConstReal(qmodel);
+        }
+        else
+        {
+          qNode = nm->mkConstRealOrInt(term.getType(), qmodel);
+        }
+        Trace("arith::collectModelInfo") << "m->assertEquality(" << term << ", "
+                                         << qNode << ", true)" << endl;
         // Add to the map
         arithModel[term] = qNode;
       }else{
@@ -4461,9 +4472,7 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
         std::transform(coeffs->begin(),
                        coeffs->end(),
                        std::back_inserter(farkasCoefficients),
-                       [nm, type](const Rational& r) {
-                         return nm->mkConstRealOrInt(type, r);
-                       });
+                       [nm](const Rational& r) { return nm->mkConstReal(r); });
 
         // Prove bottom.
         auto sumPf = d_pnm->mkNode(