Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

7 files changed, 23 insertions, 6 deletions

diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index 53c87fb97..450b2358f 100644
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -53,7 +53,7 @@ Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i)
 
 Node BoundVarManager::getCacheValue(size_t i)
 {
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(i));
+  return NodeManager::currentNM()->mkConstInt(Rational(i));
 }
 
 Node BoundVarManager::getCacheValue(TNode cv, size_t i)
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5b2503454..4902b1562 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -867,7 +867,7 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   ss << "sel_" << index;
   SkolemManager* sm = nm->getSkolemManager();
   TypeNode stype = nm->mkSelectorType(dtt, t);
-  Node nindex = nm->mkConst(CONST_RATIONAL, Rational(index));
+  Node nindex = nm->mkConstInt(Rational(index));
   s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex);
   d_sharedSel[dtt][t][index] = s;
   Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp
index a872c64c7..03ce637e4 100644
--- a/src/expr/nary_term_util.cpp
+++ b/src/expr/nary_term_util.cpp
@@ -119,10 +119,10 @@ Node getNullTerminator(Kind k, TypeNode tn)
     case OR: nullTerm = nm->mkConst(false); break;
     case AND:
     case SEP_STAR: nullTerm = nm->mkConst(true); break;
-    case PLUS: nullTerm = nm->mkConst(CONST_RATIONAL, Rational(0)); break;
+    case PLUS: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break;
     case MULT:
     case NONLINEAR_MULT:
-      nullTerm = nm->mkConst(CONST_RATIONAL, Rational(1));
+      nullTerm = nm->mkConstRealOrInt(tn, Rational(1));
       break;
     case STRING_CONCAT:
       // handles strings and sequences
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6435c488a..b2682661e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -579,6 +579,12 @@ class NodeManager
    */
   Node mkConstInt(const Rational& r);
 
+  /**
+   * Make constant real or int, which calls one of the above methods based
+   * on the type tn.
+   */
+  Node mkConstRealOrInt(const TypeNode& tn, 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/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index b00d79322..4f235a53a 100644
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1298,4 +1298,15 @@ Node NodeManager::mkConstInt(const Rational& r)
   return mkConst(kind::CONST_RATIONAL, r);
 }
 
+Node NodeManager::mkConstRealOrInt(const TypeNode& tn, const Rational& r)
+{
+  Assert(tn.isRealOrInt()) << "Expected real or int for mkConstRealOrInt, got "
+                           << tn;
+  if (tn.isReal())
+  {
+    return mkConstReal(r);
+  }
+  return mkConstInt(r);
+}
+
 }  // namespace cvc5
diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp
index 3be9faad0..91e6dbfd3 100644
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -54,7 +54,7 @@ Node TCtxNode::getNodeHash() const { return computeNodeHash(d_node, d_val); }
 Node TCtxNode::computeNodeHash(Node n, uint32_t val)
 {
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::SEXPR, n, nm->mkConst(CONST_RATIONAL, Rational(val)));
+  return nm->mkNode(kind::SEXPR, n, nm->mkConstInt(Rational(val)));
 }
 
 Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val)
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index ac89b0d71..9e4fe90de 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -54,7 +54,7 @@ class TCtxNode
   Node getNodeHash() const;
   /**
    * Get node hash, which is a unique node representation of the pair (n, val).
-   * In particular, this returns (SEXPR n (CONST_RATIONAL val)).
+   * In particular, this returns (SEXPR n (CONST_INTEGER val)).
    */
   static Node computeNodeHash(Node n, uint32_t val);
   /**