diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/bound_var_manager.cpp | 2 | ||||
-rw-r--r-- | src/expr/dtype.cpp | 2 | ||||
-rw-r--r-- | src/expr/nary_term_util.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 6 | ||||
-rw-r--r-- | src/expr/node_manager_template.cpp | 11 | ||||
-rw-r--r-- | src/expr/term_context_node.cpp | 2 | ||||
-rw-r--r-- | src/expr/term_context_node.h | 2 |
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); /** |