From e3bec47e98e76ad6e4a11259af096abb20f7de57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 15 May 2022 11:30:26 -0500 Subject: [PATCH] Eliminate ops for parameterized type constructors (#8761) We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences. --- src/CMakeLists.txt | 6 - src/api/cpp/cvc5.cpp | 38 +--- src/expr/node_manager_template.cpp | 36 --- src/expr/node_manager_template.h | 28 --- src/proof/lfsc/lfsc_node_converter.cpp | 3 +- src/theory/bags/bag_make_op.cpp | 50 ---- src/theory/bags/bag_make_op.h | 63 ----- src/theory/bags/bag_reduction.cpp | 4 +- src/theory/bags/bags_rewriter.cpp | 14 +- src/theory/bags/bags_rewriter.h | 4 +- src/theory/bags/bags_utils.cpp | 13 +- src/theory/bags/kinds | 10 +- src/theory/bags/theory_bags.cpp | 2 +- .../bags/theory_bags_type_enumerator.cpp | 2 +- src/theory/bags/theory_bags_type_rules.cpp | 21 +- .../quantifiers/fmf/bounded_integers.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 15 +- src/theory/sep/theory_sep.cpp | 22 +- src/theory/sets/cardinality_extension.cpp | 6 +- src/theory/sets/kinds | 10 +- src/theory/sets/normal_form.h | 5 +- src/theory/sets/singleton_op.cpp | 51 ----- src/theory/sets/singleton_op.h | 63 ----- src/theory/sets/theory_sets_private.cpp | 5 +- src/theory/sets/theory_sets_rels.cpp | 19 +- src/theory/sets/theory_sets_rels.h | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 9 +- .../sets/theory_sets_type_enumerator.cpp | 3 +- src/theory/sets/theory_sets_type_rules.cpp | 21 +- src/theory/sets/theory_sets_type_rules.h | 2 +- src/theory/strings/array_core_solver.cpp | 3 +- src/theory/strings/kinds | 11 +- src/theory/strings/seq_unit_op.cpp | 50 ---- src/theory/strings/seq_unit_op.h | 63 ----- src/theory/strings/theory_strings.cpp | 9 +- .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_type_rules.cpp | 23 +- src/theory/strings/theory_strings_utils.cpp | 3 +- test/unit/theory/sequences_rewriter_white.cpp | 20 +- .../theory/theory_bags_normal_form_white.cpp | 215 +++++++++--------- .../theory/theory_bags_rewriter_white.cpp | 153 ++++++------- .../theory/theory_bags_type_rules_white.cpp | 41 ++-- .../theory/theory_sets_rewriter_white.cpp | 6 +- .../theory/theory_sets_type_rules_white.cpp | 19 +- 44 files changed, 276 insertions(+), 871 deletions(-) delete mode 100644 src/theory/bags/bag_make_op.cpp delete mode 100644 src/theory/bags/bag_make_op.h delete mode 100644 src/theory/sets/singleton_op.cpp delete mode 100644 src/theory/sets/singleton_op.h delete mode 100644 src/theory/strings/seq_unit_op.cpp delete mode 100644 src/theory/strings/seq_unit_op.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3b3069723..023209605 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -547,8 +547,6 @@ libcvc5_add_sources( theory/assertion.h theory/atom_requests.cpp theory/atom_requests.h - theory/bags/bag_make_op.cpp - theory/bags/bag_make_op.h theory/bags/bags_rewriter.cpp theory/bags/bags_rewriter.h theory/bags/bag_solver.cpp @@ -1018,8 +1016,6 @@ libcvc5_add_sources( theory/sets/normal_form.h theory/sets/rels_utils.cpp theory/sets/rels_utils.h - theory/sets/singleton_op.cpp - theory/sets/singleton_op.h theory/sets/skolem_cache.cpp theory/sets/skolem_cache.h theory/sets/solver_state.cpp @@ -1090,8 +1086,6 @@ libcvc5_add_sources( theory/strings/regexp_solver.h theory/strings/rewrites.cpp theory/strings/rewrites.h - theory/strings/seq_unit_op.cpp - theory/strings/seq_unit_op.h theory/strings/sequences_rewriter.cpp theory/strings/sequences_rewriter.h theory/strings/sequences_stats.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 29208c2cd..665bbdc6b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5103,42 +5103,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const { // default case, same as above checkMkTerm(kind, children.size()); - if (kind == SET_SINGLETON) - { - // the type of the term is the same as the type of the internal node - // see Term::getSort() - internal::TypeNode type = children[0].d_node->getType(); - // Internally NodeManager::mkSingleton needs a type argument - // to construct a singleton, since there is no difference between - // integers and reals (both are Rationals). - // At the API, mkReal and mkInteger are different and therefore the - // element type can be used safely here. - res = getNodeManager()->mkSingleton(type, *children[0].d_node); - } - else if (kind == BAG_MAKE) - { - // the type of the term is the same as the type of the internal node - // see Term::getSort() - internal::TypeNode type = children[0].d_node->getType(); - // Internally NodeManager::mkBag needs a type argument - // to construct a bag, since there is no difference between - // integers and reals (both are Rationals). - // At the API, mkReal and mkInteger are different and therefore the - // element type can be used safely here. - res = getNodeManager()->mkBag( - type, *children[0].d_node, *children[1].d_node); - } - else if (kind == SEQ_UNIT) - { - // the type of the term is the same as the type of the internal node - // see Term::getSort() - internal::TypeNode type = children[0].d_node->getType(); - res = getNodeManager()->mkSeqUnit(type, *children[0].d_node); - } - else - { - res = d_nodeMgr->mkNode(k, echildren); - } + // make the term + res = d_nodeMgr->mkNode(k, echildren); } (void)res.getType(true); /* kick off type checking */ diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 6259971cc..7077f2bfe 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -30,9 +30,6 @@ #include "expr/skolem_manager.h" #include "expr/type_checker.h" #include "expr/type_properties.h" -#include "theory/bags/bag_make_op.h" -#include "theory/sets/singleton_op.h" -#include "theory/strings/seq_unit_op.h" #include "util/bitvector.h" #include "util/poly_util.h" #include "util/rational.h" @@ -1148,39 +1145,6 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) } } -Node NodeManager::mkSeqUnit(const TypeNode& t, const TNode n) -{ - Assert(n.getType().isSubtypeOf(t)) - << "Invalid operands for mkSeqUnit. The type '" << n.getType() - << "' of node '" << n << "' is not a subtype of '" << t << "'." - << std::endl; - Node op = mkConst(SeqUnitOp(t)); - Node sunit = mkNode(kind::SEQ_UNIT, op, n); - return sunit; -} - -Node NodeManager::mkSingleton(const TypeNode& t, const TNode n) -{ - Assert(n.getType().isSubtypeOf(t)) - << "Invalid operands for mkSingleton. The type '" << n.getType() - << "' of node '" << n << "' is not a subtype of '" << t << "'." - << std::endl; - Node op = mkConst(SetSingletonOp(t)); - Node singleton = mkNode(kind::SET_SINGLETON, op, n); - return singleton; -} - -Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) -{ - Assert(n.getType().isSubtypeOf(t)) - << "Invalid operands for mkBag. The type '" << n.getType() - << "' of node '" << n << "' is not a subtype of '" << t << "'." - << std::endl; - Node op = mkConst(BagMakeOp(t)); - Node bag = mkNode(kind::BAG_MAKE, op, n, m); - return bag; -} - bool NodeManager::hasOperator(Kind k) { switch (kind::MetaKind mk = kind::metaKindOf(k)) diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index 513742383..1aa0a24b9 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -627,34 +627,6 @@ class NodeManager /** make unique (per Type,Kind) variable. */ Node mkNullaryOperator(const TypeNode& type, Kind k); - /** - * Create a sequence unit from the given element n. - * @param t the element type of the returned sequence. - * Note that the type of n needs to be a subtype of t. - * @param n the single element in the sequence. - * @return a sequence unit constructed from the element n. - */ - Node mkSeqUnit(const TypeNode& t, const TNode n); - - /** - * Create a singleton set from the given element n. - * @param t the element type of the returned set. - * Note that the type of n needs to be a subtype of t. - * @param n the single element in the singleton. - * @return a singleton set constructed from the element n. - */ - Node mkSingleton(const TypeNode& t, const TNode n); - - /** - * Create a bag from the given element n along with its multiplicity m. - * @param t the element type of the returned bag. - * Note that the type of n needs to be a subtype of t. - * @param n the element that is used to to construct the bag - * @param m the multiplicity of the element n - * @return a bag that contains m occurrences of n. - */ - Node mkBag(const TypeNode& t, const TNode n, const TNode m); - /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 2ed7c3f89..aef461adc 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -313,8 +313,7 @@ Node LfscNodeConverter::postConvert(Node n) std::vector vecu; for (size_t i = 0, size = charVec.size(); i < size; i++) { - Node u = nm->mkSeqUnit(tn.getSequenceElementType(), - postConvert(charVec[size - (i + 1)])); + Node u = nm->mkNode(SEQ_UNIT, postConvert(charVec[size - (i + 1)])); if (size == 1) { // singleton case diff --git a/src/theory/bags/bag_make_op.cpp b/src/theory/bags/bag_make_op.cpp deleted file mode 100644 index 55780a880..000000000 --- a/src/theory/bags/bag_make_op.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for BAG_MAKE operator. - */ - -#include "bag_make_op.h" - -#include - -#include "expr/type_node.h" - -namespace cvc5::internal { - -std::ostream& operator<<(std::ostream& out, const BagMakeOp& op) -{ - return out << "(BagMakeOp " << op.getType() << ')'; -} - -size_t BagMakeOpHashFunction::operator()(const BagMakeOp& op) const -{ - return std::hash()(op.getType()); -} - -BagMakeOp::BagMakeOp(const TypeNode& elementType) - : d_type(new TypeNode(elementType)) -{ -} - -BagMakeOp::BagMakeOp(const BagMakeOp& op) : d_type(new TypeNode(op.getType())) -{ -} - -const TypeNode& BagMakeOp::getType() const { return *d_type; } - -bool BagMakeOp::operator==(const BagMakeOp& op) const -{ - return getType() == op.getType(); -} - -} // namespace cvc5::internal diff --git a/src/theory/bags/bag_make_op.h b/src/theory/bags/bag_make_op.h deleted file mode 100644 index a4dd7e5be..000000000 --- a/src/theory/bags/bag_make_op.h +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for BAG_MAKE operator. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__BAG_MAKE_OP_H -#define CVC5__BAG_MAKE_OP_H - -#include - -namespace cvc5::internal { - -class TypeNode; - -/** - * The class is an operator for kind BAG_MAKE used to construct bags. - * It specifies the type of the element especially when it is a constant. - * e.g. the type of rational 1 is Int, however - * (bag (BagMakeOp Real) 1) is of type (Bag Real), not (Bag Int). - * Note that the type passed to the constructor is the element's type, not the - * bag type. - */ -class BagMakeOp -{ - public: - explicit BagMakeOp(const TypeNode& elementType); - BagMakeOp(const BagMakeOp& op); - - /** return the type of the current object */ - const TypeNode& getType() const; - - bool operator==(const BagMakeOp& op) const; - - private: - /** a pointer to the type of the bag element */ - std::unique_ptr d_type; -}; /* class BagMakeOp */ - -std::ostream& operator<<(std::ostream& out, const BagMakeOp& op); - -/** - * Hash function for the BagMakeOpHashFunction objects. - */ -struct BagMakeOpHashFunction -{ - size_t operator()(const BagMakeOp& op) const; -}; /* struct BagMakeOpHashFunction */ - -} // namespace cvc5::internal - -#endif /* CVC5__BAG_MAKE_OP_H */ diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index 5e6d71935..89a422301 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -102,7 +102,7 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector& asserts) combine_i.eqNode(nm->mkNode(APPLY_UF, f, uf_i, combine_iMinusOne)); Node unionDisjoint_0_equal = unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType))); - Node singleton = nm->mkBag(elementType, uf_i, one); + Node singleton = nm->mkNode(BAG_MAKE, uf_i, one); Node unionDisjoint_i_equal = unionDisjoint_i.eqNode( nm->mkNode(BAG_UNION_DISJOINT, singleton, unionDisjoint_iMinusOne)); @@ -171,7 +171,7 @@ Node BagReduction::reduceCardOperator(Node node, std::vector& asserts) nm->mkNode(ADD, uf_i_multiplicity, cardinality_iMinusOne)); Node unionDisjoint_0_equal = unionDisjoint_0.eqNode(nm->mkConst(EmptyBag(bagType))); - Node bag = nm->mkBag(elementType, uf_i, uf_i_multiplicity); + Node bag = nm->mkNode(BAG_MAKE, uf_i, uf_i_multiplicity); Node unionDisjoint_i_equal = unionDisjoint_i.eqNode( nm->mkNode(BAG_UNION_DISJOINT, bag, unionDisjoint_iMinusOne)); diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index e401551a7..862af9f43 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -211,7 +211,7 @@ BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const { // (bag.duplicate_removal (bag x n)) = (bag x 1) // where n is a positive constant - Node bag = d_nm->mkBag(n[0][0].getType(), n[0][0], d_one); + Node bag = d_nm->mkNode(BAG_MAKE, n[0][0], d_one); return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); @@ -477,9 +477,8 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const Assert(n.getKind() == BAG_FROM_SET); if (n[0].getKind() == SET_SINGLETON) { - // (bag.from_set (set.singleton (SetSingletonOp Int) x)) = (bag x 1) - TypeNode type = n[0].getType().getSetElementType(); - Node bag = d_nm->mkBag(type, n[0][0], d_one); + // (bag.from_set (set.singleton x)) = (bag x 1) + Node bag = d_nm->mkNode(BAG_MAKE, n[0][0], d_one); return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); } return BagsRewriteResponse(n, Rewrite::NONE); @@ -491,9 +490,9 @@ BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst().sgn() == 1) { - // (bag.to_set (bag x n)) = (set.singleton (SetSingletonOp T) x) + // (bag.to_set (bag x n)) = (set.singleton x) // where n is a positive constant and T is the type of the bag's elements - Node set = d_nm->mkSingleton(n[0][0].getType(), n[0][0]); + Node set = d_nm->mkNode(SET_SINGLETON, n[0][0]); return BagsRewriteResponse(set, Rewrite::TO_SINGLETON); } return BagsRewriteResponse(n, Rewrite::NONE); @@ -550,8 +549,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const { // (bag.map f (bag x y)) = (bag (apply f x) y) Node mappedElement = d_nm->mkNode(APPLY_UF, n[0], n[1][0]); - Node ret = - d_nm->mkBag(n[0].getType().getRangeType(), mappedElement, n[1][1]); + Node ret = d_nm->mkNode(BAG_MAKE, mappedElement, n[1][1]); return BagsRewriteResponse(ret, Rewrite::MAP_BAG_MAKE); } diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 711846143..a73080f1b 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -198,13 +198,13 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.from_set (singleton (SetSingletonOp Int) x)) = (bag x 1) + * - (bag.from_set (set.singleton x)) = (bag x 1) */ BagsRewriteResponse rewriteFromSet(const TNode& n) const; /** * rewrites for n include: - * - (bag.to_set (bag x n)) = (singleton (SetSingletonOp T) x) + * - (bag.to_set (bag x n)) = (set.singleton x) * where n is a positive constant and T is the type of the bag's elements */ BagsRewriteResponse rewriteToSet(const TNode& n) const; diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 7ee00c432..1379b1ef8 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -237,10 +237,10 @@ Node BagsUtils::constructConstantBagFromElements( } TypeNode elementType = t.getBagElementType(); std::map::const_reverse_iterator it = elements.rbegin(); - Node bag = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second)); + Node bag = nm->mkNode(BAG_MAKE, it->first, nm->mkConstInt(it->second)); while (++it != elements.rend()) { - Node n = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second)); + Node n = nm->mkNode(BAG_MAKE, it->first, nm->mkConstInt(it->second)); bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag); } return bag; @@ -257,10 +257,10 @@ Node BagsUtils::constructBagFromElements(TypeNode t, } TypeNode elementType = t.getBagElementType(); std::map::const_reverse_iterator it = elements.rbegin(); - Node bag = nm->mkBag(elementType, it->first, it->second); + Node bag = nm->mkNode(BAG_MAKE, it->first, it->second); while (++it != elements.rend()) { - Node n = nm->mkBag(elementType, it->first, it->second); + Node n = nm->mkNode(BAG_MAKE, it->first, it->second); bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag); } return bag; @@ -745,7 +745,7 @@ Node BagsUtils::evaluateBagFilter(TNode n) for (const auto& [e, count] : elements) { Node multiplicity = nm->mkConstInt(count); - Node bag = nm->mkBag(bagType.getBagElementType(), e, multiplicity); + Node bag = nm->mkNode(BAG_MAKE, e, multiplicity); Node pOfe = nm->mkNode(APPLY_UF, P, e); Node ite = nm->mkNode(ITE, pOfe, bag, empty); bags.push_back(ite); @@ -868,8 +868,7 @@ Node BagsUtils::evaluateBagPartition(Rewriter* rewriter, TNode n) std::vector bags; for (const Node& node : eqc) { - Node bag = nm->mkBag( - bagType.getBagElementType(), node, nm->mkConstInt(elements[node])); + Node bag = nm->mkNode(BAG_MAKE, node, nm->mkConstInt(elements[node])); bags.push_back(bag); } Node part = computeDisjointUnion(bagType, bags); diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index ecde27c62..d3a98a311 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -51,14 +51,7 @@ operator BAG_COUNT 2 "multiplicity of an element in a bag" operator BAG_MEMBER 2 "bag membership predicate; is first parameter a member of second?" operator BAG_DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" -constant BAG_MAKE_OP \ - class \ - BagMakeOp \ - ::cvc5::internal::BagMakeOpHashFunction \ - "theory/bags/bag_make_op.h" \ - "operator for BAG_MAKE; payload is an instance of the cvc5::internal::BagMakeOp class" -parameterized BAG_MAKE BAG_MAKE_OP 2 \ -"constructs a bag from one element along with its multiplicity" +operator BAG_MAKE 2 "constructs a bag from one element along with its multiplicity" # The operator bag-is-singleton returns whether the given bag is a singleton operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton" @@ -102,7 +95,6 @@ typerule BAG_SUBBAG ::cvc5::internal::theory::bags::SubBagTypeRule typerule BAG_COUNT ::cvc5::internal::theory::bags::CountTypeRule typerule BAG_MEMBER ::cvc5::internal::theory::bags::MemberTypeRule typerule BAG_DUPLICATE_REMOVAL ::cvc5::internal::theory::bags::DuplicateRemovalTypeRule -typerule BAG_MAKE_OP "SimpleTypeRule" typerule BAG_MAKE ::cvc5::internal::theory::bags::BagMakeTypeRule typerule BAG_EMPTY ::cvc5::internal::theory::bags::EmptyBagTypeRule typerule BAG_CARD ::cvc5::internal::theory::bags::CardTypeRule diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 3fa491a7c..c1d34eac8 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -412,7 +412,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m, Trace("bags-model") << "newElement is " << newElement << std::endl; Rational difference = rCardRational - constructedRational; Node multiplicity = nm->mkConstInt(difference); - Node slackBag = nm->mkBag(elementType, newElement, multiplicity); + Node slackBag = nm->mkNode(BAG_MAKE, newElement, multiplicity); constructedBag = nm->mkNode(kind::BAG_UNION_DISJOINT, constructedBag, slackBag); constructedBag = rewrite(constructedBag); diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 625909bc0..b64e83407 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -61,7 +61,7 @@ BagEnumerator& BagEnumerator::operator++() // return (bag d_element 1) Node one = d_nodeManager->mkConstInt(Rational(1)); TypeNode elementType = d_elementTypeEnumerator.getType(); - Node singleton = d_nodeManager->mkBag(elementType, d_element, one); + Node singleton = d_nodeManager->mkNode(BAG_MAKE, d_element, one); d_currentBag = singleton; } else diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 4e3da85f5..ee3d9b5a8 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -22,7 +22,6 @@ #include "expr/dtype_cons.h" #include "expr/emptybag.h" #include "table_project_op.h" -#include "theory/bags/bag_make_op.h" #include "theory/bags/bags_utils.h" #include "theory/datatypes/tuple_project_op.h" #include "theory/datatypes/tuple_utils.h" @@ -174,10 +173,8 @@ TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager, TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check) { - Assert(n.getKind() == kind::BAG_MAKE && n.hasOperator() - && n.getOperator().getKind() == kind::BAG_MAKE_OP); - BagMakeOp op = n.getOperator().getConst(); - TypeNode expectedElementType = op.getType(); + Assert(n.getKind() == kind::BAG_MAKE); + TypeNode actualElementType = n[0].getType(check); if (check) { if (n.getNumChildren() != 2) @@ -194,21 +191,9 @@ TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check) ss << "BAG_MAKE expects an integer for " << n[1] << ". Found" << type1; throw TypeCheckingExceptionPrivate(n, ss.str()); } - - TypeNode actualElementType = n[0].getType(check); - // the type of the element should be a subtype of the type of the operator - // e.g. (bag (bag_op Real) 1 1) where 1 is an Int - if (actualElementType != expectedElementType) - { - std::stringstream ss; - ss << "The type '" << actualElementType - << "' of the element is not type of '" << expectedElementType - << "' in term : " << n; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } } - return nm->mkBagType(expectedElementType); + return nm->mkBagType(actualElementType); } bool BagMakeTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ef47b2fb3..dd3ddd54d 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -701,7 +701,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Assert(i < d_setm_choice[sro].size()); choice_i = d_setm_choice[sro][i]; choices.push_back(choice_i); - Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i); + Node sChoiceI = nm->mkNode(SET_SINGLETON, choice_i); if (nsr.isNull()) { nsr = sChoiceI; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index f6cdc2411..9d3e9d7fa 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -934,12 +934,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl; std::vector cargsSeqUnit; cargsSeqUnit.push_back(unresElemType); - // lambda x . (seq.unit (seq_unit_op T) x) where T = x.getType() - Node x = nm->mkBoundVar(etype); - Node vars = nm->mkNode(BOUND_VAR_LIST, x); - Node seqUnit = nm->mkSeqUnit(etype, x); - Node lambda = nm->mkNode(LAMBDA, vars, seqUnit); - sdts[i].addConstructor(lambda, "seq.unit", cargsSeqUnit); + sdts[i].addConstructor(SEQ_UNIT, cargsSeqUnit); } } else if (types[i].isArray()) @@ -985,13 +980,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for singleton" << std::endl; std::vector cargsSingleton; cargsSingleton.push_back(unresElemType); - - // lambda x . (singleton (singleton_op T) x) where T = x.getType() - Node x = nm->mkBoundVar(etype); - Node vars = nm->mkNode(BOUND_VAR_LIST, x); - Node singleton = nm->mkSingleton(etype, x); - Node lambda = nm->mkNode(LAMBDA,vars, singleton); - sdts[i].addConstructor(lambda, "singleton", cargsSingleton); + sdts[i].addConstructor(SET_SINGLETON, cargsSingleton); // add for union, difference, intersection std::vector bin_kinds = {SET_UNION, SET_INTER, SET_MINUS}; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 2c5cdf029..cbde4c89c 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -291,7 +291,7 @@ bool TheorySep::preNotifyFact( { NodeManager* nm = NodeManager::currentNM(); // (SEP_LABEL (sep.pto x y) L) => L = (set.singleton x) - Node s = nm->mkSingleton(slbl.getType().getSetElementType(), satom[0]); + Node s = nm->mkNode(SET_SINGLETON, satom[0]); Node eq = slbl.eqNode(s); TrustNode trn = d_im.mkLemmaExp(eq, PfRule::THEORY_INFERENCE, {fact}, {fact}, {eq}); @@ -410,8 +410,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } else if (satom.getKind() == SEP_PTO) { - // TODO(project##230): Find a safe type for the singleton operator - Node ss = nm->mkSingleton(satom[0].getType(), satom[0]); + Node ss = nm->mkNode(SET_SINGLETON, satom[0]); if (slbl != ss) { conc = slbl.eqNode(ss); @@ -1280,7 +1279,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { for( unsigned i=0; imkSingleton(tn, s); + s = NodeManager::currentNM()->mkNode(SET_SINGLETON, s); if( u.isNull() ){ u = s; }else{ @@ -1452,6 +1451,7 @@ Node TheorySep::instantiateLabel(Node n, std::map& active_lbl, unsigned ind) { + NodeManager* nm = NodeManager::currentNM(); Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl; if (options().sep.sepMinimalRefine && lbl != o_lbl && active_lbl.find(lbl) != active_lbl.end()) @@ -1552,14 +1552,12 @@ Node TheorySep::instantiateLabel(Node n, //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption Assert(d_label_model.find(o_lbl) != d_label_model.end()); Node vr = d_valuation.getModel()->getRepresentative( n[0] ); - // TODO(project##230): Find a safe type for the singleton operator - Node svr = NodeManager::currentNM()->mkSingleton(vr.getType(), vr); + Node svr = nm->mkNode(SET_SINGLETON, vr); bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end(); Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl; std::vector< Node > children; if( inBaseHeap ){ - // TODO(project##230): Find a safe type for the singleton operator - Node s = NodeManager::currentNM()->mkSingleton(n[0].getType(), n[0]); + Node s = nm->mkNode(SET_SINGLETON, n[0]); children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) ); }else{ //look up value of data @@ -1572,8 +1570,7 @@ Node TheorySep::instantiateLabel(Node n, Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl; } } - // TODO(project##230): Find a safe type for the singleton operator - Node singleton = NodeManager::currentNM()->mkSingleton(n[0].getType(), n[0]); + Node singleton = nm->mkNode(SET_SINGLETON, n[0]); children.push_back(singleton.eqNode(lbl_v)); Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) ); Trace("sep-inst-debug") << "Return " << ret << std::endl; @@ -1658,7 +1655,7 @@ void TheorySep::getLabelChildren(Node satom, void TheorySep::computeLabelModel( Node lbl ) { if( !d_label_model[lbl].d_computed ){ d_label_model[lbl].d_computed = true; - + NodeManager* nm = NodeManager::currentNM(); //we must get the value of lbl from the model: this is being run at last call, after the model is constructed //Assert(...); TODO Node v_val = d_valuation.getModel()->getRepresentative( lbl ); @@ -1700,8 +1697,7 @@ void TheorySep::computeLabelModel( Node lbl ) { }else{ tt = itm->second; } - // TODO(project##230): Find a safe type for the singleton operator - Node stt = NodeManager::currentNM()->mkSingleton(tt.getType(), tt); + Node stt = nm->mkNode(SET_SINGLETON, tt); Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl; d_label_model[lbl].d_heap_locs.push_back( stt ); } diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 78658f7bd..f6079f477 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1082,7 +1082,7 @@ void CardinalityExtension::mkModelValueElementsFor( // the current members of this finite type. Node slack = sm->mkDummySkolem("slack", elementType); - Node singleton = nm->mkSingleton(elementType, slack); + Node singleton = nm->mkNode(SET_SINGLETON, slack); els.push_back(singleton); d_finite_type_slack_elements[elementType].push_back(slack); Trace("sets-model") << "Added slack element " << slack << " to set " @@ -1090,8 +1090,8 @@ void CardinalityExtension::mkModelValueElementsFor( } else { - els.push_back(nm->mkSingleton( - elementType, sm->mkDummySkolem("msde", elementType))); + els.push_back(nm->mkNode(SET_SINGLETON, + sm->mkDummySkolem("msde", elementType))); } } } diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 30e0006d6..da7c2b930 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -42,14 +42,7 @@ operator SET_MINUS 2 "set subtraction" operator SET_SUBSET 2 "subset predicate; first parameter a subset of second" operator SET_MEMBER 2 "set membership predicate; first parameter a member of second" -constant SET_SINGLETON_OP \ - class \ - SetSingletonOp \ - ::cvc5::internal::SetSingletonOpHashFunction \ - "theory/sets/singleton_op.h" \ - "operator for singletons; payload is an instance of the cvc5::internal::SingletonOp class" -parameterized SET_SINGLETON SET_SINGLETON_OP 1 \ -"constructs a set of a single element. First parameter is a SingletonOp. Second is a term" +operator SET_SINGLETON 1 "constructs a set of a single element. First parameter is a term" operator SET_INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" operator SET_CARD 1 "set cardinality operator" @@ -96,7 +89,6 @@ typerule SET_INTER ::cvc5::internal::theory::sets::SetsBinaryOperatorTypeRule typerule SET_MINUS ::cvc5::internal::theory::sets::SetsBinaryOperatorTypeRule typerule SET_SUBSET ::cvc5::internal::theory::sets::SubsetTypeRule typerule SET_MEMBER ::cvc5::internal::theory::sets::MemberTypeRule -typerule SET_SINGLETON_OP "SimpleTypeRule" typerule SET_SINGLETON ::cvc5::internal::theory::sets::SingletonTypeRule typerule SET_EMPTY ::cvc5::internal::theory::sets::EmptySetTypeRule typerule SET_INSERT ::cvc5::internal::theory::sets::InsertTypeRule diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index c8b6b5c80..75d2d9798 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -45,12 +45,11 @@ class NormalForm { } else { - TypeNode elementType = setType.getSetElementType(); ElementsIterator it = elements.begin(); - Node cur = nm->mkSingleton(elementType, *it); + Node cur = nm->mkNode(kind::SET_SINGLETON, *it); while (++it != elements.end()) { - Node singleton = nm->mkSingleton(elementType, *it); + Node singleton = nm->mkNode(kind::SET_SINGLETON, *it); cur = nm->mkNode(kind::SET_UNION, singleton, cur); } return cur; diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp deleted file mode 100644 index e1a609de8..000000000 --- a/src/theory/sets/singleton_op.cpp +++ /dev/null @@ -1,51 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed, Aina Niemetz, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for singleton operator for sets. - */ - -#include "theory/sets/singleton_op.h" - -#include - -#include "expr/type_node.h" - -namespace cvc5::internal { - -std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op) -{ - return out << "(SetSingletonOp " << op.getType() << ')'; -} - -size_t SetSingletonOpHashFunction::operator()(const SetSingletonOp& op) const -{ - return std::hash()(op.getType()); -} - -SetSingletonOp::SetSingletonOp(const TypeNode& elementType) - : d_type(new TypeNode(elementType)) -{ -} - -SetSingletonOp::SetSingletonOp(const SetSingletonOp& op) - : d_type(new TypeNode(op.getType())) -{ -} - -const TypeNode& SetSingletonOp::getType() const { return *d_type; } - -bool SetSingletonOp::operator==(const SetSingletonOp& op) const -{ - return getType() == op.getType(); -} - -} // namespace cvc5::internal diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h deleted file mode 100644 index bf88ba8d4..000000000 --- a/src/theory/sets/singleton_op.h +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for singleton operator for sets. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__THEORY__SETS__SINGLETON_OP_H -#define CVC5__THEORY__SETS__SINGLETON_OP_H - -#include - -namespace cvc5::internal { - -class TypeNode; - -/** - * The class is an operator for kind SET_SINGLETON used to construct singleton - * sets. It specifies the type of the single element especially when it is a - * constant. e.g. the type of rational 1 is Int, however (singleton - * (singleton_op Real) 1) is of type (Set Real), not (Set Int). Note that the - * type passed to the constructor is the element's type, not the set type. - */ -class SetSingletonOp -{ - public: - SetSingletonOp(const TypeNode& elementType); - SetSingletonOp(const SetSingletonOp& op); - - /** return the type of the current object */ - const TypeNode& getType() const; - - bool operator==(const SetSingletonOp& op) const; - - private: - SetSingletonOp(); - /** a pointer to the type of the singleton element */ - std::unique_ptr d_type; -}; /* class SetSingletonOp */ - -std::ostream& operator<<(std::ostream& out, const SetSingletonOp& op); - -/** - * Hash function for the SetSingletonOp objects. - */ -struct SetSingletonOpHashFunction -{ - size_t operator()(const SetSingletonOp& op) const; -}; /* struct SetSingletonOpHashFunction */ - -} // namespace cvc5::internal - -#endif /* CVC5__THEORY__SETS__SINGLETON_OP_H */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e29821d55..393bcc415 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -966,13 +966,12 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, const std::map& emems = d_state.getMembers(eqc); if (!emems.empty()) { - TypeNode elementType = eqc.getType().getSetElementType(); for (const std::pair& itmm : emems) { // when we have y -> (set.member x S) where rep(x)=y, we use x // in the model here. Using y may not be legal with respect to // subtyping, since y may be real where x is an int. - Node t = nm->mkSingleton(elementType, itmm.second[0]); + Node t = nm->mkNode(SET_SINGLETON, itmm.second[0]); els.push_back(t); } } @@ -1246,7 +1245,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node) TypeNode setType = set.getType(); ensureFirstClassSetType(setType); Node boundVar = nm->mkBoundVar(setType.getSetElementType()); - Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar); + Node singleton = nm->mkNode(SET_SINGLETON, boundVar); Node equal = set.eqNode(singleton); std::vector variables = {boundVar}; Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index bd6fe1e8c..e83eabedb 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -275,7 +275,7 @@ void TheorySetsRels::check(Theory::Effort level) Node element = TupleUtils::nthElementOfTuple(eqc_node, i); if (!element.isConst()) { - makeSharedTerm(element, tupleTypes[i]); + makeSharedTerm(element); } } } @@ -929,7 +929,7 @@ void TheorySetsRels::check(Theory::Effort level) fact = NodeManager::currentNM()->mkNode(kind::SET_MEMBER, mem2, join_rel[1]); sendInfer(fact, InferenceId::SETS_RELS_JOIN_SPLIT_2, reason); - makeSharedTerm(shared_x, shared_type); + makeSharedTerm(shared_x); } /* @@ -1122,8 +1122,8 @@ void TheorySetsRels::check(Theory::Effort level) // Since we require notification r1_rmost and r2_lmost are equal, // they must be shared terms of theory of sets. Hence, we make the // following calls to makeSharedTerm to ensure this is the case. - makeSharedTerm(r1_rmost, r1_rmost.getType()); - makeSharedTerm(r2_lmost, r2_lmost.getType()); + makeSharedTerm(r1_rmost); + makeSharedTerm(r2_lmost); Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost << " of type " << r1_rmost.getType() << std::endl; @@ -1238,9 +1238,8 @@ void TheorySetsRels::check(Theory::Effort level) } else if (!atn.isBoolean()) { - // TODO(project##230): Find a safe type for the singleton operator - makeSharedTerm(a, atn); - makeSharedTerm(b, b.getType()); + makeSharedTerm(a); + makeSharedTerm(b); } return false; } @@ -1269,7 +1268,7 @@ void TheorySetsRels::check(Theory::Effort level) return false; } - void TheorySetsRels::makeSharedTerm(Node n, TypeNode t) + void TheorySetsRels::makeSharedTerm(Node n) { if (d_shared_terms.find(n) != d_shared_terms.end()) { @@ -1277,7 +1276,7 @@ void TheorySetsRels::check(Theory::Effort level) } Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl; // force a proxy lemma to be sent for the singleton containing n - Node ss = NodeManager::currentNM()->mkSingleton(t, n); + Node ss = NodeManager::currentNM()->mkNode(SET_SINGLETON, n); d_treg.getProxy(ss); d_shared_terms.insert(n); } @@ -1308,7 +1307,7 @@ void TheorySetsRels::check(Theory::Effort level) for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) { Node element = TupleUtils::nthElementOfTuple(n[0], i); - makeSharedTerm(element, tupleTypes[i]); + makeSharedTerm(element); tuple_elements.push_back(element); } Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 64f7b2406..2ee5cb247 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -180,7 +180,7 @@ class TheorySetsRels : protected EnvObj /** Helper functions */ bool hasTerm( Node a ); - void makeSharedTerm(Node, TypeNode t); + void makeSharedTerm(Node a); void reduceTupleVar( Node ); bool hasMember( Node, Node ); void computeTupleReps( Node ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 85f24c7fd..f156f3db5 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -608,12 +608,11 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { else if (k == kind::SET_INSERT) { size_t setNodeIndex = node.getNumChildren()-1; - TypeNode elementType = node[setNodeIndex].getType().getSetElementType(); - Node insertedElements = nm->mkSingleton(elementType, node[0]); + Node insertedElements = nm->mkNode(SET_SINGLETON, node[0]); for (size_t i = 1; i < setNodeIndex; ++i) { - Node singleton = nm->mkSingleton(elementType, node[i]); + Node singleton = nm->mkNode(SET_SINGLETON, node[i]); insertedElements = nm->mkNode(kind::SET_UNION, insertedElements, singleton); } @@ -641,11 +640,11 @@ RewriteResponse TheorySetsRewriter::postRewriteMap(TNode n) Assert(n.getKind() == kind::SET_MAP); NodeManager* nm = NodeManager::currentNM(); Kind k = n[1].getKind(); - TypeNode rangeType = n[0].getType().getRangeType(); switch (k) { case SET_EMPTY: { + TypeNode rangeType = n[0].getType().getRangeType(); // (set.map f (as set.empty (Set T1)) = (as set.empty (Set T2)) Node ret = nm->mkConst(EmptySet(nm->mkSetType(rangeType))); return RewriteResponse(REWRITE_DONE, ret); @@ -654,7 +653,7 @@ RewriteResponse TheorySetsRewriter::postRewriteMap(TNode n) { // (set.map f (set.singleton x)) = (set.singleton (f x)) Node mappedElement = nm->mkNode(APPLY_UF, n[0], n[1][0]); - Node ret = nm->mkSingleton(rangeType, mappedElement); + Node ret = nm->mkNode(SET_SINGLETON, mappedElement); return RewriteResponse(REWRITE_AGAIN_FULL, ret); } case SET_UNION: diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 18cbf55c2..174988b48 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -90,8 +90,7 @@ SetEnumerator& SetEnumerator::operator++() // get a new element and return it as a singleton set Node element = *d_elementEnumerator; d_elementsSoFar.push_back(element); - TypeNode elementType = d_elementEnumerator.getType(); - d_currentSet = d_nodeManager->mkSingleton(elementType, element); + d_currentSet = d_nodeManager->mkNode(kind::SET_SINGLETON, element); d_elementEnumerator++; } else diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index fe10f303a..27583e71f 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -19,7 +19,6 @@ #include #include "theory/sets/normal_form.h" -#include "theory/sets/singleton_op.h" #include "util/cardinality.h" namespace cvc5::internal { @@ -118,24 +117,8 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::SET_SINGLETON && n.hasOperator() - && n.getOperator().getKind() == kind::SET_SINGLETON_OP); - - const SetSingletonOp& op = n.getOperator().getConst(); - TypeNode type1 = op.getType(); - if (check) - { - TypeNode type2 = n[0].getType(check); - // the type of the element should be a subtype of the type of the operator - // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int - if (type1 != type2) - { - std::stringstream ss; - ss << "The type '" << type2 << "' of the element is not a type of '" - << type1 << "' in term : " << n; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } + Assert(n.getKind() == kind::SET_SINGLETON); + TypeNode type1 = n[0].getType(check); return nodeManager->mkSetType(type1); } diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index d6f16a79b..ee1fc06c7 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -54,7 +54,7 @@ struct MemberTypeRule }; /** - * Type rule for (set.singleton (SetSingletonOp t) x) to check the sort of x + * Type rule for (set.singleton x) to check the sort of x * matches the sort t. */ struct SingletonTypeRule diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index ff3dced65..2dbc6838e 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -74,9 +74,8 @@ void ArrayCoreSolver::checkNth(const std::vector& nthTerms) Node cond1 = nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n[1]); Node cond2 = nm->mkNode(LT, n[1], nm->mkNode(STRING_LENGTH, n[0])); Node cond = nm->mkNode(AND, cond1, cond2); - TypeNode etn = n.getType().getSequenceElementType(); Node body1 = nm->mkNode( - EQUAL, n, nm->mkSeqUnit(etn, nm->mkNode(SEQ_NTH, n[0], n[1]))); + EQUAL, n, nm->mkNode(SEQ_UNIT, nm->mkNode(SEQ_NTH, n[0], n[1]))); Node body2 = nm->mkNode(EQUAL, n, Word::mkEmptyWord(n.getType())); Node lem = nm->mkNode(ITE, cond, body1, body2); sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_EXTRACT); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 8d9e427ca..b6f0eb956 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -88,15 +88,7 @@ constant CONST_SEQUENCE \ "expr/sequence.h" \ "a sequence of characters" -constant SEQ_UNIT_OP \ - class \ - SeqUnitOp \ - ::cvc5::internal::SeqUnitOpHashFunction \ - "theory/strings/seq_unit_op.h" \ - "operator for sequence units; payload is an instance of the cvc5::internal::SeqUnitOp class" -parameterized SEQ_UNIT SEQ_UNIT_OP 1 \ -"a sequence of length one. First parameter is a SeqUnitOp. Second is a term" - +operator SEQ_UNIT 1 "a sequence of length one. First parameter is a term" operator SEQ_NTH 2 "The nth element of a sequence" # equal equal / less than / output @@ -194,7 +186,6 @@ typerule STRING_TO_LOWER "SimpleTypeRule" ### sequence specific operators typerule CONST_SEQUENCE ::cvc5::internal::theory::strings::ConstSequenceTypeRule -typerule SEQ_UNIT_OP "SimpleTypeRule" typerule SEQ_UNIT ::cvc5::internal::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::cvc5::internal::theory::strings::SeqNthTypeRule diff --git a/src/theory/strings/seq_unit_op.cpp b/src/theory/strings/seq_unit_op.cpp deleted file mode 100644 index 8ecccf3f4..000000000 --- a/src/theory/strings/seq_unit_op.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for sequence unit - */ - -#include "theory/strings/seq_unit_op.h" - -#include - -#include "expr/type_node.h" - -namespace cvc5::internal { - -std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op) -{ - return out << "(SeqUnitOp " << op.getType() << ')'; -} - -size_t SeqUnitOpHashFunction::operator()(const SeqUnitOp& op) const -{ - return std::hash()(op.getType()); -} - -SeqUnitOp::SeqUnitOp(const TypeNode& elementType) - : d_type(new TypeNode(elementType)) -{ -} - -SeqUnitOp::SeqUnitOp(const SeqUnitOp& op) : d_type(new TypeNode(op.getType())) -{ -} - -const TypeNode& SeqUnitOp::getType() const { return *d_type; } - -bool SeqUnitOp::operator==(const SeqUnitOp& op) const -{ - return getType() == op.getType(); -} - -} // namespace cvc5::internal diff --git a/src/theory/strings/seq_unit_op.h b/src/theory/strings/seq_unit_op.h deleted file mode 100644 index 669285448..000000000 --- a/src/theory/strings/seq_unit_op.h +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * A class for sequence unit - */ - -#include "cvc5_public.h" - -#ifndef CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H -#define CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H - -#include - -namespace cvc5::internal { - -class TypeNode; - -/** - * The class is an operator for kind SEQ_UNIT used to construct sequences - * of length one. It specifies the type of the single element especially when it - * is a constant. e.g. the type of rational 1 is Int, however (seq.unit - * (seq_unit_op Real) 1) is of type (Seq Real), not (Seq Int). Note that the - * type passed to the constructor is the element's type, not the sequence type. - */ -class SeqUnitOp -{ - public: - SeqUnitOp(const TypeNode& elementType); - SeqUnitOp(const SeqUnitOp& op); - - /** return the type of the current object */ - const TypeNode& getType() const; - - bool operator==(const SeqUnitOp& op) const; - - private: - SeqUnitOp(); - /** a pointer to the type of the singleton element */ - std::unique_ptr d_type; -}; /* class SeqUnitOp */ - -std::ostream& operator<<(std::ostream& out, const SeqUnitOp& op); - -/** - * Hash function for the SeqUnitOp objects. - */ -struct SeqUnitOpHashFunction -{ - size_t operator()(const SeqUnitOp& op) const; -}; /* struct SeqUnitOpHashFunction */ - -} // namespace cvc5::internal - -#endif /* CVC5__THEORY__STRINGS__SEQ_UNIT_OP_H */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 73d790200..165fedb51 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -466,8 +466,7 @@ bool TheoryStrings::collectModelInfoType( argVal = nfe.d_nf[0][0]; } Assert(!argVal.isNull()) << "No value for " << nfe.d_nf[0][0]; - assignedValue = rewrite( - nm->mkSeqUnit(eqc.getType().getSequenceElementType(), argVal)); + assignedValue = rewrite(nm->mkNode(SEQ_UNIT, argVal)); Trace("strings-model") << "-> assign via seq.unit: " << assignedValue << std::endl; } @@ -521,7 +520,7 @@ bool TheoryStrings::collectModelInfoType( continue; } usedWrites.insert(ivalue); - Node wsunit = nm->mkSeqUnit(etype, w.second); + Node wsunit = nm->mkNode(SEQ_UNIT, w.second); writes.emplace_back(ivalue, wsunit); } // sort based on index value @@ -758,7 +757,7 @@ Node TheoryStrings::mkSkeletonFor(Node c) Node v = bvm->mkBoundVar(snv, etn); // use a skolem, not a bound variable Node kv = sm->mkPurifySkolem(v, "smv"); - skChildren.push_back(nm->mkSeqUnit(etn, kv)); + skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); } return utils::mkConcat(skChildren, c.getType()); } @@ -780,7 +779,7 @@ Node TheoryStrings::mkSkeletonFromBase(Node r, cacheVals.push_back(nm->mkConstInt(Rational(currIndex))); Node kv = sm->mkSkolemFunction( SkolemFunId::SEQ_MODEL_BASE_ELEMENT, etn, cacheVals); - skChildren.push_back(nm->mkSeqUnit(etn, kv)); + skChildren.push_back(nm->mkNode(SEQ_UNIT, kv)); cacheVals.pop_back(); } return utils::mkConcat(skChildren, r.getType()); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1d32a310d..97ab305a8 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -513,7 +513,7 @@ Node StringsPreprocess::reduce(Node t, // nodes for the case where `seq.nth` is defined. Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); - Node unit = nm->mkSeqUnit(t.getType(), skt); + Node unit = nm->mkNode(SEQ_UNIT, skt); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, unit, sk2)); // length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index 01adb7e3a..ae1f3613a 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,7 +19,6 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" -#include "theory/strings/seq_unit_op.h" #include "util/cardinality.h" namespace cvc5::internal { @@ -326,25 +325,9 @@ TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::SEQ_UNIT && n.hasOperator() - && n.getOperator().getKind() == kind::SEQ_UNIT_OP); - - const SeqUnitOp& op = n.getOperator().getConst(); - TypeNode otype = op.getType(); - if (check) - { - TypeNode argType = n[0].getType(check); - // the type of the element should be a subtype of the type of the operator - // e.g. (seq.unit (SeqUnitOp Real) 1) where 1 is an Int - if (argType != otype) - { - std::stringstream ss; - ss << "The type '" << argType << "' of the element is not the type of '" - << otype << "' in term : " << n; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - return nodeManager->mkSequenceType(otype); + Assert(n.getKind() == kind::SEQ_UNIT); + TypeNode argType = n[0].getType(check); + return nodeManager->mkSequenceType(argType); } TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 34488806b..e692e93c4 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -162,8 +162,7 @@ Node mkUnit(TypeNode tn, Node n) return nm->mkNode(STRING_UNIT, n); } Assert(tn.isSequence()); - TypeNode etn = tn.getSequenceElementType(); - return nm->mkSeqUnit(etn, n); + return nm->mkNode(SEQ_UNIT, n); } Node getConstantComponent(Node t) diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index e480db6ca..04099a01b 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -235,11 +235,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_nth) static_cast(std::numeric_limits::max()) + 1); Node s01 = d_nodeManager->mkConst(Sequence(intType, {zero, one})); - Node sx = d_nodeManager->mkSeqUnit(intType, x); - Node sy = d_nodeManager->mkSeqUnit(intType, y); - Node sz = d_nodeManager->mkSeqUnit(intType, z); - Node sw = d_nodeManager->mkSeqUnit(intType, w); - Node sv = d_nodeManager->mkSeqUnit(intType, v); + Node sx = d_nodeManager->mkNode(SEQ_UNIT, x); + Node sy = d_nodeManager->mkNode(SEQ_UNIT, y); + Node sz = d_nodeManager->mkNode(SEQ_UNIT, z); + Node sw = d_nodeManager->mkNode(SEQ_UNIT, w); + Node sv = d_nodeManager->mkNode(SEQ_UNIT, v); Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz); Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv); @@ -435,11 +435,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_update) Node one = d_nodeManager->mkConstInt(1); Node three = d_nodeManager->mkConstInt(3); - Node sx = d_nodeManager->mkSeqUnit(intType, x); - Node sy = d_nodeManager->mkSeqUnit(intType, y); - Node sz = d_nodeManager->mkSeqUnit(intType, z); - Node sw = d_nodeManager->mkSeqUnit(intType, w); - Node sv = d_nodeManager->mkSeqUnit(intType, v); + Node sx = d_nodeManager->mkNode(SEQ_UNIT, x); + Node sy = d_nodeManager->mkNode(SEQ_UNIT, y); + Node sz = d_nodeManager->mkNode(SEQ_UNIT, z); + Node sw = d_nodeManager->mkNode(SEQ_UNIT, w); + Node sv = d_nodeManager->mkNode(SEQ_UNIT, v); Node xyz = d_nodeManager->mkNode(STRING_CONCAT, sx, sy, sz); Node wv = d_nodeManager->mkNode(STRING_CONCAT, sw, sv); diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index e6cc722a3..747d912ca 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -73,15 +73,12 @@ 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->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 negative = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); @@ -109,12 +106,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) 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->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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkNode( + BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5))); + Node z_5 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(5))); Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty); Node output1 = zero; @@ -158,15 +155,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->mkConstInt(Rational(1))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); + Node x_1 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkNode( + BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5))); Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4); Node output2 = x_1; @@ -193,16 +190,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->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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -223,15 +220,12 @@ 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->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 A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(2))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(3))); + Node C = d_nodeManager->mkNode( + BAG_MAKE, elements[2], d_nodeManager->mkConstInt(Rational(4))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // unionDisjointAB is already in a normal form @@ -254,9 +248,8 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) ASSERT_EQ(unionDisjointA_BC, rewrite(unionDisjointAB_C)); Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A); - Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[0], - d_nodeManager->mkConstInt(Rational(4))); + Node AA = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(4))); ASSERT_FALSE(unionDisjointAA.isConst()); ASSERT_TRUE(AA.isConst()); ASSERT_EQ(AA, rewrite(unionDisjointAA)); @@ -277,16 +270,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->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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -315,16 +308,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->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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -350,18 +343,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->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 x_1 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -387,18 +380,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->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 x_1 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node x_3 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(3))); + Node x_7 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(7))); + Node z_2 = d_nodeManager->mkNode( + BAG_MAKE, z, d_nodeManager->mkConstInt(Rational(2))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -423,10 +416,10 @@ 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->mkConstInt(Rational(4))); - Node y_1 = d_nodeManager->mkBag( - d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_CARD, empty); Node output1 = d_nodeManager->mkConstInt(Rational(0)); @@ -459,12 +452,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->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 x_1 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); + Node x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1))); Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty); Node output1 = falseNode; @@ -504,13 +497,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); - Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); - Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); + Node xSingleton = d_nodeManager->mkNode(SET_SINGLETON, x); + Node ySingleton = d_nodeManager->mkNode(SET_SINGLETON, y); - 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_1 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); + Node y_1 = d_nodeManager->mkNode( + BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1))); Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton); Node output2 = x_1; @@ -543,13 +536,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); - Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); - Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y); + Node xSingleton = d_nodeManager->mkNode(SET_SINGLETON, x); + Node ySingleton = d_nodeManager->mkNode(SET_SINGLETON, y); - 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 x_4 = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); + Node y_5 = d_nodeManager->mkNode( + BAG_MAKE, 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 934649755..48a44ecae 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -70,15 +70,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality) Node y = elements[1]; Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType()); - Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d); + Node A = d_nodeManager->mkNode(BAG_MAKE, x, c); + Node B = d_nodeManager->mkNode(BAG_MAKE, y, d); Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node emptyString = d_nodeManager->mkConst(String("")); - Node constantBag = - d_nodeManager->mkBag(d_nodeManager->stringType(), - emptyString, - d_nodeManager->mkConstInt(Rational(1))); + Node constantBag = d_nodeManager->mkNode( + BAG_MAKE, emptyString, d_nodeManager->mkConstInt(Rational(1))); // (= A A) = true where A is a bag Node n1 = A.eqNode(A); @@ -107,15 +105,12 @@ 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->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 negative = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -137,18 +132,14 @@ 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->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 variable = d_nodeManager->mkNode( + BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(-1))); + Node negative = d_nodeManager->mkNode( + BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkNode( + BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkNode( + BAG_MAKE, skolem, d_nodeManager->mkConstInt(Rational(1))); Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); RewriteResponse negativeResponse = d_rewriter->postRewrite(negative); @@ -183,7 +174,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) && response1.d_node == zero); // (bag.count x (bag x c) = c, c > 0 is a constant - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three); + Node bag = d_nodeManager->mkNode(BAG_MAKE, skolem, three); Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); @@ -196,14 +187,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->mkConstInt(Rational(5))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, 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->mkConstInt(Rational(1))); + Node noDuplicate = d_nodeManager->mkNode( + BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); ASSERT_TRUE(response.d_node == noDuplicate && response.d_status == REWRITE_AGAIN_FULL); } @@ -214,12 +205,10 @@ 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->mkConstInt(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConstInt(Rational(n + 1))); + Node A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -298,15 +287,12 @@ 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->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 A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, elements[1], d_nodeManager->mkConstInt(Rational(n + 1))); + Node C = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -359,12 +345,10 @@ 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->mkConstInt(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConstInt(Rational(n + 1))); + Node A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -445,12 +429,10 @@ 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->mkConstInt(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConstInt(Rational(n + 1))); + Node A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -538,12 +520,10 @@ 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->mkConstInt(Rational(n))); - Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), - elements[1], - d_nodeManager->mkConstInt(Rational(n + 1))); + Node A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(n))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, 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); @@ -617,7 +597,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node c = d_nodeManager->mkConstInt(Rational(3)); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); + Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c); // (bag.choose (bag x c)) = x where c is a constant > 0 Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag); @@ -633,14 +613,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node zero = d_nodeManager->mkConstInt(Rational(0)); Node c = d_nodeManager->mkConstInt(Rational(3)); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); + Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c); std::vector elements = getNStrings(2); - 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 A = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(4))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, 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 @@ -662,7 +640,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); + Node bag = d_nodeManager->mkNode(BAG_MAKE, x, c); // (bag.is_singleton (as bag.empty (Bag String)) = false Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); @@ -682,13 +660,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) TEST_F(TestTheoryWhiteBagsRewriter, from_set) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); + Node singleton = d_nodeManager->mkNode(SET_SINGLETON, x); // (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->mkConstInt(Rational(1)); - Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one); + Node bag = d_nodeManager->mkNode(BAG_MAKE, x, one); ASSERT_TRUE(response.d_node == bag && response.d_status == REWRITE_AGAIN_FULL); } @@ -696,13 +674,13 @@ 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->mkConstInt(Rational(5))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, 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); RewriteResponse response = d_rewriter->postRewrite(n); - Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); + Node singleton = d_nodeManager->mkNode(SET_SINGLETON, x); ASSERT_TRUE(response.d_node == singleton && response.d_status == REWRITE_AGAIN_FULL); } @@ -728,10 +706,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->mkConstInt(Rational(3))); - Node B = d_nodeManager->mkBag( - d_nodeManager->stringType(), b, d_nodeManager->mkConstInt(Rational(4))); + Node A = d_nodeManager->mkNode( + BAG_MAKE, a, d_nodeManager->mkConstInt(Rational(3))); + Node B = d_nodeManager->mkNode( + BAG_MAKE, b, d_nodeManager->mkConstInt(Rational(4))); Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); @@ -742,9 +720,8 @@ 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->mkConstInt(Rational(7))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, 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()); @@ -785,7 +762,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) f = d_nodeManager->mkNode(LAMBDA, xy, sum); Node xSkolem = d_nodeManager->getSkolemManager()->mkDummySkolem( "x", d_nodeManager->integerType()); - Node bag = d_nodeManager->mkBag(d_nodeManager->integerType(), xSkolem, n); + Node bag = d_nodeManager->mkNode(BAG_MAKE, xSkolem, n); Node node2 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag); Node apply_f_once = d_nodeManager->mkNode(APPLY_UF, f, xSkolem, one); Node apply_f_twice = @@ -795,7 +772,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold) && response2.d_status == REWRITE_AGAIN_FULL); // (bag.fold (lambda ((x Int)(y Int)) (+ x y)) 1 (bag 10 2)) = 21 - bag = d_nodeManager->mkBag(d_nodeManager->integerType(), ten, n); + bag = d_nodeManager->mkNode(BAG_MAKE, ten, n); Node node3 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag); Node result3 = d_nodeManager->mkConstInt(Rational(21)); Node response3 = Rewriter::rewrite(node3); diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 7f280583b..ed410583a 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -50,9 +50,8 @@ 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->mkConstInt(Rational(100))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(100))); Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag); Node node = d_nodeManager->mkConstInt(Rational(10)); @@ -65,9 +64,8 @@ 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->mkConstInt(Rational(10))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, 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()); @@ -76,15 +74,12 @@ 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->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 negative = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(-1))); + Node zero = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(0))); + Node positive = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(1))); // only positive multiplicity are constants ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative)); @@ -95,8 +90,7 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) { std::vector elements = getNStrings(1); - Node set = - d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); + Node set = d_nodeManager->mkNode(SET_SINGLETON, elements[0]); ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_FROM_SET, set)); ASSERT_TRUE(d_nodeManager->mkNode(BAG_FROM_SET, set).getType().isBag()); } @@ -104,9 +98,8 @@ 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->mkConstInt(Rational(10))); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, 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()); } @@ -114,11 +107,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->mkConstInt(Rational(10))); - Node set = - d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]); + Node bag = d_nodeManager->mkNode( + BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10))); + Node set = d_nodeManager->mkNode(SET_SINGLETON, elements[0]); Node x1 = d_nodeManager->mkBoundVar("x", d_nodeManager->stringType()); Node length = d_nodeManager->mkNode(STRING_LENGTH, x1); diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp index 91b246bb8..3d3bf94d5 100644 --- a/test/unit/theory/theory_sets_rewriter_white.cpp +++ b/test/unit/theory/theory_sets_rewriter_white.cpp @@ -63,8 +63,8 @@ TEST_F(TestTheoryWhiteSetsRewriter, map) Node a = d_nodeManager->mkConst(String("a")); Node b = d_nodeManager->mkConst(String("b")); - Node A = d_nodeManager->mkSingleton(d_nodeManager->stringType(), a); - Node B = d_nodeManager->mkSingleton(d_nodeManager->stringType(), b); + Node A = d_nodeManager->mkNode(SET_SINGLETON, a); + Node B = d_nodeManager->mkNode(SET_SINGLETON, b); Node unionAB = d_nodeManager->mkNode(SET_UNION, A, B); // (set.map @@ -72,7 +72,7 @@ TEST_F(TestTheoryWhiteSetsRewriter, map) // (set.union (set.singleton "a") (set.singleton "b"))) = (set.singleton 1)) Node n2 = d_nodeManager->mkNode(SET_MAP, lambda, unionAB); Node rewritten2 = Rewriter::rewrite(n2); - Node bag = d_nodeManager->mkSingleton(d_nodeManager->integerType(), one); + Node bag = d_nodeManager->mkNode(SET_SINGLETON, one); ASSERT_TRUE(rewritten2 == bag); // - (set.map f (set.union K1 K2)) = diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index c5b8a3bd3..d7a03364c 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,7 +16,6 @@ #include "expr/dtype.h" #include "test_api.h" #include "test_node.h" -#include "theory/sets/singleton_op.h" #include "util/rational.h" using namespace cvc5; @@ -63,22 +62,12 @@ TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term) TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) { - Node singletonInt = - d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->integerType())); - Node singletonReal = - d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->realType())); - Node intConstant = d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1)); - Node realConstant = - d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1, 5)); + Node intConstant = d_nodeManager->mkConstReal(Rational(1)); + Node realConstant = d_nodeManager->mkConstReal(Rational(1, 5)); // (singleton (singleton_op Real) 1) - ASSERT_NO_THROW( - d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant)); - // (singleton (singleton_op Int) (/ 1 5)) - ASSERT_DEATH( - d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant), - "Invalid operands for mkSingleton"); + ASSERT_NO_THROW(d_nodeManager->mkNode(kind::SET_SINGLETON, intConstant)); - Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant); + Node n = d_nodeManager->mkNode(kind::SET_SINGLETON, intConstant); // the type of (singleton (singleton_op Real) 1) is (Set Real) ASSERT_TRUE(n.getType() == d_nodeManager->mkSetType(d_nodeManager->realType())); -- 2.30.2