diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-11-12 15:33:16 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-12 21:33:16 +0000 |
| commit | cc4a58f5d43c62b72783d4bd1f4f00e6ef9257b4 (patch) | |
| tree | 628f9e849c17de977d143d7f5af24b2cbe924789 /src | |
| parent | 9b1c8a8053fdf57f6491ffd45be301e87e5df52e (diff) | |
bags: Rename kinds with a more consistent naming scheme (#7611)
Diffstat (limited to 'src')
30 files changed, 536 insertions, 527 deletions
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<Kind, cvc5::Kind> 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, Kind, cvc5::kind::KindHashFunction> {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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<EmptyBag>().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/make_bag_op.cpp b/src/theory/bags/bag_make_op.cpp index c03b21236..786267976 100644 --- a/src/theory/bags/make_bag_op.cpp +++ b/src/theory/bags/bag_make_op.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * A class for MK_BAG operator. + * A class for BAG_MAKE operator. */ -#include "make_bag_op.h" +#include "bag_make_op.h" #include <iostream> @@ -21,28 +21,28 @@ namespace cvc5 { -std::ostream& operator<<(std::ostream& out, const MakeBagOp& op) +std::ostream& operator<<(std::ostream& out, const BagMakeOp& op) { - return out << "(mkBag_op " << op.getType() << ')'; + return out << "(BagMakeOp " << op.getType() << ')'; } -size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const +size_t BagMakeOpHashFunction::operator()(const BagMakeOp& op) const { return std::hash<TypeNode>()(op.getType()); } -MakeBagOp::MakeBagOp(const TypeNode& elementType) +BagMakeOp::BagMakeOp(const TypeNode& elementType) : d_type(new TypeNode(elementType)) { } -MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType())) +BagMakeOp::BagMakeOp(const BagMakeOp& op) : d_type(new TypeNode(op.getType())) { } -const TypeNode& MakeBagOp::getType() const { return *d_type; } +const TypeNode& BagMakeOp::getType() const { return *d_type; } -bool MakeBagOp::operator==(const MakeBagOp& op) const +bool BagMakeOp::operator==(const BagMakeOp& op) const { return getType() == op.getType(); } diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/bag_make_op.h index 4756009ae..e4a7e9e8f 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/bag_make_op.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * A class for MK_BAG operator. + * A class for BAG_MAKE operator. */ #include "cvc5_public.h" -#ifndef CVC5__MAKE_BAG_OP_H -#define CVC5__MAKE_BAG_OP_H +#ifndef CVC5__BAG_MAKE_OP_H +#define CVC5__BAG_MAKE_OP_H #include <memory> @@ -25,39 +25,39 @@ namespace cvc5 { class TypeNode; /** - * The class is an operator for kind MK_BAG used to construct bags. + * 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 - * (mkBag (mkBag_op Real) 1) is of type (Bag Real), not (Bag Int). + * (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 MakeBagOp +class BagMakeOp { public: - explicit MakeBagOp(const TypeNode& elementType); - MakeBagOp(const MakeBagOp& op); + explicit BagMakeOp(const TypeNode& elementType); + BagMakeOp(const BagMakeOp& op); /** return the type of the current object */ const TypeNode& getType() const; - bool operator==(const MakeBagOp& op) const; + bool operator==(const BagMakeOp& op) const; private: /** a pointer to the type of the bag element */ std::unique_ptr<TypeNode> d_type; -}; /* class MakeBagOp */ +}; /* class BagMakeOp */ -std::ostream& operator<<(std::ostream& out, const MakeBagOp& op); +std::ostream& operator<<(std::ostream& out, const BagMakeOp& op); /** - * Hash function for the MakeBagOpHashFunction objects. + * Hash function for the BagMakeOpHashFunction objects. */ -struct MakeBagOpHashFunction +struct BagMakeOpHashFunction { - size_t operator()(const MakeBagOp& op) const; -}; /* struct MakeBagOpHashFunction */ + size_t operator()(const BagMakeOp& op) const; +}; /* struct BagMakeOpHashFunction */ } // namespace cvc5 -#endif /* CVC5__MAKE_BAG_OP_H */ +#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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> elements; const set<Node>& downwards = d_state.getElements(n); const set<Node>& 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<Rational>().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<Rational>().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<Node> left(n[0].begin(), n[0].end()); std::set<Node> 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<Rational>() > 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<Rational>().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<Node, Rational> elements = NormalForm::getBagElements(n[1]); std::map<Node, Rational> 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<Rewrite>* 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<RBuiltinOperator>" -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<RBuiltinOperator>" +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/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<Node, Rational> NormalForm::getBagElements(TNode n) Assert(n.isConst()) << "node " << n << " is not in a normal form" << std::endl; std::map<Node, Rational> 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<Rational>(); 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<Rational>(); elements[lastElement] = lastCount; @@ -210,7 +210,7 @@ Node NormalForm::constructConstantBagFromElements( Node n = nm->mkBag(elementType, it->first, nm->mkConst<Rational>(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<Rational>().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<Node, Rational> elements = getBagElements(n[1]); std::map<Node, Rational>::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<Node, Rational> 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<Node, Rational>& elements, std::map<Node, Rational>::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<Node, Rational>& elements, std::map<Node, Rational>::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<Node, Rational>& elements, std::map<Node, Rational>::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<Node, Rational>& elements, std::map<Node, Rational>::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<Node, Rational>& elements, std::map<Node, Rational>::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<Node, Rational> 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<Rational>().isOne()) + if (n[0].getKind() == BAG_MAKE && n[0][1].getConst<Rational>().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<Node> 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<Node, Rational> 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<MakeBagOp>(); + Assert(n.getKind() == kind::BAG_MAKE && n.hasOperator() + && n.getOperator().getKind() == kind::BAG_MAKE_OP); + BagMakeOp op = n.getOperator().getConst<BagMakeOp>(); 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<EmptyBag>(); 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, |