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.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 62c718245faff25acf9bddc80ce6282cd01d5304..7b1c2de13f1f0a70606f89b6e448381ce755d8ad 100644 (file)
--- 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<TNode> 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 d301c857c59d900abf97f068feabab7e8ffdb6e8..f3dc1c1dfd83abeca13789e0094885c9998e9b99 100644 (file)
--- 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 <class NodeClass, class T>
   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 6f522bbe82d97fd8aa09cb86d0c74bc02d1196fa..c8a0d9ce26be3a24a79a0c76b568b6b24fcf8912 100644 (file)
--- 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 89b5b7299300a7106ecbb28ac455d59b1439cfa7..8469344dba35a6377373a0f9b0b37fe9d5453c27 100644 (file)
--- 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 81f5718cf4e8d5b4bea120424f1c626fc78fb437..642a63aa48fe916fa378de3456eae52fe9809eb6 100644 (file)
--- 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<Node, Node> msum;
     if (ArithMSum::getMonomialSumLit(nr, msum))

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fe41f22567f2f19edcc9c4ae7b8340e4eace3604..fe464a8bdd47617f798bdfdc1daa71eb5c725a9f 100644 (file)
--- 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 54fb09228b6f3c9858acb662e7aac72dc2fd6722..e8c115ebe1794bef986e825fc7bf58829004a289 100644 (file)
--- 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<Node> 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 b42b97d59fce46b95bffeefa69fdd67d8561caed..d986dd74b4373ed151000d5832d86e990c039d4e 100644 (file)
--- 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 ac3780b367cd7f9cac44673f7b6fc81d77d9bded..a8edb0e7908bf06ece2a49016589d04b14486c69 100644 (file)
--- 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<Node, Node> msum;
     if (ArithMSum::getMonomialSumLit(lit, msum))

diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h
index 3c205c9b75ec27aea6c3b5e4877774d5a820907d..87f56e64f8f106f625a3252fc2c4685be0ff6fe1 100644 (file)
--- 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 81cd3646ae4eb91c8d6c16afa801258683cf7524..151adc874608a52f6d3fea4a08fbab148c54f125 100644 (file)
--- a/src/theory/arith/arith_poly_norm.cpp
+++ b/src/theory/arith/arith_poly_norm.cpp
@@ -173,7 +173,7 @@ std::vector<TNode> 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<TNode, PolyNorm> visited;

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 0f3e345ee4cc689e923d219dd5d883430f81fb55..f577b41094bd36d1d983e6fac23ddd3c9cf8f932 100644 (file)
--- 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<RBool, AReal, AReal>"
-typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
-typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
-typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
+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<RBuiltinOperator>"
 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 7acee487da9a0f6b8ade0684e50340b00c2b0df5..ff6d6a5e810fc1a218b0fe92f5d626af56f4d4cd 100644 (file)
--- 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<Rational>().isIntegral());
     Node t = args[0];

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 8d06f41d0f3b8d5d844535530c93e09544037732..d23ddd53dc3d67435ca02ff557a6eb8ae3097993 100644 (file)
--- 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<Node>& 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 aa186edd6d7946d309407c38d00fa2750eeef9fe..6391836e551f100d1cdef326832703a5fd364e4e 100644 (file)
--- 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 6a43ed09b93e842adf1f311c8ce21d96ab8f8f6d..d4b84be01e8d7e893b87966ecc4889f859f9e393 100644 (file)
--- 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 9bcc6ca2b24a615ea0641b0f5c2ed5af41e3d544..786b98196f665869aabc7dbfd0da928bdb90bcb2 100644 (file)
--- 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 1fbd9664864021b421f9f1745ad5ed946867f7de..66b3ebedd783031891b274e57e04976a355a73fe 100644 (file)
--- 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 4f11e323eba7288a5de12fcd3fd607765847ade1..e933eaacd07884c373a633ad9ad42be635afa8d6 100644 (file)
--- 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 433768e5d1dc56f90f7153f439f1a2294aedd32c..a389c6efb66ffd3aa3bd180f02705fa15f1f51ec 100644 (file)
--- 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 425ab0484c0fbbe0d387ca3ed9becde0e824f3d5..2d483d50225eb8c805b2ec2bf57143478aba3d44 100644 (file)
--- 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 494ac8e53175873d9a3b66d7dd01277efcade1fc..9556d3f9c381c6f0374085a3f8394b5a9391affa 100644 (file)
--- 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 8c2d8e6c450195503eb1591effdb9a8335fdea01..e3dd246a7cc4d8d8b9fefe518c8d1d88b3a6b12a 100644 (file)
--- 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 0ab6e1098a42c7409d83a3686f458060b3ae6f53..9933eb6c99c24fc79846a903e654742dde927866 100644 (file)
--- 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<Node, Node> m;

diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
index dc8f64f6df8cf0c18d96ba3f3f7cf1021a8f9e97..5cf9079e8e7c719684f5d30a11a3d70d3af38a27 100644 (file)
--- 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 24efc60c3cc716b5a55ae843f7f87dd0c02be76c..611f30ef05391edf232f82a300e1c5d6891d704d 100644 (file)
--- 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 5aab618c05c97df343ee384bf1730ecbcded0094..4ed918b43fd9231188b0616d13576ffd746dae02 100644 (file)
--- 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 3afa2715ba267642b9b5c508aee7fbf454e9bc2c..bb9568c88bc7c620d9f20887619527c83f5523d3 100644 (file)
--- 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<Node, Node> msum;

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index adb91fdddac042d050f5663fba3b81f9aa626d5f..c38d0aa91128f8df236d1ef5947d159619f1dfdc 100644 (file)
--- 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 a531d88b79c4dcd722c29f9d6d2a46ac3744adac..0f3699990992b19e87270e36c7cb60c42a27f248 100644 (file)
--- 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 cca1d76e222b4f4ccf94620448de967687f2659d..a05b64249bee6e3455b7a7cbc3eda9fa7cca25aa 100644 (file)
--- 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<Rational>().abs());
         }
         consts[tn].insert(c);
@@ -407,7 +408,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
                                                     std::vector<Node>& 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 cb8bad1744de2871db9e6d9ce3379b9d36f83fa6..beb02c1c57b70c78f2ef10ce787b179ae64dd13c 100644 (file)
--- 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<Rational>().sgn() < 0)
+    if (n.getType().isInteger() && n.getConst<Rational>().sgn() < 0)
     {
       // negative arguments
       if (ik == STRING_SUBSTR || ik == STRING_CHARAT)