From d43b252d1c4588c1662811bfe7d7352823aae447 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Nov 2021 13:07:14 -0600 Subject: [PATCH] Preparations for eliminating arithmetic subtyping (#7637) Adds TypeNode::isArithmetic, NodeManager::mkConstReal and NodeManager::mkConstInt. The first method (for now) is equivalent to TypeNode::isReal, and the latter 2 are equivalent to NodeManager::mkConst(CONST_RATIONAL, ...). This furthermore distinguishes all uses of isReal: all that intend to be isArithmetic are changed in this PR. Redundant uses of isReal() || isInteger() are merged to isArithmetic(). Due to the above, there are no behavior changes in this PR. --- src/expr/node_manager.cpp | 12 +++++++ src/expr/node_manager.h | 16 ++++++++++ src/expr/type_node.cpp | 6 +++- src/expr/type_node.h | 3 ++ src/preprocessing/passes/learned_rewrite.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- .../alethe_nosubtype_node_converter.cpp | 4 +-- src/theory/arith/arith_ite_utils.cpp | 23 +++++++++---- src/theory/arith/arith_msum.cpp | 2 +- src/theory/arith/arith_msum.h | 2 +- src/theory/arith/arith_poly_norm.cpp | 2 +- src/theory/arith/kinds | 16 +++++++--- src/theory/arith/nl/ext/proof_checker.cpp | 10 +++--- src/theory/arith/nl/nl_model.cpp | 2 +- src/theory/arith/pp_rewrite_eq.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 13 +++++--- src/theory/arith/theory_arith_type_rules.cpp | 27 ++++++++++++++-- src/theory/arith/theory_arith_type_rules.h | 10 ++++++ src/theory/arrays/theory_arrays_rewriter.cpp | 2 +- .../arrays/theory_arrays_type_rules.cpp | 2 +- .../cegqi/ceg_arith_instantiator.cpp | 4 +-- .../quantifiers/cegqi/ceg_instantiator.cpp | 32 +++++++++++++------ .../ematching/inst_match_generator.cpp | 2 +- .../ematching/pattern_term_selector.cpp | 2 +- .../ematching/relational_match_generator.cpp | 2 +- .../ematching/trigger_term_info.cpp | 2 +- src/theory/quantifiers/extended_rewrite.cpp | 2 +- .../quantifiers/quantifiers_attributes.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 4 +-- src/theory/quantifiers/relevant_domain.cpp | 3 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 17 +++++----- src/theory/quantifiers/term_util.cpp | 6 ++-- 32 files changed, 171 insertions(+), 65 deletions(-) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 62c718245..7b1c2de13 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -34,6 +34,7 @@ #include "theory/sets/singleton_op.h" #include "util/abstract_value.h" #include "util/bitvector.h" +#include "util/rational.h" #include "util/resource_manager.h" using namespace std; @@ -1109,4 +1110,15 @@ Node NodeManager::mkNode(TNode opNode, std::initializer_list children) return nb.constructNode(); } +Node NodeManager::mkConstReal(const Rational& r) +{ + return mkConst(kind::CONST_RATIONAL, r); +} + +Node NodeManager::mkConstInt(const Rational& r) +{ + // !!!! Note will update to CONST_INTEGER. + return mkConst(kind::CONST_RATIONAL, r); +} + } // namespace cvc5 diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d301c857c..f3dc1c1df 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -46,6 +46,7 @@ class SkolemManager; class BoundVarManager; class DType; +class Rational; namespace expr { namespace attr { @@ -534,6 +535,21 @@ class NodeManager template NodeClass mkConstInternal(Kind k, const T&); + /** + * Make constant real. Returns constant of kind CONST_RATIONAL with Rational + * payload. + */ + Node mkConstReal(const Rational& r); + + /** + * Make constant real. Returns constant of kind CONST_INTEGER with Rational + * payload. + * + * !!! Note until subtypes are eliminated, this returns a constant of kind + * CONST_RATIONAL. + */ + Node mkConstInt(const Rational& r); + /** Create a node with children. */ TypeNode mkTypeNode(Kind kind, TypeNode child1); TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 6f522bbe8..c8a0d9ce2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -96,7 +96,7 @@ CardinalityClass TypeNode::getCardinalityClass() { ret = CardinalityClass::FINITE; } - else if (isString() || isRegExp() || isSequence() || isReal() || isBag()) + else if (isString() || isRegExp() || isSequence() || isRealOrInt() || isBag()) { ret = CardinalityClass::INFINITE; } @@ -276,6 +276,10 @@ Node TypeNode::mkGroundValue() const bool TypeNode::isStringLike() const { return isString() || isSequence(); } +// !!! Note that this will change to isReal() || isInteger() when subtyping is +// eliminated +bool TypeNode::isRealOrInt() const { return isReal(); } + bool TypeNode::isSubtypeOf(TypeNode t) const { if(*this == t) { return true; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 89b5b7299..8469344db 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -485,6 +485,9 @@ private: /** Is this a string-like type? (string or sequence) */ bool isStringLike() const; + /** Is this the integer or real type? */ + bool isRealOrInt() const; + /** Is this the Rounding Mode type? */ bool isRoundingMode() const; diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index 81f5718cf..642a63aa4 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -309,7 +309,7 @@ Node LearnedRewrite::rewriteLearned(Node n, // could also do num + k*den checks } } - else if (k == GEQ || (k == EQUAL && nr[0].getType().isReal())) + else if (k == GEQ || (k == EQUAL && nr[0].getType().isRealOrInt())) { std::map msum; if (ArithMSum::getMonomialSumLit(nr, msum)) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fe41f2256..fe464a8bd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -495,7 +495,7 @@ void Smt2Printer::toStream(std::ostream& out, } if (!type_asc_arg.isNull()) { - if (force_nt.isReal()) + if (force_nt.isRealOrInt()) { // we prefer using (/ x 1) instead of (to_real x) here. // the reason is that (/ x 1) is SMT-LIB compliant when x is a constant diff --git a/src/proof/alethe/alethe_nosubtype_node_converter.cpp b/src/proof/alethe/alethe_nosubtype_node_converter.cpp index 54fb09228..e8c115ebe 100644 --- a/src/proof/alethe/alethe_nosubtype_node_converter.cpp +++ b/src/proof/alethe/alethe_nosubtype_node_converter.cpp @@ -32,8 +32,8 @@ Node AletheNoSubtypeNodeConverter::postConvert(Node n) std::vector children; for (size_t i = 0, size = n.getNumChildren(); i < size; ++i) { - if (!argTypes[i].isReal() || argTypes[i].isInteger() || !n[i].isConst() - || !n[i].getType().isInteger()) + if (!argTypes[i].isRealOrInt() || argTypes[i].isInteger() + || !n[i].isConst() || !n[i].getType().isInteger()) { children.push_back(n[i]); continue; diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index b42b97d59..d986dd74b 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -59,7 +59,8 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ switch(n.getKind()){ case ITE:{ Node c = n[0], t = n[1], e = n[2]; - if(n.getType().isReal()){ + if (n.getType().isRealOrInt()) + { Node rc = reduceVariablesInItes(c); Node rt = reduceVariablesInItes(t); Node re = reduceVariablesInItes(e); @@ -84,7 +85,9 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ d_varParts[n] = vpite; return sum; } - }else{ // non-arith ite + } + else + { // non-arith ite if(!d_contains.containsTermITE(n)){ // don't bother adding to d_reduceVar return n; @@ -96,7 +99,8 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ } }break; default: - if(n.getType().isReal() && Polynomial::isMember(n)){ + if (n.getType().isRealOrInt() && Polynomial::isMember(n)) + { Node newn = Node::null(); if(!d_contains.containsTermITE(n)){ newn = n; @@ -126,7 +130,9 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ d_reduceVar[n] = newn; return newn; } - }else{ + } + else + { if(!d_contains.containsTermITE(n)){ return n; } @@ -179,7 +185,9 @@ const Integer& ArithIteUtils::gcdIte(Node n){ }else{ return d_one; } - }else if(n.getKind() == kind::ITE && n.getType().isReal()){ + } + else if (n.getKind() == kind::ITE && n.getType().isRealOrInt()) + { const Integer& tgcd = gcdIte(n[1]); if(tgcd.isOne()){ d_gcds[n] = d_one; @@ -210,7 +218,7 @@ Node ArithIteUtils::reduceIteConstantIteByGCD_rec(Node n, const Rational& q){ Node ArithIteUtils::reduceIteConstantIteByGCD(Node n){ Assert(n.getKind() == kind::ITE); - Assert(n.getType().isReal()); + Assert(n.getType().isRealOrInt()); const Integer& gcd = gcdIte(n); if(gcd.isOne()){ Node newIte = reduceConstantIteByGCD(n[0]).iteNode(n[1],n[2]); @@ -234,7 +242,8 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){ if(d_reduceGcd.find(n) != d_reduceGcd.end()){ return d_reduceGcd[n]; } - if(n.getKind() == kind::ITE && n.getType().isReal()){ + if (n.getKind() == kind::ITE && n.getType().isRealOrInt()) + { return reduceIteConstantIteByGCD(n); } diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index ac3780b36..a8edb0e79 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -249,7 +249,7 @@ Node ArithMSum::solveEqualityFor(Node lit, Node v) return lit[1 - r]; } } - if (tn.isReal()) + if (tn.isRealOrInt()) { std::map msum; if (ArithMSum::getMonomialSumLit(lit, msum)) diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index 3c205c9b7..87f56e64f 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -34,7 +34,7 @@ namespace theory { * (b) c is null. * * We say Node v is a {monomial variable} (or m-variable) if either: - * (a) v.getType().isReal() and v is not a constant, or + * (a) v.getType().isRealOrInt() and v is not a constant, or * (b) v is null. * * For m-constant or m-variable t, we write [t] to denote 1 if t.isNull() and diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp index 81cd3646a..151adc874 100644 --- a/src/theory/arith/arith_poly_norm.cpp +++ b/src/theory/arith/arith_poly_norm.cpp @@ -173,7 +173,7 @@ std::vector PolyNorm::getMonoVars(TNode m) PolyNorm PolyNorm::mkPolyNorm(TNode n) { - Assert(n.getType().isReal()); + Assert(n.getType().isRealOrInt()); Rational one(1); Node null; std::unordered_map visited; diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 0f3e345ee..f577b4109 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -71,6 +71,13 @@ constant CONST_RATIONAL \ "util/rational.h" \ "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class" +constant CONST_INTEGER \ + class \ + Rational \ + ::cvc5::RationalHashFunction \ + "util/rational.h" \ + "a multiple-precision integer constant; payload is an instance of the cvc5::Rational class" + enumerator REAL_TYPE \ "::cvc5::theory::arith::RationalEnumerator" \ "theory/arith/type_enumerator.h" @@ -112,11 +119,12 @@ typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule typerule CONST_RATIONAL ::cvc5::theory::arith::ArithConstantTypeRule +typerule CONST_INTEGER ::cvc5::theory::arith::ArithConstantTypeRule -typerule LT "SimpleTypeRule" -typerule LEQ "SimpleTypeRule" -typerule GT "SimpleTypeRule" -typerule GEQ "SimpleTypeRule" +typerule LT ::cvc5::theory::arith::ArithRelationTypeRule +typerule LEQ ::cvc5::theory::arith::ArithRelationTypeRule +typerule GT ::cvc5::theory::arith::ArithRelationTypeRule +typerule GEQ ::cvc5::theory::arith::ArithRelationTypeRule typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule" typerule INDEXED_ROOT_PREDICATE ::cvc5::theory::arith::IndexedRootPredicateTypeRule diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 7acee487d..ff6d6a5e8 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -122,11 +122,11 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, { Assert(children.empty()); Assert(args.size() == 6); - Assert(args[0].getType().isReal()); - Assert(args[1].getType().isReal()); - Assert(args[2].getType().isReal()); - Assert(args[3].getType().isReal()); - Assert(args[4].getType().isReal()); + Assert(args[0].getType().isRealOrInt()); + Assert(args[1].getType().isRealOrInt()); + Assert(args[2].getType().isRealOrInt()); + Assert(args[3].getType().isRealOrInt()); + Assert(args[4].getType().isRealOrInt()); Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL && args[5].getConst().isIntegral()); Node t = args[0]; diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 8d06f41d0..d23ddd53d 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -205,7 +205,7 @@ bool NlModel::checkModel(const std::vector& assertions, if (visited.find(cur) == visited.end()) { visited.insert(cur); - if (cur.getType().isReal() && !cur.isConst()) + if (cur.getType().isRealOrInt() && !cur.isConst()) { Kind k = cur.getKind(); if (k != MULT && k != PLUS && k != NONLINEAR_MULT diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index aa186edd6..6391836e5 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -37,7 +37,7 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) { return TrustNode::null(); } - Assert(atom[0].getType().isReal()); + Assert(atom[0].getType().isRealOrInt()); Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; Node rewritten = rewrite(leq.andNode(geq)); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 6a43ed09b..d4b84be01 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1274,7 +1274,7 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){ throw LogicException(ss.str()); } Assert(!d_partialModel.hasArithVar(x)); - Assert(x.getType().isReal()); // real or integer + Assert(x.getType().isRealOrInt()); // real or integer ArithVar max = d_partialModel.getNumberOfVariables(); ArithVar varX = d_partialModel.allocate(x, aux); @@ -3044,12 +3044,17 @@ bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{ case kind::LT: return !isSatLiteral(n); case kind::EQUAL: - if(n[0].getType().isReal()){ + if (n[0].getType().isRealOrInt()) + { return !isSatLiteral(n); - }else if(n[0].getType().isBoolean()){ + } + else if (n[0].getType().isBoolean()) + { return hasFreshArithLiteral(n[0]) || hasFreshArithLiteral(n[1]); - }else{ + } + else + { return false; } case kind::IMPLIES: diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index 9bcc6ca2b..786b98196 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -59,7 +59,7 @@ TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager, } if (check) { - if (!childType.isReal()) + if (!childType.isRealOrInt()) { throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); @@ -83,6 +83,29 @@ TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager, } } +TypeNode ArithRelationTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + Assert(n.getNumChildren() == 2); + TypeNode t1 = n[0].getType(check); + if (!t1.isRealOrInt()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an arithmetic term for arithmetic relation"); + } + TypeNode t2 = n[1].getType(check); + if (!t1.isComparableTo(t2)) + { + throw TypeCheckingExceptionPrivate( + n, "expecting arithmetic terms of comparable type"); + } + } + return nodeManager->booleanType(); +} + TypeNode RealNullaryOperatorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) @@ -165,7 +188,7 @@ TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager, n, "expecting boolean term as first argument"); } TypeNode t2 = n[1].getType(check); - if (!t2.isReal()) + if (!t2.isRealOrInt()) { throw TypeCheckingExceptionPrivate( n, "expecting polynomial as second argument"); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 1fbd96648..66b3ebedd 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -35,6 +35,16 @@ class ArithConstantTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +/** + * Type rule for arithmetic relations. Returns Boolean. Throws a type error + * if the types of the children are not arithmetic or not comparable. + */ +class ArithRelationTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + /** * Type rule for arithmetic operators. * Takes care of mixed-integer operators, cases and (total) division. diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 4f11e323e..e933eaacd 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -307,7 +307,7 @@ Node TheoryArraysRewriter::expandEqRange(TNode node) { kle = kind::FLOATINGPOINT_LEQ; } - else if (type.isInteger() || type.isReal()) + else if (type.isRealOrInt()) { kle = kind::LEQ; } diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 433768e5d..a389c6efb 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -316,7 +316,7 @@ TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager, n, "eqrange upper index type does not match array index type"); } if (!indexType.isBitVector() && !indexType.isFloatingPoint() - && !indexType.isInteger() && !indexType.isReal()) + && !indexType.isRealOrInt()) { throw TypeCheckingExceptionPrivate( n, diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 425ab0484..2d483d502 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -130,7 +130,7 @@ Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, Node atom = lit.getKind() == NOT ? lit[0] : lit; // arithmetic inequalities and disequalities if (atom.getKind() == GEQ - || (atom.getKind() == EQUAL && atom[0].getType().isReal())) + || (atom.getKind() == EQUAL && atom[0].getType().isRealOrInt())) { return lit; } @@ -149,7 +149,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, bool pol = lit.getKind() != NOT; // arithmetic inequalities and disequalities Assert(atom.getKind() == GEQ - || (atom.getKind() == EQUAL && atom[0].getType().isReal())); + || (atom.getKind() == EQUAL && atom[0].getType().isRealOrInt())); // get model value for pv Node pv_value = ci->getModelValue(pv); // cannot contain infinity? diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 494ac8e53..9556d3f9c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -337,7 +337,7 @@ CegHandledStatus CegInstantiator::isCbqiSort( return itv->second; } CegHandledStatus ret = CEG_UNHANDLED; - if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() + if (tn.isRealOrInt() || tn.isBoolean() || tn.isBitVector() || tn.isFloatingPoint()) { ret = CEG_HANDLED; @@ -482,15 +482,24 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) if( d_instantiator.find( v )==d_instantiator.end() ){ TypeNode tn = v.getType(); Instantiator * vinst; - if( tn.isReal() ){ + if (tn.isRealOrInt()) + { vinst = new ArithInstantiator(d_env, tn, d_parent->getVtsTermCache()); - }else if( tn.isDatatype() ){ + } + else if (tn.isDatatype()) + { vinst = new DtInstantiator(d_env, tn); - }else if( tn.isBitVector() ){ + } + else if (tn.isBitVector()) + { vinst = new BvInstantiator(d_env, tn, d_parent->getBvInverter()); - }else if( tn.isBoolean() ){ + } + else if (tn.isBoolean()) + { vinst = new ModelValueInstantiator(d_env, tn); - }else{ + } + else + { //default vinst = new Instantiator(d_env, tn); } @@ -1261,7 +1270,9 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + if (atom.getKind() == GEQ + || (atom.getKind() == EQUAL && !pol && atom[0].getType().isRealOrInt())) + { NodeManager* nm = NodeManager::currentNM(); Assert(atom.getKind() != GEQ || atom[1].isConst()); Node atom_lhs; @@ -1296,7 +1307,9 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& } } } - }else{ + } + else + { // don't know how to apply substitution to literal } } @@ -1396,7 +1409,8 @@ void CegInstantiator::processAssertions() { TheoryId tid = Theory::theoryOf( rtn ); //if we care about the theory of this eqc if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){ - if( rtn.isInteger() || rtn.isReal() ){ + if (rtn.isRealOrInt()) + { rtn = rtn.getBaseType(); } Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl; diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 8c2d8e6c4..e3dd246a7 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -380,7 +380,7 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) } else { - Assert(t.getType().isReal()); + Assert(t.getType().isRealOrInt()); t_match = nm->mkNode(PLUS, t, nm->mkConst(CONST_RATIONAL, Rational(1))); } diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 0ab6e1098..9933eb6c9 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -154,7 +154,7 @@ Node PatternTermSelector::getIsUsableTrigger(Node n, Node q) else if (TriggerTermInfo::isRelationalTrigger(n)) { Node rtr = getIsUsableEq(q, n); - if (rtr.isNull() && n[0].getType().isReal()) + if (rtr.isNull() && n[0].getType().isRealOrInt()) { // try to solve relation std::map m; diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp index dc8f64f6d..5cf9079e8 100644 --- a/src/theory/quantifiers/ematching/relational_match_generator.cpp +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -35,7 +35,7 @@ RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, d_pol(pol), d_counter(0) { - Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal()) + Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isRealOrInt()) || rtrigger.getKind() == GEQ); Trace("relational-match-gen") << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 24efc60c3..611f30ef0 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -94,7 +94,7 @@ bool TriggerTermInfo::isUsableRelationTrigger(Node n, lit = lit[0]; } // is it a relational trigger? - if ((lit.getKind() == EQUAL && lit[0].getType().isReal()) + if ((lit.getKind() == EQUAL && lit[0].getType().isRealOrInt()) || lit.getKind() == GEQ) { // if one side of the relation is a variable and the other side is a ground diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 5aab618c0..4ed918b43 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -291,7 +291,7 @@ Node ExtendedRewriter::extendedRewriteAggr(Node n) const << "Do aggressive rewrites on " << n << std::endl; bool polarity = n.getKind() != NOT; Node ret_atom = n.getKind() == NOT ? n[0] : n; - if ((ret_atom.getKind() == EQUAL && ret_atom[0].getType().isReal()) + if ((ret_atom.getKind() == EQUAL && ret_atom[0].getType().isRealOrInt()) || ret_atom.getKind() == GEQ) { // ITE term removal in polynomials diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 3afa2715b..bb9568c88 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -113,7 +113,7 @@ Node QuantAttributes::getFunDefBody( Node q ) { }else if( q[1][1]==h ){ return q[1][0]; } - else if (q[1][0].getType().isReal()) + else if (q[1][0].getType().isRealOrInt()) { // solve for h in the equality std::map msum; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index adb91fddd..c38d0aa91 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -723,7 +723,7 @@ Node QuantifiersRewriter::getVarElimEq(Node lit, Assert(lit.getKind() == EQUAL); Node slv; TypeNode tt = lit[0].getType(); - if (tt.isReal()) + if (tt.isRealOrInt()) { slv = getVarElimEqReal(lit, args, var); } @@ -1098,7 +1098,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, << ", pol = " << pol << "..." << std::endl; bool canSolve = lit.getKind() == GEQ - || (lit.getKind() == EQUAL && lit[0].getType().isReal() && !pol); + || (lit.getKind() == EQUAL && lit[0].getType().isRealOrInt() && !pol); if (!canSolve) { continue; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index a531d88b7..0f3699990 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -331,7 +331,8 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No rdl.d_rd[1] = nullptr; }else{ //solve the inequality for one/two variables, if possible - if( n[0].getType().isReal() ){ + if (n[0].getType().isRealOrInt()) + { std::map< Node, Node > msum; if (ArithMSum::getMonomialSumLit(n, msum)) { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index cca1d76e2..a05b64249 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -83,7 +83,8 @@ void CegGrammarConstructor::collectTerms( if( cur.isConst() ){ TypeNode tn = cur.getType(); Node c = cur; - if( tn.isReal() ){ + if (tn.isRealOrInt()) + { c = nm->mkConst(CONST_RATIONAL, c.getConst().abs()); } consts[tn].insert(c); @@ -407,7 +408,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, std::vector& ops) { NodeManager* nm = NodeManager::currentNM(); - if (type.isReal()) + if (type.isRealOrInt()) { ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(0))); ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(1))); @@ -552,8 +553,8 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( opLArgs.push_back(nm->mkBoundVar(bArgType)); // build zarg Node zarg; - Assert(bArgType.isReal() || bArgType.isBitVector()); - if (bArgType.isReal()) + Assert(bArgType.isRealOrInt() || bArgType.isBitVector()); + if (bArgType.isRealOrInt()) { zarg = nm->mkConst(CONST_RATIONAL, Rational(0)); } @@ -678,7 +679,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // If the type does not support any term, we do any constant instead. // We also fall back on any constant construction if the type has no // constructors at this point (e.g. it simply encodes all constants). - if (!types[i].isReal()) + if (!types[i].isRealOrInt()) { tsgcm = options::SygusGrammarConsMode::ANY_CONST; } @@ -769,7 +770,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } - if (types[i].isReal()) + if (types[i].isRealOrInt()) { // Add PLUS, MINUS Kind kinds[2] = {PLUS, MINUS}; @@ -1099,7 +1100,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( << "Build any-term datatype for " << types[i] << "..." << std::endl; // for now, only real has any term construction - Assert(types[i].isReal()); + Assert(types[i].isRealOrInt()); // We have initialized the given type sdts[i], which should now contain // a constructor for each relevant arithmetic term/variable. We now // construct a sygus datatype of one of the following two forms. @@ -1377,7 +1378,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // type specific predicates std::stringstream ssop; - if (types[i].isReal()) + if (types[i].isRealOrInt()) { Kind kind = LEQ; Trace("sygus-grammar-def") << "...add for " << k << std::endl; diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index cb8bad174..beb02c1c5 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -329,7 +329,7 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) { Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) { Node n; - if (tn.isInteger() || tn.isReal()) + if (tn.isRealOrInt()) { Rational c(val); n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c); @@ -382,7 +382,7 @@ Node TermUtil::mkTypeValueOffset(TypeNode tn, status = -1; if (!offset_val.isNull()) { - if (tn.isInteger() || tn.isReal()) + if (tn.isRealOrInt()) { val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode(PLUS, val, offset_val)); @@ -557,7 +557,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) } else { - if (n.getType().isReal() && n.getConst().sgn() < 0) + if (n.getType().isInteger() && n.getConst().sgn() < 0) { // negative arguments if (ik == STRING_SUBSTR || ik == STRING_CHARAT) -- 2.30.2