From: Andrew Reynolds Date: Fri, 8 Apr 2022 20:58:02 +0000 (-0500) Subject: Eliminate more uses of CONST_RATIONAL (#8590) X-Git-Tag: cvc5-1.0.1~282 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de3d3cabc372a50c953404e3e193b15ef7609ba4;p=cvc5.git Eliminate more uses of CONST_RATIONAL (#8590) To eliminate arithmetic subtyping, we require distinguishing CONST_RATIONAL and CONST_INTEGER internally. Code should avoid usage of these kinds and use trusted utilities instead (e.g. mkConstReal, mkConstInst, isConst). --- diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index a30d312e7..6bf79b4ea 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -181,7 +181,8 @@ const Integer& ArithIteUtils::gcdIte(Node n){ if(d_gcds.find(n) != d_gcds.end()){ return d_gcds[n]; } - if(n.getKind() == kind::CONST_RATIONAL){ + if (n.isConst()) + { const Rational& q = n.getConst(); if(q.isIntegral()){ d_gcds[n] = q.getNumerator(); diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 7b9db4beb..b0709c1b3 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -99,6 +99,12 @@ Kind transKinds(Kind k1, Kind k2) return UNDEFINED_KIND; } +bool isZero(const Node& n) +{ + Assert(n.getType().isRealOrInt()); + return n.isConst() && n.getConst().sgn() == 0; +} + bool isTranscendentalKind(Kind k) { // many operators are eliminated during rewriting diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index d4df80e3d..98afea98f 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -298,6 +298,9 @@ Kind joinKinds(Kind k1, Kind k2); */ Kind transKinds(Kind k1, Kind k2); +/** Is n (integer or real) zero? */ +bool isZero(const Node& n); + /** Is k a transcendental function kind? */ bool isTranscendentalKind(Kind k); /** diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index d69933984..bc21c6b4b 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -27,7 +27,6 @@ namespace nl { NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } bool NlExtTheoryCallback::getCurrentSubstitution( @@ -73,7 +72,7 @@ bool NlExtTheoryCallback::isExtfReduced( // we do not handle reductions of transcendental functions here return false; } - if (n != d_zero) + if (!isZero(n)) { Kind k = n.getKind(); if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND @@ -91,7 +90,6 @@ bool NlExtTheoryCallback::isExtfReduced( // As an optimization, we minimize the explanation for why a term can be // simplified to zero, for example, if (= x 0) ^ (= y 5) => (= (* x y) 0), // we minimize the explanation to (= x 0) => (= (* x y) 0). - Assert(n == d_zero); id = ExtReducedId::ARITH_SR_ZERO; if (on.getKind() == NONLINEAR_MULT) { @@ -124,7 +122,7 @@ bool NlExtTheoryCallback::isExtfReduced( { for (unsigned r = 0; r < 2; r++) { - if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) + if (isZero(eqs[j][r]) && vars.find(eqs[j][1 - r]) != vars.end()) { Trace("nl-ext-zero-exp") << "...single exp : " << eqs[j] << std::endl; diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index c27fef929..c458e55f9 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -68,8 +68,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback private: /** The underlying equality engine. */ eq::EqualityEngine* d_ee; - /** Commonly used nodes */ - Node d_zero; }; } // namespace nl diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index a73cf4771..e13294f10 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -324,6 +324,8 @@ bool NlModel::addSubstitution(TNode v, TNode s) bool NlModel::addBound(TNode v, TNode l, TNode u) { + Assert(l.getType().isSubtypeOf(v.getType())); + Assert(u.getType().isSubtypeOf(v.getType())); Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " " << u << "]" << std::endl; if (l == u) diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 0e5c0d5f0..cb116e97d 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -41,7 +41,7 @@ class RationalEnumerator : public TypeEnumeratorBase { Node operator*() override { - return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, d_rat); + return NodeManager::currentNM()->mkConstReal(d_rat); } RationalEnumerator& operator++() override { @@ -85,8 +85,7 @@ class IntegerEnumerator : public TypeEnumeratorBase { Node operator*() override { - return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, - Rational(d_int)); + return NodeManager::currentNM()->mkConstInt(Rational(d_int)); } IntegerEnumerator& operator++() override diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 2c1b5126e..3c5089943 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -738,7 +738,7 @@ Node BagsUtils::evaluateBagFilter(TNode n) for (const auto& [e, count] : elements) { - Node multiplicity = nm->mkConst(CONST_RATIONAL, count); + Node multiplicity = nm->mkConstInt(count); Node bag = nm->mkBag(bagType.getBagElementType(), e, multiplicity); Node pOfe = nm->mkNode(APPLY_UF, P, e); Node ite = nm->mkNode(ITE, pOfe, bag, empty); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 183b3213b..4307dcbe3 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -401,7 +401,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m, nm->getSkolemManager()->mkDummySkolem("slack", elementType); Trace("bags-model") << "newElement is " << newElement << std::endl; Rational difference = rCardRational - constructedRational; - Node multiplicity = nm->mkConst(CONST_RATIONAL, difference); + Node multiplicity = nm->mkConstInt(difference); Node slackBag = nm->mkBag(elementType, newElement, multiplicity); constructedBag = nm->mkNode(kind::BAG_UNION_DISJOINT, constructedBag, slackBag); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 479aa870b..e1627de97 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -775,7 +775,7 @@ Node TheoryStrings::mkSkeletonFromBase(Node r, TypeNode etn = r.getType().getSequenceElementType(); for (size_t i = currIndex; i < nextIndex; i++) { - cacheVals.push_back(nm->mkConst(CONST_RATIONAL, Rational(currIndex))); + cacheVals.push_back(nm->mkConstInt(Rational(currIndex))); Node kv = sm->mkSkolemFunction( SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals); skChildren.push_back(nm->mkSeqUnit(etn, kv));