From ad340126a7adbb9840cca1d082c57b43995987a4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 12 Nov 2021 06:14:49 -0800 Subject: Remove `ConstantMap` (#7635) This is in preparation of having two different kinds (CONST_RATIONAL and CONST_INT) share the same payload. To do so, we cannot rely on ConstantMap anymore to map the payload type to a kind. This commit extends support in the mkmetakind script to deal with such payloads by adding a + suffix to the type. The commit also does some minor refactoring of NodeManager::mkConst() and NodeManager::mkConstInternal() to support setting the kind explicitly. Finally, the commit addresses all instances where mkConst() is used, including the API. --- src/proof/lfsc/lfsc_node_converter.cpp | 42 +++++++++++++++++++++------------- 1 file changed, 26 insertions(+), 16 deletions(-) (limited to 'src/proof/lfsc/lfsc_node_converter.cpp') diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 7ec0b2bd5..33529df39 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -89,7 +89,7 @@ Node LfscNodeConverter::postConvert(Node n) } // bound variable v is (bvar x T) TypeNode intType = nm->integerType(); - Node x = nm->mkConst(Rational(getOrAssignIndexForVar(n))); + Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn); Node bvarOp = getSymbolInternal(k, ftype, "bvar"); @@ -136,7 +136,8 @@ Node LfscNodeConverter::postConvert(Node n) TypeNode intType = nm->integerType(); TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn); Node var = mkInternalSymbol("var", varType); - Node index = nm->mkConst(Rational(getOrAssignIndexForVar(n))); + Node index = + nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n))); Node tc = typeAsNode(convertType(tn)); return nm->mkNode(APPLY_UF, var, index, tc); } @@ -197,7 +198,7 @@ Node LfscNodeConverter::postConvert(Node n) { // use LFSC syntax for mpz negation Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~"); - arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(r.abs())); + arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs())); } else { @@ -343,8 +344,8 @@ Node LfscNodeConverter::postConvert(Node n) Node rop = getSymbolInternal( k, relType, printer::smt2::Smt2Printer::smtKindString(k)); RegExpLoop op = n.getOperator().getConst(); - Node n1 = nm->mkConst(Rational(op.d_loopMinOcc)); - Node n2 = nm->mkConst(Rational(op.d_loopMaxOcc)); + Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc)); + Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc)); return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]); } else if (k == MATCH) @@ -484,14 +485,16 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) else if (k == BITVECTOR_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node w = nm->mkConst(Rational(tn.getBitVectorSize())); + Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize())); tnn = nm->mkNode(APPLY_UF, tnn, w); } else if (k == FLOATINGPOINT_TYPE) { tnn = d_typeKindToNodeCons[k]; - Node e = nm->mkConst(Rational(tn.getFloatingPointExponentSize())); - Node s = nm->mkConst(Rational(tn.getFloatingPointSignificandSize())); + Node e = nm->mkConst(CONST_RATIONAL, + Rational(tn.getFloatingPointExponentSize())); + Node s = nm->mkConst(CONST_RATIONAL, + Rational(tn.getFloatingPointSignificandSize())); tnn = nm->mkNode(APPLY_UF, tnn, e, s); } else if (tn.getNumChildren() == 0) @@ -719,7 +722,8 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector& chars) Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char"); for (unsigned i = 0, size = vec.size(); i < size; i++) { - Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConst(Rational(vec[i]))); + Node cc = nm->mkNode( + APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i]))); chars.push_back(cc); } } @@ -742,36 +746,42 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) case BITVECTOR_EXTRACT: { BitVectorExtract p = n.getConst(); - indices.push_back(nm->mkConst(Rational(p.d_high))); - indices.push_back(nm->mkConst(Rational(p.d_low))); + indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high))); + indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low))); break; } case BITVECTOR_REPEAT: indices.push_back( - nm->mkConst(Rational(n.getConst().d_repeatAmount))); + nm->mkConst(CONST_RATIONAL, + Rational(n.getConst().d_repeatAmount))); break; case BITVECTOR_ZERO_EXTEND: indices.push_back(nm->mkConst( + CONST_RATIONAL, Rational(n.getConst().d_zeroExtendAmount))); break; case BITVECTOR_SIGN_EXTEND: indices.push_back(nm->mkConst( + CONST_RATIONAL, Rational(n.getConst().d_signExtendAmount))); break; case BITVECTOR_ROTATE_LEFT: indices.push_back(nm->mkConst( + CONST_RATIONAL, Rational(n.getConst().d_rotateLeftAmount))); break; case BITVECTOR_ROTATE_RIGHT: indices.push_back(nm->mkConst( + CONST_RATIONAL, Rational(n.getConst().d_rotateRightAmount))); break; case INT_TO_BITVECTOR: - indices.push_back( - nm->mkConst(Rational(n.getConst().d_size))); + indices.push_back(nm->mkConst( + CONST_RATIONAL, Rational(n.getConst().d_size))); break; case IAND: - indices.push_back(nm->mkConst(Rational(n.getConst().d_size))); + indices.push_back( + nm->mkConst(CONST_RATIONAL, Rational(n.getConst().d_size))); break; case APPLY_TESTER: { @@ -1012,7 +1022,7 @@ Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply) Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v) { NodeManager* nm = NodeManager::currentNM(); - Node x = nm->mkConst(Rational(getOrAssignIndexForVar(v))); + Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v))); Node tc = typeAsNode(convertType(v.getType())); return nm->mkNode(APPLY_UF, cop, x, tc); } -- cgit v1.2.3 From cc4a58f5d43c62b72783d4bd1f4f00e6ef9257b4 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 12 Nov 2021 15:33:16 -0600 Subject: bags: Rename kinds with a more consistent naming scheme (#7611) --- src/CMakeLists.txt | 4 +- src/api/cpp/cvc5.cpp | 38 +-- src/api/cpp/cvc5_kind.h | 18 +- src/expr/node_manager.cpp | 6 +- src/parser/parser.cpp | 2 +- src/parser/smt2/smt2.cpp | 18 +- src/printer/smt2/smt2_printer.cpp | 24 +- src/proof/lfsc/lfsc_node_converter.cpp | 6 +- src/theory/bags/bag_make_op.cpp | 50 ++++ src/theory/bags/bag_make_op.h | 63 ++++ src/theory/bags/bag_solver.cpp | 38 +-- src/theory/bags/bag_solver.h | 6 +- src/theory/bags/bags_rewriter.cpp | 233 +++++++-------- src/theory/bags/bags_rewriter.h | 124 ++++---- src/theory/bags/infer_info.h | 1 - src/theory/bags/inference_generator.cpp | 20 +- src/theory/bags/inference_generator.h | 73 ++--- src/theory/bags/kinds | 74 ++--- src/theory/bags/make_bag_op.cpp | 50 ---- src/theory/bags/make_bag_op.h | 63 ---- src/theory/bags/normal_form.cpp | 164 ++++++----- src/theory/bags/normal_form.h | 33 ++- src/theory/bags/rewrites.cpp | 15 +- src/theory/bags/rewrites.h | 14 +- src/theory/bags/solver_state.cpp | 2 +- src/theory/bags/solver_state.h | 3 +- src/theory/bags/theory_bags.cpp | 16 +- src/theory/bags/theory_bags_type_enumerator.cpp | 6 +- src/theory/bags/theory_bags_type_rules.cpp | 48 +-- src/theory/bags/theory_bags_type_rules.h | 20 +- src/theory/inference_id.cpp | 5 +- src/theory/inference_id.h | 2 +- test/regress/regress1/bags/choose1.smt2 | 2 +- test/regress/regress1/bags/choose3.smt2 | 2 +- test/regress/regress1/bags/choose4.smt2 | 2 +- test/regress/regress1/bags/difference_remove1.smt2 | 4 +- test/regress/regress1/bags/duplicate_removal1.smt2 | 4 +- test/regress/regress1/bags/duplicate_removal2.smt2 | 6 +- test/regress/regress1/bags/emptybag1.smt2 | 2 +- test/regress/regress1/bags/fuzzy1.smt2 | 2 +- test/regress/regress1/bags/fuzzy2.smt2 | 8 +- test/regress/regress1/bags/fuzzy3.smt2 | 2 +- test/regress/regress1/bags/fuzzy4.smt2 | 4 +- test/regress/regress1/bags/fuzzy5.smt2 | 2 +- test/regress/regress1/bags/intersection_min1.smt2 | 4 +- test/regress/regress1/bags/intersection_min2.smt2 | 6 +- test/regress/regress1/bags/issue5759.smt2 | 4 +- test/regress/regress1/bags/map1.smt2 | 4 +- test/regress/regress1/bags/map3.smt2 | 2 +- test/regress/regress1/bags/subbag1.smt2 | 4 +- test/regress/regress1/bags/subbag2.smt2 | 4 +- test/regress/regress1/bags/union_disjoint.smt2 | 4 +- test/regress/regress1/bags/union_max1.smt2 | 4 +- test/regress/regress1/bags/union_max2.smt2 | 6 +- test/unit/theory/theory_bags_normal_form_white.cpp | 173 +++++------ test/unit/theory/theory_bags_rewriter_white.cpp | 326 +++++++++++---------- test/unit/theory/theory_bags_type_rules_white.cpp | 10 +- 57 files changed, 930 insertions(+), 900 deletions(-) create mode 100644 src/theory/bags/bag_make_op.cpp create mode 100644 src/theory/bags/bag_make_op.h delete mode 100644 src/theory/bags/make_bag_op.cpp delete mode 100644 src/theory/bags/make_bag_op.h (limited to 'src/proof/lfsc/lfsc_node_converter.cpp') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4d90ae742..58ccd288c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -529,6 +529,8 @@ 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 @@ -541,8 +543,6 @@ libcvc5_add_sources( theory/bags/inference_generator.h theory/bags/inference_manager.cpp theory/bags/inference_manager.h - theory/bags/make_bag_op.cpp - theory/bags/make_bag_op.h theory/bags/normal_form.cpp theory/bags/normal_form.h theory/bags/rewrites.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 39277b7e8..e1a2a547c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -296,16 +296,16 @@ const static std::unordered_map s_kinds{ {RELATION_JOIN_IMAGE, cvc5::Kind::RELATION_JOIN_IMAGE}, {RELATION_IDEN, cvc5::Kind::RELATION_IDEN}, /* Bags ---------------------------------------------------------------- */ - {UNION_MAX, cvc5::Kind::UNION_MAX}, - {UNION_DISJOINT, cvc5::Kind::UNION_DISJOINT}, - {INTERSECTION_MIN, cvc5::Kind::INTERSECTION_MIN}, - {DIFFERENCE_SUBTRACT, cvc5::Kind::DIFFERENCE_SUBTRACT}, - {DIFFERENCE_REMOVE, cvc5::Kind::DIFFERENCE_REMOVE}, - {SUBBAG, cvc5::Kind::SUBBAG}, + {BAG_UNION_MAX, cvc5::Kind::BAG_UNION_MAX}, + {BAG_UNION_DISJOINT, cvc5::Kind::BAG_UNION_DISJOINT}, + {BAG_INTER_MIN, cvc5::Kind::BAG_INTER_MIN}, + {BAG_DIFFERENCE_SUBTRACT, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT}, + {BAG_DIFFERENCE_REMOVE, cvc5::Kind::BAG_DIFFERENCE_REMOVE}, + {BAG_SUBBAG, cvc5::Kind::BAG_SUBBAG}, {BAG_COUNT, cvc5::Kind::BAG_COUNT}, - {DUPLICATE_REMOVAL, cvc5::Kind::DUPLICATE_REMOVAL}, - {MK_BAG, cvc5::Kind::MK_BAG}, - {EMPTYBAG, cvc5::Kind::EMPTYBAG}, + {BAG_DUPLICATE_REMOVAL, cvc5::Kind::BAG_DUPLICATE_REMOVAL}, + {BAG_MAKE, cvc5::Kind::BAG_MAKE}, + {BAG_EMPTY, cvc5::Kind::BAG_EMPTY}, {BAG_CARD, cvc5::Kind::BAG_CARD}, {BAG_CHOOSE, cvc5::Kind::BAG_CHOOSE}, {BAG_IS_SINGLETON, cvc5::Kind::BAG_IS_SINGLETON}, @@ -606,16 +606,16 @@ const static std::unordered_map {cvc5::Kind::RELATION_JOIN_IMAGE, RELATION_JOIN_IMAGE}, {cvc5::Kind::RELATION_IDEN, RELATION_IDEN}, /* Bags ------------------------------------------------------------ */ - {cvc5::Kind::UNION_MAX, UNION_MAX}, - {cvc5::Kind::UNION_DISJOINT, UNION_DISJOINT}, - {cvc5::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, - {cvc5::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, - {cvc5::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, - {cvc5::Kind::SUBBAG, SUBBAG}, + {cvc5::Kind::BAG_UNION_MAX, BAG_UNION_MAX}, + {cvc5::Kind::BAG_UNION_DISJOINT, BAG_UNION_DISJOINT}, + {cvc5::Kind::BAG_INTER_MIN, BAG_INTER_MIN}, + {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_SUBTRACT}, + {cvc5::Kind::BAG_DIFFERENCE_REMOVE, BAG_DIFFERENCE_REMOVE}, + {cvc5::Kind::BAG_SUBBAG, BAG_SUBBAG}, {cvc5::Kind::BAG_COUNT, BAG_COUNT}, - {cvc5::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL}, - {cvc5::Kind::MK_BAG, MK_BAG}, - {cvc5::Kind::EMPTYBAG, EMPTYBAG}, + {cvc5::Kind::BAG_DUPLICATE_REMOVAL, BAG_DUPLICATE_REMOVAL}, + {cvc5::Kind::BAG_MAKE, BAG_MAKE}, + {cvc5::Kind::BAG_EMPTY, BAG_EMPTY}, {cvc5::Kind::BAG_CARD, BAG_CARD}, {cvc5::Kind::BAG_CHOOSE, BAG_CHOOSE}, {cvc5::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, @@ -5219,7 +5219,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const // element type can be used safely here. res = getNodeManager()->mkSingleton(type, *children[0].d_node); } - else if (kind == api::MK_BAG) + else if (kind == api::BAG_MAKE) { // the type of the term is the same as the type of the internal node // see Term::getSort() diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index c0c269be2..8da58ebd6 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2352,7 +2352,7 @@ enum Kind : int32_t * Create with: * mkEmptyBag(const Sort& sort) */ - EMPTYBAG, + BAG_EMPTY, /** * Bag max union. * Parameters: @@ -2362,7 +2362,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - UNION_MAX, + BAG_UNION_MAX, /** * Bag disjoint union (sum). * @@ -2373,7 +2373,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - UNION_DISJOINT, + BAG_UNION_DISJOINT, /** * Bag intersection (min). * @@ -2384,7 +2384,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - INTERSECTION_MIN, + BAG_INTER_MIN, /** * Bag difference subtract (subtracts multiplicities of the second from the * first). @@ -2396,7 +2396,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - DIFFERENCE_SUBTRACT, + BAG_DIFFERENCE_SUBTRACT, /** * Bag difference 2 (removes shared elements in the two bags). * @@ -2407,7 +2407,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - DIFFERENCE_REMOVE, + BAG_DIFFERENCE_REMOVE, /** * Inclusion predicate for bags * (multiplicities of the first bag <= multiplicities of the second bag). @@ -2419,7 +2419,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - SUBBAG, + BAG_SUBBAG, /** * Element multiplicity in a bag * @@ -2442,7 +2442,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - DUPLICATE_REMOVAL, + BAG_DUPLICATE_REMOVAL, /** * The bag of the single element given as a parameter. * @@ -2452,7 +2452,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - MK_BAG, + BAG_MAKE, /** * Bag cardinality. * diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6f614e927..62c718245 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -30,7 +30,7 @@ #include "expr/node_manager_attributes.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" -#include "theory/bags/make_bag_op.h" +#include "theory/bags/bag_make_op.h" #include "theory/sets/singleton_op.h" #include "util/abstract_value.h" #include "util/bitvector.h" @@ -1044,8 +1044,8 @@ Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) << "Invalid operands for mkBag. The type '" << n.getType() << "' of node '" << n << "' is not a subtype of '" << t << "'." << std::endl; - Node op = mkConst(MakeBagOp(t)); - Node bag = mkNode(kind::MK_BAG, op, n, m); + Node op = mkConst(BagMakeOp(t)); + Node bag = mkNode(kind::BAG_MAKE, op, n, m); return bag; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 570f1369a..c94e39748 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -534,7 +534,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { t = d_solver->mkEmptySet(s); } - else if (k == api::EMPTYBAG) + else if (k == api::BAG_EMPTY) { t = d_solver->mkEmptyBag(s); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b4f39a315..30dcd06cc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -612,16 +612,16 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (d_logic.isTheoryEnabled(theory::THEORY_BAGS)) { - defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort())); - addOperator(api::UNION_MAX, "union_max"); - addOperator(api::UNION_DISJOINT, "union_disjoint"); - addOperator(api::INTERSECTION_MIN, "intersection_min"); - addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract"); - addOperator(api::DIFFERENCE_REMOVE, "difference_remove"); - addOperator(api::SUBBAG, "subbag"); + defineVar("bag.empty", d_solver->mkEmptyBag(d_solver->getNullSort())); + addOperator(api::BAG_UNION_MAX, "bag.union_max"); + addOperator(api::BAG_UNION_DISJOINT, "bag.union_disjoint"); + addOperator(api::BAG_INTER_MIN, "bag.inter_min"); + addOperator(api::BAG_DIFFERENCE_SUBTRACT, "bag.difference_subtract"); + addOperator(api::BAG_DIFFERENCE_REMOVE, "bag.difference_remove"); + addOperator(api::BAG_SUBBAG, "bag.subbag"); addOperator(api::BAG_COUNT, "bag.count"); - addOperator(api::DUPLICATE_REMOVAL, "duplicate_removal"); - addOperator(api::MK_BAG, "bag"); + addOperator(api::BAG_DUPLICATE_REMOVAL, "bag.duplicate_removal"); + addOperator(api::BAG_MAKE, "bag"); addOperator(api::BAG_CARD, "bag.card"); addOperator(api::BAG_CHOOSE, "bag.choose"); addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8ed4929e5..07ad0b2c2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -336,8 +336,8 @@ void Smt2Printer::toStream(std::ostream& out, out << ")"; break; - case kind::EMPTYBAG: - out << "(as emptybag "; + case kind::BAG_EMPTY: + out << "(as bag.empty "; toStreamType(out, n.getConst().getType()); out << ")"; break; @@ -701,9 +701,9 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SET_UNIVERSE: out << "(as set.universe " << n.getType() << ")"; break; // bags - case kind::MK_BAG: + case kind::BAG_MAKE: { - // print (bag (mkBag_op Real) 1 3) as (bag 1.0 3) + // print (bag (BAG_MAKE_OP Real) 1 3) as (bag 1.0 3) out << smtKindString(k, d_variant) << " "; TypeNode elemType = n.getType().getBagElementType(); toStreamCastToType( @@ -1082,15 +1082,15 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) // bag theory case kind::BAG_TYPE: return "Bag"; - case kind::UNION_MAX: return "union_max"; - case kind::UNION_DISJOINT: return "union_disjoint"; - case kind::INTERSECTION_MIN: return "intersection_min"; - case kind::DIFFERENCE_SUBTRACT: return "difference_subtract"; - case kind::DIFFERENCE_REMOVE: return "difference_remove"; - case kind::SUBBAG: return "subbag"; + case kind::BAG_UNION_MAX: return "bag.union_max"; + case kind::BAG_UNION_DISJOINT: return "bag.union_disjoint"; + case kind::BAG_INTER_MIN: return "bag.inter_min"; + case kind::BAG_DIFFERENCE_SUBTRACT: return "bag.difference_subtract"; + case kind::BAG_DIFFERENCE_REMOVE: return "bag.difference_remove"; + case kind::BAG_SUBBAG: return "bag.subbag"; case kind::BAG_COUNT: return "bag.count"; - case kind::DUPLICATE_REMOVAL: return "duplicate_removal"; - case kind::MK_BAG: return "bag"; + case kind::BAG_DUPLICATE_REMOVAL: return "bag.duplicate_removal"; + case kind::BAG_MAKE: return "bag"; case kind::BAG_CARD: return "bag.card"; case kind::BAG_CHOOSE: return "bag.choose"; case kind::BAG_IS_SINGLETON: return "bag.is_singleton"; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 33529df39..7f1d9e192 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -307,7 +307,7 @@ Node LfscNodeConverter::postConvert(Node n) children.insert(children.end(), n.begin(), n.end()); return nm->mkNode(APPLY_UF, children); } - else if (k == SET_EMPTY || k == SET_UNIVERSE || k == EMPTYBAG) + else if (k == SET_EMPTY || k == SET_UNIVERSE || k == BAG_EMPTY) { Node t = typeAsNode(convertType(tn)); TypeNode etype = nm->mkFunctionType(d_sortType, tn); @@ -315,7 +315,7 @@ Node LfscNodeConverter::postConvert(Node n) k, etype, k == SET_EMPTY ? "set.empty" - : (k == SET_UNIVERSE ? "set.universe" : "emptybag")); + : (k == SET_UNIVERSE ? "set.universe" : "bag.empty")); return nm->mkNode(APPLY_UF, ef, t); } else if (n.isClosure()) @@ -933,7 +933,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) ret = maybeMkSkolemFun(op, macroApply); Assert(!ret.isNull()); } - else if (k == SET_SINGLETON || k == MK_BAG) + else if (k == SET_SINGLETON || k == BAG_MAKE) { if (!macroApply) { diff --git a/src/theory/bags/bag_make_op.cpp b/src/theory/bags/bag_make_op.cpp new file mode 100644 index 000000000..786267976 --- /dev/null +++ b/src/theory/bags/bag_make_op.cpp @@ -0,0 +1,50 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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 { + +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 diff --git a/src/theory/bags/bag_make_op.h b/src/theory/bags/bag_make_op.h new file mode 100644 index 000000000..e4a7e9e8f --- /dev/null +++ b/src/theory/bags/bag_make_op.h @@ -0,0 +1,63 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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 { + +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 + +#endif /* CVC5__BAG_MAKE_OP_H */ diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index c2d73d625..444878574 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -69,14 +69,14 @@ void BagSolver::postCheck() Kind k = n.getKind(); switch (k) { - case kind::EMPTYBAG: checkEmpty(n); break; - case kind::MK_BAG: checkMkBag(n); break; - case kind::UNION_DISJOINT: checkUnionDisjoint(n); break; - case kind::UNION_MAX: checkUnionMax(n); break; - case kind::INTERSECTION_MIN: checkIntersectionMin(n); break; - case kind::DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break; - case kind::DIFFERENCE_REMOVE: checkDifferenceRemove(n); break; - case kind::DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break; + case kind::BAG_EMPTY: checkEmpty(n); break; + case kind::BAG_MAKE: checkBagMake(n); break; + case kind::BAG_UNION_DISJOINT: checkUnionDisjoint(n); break; + case kind::BAG_UNION_MAX: checkUnionMax(n); break; + case kind::BAG_INTER_MIN: checkIntersectionMin(n); break; + case kind::BAG_DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break; + case kind::BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(n); break; + case kind::BAG_DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break; case kind::BAG_MAP: checkMap(n); break; default: break; } @@ -112,7 +112,7 @@ set BagSolver::getElementsForBinaryOperator(const Node& n) void BagSolver::checkEmpty(const Node& n) { - Assert(n.getKind() == EMPTYBAG); + Assert(n.getKind() == BAG_EMPTY); for (const Node& e : d_state.getElements(n)) { InferInfo i = d_ig.empty(n, e); @@ -122,7 +122,7 @@ void BagSolver::checkEmpty(const Node& n) void BagSolver::checkUnionDisjoint(const Node& n) { - Assert(n.getKind() == UNION_DISJOINT); + Assert(n.getKind() == BAG_UNION_DISJOINT); std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { @@ -133,7 +133,7 @@ void BagSolver::checkUnionDisjoint(const Node& n) void BagSolver::checkUnionMax(const Node& n) { - Assert(n.getKind() == UNION_MAX); + Assert(n.getKind() == BAG_UNION_MAX); std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { @@ -144,7 +144,7 @@ void BagSolver::checkUnionMax(const Node& n) void BagSolver::checkIntersectionMin(const Node& n) { - Assert(n.getKind() == INTERSECTION_MIN); + Assert(n.getKind() == BAG_INTER_MIN); std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { @@ -155,7 +155,7 @@ void BagSolver::checkIntersectionMin(const Node& n) void BagSolver::checkDifferenceSubtract(const Node& n) { - Assert(n.getKind() == DIFFERENCE_SUBTRACT); + Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT); std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { @@ -164,15 +164,15 @@ void BagSolver::checkDifferenceSubtract(const Node& n) } } -void BagSolver::checkMkBag(const Node& n) +void BagSolver::checkBagMake(const Node& n) { - Assert(n.getKind() == MK_BAG); + Assert(n.getKind() == BAG_MAKE); Trace("bags::BagSolver::postCheck") - << "BagSolver::checkMkBag Elements of " << n + << "BagSolver::checkBagMake Elements of " << n << " are: " << d_state.getElements(n) << std::endl; for (const Node& e : d_state.getElements(n)) { - InferInfo i = d_ig.mkBag(n, e); + InferInfo i = d_ig.bagMake(n, e); d_im.lemmaTheoryInference(&i); } } @@ -184,7 +184,7 @@ void BagSolver::checkNonNegativeCountTerms(const Node& bag, const Node& element) void BagSolver::checkDifferenceRemove(const Node& n) { - Assert(n.getKind() == DIFFERENCE_REMOVE); + Assert(n.getKind() == BAG_DIFFERENCE_REMOVE); std::set elements = getElementsForBinaryOperator(n); for (const Node& e : elements) { @@ -195,7 +195,7 @@ void BagSolver::checkDifferenceRemove(const Node& n) void BagSolver::checkDuplicateRemoval(Node n) { - Assert(n.getKind() == DUPLICATE_REMOVAL); + Assert(n.getKind() == BAG_DUPLICATE_REMOVAL); set elements; const set& downwards = d_state.getElements(n); const set& upwards = d_state.getElements(n[0]); diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 9155c93d0..45a20e055 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -46,15 +46,15 @@ class BagSolver : protected EnvObj /** apply inference rules for empty bags */ void checkEmpty(const Node& n); /** - * apply inference rules for MK_BAG operator. + * apply inference rules for BAG_MAKE operator. * Example: Suppose n = (bag x c), and we have two count terms (bag.count x n) * and (bag.count y n). * This function will add inferences for the count terms as documented in - * InferenceGenerator::mkBag. + * InferenceGenerator::bagMake. * Note that element y may not be in bag n. See the documentation of * SolverState::getElements. */ - void checkMkBag(const Node& n); + void checkBagMake(const Node& n); /** * @param n is a bag that has the form (op A B) * @return the set union of known elements in (op A B) , A, and B. diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 31c33b901..f9cc990f4 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -75,14 +75,16 @@ RewriteResponse BagsRewriter::postRewrite(TNode n) Kind k = n.getKind(); switch (k) { - case MK_BAG: response = rewriteMakeBag(n); break; + case BAG_MAKE: response = rewriteMakeBag(n); break; case BAG_COUNT: response = rewriteBagCount(n); break; - case DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break; - case UNION_MAX: response = rewriteUnionMax(n); break; - case UNION_DISJOINT: response = rewriteUnionDisjoint(n); break; - case INTERSECTION_MIN: response = rewriteIntersectionMin(n); break; - case DIFFERENCE_SUBTRACT: response = rewriteDifferenceSubtract(n); break; - case DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break; + case BAG_DUPLICATE_REMOVAL: response = rewriteDuplicateRemoval(n); break; + case BAG_UNION_MAX: response = rewriteUnionMax(n); break; + case BAG_UNION_DISJOINT: response = rewriteUnionDisjoint(n); break; + case BAG_INTER_MIN: response = rewriteIntersectionMin(n); break; + case BAG_DIFFERENCE_SUBTRACT: + response = rewriteDifferenceSubtract(n); + break; + case BAG_DIFFERENCE_REMOVE: response = rewriteDifferenceRemove(n); break; case BAG_CARD: response = rewriteCard(n); break; case BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break; case BAG_FROM_SET: response = rewriteFromSet(n); break; @@ -113,7 +115,7 @@ RewriteResponse BagsRewriter::preRewrite(TNode n) switch (k) { case EQUAL: response = preRewriteEqual(n); break; - case SUBBAG: response = rewriteSubBag(n); break; + case BAG_SUBBAG: response = rewriteSubBag(n); break; default: response = BagsRewriteResponse(n, Rewrite::NONE); } @@ -144,24 +146,24 @@ BagsRewriteResponse BagsRewriter::preRewriteEqual(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteSubBag(const TNode& n) const { - Assert(n.getKind() == SUBBAG); + Assert(n.getKind() == BAG_SUBBAG); - // (bag.is_included A B) = ((difference_subtract A B) == emptybag) + // (bag.subbag A B) = ((bag.difference_subtract A B) == bag.empty) Node emptybag = d_nm->mkConst(EmptyBag(n[0].getType())); - Node subtract = d_nm->mkNode(DIFFERENCE_SUBTRACT, n[0], n[1]); + Node subtract = d_nm->mkNode(BAG_DIFFERENCE_SUBTRACT, n[0], n[1]); Node equal = subtract.eqNode(emptybag); return BagsRewriteResponse(equal, Rewrite::SUB_BAG); } BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const { - Assert(n.getKind() == MK_BAG); - // return emptybag for negative or zero multiplicity + Assert(n.getKind() == BAG_MAKE); + // return bag.empty for negative or zero multiplicity if (n[1].isConst() && n[1].getConst().sgn() != 1) { - // (mkBag x c) = emptybag where c <= 0 + // (bag x c) = bag.empty where c <= 0 Node emptybag = d_nm->mkConst(EmptyBag(n.getType())); - return BagsRewriteResponse(emptybag, Rewrite::MK_BAG_COUNT_NEGATIVE); + return BagsRewriteResponse(emptybag, Rewrite::BAG_MAKE_COUNT_NEGATIVE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -169,68 +171,68 @@ BagsRewriteResponse BagsRewriter::rewriteMakeBag(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const { Assert(n.getKind() == BAG_COUNT); - if (n[1].isConst() && n[1].getKind() == EMPTYBAG) + if (n[1].isConst() && n[1].getKind() == BAG_EMPTY) { - // (bag.count x emptybag) = 0 + // (bag.count x bag.empty) = 0 return BagsRewriteResponse(d_zero, Rewrite::COUNT_EMPTY); } - if (n[1].getKind() == MK_BAG && n[0] == n[1][0]) + if (n[1].getKind() == BAG_MAKE && n[0] == n[1][0]) { - // (bag.count x (mkBag x c)) = (ite (>= c 1) c 0) + // (bag.count x (bag x c)) = (ite (>= c 1) c 0) Node c = n[1][1]; Node geq = d_nm->mkNode(GEQ, c, d_one); Node ite = d_nm->mkNode(ITE, geq, c, d_zero); - return BagsRewriteResponse(ite, Rewrite::COUNT_MK_BAG); + return BagsRewriteResponse(ite, Rewrite::COUNT_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const { - Assert(n.getKind() == DUPLICATE_REMOVAL); - if (n[0].getKind() == MK_BAG && n[0][1].isConst() + Assert(n.getKind() == BAG_DUPLICATE_REMOVAL); + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst().sgn() == 1) { - // (duplicate_removal (mkBag x n)) = (mkBag x 1) + // (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); - return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_MK_BAG); + return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const { - Assert(n.getKind() == UNION_MAX); - if (n[1].getKind() == EMPTYBAG || n[0] == n[1]) + Assert(n.getKind() == BAG_UNION_MAX); + if (n[1].getKind() == BAG_EMPTY || n[0] == n[1]) { - // (union_max A A) = A - // (union_max A emptybag) = A + // (bag.union_max A A) = A + // (bag.union_max A bag.empty) = A return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_SAME_OR_EMPTY); } - if (n[0].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY) { - // (union_max emptybag A) = A + // (bag.union_max bag.empty A) = A return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_EMPTY); } - if ((n[1].getKind() == UNION_MAX || n[1].getKind() == UNION_DISJOINT) + if ((n[1].getKind() == BAG_UNION_MAX || n[1].getKind() == BAG_UNION_DISJOINT) && (n[0] == n[1][0] || n[0] == n[1][1])) { - // (union_max A (union_max A B)) = (union_max A B) - // (union_max A (union_max B A)) = (union_max B A) - // (union_max A (union_disjoint A B)) = (union_disjoint A B) - // (union_max A (union_disjoint B A)) = (union_disjoint B A) + // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) return BagsRewriteResponse(n[1], Rewrite::UNION_MAX_UNION_LEFT); } - if ((n[0].getKind() == UNION_MAX || n[0].getKind() == UNION_DISJOINT) + if ((n[0].getKind() == BAG_UNION_MAX || n[0].getKind() == BAG_UNION_DISJOINT) && (n[0][0] == n[1] || n[0][1] == n[1])) { - // (union_max (union_max A B) A)) = (union_max A B) - // (union_max (union_max B A) A)) = (union_max B A) - // (union_max (union_disjoint A B) A)) = (union_disjoint A B) - // (union_max (union_disjoint B A) A)) = (union_disjoint B A) + // (bag.union_max (bag.union_max A B) A)) = (bag.union_max A B) + // (bag.union_max (bag.union_max B A) A)) = (bag.union_max B A) + // (bag.union_max (bag.union_disjoint A B) A)) = (bag.union_disjoint A B) + // (bag.union_max (bag.union_disjoint B A) A)) = (bag.union_disjoint B A) return BagsRewriteResponse(n[0], Rewrite::UNION_MAX_UNION_RIGHT); } return BagsRewriteResponse(n, Rewrite::NONE); @@ -238,29 +240,30 @@ BagsRewriteResponse BagsRewriter::rewriteUnionMax(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const { - Assert(n.getKind() == UNION_DISJOINT); - if (n[1].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_UNION_DISJOINT); + if (n[1].getKind() == BAG_EMPTY) { - // (union_disjoint A emptybag) = A + // (bag.union_disjoint A bag.empty) = A return BagsRewriteResponse(n[0], Rewrite::UNION_DISJOINT_EMPTY_RIGHT); } - if (n[0].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY) { - // (union_disjoint emptybag A) = A + // (bag.union_disjoint bag.empty A) = A return BagsRewriteResponse(n[1], Rewrite::UNION_DISJOINT_EMPTY_LEFT); } - if ((n[0].getKind() == UNION_MAX && n[1].getKind() == INTERSECTION_MIN) - || (n[1].getKind() == UNION_MAX && n[0].getKind() == INTERSECTION_MIN)) + if ((n[0].getKind() == BAG_UNION_MAX && n[1].getKind() == BAG_INTER_MIN) + || (n[1].getKind() == BAG_UNION_MAX && n[0].getKind() == BAG_INTER_MIN)) { - // (union_disjoint (union_max A B) (intersection_min A B)) = - // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) - // check if the operands of union_max and intersection_min are the same + // (bag.union_disjoint (bag.union_max A B) (bag.inter_min A B)) = + // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + // check if the operands of bag.union_max and bag.inter_min are the + // same std::set left(n[0].begin(), n[0].end()); std::set right(n[1].begin(), n[1].end()); if (left == right) { - Node rewritten = d_nm->mkNode(UNION_DISJOINT, n[0][0], n[0][1]); + Node rewritten = d_nm->mkNode(BAG_UNION_DISJOINT, n[0][0], n[0][1]); return BagsRewriteResponse(rewritten, Rewrite::UNION_DISJOINT_MAX_MIN); } } @@ -269,42 +272,42 @@ BagsRewriteResponse BagsRewriter::rewriteUnionDisjoint(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const { - Assert(n.getKind() == INTERSECTION_MIN); - if (n[0].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_INTER_MIN); + if (n[0].getKind() == BAG_EMPTY) { - // (intersection_min emptybag A) = emptybag + // (bag.inter_min bag.empty A) = bag.empty return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_EMPTY_LEFT); } - if (n[1].getKind() == EMPTYBAG) + if (n[1].getKind() == BAG_EMPTY) { - // (intersection_min A emptybag) = emptybag + // (bag.inter_min A bag.empty) = bag.empty return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_EMPTY_RIGHT); } if (n[0] == n[1]) { - // (intersection_min A A) = A + // (bag.inter_min A A) = A return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SAME); } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (intersection_min A (union_disjoint A B)) = A - // (intersection_min A (union_disjoint B A)) = A - // (intersection_min A (union_max A B)) = A - // (intersection_min A (union_max B A)) = A + // (bag.inter_min A (bag.union_disjoint A B)) = A + // (bag.inter_min A (bag.union_disjoint B A)) = A + // (bag.inter_min A (bag.union_max A B)) = A + // (bag.inter_min A (bag.union_max B A)) = A return BagsRewriteResponse(n[0], Rewrite::INTERSECTION_SHARED_LEFT); } } - if (n[0].getKind() == UNION_DISJOINT || n[0].getKind() == UNION_MAX) + if (n[0].getKind() == BAG_UNION_DISJOINT || n[0].getKind() == BAG_UNION_MAX) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (intersection_min (union_disjoint A B) A) = A - // (intersection_min (union_disjoint B A) A) = A - // (intersection_min (union_max A B) A) = A - // (intersection_min (union_max B A) A) = A + // (bag.inter_min (bag.union_disjoint A B) A) = A + // (bag.inter_min (bag.union_disjoint B A) A) = A + // (bag.inter_min (bag.union_max A B) A) = A + // (bag.inter_min (bag.union_max B A) A) = A return BagsRewriteResponse(n[1], Rewrite::INTERSECTION_SHARED_RIGHT); } } @@ -315,55 +318,55 @@ BagsRewriteResponse BagsRewriter::rewriteIntersectionMin(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract( const TNode& n) const { - Assert(n.getKind() == DIFFERENCE_SUBTRACT); - if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) + Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT); + if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY) { - // (difference_subtract A emptybag) = A - // (difference_subtract emptybag A) = emptybag + // (bag.difference_subtract A bag.empty) = A + // (bag.difference_subtract bag.empty A) = bag.empty return BagsRewriteResponse(n[0], Rewrite::SUBTRACT_RETURN_LEFT); } if (n[0] == n[1]) { - // (difference_subtract A A) = emptybag + // (bag.difference_subtract A A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_SAME); } - if (n[0].getKind() == UNION_DISJOINT) + if (n[0].getKind() == BAG_UNION_DISJOINT) { if (n[1] == n[0][0]) { - // (difference_subtract (union_disjoint A B) A) = B + // (bag.difference_subtract (bag.union_disjoint A B) A) = B return BagsRewriteResponse(n[0][1], Rewrite::SUBTRACT_DISJOINT_SHARED_LEFT); } if (n[1] == n[0][1]) { - // (difference_subtract (union_disjoint B A) A) = B + // (bag.difference_subtract (bag.union_disjoint B A) A) = B return BagsRewriteResponse(n[0][0], Rewrite::SUBTRACT_DISJOINT_SHARED_RIGHT); } } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (difference_subtract A (union_disjoint A B)) = emptybag - // (difference_subtract A (union_disjoint B A)) = emptybag - // (difference_subtract A (union_max A B)) = emptybag - // (difference_subtract A (union_max B A)) = emptybag + // (bag.difference_subtract A (bag.union_disjoint A B)) = bag.empty + // (bag.difference_subtract A (bag.union_disjoint B A)) = bag.empty + // (bag.difference_subtract A (bag.union_max A B)) = bag.empty + // (bag.difference_subtract A (bag.union_max B A)) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_FROM_UNION); } } - if (n[0].getKind() == INTERSECTION_MIN) + if (n[0].getKind() == BAG_INTER_MIN) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (difference_subtract (intersection_min A B) A) = emptybag - // (difference_subtract (intersection_min B A) A) = emptybag + // (bag.difference_subtract (bag.inter_min A B) A) = bag.empty + // (bag.difference_subtract (bag.inter_min B A) A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::SUBTRACT_MIN); } @@ -374,41 +377,41 @@ BagsRewriteResponse BagsRewriter::rewriteDifferenceSubtract( BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const { - Assert(n.getKind() == DIFFERENCE_REMOVE); + Assert(n.getKind() == BAG_DIFFERENCE_REMOVE); - if (n[0].getKind() == EMPTYBAG || n[1].getKind() == EMPTYBAG) + if (n[0].getKind() == BAG_EMPTY || n[1].getKind() == BAG_EMPTY) { - // (difference_remove A emptybag) = A - // (difference_remove emptybag B) = emptybag + // (bag.difference_remove A bag.empty) = A + // (bag.difference_remove bag.empty B) = bag.empty return BagsRewriteResponse(n[0], Rewrite::REMOVE_RETURN_LEFT); } if (n[0] == n[1]) { - // (difference_remove A A) = emptybag + // (bag.difference_remove A A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_SAME); } - if (n[1].getKind() == UNION_DISJOINT || n[1].getKind() == UNION_MAX) + if (n[1].getKind() == BAG_UNION_DISJOINT || n[1].getKind() == BAG_UNION_MAX) { if (n[0] == n[1][0] || n[0] == n[1][1]) { - // (difference_remove A (union_disjoint A B)) = emptybag - // (difference_remove A (union_disjoint B A)) = emptybag - // (difference_remove A (union_max A B)) = emptybag - // (difference_remove A (union_max B A)) = emptybag + // (bag.difference_remove A (bag.union_disjoint A B)) = bag.empty + // (bag.difference_remove A (bag.union_disjoint B A)) = bag.empty + // (bag.difference_remove A (bag.union_max A B)) = bag.empty + // (bag.difference_remove A (bag.union_max B A)) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_FROM_UNION); } } - if (n[0].getKind() == INTERSECTION_MIN) + if (n[0].getKind() == BAG_INTER_MIN) { if (n[1] == n[0][0] || n[1] == n[0][1]) { - // (difference_remove (intersection_min A B) A) = emptybag - // (difference_remove (intersection_min B A) A) = emptybag + // (bag.difference_remove (bag.inter_min A B) A) = bag.empty + // (bag.difference_remove (bag.inter_min B A) A) = bag.empty Node emptyBag = d_nm->mkConst(EmptyBag(n.getType())); return BagsRewriteResponse(emptyBag, Rewrite::REMOVE_MIN); } @@ -420,11 +423,11 @@ BagsRewriteResponse BagsRewriter::rewriteDifferenceRemove(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const { Assert(n.getKind() == BAG_CHOOSE); - if (n[0].getKind() == MK_BAG && n[0][1].isConst() + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst() > 0) { - // (bag.choose (mkBag x c)) = x where c is a constant > 0 - return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_MK_BAG); + // (bag.choose (bag x c)) = x where c is a constant > 0 + return BagsRewriteResponse(n[0][0], Rewrite::CHOOSE_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -432,15 +435,15 @@ BagsRewriteResponse BagsRewriter::rewriteChoose(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const { Assert(n.getKind() == BAG_CARD); - if (n[0].getKind() == MK_BAG && n[0][1].isConst()) + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst()) { - // (bag.card (mkBag x c)) = c where c is a constant > 0 - return BagsRewriteResponse(n[0][1], Rewrite::CARD_MK_BAG); + // (bag.card (bag x c)) = c where c is a constant > 0 + return BagsRewriteResponse(n[0][1], Rewrite::CARD_BAG_MAKE); } - if (n[0].getKind() == UNION_DISJOINT) + if (n[0].getKind() == BAG_UNION_DISJOINT) { - // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) + // (bag.card (bag.union-disjoint A B)) = (+ (bag.card A) (bag.card B)) Node A = d_nm->mkNode(BAG_CARD, n[0][0]); Node B = d_nm->mkNode(BAG_CARD, n[0][1]); Node plus = d_nm->mkNode(PLUS, A, B); @@ -453,11 +456,11 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const { Assert(n.getKind() == BAG_IS_SINGLETON); - if (n[0].getKind() == MK_BAG) + if (n[0].getKind() == BAG_MAKE) { - // (bag.is_singleton (mkBag x c)) = (c == 1) + // (bag.is_singleton (bag x c)) = (c == 1) Node equal = n[0][1].eqNode(d_one); - return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_MK_BAG); + return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -467,7 +470,7 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const Assert(n.getKind() == BAG_FROM_SET); if (n[0].getKind() == SET_SINGLETON) { - // (bag.from_set (set.singleton (singleton_op Int) x)) = (mkBag x 1) + // (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); return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); @@ -478,10 +481,10 @@ BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const { Assert(n.getKind() == BAG_TO_SET); - if (n[0].getKind() == MK_BAG && n[0][1].isConst() + if (n[0].getKind() == BAG_MAKE && n[0][1].isConst() && n[0][1].getConst().sgn() == 1) { - // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // (bag.to_set (bag x n)) = (set.singleton (SetSingletonOp T) 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]); return BagsRewriteResponse(set, Rewrite::TO_SINGLETON); @@ -518,7 +521,7 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const Assert(n.getKind() == kind::BAG_MAP); if (n[1].isConst()) { - // (bag.map f emptybag) = emptybag + // (bag.map f bag.empty) = bag.empty // (bag.map f (bag "a" 3)) = (bag (f "a") 3) std::map elements = NormalForm::getBagElements(n[1]); std::map mappedElements; @@ -536,19 +539,19 @@ BagsRewriteResponse BagsRewriter::postRewriteMap(const TNode& n) const Kind k = n[1].getKind(); switch (k) { - case MK_BAG: + case BAG_MAKE: { 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]); - return BagsRewriteResponse(ret, Rewrite::MAP_MK_BAG); + return BagsRewriteResponse(ret, Rewrite::MAP_BAG_MAKE); } - case UNION_DISJOINT: + case BAG_UNION_DISJOINT: { Node a = d_nm->mkNode(BAG_MAP, n[1][0]); Node b = d_nm->mkNode(BAG_MAP, n[1][1]); - Node ret = d_nm->mkNode(UNION_DISJOINT, a, b); + Node ret = d_nm->mkNode(BAG_UNION_DISJOINT, a, b); return BagsRewriteResponse(ret, Rewrite::MAP_UNION_DISJOINT); } diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 3edd5af32..36958a491 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -45,14 +45,14 @@ class BagsRewriter : public TheoryRewriter BagsRewriter(HistogramStat* statistics = nullptr); /** - * postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT, - * INTERSECTION_MIN, DIFFERENCE_SUBTRACT, DIFFERENCE_REMOVE, BAG_CHOOSE, - * BAG_CARD, BAG_IS_SINGLETON. - * See the rewrite rules for these kinds below. + * postRewrite nodes with kinds: BAG_MAKE, BAG_COUNT, BAG_UNION_MAX, + * BAG_UNION_DISJOINT, BAG_INTER_MIN, BAG_DIFFERENCE_SUBTRACT, + * BAG_DIFFERENCE_REMOVE, BAG_CHOOSE, BAG_CARD, BAG_IS_SINGLETON. See the + * rewrite rules for these kinds below. */ RewriteResponse postRewrite(TNode n) override; /** - * preRewrite nodes with kinds: EQUAL, SUBBAG. + * preRewrite nodes with kinds: EQUAL, BGA_SUBBAG. * See the rewrite rules for these kinds below. */ RewriteResponse preRewrite(TNode n) override; @@ -66,14 +66,14 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.is_included A B) = ((difference_subtract A B) == emptybag) + * - (bag.subbag A B) = ((bag.difference_subtract A B) == bag.empty) */ BagsRewriteResponse rewriteSubBag(const TNode& n) const; /** * rewrites for n include: - * - (bag x 0) = (emptybag T) where T is the type of x - * - (bag x (-c)) = (emptybag T) where T is the type of x, and c > 0 is a + * - (bag x 0) = (bag.empty T) where T is the type of x + * - (bag x (-c)) = (bag.empty T) where T is the type of x, and c > 0 is a * constant * - otherwise = n */ @@ -81,7 +81,7 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.count x emptybag) = 0 + * - (bag.count x bag.empty) = 0 * - (bag.count x (bag x c)) = (ite (>= c 1) c 0) * - otherwise = n */ @@ -89,85 +89,85 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (duplicate_removal (bag x n)) = (bag x 1) + * - (bag.duplicate_removal (bag x n)) = (bag x 1) * where n is a positive constant */ BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const; /** * rewrites for n include: - * - (union_max A emptybag) = A - * - (union_max emptybag A) = A - * - (union_max A A) = A - * - (union_max A (union_max A B)) = (union_max A B) - * - (union_max A (union_max B A)) = (union_max B A) - * - (union_max (union_max A B) A) = (union_max A B) - * - (union_max (union_max B A) A) = (union_max B A) - * - (union_max A (union_disjoint A B)) = (union_disjoint A B) - * - (union_max A (union_disjoint B A)) = (union_disjoint B A) - * - (union_max (union_disjoint A B) A) = (union_disjoint A B) - * - (union_max (union_disjoint B A) A) = (union_disjoint B A) + * - (bag.union_max A bag.empty) = A + * - (bag.union_max bag.empty A) = A + * - (bag.union_max A A) = A + * - (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + * - (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + * - (bag.union_max (bag.union_max A B) A) = (bag.union_max A B) + * - (bag.union_max (bag.union_max B A) A) = (bag.union_max B A) + * - (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + * - (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) + * - (bag.union_max (bag.union_disjoint A B) A) = (bag.union_disjoint A B) + * - (bag.union_max (bag.union_disjoint B A) A) = (bag.union_disjoint B A) * - otherwise = n */ BagsRewriteResponse rewriteUnionMax(const TNode& n) const; /** * rewrites for n include: - * - (union_disjoint A emptybag) = A - * - (union_disjoint emptybag A) = A - * - (union_disjoint (union_max A B) (intersection_min A B)) = - * (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + * - (bag.union_disjoint A bag.empty) = A + * - (bag.union_disjoint bag.empty A) = A + * - (bag.union_disjoint (bag.union_max A B) (bag.inter_min A B)) = + * (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) * - other permutations of the above like swapping A and B, or swapping - * intersection_min and union_max + * bag.intersection_min and bag.union_max * - otherwise = n */ BagsRewriteResponse rewriteUnionDisjoint(const TNode& n) const; /** * rewrites for n include: - * - (intersection_min A emptybag) = emptybag - * - (intersection_min emptybag A) = emptybag - * - (intersection_min A A) = A - * - (intersection_min A (union_disjoint A B)) = A - * - (intersection_min A (union_disjoint B A)) = A - * - (intersection_min (union_disjoint A B) A) = A - * - (intersection_min (union_disjoint B A) A) = A - * - (intersection_min A (union_max A B)) = A - * - (intersection_min A (union_max B A)) = A - * - (intersection_min (union_max A B) A) = A - * - (intersection_min (union_max B A) A) = A + * - (bag.inter_min A bag.empty) = bag.empty + * - (bag.inter_min bag.empty A) = bag.empty + * - (bag.inter_min A A) = A + * - (bag.inter_min A (bag.union_disjoint A B)) = A + * - (bag.inter_min A (bag.union_disjoint B A)) = A + * - (bag.inter_min (bag.union_disjoint A B) A) = A + * - (bag.inter_min (bag.union_disjoint B A) A) = A + * - (bag.inter_min A (bag.union_max A B)) = A + * - (bag.inter_min A (bag.union_max B A)) = A + * - (bag.inter_min (bag.union_max A B) A) = A + * - (bag.inter_min (bag.union_max B A) A) = A * - otherwise = n */ BagsRewriteResponse rewriteIntersectionMin(const TNode& n) const; /** * rewrites for n include: - * - (difference_subtract A emptybag) = A - * - (difference_subtract emptybag A) = emptybag - * - (difference_subtract A A) = emptybag - * - (difference_subtract (union_disjoint A B) A) = B - * - (difference_subtract (union_disjoint B A) A) = B - * - (difference_subtract A (union_disjoint A B)) = emptybag - * - (difference_subtract A (union_disjoint B A)) = emptybag - * - (difference_subtract A (union_max A B)) = emptybag - * - (difference_subtract A (union_max B A)) = emptybag - * - (difference_subtract (intersection_min A B) A) = emptybag - * - (difference_subtract (intersection_min B A) A) = emptybag + * - (bag.difference_subtract A bag.empty) = A + * - (bag.difference_subtract bag.empty A) = bag.empty + * - (bag.difference_subtract A A) = bag.empty + * - (bag.difference_subtract (bag.union_disjoint A B) A) = B + * - (bag.difference_subtract (bag.union_disjoint B A) A) = B + * - (bag.difference_subtract A (bag.union_disjoint A B)) = bag.empty + * - (bag.difference_subtract A (bag.union_disjoint B A)) = bag.empty + * - (bag.difference_subtract A (bag.union_max A B)) = bag.empty + * - (bag.difference_subtract A (bag.union_max B A)) = bag.empty + * - (bag.difference_subtract (bag.inter_min A B) A) = bag.empty + * - (bag.difference_subtract (bag.inter_min B A) A) = bag.empty * - otherwise = n */ BagsRewriteResponse rewriteDifferenceSubtract(const TNode& n) const; /** * rewrites for n include: - * - (difference_remove A emptybag) = A - * - (difference_remove emptybag A) = emptybag - * - (difference_remove A A) = emptybag - * - (difference_remove A (union_disjoint A B)) = emptybag - * - (difference_remove A (union_disjoint B A)) = emptybag - * - (difference_remove A (union_max A B)) = emptybag - * - (difference_remove A (union_max B A)) = emptybag - * - (difference_remove (intersection_min A B) A) = emptybag - * - (difference_remove (intersection_min B A) A) = emptybag + * - (bag.difference_remove A bag.empty) = A + * - (bag.difference_remove bag.empty A) = bag.empty + * - (bag.difference_remove A A) = bag.empty + * - (bag.difference_remove A (bag.union_disjoint A B)) = bag.empty + * - (bag.difference_remove A (bag.union_disjoint B A)) = bag.empty + * - (bag.difference_remove A (bag.union_max A B)) = bag.empty + * - (bag.difference_remove A (bag.union_max B A)) = bag.empty + * - (bag.difference_remove (bag.inter_min A B) A) = bag.empty + * - (bag.difference_remove (bag.inter_min B A) A) = bag.empty * - otherwise = n */ BagsRewriteResponse rewriteDifferenceRemove(const TNode& n) const; @@ -193,13 +193,13 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.from_set (singleton (singleton_op Int) x)) = (bag x 1) + * - (bag.from_set (singleton (SetSingletonOp Int) x)) = (bag x 1) */ BagsRewriteResponse rewriteFromSet(const TNode& n) const; /** * rewrites for n include: - * - (bag.to_set (bag x n)) = (singleton (singleton_op T) x) + * - (bag.to_set (bag x n)) = (singleton (SetSingletonOp T) x) * where n is a positive constant and T is the type of the bag's elements */ BagsRewriteResponse rewriteToSet(const TNode& n) const; @@ -214,11 +214,11 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.map (lambda ((x U)) t) emptybag) = emptybag + * - (bag.map (lambda ((x U)) t) bag.empty) = bag.empty * - (bag.map (lambda ((x U)) t) (bag y z)) = (bag (apply (lambda ((x U)) t) * y) z) - * - (bag.map (lambda ((x U)) t) (union_disjoint A B)) = - * (union_disjoint + * - (bag.map (lambda ((x U)) t) (bag.union_disjoint A B)) = + * (bag.union_disjoint * (bag ((lambda ((x U)) t) "a") 3) * (bag ((lambda ((x U)) t) "b") 4)) * diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index b0519993b..4fde553f0 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -32,7 +32,6 @@ class TheoryInferenceManager; namespace bags { - /** * An inference. This is a class to track an unprocessed call to either * send a fact, lemma, or conflict that is waiting to be asserted to the diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index c65f5ccc2..a433ceb2d 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -53,9 +53,9 @@ InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) return inferInfo; } -InferInfo InferenceGenerator::mkBag(Node n, Node e) +InferInfo InferenceGenerator::bagMake(Node n, Node e) { - Assert(n.getKind() == MK_BAG); + Assert(n.getKind() == BAG_MAKE); Assert(e.getType() == n.getType().getBagElementType()); /* @@ -65,7 +65,7 @@ InferInfo InferenceGenerator::mkBag(Node n, Node e) */ Node x = n[0]; Node c = n[1]; - InferInfo inferInfo(d_im, InferenceId::BAGS_MK_BAG); + InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE); Node same = d_nm->mkNode(EQUAL, e, x); Node geq = d_nm->mkNode(GEQ, c, d_one); Node andNode = same.andNode(geq); @@ -141,7 +141,7 @@ Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo) InferInfo InferenceGenerator::empty(Node n, Node e) { - Assert(n.getKind() == EMPTYBAG); + Assert(n.getKind() == BAG_EMPTY); Assert(e.getType() == n.getType().getBagElementType()); InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY); @@ -155,7 +155,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e) InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) { - Assert(n.getKind() == UNION_DISJOINT && n[0].getType().isBag()); + Assert(n.getKind() == BAG_UNION_DISJOINT && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; @@ -177,7 +177,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) InferInfo InferenceGenerator::unionMax(Node n, Node e) { - Assert(n.getKind() == UNION_MAX && n[0].getType().isBag()); + Assert(n.getKind() == BAG_UNION_MAX && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; @@ -200,7 +200,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e) InferInfo InferenceGenerator::intersection(Node n, Node e) { - Assert(n.getKind() == INTERSECTION_MIN && n[0].getType().isBag()); + Assert(n.getKind() == BAG_INTER_MIN && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; @@ -221,7 +221,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e) InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) { - Assert(n.getKind() == DIFFERENCE_SUBTRACT && n[0].getType().isBag()); + Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; @@ -243,7 +243,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) InferInfo InferenceGenerator::differenceRemove(Node n, Node e) { - Assert(n.getKind() == DIFFERENCE_REMOVE && n[0].getType().isBag()); + Assert(n.getKind() == BAG_DIFFERENCE_REMOVE && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; @@ -265,7 +265,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e) InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e) { - Assert(n.getKind() == DUPLICATE_REMOVAL && n[0].getType().isBag()); + Assert(n.getKind() == BAG_DUPLICATE_REMOVAL && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 391a352bd..8ed3ead38 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -56,108 +56,109 @@ class InferenceGenerator * (= (bag.count e skolem) 0)) * where skolem = (bag x c) is a fresh variable */ - InferInfo mkBag(Node n, Node e); + InferInfo bagMake(Node n, Node e); /** * @param n is (= A B) where A, B are bags of type (Bag E), and * (not (= A B)) is an assertion in the equality engine * @return an inference that represents the following implication * (=> * (not (= A B)) - * (not (= (count e A) (count e B)))) + * (not (= (bag.count e A) (bag.count e B)))) * where e is a fresh skolem of type E. */ InferInfo bagDisequality(Node n); /** - * @param n is (as emptybag (Bag E)) + * @param n is (as bag.empty (Bag E)) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true - * (= 0 (count e skolem))) - * where skolem = (as emptybag (Bag String)) + * (= 0 (bag.count e skolem))) + * where skolem = (as bag.empty (Bag E)) */ InferInfo empty(Node n, Node e); /** - * @param n is (union_disjoint A B) where A, B are bags of type (Bag E) + * @param n is (bag.union_disjoint A B) where A, B are bags of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true - * (= (count e skolem) - * (+ (count e A) (count e B)))) - * where skolem is a fresh variable equals (union_disjoint A B) + * (= (bag.count e skolem) + * (+ (bag.count e A) (bag.count e B)))) + * where skolem is a fresh variable equals (bag.union_disjoint A B) */ InferInfo unionDisjoint(Node n, Node e); /** - * @param n is (union_disjoint A B) where A, B are bags of type (Bag E) + * @param n is (bag.union_disjoint A B) where A, B are bags of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true * (= - * (count e skolem) + * (bag.count e skolem) * (ite - * (> (count e A) (count e B)) - * (count e A) - * (count e B))))) - * where skolem is a fresh variable equals (union_max A B) + * (> (bag.count e A) (bag.count e B)) + * (bag.count e A) + * (bag.count e B))))) + * where skolem is a fresh variable equals (bag.union_max A B) */ InferInfo unionMax(Node n, Node e); /** - * @param n is (intersection_min A B) where A, B are bags of type (Bag E) + * @param n is (bag.inter_min A B) where A, B are bags of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true * (= - * (count e skolem) + * (bag.count e skolem) * (ite( - * (< (count e A) (count e B)) - * (count e A) - * (count e B))))) - * where skolem is a fresh variable equals (intersection_min A B) + * (< (bag.count e A) (bag.count e B)) + * (bag.count e A) + * (bag.count e B))))) + * where skolem is a fresh variable equals (bag.inter_min A B) */ InferInfo intersection(Node n, Node e); /** - * @param n is (difference_subtract A B) where A, B are bags of type (Bag E) + * @param n is (bag.difference_subtract A B) where A, B are bags of type + * (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true * (= - * (count e skolem) + * (bag.count e skolem) * (ite - * (>= (count e A) (count e B)) - * (- (count e A) (count e B)) + * (>= (bag.count e A) (bag.count e B)) + * (- (bag.count e A) (bag.count e B)) * 0)))) - * where skolem is a fresh variable equals (difference_subtract A B) + * where skolem is a fresh variable equals (bag.difference_subtract A B) */ InferInfo differenceSubtract(Node n, Node e); /** - * @param n is (difference_remove A B) where A, B are bags of type (Bag E) + * @param n is (bag.difference_remove A B) where A, B are bags of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true * (= - * (count e skolem) + * (bag.count e skolem) * (ite - * (<= (count e B) 0) - * (count e A) + * (<= (bag.count e B) 0) + * (bag.count e A) * 0)))) - * where skolem is a fresh variable equals (difference_remove A B) + * where skolem is a fresh variable equals (bag.difference_remove A B) */ InferInfo differenceRemove(Node n, Node e); /** - * @param n is (duplicate_removal A) where A is a bag of type (Bag E) + * @param n is (bag.duplicate_removal A) where A is a bag of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> * true * (= - * (count e skolem) - * (ite (>= (count e A) 1) 1 0)))) - * where skolem is a fresh variable equals (duplicate_removal A) + * (bag.count e skolem) + * (ite (>= (bag.count e A) 1) 1 0)))) + * where skolem is a fresh variable equals (bag.duplicate_removal A) */ InferInfo duplicateRemoval(Node n, Node e); /** @@ -171,7 +172,7 @@ class InferenceGenerator * (>= preImageSize 0) * (forall ((i Int)) * (let ((uf_i (uf i))) - * (let ((count_uf_i (bag.count uf_i A))) + * (let ((bag.count_uf_i (bag.count uf_i A))) * (=> * (and (>= i 1) (<= i preImageSize)) * (and diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 55fd28695..a5c6e75bf 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -15,7 +15,7 @@ properties parametric properties check presolve # constants -constant EMPTYBAG \ +constant BAG_EMPTY \ class \ EmptyBag \ ::cvc5::EmptyBagHashFunction \ @@ -36,27 +36,27 @@ enumerator BAG_TYPE \ "theory/bags/theory_bags_type_enumerator.h" # operators -operator UNION_MAX 2 "union for bags (max)" -operator UNION_DISJOINT 2 "disjoint union for bags (sum)" -operator INTERSECTION_MIN 2 "bag intersection (min)" +operator BAG_UNION_MAX 2 "union for bags (max)" +operator BAG_UNION_DISJOINT 2 "disjoint union for bags (sum)" +operator BAG_INTER_MIN 2 "bag intersection (min)" -# {("a", 2), ("b", 3)} \ {("a", 1)} = {("a", 1), ("b", 3)} -operator DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicities)" +# {|("a", 2), ("b", 3)} \ {("a", 1)|} = {|("a", 1), ("b", 3)|} +operator BAG_DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicities)" -# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)} -operator DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)" +# {|("a", 2), ("b", 3)} \\ {("a", 1)|} = {|("b", 3)|} +operator BAG_DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)" -operator SUBBAG 2 "inclusion predicate for bags (less than or equal multiplicities)" -operator BAG_COUNT 2 "multiplicity of an element in a bag" -operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" +operator BAG_SUBBAG 2 "inclusion predicate for bags (less than or equal multiplicities)" +operator BAG_COUNT 2 "multiplicity of an element in a bag" +operator BAG_DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" -constant MK_BAG_OP \ +constant BAG_MAKE_OP \ class \ - MakeBagOp \ - ::cvc5::MakeBagOpHashFunction \ - "theory/bags/make_bag_op.h" \ - "operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class" -parameterized MK_BAG MK_BAG_OP 2 \ + BagMakeOp \ + ::cvc5::BagMakeOpHashFunction \ + "theory/bags/bag_make_op.h" \ + "operator for BAG_MAKE; payload is an instance of the cvc5::BagMakeOp class" +parameterized BAG_MAKE BAG_MAKE_OP 2 \ "constructs a bag from one element along with its multiplicity" # The operator bag-is-singleton returns whether the given bag is a singleton @@ -76,25 +76,25 @@ operator BAG_CHOOSE 1 "return an element in the bag given as a parameter # of the second argument, a bag of type (Bag T1), and returns a bag of type (Bag T2). operator BAG_MAP 2 "bag map function" -typerule UNION_MAX ::cvc5::theory::bags::BinaryOperatorTypeRule -typerule UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule -typerule INTERSECTION_MIN ::cvc5::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule -typerule DIFFERENCE_REMOVE ::cvc5::theory::bags::BinaryOperatorTypeRule -typerule SUBBAG ::cvc5::theory::bags::SubBagTypeRule -typerule BAG_COUNT ::cvc5::theory::bags::CountTypeRule -typerule DUPLICATE_REMOVAL ::cvc5::theory::bags::DuplicateRemovalTypeRule -typerule MK_BAG_OP "SimpleTypeRule" -typerule MK_BAG ::cvc5::theory::bags::MkBagTypeRule -typerule EMPTYBAG ::cvc5::theory::bags::EmptyBagTypeRule -typerule BAG_CARD ::cvc5::theory::bags::CardTypeRule -typerule BAG_CHOOSE ::cvc5::theory::bags::ChooseTypeRule -typerule BAG_IS_SINGLETON ::cvc5::theory::bags::IsSingletonTypeRule -typerule BAG_FROM_SET ::cvc5::theory::bags::FromSetTypeRule -typerule BAG_TO_SET ::cvc5::theory::bags::ToSetTypeRule -typerule BAG_MAP ::cvc5::theory::bags::BagMapTypeRule - -construle UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule -construle MK_BAG ::cvc5::theory::bags::MkBagTypeRule +typerule BAG_UNION_MAX ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule BAG_UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule BAG_INTER_MIN ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule BAG_DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule BAG_DIFFERENCE_REMOVE ::cvc5::theory::bags::BinaryOperatorTypeRule +typerule BAG_SUBBAG ::cvc5::theory::bags::SubBagTypeRule +typerule BAG_COUNT ::cvc5::theory::bags::CountTypeRule +typerule BAG_DUPLICATE_REMOVAL ::cvc5::theory::bags::DuplicateRemovalTypeRule +typerule BAG_MAKE_OP "SimpleTypeRule" +typerule BAG_MAKE ::cvc5::theory::bags::BagMakeTypeRule +typerule BAG_EMPTY ::cvc5::theory::bags::EmptyBagTypeRule +typerule BAG_CARD ::cvc5::theory::bags::CardTypeRule +typerule BAG_CHOOSE ::cvc5::theory::bags::ChooseTypeRule +typerule BAG_IS_SINGLETON ::cvc5::theory::bags::IsSingletonTypeRule +typerule BAG_FROM_SET ::cvc5::theory::bags::FromSetTypeRule +typerule BAG_TO_SET ::cvc5::theory::bags::ToSetTypeRule +typerule BAG_MAP ::cvc5::theory::bags::BagMapTypeRule + +construle BAG_UNION_DISJOINT ::cvc5::theory::bags::BinaryOperatorTypeRule +construle BAG_MAKE ::cvc5::theory::bags::BagMakeTypeRule endtheory diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp deleted file mode 100644 index c03b21236..000000000 --- a/src/theory/bags/make_bag_op.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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 MK_BAG operator. - */ - -#include "make_bag_op.h" - -#include - -#include "expr/type_node.h" - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) -{ - return out << "(mkBag_op " << op.getType() << ')'; -} - -size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const -{ - return std::hash()(op.getType()); -} - -MakeBagOp::MakeBagOp(const TypeNode& elementType) - : d_type(new TypeNode(elementType)) -{ -} - -MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType())) -{ -} - -const TypeNode& MakeBagOp::getType() const { return *d_type; } - -bool MakeBagOp::operator==(const MakeBagOp& op) const -{ - return getType() == op.getType(); -} - -} // namespace cvc5 diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h deleted file mode 100644 index 4756009ae..000000000 --- a/src/theory/bags/make_bag_op.h +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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 MK_BAG operator. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__MAKE_BAG_OP_H -#define CVC5__MAKE_BAG_OP_H - -#include - -namespace cvc5 { - -class TypeNode; - -/** - * The class is an operator for kind MK_BAG 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 - * (mkBag (mkBag_op 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 MakeBagOp -{ - public: - explicit MakeBagOp(const TypeNode& elementType); - MakeBagOp(const MakeBagOp& op); - - /** return the type of the current object */ - const TypeNode& getType() const; - - bool operator==(const MakeBagOp& op) const; - - private: - /** a pointer to the type of the bag element */ - std::unique_ptr d_type; -}; /* class MakeBagOp */ - -std::ostream& operator<<(std::ostream& out, const MakeBagOp& op); - -/** - * Hash function for the MakeBagOpHashFunction objects. - */ -struct MakeBagOpHashFunction -{ - size_t operator()(const MakeBagOp& op) const; -}; /* struct MakeBagOpHashFunction */ - -} // namespace cvc5 - -#endif /* CVC5__MAKE_BAG_OP_H */ diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 69d76bd88..12bf513b5 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -28,19 +28,19 @@ namespace bags { bool NormalForm::isConstant(TNode n) { - if (n.getKind() == EMPTYBAG) + if (n.getKind() == BAG_EMPTY) { // empty bags are already normalized return true; } - if (n.getKind() == MK_BAG) + if (n.getKind() == BAG_MAKE) { // see the implementation in MkBagTypeRule::computeIsConst return n.isConst(); } - if (n.getKind() == UNION_DISJOINT) + if (n.getKind() == BAG_UNION_DISJOINT) { - if (!(n[0].getKind() == kind::MK_BAG && n[0].isConst())) + if (!(n[0].getKind() == kind::BAG_MAKE && n[0].isConst())) { // the first child is not a constant return false; @@ -48,9 +48,9 @@ bool NormalForm::isConstant(TNode n) // store the previous element to check the ordering of elements Node previousElement = n[0][0]; Node current = n[1]; - while (current.getKind() == UNION_DISJOINT) + while (current.getKind() == BAG_UNION_DISJOINT) { - if (!(current[0].getKind() == kind::MK_BAG && current[0].isConst())) + if (!(current[0].getKind() == kind::BAG_MAKE && current[0].isConst())) { // the current element is not a constant return false; @@ -64,7 +64,7 @@ bool NormalForm::isConstant(TNode n) current = current[1]; } // check last element - if (!(current.getKind() == kind::MK_BAG && current.isConst())) + if (!(current.getKind() == kind::BAG_MAKE && current.isConst())) { // the last element is not a constant return false; @@ -77,7 +77,7 @@ bool NormalForm::isConstant(TNode n) return true; } - // only nodes with kinds EMPTY_BAG, MK_BAG, and UNION_DISJOINT can be + // only nodes with kinds EMPTY_BAG, BAG_MAKE, and BAG_UNION_DISJOINT can be // constants return false; } @@ -97,14 +97,14 @@ Node NormalForm::evaluate(TNode n) } switch (n.getKind()) { - case MK_BAG: return evaluateMakeBag(n); + case BAG_MAKE: return evaluateMakeBag(n); case BAG_COUNT: return evaluateBagCount(n); - case DUPLICATE_REMOVAL: return evaluateDuplicateRemoval(n); - case UNION_DISJOINT: return evaluateUnionDisjoint(n); - case UNION_MAX: return evaluateUnionMax(n); - case INTERSECTION_MIN: return evaluateIntersectionMin(n); - case DIFFERENCE_SUBTRACT: return evaluateDifferenceSubtract(n); - case DIFFERENCE_REMOVE: return evaluateDifferenceRemove(n); + case BAG_DUPLICATE_REMOVAL: return evaluateDuplicateRemoval(n); + case BAG_UNION_DISJOINT: return evaluateUnionDisjoint(n); + case BAG_UNION_MAX: return evaluateUnionMax(n); + case BAG_INTER_MIN: return evaluateIntersectionMin(n); + case BAG_DIFFERENCE_SUBTRACT: return evaluateDifferenceSubtract(n); + case BAG_DIFFERENCE_REMOVE: return evaluateDifferenceRemove(n); case BAG_CARD: return evaluateCard(n); case BAG_IS_SINGLETON: return evaluateIsSingleton(n); case BAG_FROM_SET: return evaluateFromSet(n); @@ -172,19 +172,19 @@ std::map NormalForm::getBagElements(TNode n) Assert(n.isConst()) << "node " << n << " is not in a normal form" << std::endl; std::map elements; - if (n.getKind() == EMPTYBAG) + if (n.getKind() == BAG_EMPTY) { return elements; } - while (n.getKind() == kind::UNION_DISJOINT) + while (n.getKind() == kind::BAG_UNION_DISJOINT) { - Assert(n[0].getKind() == kind::MK_BAG); + Assert(n[0].getKind() == kind::BAG_MAKE); Node element = n[0][0]; Rational count = n[0][1].getConst(); elements[element] = count; n = n[1]; } - Assert(n.getKind() == kind::MK_BAG); + Assert(n.getKind() == kind::BAG_MAKE); Node lastElement = n[0]; Rational lastCount = n[1].getConst(); elements[lastElement] = lastCount; @@ -210,7 +210,7 @@ Node NormalForm::constructConstantBagFromElements( Node n = nm->mkBag(elementType, it->first, nm->mkConst(CONST_RATIONAL, it->second)); - bag = nm->mkNode(UNION_DISJOINT, n, bag); + bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag); } return bag; } @@ -230,7 +230,7 @@ Node NormalForm::constructBagFromElements(TypeNode t, while (++it != elements.rend()) { Node n = nm->mkBag(elementType, it->first, it->second); - bag = nm->mkNode(UNION_DISJOINT, n, bag); + bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag); } return bag; } @@ -239,7 +239,7 @@ Node NormalForm::evaluateMakeBag(TNode n) { // the case where n is const should be handled earlier. // here we handle the case where the multiplicity is zero or negative - Assert(n.getKind() == MK_BAG && !n.isConst() + Assert(n.getKind() == BAG_MAKE && !n.isConst() && n[1].getConst().sgn() < 1); Node emptybag = NodeManager::currentNM()->mkConst(EmptyBag(n.getType())); return emptybag; @@ -250,11 +250,11 @@ Node NormalForm::evaluateBagCount(TNode n) Assert(n.getKind() == BAG_COUNT); // Examples // -------- - // - (bag.count "x" (emptybag String)) = 0 - // - (bag.count "x" (mkBag "y" 5)) = 0 - // - (bag.count "x" (mkBag "x" 4)) = 4 - // - (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4 - // - (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0 + // - (bag.count "x" (as bag.empty (Bag String))) = 0 + // - (bag.count "x" (bag "y" 5)) = 0 + // - (bag.count "x" (bag "x" 4)) = 4 + // - (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4 + // - (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0 std::map elements = getBagElements(n[1]); std::map::iterator it = elements.find(n[0]); @@ -270,14 +270,15 @@ Node NormalForm::evaluateBagCount(TNode n) Node NormalForm::evaluateDuplicateRemoval(TNode n) { - Assert(n.getKind() == DUPLICATE_REMOVAL); + Assert(n.getKind() == BAG_DUPLICATE_REMOVAL); // Examples // -------- - // - (duplicate_removal (emptybag String)) = (emptybag String) - // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1) - // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1) + // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // String)) + // - (bag.duplicate_removal (bag "x" 4)) = (bag "x" 1) + // - (bag.duplicate_removal (bag.disjoint_union (bag "x" 3) (bag "y" 5)) = + // (bag.disjoint_union (bag "x" 1) (bag "y" 1) std::map oldElements = getBagElements(n[0]); // copy elements from the old bag @@ -294,16 +295,16 @@ Node NormalForm::evaluateDuplicateRemoval(TNode n) Node NormalForm::evaluateUnionDisjoint(TNode n) { - Assert(n.getKind() == UNION_DISJOINT); + Assert(n.getKind() == BAG_UNION_DISJOINT); // Example // ------- - // input: (union_disjoint A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_disjoint A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 7) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 7) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) auto equal = [](std::map& elements, std::map::const_iterator& itA, @@ -354,16 +355,16 @@ Node NormalForm::evaluateUnionDisjoint(TNode n) Node NormalForm::evaluateUnionMax(TNode n) { - Assert(n.getKind() == UNION_MAX); + Assert(n.getKind() == BAG_UNION_MAX); // Example // ------- - // input: (union_max A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_max A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 4) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 4) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) auto equal = [](std::map& elements, std::map::const_iterator& itA, @@ -414,14 +415,14 @@ Node NormalForm::evaluateUnionMax(TNode n) Node NormalForm::evaluateIntersectionMin(TNode n) { - Assert(n.getKind() == INTERSECTION_MIN); + Assert(n.getKind() == BAG_INTER_MIN); // Example // ------- - // input: (intersectionMin A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.inter_min A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "x" 3) + // (bag "x" 3) auto equal = [](std::map& elements, std::map::const_iterator& itA, @@ -460,14 +461,14 @@ Node NormalForm::evaluateIntersectionMin(TNode n) Node NormalForm::evaluateDifferenceSubtract(TNode n) { - Assert(n.getKind() == DIFFERENCE_SUBTRACT); + Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT); // Example // ------- - // input: (difference_subtract A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_subtract A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2)) + // (bag.union_disjoint (bag "x" 1) (bag "z" 2)) auto equal = [](std::map& elements, std::map::const_iterator& itA, @@ -512,14 +513,14 @@ Node NormalForm::evaluateDifferenceSubtract(TNode n) Node NormalForm::evaluateDifferenceRemove(TNode n) { - Assert(n.getKind() == DIFFERENCE_REMOVE); + Assert(n.getKind() == BAG_DIFFERENCE_REMOVE); // Example // ------- - // input: (difference_subtract A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_remove A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "z" 2) + // (bag "z" 2) auto equal = [](std::map& elements, std::map::const_iterator& itA, @@ -566,9 +567,9 @@ Node NormalForm::evaluateChoose(TNode n) Assert(n.getKind() == BAG_CHOOSE); // Examples // -------- - // - (bag.choose (MK_BAG "x" 4)) = "x" + // - (bag.choose (bag "x" 4)) = "x" - if (n[0].getKind() == MK_BAG) + if (n[0].getKind() == BAG_MAKE) { return n[0][0]; } @@ -580,9 +581,9 @@ Node NormalForm::evaluateCard(TNode n) Assert(n.getKind() == BAG_CARD); // Examples // -------- - // - (card (emptyBag String)) = 0 - // - (choose (MK_BAG "x" 4)) = 4 - // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5 + // - (card (as bag.empty (Bag String))) = 0 + // - (bag.choose (bag "x" 4)) = 4 + // - (bag.choose (bag.union_disjoint (bag "x" 4) (bag "y" 1))) = 5 std::map elements = getBagElements(n[0]); Rational sum(0); @@ -601,12 +602,13 @@ Node NormalForm::evaluateIsSingleton(TNode n) Assert(n.getKind() == BAG_IS_SINGLETON); // Examples // -------- - // - (bag.is_singleton (emptyBag String)) = false - // - (bag.is_singleton (MK_BAG "x" 1)) = true - // - (bag.is_singleton (MK_BAG "x" 4)) = false - // - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) = false + // - (bag.is_singleton (as bag.empty (Bag String))) = false + // - (bag.is_singleton (bag "x" 1)) = true + // - (bag.is_singleton (bag "x" 4)) = false + // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) + // = false - if (n[0].getKind() == MK_BAG && n[0][1].getConst().isOne()) + if (n[0].getKind() == BAG_MAKE && n[0][1].getConst().isOne()) { return NodeManager::currentNM()->mkConst(true); } @@ -619,10 +621,10 @@ Node NormalForm::evaluateFromSet(TNode n) // Examples // -------- - // - (bag.from_set (set.empty String)) = (emptybag String) - // - (bag.from_set (singleton "x")) = (mkBag "x" 1) - // - (bag.from_set (union (singleton "x") (singleton "y"))) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)) + // - (bag.from_set (as set.empty (Set String))) = (as bag.empty (Bag String)) + // - (bag.from_set (set.singleton "x")) = (bag "x" 1) + // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = + // (bag.disjoint_union (bag "x" 1) (bag "y" 1)) NodeManager* nm = NodeManager::currentNM(); std::set setElements = @@ -644,10 +646,10 @@ Node NormalForm::evaluateToSet(TNode n) // Examples // -------- - // - (bag.to_set (emptybag String)) = (set.empty String) - // - (bag.to_set (mkBag "x" 4)) = (singleton "x") - // - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (union (singleton "x") (singleton "y"))) + // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Set String)) + // - (bag.to_set (bag "x" 4)) = (set.singleton "x") + // - (bag.to_set (bag.disjoint_union (bag "x" 3) (bag "y" 5)) = + // (set.union (set.singleton "x") (set.singleton "y"))) NodeManager* nm = NodeManager::currentNM(); std::map bagElements = getBagElements(n[0]); @@ -669,8 +671,8 @@ Node NormalForm::evaluateBagMap(TNode n) // Examples // -------- // - (bag.map ((lambda ((x String)) "z") - // (union_disjoint (bag "a" 2) (bag "b" 3)) = - // (union_disjoint + // (bag.union_disjoint (bag "a" 2) (bag "b" 3)) = + // (bag.union_disjoint // (bag ((lambda ((x String)) "z") "a") 2) // (bag ((lambda ((x String)) "z") "b") 3)) = // (bag "z" 5) diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index bf96a1fba..8ceee2881 100644 --- a/src/theory/bags/normal_form.h +++ b/src/theory/bags/normal_form.h @@ -30,11 +30,11 @@ class NormalForm /** * Returns true if n is considered a to be a (canonical) constant bag value. * A canonical bag value is one whose AST is: - * (union_disjoint (mkBag e1 c1) ... - * (union_disjoint (mkBag e_{n-1} c_{n-1}) (mkBag e_n c_n)))) + * (bag.union_disjoint (bag e1 c1) ... + * (bag.union_disjoint (bag e_{n-1} c_{n-1}) (bag e_n c_n)))) * where c1 ... cn are positive integers, e1 ... en are constants, and the * node identifier of these constants are such that: e1 < ... < en. - * Also handles the corner cases of empty bag and bag constructed by mkBag + * Also handles the corner cases of empty bag and bag constructed by bag */ static bool isConstant(TNode n); /** @@ -83,9 +83,9 @@ class NormalForm * and elements of B (elementsB with iterator itB). * The arguments below specify how these iterators are used to generate the * elements of the result (elements). - * @param n a node whose kind is a binary operator (union_disjoint, union_max, - * intersection_min, difference_subtract, difference_remove) and whose - * children are constant bags. + * @param n a node whose kind is a binary operator (bag.union_disjoint, + * union_max, intersection_min, difference_subtract, difference_remove) and + * whose children are constant bags. * @param equal a lambda expression that receives (elements, itA, itB) and * specify the action that needs to be taken when the elements of itA, itB are * equal. @@ -112,8 +112,8 @@ class NormalForm T5&& remainderOfB); /** * evaluate n as follows: - * - (mkBag a 0) = (emptybag T) where T is the type of the original bag - * - (mkBag a (-c)) = (emptybag T) where T is the type the original bag, + * - (bag a 0) = (as bag.empty T) where T is the type of the original bag + * - (bag a (-c)) = (as bag.empty T) where T is the type the original bag, * and c > 0 is a constant */ static Node evaluateMakeBag(TNode n); @@ -126,7 +126,7 @@ class NormalForm static Node evaluateBagCount(TNode n); /** - * @param n has the form (duplicate_removal A) where A is a constant bag + * @param n has the form (bag.duplicate_removal A) where A is a constant bag * @return a constant bag constructed from the elements in A where each * element has multiplicity one */ @@ -135,32 +135,33 @@ class NormalForm /** * evaluates union disjoint node such that the returned node is a canonical * bag that has the form - * (union_disjoint (mkBag e1 c1) ... - * (union_disjoint * (mkBag e_{n-1} c_{n-1}) (mkBag e_n c_n)))) where + * (bag.union_disjoint (bag e1 c1) ... + * (bag.union_disjoint * (bag e_{n-1} c_{n-1}) (bag e_n c_n)))) where * c1... cn are positive integers, e1 ... en are constants, and the node * identifier of these constants are such that: e1 < ... < en. - * @param n has the form (union_disjoint A B) where A, B are constant bags + * @param n has the form (bag.union_disjoint A B) where A, B are constant bags * @return the union disjoint of A and B */ static Node evaluateUnionDisjoint(TNode n); /** - * @param n has the form (union_max A B) where A, B are constant bags + * @param n has the form (bag.union_max A B) where A, B are constant bags * @return the union max of A and B */ static Node evaluateUnionMax(TNode n); /** - * @param n has the form (intersection_min A B) where A, B are constant bags + * @param n has the form (bag.inter_min A B) where A, B are constant bags * @return the intersection min of A and B */ static Node evaluateIntersectionMin(TNode n); /** - * @param n has the form (difference_subtract A B) where A, B are constant + * @param n has the form (bag.difference_subtract A B) where A, B are constant * bags * @return the difference subtract of A and B */ static Node evaluateDifferenceSubtract(TNode n); /** - * @param n has the form (difference_remove A B) where A, B are constant bags + * @param n has the form (bag.difference_remove A B) where A, B are constant + * bags * @return the difference remove of A and B */ static Node evaluateDifferenceRemove(TNode n); diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index c8aeec147..896c4f251 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -27,12 +27,13 @@ const char* toString(Rewrite r) { case Rewrite::NONE: return "NONE"; case Rewrite::CARD_DISJOINT: return "CARD_DISJOINT"; - case Rewrite::CARD_MK_BAG: return "CARD_MK_BAG"; - case Rewrite::CHOOSE_MK_BAG: return "CHOOSE_MK_BAG"; + case Rewrite::CARD_BAG_MAKE: return "CARD_BAG_MAKE"; + case Rewrite::CHOOSE_BAG_MAKE: return "CHOOSE_BAG_MAKE"; case Rewrite::CONSTANT_EVALUATION: return "CONSTANT_EVALUATION"; case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY"; - case Rewrite::COUNT_MK_BAG: return "COUNT_MK_BAG"; - case Rewrite::DUPLICATE_REMOVAL_MK_BAG: return "DUPLICATE_REMOVAL_MK_BAG"; + case Rewrite::COUNT_BAG_MAKE: return "COUNT_BAG_MAKE"; + case Rewrite::DUPLICATE_REMOVAL_BAG_MAKE: + return "DUPLICATE_REMOVAL_BAG_MAKE"; case Rewrite::EQ_CONST_FALSE: return "EQ_CONST_FALSE"; case Rewrite::EQ_REFL: return "EQ_REFL"; case Rewrite::EQ_SYM: return "EQ_SYM"; @@ -43,11 +44,11 @@ const char* toString(Rewrite r) case Rewrite::INTERSECTION_SAME: return "INTERSECTION_SAME"; case Rewrite::INTERSECTION_SHARED_LEFT: return "INTERSECTION_SHARED_LEFT"; case Rewrite::INTERSECTION_SHARED_RIGHT: return "INTERSECTION_SHARED_RIGHT"; - case Rewrite::IS_SINGLETON_MK_BAG: return "IS_SINGLETON_MK_BAG"; + case Rewrite::IS_SINGLETON_BAG_MAKE: return "IS_SINGLETON_BAG_MAKE"; case Rewrite::MAP_CONST: return "MAP_CONST"; - case Rewrite::MAP_MK_BAG: return "MAP_MK_BAG"; + case Rewrite::MAP_BAG_MAKE: return "MAP_BAG_MAKE"; case Rewrite::MAP_UNION_DISJOINT: return "MAP_UNION_DISJOINT"; - case Rewrite::MK_BAG_COUNT_NEGATIVE: return "MK_BAG_COUNT_NEGATIVE"; + case Rewrite::BAG_MAKE_COUNT_NEGATIVE: return "BAG_MAKE_COUNT_NEGATIVE"; case Rewrite::REMOVE_FROM_UNION: return "REMOVE_FROM_UNION"; case Rewrite::REMOVE_MIN: return "REMOVE_MIN"; case Rewrite::REMOVE_RETURN_LEFT: return "REMOVE_RETURN_LEFT"; diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index 78eb502c8..c5050ea72 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -32,12 +32,12 @@ enum class Rewrite : uint32_t { NONE, // no rewrite happened CARD_DISJOINT, - CARD_MK_BAG, - CHOOSE_MK_BAG, + CARD_BAG_MAKE, + CHOOSE_BAG_MAKE, CONSTANT_EVALUATION, COUNT_EMPTY, - COUNT_MK_BAG, - DUPLICATE_REMOVAL_MK_BAG, + COUNT_BAG_MAKE, + DUPLICATE_REMOVAL_BAG_MAKE, EQ_CONST_FALSE, EQ_REFL, EQ_SYM, @@ -48,11 +48,11 @@ enum class Rewrite : uint32_t INTERSECTION_SAME, INTERSECTION_SHARED_LEFT, INTERSECTION_SHARED_RIGHT, - IS_SINGLETON_MK_BAG, + IS_SINGLETON_BAG_MAKE, MAP_CONST, - MAP_MK_BAG, + MAP_BAG_MAKE, MAP_UNION_DISJOINT, - MK_BAG_COUNT_NEGATIVE, + BAG_MAKE_COUNT_NEGATIVE, REMOVE_FROM_UNION, REMOVE_MIN, REMOVE_RETURN_LEFT, diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 50c6919fa..5c7c1dd73 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -91,7 +91,7 @@ void SolverState::collectBagsAndCountTerms() Node n = (*it); Trace("bags-eqc") << (*it) << " "; Kind k = n.getKind(); - if (k == MK_BAG) + if (k == BAG_MAKE) { // for terms (bag x c) we need to store x by registering the count term // (bag.count x (bag x c)) diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 68fffacbd..d6f628537 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -29,8 +29,7 @@ namespace bags { class SolverState : public TheoryState { public: - SolverState(Env& env, - Valuation val); + SolverState(Env& env, Valuation val); /** * This function adds the bag representative n to the set d_bags if it is not diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 3ab184eab..861aaf862 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -66,14 +66,14 @@ void TheoryBags::finishInit() d_valuation.setUnevaluatedKind(WITNESS); // functions we are doing congruence over - d_equalityEngine->addFunctionKind(UNION_MAX); - d_equalityEngine->addFunctionKind(UNION_DISJOINT); - d_equalityEngine->addFunctionKind(INTERSECTION_MIN); - d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT); - d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE); + d_equalityEngine->addFunctionKind(BAG_UNION_MAX); + d_equalityEngine->addFunctionKind(BAG_UNION_DISJOINT); + d_equalityEngine->addFunctionKind(BAG_INTER_MIN); + d_equalityEngine->addFunctionKind(BAG_DIFFERENCE_SUBTRACT); + d_equalityEngine->addFunctionKind(BAG_DIFFERENCE_REMOVE); d_equalityEngine->addFunctionKind(BAG_COUNT); - d_equalityEngine->addFunctionKind(DUPLICATE_REMOVAL); - d_equalityEngine->addFunctionKind(MK_BAG); + d_equalityEngine->addFunctionKind(BAG_DUPLICATE_REMOVAL); + d_equalityEngine->addFunctionKind(BAG_MAKE); d_equalityEngine->addFunctionKind(BAG_CARD); d_equalityEngine->addFunctionKind(BAG_FROM_SET); d_equalityEngine->addFunctionKind(BAG_TO_SET); @@ -98,7 +98,7 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, // (bag.choose A) is expanded as // (witness ((x elementType)) // (ite - // (= A (as emptybag (Bag E))) + // (= A (as bag.empty (Bag E))) // (= x (uf A)) // (and (>= (bag.count x A) 1) (= x (uf A))) // where uf: (Bag E) -> E is a skolem function, and E is the type of elements diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 06771a418..58a1b3291 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -60,14 +60,14 @@ BagEnumerator& BagEnumerator::operator++() Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); TypeNode elementType = d_elementTypeEnumerator.getType(); Node singleton = d_nodeManager->mkBag(elementType, d_element, one); - if (d_currentBag.getKind() == kind::EMPTYBAG) + if (d_currentBag.getKind() == kind::BAG_EMPTY) { d_currentBag = singleton; } else { - d_currentBag = - d_nodeManager->mkNode(kind::UNION_DISJOINT, singleton, d_currentBag); + d_currentBag = d_nodeManager->mkNode( + kind::BAG_UNION_DISJOINT, singleton, d_currentBag); } d_currentBag = Rewriter::rewrite(d_currentBag); diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 089038267..2623f3ed7 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -19,7 +19,7 @@ #include "base/check.h" #include "expr/emptybag.h" -#include "theory/bags/make_bag_op.h" +#include "theory/bags/bag_make_op.h" #include "theory/bags/normal_form.h" #include "util/cardinality.h" #include "util/rational.h" @@ -32,10 +32,11 @@ TypeNode BinaryOperatorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT - || n.getKind() == kind::INTERSECTION_MIN - || n.getKind() == kind::DIFFERENCE_SUBTRACT - || n.getKind() == kind::DIFFERENCE_REMOVE); + Assert(n.getKind() == kind::BAG_UNION_MAX + || n.getKind() == kind::BAG_UNION_DISJOINT + || n.getKind() == kind::BAG_INTER_MIN + || n.getKind() == kind::BAG_DIFFERENCE_SUBTRACT + || n.getKind() == kind::BAG_DIFFERENCE_REMOVE); TypeNode bagType = n[0].getType(check); if (check) { @@ -61,7 +62,7 @@ bool BinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { // only UNION_DISJOINT has a const rule in kinds. // Other binary operators do not have const rules in kinds - Assert(n.getKind() == kind::UNION_DISJOINT); + Assert(n.getKind() == kind::BAG_UNION_DISJOINT); return NormalForm::isConstant(n); } @@ -69,13 +70,13 @@ TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::SUBBAG); + Assert(n.getKind() == kind::BAG_SUBBAG); TypeNode bagType = n[0].getType(check); if (check) { if (!bagType.isBag()) { - throw TypeCheckingExceptionPrivate(n, "SUBBAG operating on non-bag"); + throw TypeCheckingExceptionPrivate(n, "BAG_SUBBAG operating on non-bag"); } TypeNode secondBagType = n[1].getType(check); if (secondBagType != bagType) @@ -83,7 +84,7 @@ TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager, if (!bagType.isComparableTo(secondBagType)) { throw TypeCheckingExceptionPrivate( - n, "SUBBAG operating on bags of different types"); + n, "BAG_SUBBAG operating on bags of different types"); } } } @@ -104,8 +105,8 @@ TypeNode CountTypeRule::computeType(NodeManager* nodeManager, n, "checking for membership in a non-bag"); } TypeNode elementType = n[0].getType(check); - // e.g. (count 1 (mkBag (mkBag_op Real) 1.0 3))) is 3 whereas - // (count 1.0 (mkBag (mkBag_op Int) 1 3))) throws a typing error + // e.g. (bag.count 1 (bag (BagMakeOp Real) 1.0 3))) is 3 whereas + // (bag.count 1.0 (bag (BagMakeOp Int) 1 3)) throws a typing error if (!elementType.isSubtypeOf(bagType.getBagElementType())) { std::stringstream ss; @@ -123,25 +124,26 @@ TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::DUPLICATE_REMOVAL); + Assert(n.getKind() == kind::BAG_DUPLICATE_REMOVAL); TypeNode bagType = n[0].getType(check); if (check) { if (!bagType.isBag()) { std::stringstream ss; - ss << "Applying DUPLICATE_REMOVAL on a non-bag argument in term " << n; + ss << "Applying BAG_DUPLICATE_REMOVAL on a non-bag argument in term " + << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } } return bagType; } -TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check) +TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check) { - Assert(n.getKind() == kind::MK_BAG && n.hasOperator() - && n.getOperator().getKind() == kind::MK_BAG_OP); - MakeBagOp op = n.getOperator().getConst(); + Assert(n.getKind() == kind::BAG_MAKE && n.hasOperator() + && n.getOperator().getKind() == kind::BAG_MAKE_OP); + BagMakeOp op = n.getOperator().getConst(); TypeNode expectedElementType = op.getType(); if (check) { @@ -149,20 +151,20 @@ TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check) { std::stringstream ss; ss << "operands in term " << n << " are " << n.getNumChildren() - << ", but MK_BAG expects 2 operands."; + << ", but BAG_MAKE expects 2 operands."; throw TypeCheckingExceptionPrivate(n, ss.str()); } TypeNode type1 = n[1].getType(check); if (!type1.isInteger()) { std::stringstream ss; - ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1; + 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. (mkBag (mkBag_op Real) 1 1) where 1 is an Int + // e.g. (bag (bag_op Real) 1 1) where 1 is an Int if (!actualElementType.isSubtypeOf(expectedElementType)) { std::stringstream ss; @@ -176,9 +178,9 @@ TypeNode MkBagTypeRule::computeType(NodeManager* nm, TNode n, bool check) return nm->mkBagType(expectedElementType); } -bool MkBagTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) +bool BagMakeTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::MK_BAG); + Assert(n.getKind() == kind::BAG_MAKE); // for a bag to be a constant, both the element and its multiplicity should // be constants, and the multiplicity should be > 0. return n[0].isConst() && n[1].isConst() @@ -206,7 +208,7 @@ TypeNode EmptyBagTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::EMPTYBAG); + Assert(n.getKind() == kind::BAG_EMPTY); EmptyBag emptyBag = n.getConst(); return emptyBag.getType(); } diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 53a63a687..3bc3b3462 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -29,9 +29,9 @@ namespace theory { namespace bags { /** - * Type rule for binary operators (union_max, union_disjoint, intersection_min - * difference_subtract, difference_remove) - * to check if the two arguments are of the same sort. + * Type rule for binary operators (bag.union_max, bag.union_disjoint, + * bag.inter_min bag.difference_subtract, bag.difference_remove) to check + * if the two arguments are of the same sort. */ struct BinaryOperatorTypeRule { @@ -40,8 +40,8 @@ struct BinaryOperatorTypeRule }; /* struct BinaryOperatorTypeRule */ /** - * Type rule for binary operator subbag to check if the two arguments have the - * same sort. + * Type rule for binary operator bag.subbag to check if the two arguments have + * the same sort. */ struct SubBagTypeRule { @@ -58,7 +58,7 @@ struct CountTypeRule }; /* struct CountTypeRule */ /** - * Type rule for duplicate_removal to check the argument is of a bag. + * Type rule for bag.duplicate_removal to check the argument is of a bag. */ struct DuplicateRemovalTypeRule { @@ -69,11 +69,11 @@ struct DuplicateRemovalTypeRule * Type rule for (bag op e) operator to check the sort of e matches the sort * stored in op. */ -struct MkBagTypeRule +struct BagMakeTypeRule { static TypeNode computeType(NodeManager* nm, TNode n, bool check); static bool computeIsConst(NodeManager* nodeManager, TNode n); -}; /* struct MkBagTypeRule */ +}; /* struct BagMakeTypeRule */ /** * Type rule for bag.is_singleton to check the argument is of a bag. @@ -81,10 +81,10 @@ struct MkBagTypeRule struct IsSingletonTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; /* struct IsMkBagTypeRule */ +}; /* struct IsSingletonTypeRule */ /** - * Type rule for (as emptybag (Bag ...)) + * Type rule for (as bag.empty (Bag ...)) */ struct EmptyBagTypeRule { diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 4747aeaf2..82ae674e2 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -106,14 +106,15 @@ const char* toString(InferenceId i) case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY"; case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT"; - case InferenceId::BAGS_MK_BAG: return "BAGS_MK_BAG"; + case InferenceId::BAGS_BAG_MAKE: return "BAGS_BAG_MAKE"; case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY"; case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY"; case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY"; case InferenceId::BAGS_UNION_DISJOINT: return "BAGS_UNION_DISJOINT"; case InferenceId::BAGS_UNION_MAX: return "BAGS_UNION_MAX"; case InferenceId::BAGS_INTERSECTION_MIN: return "BAGS_INTERSECTION_MIN"; - case InferenceId::BAGS_DIFFERENCE_SUBTRACT: return "BAGS_DIFFERENCE_SUBTRACT"; + case InferenceId::BAGS_DIFFERENCE_SUBTRACT: + return "BAGS_DIFFERENCE_SUBTRACT"; case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE"; case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL"; case InferenceId::BAGS_MAP: return "BAGS_MAP"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index a13bc4d1b..ad879d7ab 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -169,7 +169,7 @@ enum class InferenceId // ---------------------------------- bags theory BAGS_NON_NEGATIVE_COUNT, - BAGS_MK_BAG, + BAGS_BAG_MAKE, BAGS_EQUALITY, BAGS_DISEQUALITY, BAGS_EMPTY, diff --git a/test/regress/regress1/bags/choose1.smt2 b/test/regress/regress1/bags/choose1.smt2 index b157bbc70..53cd7c771 100644 --- a/test/regress/regress1/bags/choose1.smt2 +++ b/test/regress/regress1/bags/choose1.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (= (bag.choose A) 10)) (assert (= a (bag.choose A))) (assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a)))) diff --git a/test/regress/regress1/bags/choose3.smt2 b/test/regress/regress1/bags/choose3.smt2 index ffa9ae9a7..adf1a3e21 100644 --- a/test/regress/regress1/bags/choose3.smt2 +++ b/test/regress/regress1/bags/choose3.smt2 @@ -4,5 +4,5 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (assert (= (bag.choose A) 10)) -(assert (= A (as emptybag (Bag Int)))) +(assert (= A (as bag.empty (Bag Int)))) (check-sat) diff --git a/test/regress/regress1/bags/choose4.smt2 b/test/regress/regress1/bags/choose4.smt2 index a0290b90b..cdf4065d4 100644 --- a/test/regress/regress1/bags/choose4.smt2 +++ b/test/regress/regress1/bags/choose4.smt2 @@ -3,7 +3,7 @@ (set-info :status sat) (declare-fun A () (Bag Int)) (declare-fun a () Int) -(assert (not (= A (as emptybag (Bag Int))))) +(assert (not (= A (as bag.empty (Bag Int))))) (assert (> (bag.count 10 A) 0)) (assert (= a (bag.choose A))) (check-sat) diff --git a/test/regress/regress1/bags/difference_remove1.smt2 b/test/regress/regress1/bags/difference_remove1.smt2 index f5a87c149..82f6ec53d 100644 --- a/test/regress/regress1/bags/difference_remove1.smt2 +++ b/test/regress/regress1/bags/difference_remove1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal1.smt2 b/test/regress/regress1/bags/duplicate_removal1.smt2 index 2b662c6e5..27ce2360b 100644 --- a/test/regress/regress1/bags/duplicate_removal1.smt2 +++ b/test/regress/regress1/bags/duplicate_removal1.smt2 @@ -3,6 +3,6 @@ (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) (check-sat) diff --git a/test/regress/regress1/bags/duplicate_removal2.smt2 b/test/regress/regress1/bags/duplicate_removal2.smt2 index 7dacaae43..5382f773f 100644 --- a/test/regress/regress1/bags/duplicate_removal2.smt2 +++ b/test/regress/regress1/bags/duplicate_removal2.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (duplicate_removal A))) -(assert (distinct (as emptybag (Bag String)) A B)) -(assert (= B (union_max A B))) +(assert (= B (bag.duplicate_removal A))) +(assert (distinct (as bag.empty (Bag String)) A B)) +(assert (= B (bag.union_max A B))) (check-sat) \ No newline at end of file diff --git a/test/regress/regress1/bags/emptybag1.smt2 b/test/regress/regress1/bags/emptybag1.smt2 index f7f92599d..61b29f414 100644 --- a/test/regress/regress1/bags/emptybag1.smt2 +++ b/test/regress/regress1/bags/emptybag1.smt2 @@ -4,7 +4,7 @@ (declare-fun x () String) (declare-fun y () Int) (assert (= x "x")) -(assert (= A (as emptybag (Bag String)))) +(assert (= A (as bag.empty (Bag String)))) (assert (= (bag.count x A) y)) (assert(> y 1)) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2 index f9fee0ec4..79ccc4b82 100644 --- a/test/regress/regress1/bags/fuzzy1.smt2 +++ b/test/regress/regress1/bags/fuzzy1.smt2 @@ -5,6 +5,6 @@ (declare-fun c () Int) ; c here is zero (assert (and - (= b (difference_subtract b a)) ; b is empty + (= b (bag.difference_subtract b a)) ; b is empty (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|} (check-sat) diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2 index 31da47f53..c7968b274 100644 --- a/test/regress/regress1/bags/fuzzy2.smt2 +++ b/test/regress/regress1/bags/fuzzy2.smt2 @@ -8,8 +8,8 @@ (let ((D (bag d c))) ; when c = zero, then D is empty (and (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty - (= a (union_max a D)) - (= a (difference_subtract a (bag d 1))) - (= a (union_disjoint a D)) - (= a (intersection_min a D))))) + (= a (bag.union_max a D)) + (= a (bag.difference_subtract a (bag d 1))) + (= a (bag.union_disjoint a D)) + (= a (bag.inter_min a D))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 index dd6dd02dc..a457bf9ae 100644 --- a/test/regress/regress1/bags/fuzzy3.smt2 +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -8,6 +8,6 @@ (assert (not (= - (= A (difference_remove (bag d c) A)) + (= A (bag.difference_remove (bag d c) A)) (= A (bag (tuple c c) c))))) (check-sat) diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 index b733a4862..5b24b8d6e 100644 --- a/test/regress/regress1/bags/fuzzy4.smt2 +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -7,8 +7,8 @@ (assert (not (= - (= A (bag d (+ c (bag.count d (union_disjoint A A))))) - (= A (difference_remove (bag d c) A))))) + (= A (bag d (+ c (bag.count d (bag.union_disjoint A A))))) + (= A (bag.difference_remove (bag d c) A))))) (assert (= A (bag (tuple 0 0) 5))) (assert (= c (- 5))) (assert (= d (tuple 0 0))) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 index 2dea236a5..0674fad9c 100644 --- a/test/regress/regress1/bags/fuzzy5.smt2 +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -10,7 +10,7 @@ (and (not (= (= A (bag (tuple 0 c) (+ c c))) - (= A (difference_remove (bag d c) A)))) + (= A (bag.difference_remove (bag d c) A)))) (not (= (= A (bag (tuple 0 1) c_plus_1)) (= A (bag (tuple c 1) c_plus_1))))))) diff --git a/test/regress/regress1/bags/intersection_min1.smt2 b/test/regress/regress1/bags/intersection_min1.smt2 index f5a515b9c..0ced4aa89 100644 --- a/test/regress/regress1/bags/intersection_min1.smt2 +++ b/test/regress/regress1/bags/intersection_min1.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (assert (distinct A B C)) (check-sat) \ No newline at end of file diff --git a/test/regress/regress1/bags/intersection_min2.smt2 b/test/regress/regress1/bags/intersection_min2.smt2 index 66afa2f3a..119f34665 100644 --- a/test/regress/regress1/bags/intersection_min2.smt2 +++ b/test/regress/regress1/bags/intersection_min2.smt2 @@ -3,7 +3,7 @@ (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) (declare-fun C () (Bag String)) -(assert (= C (intersection_min A B))) -(assert (= C (union_disjoint A B))) -(assert (distinct (as emptybag (Bag String)) C)) +(assert (= C (bag.inter_min A B))) +(assert (= C (bag.union_disjoint A B))) +(assert (distinct (as bag.empty (Bag String)) C)) (check-sat) diff --git a/test/regress/regress1/bags/issue5759.smt2 b/test/regress/regress1/bags/issue5759.smt2 index ba3752e09..1c29afea6 100644 --- a/test/regress/regress1/bags/issue5759.smt2 +++ b/test/regress/regress1/bags/issue5759.smt2 @@ -4,7 +4,7 @@ (declare-fun A () (Bag Int)) (declare-fun B () (Bag Int)) (declare-fun x () Int) -(assert (not (= A (union_max (bag x 1) (bag 0 1))))) -(assert (= A (union_disjoint B (bag 0 1)))) +(assert (not (= A (bag.union_max (bag x 1) (bag 0 1))))) +(assert (= A (bag.union_disjoint B (bag 0 1)))) (assert (= x 1)) (check-sat) \ No newline at end of file diff --git a/test/regress/regress1/bags/map1.smt2 b/test/regress/regress1/bags/map1.smt2 index 54d671415..c7dc3d636 100644 --- a/test/regress/regress1/bags/map1.smt2 +++ b/test/regress/regress1/bags/map1.smt2 @@ -5,8 +5,8 @@ (declare-fun x () Int) (declare-fun y () Int) (declare-fun f (Int) Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) (assert (= B (bag.map f A))) (assert (distinct (f x) (f y) x y)) (check-sat) diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2 index 637815fa5..ae0184008 100644 --- a/test/regress/regress1/bags/map3.smt2 +++ b/test/regress/regress1/bags/map3.smt2 @@ -6,5 +6,5 @@ (define-fun f ((x Int)) Int (+ x 1)) (assert (= B (bag.map f A))) (assert (= (bag.count (- 2) B) 57)) -(assert (= A (as emptybag (Bag Int)) )) +(assert (= A (as bag.empty (Bag Int)) )) (check-sat) diff --git a/test/regress/regress1/bags/subbag1.smt2 b/test/regress/regress1/bags/subbag1.smt2 index 055e47a17..7a6bf66d7 100644 --- a/test/regress/regress1/bags/subbag1.smt2 +++ b/test/regress/regress1/bags/subbag1.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (assert (= x 1)) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) 5)) (assert (= (bag.count x B) 10)) (check-sat) \ No newline at end of file diff --git a/test/regress/regress1/bags/subbag2.smt2 b/test/regress/regress1/bags/subbag2.smt2 index 6d5cde362..abdb3b7d9 100644 --- a/test/regress/regress1/bags/subbag2.smt2 +++ b/test/regress/regress1/bags/subbag2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (subbag A B)) -(assert (subbag B A)) +(assert (bag.subbag A B)) +(assert (bag.subbag B A)) (assert (= (bag.count x A) x)) (assert (= (bag.count y A) x)) (assert (distinct x y)) diff --git a/test/regress/regress1/bags/union_disjoint.smt2 b/test/regress/regress1/bags/union_disjoint.smt2 index d30ed4b14..fdb9d16d3 100644 --- a/test/regress/regress1/bags/union_disjoint.smt2 +++ b/test/regress/regress1/bags/union_disjoint.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_disjoint (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_disjoint (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) diff --git a/test/regress/regress1/bags/union_max1.smt2 b/test/regress/regress1/bags/union_max1.smt2 index d278527b9..d41e1425a 100644 --- a/test/regress/regress1/bags/union_max1.smt2 +++ b/test/regress/regress1/bags/union_max1.smt2 @@ -4,7 +4,7 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) (check-sat) \ No newline at end of file diff --git a/test/regress/regress1/bags/union_max2.smt2 b/test/regress/regress1/bags/union_max2.smt2 index dd4bceff5..1366130bf 100644 --- a/test/regress/regress1/bags/union_max2.smt2 +++ b/test/regress/regress1/bags/union_max2.smt2 @@ -4,8 +4,8 @@ (declare-fun B () (Bag Int)) (declare-fun x () Int) (declare-fun y () Int) -(assert (= A (union_max (bag x 1) (bag y 2)))) -(assert (= A (union_disjoint B (bag y 2)))) +(assert (= A (bag.union_max (bag x 1) (bag y 2)))) +(assert (= A (bag.union_disjoint B (bag y 2)))) (assert (= x y)) -(assert (distinct (as emptybag (Bag Int)) B)) +(assert (distinct (as bag.empty (Bag Int)) B)) (check-sat) \ No newline at end of file diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 6c52f539d..5f3abfcee 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -98,11 +98,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) { // Examples // ------- - // (bag.count "x" (emptybag String)) = 0 - // (bag.count "x" (mkBag "y" 5)) = 0 - // (bag.count "x" (mkBag "x" 4)) = 4 - // (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4 - // (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0 + // (bag.count "x" (as bag.empty (Bag String))) = 0 + // (bag.count "x" (bag "y" 5)) = 0 + // (bag.count "x" (bag "x" 4)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4 + // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0 Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); @@ -136,12 +136,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) Node output3 = four; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node unionDisjointXY = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node unionDisjointXY = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input4 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointXY); Node output4 = four; ASSERT_EQ(output3, NormalForm::evaluate(input3)); - Node unionDisjointYZ = d_nodeManager->mkNode(UNION_DISJOINT, y_5, z_5); + Node unionDisjointYZ = d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_5, z_5); Node input5 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointYZ); Node output5 = zero; ASSERT_EQ(output4, NormalForm::evaluate(input4)); @@ -151,14 +151,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) { // Examples // -------- - // - (duplicate_removal (emptybag String)) = (emptybag String) - // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1) - // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1) + // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // String)) + // - (bag.duplicate_removal (bag "x" 4)) = (bag.empty"x" 1) + // - (bag.duplicate_removal (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (bag.union_disjoint(bag "x" 1) (bag "y" 1) Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, emptybag); + Node input1 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, emptybag); Node output1 = emptybag; ASSERT_EQ(output1, NormalForm::evaluate(input1)); @@ -183,13 +184,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4); + Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4); Node output2 = x_1; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); - Node input3 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, normalBag); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); + Node input3 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, normalBag); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -197,13 +198,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) { // Example // ------- - // input: (union_max A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_max A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 4) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 4) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -229,13 +230,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_MAX, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_4, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_4, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -259,27 +262,27 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1) elements[2], d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // unionDisjointAB is already in a normal form ASSERT_TRUE(unionDisjointAB.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointAB)); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - // unionDisjointAB is is the normal form of unionDisjointBA + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + // unionDisjointAB is the normal form of unionDisjointBA ASSERT_FALSE(unionDisjointBA.isConst()); ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointBA)); Node unionDisjointAB_C = - d_nodeManager->mkNode(UNION_DISJOINT, unionDisjointAB, C); - Node unionDisjointBC = d_nodeManager->mkNode(UNION_DISJOINT, B, C); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionDisjointAB, C); + Node unionDisjointBC = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, C); Node unionDisjointA_BC = - d_nodeManager->mkNode(UNION_DISJOINT, A, unionDisjointBC); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, unionDisjointBC); // unionDisjointA_BC is the normal form of unionDisjointAB_C ASSERT_FALSE(unionDisjointAB_C.isConst()); ASSERT_TRUE(unionDisjointA_BC.isConst()); ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C)); - Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A); + Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A); Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(), elements[0], @@ -293,13 +296,13 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) { // Example // ------- - // input: (union_disjoint A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.union_disjoint A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint A B) - // where A = (MK_BAG "x" 7) - // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2))) + // (bag.union_disjoint A B) + // where A = (bag "x" 7) + // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2))) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -325,13 +328,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); // output Node output = d_nodeManager->mkNode( - UNION_DISJOINT, x_7, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2)); + BAG_UNION_DISJOINT, + x_7, + d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2)); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -341,11 +346,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) { // Example // ------- - // input: (intersection_min A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.inter_min A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "x" 3) + // (bag "x" 3) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -371,9 +376,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); // output Node output = x_3; @@ -386,11 +391,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) { // Example // ------- - // input: (difference_subtract A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_subtract A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2)) + // (bag.union_disjoint (bag "x" 1) (bag "z" 2)) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -420,12 +425,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B); // output - Node output = d_nodeManager->mkNode(UNION_DISJOINT, x_1, z_2); + Node output = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, z_2); ASSERT_TRUE(output.isConst()); ASSERT_EQ(output, NormalForm::evaluate(input)); @@ -435,11 +440,11 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) { // Example // ------- - // input: (difference_remove A B) - // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2))) - // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1))) + // input: (bag.difference_remove A B) + // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2))) + // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1))) // output: - // (MK_BAG "z" 2) + // (bag "z" 2) Node x = d_nodeManager->mkConst(String("x")); Node y = d_nodeManager->mkConst(String("y")); @@ -469,9 +474,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove) y, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); - Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2); - Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1); - Node input = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, B); + Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2); + Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1); + Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, B); // output Node output = z_2; @@ -484,9 +489,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) { // Examples // -------- - // - (card (emptybag String)) = 0 - // - (choose (MK_BAG "x" 4)) = 4 - // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5 + // - (bag.card (as bag.empty (Bag String))) = 0 + // - (bag.choose (bag "x" 4)) = 4 + // - (bag.choose (bag.union_disjoint (bag "x" 4) (bag "y" 1))) = 5 Node empty = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); Node x = d_nodeManager->mkConst(String("x")); @@ -510,7 +515,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)); ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1); Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint); Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)); ASSERT_EQ(output3, NormalForm::evaluate(input3)); @@ -520,10 +525,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) { // Examples // -------- - // - (bag.is_singleton (emptybag String)) = false - // - (bag.is_singleton (MK_BAG "x" 1)) = true - // - (bag.is_singleton (MK_BAG "x" 4)) = false - // - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) = + // - (bag.is_singleton (as bag.empty (Bag String))) = false + // - (bag.is_singleton (bag "x" 1)) = true + // - (bag.is_singleton (bag "x" 4)) = false + // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) = // false Node falseNode = d_nodeManager->mkConst(false); Node trueNode = d_nodeManager->mkConst(true); @@ -557,7 +562,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) Node output3 = falseNode; ASSERT_EQ(output2, NormalForm::evaluate(input2)); - Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); Node input4 = d_nodeManager->mkNode(BAG_IS_SINGLETON, union_disjoint); Node output4 = falseNode; ASSERT_EQ(output3, NormalForm::evaluate(input3)); @@ -567,10 +572,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) { // Examples // -------- - // - (bag.from_set (emptyset String)) = (emptybag String) - // - (bag.from_set (singleton "x")) = (mkBag "x" 1) - // - (bag.to_set (union (singleton "x") (singleton "y"))) = - // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)) + // - (bag.from_set (as set.empty (Bag String))) = (as bag.empty (Bag String)) + // - (bag.from_set (set.singleton "x")) = (bag "x" 1) + // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = + // (bag.union_disjoint (bag "x" 1) (bag "y" 1)) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -602,7 +607,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set) // for normal sets, the first node is the largest, not smallest Node normalSet = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); Node input3 = d_nodeManager->mkNode(BAG_FROM_SET, normalSet); - Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1); + Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, NormalForm::evaluate(input3)); } @@ -610,10 +615,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) { // Examples // -------- - // - (bag.to_set (emptybag String)) = (emptyset String) - // - (bag.to_set (mkBag "x" 4)) = (singleton "x") - // - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) = - // (union (singleton "x") (singleton "y"))) + // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Bag String)) + // - (bag.to_set (bag "x" 4)) = (set.singleton "x") + // - (bag.to_set (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // (set.union (set.singleton "x") (set.singleton "y"))) Node emptyset = d_nodeManager->mkConst( EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); @@ -643,7 +648,7 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) ASSERT_EQ(output2, NormalForm::evaluate(input2)); // for normal sets, the first node is the largest, not smallest - Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5); + Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5); Node input3 = d_nodeManager->mkNode(BAG_TO_SET, normalBag); Node output3 = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton); ASSERT_EQ(output3, NormalForm::evaluate(input3)); diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 639de0a66..ca142c6b9 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -183,13 +183,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) Node emptyBag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(skolem.getType()))); - // (bag.count x emptybag) = 0 + // (bag.count x (as bag.empty (Bag String))) = 0 Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL && response1.d_node == zero); - // (bag.count x (mkBag x c) = (ite (>= c 1) c 0) + // (bag.count x (bag x c) = (ite (>= c 1) c 0) Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three); Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); @@ -208,8 +208,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (duplicate_removal (mkBag x n)) = (mkBag x 1) - Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag); + // (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(), @@ -233,73 +233,73 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_max) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); + 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); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); - // (union_max A emptybag) = A - Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag); + // (bag.union_max A (as bag.empty (Bag String))) = A + Node unionMax1 = d_nodeManager->mkNode(BAG_UNION_MAX, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionMax1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_max emptybag A) = A - Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A); + // (bag.union_max (as bag.empty (Bag String)) A) = A + Node unionMax2 = d_nodeManager->mkNode(BAG_UNION_MAX, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionMax2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_max A A) = A - Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A); + // (bag.union_max A A) = A + Node unionMax3 = d_nodeManager->mkNode(BAG_UNION_MAX, A, A); RewriteResponse response3 = d_rewriter->postRewrite(unionMax3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max A B)) = (union_max A B) - Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB); + // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B) + Node unionMax4 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(unionMax4); ASSERT_TRUE(response4.d_node == unionMaxAB && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_max B A)) = (union_max B A) - Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA); + // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A) + Node unionMax5 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(unionMax5); ASSERT_TRUE(response5.d_node == unionMaxBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max A B) A) = (union_max A B) - Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A); + // (bag.union_max (bag.union_max A B) A) = (bag.union_max A B) + Node unionMax6 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(unionMax6); ASSERT_TRUE(response6.d_node == unionMaxAB && response6.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_max B A) A) = (union_max B A) - Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A); + // (bag.union_max (bag.union_max B A) A) = (bag.union_max B A) + Node unionMax7 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(unionMax7); ASSERT_TRUE(response7.d_node == unionMaxBA && response7.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint A B)) = (union_disjoint A B) - Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB); + // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B) + Node unionMax8 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(unionMax8); ASSERT_TRUE(response8.d_node == unionDisjointAB && response8.d_status == REWRITE_AGAIN_FULL); - // (union_max A (union_disjoint B A)) = (union_disjoint B A) - Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA); + // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A) + Node unionMax9 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(unionMax9); ASSERT_TRUE(response9.d_node == unionDisjointBA && response9.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint A B) A) = (union_disjoint A B) - Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A); + // (bag.union_max (bag.union_disjoint A B) A) = (bag.union_disjoint A B) + Node unionMax10 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(unionMax10); ASSERT_TRUE(response10.d_node == unionDisjointAB && response10.d_status == REWRITE_AGAIN_FULL); - // (union_max (union_disjoint B A) A) = (union_disjoint B A) - Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A); + // (bag.union_max (bag.union_disjoint B A) A) = (bag.union_disjoint B A) + Node unionMax11 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(unionMax11); ASSERT_TRUE(response11.d_node == unionDisjointBA && response11.d_status == REWRITE_AGAIN_FULL); @@ -324,46 +324,46 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint) elements[2], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B); + Node unionMaxAC = d_nodeManager->mkNode(BAG_UNION_MAX, A, C); + Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); - // (union_disjoint A emptybag) = A - Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag); + // (bag.union_disjoint A (as bag.empty (Bag String))) = A + Node unionDisjoint1 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint emptybag A) = A - Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A); + // (bag.union_disjoint (as bag.empty (Bag String)) A) = A + Node unionDisjoint2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2); ASSERT_TRUE(response2.d_node == A && response2.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (union_max A B) (intersection_min B A)) = - // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.union_max A B) (bag.inter_min B A)) = + // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint3 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAB, intersectionBA); RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3); ASSERT_TRUE(response3.d_node == unionDisjointAB && response3.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint4 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxBA, intersectionBA); RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4); ASSERT_TRUE(response4.d_node == unionDisjointBA && response4.d_status == REWRITE_AGAIN_FULL); - // (union_disjoint (intersection_min B A)) (union_max A B) = - // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) + // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) = + // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b) Node unionDisjoint5 = - d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB); + d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAC, intersectionAB); RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5); ASSERT_TRUE(response5.d_node == unionDisjoint5 && response5.d_status == REWRITE_DONE); @@ -383,73 +383,75 @@ TEST_F(TestTheoryWhiteBagsRewriter, intersection_min) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - - // (intersection_min A emptybag) = emptyBag - Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag); + 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); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + + // (bag.inter_min A (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) + Node n1 = d_nodeManager->mkNode(BAG_INTER_MIN, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptyBag && response1.d_status == REWRITE_AGAIN_FULL); - // (intersection_min emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A); + // (bag.inter_min (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_INTER_MIN, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A A) = A - Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A); + // (bag.inter_min A A) = A + Node n3 = d_nodeManager->mkNode(BAG_INTER_MIN, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == A && response3.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max A B) = A - Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB); + // (bag.inter_min A (bag.union_max A B) = A + Node n4 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxAB); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_max B A) = A - Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA); + // (bag.inter_min A (bag.union_max B A) = A + Node n5 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxBA); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == A && response4.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max A B) A) = A - Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A); + // (bag.inter_min (bag.union_max A B) A) = A + Node n6 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxAB, A); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == A && response6.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_max B A) A) = A - Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A); + // (bag.inter_min (bag.union_max B A) A) = A + Node n7 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxBA, A); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == A && response7.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint A B) = A - Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB); + // (bag.inter_min A (bag.union_disjoint A B) = A + Node n8 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == A && response8.d_status == REWRITE_AGAIN_FULL); - // (intersection_min A (union_disjoint B A) = A - Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA); + // (bag.inter_min A (bag.union_disjoint B A) = A + Node n9 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == A && response9.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint A B) A) = A - Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A); + // (bag.inter_min (bag.union_disjoint A B) A) = A + Node n10 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == A && response10.d_status == REWRITE_AGAIN_FULL); - // (intersection_min (union_disjoint B A) A) = A - Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A); + // (bag.inter_min (bag.union_disjoint B A) A) = A + Node n11 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == A && response11.d_status == REWRITE_AGAIN_FULL); @@ -469,75 +471,82 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_subtract A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag); + 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); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_subtract A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A); + // (bag.difference_subtract (as bag.empty (Bag String)) A) = + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A); + // (bag.difference_subtract A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint A B) A) = B - Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A); + // (bag.difference_subtract (bag.union_disjoint A B) A) = B + Node n4 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointAB, A); RewriteResponse response4 = d_rewriter->postRewrite(n4); ASSERT_TRUE(response4.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (union_disjoint B A) A) = B - Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A); + // (bag.difference_subtract (bag.union_disjoint B A) A) = B + Node n5 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointBA, A); RewriteResponse response5 = d_rewriter->postRewrite(n5); ASSERT_TRUE(response5.d_node == B && response4.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB); + // (bag.difference_subtract A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA); + // (bag.difference_subtract A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB); + // (bag.difference_subtract A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA); + // (bag.difference_subtract A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A); + // (bag.difference_subtract (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_subtract (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A); + // (bag.difference_subtract (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -557,63 +566,70 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove) d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1))); - Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B); - Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); - Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A); - Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B); - Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A); - - // (difference_remove A emptybag) = A - Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag); + 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); + Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A); + Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B); + Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A); + + // (bag.difference_remove A (as bag.empty (Bag String)) = A + Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, emptyBag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == A && response1.d_status == REWRITE_AGAIN_FULL); - // (difference_remove emptybag A) = emptyBag - Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A); + // (bag.difference_remove (as bag.empty (Bag String)) A)= + // (as bag.empty (Bag String)) + Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, emptyBag, A); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == emptyBag && response2.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A A) = emptybag - Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A); + // (bag.difference_remove A A) = (as bag.empty (Bag String)) + Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, A); RewriteResponse response3 = d_rewriter->postRewrite(n3); ASSERT_TRUE(response3.d_node == emptyBag && response3.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint A B)) = emptybag - Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB); + // (bag.difference_remove A (bag.union_disjoint A B)) = + // (as bag.empty (Bag String)) + Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointAB); RewriteResponse response6 = d_rewriter->postRewrite(n6); ASSERT_TRUE(response6.d_node == emptyBag && response6.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_disjoint B A)) = emptybag - Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA); + // (bag.difference_remove A (bag.union_disjoint B A)) = + // (as bag.empty (Bag String)) + Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointBA); RewriteResponse response7 = d_rewriter->postRewrite(n7); ASSERT_TRUE(response7.d_node == emptyBag && response7.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max A B)) = emptybag - Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB); + // (bag.difference_remove A (bag.union_max A B)) = + // (as bag.empty (Bag String)) + Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxAB); RewriteResponse response8 = d_rewriter->postRewrite(n8); ASSERT_TRUE(response8.d_node == emptyBag && response8.d_status == REWRITE_AGAIN_FULL); - // (difference_remove A (union_max B A)) = emptybag - Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA); + // (bag.difference_remove A (bag.union_max B A)) = + // (as bag.empty (Bag String)) + Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxBA); RewriteResponse response9 = d_rewriter->postRewrite(n9); ASSERT_TRUE(response9.d_node == emptyBag && response9.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min A B) A) = emptybag - Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A); + // (bag.difference_remove (bag.inter_min A B) A) = + // (as bag.empty (Bag String)) + Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionAB, A); RewriteResponse response10 = d_rewriter->postRewrite(n10); ASSERT_TRUE(response10.d_node == emptyBag && response10.d_status == REWRITE_AGAIN_FULL); - // (difference_remove (intersection_min B A) A) = emptybag - Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A); + // (bag.difference_remove (bag.inter_min B A) A) = + // (as bag.empty (Bag String)) + Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionBA, A); RewriteResponse response11 = d_rewriter->postRewrite(n11); ASSERT_TRUE(response11.d_node == emptyBag && response11.d_status == REWRITE_AGAIN_FULL); @@ -625,7 +641,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, choose) Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // (bag.choose (mkBag x c)) = x where c is a constant > 0 + // (bag.choose (bag x c)) = x where c is a constant > 0 Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == x @@ -649,22 +665,21 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) d_nodeManager->mkBag(d_nodeManager->stringType(), elements[1], d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); - // TODO(projects#223): enable this test after implementing bags normal form - // // (bag.card emptybag) = 0 - // Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == zero && response1.d_status == - // REWRITE_AGAIN_FULL); + // (bag.card (as bag.empty (Bag String)) = 0 + Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == zero + && response1.d_status == REWRITE_AGAIN_FULL); - // (bag.card (mkBag x c)) = c where c is a constant > 0 + // (bag.card (bag x c)) = c where c is a constant > 0 Node n2 = d_nodeManager->mkNode(BAG_CARD, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); ASSERT_TRUE(response2.d_node == c && response2.d_status == REWRITE_AGAIN_FULL); - // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B)) + // (bag.card (bag.union_disjoint A B)) = (+ (bag.card A) (bag.card B)) Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB); Node cardA = d_nodeManager->mkNode(BAG_CARD, A); Node cardB = d_nodeManager->mkNode(BAG_CARD, B); @@ -682,14 +697,13 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c); - // TODO(projects#223): complete this function - // (bag.is_singleton emptybag) = false - // Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); - // RewriteResponse response1 = d_rewriter->postRewrite(n1); - // ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) - // && response1.d_status == REWRITE_AGAIN_FULL); + // (bag.is_singleton (as bag.empty (Bag String)) = false + Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag); + RewriteResponse response1 = d_rewriter->postRewrite(n1); + ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) + && response1.d_status == REWRITE_AGAIN_FULL); - // (bag.is_singleton (mkBag x c) = (c == 1) + // (bag.is_singleton (bag x c) = (c == 1) Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag); RewriteResponse response2 = d_rewriter->postRewrite(n2); Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); @@ -703,7 +717,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set) Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x); - // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1) + // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1) Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton); RewriteResponse response = d_rewriter->postRewrite(n); Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)); @@ -720,7 +734,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set) x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5))); - // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x) + // (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); @@ -739,7 +753,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, xString); Node lambda = d_nodeManager->mkNode(LAMBDA, bound, empty); - // (bag.map (lambda ((x U)) t) emptybag) = emptybag + // (bag.map (lambda ((x U)) t) (as bag.empty (Bag String)) = + // (as bag.empty (Bag String)) Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString); RewriteResponse response1 = d_rewriter->postRewrite(n1); ASSERT_TRUE(response1.d_node == emptybagString @@ -756,14 +771,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, map) d_nodeManager->mkBag(d_nodeManager->stringType(), b, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))); - Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B); + Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B); ASSERT_TRUE(unionDisjointAB.isConst()); - // (bag.map (lambda ((x Int)) "") (union_disjoint (bag "a" 3) (bag "b" 4))) = - // (bag "" 7)) + // (bag.map + // (lambda ((x Int)) "") + // (bag.union_disjoint (bag "a" 3) (bag "b" 4))) = + // (bag "" 7)) Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB); - Node rewritten = Rewriter::rewrite(n2); Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index b516685af..7b5b3be2c 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -71,8 +71,8 @@ TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) d_nodeManager->stringType(), elements[0], d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))); - ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag)); - ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(), + ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag)); + ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(), bag.getType()); } @@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))); // only positive multiplicity are constants - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative)); - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero)); - ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative)); + ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, zero)); + ASSERT_TRUE(BagMakeTypeRule::computeIsConst(d_nodeManager, positive)); } TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) -- cgit v1.2.3