From 2b364e03e54e06ca00b47812b7abbcedb6165409 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 May 2022 21:36:33 -0500 Subject: [PATCH] Final preparation for CONST_INTEGER (#8700) With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL. This does not make this change yet, so CONST_RATIONAL is still used throughout. --- src/api/cpp/cvc5.cpp | 15 +- src/expr/node_manager_template.cpp | 1 + src/theory/arith/arith_poly_norm.cpp | 7 +- src/theory/arith/arith_rewriter.cpp | 74 ++-- src/theory/arith/arith_rewriter.h | 11 - src/theory/arith/arith_utilities.h | 4 - src/theory/arith/linear/normal_form.cpp | 6 +- .../arith/linear/theory_arith_private.cpp | 20 +- src/theory/arith/rewriter/node_utils.cpp | 31 ++ src/theory/arith/rewriter/node_utils.h | 12 + test/unit/node/node_algorithm_black.cpp | 4 +- test/unit/node/node_black.cpp | 10 +- test/unit/node/node_manager_black.cpp | 2 +- test/unit/node/node_manager_white.cpp | 4 +- test/unit/node/node_white.cpp | 2 +- test/unit/node/type_node_white.cpp | 4 +- .../pass_foreign_theory_rewrite_white.cpp | 2 +- test/unit/theory/arith_poly_white.cpp | 14 +- test/unit/theory/evaluator_white.cpp | 8 +- test/unit/theory/sequences_rewriter_white.cpp | 64 ++-- .../theory/theory_arith_coverings_white.cpp | 23 +- test/unit/theory/theory_arith_pow2_white.cpp | 4 - .../theory/theory_arith_rewriter_black.cpp | 6 +- test/unit/theory/theory_arith_white.cpp | 8 +- .../theory/theory_bags_normal_form_white.cpp | 319 +++++++----------- .../theory/theory_bags_rewriter_white.cpp | 205 +++++------ .../theory/theory_bags_type_rules_white.cpp | 53 ++- test/unit/theory/theory_black.cpp | 4 +- .../theory/theory_bv_int_blaster_white.cpp | 6 +- test/unit/theory/theory_engine_white.cpp | 6 +- test/unit/theory/theory_int_opt_white.cpp | 18 +- .../theory/theory_sets_rewriter_white.cpp | 2 +- .../theory_strings_skolem_cache_black.cpp | 2 +- test/unit/theory/type_enumerator_white.cpp | 130 +++---- test/unit/util/array_store_all_white.cpp | 28 +- test/unit/util/datatype_black.cpp | 2 +- 36 files changed, 477 insertions(+), 634 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b5f0d463a..d1146649b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2608,6 +2608,7 @@ const internal::Rational& getRational(const internal::Node& node) { case internal::Kind::CAST_TO_REAL: return node[0].getConst(); + case internal::Kind::CONST_INTEGER: case internal::Kind::CONST_RATIONAL: return node.getConst(); default: @@ -2639,6 +2640,7 @@ bool checkReal64Bounds(const internal::Rational& r) bool isReal(const internal::Node& node) { return node.getKind() == internal::Kind::CONST_RATIONAL + || node.getKind() == internal::Kind::CONST_INTEGER || node.getKind() == internal::Kind::CAST_TO_REAL; } bool isReal32(const internal::Node& node) @@ -2652,7 +2654,8 @@ bool isReal64(const internal::Node& node) bool isInteger(const internal::Node& node) { - return node.getKind() == internal::Kind::CONST_RATIONAL + return (node.getKind() == internal::Kind::CONST_RATIONAL + || node.getKind() == internal::Kind::CONST_INTEGER) && node.getConst().isIntegral(); } bool isInt32(const internal::Node& node) @@ -5242,12 +5245,10 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const // constructors. We do this cast using division with 1. This has the // advantage wrt using TO_REAL since (constant) division is always included // in the theory. - res = Term( - this, - d_nodeMgr->mkNode(extToIntKind(DIVISION), - *res.d_node, - d_nodeMgr->mkConst(internal::kind::CONST_RATIONAL, - internal::Rational(1)))); + res = Term(this, + d_nodeMgr->mkNode(extToIntKind(DIVISION), + *res.d_node, + d_nodeMgr->mkConstInt(internal::Rational(1)))); } Assert(res.getSort() == sort); return res; diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index c27679b4f..dad48ba1f 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1304,6 +1304,7 @@ Node NodeManager::mkNode(TNode opNode, std::initializer_list children) Node NodeManager::mkConstReal(const Rational& r) { + // works with (r.isIntegral() ? kind::CONST_INTEGER : kind::CONST_RATIONAL) return mkConst(kind::CONST_RATIONAL, r); } diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp index 6da9653e4..2226e94fc 100644 --- a/src/theory/arith/arith_poly_norm.cpp +++ b/src/theory/arith/arith_poly_norm.cpp @@ -158,7 +158,7 @@ std::vector PolyNorm::getMonoVars(TNode m) if (!m.isNull()) { Kind k = m.getKind(); - Assert(k != CONST_RATIONAL); + Assert(k != CONST_RATIONAL && k != CONST_INTEGER); if (k == MULT || k == NONLINEAR_MULT) { vars.insert(vars.end(), m.begin(), m.end()); @@ -188,7 +188,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) Kind k = cur.getKind(); if (it == visited.end()) { - if (k == CONST_RATIONAL) + if (k == CONST_RATIONAL || k == CONST_INTEGER) { Rational r = cur.getConst(); if (r.sgn() == 0) @@ -247,7 +247,8 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n) } } break; - case CONST_RATIONAL: break; + case CONST_RATIONAL: + case CONST_INTEGER: break; default: Unhandled() << "Unhandled polynomial operation " << cur; break; } } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 8920c51aa..502b528b1 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -152,8 +152,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom) } // left |><| right Kind kind = atom.getKind(); - Node left = removeToReal(atom[0]); - Node right = removeToReal(atom[1]); + Node left = rewriter::removeToReal(atom[0]); + Node right = rewriter::removeToReal(atom[1]); if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right); response) @@ -441,7 +441,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t) rewriter::addToSum(sum, child); } Node retSum = rewriter::collectSum(sum); - retSum = maybeEnsureReal(t.getType(), retSum); + retSum = rewriter::maybeEnsureReal(t.getType(), retSum); return RewriteResponse(REWRITE_DONE, retSum); } @@ -452,7 +452,8 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode node) if (auto res = rewriter::getZeroChild(node); res) { - return RewriteResponse(REWRITE_DONE, maybeEnsureReal(node.getType(), *res)); + return RewriteResponse(REWRITE_DONE, + rewriter::maybeEnsureReal(node.getType(), *res)); } return RewriteResponse(REWRITE_DONE, node); } @@ -466,7 +467,8 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ if (auto res = rewriter::getZeroChild(children); res) { - return RewriteResponse(REWRITE_DONE, maybeEnsureReal(t.getType(), *res)); + return RewriteResponse(REWRITE_DONE, + rewriter::maybeEnsureReal(t.getType(), *res)); } Node ret; @@ -489,7 +491,7 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ if (child.getConst().isZero()) { return RewriteResponse(REWRITE_DONE, - maybeEnsureReal(t.getType(), child)); + rewriter::maybeEnsureReal(t.getType(), child)); } ran *= child.getConst(); } @@ -504,7 +506,7 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ } ret = rewriter::mkMultTerm(ran, std::move(leafs)); } - ret = maybeEnsureReal(t.getType(), ret); + ret = rewriter::maybeEnsureReal(t.getType(), ret); return RewriteResponse(REWRITE_DONE, ret); } @@ -513,8 +515,8 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION); Assert(t.getNumChildren() == 2); - Node left = removeToReal(t[0]); - Node right = removeToReal(t[1]); + Node left = rewriter::removeToReal(t[0]); + Node right = rewriter::removeToReal(t[1]); NodeManager* nm = NodeManager::currentNM(); if (right.isConst()) { @@ -547,8 +549,8 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) } Node result = nm->mkConstReal(den.inverse()); - Node mult = - ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result)); + Node mult = rewriter::ensureReal( + NodeManager::currentNM()->mkNode(kind::MULT, left, result)); if (pre) { return RewriteResponse(REWRITE_DONE, mult); @@ -562,20 +564,20 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre) // mkConst is applied to RAN in this block, which are always Real if (left.isConst()) { - return RewriteResponse( - REWRITE_DONE, - ensureReal(rewriter::mkConst(left.getConst() / den))); + return RewriteResponse(REWRITE_DONE, + rewriter::ensureReal(rewriter::mkConst( + left.getConst() / den))); } if (rewriter::isRAN(left)) { - return RewriteResponse( - REWRITE_DONE, - ensureReal(rewriter::mkConst(rewriter::getRAN(left) / den))); + return RewriteResponse(REWRITE_DONE, + rewriter::ensureReal(rewriter::mkConst( + rewriter::getRAN(left) / den))); } Node result = rewriter::mkConst(inverse(den)); - Node mult = - ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result)); + Node mult = rewriter::ensureReal( + NodeManager::currentNM()->mkNode(kind::MULT, left, result)); if (pre) { return RewriteResponse(REWRITE_DONE, mult); @@ -1124,40 +1126,6 @@ TrustNode ArithRewriter::expandDefinition(Node node) return ret; } -TNode ArithRewriter::removeToReal(TNode t) -{ - return t.getKind() == kind::TO_REAL ? t[0] : t; -} - -Node ArithRewriter::maybeEnsureReal(TypeNode tn, TNode t) -{ - // if we require being a real - if (!tn.isInteger()) - { - // ensure that t has type real - Assert(tn.isReal()); - return ensureReal(t); - } - return t; -} - -Node ArithRewriter::ensureReal(TNode t) -{ - if (t.getType().isInteger()) - { - if (t.isConst()) - { - // short-circuit - Node ret = NodeManager::currentNM()->mkConstReal(t.getConst()); - Assert(ret.getType().isReal()); - return ret; - } - Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl; - return NodeManager::currentNM()->mkNode(kind::TO_REAL, t); - } - return t; -} - RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r) { Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by " diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 3da45fead..12f288d74 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -94,17 +94,6 @@ class ArithRewriter : public TheoryRewriter /** return rewrite */ static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r); - /** - * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL. - */ - static TNode removeToReal(TNode t); - /** - * Ensure that t has real type if tn is the real type. Do so by applying - * TO_REAL to t. - */ - static Node maybeEnsureReal(TypeNode tn, TNode t); - /** Same as above, without a check for the type of tn. */ - static Node ensureReal(TNode t); /** The operator elimination utility */ OperatorElim& d_opElim; }; /* class ArithRewriter */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 7f4398b9b..748703cf6 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -38,10 +38,6 @@ typedef std::unordered_set NodeSet; typedef std::unordered_set TNodeSet; typedef context::CDHashSet CDNodeSet; -inline Node mkRationalNode(const Rational& q){ - return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, q); -} - inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst(b); } diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp index ecbf10b1b..f2c1b5736 100644 --- a/src/theory/arith/linear/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -29,8 +29,10 @@ namespace cvc5::internal { namespace theory { namespace arith::linear { -Constant Constant::mkConstant(const Rational& rat) { - return Constant(mkRationalNode(rat)); +Constant Constant::mkConstant(const Rational& rat) +{ + NodeManager* nm = NodeManager::currentNM(); + return Constant(nm->mkConstReal(rat)); } size_t Variable::getComplexity() const{ diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 0458a43ec..793eb816a 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -2041,7 +2041,7 @@ Node toSumNode(const ArithVariables& vars, const DenseMap& sum){ if(!vars.hasNode(x)){ return Node::null(); } Node xNode = vars.asNode(x); const Rational& q = sum[x]; - Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode); + Node mult = nm->mkNode(kind::MULT, nm->mkConstReal(q), xNode); Trace("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl; children.push_back(mult); } @@ -4789,7 +4789,7 @@ bool TheoryArithPrivate::decomposeTerm(Node t, Polynomial poly = Polynomial::parsePolynomial(t); if(poly.isConstant()){ c = poly.getHead().getConstant().getValue(); - p = mkRationalNode(Rational(0)); + p = NodeManager::currentNM()->mkConstReal(Rational(0)); m = Rational(1); return true; }else if(poly.containsConstant()){ @@ -4838,22 +4838,6 @@ void TheoryArithPrivate::setToMin(int sgn, std::pair& min, } } -// std::pair TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ - -// Rational negRM = -rm; -// Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp); - -// Rational diffm; -// Node diffp; -// decompose(diff, diffm, diffNode); - - -// std::pair bestUbLeft, bestLbRight, bestUbDiff, tmp; -// bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational()); - -// return make_pair(false, Node::null()); -// } - /** * Decomposes a literal into the form: * dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ] diff --git a/src/theory/arith/rewriter/node_utils.cpp b/src/theory/arith/rewriter/node_utils.cpp index 3dfdff931..5285e2955 100644 --- a/src/theory/arith/rewriter/node_utils.cpp +++ b/src/theory/arith/rewriter/node_utils.cpp @@ -81,6 +81,37 @@ Node mkMultTerm(const RealAlgebraicNumber& multiplicity, return NodeManager::currentNM()->mkNode(Kind::NONLINEAR_MULT, monomial); } +TNode removeToReal(TNode t) { return t.getKind() == kind::TO_REAL ? t[0] : t; } + +Node maybeEnsureReal(TypeNode tn, TNode t) +{ + // if we require being a real + if (!tn.isInteger()) + { + // ensure that t has type real + Assert(tn.isReal()); + return ensureReal(t); + } + return t; +} + +Node ensureReal(TNode t) +{ + if (t.getType().isInteger()) + { + if (t.isConst()) + { + // short-circuit + Node ret = NodeManager::currentNM()->mkConstReal(t.getConst()); + Assert(ret.getType().isReal()); + return ret; + } + Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl; + return NodeManager::currentNM()->mkNode(kind::TO_REAL, t); + } + return t; +} + } // namespace rewriter } // namespace arith } // namespace theory diff --git a/src/theory/arith/rewriter/node_utils.h b/src/theory/arith/rewriter/node_utils.h index 54f8a1696..71476b2d2 100644 --- a/src/theory/arith/rewriter/node_utils.h +++ b/src/theory/arith/rewriter/node_utils.h @@ -144,6 +144,18 @@ Node mkMultTerm(const RealAlgebraicNumber& multiplicity, TNode monomial); Node mkMultTerm(const RealAlgebraicNumber& multiplicity, std::vector&& monomial); +/** + * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL. + */ +TNode removeToReal(TNode t); +/** + * Ensure that t has real type if tn is the real type. Do so by applying + * TO_REAL to t. + */ +Node maybeEnsureReal(TypeNode tn, TNode t); +/** Same as above, without a check for the type of tn. */ +Node ensureReal(TNode t); + } // namespace rewriter } // namespace arith } // namespace theory diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index 6c6ce1fe3..388e2e438 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -140,8 +140,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) { TypeNode integer = d_nodeManager->integerType(); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); Node x = d_nodeManager->mkBoundVar(integer); Node a = d_skolemManager->mkDummySkolem("a", integer); diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 039d591cd..f0e8d0be8 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -737,15 +737,15 @@ TEST_F(TestNodeBlackNode, isConst) Node cons_1_nil = d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), + d_nodeManager->mkConstInt(Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); Node cons_1_cons_2_nil = d_nodeManager->mkNode( APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), + d_nodeManager->mkConstInt(Rational(1)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)), + d_nodeManager->mkConstInt(Rational(2)), d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); ASSERT_FALSE(cons_x_nil.isConst()); @@ -754,8 +754,8 @@ TEST_F(TestNodeBlackNode, isConst) TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); ASSERT_TRUE(storeAll.isConst()); diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index ec0ee24f9..371bef1f0 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -140,7 +140,7 @@ TEST_F(TestNodeBlackNodeManager, mkConst_bool) TEST_F(TestNodeBlackNodeManager, mkConst_rational) { Rational r("3/2"); - Node n = d_nodeManager->mkConst(CONST_RATIONAL, r); + Node n = d_nodeManager->mkConstReal(r); ASSERT_EQ(n.getConst(), r); } diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index c90625175..2c455a5dc 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -34,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode TEST_F(TestNodeWhiteNodeManager, mkConst_rational) { Rational i("3"); - Node n = d_nodeManager->mkConst(CONST_RATIONAL, i); - Node m = d_nodeManager->mkConst(CONST_RATIONAL, i); + Node n = d_nodeManager->mkConstInt(i); + Node m = d_nodeManager->mkConstInt(i); ASSERT_EQ(n.getId(), m.getId()); } diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index edc9a2855..3ace15512 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -49,7 +49,7 @@ TEST_F(TestNodeWhiteNode, iterators) Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); Node x_plus_y = d_nodeManager->mkNode(ADD, x, y); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node two = d_nodeManager->mkConstInt(Rational(2)); Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); Node n = d_nodeManager->mkNode(ADD, x_times_2, x_plus_y, y); diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 83e74e078..b2a349ca0 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -50,8 +50,8 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) TypeNode bvType = d_nodeManager->mkBitVectorType(32); Node x = d_nodeManager->mkBoundVar("x", realType); - Node xPos = d_nodeManager->mkNode( - GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + Node xPos = + d_nodeManager->mkNode(GT, x, d_nodeManager->mkConstInt(Rational(0))); TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType); Node lambda = d_nodeManager->mkVar("lambda", funtype); std::vector formals; diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index e4e6c35f7..84d6e8e3f 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -35,7 +35,7 @@ TEST_F(TestPPWhiteForeignTheoryRewrite, simplify) std::cout << "len(x) >= 0 is simplified to true" << std::endl; Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType()); Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, 0); + Node zero = d_nodeManager->mkConstInt(0); Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero); Node tt = d_nodeManager->mkConst(true); Node simplified1 = ftr.foreignRewrite(geq1); diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp index 4162ba611..44d3f39bb 100644 --- a/test/unit/theory/arith_poly_white.cpp +++ b/test/unit/theory/arith_poly_white.cpp @@ -40,9 +40,9 @@ class TestTheoryWhiteArithPolyNorm : public TestSmt TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) { TypeNode intType = d_nodeManager->integerType(); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node zero = d_nodeManager->mkConstReal(Rational(0)); + Node one = d_nodeManager->mkConstReal(Rational(1)); + Node two = d_nodeManager->mkConstReal(Rational(2)); Node x = d_nodeManager->mkVar("x", intType); Node y = d_nodeManager->mkVar("y", intType); Node z = d_nodeManager->mkVar("z", intType); @@ -101,10 +101,10 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real) { TypeNode realType = d_nodeManager->realType(); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node half = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node zero = d_nodeManager->mkConstReal(Rational(0)); + Node one = d_nodeManager->mkConstReal(Rational(1)); + Node half = d_nodeManager->mkConstReal(Rational(1) / Rational(2)); + Node two = d_nodeManager->mkConstReal(Rational(2)); Node x = d_nodeManager->mkVar("x", realType); Node y = d_nodeManager->mkVar("y", realType); diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index 06106de2c..5d480c7d4 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -103,8 +103,8 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf) { Node a = d_nodeManager->mkConst(String("A")); Node empty = d_nodeManager->mkConst(String("")); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); std::vector args; std::vector vals; @@ -150,14 +150,14 @@ TEST_F(TestTheoryWhiteEvaluator, code) { Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a); Node r = eval.eval(n, args, vals); - ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(65))); + ASSERT_EQ(r, d_nodeManager->mkConstInt(Rational(65))); } // (str.code "") ---> -1 { Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty); Node r = eval.eval(n, args, vals); - ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); + ASSERT_EQ(r, d_nodeManager->mkConstInt(Rational(-1))); } } } // namespace test diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 04c7d2502..e480db6ca 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -94,11 +94,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one) Node b = d_nodeManager->mkConst(String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); - Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node negOne = d_nodeManager->mkConstInt(Rational(-1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); + Node three = d_nodeManager->mkConstInt(Rational(3)); Node i = d_nodeManager->mkVar("i", intType); ASSERT_TRUE(se.checkLengthOne(a)); @@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith) Node z = d_nodeManager->mkVar("z", strType); Node n = d_nodeManager->mkVar("n", intType); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); // 1 >= (str.len (str.substr z n 1)) ---> true Node substr_z = d_nodeManager->mkNode( @@ -151,8 +151,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", intType); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node empty = d_nodeManager->mkConst(String("")); Node a = d_nodeManager->mkConst(String("A")); @@ -185,8 +185,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) ASSERT_TRUE(ae.checkWithAssumption( x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); - Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); - Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6)); + Node five = d_nodeManager->mkConstInt(Rational(5)); + Node six = d_nodeManager->mkConstInt(Rational(6)); Node x_plus_five = d_nodeManager->mkNode(kind::ADD, x, five); Node x_plus_five_lt_six = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six)); @@ -292,11 +292,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) Node a = d_nodeManager->mkConst(String("A")); Node b = d_nodeManager->mkConst(String("B")); Node abcd = d_nodeManager->mkConst(String("ABCD")); - Node negone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node negone = d_nodeManager->mkConstInt(Rational(-1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); + Node three = d_nodeManager->mkConstInt(Rational(3)); Node s = d_nodeManager->mkVar("s", strType); Node s2 = d_nodeManager->mkVar("s2", strType); @@ -313,7 +313,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) kind::STRING_SUBSTR, a, d_nodeManager->mkNode( - kind::ADD, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))), + kind::ADD, x, d_nodeManager->mkConstInt(Rational(1))), x); sameNormalForm(n, empty); @@ -532,8 +532,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) Node empty = d_nodeManager->mkConst(String("")); Node a = d_nodeManager->mkConst(String("A")); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node three = d_nodeManager->mkConstInt(Rational(3)); Node i = d_nodeManager->mkVar("i", intType); Node s = d_nodeManager->mkVar("s", strType); @@ -639,11 +639,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) Node ccc = d_nodeManager->mkConst(String("CCC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); - Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node negOne = d_nodeManager->mkConstInt(Rational(-1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); + Node three = d_nodeManager->mkConstInt(Rational(3)); Node i = d_nodeManager->mkVar("i", intType); Node j = d_nodeManager->mkVar("j", intType); @@ -720,8 +720,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", strType); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node n = d_nodeManager->mkVar("n", intType); // (str.replace (str.replace x "B" x) x "A") --> @@ -1141,10 +1141,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) Node z = d_nodeManager->mkVar("z", strType); Node n = d_nodeManager->mkVar("n", intType); Node m = d_nodeManager->mkVar("m", intType); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); - Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); + Node three = d_nodeManager->mkConstInt(Rational(3)); + Node four = d_nodeManager->mkConstInt(Rational(4)); Node t = d_nodeManager->mkConst(true); Node f = d_nodeManager->mkConst(false); @@ -1567,9 +1567,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a); Node f = d_nodeManager->mkConst(false); Node n = d_nodeManager->mkVar("n", intType); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node three = d_nodeManager->mkConstInt(Rational(3)); // Same normal form for: // diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index cdc8282fb..912e21147 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -205,15 +205,14 @@ TEST_F(TestTheoryWhiteArithCoverings, lazard_simp) Node a = d_nodeManager->mkVar(*d_realType); Node c = d_nodeManager->mkVar(*d_realType); Node orig = d_nodeManager->mkAnd(std::vector{ - d_nodeManager->mkNode( - Kind::EQUAL, a, d_nodeManager->mkConst(CONST_RATIONAL, d_zero)), + d_nodeManager->mkNode(Kind::EQUAL, a, d_nodeManager->mkConstReal(d_zero)), d_nodeManager->mkNode( Kind::EQUAL, d_nodeManager->mkNode( Kind::ADD, d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c), - d_nodeManager->mkConst(CONST_RATIONAL, d_one)), - d_nodeManager->mkConst(CONST_RATIONAL, d_zero))}); + d_nodeManager->mkConstReal(d_one)), + d_nodeManager->mkConstReal(d_zero))}); { Node rewritten = rewriter->rewrite(orig); @@ -426,10 +425,10 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) TEST_F(TestTheoryWhiteArithCoverings, test_delta_one) { std::vector a; - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); - Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)); + Node zero = d_nodeManager->mkConstReal(Rational(0)); + Node one = d_nodeManager->mkConstReal(Rational(1)); + Node mone = d_nodeManager->mkConstReal(Rational(-1)); + Node fifth = d_nodeManager->mkConstReal(Rational(1, 2)); Node g = make_real_variable("g"); Node l = make_real_variable("l"); Node q = make_real_variable("q"); @@ -449,10 +448,10 @@ TEST_F(TestTheoryWhiteArithCoverings, test_delta_one) TEST_F(TestTheoryWhiteArithCoverings, test_delta_two) { std::vector a; - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)); - Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)); + Node zero = d_nodeManager->mkConstReal(Rational(0)); + Node one = d_nodeManager->mkConstReal(Rational(1)); + Node mone = d_nodeManager->mkConstReal(Rational(-1)); + Node fifth = d_nodeManager->mkConstReal(Rational(1, 2)); Node g = make_real_variable("g"); Node l = make_real_variable("l"); Node q = make_real_variable("q"); diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp index 1a60682bb..05576ff68 100644 --- a/test/unit/theory/theory_arith_pow2_white.cpp +++ b/test/unit/theory/theory_arith_pow2_white.cpp @@ -36,11 +36,7 @@ class TestTheoryWhiteArithPow2 : public TestSmtNoFinishInit TestSmtNoFinishInit::SetUp(); d_slvEngine->setOption("produce-models", "true"); d_slvEngine->finishInit(); - d_true = d_nodeManager->mkConst(true); - d_one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); } - Node d_true; - Node d_one; }; } // namespace test } // namespace cvc5::internal diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp index ec6277c14..844d5f369 100644 --- a/test/unit/theory/theory_arith_rewriter_black.cpp +++ b/test/unit/theory/theory_arith_rewriter_black.cpp @@ -34,7 +34,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) { RealAlgebraicNumber two({-8, 0, 0, 1}, 1, 3); Node n = d_nodeManager->mkRealAlgebraicNumber(two); - EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL); + EXPECT_EQ(n.isConst(), true); EXPECT_EQ(n.getConst(), Rational(2)); } { @@ -51,7 +51,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); n = d_nodeManager->mkNode(Kind::MULT, n, n); n = d_slvEngine->getRewriter()->rewrite(n); - EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL); + EXPECT_EQ(n.isConst(), true); EXPECT_EQ(n.getConst(), Rational(2)); } { @@ -59,7 +59,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber) Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2); n = d_nodeManager->mkNode(Kind::SUB, n, n); n = d_slvEngine->getRewriter()->rewrite(n); - EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL); + EXPECT_EQ(n.isConst(), true); EXPECT_EQ(n.getConst(), Rational(0)); } { diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 8285c07e1..d9c8abbb7 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -68,7 +68,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteArith, assert) { Node x = d_nodeManager->mkVar(*d_realType); - Node c = d_nodeManager->mkConst(CONST_RATIONAL, d_zero); + Node c = d_nodeManager->mkConstReal(d_zero); Node gt = d_nodeManager->mkNode(GT, x, c); Node leq = Rewriter::rewrite(gt.notNode()); @@ -83,9 +83,9 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) { Node x = d_nodeManager->mkVar(*d_intType); Node xr = d_nodeManager->mkVar(*d_realType); - Node c0 = d_nodeManager->mkConst(CONST_RATIONAL, d_zero); - Node c1 = d_nodeManager->mkConst(CONST_RATIONAL, d_one); - Node c2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node c0 = d_nodeManager->mkConstReal(d_zero); + Node c1 = d_nodeManager->mkConstReal(d_one); + Node c2 = d_nodeManager->mkConstReal(Rational(2)); Node geq0 = d_nodeManager->mkNode(GEQ, x, c0); Node geq1 = d_nodeManager->mkNode(GEQ, x, c1); diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 37222a589..d144f1107 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -71,18 +71,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, empty_bag_normal_form) TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element) { std::vector elements = getNStrings(1); - Node negative = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); - Node zero = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); - Node positive = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); @@ -103,25 +100,19 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4 // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0 - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node four = d_nodeManager->mkConstInt(Rational(4)); Node empty = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node y_5 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - Node z_5 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5))); + Node z_5 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(5))); Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty); Node output1 = zero; @@ -165,23 +156,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); - Node x_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node y_5 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node x_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); + + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5))); Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4); Node output2 = x_1; @@ -208,26 +191,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node x_3 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node x_7 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); - Node z_2 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); @@ -248,18 +221,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) std::vector elements = getNStrings(3); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node B = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node C = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[2], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(2))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(3))); + Node C = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[2], + d_nodeManager->mkConstInt(Rational(4))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // unionDisjointAB is already in a normal form @@ -282,10 +252,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) ASSERT_EQ(unionDisjointA_BC, BagsUtils::evaluate(unionDisjointAB_C)); Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A); - Node AA = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(4))); ASSERT_FALSE(unionDisjointAA.isConst()); ASSERT_TRUE(AA.isConst()); ASSERT_EQ(AA, BagsUtils::evaluate(unionDisjointAA)); @@ -306,26 +275,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node x_3 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node x_7 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); - Node z_2 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); @@ -354,26 +313,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node x_3 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node x_7 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); - Node z_2 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); @@ -399,30 +348,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node x_3 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node x_7 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); - Node z_2 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); @@ -448,30 +385,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node x_3 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node x_7 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); - Node z_2 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - z, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkBag( + d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); @@ -496,27 +421,23 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_CARD, empty); - Node output1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node output1 = d_nodeManager->mkConstInt(Rational(0)); ASSERT_EQ(output1, BagsUtils::evaluate(input1)); Node input2 = d_nodeManager->mkNode(BAG_CARD, x_4); - Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); + Node output2 = d_nodeManager->mkConstInt(Rational(4)); ASSERT_EQ(output2, BagsUtils::evaluate(input2)); Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1); Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint); - Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); + Node output3 = d_nodeManager->mkConstInt(Rational(5)); ASSERT_EQ(output3, BagsUtils::evaluate(input3)); } @@ -536,18 +457,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty); Node output1 = falseNode; @@ -590,14 +505,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); - Node x_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node y_1 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node x_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); + Node y_1 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton); Node output2 = x_1; @@ -633,14 +544,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); - Node x_4 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node y_5 = - d_nodeManager->mkBag(d_nodeManager->stringType(), - y, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node x_4 = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkBag( + d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5))); Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4); Node output2 = xSingleton; diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 121d26171..934649755 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -78,7 +78,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) Node constantBag = d_nodeManager->mkBag(d_nodeManager->stringType(), emptyString, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + d_nodeManager->mkConstInt(Rational(1))); // (= A A) = true where A is a bag Node n1 = A.eqNode(A); @@ -107,18 +107,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element) { std::vector elements = getNStrings(1); - Node negative = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); - Node zero = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); - Node positive = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -140,22 +137,18 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) { Node skolem = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node variable = d_nodeManager->mkBag( - d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); - Node negative = d_nodeManager->mkBag( - d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); - Node zero = - d_nodeManager->mkBag(d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); - Node positive = - d_nodeManager->mkBag(d_nodeManager->stringType(), - skolem, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConstInt(Rational(-1))); + Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), + skolem, + d_nodeManager->mkConstInt(Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -175,9 +168,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element) TEST_F(TestTheoryWhiteBagsRewriter, bag_count) { - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node three = d_nodeManager->mkConstInt(Rational(3)); Node skolem = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( @@ -203,18 +196,14 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node bag = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5))); // (bag.duplicate_removal (bag x n)) = (bag x 1) Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag); RewriteResponse response = d_rewriter->postRewrite(n); - Node noDuplicate = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node noDuplicate = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1))); ASSERT_TRUE(response.d_node == noDuplicate && response.d_status == REWRITE_AGAIN_FULL); } @@ -225,14 +214,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_max) std::vector elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(n + 1))); Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); @@ -311,18 +298,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint) std::vector elements = getNStrings(3); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node C = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[2], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(n + 1))); + Node C = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[2], + d_nodeManager->mkConstInt(Rational(n + 2))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); @@ -375,14 +359,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, intersection_min) std::vector elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(n + 1))); Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); @@ -463,14 +445,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract) std::vector elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(n + 1))); Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); @@ -558,14 +538,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) std::vector elements = getNStrings(2); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(n + 1))); Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); @@ -638,7 +616,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) TEST_F(TestTheoryWhiteBagsRewriter, choose) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node c = d_nodeManager->mkConstInt(Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); // (bag.choose (bag x c)) = x where c is a constant > 0 @@ -653,18 +631,16 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node c = d_nodeManager->mkConstInt(Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); std::vector elements = getNStrings(2); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node B = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(4))); + Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[1], + d_nodeManager->mkConstInt(Rational(5))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // (bag.card (as bag.empty (Bag String)) = 0 @@ -697,7 +673,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) // (bag.is_singleton (bag x c) = (c == 1) Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node equal = c.eqNode(one); ASSERT_TRUE(response2.d_node == equal && response2.d_status == REWRITE_AGAIN_FULL); @@ -711,7 +687,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1) Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton); RewriteResponse response = d_rewriter->postRewrite(n); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one); ASSERT_TRUE(response.d_node == bag && response.d_status == REWRITE_AGAIN_FULL); @@ -720,10 +696,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) TEST_F(TestTheoryWhiteBagsRewriter, to_set) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node bag = - d_nodeManager->mkBag(d_nodeManager->stringType(), - x, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); + Node bag = d_nodeManager->mkBag( + d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5))); // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x) Node n = d_nodeManager->mkNode(BAG_TO_SET, bag); @@ -754,14 +728,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) std::vector elements = getNStrings(2); Node a = d_nodeManager->mkConst(String("a")); Node b = d_nodeManager->mkConst(String("b")); - Node A = - d_nodeManager->mkBag(d_nodeManager->stringType(), - a, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))); - Node B = - d_nodeManager->mkBag(d_nodeManager->stringType(), - b, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); + Node A = d_nodeManager->mkBag( + d_nodeManager->stringType(), a, d_nodeManager->mkConstInt(Rational(3))); + Node B = d_nodeManager->mkBag( + d_nodeManager->stringType(), b, d_nodeManager->mkConstInt(Rational(4))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); @@ -772,10 +742,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); Node rewritten = Rewriter::rewrite(n2); - Node bag = - d_nodeManager->mkBag(d_nodeManager->stringType(), - empty, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(7))); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + empty, + d_nodeManager->mkConstInt(Rational(7))); // - (bag.map f (bag.union_disjoint K1 K2)) = // (bag.union_disjoint (bag.map f K1) (bag.map f K2)) Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType()); @@ -796,10 +765,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) TypeNode bagIntegerType = d_nodeManager->mkBagType(d_nodeManager->integerType()); Node emptybag = d_nodeManager->mkConst(EmptyBag(bagIntegerType)); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node ten = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)); - Node n = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node ten = d_nodeManager->mkConstInt(Rational(10)); + Node n = d_nodeManager->mkConstInt(Rational(2)); Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType()); Node y = d_nodeManager->mkBoundVar("y", d_nodeManager->integerType()); Node xy = d_nodeManager->mkNode(BOUND_VAR_LIST, x, y); @@ -828,7 +797,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) // (bag.fold (lambda ((x Int)(y Int)) (+ x y)) 1 (bag 10 2)) = 21 bag = d_nodeManager->mkBag(d_nodeManager->integerType(), ten, n); Node node3 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag); - Node result3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(21)); + Node result3 = d_nodeManager->mkConstInt(Rational(21)); Node response3 = Rewriter::rewrite(node3); ASSERT_TRUE(response3 == result3); diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index e98b248a8..7f280583b 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -50,13 +50,12 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) { std::vector elements = getNStrings(1); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(100))); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(100))); Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); - Node node = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)); + Node node = d_nodeManager->mkConstInt(Rational(10)); // node of type Int is not compatible with bag of type (Bag String) ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true), @@ -66,10 +65,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) { std::vector elements = getNStrings(1); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(10))); ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag)); ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(), bag.getType()); @@ -78,18 +76,15 @@ TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) { std::vector elements = getNStrings(1); - Node negative = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1))); - Node zero = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); - Node positive = - d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); + Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(1))); // only positive multiplicity are constants ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative)); @@ -109,10 +104,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) { std::vector elements = getNStrings(1); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(10))); ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag)); ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); } @@ -120,10 +114,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) { std::vector elements = getNStrings(1); - Node bag = d_nodeManager->mkBag( - d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); + Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), + elements[0], + d_nodeManager->mkConstInt(Rational(10))); Node set = d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); @@ -140,7 +133,7 @@ TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) ASSERT_EQ(d_nodeManager->integerType(), mappedBag.getType().getBagElementType()); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node x2 = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType()); std::vector args2; args2.push_back(x2); diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index cd65445b8..d53fd2a0a 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -41,8 +41,8 @@ TEST_F(TestTheoryBlack, array_const) { TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); ASSERT_TRUE(storeAll.isConst()); diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index f1f3a4289..d28f74d34 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -39,11 +39,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit TestSmtNoFinishInit::SetUp(); d_slvEngine->setOption("produce-models", "true"); d_slvEngine->finishInit(); - d_true = d_nodeManager->mkConst(true); - d_one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); } - Node d_true; - Node d_one; }; TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) @@ -63,7 +59,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants) env.d_logic.lock(); IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1); Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems); - Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)); + Node seven = d_nodeManager->mkConstInt(Rational(7)); ASSERT_EQ(seven, result); // translating integer constants should not change them diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index 6a54baa30..d00da636a 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -80,7 +80,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple) Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType()); // make the expression (ADD x y (MULT z 0)) - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); + Node zero = d_nodeManager->mkConstInt(Rational("0")); Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero); Node n = d_nodeManager->mkNode(ADD, x, y, zTimesZero); @@ -111,8 +111,8 @@ TEST_F(TestTheoryWhiteEngine, rewriter_complex) "g", d_nodeManager->mkFunctionType(d_nodeManager->realType(), d_nodeManager->integerType())); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational("1")); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational("2")); + Node one = d_nodeManager->mkConstInt(Rational("1")); + Node two = d_nodeManager->mkConstInt(Rational("2")); Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one); Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two); diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index d6573f3a7..5d40a16a9 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -44,8 +44,8 @@ class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit TEST_F(TestTheoryWhiteIntOpt, max) { - Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); - Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); + Node ub = d_nodeManager->mkConstInt(Rational("100")); + Node lb = d_nodeManager->mkConstInt(Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -75,8 +75,8 @@ TEST_F(TestTheoryWhiteIntOpt, max) TEST_F(TestTheoryWhiteIntOpt, min) { - Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); - Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); + Node ub = d_nodeManager->mkConstInt(Rational("100")); + Node lb = d_nodeManager->mkConstInt(Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -106,8 +106,8 @@ TEST_F(TestTheoryWhiteIntOpt, min) TEST_F(TestTheoryWhiteIntOpt, result) { - Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); - Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); + Node ub = d_nodeManager->mkConstInt(Rational("100")); + Node lb = d_nodeManager->mkConstInt(Rational("0")); // Objectives to be optimized max_cost is max objective Node max_cost = d_nodeManager->mkVar(*d_intType); @@ -134,9 +134,9 @@ TEST_F(TestTheoryWhiteIntOpt, result) TEST_F(TestTheoryWhiteIntOpt, open_interval) { - Node ub1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100")); - Node lb1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0")); - Node lb2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("110")); + Node ub1 = d_nodeManager->mkConstInt(Rational("100")); + Node lb1 = d_nodeManager->mkConstInt(Rational("0")); + Node lb2 = d_nodeManager->mkConstInt(Rational("110")); Node cost1 = d_nodeManager->mkVar(*d_intType); Node cost2 = d_nodeManager->mkVar(*d_intType); diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp index 8a1af2667..91b246bb8 100644 --- a/test/unit/theory/theory_sets_rewriter_white.cpp +++ b/test/unit/theory/theory_sets_rewriter_white.cpp @@ -43,7 +43,7 @@ class TestTheoryWhiteSetsRewriter : public TestSmt TEST_F(TestTheoryWhiteSetsRewriter, map) { - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); + Node one = d_nodeManager->mkConstInt(Rational(1)); TypeNode stringType = d_nodeManager->stringType(); TypeNode integerType = d_nodeManager->integerType(); Node emptysetInteger = diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 04742cfdb..8a3c8d5dc 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -33,7 +33,7 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) { - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType()); Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType()); Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType()); diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index 745df9a41..075203898 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -75,64 +75,64 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arith) { TypeEnumerator te(d_nodeManager->integerType()); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + ASSERT_EQ(*te, d_nodeManager->mkConstInt(Rational(0))); for (int i = 1; i <= 100; ++i) { ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(i))); + ASSERT_EQ(*++te, d_nodeManager->mkConstInt(Rational(i))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-i))); + ASSERT_EQ(*++te, d_nodeManager->mkConstInt(Rational(-i))); } ASSERT_FALSE(te.isFinished()); te = TypeEnumerator(d_nodeManager->realType()); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 3))); + ASSERT_EQ(*te, d_nodeManager->mkConstReal(Rational(0, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 3))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-4, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 1))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(6, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-6, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 2))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 4))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 6))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-6, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 2))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-4, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 4))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 6))); ASSERT_FALSE(te.isFinished()); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 6))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(7, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-7, 1))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 3))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 5))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 7))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 7))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 6))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-7, 1))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 3))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 5))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 7))); + ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 7))); ASSERT_FALSE(te.isFinished()); } @@ -265,26 +265,26 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite) // ensure that certain items were found TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->integerType()); - Node zeroes = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))); - Node ones = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)))); - Node twos = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)))); - Node threes = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)))); - Node fours = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)))); - Node tens = d_nodeManager->mkConst(ArrayStoreAll( - arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)))); + Node zeroes = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(0)))); + Node ones = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(1)))); + Node twos = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(2)))); + Node threes = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(3)))); + Node fours = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(4)))); + Node tens = d_nodeManager->mkConst( + ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(10)))); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); - Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); - Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)); - Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); - Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); - Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); - Node eleven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(11)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); + Node one = d_nodeManager->mkConstInt(Rational(1)); + Node two = d_nodeManager->mkConstInt(Rational(2)); + Node three = d_nodeManager->mkConstInt(Rational(3)); + Node four = d_nodeManager->mkConstInt(Rational(4)); + Node five = d_nodeManager->mkConstInt(Rational(5)); + Node eleven = d_nodeManager->mkConstInt(Rational(11)); ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)), elts.end()); diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 0f4016698..91e3e0d26 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -32,15 +32,15 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TypeNode usort = d_nodeManager->mkSort("U"); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->realType()), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))); + d_nodeManager->mkConstReal(Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), d_nodeManager->mkConst(UninterpretedSortValue(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + d_nodeManager->mkConstInt(Rational(0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->integerType()), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); + d_nodeManager->mkConstInt(Rational(0))); } TEST_F(TestUtilWhiteArrayStoreAll, type_errors) @@ -49,14 +49,13 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors) d_nodeManager->mkConst(UninterpretedSortValue( d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); - ASSERT_THROW( - ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), - IllegalArgumentException); + ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConstReal(Rational(9, 2))), + IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->mkSort("U")), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), + d_nodeManager->mkConstReal(Rational(9, 2))), IllegalArgumentException); } @@ -71,13 +70,12 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) ArrayStoreAll(d_nodeManager->integerType(), d_nodeManager->mkVar("x", d_nodeManager->integerType())), IllegalArgumentException); - ASSERT_THROW( - ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkNode( - kind::ADD, - d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), - d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))), - IllegalArgumentException); + ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkNode( + kind::ADD, + d_nodeManager->mkConstInt(Rational(1)), + d_nodeManager->mkConstInt(Rational(0)))), + IllegalArgumentException); } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index da41b41e6..ad7ccc0f4 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -255,7 +255,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) const DType& ldt = listType.getDType(); Node updater = ldt[0][0].getUpdater(); Node gt = d_nodeManager->mkGroundTerm(listType); - Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = d_nodeManager->mkConstInt(Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero); -- 2.30.2