From 4aa5c467d199e958bd3b0d10ea11fa587e199ae1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Apr 2022 12:49:05 -0500 Subject: [PATCH] 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. --- src/expr/node_manager_template.cpp | 7 ++--- src/proof/proof_rule.cpp | 3 +-- src/theory/arith/arith_msum.cpp | 2 +- src/theory/arith/linear/constraint.cpp | 2 +- .../arith/linear/theory_arith_private.cpp | 27 ++++++++++++------- 5 files changed, 25 insertions(+), 16 deletions(-) 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 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(false)}); std::vector assumptions = {leq.getNode().negate(), @@ -3896,8 +3895,20 @@ void TheoryArithPrivate::collectModelValues(const std::set& 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( -- 2.30.2