From: Andrew Reynolds Date: Mon, 13 Dec 2021 19:48:49 +0000 (-0600) Subject: Initial cut at distinguishing uses of CONST_RATIONAL (#7682) X-Git-Tag: cvc5-1.0.0~675 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e6c7645d3d98ba734ab73ed76c7785b572b86c8;p=cvc5.git Initial cut at distinguishing uses of CONST_RATIONAL (#7682) --- 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); /** diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index e6b5a4bca..2ff45aef0 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -235,25 +235,19 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) } else if (current.isConst()) { - switch (current.getKind()) + if (current.getType().isInteger()) { - case kind::CONST_RATIONAL: + Rational constant = current.getConst(); + Assert (constant.isIntegral()); + BitVector bv(size, constant.getNumerator()); + if (bv.toSignedInteger() != constant.getNumerator()) { - Rational constant = current.getConst(); - if (constant.isIntegral()) { - BitVector bv(size, constant.getNumerator()); - if (bv.toSignedInteger() != constant.getNumerator()) - { - throw TypeCheckingExceptionPrivate( - current, - string("Not enough bits for constant in intToBV: ") - + current.toString()); - } - result = nm->mkConst(bv); - } - break; + throw TypeCheckingExceptionPrivate( + current, + string("Not enough bits for constant in intToBV: ") + + current.toString()); } - default: break; + result = nm->mkConst(bv); } } else diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 66646b766..1be5ee81b 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -213,8 +213,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)), - one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)), one = nm->mkConstInt(Rational(1)); Node trueNode = nm->mkConst(true); unordered_map intVars; @@ -276,10 +275,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( break; } if ((*j1)[1].getKind() != kind::EQUAL - || !(((*j1)[1][0].isVar() - && (*j1)[1][1].getKind() == kind::CONST_RATIONAL) - || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL - && (*j1)[1][1].isVar()))) + || !(((*j1)[1][0].isVar() && (*j1)[1][1].isConst()) + || ((*j1)[1][0].isConst() && (*j1)[1][1].isVar()))) { eligible = false; Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; @@ -332,14 +329,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( } sort(posv.begin(), posv.end()); const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); - const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][1] - : (*j1)[1][0]; + const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0]; const pair pos_var(pos, var); - const Rational& constant = - ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][0].getConst() - : (*j1)[1][1].getConst(); + const Rational& constant = ((*j1)[1][0].isConst()) + ? (*j1)[1][0].getConst() + : (*j1)[1][1].getConst(); uint64_t mark = 0; unsigned countneg = 0, thepos = 0; for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii) @@ -406,14 +400,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( const bool xneg = (x.getKind() == kind::NOT); x = xneg ? x[0] : x; Debug("miplib") << " x:" << x << " " << xneg << endl; - const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][1] - : (*j1)[1][0]; + const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0]; const pair x_var(x, var); - const Rational& constant = - ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j1)[1][0].getConst() - : (*j1)[1][1].getConst(); + const Rational& constant = ((*j1)[1][0].isConst()) + ? (*j1)[1][0].getConst() + : (*j1)[1][1].getConst(); unsigned mark = (xneg ? 0 : 1); if ((marks[x_var] & (1u << mark)) != 0) { @@ -573,17 +564,15 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeBuilder sumb(kind::PLUS); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { - sumb << nm->mkNode(kind::MULT, - nm->mkConst(CONST_RATIONAL, coef[pos_var][jj]), - newVars[jj]); + sumb << nm->mkNode( + kind::MULT, nm->mkConstInt(coef[pos_var][jj]), newVars[jj]); } sum = sumb; } else { - sum = nm->mkNode(kind::MULT, - nm->mkConst(CONST_RATIONAL, coef[pos_var][0]), - newVars[0]); + sum = nm->mkNode( + kind::MULT, nm->mkConstInt(coef[pos_var][0]), newVars[0]); } Debug("miplib") << "vars[] " << var << endl << " eq " << rewrite(sum) << endl; diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 6c93eba15..0e7ac9c79 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -66,7 +66,7 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) Node l = assertion[0]; Node r = assertion[1]; - if (r.getKind() != kind::CONST_RATIONAL) + if (!r.isConst()) { Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl; return false; @@ -216,7 +216,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, Node l = assertion[0]; Node r = assertion[1]; - if (r.getKind() == kind::CONST_RATIONAL) + if (r.isConst()) { const Rational& rc = r.getConst(); if (isIntVar(l)) @@ -233,8 +233,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, else if (l.getKind() == kind::MULT && l.getNumChildren() == 2) { Node c = l[0], v = l[1]; - if (c.getKind() == kind::CONST_RATIONAL - && c.getConst().isNegativeOne()) + if (c.isConst() && c.getConst().isNegativeOne()) { if (isIntVar(v)) { diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 5c4539808..d2cde7b46 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -78,8 +78,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va if (!c.isNull()) { Assert(c.isConst()); - coeffs.push_back(NodeManager::currentNM()->mkConst( - CONST_RATIONAL, + coeffs.push_back(nm->mkConstInt( Rational(c.getConst().getDenominator()))); } } @@ -134,15 +133,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& va } Node sumt = sum.empty() - ? NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(0)) - : (sum.size() == 1 - ? sum[0] - : NodeManager::currentNM()->mkNode(kind::PLUS, sum)); - ret = NodeManager::currentNM()->mkNode( - ret_lit.getKind(), - sumt, - NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))); + ? nm->mkConstInt(Rational(0)) + : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::PLUS, sum)); + ret = nm->mkNode( + ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0))); if (!ret_pol) { ret = ret.negate(); diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index ae05d6b87..027be232b 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -515,9 +515,9 @@ void UnconstrainedSimplifier::processUnconstrained() if (current.getType().isInteger()) { // div/mult by 1 should have been simplified - Assert(other != nm->mkConst(CONST_RATIONAL, Rational(1))); + Assert(other != nm->mkConstInt(Rational(1))); // div by -1 should have been simplified - if (other != nm->mkConst(CONST_RATIONAL, Rational(-1))) + if (other != nm->mkConstInt(Rational(-1))) { break; } diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 6eab9b036..5af1c2b7e 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -89,7 +89,7 @@ Node LfscNodeConverter::postConvert(Node n) } // bound variable v is (bvar x T) TypeNode intType = nm->integerType(); - Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); + Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn); Node bvarOp = getSymbolInternal(k, ftype, "bvar"); @@ -136,8 +136,7 @@ Node LfscNodeConverter::postConvert(Node n) TypeNode intType = nm->integerType(); TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn); Node var = mkInternalSymbol("var", varType); - Node index = - nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); + Node index = nm->mkConstInt(Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); return nm->mkNode(APPLY_UF, var, index, tc); } @@ -176,7 +175,7 @@ Node LfscNodeConverter::postConvert(Node n) Node hconstf = getSymbolInternal(k, tnh, "apply"); return nm->mkNode(APPLY_UF, hconstf, n[0], n[1]); } - else if (k == CONST_RATIONAL || k == CAST_TO_REAL) + else if (k == CONST_RATIONAL || k == CONST_INTEGER || k == CAST_TO_REAL) { if (k == CAST_TO_REAL) { @@ -184,8 +183,9 @@ Node LfscNodeConverter::postConvert(Node n) do { n = n[0]; - Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL); - } while (n.getKind() != CONST_RATIONAL); + Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL + || n.getKind() == CONST_INTEGER); + } while (n.getKind() != CONST_RATIONAL && n.getKind() != CONST_INTEGER); } TypeNode tnv = nm->mkFunctionType(tn, tn); Node rconstf; @@ -198,7 +198,7 @@ Node LfscNodeConverter::postConvert(Node n) { // use LFSC syntax for mpz negation Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~"); - arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs())); + arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConstInt(r.abs())); } else { @@ -344,8 +344,8 @@ Node LfscNodeConverter::postConvert(Node n) Node rop = getSymbolInternal( k, relType, printer::smt2::Smt2Printer::smtKindString(k)); RegExpLoop op = n.getOperator().getConst(); - Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc)); - Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc)); + Node n1 = nm->mkConstInt(Rational(op.d_loopMinOcc)); + Node n2 = nm->mkConstInt(Rational(op.d_loopMaxOcc)); return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]); } else if (k == MATCH) @@ -485,16 +485,14 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) else if (k == BITVECTOR_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize())); + Node w = nm->mkConstInt(Rational(tn.getBitVectorSize())); tnn = nm->mkNode(APPLY_UF, tnn, w); } else if (k == FLOATINGPOINT_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node e = nm->mkConst(CONST_RATIONAL, - Rational(tn.getFloatingPointExponentSize())); - Node s = nm->mkConst(CONST_RATIONAL, - Rational(tn.getFloatingPointSignificandSize())); + Node e = nm->mkConstInt(Rational(tn.getFloatingPointExponentSize())); + Node s = nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize())); tnn = nm->mkNode(APPLY_UF, tnn, e, s); } else if (tn.getNumChildren() == 0) @@ -723,8 +721,7 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector& chars) Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char"); for (unsigned i = 0, size = vec.size(); i < size; i++) { - Node cc = nm->mkNode( - APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i]))); + Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConstInt(Rational(vec[i]))); chars.push_back(cc); } } @@ -747,42 +744,36 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) case BITVECTOR_EXTRACT: { BitVectorExtract p = n.getConst(); - indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high))); - indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low))); + indices.push_back(nm->mkConstInt(Rational(p.d_high))); + indices.push_back(nm->mkConstInt(Rational(p.d_low))); break; } case BITVECTOR_REPEAT: - indices.push_back( - nm->mkConst(CONST_RATIONAL, - Rational(n.getConst().d_repeatAmount))); + indices.push_back(nm->mkConstInt( + Rational(n.getConst().d_repeatAmount))); break; case BITVECTOR_ZERO_EXTEND: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst().d_zeroExtendAmount))); break; case BITVECTOR_SIGN_EXTEND: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst().d_signExtendAmount))); break; case BITVECTOR_ROTATE_LEFT: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst().d_rotateLeftAmount))); break; case BITVECTOR_ROTATE_RIGHT: - indices.push_back(nm->mkConst( - CONST_RATIONAL, + indices.push_back(nm->mkConstInt( Rational(n.getConst().d_rotateRightAmount))); break; case INT_TO_BITVECTOR: - indices.push_back(nm->mkConst( - CONST_RATIONAL, Rational(n.getConst().d_size))); + indices.push_back( + nm->mkConstInt(Rational(n.getConst().d_size))); break; case IAND: - indices.push_back( - nm->mkConst(CONST_RATIONAL, Rational(n.getConst().d_size))); + indices.push_back(nm->mkConstInt(Rational(n.getConst().d_size))); break; case APPLY_TESTER: { @@ -1023,7 +1014,7 @@ Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply) Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v) { NodeManager* nm = NodeManager::currentNM(); - Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v))); + Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(v))); Node tc = typeAsNode(convertType(v.getType())); return nm->mkNode(APPLY_UF, cop, x, tc); } diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp index 06bedb895..aca884ddc 100644 --- a/src/proof/lfsc/lfsc_util.cpp +++ b/src/proof/lfsc/lfsc_util.cpp @@ -68,8 +68,8 @@ LfscRule getLfscRule(Node n) Node mkLfscRuleNode(LfscRule r) { - return NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(static_cast(r))); + return NodeManager::currentNM()->mkConstInt( + Rational(static_cast(r))); } bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp index 9567590a8..042df92bb 100644 --- a/src/proof/method_id.cpp +++ b/src/proof/method_id.cpp @@ -51,8 +51,8 @@ std::ostream& operator<<(std::ostream& out, MethodId id) Node mkMethodId(MethodId id) { - return NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(static_cast(id))); + return NodeManager::currentNM()->mkConstInt( + Rational(static_cast(id))); } bool getMethodId(TNode n, MethodId& i) diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 5289d77ff..b688a28f3 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -74,8 +74,8 @@ Node ProofRuleChecker::mkKindNode(Kind k) // UNDEFINED_KIND is negative, hence return null to avoid cast return Node::null(); } - return NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(static_cast(k))); + return NodeManager::currentNM()->mkConstInt( + Rational(static_cast(k))); } ProofCheckerStatistics::ProofCheckerStatistics() diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 61a1a298c..b5542ab35 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -173,7 +173,7 @@ void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated) for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) { // Create a proof step for each n_i - Node iNode = nm->mkConst(CONST_RATIONAL, i); + Node iNode = nm->mkConstInt(i); d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode}); Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i << " added norm " << node[i] << "\n"; @@ -232,7 +232,7 @@ void ProofCnfStream::convertAndAssertOr(TNode node, bool negated) for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) { // Create a proof step for each (not n_i) - Node iNode = nm->mkConst(CONST_RATIONAL, i); + Node iNode = nm->mkConstInt(i); d_proof.addStep( node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode}); Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i @@ -687,7 +687,7 @@ SatLiteral ProofCnfStream::handleAnd(TNode node) if (added) { Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]); - Node iNode = nm->mkConst(CONST_RATIONAL, i); + Node iNode = nm->mkConstInt(i); d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode}); Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i << " added " << clauseNode << "\n"; @@ -747,7 +747,7 @@ SatLiteral ProofCnfStream::handleOr(TNode node) if (added) { Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode()); - Node iNode = nm->mkConst(CONST_RATIONAL, i); + Node iNode = nm->mkConstInt(i); d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode}); Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added " << clauseNode << "\n"; diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp index 31797ba5e..6d1882a4e 100644 --- a/src/smt/difficulty_post_processor.cpp +++ b/src/smt/difficulty_post_processor.cpp @@ -69,7 +69,7 @@ void DifficultyPostprocessCallback::getDifficultyMap( NodeManager* nm = NodeManager::currentNM(); for (const std::pair& d : d_accMap) { - dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second)); + dmap[d.first] = nm->mkConstInt(Rational(d.second)); } } diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a292fec8f..90f0a48bf 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -855,7 +855,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi; j++) { - Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j)); + Node nodej = nm->mkConstInt(Rational(j)); cdp->addStep( children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej}); } @@ -1086,8 +1086,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, TNode child = children[i]; TNode scalar = args[i]; bool isPos = scalar.getConst() > 0; - Node scalarCmp = nm->mkNode( - isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node scalarCmp = + nm->mkNode(isPos ? GT : LT, + scalar, + nm->mkConstRealOrInt(scalar.getType(), Rational(0))); // (= scalarCmp true) Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp}); Assert(!scalarCmpOrTrue.isNull()); diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index b5278a353..c661dab4b 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -47,9 +47,9 @@ IAndSolver::IAndSolver(Env& env, NodeManager* nm = NodeManager::currentNM(); d_false = nm->mkConst(false); d_true = nm->mkConst(true); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); - d_two = nm->mkConst(CONST_RATIONAL, Rational(2)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); + d_two = nm->mkConstInt(Rational(2)); } IAndSolver::~IAndSolver() {} diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 8af1a38fb..700eb6de9 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -38,7 +38,7 @@ Node pow2(uint64_t k) { Assert(k >= 0); NodeManager* nm = NodeManager::currentNM(); - return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k))); + return nm->mkConstInt(Rational(intpow2(k))); } bool oneBitAnd(bool a, bool b) { return (a && b); } @@ -60,9 +60,9 @@ Node intExtract(Node x, uint64_t i, uint64_t size) IAndUtils::IAndUtils() { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); - d_two = nm->mkConst(CONST_RATIONAL, Rational(2)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); + d_two = nm->mkConstInt(Rational(2)); } Node IAndUtils::createITEFromTable( @@ -80,8 +80,7 @@ Node IAndUtils::createITEFromTable( Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values))); // start with the default, most common value. // this value is represented in the table by (-1, -1). - Node ite = - nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(-1, -1)))); + Node ite = nm->mkConstInt(Rational(table.at(std::make_pair(-1, -1)))); for (uint64_t i = 0; i < num_of_values; i++) { for (uint64_t j = 0; j < num_of_values; j++) @@ -94,13 +93,10 @@ Node IAndUtils::createITEFromTable( // append the current value to the ite. ite = nm->mkNode( kind::ITE, - nm->mkNode( - kind::AND, - nm->mkNode( - kind::EQUAL, x, nm->mkConst(CONST_RATIONAL, Rational(i))), - nm->mkNode( - kind::EQUAL, y, nm->mkConst(CONST_RATIONAL, Rational(j)))), - nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(i, j)))), + nm->mkNode(kind::AND, + nm->mkNode(kind::EQUAL, x, nm->mkConstInt(Rational(i))), + nm->mkNode(kind::EQUAL, y, nm->mkConstInt(Rational(j)))), + nm->mkConstInt(Rational(table.at(std::make_pair(i, j)))), ite); } } @@ -139,7 +135,7 @@ Node IAndUtils::createSumNode(Node x, // number of elements in the sum expression uint64_t sumSize = bvsize / granularity; // initialize the sum - Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node sumNode = nm->mkConstInt(Rational(0)); // compute the table for the current granularity if needed if (d_bvandTable.find(granularity) == d_bvandTable.end()) { @@ -264,7 +260,7 @@ Node IAndUtils::twoToK(unsigned k) const { // could be faster NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k))); + return nm->mkNode(kind::POW, d_two, nm->mkConstInt(Rational(k))); } Node IAndUtils::twoToKMinusOne(unsigned k) const diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 4428d0350..80ccd6707 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -42,8 +42,8 @@ BagSolver::BagSolver(Env& env, d_termReg(tr), d_mapCache(userContext()) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 766731806..a5fb206aa 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -45,8 +45,8 @@ BagsRewriter::BagsRewriter(HistogramStat* statistics) : d_statistics(statistics) { d_nm = NodeManager::currentNM(); - d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = d_nm->mkConstInt(Rational(0)); + d_one = d_nm->mkConstInt(Rational(1)); } RewriteResponse BagsRewriter::postRewrite(TNode n) diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index a433ceb2d..cb6a3ea70 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -36,8 +36,8 @@ InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im) d_nm = NodeManager::currentNM(); d_sm = d_nm->getSkolemManager(); d_true = d_nm->mkConst(true); - d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = d_nm->mkConstInt(Rational(0)); + d_one = d_nm->mkConstInt(Rational(1)); } InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 9a510c6f5..6cf26d357 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -201,14 +201,10 @@ Node NormalForm::constructConstantBagFromElements( } TypeNode elementType = t.getBagElementType(); std::map::const_reverse_iterator it = elements.rbegin(); - Node bag = nm->mkBag(elementType, - it->first, - nm->mkConst(CONST_RATIONAL, it->second)); + Node bag = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second)); while (++it != elements.rend()) { - Node n = nm->mkBag(elementType, - it->first, - nm->mkConst(CONST_RATIONAL, it->second)); + Node n = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second)); bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag); } return bag; @@ -261,10 +257,10 @@ Node NormalForm::evaluateBagCount(TNode n) NodeManager* nm = NodeManager::currentNM(); if (it != elements.end()) { - Node count = nm->mkConst(CONST_RATIONAL, it->second); + Node count = nm->mkConstInt(it->second); return count; } - return nm->mkConst(CONST_RATIONAL, Rational(0)); + return nm->mkConstInt(Rational(0)); } Node NormalForm::evaluateDuplicateRemoval(TNode n) @@ -592,7 +588,7 @@ Node NormalForm::evaluateCard(TNode n) } NodeManager* nm = NodeManager::currentNM(); - Node sumNode = nm->mkConst(CONST_RATIONAL, sum); + Node sumNode = nm->mkConstInt(sum); return sumNode; } diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 61b4ebcbf..522f6749c 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -134,7 +134,7 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, Node emptyBag = nm->mkConst(EmptyBag(bagType)); Node isEmpty = A.eqNode(emptyBag); Node count = nm->mkNode(BAG_COUNT, x, A); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node geqOne = nm->mkNode(GEQ, count, one); Node geqOneAndEqual = geqOne.andNode(equal); Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual); diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 58a1b3291..0bfef55d2 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -57,7 +57,7 @@ Node BagEnumerator::operator*() BagEnumerator& BagEnumerator::operator++() { // increase the multiplicity by one - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); TypeNode elementType = d_elementTypeEnumerator.getType(); Node singleton = d_nodeManager->mkBag(elementType, d_element, one); if (d_currentBag.getKind() == kind::BAG_EMPTY) diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 9190f423f..60ded97b6 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -31,9 +31,9 @@ namespace { /** Shorthand to create a Node from a constant number */ template -Node mkRat(T val) +Node mkInt(T val) { - return NodeManager::currentNM()->mkConst(CONST_RATIONAL, val); + return NodeManager::currentNM()->mkConstInt(Rational(val)); } /** @@ -356,7 +356,7 @@ std::shared_ptr ProofCircuitPropagatorBackward::andTrue( return nullptr; } return mkProof( - PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())}); + PfRule::AND_ELIM, {assume(d_parent)}, {mkInt(i - d_parent.begin())}); } std::shared_ptr ProofCircuitPropagatorBackward::orFalse( @@ -368,7 +368,7 @@ std::shared_ptr ProofCircuitPropagatorBackward::orFalse( } return mkNot(mkProof(PfRule::NOT_OR_ELIM, {assume(d_parent.notNode())}, - {mkRat(i - d_parent.begin())})); + {mkInt(i - d_parent.begin())})); } std::shared_ptr ProofCircuitPropagatorBackward::iteC(bool c) @@ -463,7 +463,7 @@ std::shared_ptr ProofCircuitPropagatorForward::andOneFalse() auto it = std::find(d_parent.begin(), d_parent.end(), d_child); return mkResolution( mkProof( - PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}), + PfRule::CNF_AND_POS, {}, {d_parent, mkInt(it - d_parent.begin())}), d_child, true); } @@ -476,7 +476,7 @@ std::shared_ptr ProofCircuitPropagatorForward::orOneTrue() } auto it = std::find(d_parent.begin(), d_parent.end(), d_child); return mkNot(mkResolution( - mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}), + mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkInt(it - d_parent.begin())}), d_child, false)); } diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 9d11b9f7d..1c714b856 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -405,8 +405,8 @@ bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid) { - return NodeManager::currentNM()->mkConst( - CONST_RATIONAL, Rational(static_cast(tid))); + return NodeManager::currentNM()->mkConstInt( + Rational(static_cast(tid))); } } // namespace builtin diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 60bb0a9bc..71ce13c69 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -59,8 +59,8 @@ IntBlaster::IntBlaster(Env& env, d_context(userContext()) { d_nm = NodeManager::currentNM(); - d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = d_nm->mkConstInt(0); + d_one = d_nm->mkConstInt(1); }; IntBlaster::~IntBlaster() {} @@ -106,18 +106,18 @@ Node IntBlaster::maxInt(uint64_t k) { Assert(k > 0); Rational max_value = intpow2(k) - 1; - return d_nm->mkConst(CONST_RATIONAL, max_value); + return d_nm->mkConstInt(max_value); } Node IntBlaster::pow2(uint64_t k) { Assert(k >= 0); - return d_nm->mkConst(CONST_RATIONAL, intpow2(k)); + return d_nm->mkConstInt(intpow2(k)); } Node IntBlaster::modpow2(Node n, uint64_t exponent) { - Node p2 = d_nm->mkConst(CONST_RATIONAL, intpow2(exponent)); + Node p2 = d_nm->mkConstInt(intpow2(exponent)); return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2); } @@ -720,7 +720,7 @@ Node IntBlaster::translateNoChildren(Node original, BitVector constant(original.getConst()); Integer c = constant.toInteger(); Rational r = Rational(c, Integer(1)); - translation = d_nm->mkConst(CONST_RATIONAL, r); + translation = d_nm->mkConstInt(r); } else { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index adb067045..fd300fe41 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -467,7 +467,7 @@ Node eliminateBv2Nat(TNode node) { const unsigned size = utils::getSize(node[0]); NodeManager* const nm = NodeManager::currentNM(); - const Node z = nm->mkConst(CONST_RATIONAL, Rational(0)); + const Node z = nm->mkConstInt(Rational(0)); const Node bvone = utils::mkOne(1); Integer i = 1; @@ -478,8 +478,8 @@ Node eliminateBv2Nat(TNode node) nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone); - children.push_back(nm->mkNode( - kind::ITE, cond, nm->mkConst(CONST_RATIONAL, Rational(i)), z)); + children.push_back( + nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z)); } // avoid plus with one child return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); @@ -496,11 +496,11 @@ Node eliminateInt2Bv(TNode node) Integer i = 2; while (v.size() < size) { - Node cond = nm->mkNode(kind::GEQ, - nm->mkNode(kind::INTS_MODULUS_TOTAL, - node[0], - nm->mkConst(CONST_RATIONAL, Rational(i))), - nm->mkConst(CONST_RATIONAL, Rational(i, 2))); + Node cond = nm->mkNode( + kind::GEQ, + nm->mkNode( + kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))), + nm->mkConstInt(Rational(i, 2))); v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); i *= 2; } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index b475d51e7..196b4f01d 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -78,7 +78,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) const DType& dt = utils::datatypeOf(constructor); const DTypeConstructor& c = dt[constructorIndex]; unsigned weight = c.getWeight(); - children.push_back(nm->mkConst(CONST_RATIONAL, Rational(weight))); + children.push_back(nm->mkConstInt(Rational(weight))); Node res = children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children); Trace("datatypes-rewrite") @@ -104,9 +104,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) res = nm->mkConst(false); break; } - children.push_back(nm->mkNode(kind::DT_HEIGHT_BOUND, - in[0][i], - nm->mkConst(CONST_RATIONAL, rmo))); + children.push_back( + nm->mkNode(kind::DT_HEIGHT_BOUND, in[0][i], nm->mkConstInt(rmo))); } } if (res.isNull()) diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 7ca58905f..4ed6e3da9 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -108,7 +108,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* } if (argSuccess) { - narg = nm->mkConst(CONST_RATIONAL, Rational(i)); + narg = nm->mkConstInt(Rational(i)); break; } } @@ -141,7 +141,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* if (n >= 0) { Node t = exp[0]; - Node nn = nm->mkConst(CONST_RATIONAL, Rational(n)); + Node nn = nm->mkConstInt(Rational(n)); Node eq = exp.eqNode(conc); cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn}); cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {}); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 5324e1c79..ee42add6b 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -107,10 +107,10 @@ operator DT_SIZE_BOUND 2 "datatypes height bound" typerule DT_SIZE_BOUND ::cvc5::theory::datatypes::DtBoundTypeRule operator DT_SYGUS_BOUND 2 "datatypes sygus bound" -typerule DT_SYGUS_BOUND ::cvc5::theory::datatypes::DtSygusBoundTypeRule +typerule DT_SYGUS_BOUND ::cvc5::theory::datatypes::DtBoundTypeRule operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function" -typerule DT_SYGUS_EVAL ::cvc5::theory::datatypes::DtSyguEvalTypeRule +typerule DT_SYGUS_EVAL ::cvc5::theory::datatypes::DtSygusEvalTypeRule # Kinds for match terms. For example, the match term diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 88a3e43d7..90511112c 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -57,7 +57,7 @@ SygusExtension::SygusExtension(Env& env, d_active_terms(context()), d_currTermSize(context()) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_true = NodeManager::currentNM()->mkConst(true); } @@ -1772,8 +1772,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue() NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); d_measure_value = sm->mkDummySkolem("mt", nm->integerType()); - Node mtlem = nm->mkNode( - kind::GEQ, d_measure_value, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node mtlem = + nm->mkNode(kind::GEQ, d_measure_value, nm->mkConstInt(Rational(0))); d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); } return d_measure_value; @@ -1787,8 +1787,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); Node new_mt = sm->mkDummySkolem("mt", nm->integerType()); - Node mtlem = - nm->mkNode(kind::GEQ, new_mt, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConstInt(Rational(0))); d_measure_value_active = new_mt; d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); } @@ -1817,8 +1816,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s) NodeManager* nm = NodeManager::currentNM(); Trace("sygus-engine") << "******* Sygus : allocate size literal " << s << " for " << d_this << std::endl; - return nm->mkNode( - DT_SYGUS_BOUND, d_this, nm->mkConst(CONST_RATIONAL, Rational(s))); + return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConstInt(Rational(s))); } int SygusExtension::getGuardStatus( Node g ) { diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 1b5e37bc3..4826e87bc 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -245,7 +245,7 @@ bool SygusSimpleSymBreak::considerArgKind( rt.d_children[0].d_req_kind = PLUS; rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1); rt.d_children[0].d_children[1].d_req_const = - NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + NodeManager::currentNM()->mkConstInt(Rational(1)); rt.d_children[1].d_req_type = dt[c].getArgType(0); } else if (k == LT || k == GEQ) @@ -256,7 +256,7 @@ bool SygusSimpleSymBreak::considerArgKind( rt.d_children[1].d_req_kind = PLUS; rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0); rt.d_children[1].d_children[1].d_req_const = - NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); + NodeManager::currentNM()->mkConstInt(Rational(1)); } } else if (pk == BITVECTOR_NOT) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3f11ab1da..3f13886ed 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -68,7 +68,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env, { d_true = NodeManager::currentNM()->mkConst( true ); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_dtfCounter = 0; // indicate we are using the default theory state object diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 78bc67868..422af1731 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -322,10 +322,10 @@ TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager, throw TypeCheckingExceptionPrivate( n, "expecting datatype bound term to have datatype argument."); } - if (n[1].getKind() != kind::CONST_RATIONAL) + if (!n[1].isConst() || !n[1].getType().isInteger()) { - throw TypeCheckingExceptionPrivate(n, - "datatype bound must be a constant"); + throw TypeCheckingExceptionPrivate( + n, "datatype bound must be a constant integer"); } if (n[1].getConst().getNumerator().sgn() == -1) { @@ -336,34 +336,9 @@ TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager, return nodeManager->booleanType(); } -TypeNode DtSygusBoundTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - if (check) - { - if (!n[0].getType().isDatatype()) - { - throw TypeCheckingExceptionPrivate( - n, "datatype sygus bound takes a datatype"); - } - if (n[1].getKind() != kind::CONST_RATIONAL) - { - throw TypeCheckingExceptionPrivate( - n, "datatype sygus bound must be a constant"); - } - if (n[1].getConst().getNumerator().sgn() == -1) - { - throw TypeCheckingExceptionPrivate( - n, "datatype sygus bound must be non-negative"); - } - } - return nodeManager->booleanType(); -} - -TypeNode DtSyguEvalTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) +TypeNode DtSygusEvalTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) { TypeNode headType = n[0].getType(check); if (!headType.isDatatype()) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 7cf98aa74..3b1276221 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -64,12 +64,7 @@ class DtBoundTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class DtSygusBoundTypeRule { - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -class DtSyguEvalTypeRule +class DtSygusEvalTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp index d50d10d9f..7714abfa9 100644 --- a/src/theory/difficulty_manager.cpp +++ b/src/theory/difficulty_manager.cpp @@ -44,7 +44,7 @@ void DifficultyManager::getDifficultyMap(std::map& dmap) NodeManager* nm = NodeManager::currentNM(); for (const std::pair p : d_dfmap) { - dmap[p.first] = nm->mkConst(CONST_RATIONAL, Rational(p.second)); + dmap[p.first] = nm->mkConstInt(Rational(p.second)); } } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 5a4e8e7bc..d4fc32197 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -469,8 +469,8 @@ std::ostream& operator<<(std::ostream& out, InferenceId i) Node mkInferenceIdNode(InferenceId i) { - return NodeManager::currentNM()->mkConst(CONST_RATIONAL, - Rational(static_cast(i))); + return NodeManager::currentNM()->mkConstInt( + Rational(static_cast(i))); } bool getInferenceId(TNode n, InferenceId& i) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index ec33fe5fd..81ae18f4f 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -163,8 +163,8 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop) } else { - Assert(new_theta.getKind() == CONST_RATIONAL); - Assert(pv_prop.d_coeff.getKind() == CONST_RATIONAL); + Assert(new_theta.isConst()); + Assert(pv_prop.d_coeff.isConst()); NodeManager* nm = NodeManager::currentNM(); new_theta = nm->mkConst(CONST_RATIONAL, Rational(new_theta.getConst() @@ -1165,8 +1165,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], - NodeManager::currentNM()->mkConst( - CONST_RATIONAL, + NodeManager::currentNM()->mkConstReal( Rational(1) / prop[i].d_coeff.getConst())); nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); nn = rewrite(nn); @@ -1214,10 +1213,9 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ Node c_coeff; if( !msum_coeff[it->first].isNull() ){ - c_coeff = rewrite(NodeManager::currentNM()->mkConst( - CONST_RATIONAL, + c_coeff = rewrite(NodeManager::currentNM()->mkConstReal( pv_prop.d_coeff.getConst() - / msum_coeff[it->first].getConst())); + / msum_coeff[it->first].getConst())); }else{ c_coeff = pv_prop.d_coeff; } @@ -1283,7 +1281,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& }else{ atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]); atom_lhs = rewrite(atom_lhs); - atom_rhs = nm->mkConst(CONST_RATIONAL, Rational(0)); + atom_rhs = nm->mkConstRealOrInt(atom_lhs.getType(), Rational(0)); } //must be an eligible term if( isEligible( atom_lhs ) ){ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index e08f89218..2555ff637 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -58,8 +58,8 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, d_added_cbqi_lemma(userContext()), d_vtsCache(new VtsTermCache(env, qim)), d_bv_invert(nullptr), - d_small_const_multiplier(NodeManager::currentNM()->mkConst( - CONST_RATIONAL, Rational(1) / Rational(1000000))), + d_small_const_multiplier(NodeManager::currentNM()->mkConstReal( + Rational(1) / Rational(1000000))), d_small_const(d_small_const_multiplier) { d_check_vts_lemma_lc = false; @@ -435,6 +435,7 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { } d_curr_quant = Node::null(); }else if( e==1 ){ + NodeManager* nm = NodeManager::currentNM(); //minimize the free delta heuristically on demand if( d_check_vts_lemma_lc ){ Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; @@ -453,12 +454,10 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_vtsCache->getVtsTerms(inf, true, false, false); for( unsigned i=0; imkNode( + Node inf_lem_lb = nm->mkNode( GT, inf[i], - NodeManager::currentNM()->mkConst( - CONST_RATIONAL, - Rational(1) / d_small_const.getConst())); + nm->mkConstReal(Rational(1) / d_small_const.getConst())); d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF); } } diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index f405da345..058b6a8bf 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -31,7 +31,6 @@ namespace quantifiers { VtsTermCache::VtsTermCache(Env& env, QuantifiersInferenceManager& qim) : EnvObj(env), d_qim(qim) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } void VtsTermCache::getVtsTerms(std::vector& t, @@ -71,7 +70,8 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create) sm->mkDummySkolem("delta_free", nm->realType(), "free delta for virtual term substitution"); - Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero); + Node zero = nm->mkConstReal(Rational(0)); + Node delta_lem = nm->mkNode(GT, d_vts_delta_free, zero); d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA); } if (d_vts_delta.isNull()) @@ -216,13 +216,17 @@ Node VtsTermCache::rewriteVtsSymbols(Node n) { nlit = nm->mkConst(false); } - else if (res == 1) - { - nlit = nm->mkNode(GEQ, d_zero, slv); - } else { - nlit = nm->mkNode(GT, slv, d_zero); + Node zero = nm->mkConstRealOrInt(slv.getType(), Rational(0)); + if (res == 1) + { + nlit = nm->mkNode(GEQ, zero, slv); + } + else + { + nlit = nm->mkNode(GT, slv, zero); + } } } } diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 60c8f28f3..7ae16aec8 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -127,8 +127,6 @@ class VtsTermCache : protected EnvObj private: /** Reference to the quantifiers inference manager */ QuantifiersInferenceManager& d_qim; - /** constants */ - Node d_zero; /** The virtual term substitution delta */ Node d_vts_delta; /** The virtual term substitution "free delta" */ diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 9933eb6c9..e4d7436c8 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -678,8 +678,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) Assert(nc.isConst()); if (x.getType().isInteger()) { - Node coeff = - nm->mkConst(CONST_RATIONAL, nc.getConst().abs()); + Node coeff = nm->mkConstInt(nc.getConst().abs()); if (!nc.getConst().abs().isOne()) { x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff); @@ -691,8 +690,7 @@ Node PatternTermSelector::getInversion(Node n, Node x) } else { - Node coeff = nm->mkConst(CONST_RATIONAL, - Rational(1) / nc.getConst()); + Node coeff = nm->mkConstReal(Rational(1) / nc.getConst()); x = nm->mkNode(MULT, x, coeff); } } diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 4ed918b43..1152267e8 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -49,7 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_intZero = NodeManager::currentNM()->mkConstInt(Rational(0)); } void ExtendedRewriter::setCache(Node n, Node ret) const @@ -1723,7 +1723,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const strings::ArithEntail aent(&d_rew); // (str.substr s x y) --> "" if x < len(s) |= 0 >= y Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(LT, node[1], tot_len)); - if (aent.checkWithAssumption(n1_lt_tot_len, d_zero, node[2], false)) + if (aent.checkWithAssumption(n1_lt_tot_len, d_intZero, node[2], false)) { Node ret = strings::Word::mkEmptyWord(node.getType()); debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN"); @@ -1731,7 +1731,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const } // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s) - Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_zero, node[2])); + Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_intZero, node[2])); if (aent.checkWithAssumption(non_zero_len, node[1], tot_len, false)) { Node ret = strings::Word::mkEmptyWord(node.getType()); @@ -1739,8 +1739,8 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const return ret; } // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s) - Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_zero)); - if (aent.checkWithAssumption(geq_zero_start, d_zero, tot_len, false)) + Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_intZero)); + if (aent.checkWithAssumption(geq_zero_start, d_intZero, tot_len, false)) { Node ret = strings::Word::mkEmptyWord(node.getType()); debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S"); diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 1b9d0dae4..bf5829e03 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -262,7 +262,7 @@ class ExtendedRewriter /** Common constant nodes */ Node d_true; Node d_false; - Node d_zero; + Node d_intZero; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b5b9e7d88..18a63d245 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -59,7 +59,7 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n) { NodeManager* nm = NodeManager::currentNM(); - Node cn = nm->mkConst(CONST_RATIONAL, Rational(n == 0 ? 0 : n - 1)); + Node cn = nm->mkConstInt(Rational(n == 0 ? 0 : n - 1)); return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn); } @@ -84,10 +84,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() Node lem = nm->mkNode( EQUAL, currLit, - nm->mkNode( - curr == 0 ? LT : LEQ, - d_range, - nm->mkConst(CONST_RATIONAL, Rational(curr == 0 ? 0 : curr - 1)))); + nm->mkNode(curr == 0 ? LT : LEQ, + d_range, + nm->mkConstInt(Rational(curr == 0 ? 0 : curr - 1)))); return lem; } @@ -693,8 +692,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { } choices.pop_back(); Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i); - Node cMinCard = - nm->mkNode(LEQ, srCardN, nm->mkConst(CONST_RATIONAL, Rational(i))); + Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConstInt(Rational(i))); choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody)); d_setm_choice[sro].push_back(choice_i); } @@ -818,8 +816,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node range = rewrite(nm->mkNode(MINUS, u, l)); // 9999 is an arbitrary range past which we do not do exhaustive // bounded instantation, based on the check below. - Node ra = rewrite(nm->mkNode( - LEQ, range, nm->mkConst(CONST_RATIONAL, Rational(9999)))); + Node ra = + rewrite(nm->mkNode(LEQ, range, nm->mkConstInt(Rational(9999)))); Node tl = l; Node tu = u; getBounds( q, v, rsi, tl, tu ); @@ -830,8 +828,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for (long k = 0; k < rr; k++) { - Node t = - nm->mkNode(PLUS, tl, nm->mkConst(CONST_RATIONAL, Rational(k))); + Node t = nm->mkNode(PLUS, tl, nm->mkConstInt(Rational(k))); t = rewrite(t); elements.push_back( t ); } diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index af72e2a7c..dfffe64cf 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -61,10 +61,9 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) if (!c.isLargeFinite()) { NodeManager* nm = NodeManager::currentNM(); - Node card = - nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality())); + Node card = nm->mkConstInt(Rational(c.getFiniteCardinality())); // check if less than fixed upper bound - Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard)); + Node oth = nm->mkConstInt(Rational(maxCard)); Node eq = nm->mkNode(LEQ, card, oth); eq = Rewriter::rewrite(eq); mc = eq.isConst() && eq.getConst(); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9522a4b9b..d39212ddc 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -721,7 +721,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign break; } }else{ - Node z = p->getZero( k ); + Node z = p->getZero(d_vars[index].getType(), k); if( !z.isNull() ){ Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl; assigned.push_back( vn ); @@ -744,7 +744,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( slv_v!=-1 ){ Node lhs; if( children.empty() ){ - lhs = p->getZero( k ); + lhs = p->getZero(d_vars[index].getType(), k); }else if( children.size()==1 ){ lhs = children[0]; }else{ @@ -2280,18 +2280,20 @@ QuantConflictFind::Statistics::Statistics() { } -TNode QuantConflictFind::getZero( Kind k ) { - std::map< Kind, Node >::iterator it = d_zero.find( k ); - if( it==d_zero.end() ){ +TNode QuantConflictFind::getZero(TypeNode tn, Kind k) +{ + std::pair key(tn, k); + std::map, Node>::iterator it = d_zero.find(key); + if (it == d_zero.end()) + { Node nn; if( k==PLUS ){ - nn = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + nn = NodeManager::currentNM()->mkConstRealOrInt(tn, Rational(0)); } - d_zero[k] = nn; + d_zero[key] = nn; return nn; - }else{ - return it->second; } + return it->second; } std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index d14e281fb..82a925d3b 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -195,7 +195,7 @@ class QuantConflictFind : public QuantifiersModule private: context::CDO< bool > d_conflict; - std::map< Kind, Node > d_zero; + std::map, Node> d_zero; //for storing nodes created during t-constraint solving (prevents memory leaks) std::vector< Node > d_tempCache; //optimization: list of quantifiers that depend on ground function applications @@ -209,8 +209,9 @@ private: public: //for ground terms Node d_true; Node d_false; - TNode getZero( Kind k ); -private: + TNode getZero(TypeNode tn, Kind k); + + private: std::map< Node, QuantInfo > d_qinfo; private: //for equivalence classes // type -> list(eqc) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2002c73db..c53809d6e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -920,7 +920,7 @@ bool QuantifiersRewriter::getVarElimLit(Node body, for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { TypeNode tn = tspec[j]; - Node rn = nm->mkConst(CONST_RATIONAL, Rational(j)); + Node rn = nm->mkConstInt(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar(cacheVal, tn); newChildren.push_back(v); diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 9f2f9c91c..6399340aa 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -285,11 +285,10 @@ Node Skolemize::mkSkolemizedBody(Node f, } else if (options::intWfInduction() && tn.isInteger()) { - Node icond = nm->mkNode(GEQ, k, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0))); Node iret = - ret.substitute( - ind_vars[0], - nm->mkNode(MINUS, k, nm->mkConst(CONST_RATIONAL, Rational(1)))) + ret.substitute(ind_vars[0], + nm->mkNode(MINUS, k, nm->mkConstInt(Rational(1)))) .negate(); n_str_ind = nm->mkNode(OR, icond.negate(), iret); n_str_ind = nm->mkNode(AND, icond, n_str_ind); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index be80992ea..c9706b40f 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -480,7 +480,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) std::set unresolvedTypes; unresolvedTypes.insert(u); std::vector cargsEmpty; - Node cr = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node cr = nm->mkConstInt(Rational(1)); sdt.addConstructor(cr, "1", cargsEmpty); std::vector cargsPlus; cargsPlus.push_back(u); @@ -503,8 +503,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) if (pow_two > 0) { Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); - Node fair_lemma = nm->mkNode( - GEQ, size_ve, nm->mkConst(CONST_RATIONAL, Rational(pow_two - 1))); + Node fair_lemma = + nm->mkNode(GEQ, size_ve, nm->mkConstInt(Rational(pow_two - 1))); fair_lemma = nm->mkNode(OR, newLit, fair_lemma); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 674183b20..711d390f8 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -257,7 +257,7 @@ void SygusEnumerator::TermCache::initialize(SygusStatistics* s, // more aggressive merging of constructor classes. On the negative side, // this adds another level of indirection to remember which argument // positions the argument types occur in, for each constructor. - Node n = nm->mkConst(CONST_RATIONAL, Rational(i)); + Node n = nm->mkConstInt(Rational(i)); nToC[n] = i; tnit.add(n, argTypes[i]); } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 95d3a5ab5..7227b7184 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -85,11 +85,12 @@ void CegGrammarConstructor::collectTerms( Node c = cur; if (tn.isRealOrInt()) { - c = nm->mkConst(CONST_RATIONAL, c.getConst().abs()); + c = nm->mkConstRealOrInt(tn, c.getConst().abs()); } consts[tn].insert(c); if (tn.isInteger()) { + c = nm->mkConstReal(c.getConst().abs()); TypeNode rtype = nm->realType(); consts[rtype].insert(c); } @@ -410,8 +411,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, NodeManager* nm = NodeManager::currentNM(); if (type.isRealOrInt()) { - ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(0))); - ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(1))); + ops.push_back(nm->mkConstRealOrInt(type, Rational(0))); + ops.push_back(nm->mkConstRealOrInt(type, Rational(1))); } else if (type.isBitVector()) { @@ -556,7 +557,7 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( Assert(bArgType.isRealOrInt() || bArgType.isBitVector()); if (bArgType.isRealOrInt()) { - zarg = nm->mkConst(CONST_RATIONAL, Rational(0)); + zarg = nm->mkConstRealOrInt(bArgType, Rational(0)); } else { @@ -800,7 +801,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; std::vector cargsEmpty; sdts.back().addConstructor( - nm->mkConst(CONST_RATIONAL, Rational(1)), "1", cargsEmpty); + nm->mkConstInt(Rational(1)), "1", cargsEmpty); /* Add operator PLUS */ Kind kind = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; @@ -1150,7 +1151,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { const SygusDatatypeConstructor& sdc = sdti.getConstructor(k); Node sop = sdc.d_op; - bool isBuiltinArithOp = (sop.getKind() == CONST_RATIONAL); + bool isBuiltinArithOp = (sop.getType().isRealOrInt() && sop.isConst()); bool hasExternalType = false; for (unsigned j = 0, nargs = sdc.d_argTypes.size(); j < nargs; j++) { diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 89cee0145..1402c845c 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -589,14 +589,14 @@ Node SygusSampler::getRandomValue(TypeNode tn) std::vector sum; for (unsigned j = 0, size = vec.size(); j < size; j++) { - Node digit = nm->mkConst(CONST_RATIONAL, Rational(vec[j]) * curr); + Node digit = nm->mkConstInt(Rational(vec[j]) * curr); sum.push_back(digit); curr = curr * baser; } Node ret; if (sum.empty()) { - ret = nm->mkConst(CONST_RATIONAL, Rational(0)); + ret = nm->mkConstInt(Rational(0)); } else if (sum.size() == 1) { @@ -631,7 +631,7 @@ Node SygusSampler::getRandomValue(TypeNode tn) } else { - return nm->mkConst(CONST_RATIONAL, sr / rr); + return nm->mkConstReal(sr / rr); } } } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 1dfcc044e..18f9ec7e2 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -332,7 +332,7 @@ Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) if (tn.isRealOrInt()) { Rational c(val); - n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c); + n = NodeManager::currentNM()->mkConstRealOrInt(tn, c); } else if (tn.isBitVector()) { diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index e2181b4c6..7bb752acd 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -47,7 +47,7 @@ CardinalityExtension::CardinalityExtension(Env& env, d_finite_type_constants_processed(false) { d_true = NodeManager::currentNM()->mkConst(true); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); } void CardinalityExtension::reset() @@ -134,7 +134,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) if (finiteType) { Node typeCardinality = - nm->mkConst(CONST_RATIONAL, Rational(card.getFiniteCardinality())); + nm->mkConstInt(Rational(card.getFiniteCardinality())); Node cardUniv = nm->mkNode(kind::SET_CARD, proxy); Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality); @@ -980,8 +980,8 @@ void CardinalityExtension::checkMinCard() } if (!members.empty()) { - Node conc = nm->mkNode( - GEQ, cardTerm, nm->mkConst(CONST_RATIONAL, Rational(members.size()))); + Node conc = + nm->mkNode(GEQ, cardTerm, nm->mkConstInt(Rational(members.size()))); Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f06580292..a08c051f6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -59,7 +59,7 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env, { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); } TheorySetsPrivate::~TheorySetsPrivate() @@ -1289,7 +1289,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) case kind::RELATION_JOIN_IMAGE: { // these are logic exceptions, not type checking exceptions - if (node[1].getKind() != kind::CONST_RATIONAL) + if (!node[1].isConst()) { throw LogicException( "JoinImage cardinality constraint must be a constant"); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d603946c4..cb9b26731 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -272,13 +272,12 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { { if(node[0].isConst()) { std::set elements = NormalForm::getElementsFromNormalConstant(node[0]); - return RewriteResponse( - REWRITE_DONE, nm->mkConst(CONST_RATIONAL, Rational(elements.size()))); + return RewriteResponse(REWRITE_DONE, + nm->mkConstInt(Rational(elements.size()))); } else if (node[0].getKind() == kind::SET_SINGLETON) { - return RewriteResponse(REWRITE_DONE, - nm->mkConst(CONST_RATIONAL, Rational(1))); + return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(1))); } else if (node[0].getKind() == kind::SET_UNION) { diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 8eaa50354..19f1bc97d 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -32,7 +32,7 @@ namespace strings { ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); } Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); } @@ -76,11 +76,10 @@ bool ArithEntail::check(Node a, bool strict) return a.getConst().sgn() >= (strict ? 1 : 0); } - Node ar = strict ? NodeManager::currentNM()->mkNode( - kind::MINUS, - a, - NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1))) - : a; + Node ar = + strict ? NodeManager::currentNM()->mkNode( + kind::MINUS, a, NodeManager::currentNM()->mkConstInt(Rational(1))) + : a; ar = d_rr->rewrite(ar); if (ar.getAttribute(StrCheckEntailArithComputedAttr())) @@ -133,7 +132,7 @@ bool ArithEntail::checkApprox(Node ar) << "Get approximations " << v << "..." << std::endl; if (v.isNull()) { - Node mn = c.isNull() ? nm->mkConst(CONST_RATIONAL, Rational(1)) : c; + Node mn = c.isNull() ? nm->mkConstInt(Rational(1)) : c; aarSum.push_back(mn); } else @@ -496,8 +495,8 @@ void ArithEntail::getArithApproximations(Node a, { // x >= 0 implies // x+1 >= len( int.to.str( x ) ) - approx.push_back(nm->mkNode( - PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), a[0][0])); + approx.push_back( + nm->mkNode(PLUS, nm->mkConstInt(Rational(1)), a[0][0])); } } } @@ -507,7 +506,7 @@ void ArithEntail::getArithApproximations(Node a, { // x >= 0 implies // len( int.to.str( x ) ) >= 1 - approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(1))); + approx.push_back(nm->mkConstInt(Rational(1))); } // other crazy things are possible here, e.g. // len( int.to.str( len( y ) + 10 ) ) >= 2 @@ -541,7 +540,7 @@ void ArithEntail::getArithApproximations(Node a, // ...hard to test, runs risk of non-termination // -1 <= indexof( x, y, n ) - approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1))); + approx.push_back(nm->mkConstInt(Rational(-1))); } } else if (ak == STRING_STOI) @@ -556,7 +555,7 @@ void ArithEntail::getArithApproximations(Node a, else { // -1 <= str.to.int( x ) - approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1))); + approx.push_back(nm->mkConstInt(Rational(-1))); } } Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl; @@ -661,9 +660,8 @@ bool ArithEntail::checkWithAssumption(Node assumption, // (not (>= s t)) --> (>= (t - 1) s) Assert(assumption.getKind() == kind::NOT && assumption[0].getKind() == kind::GEQ); - x = nm->mkNode(kind::MINUS, - assumption[0][1], - nm->mkConst(CONST_RATIONAL, Rational(1))); + x = nm->mkNode( + kind::MINUS, assumption[0][1], nm->mkConstInt(Rational(1))); y = assumption[0][0]; } @@ -866,7 +864,7 @@ Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const if (s.isConst()) { size_t len = Word::getLength(s); - ret = nm->mkConst(CONST_RATIONAL, Rational(len)); + ret = nm->mkConstInt(Rational(len)); } else if (s.getKind() == STRING_CONCAT) { @@ -885,12 +883,12 @@ Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const success = false; break; } - Assert(b.getKind() == CONST_RATIONAL); + Assert(b.isConst()); sum = sum + b.getConst(); } if (success && (!isLower || sum.sgn() != 0)) { - ret = nm->mkConst(CONST_RATIONAL, sum); + ret = nm->mkConstInt(sum); } } if (ret.isNull() && isLower) diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index 65ff4cde4..c04bfe918 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -44,7 +44,7 @@ ArraySolver::ArraySolver(Env& env, d_eqProc(context()) { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = nm->mkConstInt(Rational(0)); } ArraySolver::~ArraySolver() {} diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 69d50a7d9..2d25a0d1e 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -604,8 +604,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, if (lr.isConst()) { // if constant, compare - Node cmp = - nm->mkNode(GEQ, lr, nm->mkConst(CONST_RATIONAL, Rational(card_need))); + Node cmp = nm->mkNode(GEQ, lr, nm->mkConstInt(Rational(card_need))); cmp = rewrite(cmp); needsSplit = !cmp.getConst(); } @@ -619,7 +618,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, bool success = true; while (r < card_need && success) { - Node rr = nm->mkConst(CONST_RATIONAL, Rational(r)); + Node rr = nm->mkConstInt(Rational(r)); if (d_state.areDisequal(rr, lr)) { r++; @@ -669,7 +668,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, << std::endl; if (int_k + 1 > ei->d_cardinalityLemK.get()) { - Node k_node = nm->mkConst(CONST_RATIONAL, Rational(int_k)); + Node k_node = nm->mkConstInt(Rational(int_k)); // add cardinality lemma Node dist = nm->mkNode(DISTINCT, cols[i]); std::vector expn; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 46f75bd10..ab214c9ce 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -50,9 +50,9 @@ CoreSolver::CoreSolver(Env& env, d_nfPairs(context()), d_extDeq(userContext()) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -776,12 +776,12 @@ Node CoreSolver::getConclusion(Node x, { // we can assume its length is greater than zero Node emp = Word::mkEmptyWord(sk1.getType()); - conc = nm->mkNode(AND, - conc, - sk1.eqNode(emp).negate(), - nm->mkNode(GT, - nm->mkNode(STRING_LENGTH, sk1), - nm->mkConst(CONST_RATIONAL, Rational(0)))); + conc = nm->mkNode( + AND, + conc, + sk1.eqNode(emp).negate(), + nm->mkNode( + GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConstInt(Rational(0)))); } } else if (rule == PfRule::CONCAT_CSPLIT) diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp index ac8e815df..0e5c19658 100644 --- a/src/theory/strings/eager_solver.cpp +++ b/src/theory/strings/eager_solver.cpp @@ -227,7 +227,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower) Assert(e != nullptr); Assert(!t.isNull()); Node tb = t.isConst() ? t : getBoundForLength(t, isLower); - Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL) + Assert(!tb.isNull() && tb.isConst() && tb.getType().isInteger()) << "Unexpected bound " << tb << " from " << t; Rational br = tb.getConst(); Node prev = isLower ? e->d_firstBound : e->d_secondBound; @@ -236,7 +236,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower) { // convert to bound Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower); - Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL); + Assert(!prevb.isNull() && prevb.isConst() && prevb.getType().isInteger()); Rational prevbr = prevb.getConst(); if (prevbr == br || (br < prevbr) == isLower) { @@ -251,7 +251,8 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower) { // are we in conflict? Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower); - Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL); + Assert(!prevob.isNull() && prevob.isConst() + && prevob.getType().isInteger()); Rational prevobr = prevob.getConst(); if (prevobr != br && (prevobr < br) == isLower) { diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index edfb91c64..81da50062 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -499,7 +499,7 @@ void InferProofCons::convert(InferenceId infer, { // it should be the case that lenConstraint => lenReq lenReq = nm->mkNode(STRING_LENGTH, t0) - .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))) + .eqNode(nm->mkConstInt(Rational(0))) .notNode(); lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); rule = PfRule::CONCAT_CSPLIT; @@ -530,7 +530,7 @@ void InferProofCons::convert(InferenceId infer, { // it should be the case that lenConstraint => lenReq lenReq = nm->mkNode(STRING_LENGTH, t0) - .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))) + .eqNode(nm->mkConstInt(Rational(0))) .notNode(); lenSuccess = convertLengthPf(lenReq, lenConstraint, psb); rule = PfRule::CONCAT_CPROP; @@ -837,7 +837,7 @@ void InferProofCons::convert(InferenceId infer, std::vector childrenAE; childrenAE.push_back(eunf); std::vector argsAE; - argsAE.push_back(nm->mkConst(CONST_RATIONAL, Rational(0))); + argsAE.push_back(nm->mkConstInt(Rational(0))); Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE); Trace("strings-ipc-prefix") << "--- and elim to " << eunfAE << std::endl; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 5247e222d..c7020869f 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -51,8 +51,8 @@ InferenceManager::InferenceManager(Env& env, : nullptr) { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); d_true = nm->mkConst(true); d_false = nm->mkConst(false); } diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index edb38e702..dc01bb6d7 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -212,8 +212,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::CONCAT_CSPLIT) { Assert(children.size() == 2); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL || children[1][0][0].getKind() != STRING_LENGTH || children[1][0][0][0] != t0 || children[1][0][1] != zero) @@ -240,7 +240,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, else if (id == PfRule::CONCAT_CPROP) { Assert(children.size() == 2); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); Trace("pfcheck-strings-cprop") << "CONCAT_PROP, isRev=" << isRev << std::endl; @@ -352,7 +352,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]); return clen.eqNode(zero).notNode(); } @@ -462,7 +462,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, && args[1].getType().isStringLike()); Node c1 = nm->mkNode(STRING_TO_CODE, args[0]); Node c2 = nm->mkNode(STRING_TO_CODE, args[1]); - Node eqNegOne = c1.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))); + Node eqNegOne = c1.eqNode(nm->mkConstInt(Rational(-1))); Node deq = c1.eqNode(c2).negate(); Node eqn = args[0].eqNode(args[1]); return nm->mkNode(kind::OR, eqNegOne, deq, eqn); diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 8a96e22d2..477533bee 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -98,7 +98,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node x = atom[0]; Node lenx = nm->mkNode(STRING_LENGTH, x); Node re = atom[1]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); std::vector children; utils::getConcat(re, children); @@ -252,10 +252,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) if (gap_minsize[i] > 0) { // the gap to this child is at least gap_minsize[i] - prev_end = - nm->mkNode(PLUS, - prev_end, - nm->mkConst(CONST_RATIONAL, Rational(gap_minsize[i]))); + prev_end = nm->mkNode( + PLUS, prev_end, nm->mkConstInt(Rational(gap_minsize[i]))); } prev_ends.push_back(prev_end); Node sc = sep_children[i]; @@ -280,8 +278,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } // if the gap after this one is strict, we need a non-greedy find // thus, we add a symbolic constant - Node cacheVal = BoundVarManager::getCacheValue( - atom, nm->mkConst(CONST_RATIONAL, Rational(i))); + Node cacheVal = + BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i))); TypeNode intType = nm->integerType(); Node k = bvm->mkBoundVar(cacheVal, intType); @@ -289,8 +287,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) prev_end = nm->mkNode(PLUS, prev_end, k); } Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end); - Node idofFind = - curr.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))).negate(); + Node idofFind = curr.eqNode(nm->mkConstInt(Rational(-1))).negate(); conj.push_back(idofFind); prev_end = nm->mkNode(PLUS, curr, lensc); } @@ -305,7 +302,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // then the last indexof/substr constraint entails the following // constraint, so it is not necessary to add. // Below, we may write "A" for (str.to.re "A") and _ for re.allchar: - Node cEnd = nm->mkConst(CONST_RATIONAL, Rational(gap_minsize_end)); + Node cEnd = nm->mkConstInt(Rational(gap_minsize_end)); if (gap_exact_end) { Assert(!sep_children.empty()); @@ -477,8 +474,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) } else { - Node cacheVal = BoundVarManager::getCacheValue( - atom, nm->mkConst(CONST_RATIONAL, Rational(i))); + Node cacheVal = + BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i))); TypeNode intType = nm->integerType(); k = bvm->mkBoundVar(cacheVal, intType); Node bound = @@ -541,7 +538,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) Node x = atom[0]; Node lenx = nm->mkNode(STRING_LENGTH, x); Node re = atom[1]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); // for regular expression star, // if the period is a fixed constant, we can turn it into a bounded // quantifier @@ -561,8 +558,8 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) std::vector char_constraints; TypeNode intType = nm->integerType(); Node index = bvm->mkBoundVar(atom, intType); - Node substr_ch = nm->mkNode( - STRING_SUBSTR, x, index, nm->mkConst(CONST_RATIONAL, Rational(1))); + Node substr_ch = + nm->mkNode(STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1))); substr_ch = Rewriter::rewrite(substr_ch); // handle the case where it is purely characters for (const Node& r : disj) diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 645dc05cd..4c4540366 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -584,7 +584,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, } else { - Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(u - 1)); + Node num2 = nm->mkConstInt(cvc5::Rational(u - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -616,7 +616,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s, cvc5::String t = s.substr(index_start, len); if (testConstStringInRegExp(t, 0, r[0])) { - Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(l - 1)); + Node num2 = nm->mkConstInt(cvc5::Rational(l - 1)); Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2); if (testConstStringInRegExp(s, index_start + len, r2)) { @@ -668,7 +668,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) } else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE) { - return nm->mkConst(CONST_RATIONAL, Rational(1)); + return nm->mkConstInt(Rational(1)); } else if (k == REGEXP_UNION || k == REGEXP_INTER) { diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a7ba37b18..eb6d2d355 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -37,10 +37,8 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc) d_false(NodeManager::currentNM()->mkConst(false)), d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE, std::vector{})), - d_zero(NodeManager::currentNM()->mkConst(CONST_RATIONAL, - ::cvc5::Rational(0))), - d_one(NodeManager::currentNM()->mkConst(CONST_RATIONAL, - ::cvc5::Rational(1))), + d_zero(NodeManager::currentNM()->mkConstInt(Rational(0))), + d_one(NodeManager::currentNM()->mkConstInt(Rational(1))), d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR, std::vector{})), d_sigma_star( @@ -911,7 +909,7 @@ Node RegExpOpr::reduceRegExpNeg(Node mem) Node r = mem[0][1]; NodeManager* nm = NodeManager::currentNM(); Kind k = r.getKind(); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); Node conc; if (k == REGEXP_CONCAT) { @@ -955,7 +953,7 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index) Node r = mem[0][1]; NodeManager* nm = NodeManager::currentNM(); Assert(r.getKind() == REGEXP_CONCAT); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); // The following simplification states that // ~( s in R1 ++ R2 ++... ++ Rn ) // is equivalent to @@ -1040,7 +1038,7 @@ Node RegExpOpr::reduceRegExpPos(Node mem, } else { - Node ivalue = nm->mkConst(CONST_RATIONAL, Rational(i)); + Node ivalue = nm->mkConstInt(Rational(i)); Node sk = sm->mkSkolemFunction(SkolemFunId::RE_UNFOLD_POS_COMPONENT, s.getType(), {mem[0], mem[1], ivalue}); @@ -1321,10 +1319,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > rt = itr2->second; } else { std::map< PairNodes, Node > cache2(cache); - cache2[p] = NodeManager::currentNM()->mkNode( - kind::REGEXP_RV, - NodeManager::currentNM()->mkConst(CONST_RATIONAL, - cvc5::Rational(cnt))); + cache2[p] = + nm->mkNode(kind::REGEXP_RV, nm->mkConstInt(Rational(cnt))); rt = intersectInternal(r1l, r2l, cache2, cnt+1); cacheX[ pp ] = rt; } diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1d82f9abd..7670c0b70 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -352,7 +352,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) } else if (ne.getKind() == STRING_SUBSTR) { - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); if (d_arithEntail.check(ne[1], false) && d_arithEntail.check(ne[2], true)) @@ -586,8 +586,7 @@ Node SequencesRewriter::rewriteLength(Node node) Kind nk0 = node[0].getKind(); if (node[0].isConst()) { - Node retNode = - nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(node[0]))); + Node retNode = nm->mkConstInt(Rational(Word::getLength(node[0]))); return returnRewrite(node, retNode, Rewrite::LEN_EVAL); } else if (nk0 == kind::STRING_CONCAT) @@ -600,8 +599,8 @@ Node SequencesRewriter::rewriteLength(Node node) { if (tmpNode[i].isConst()) { - node_vec.push_back(nm->mkConst( - CONST_RATIONAL, Rational(Word::getLength(tmpNode[i])))); + node_vec.push_back( + nm->mkConstInt(Rational(Word::getLength(tmpNode[i])))); } else { @@ -634,7 +633,7 @@ Node SequencesRewriter::rewriteLength(Node node) } else if (nk0 == SEQ_UNIT) { - Node retNode = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node retNode = nm->mkConstInt(Rational(1)); return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT); } return node; @@ -1311,7 +1310,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) } else if (r.getKind() == kind::REGEXP_ALLCHAR) { - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA); } @@ -1344,7 +1343,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]); if (!flr.isNull()) { - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); if (flr == one) { NodeBuilder nb(AND); @@ -1430,7 +1429,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) if (constStr.isNull()) { // x in re.++(_*, _, _) ---> str.len(x) >= 2 - Node num = nm->mkConst(CONST_RATIONAL, Rational(allSigmaMinSize)); + Node num = nm->mkConstInt(Rational(allSigmaMinSize)); Node lenx = nm->mkNode(STRING_LENGTH, x); Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR); @@ -1722,10 +1721,9 @@ TrustNode SequencesRewriter::expandDefinition(Node node) Node s = node[0]; Node n = node[1]; // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n)) - Node cond = - nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), n), - nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); + Node cond = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n), + nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n); Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf"); Node u = nm->mkNode(APPLY_UF, uf, s, n); @@ -1776,7 +1774,7 @@ Node SequencesRewriter::rewriteCharAt(Node node) { Assert(node.getKind() == STRING_CHARAT); NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one); return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM); } @@ -1854,7 +1852,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } } - Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0)); + Node zero = nm->mkConstInt(cvc5::Rational(0)); // if entailed non-positive length or negative start point if (d_arithEntail.check(zero, node[1], true)) @@ -2453,7 +2451,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (node[2].isConst() && node[2].getConst().sgn() < 0) { // z<0 implies str.indexof( x, y, z ) --> -1 - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NEG); } @@ -2471,7 +2469,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than // rMaxInt is guaranteed to be out of bounds. - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_MAX); } Assert(node[2].getConst().sgn() >= 0); @@ -2482,13 +2480,12 @@ Node SequencesRewriter::rewriteIndexof(Node node) std::size_t ret = Word::find(s, t, start); if (ret != std::string::npos) { - Node retv = - nm->mkConst(CONST_RATIONAL, Rational(static_cast(ret))); + Node retv = nm->mkConstInt(Rational(static_cast(ret))); return returnRewrite(node, retv, Rewrite::IDOF_FIND); } else if (children0.size() == 1) { - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NFIND); } } @@ -2500,14 +2497,14 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (node[2].getConst().sgn() == 0) { // indexof( x, x, 0 ) --> 0 - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START); } } if (d_arithEntail.check(node[2], true)) { // y>0 implies indexof( x, x, y ) --> -1 - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART); } Node emp = Word::mkEmptyWord(stype); @@ -2538,7 +2535,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (d_arithEntail.check(len1, len0m2, true)) { // len(x)-z < len(y) implies indexof( x, y, z ) ----> -1 - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_LEN); } @@ -2620,7 +2617,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) else { // str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1 - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NCTN); } } @@ -2675,12 +2672,12 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) Node s = node[0]; Node r = node[1]; Node n = node[2]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); Node slen = nm->mkNode(STRING_LENGTH, s); if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true)) { - Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node ret = nm->mkConstInt(Rational(-1)); return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX); } @@ -2695,15 +2692,14 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than // rMaxInt is guaranteed to be out of bounds. - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::INDEXOF_RE_MAX_INDEX); } uint32_t start = nrat.getNumerator().toUnsignedInt(); Node rem = nm->mkConst(s.getConst().substr(start)); std::pair match = firstMatch(rem, r); - Node ret = nm->mkConst( - CONST_RATIONAL, + Node ret = nm->mkConstInt( Rational(match.first == string::npos ? -1 : static_cast(start + match.first))); @@ -2967,8 +2963,8 @@ Node SequencesRewriter::rewriteReplace(Node node) nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype)); Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]); Node len0_1 = nm->mkNode(kind::PLUS, len0, one); // Check len(t) + j > len(x) + 1 @@ -3491,8 +3487,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node val; if (isPrefix) { - val = - NodeManager::currentNM()->mkConst(CONST_RATIONAL, ::cvc5::Rational(0)); + val = NodeManager::currentNM()->mkConstInt(::cvc5::Rational(0)); } else { @@ -3527,7 +3522,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) NodeManager* nm = NodeManager::currentNM(); Node res; - if (len.getKind() == CONST_RATIONAL) + if (len.isConst()) { // c -> "A" repeated c times Rational ratLen = len.getConst(); diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index eb09ff187..03c9f9375 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -54,7 +54,7 @@ SkolemCache::SkolemCache(Rewriter* rr) : d_rr(rr) { NodeManager* nm = NodeManager::currentNM(); d_strType = nm->stringType(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = nm->mkConstInt(Rational(0)); } Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c) @@ -217,27 +217,26 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) { // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1) id = SK_SUFFIX_REM; - b = nm->mkConst(CONST_RATIONAL, Rational(1)); + b = nm->mkConstInt(Rational(1)); } else if (id == SK_ID_VC_SPT_REV) { // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1)) id = SK_PREFIX; - b = nm->mkNode(MINUS, - nm->mkNode(STRING_LENGTH, a), - nm->mkConst(CONST_RATIONAL, Rational(1))); + b = nm->mkNode( + MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1))); } else if (id == SK_ID_DC_SPT) { // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1) id = SK_PREFIX; - b = nm->mkConst(CONST_RATIONAL, Rational(1)); + b = nm->mkConstInt(Rational(1)); } else if (id == SK_ID_DC_SPT_REM) { // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1) id = SK_SUFFIX_REM; - b = nm->mkConst(CONST_RATIONAL, Rational(1)); + b = nm->mkConstInt(Rational(1)); } else if (id == SK_ID_DEQ_X) { diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 045347cbb..6b7fc699b 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -34,7 +34,7 @@ SolverState::SolverState(Env& env, Valuation& v) d_pendingConflictSet(env.getContext(), false), d_pendingConflict(InferenceId::UNKNOWN) { - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 6e4ba25a5..952a1a36b 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -123,7 +123,7 @@ bool StringsEntail::stripSymbolicLength(std::vector& n1, Assert(dir == 1 || dir == -1); Assert(nr.empty()); NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0)); + Node zero = nm->mkConstInt(cvc5::Rational(0)); bool ret = false; bool success = true; unsigned sindex = 0; @@ -145,7 +145,7 @@ bool StringsEntail::stripSymbolicLength(std::vector& n1, Assert(d_arithEntail.check(curr, true)); Node s = n1[sindex_use]; size_t slen = Word::getLength(s); - Node ncl = nm->mkConst(CONST_RATIONAL, cvc5::Rational(slen)); + Node ncl = nm->mkConstInt(cvc5::Rational(slen)); Node next_s = nm->mkNode(MINUS, lowerBound, ncl); next_s = d_rr->rewrite(next_s); Assert(next_s.isConst()); @@ -461,7 +461,7 @@ bool StringsEntail::componentContainsBase( { n1rb = nm->mkNode(STRING_SUBSTR, n2[0], - nm->mkConst(CONST_RATIONAL, Rational(0)), + nm->mkConstInt(Rational(0)), start_pos); } if (dir != 1) @@ -714,7 +714,7 @@ bool StringsEntail::checkNonEmpty(Node a) bool StringsEntail::checkLengthOne(Node s, bool strict) { NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node len = nm->mkNode(STRING_LENGTH, s); len = d_rr->rewrite(len); return d_arithEntail.check(one, len) diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index 2951c86a2..a3ae03099 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -85,8 +85,7 @@ Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i) return Node::null(); } NodeManager* nm = NodeManager::currentNM(); - Node lit = nm->mkNode( - LEQ, d_inputVarLsum.get(), nm->mkConst(CONST_RATIONAL, Rational(i))); + Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConstInt(Rational(i))); Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl; return lit; } diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index e4b91d4d8..2ff7598b5 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -100,11 +100,11 @@ Node StringsRewriter::rewriteStrToInt(Node node) String s = node[0].getConst(); if (s.isNumber()) { - ret = nm->mkConst(CONST_RATIONAL, s.toNumber()); + ret = nm->mkConstInt(s.toNumber()); } else { - ret = nm->mkConst(CONST_RATIONAL, Rational(-1)); + ret = nm->mkConstInt(Rational(-1)); } return returnRewrite(node, ret, Rewrite::STOI_EVAL); } @@ -117,7 +117,7 @@ Node StringsRewriter::rewriteStrToInt(Node node) String t = nc.getConst(); if (!t.isNumber()) { - Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node ret = nm->mkConstInt(Rational(-1)); return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM); } } @@ -303,11 +303,11 @@ Node StringsRewriter::rewriteStringToCode(Node n) { std::vector vec = s.getVec(); Assert(vec.size() == 1); - ret = nm->mkConst(CONST_RATIONAL, Rational(vec[0])); + ret = nm->mkConstInt(Rational(vec[0])); } else { - ret = nm->mkConst(CONST_RATIONAL, Rational(-1)); + ret = nm->mkConstInt(Rational(-1)); } return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL); } @@ -320,10 +320,9 @@ Node StringsRewriter::rewriteStringIsDigit(Node n) NodeManager* nm = NodeManager::currentNM(); // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57 Node t = nm->mkNode(STRING_TO_CODE, n[0]); - Node retNode = - nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(48)), t), - nm->mkNode(LEQ, t, nm->mkConst(CONST_RATIONAL, Rational(57)))); + Node retNode = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstInt(Rational(48)), t), + nm->mkNode(LEQ, t, nm->mkConstInt(Rational(57)))); return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM); } diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 85027370e..d2d723276 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -60,9 +60,9 @@ TermRegistry::TermRegistry(Env& env, : nullptr) { NodeManager* nm = NodeManager::currentNM(); - d_zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - d_one = nm->mkConst(CONST_RATIONAL, Rational(1)); - d_negOne = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1)); + d_zero = nm->mkConstInt(Rational(0)); + d_one = nm->mkConstInt(Rational(1)); + d_negOne = NodeManager::currentNM()->mkConstInt(Rational(-1)); Assert(options().strings.stringsAlphaCard <= String::num_codes()); d_alphaCard = options().strings.stringsAlphaCard; } @@ -81,13 +81,12 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) if (tk == STRING_TO_CODE) { // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) - Node code_len = - utils::mkNLength(t[0]).eqNode(nm->mkConst(CONST_RATIONAL, Rational(1))); - Node code_eq_neg1 = t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))); - Node code_range = nm->mkNode( - AND, - nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(0))), - nm->mkNode(LT, t, nm->mkConst(CONST_RATIONAL, Rational(alphaCard)))); + Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConstInt(Rational(1))); + Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1))); + Node code_range = + nm->mkNode(AND, + nm->mkNode(GEQ, t, nm->mkConstInt(Rational(0))), + nm->mkNode(LT, t, nm->mkConstInt(Rational(alphaCard)))); lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); } else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE) @@ -98,17 +97,16 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) // // where f in { str.indexof, str.indexof_re } Node l = nm->mkNode(STRING_LENGTH, t[0]); - lemma = nm->mkNode( - AND, - nm->mkNode(OR, - t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))), - nm->mkNode(GEQ, t, t[2])), - nm->mkNode(LEQ, t, l)); + lemma = nm->mkNode(AND, + nm->mkNode(OR, + t.eqNode(nm->mkConstInt(Rational(-1))), + nm->mkNode(GEQ, t, t[2])), + nm->mkNode(LEQ, t, l)); } else if (tk == STRING_STOI) { // (>= (str.to_int x) (- 1)) - lemma = nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(-1))); + lemma = nm->mkNode(GEQ, t, nm->mkConstInt(Rational(-1))); } else if (tk == STRING_CONTAINS) { @@ -126,7 +124,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) Node TermRegistry::lengthPositive(Node t) { NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); Node emp = Word::mkEmptyWord(t.getType()); Node tlen = nm->mkNode(STRING_LENGTH, t); Node tlenEqZero = tlen.eqNode(zero); @@ -416,7 +414,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) } else if (n.isConst()) { - lsum = nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(n))); + lsum = nm->mkConstInt(Rational(Word::getLength(n))); } Assert(!lsum.isNull()); d_proxyVarToLength[sk] = lsum; @@ -486,7 +484,7 @@ bool TermRegistry::isHandledUpdate(Node n) { lenN = nm->mkNode(STRING_LENGTH, n[2]); } - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); return d_aent.checkEq(lenN, one); } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4ed754b16..8b496b725 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -84,9 +84,9 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) { d_termReg.finishInit(&d_im); - d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); - d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1)); + d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); + d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1)); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -425,7 +425,7 @@ bool TheoryStrings::collectModelInfoType( lvalue++; } Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl; - lts_values[i] = nm->mkConst(CONST_RATIONAL, Rational(lvalue)); + lts_values[i] = nm->mkConstInt(Rational(lvalue)); values_used[lvalue] = Node::null(); } Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; @@ -1071,8 +1071,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) SkolemCache* sc = d_termReg.getSkolemCache(); Node k = sc->mkSkolemCached(atom, SkolemCache::SK_PURIFY, "kFromCode"); Node t = atom[0]; - Node card = nm->mkConst(CONST_RATIONAL, - Rational(d_termReg.getAlphabetCardinality())); + Node card = nm->mkConstInt(Rational(d_termReg.getAlphabetCardinality())); Node cond = nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card)); Node emp = Word::mkEmptyWord(atom.getType()); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4f27371ff..4c2319b4e 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -53,9 +53,9 @@ Node StringsPreprocess::reduce(Node t, << "StringsPreprocess::reduce: " << t << std::endl; Node retNode = t; NodeManager* nm = NodeManager::currentNM(); - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); - Node negOne = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); + Node negOne = nm->mkConstInt(Rational(-1)); if( t.getKind() == kind::STRING_SUBSTR ) { // processing term: substr( s, n, m ) @@ -184,7 +184,7 @@ Node StringsPreprocess::reduce(Node t, Node skk = sc->mkTypedSkolemCached( nm->integerType(), t, SkolemCache::SK_PURIFY, "iok"); - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); // substr( x, n, len( x ) - n ) Node st = nm->mkNode(STRING_SUBSTR, @@ -364,7 +364,7 @@ Node StringsPreprocess::reduce(Node t, Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); - Node ten = nm->mkConst(CONST_RATIONAL, Rational(10)); + Node ten = nm->mkConstInt(Rational(10)); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); Node leadingZeroPos = nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one)); @@ -431,7 +431,7 @@ Node StringsPreprocess::reduce(Node t, MINUS, nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)), c0); - Node ten = nm->mkConst(CONST_RATIONAL, Rational(10)); + Node ten = nm->mkConstInt(Rational(10)); Node kc3 = nm->mkNode( OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten)); conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3))); @@ -865,12 +865,11 @@ Node StringsPreprocess::reduce(Node t, Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one)); Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one)); - Node lb = nm->mkConst(CONST_RATIONAL, - Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); - Node ub = nm->mkConst(CONST_RATIONAL, - Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); - Node offset = nm->mkConst( - CONST_RATIONAL, Rational(t.getKind() == STRING_TOUPPER ? -32 : 32)); + Node lb = nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); + Node ub = + nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); + Node offset = + nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32)); Node res = nm->mkNode( ITE, diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index a133babba..0ee2e906d 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -165,8 +165,7 @@ Node mkNLength(Node t) Node mkPrefix(Node t, Node n) { NodeManager* nm = NodeManager::currentNM(); - return nm->mkNode( - STRING_SUBSTR, t, nm->mkConst(CONST_RATIONAL, Rational(0)), n); + return nm->mkNode(STRING_SUBSTR, t, nm->mkConstInt(Rational(0)), n); } Node mkSuffix(Node t, Node n)