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
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
{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},
{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},
// 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()
* Create with:
* mkEmptyBag(const Sort& sort)
*/
- EMPTYBAG,
+ BAG_EMPTY,
/**
* Bag max union.
* Parameters:
* - `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).
*
* - `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).
*
* - `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).
* - `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).
*
* - `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).
* - `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
*
* - `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.
*
* Create with:
* - `Solver::mkTerm(Kind kind, const Term& child) const`
*/
- MK_BAG,
+ BAG_MAKE,
/**
* Bag cardinality.
*
#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"
<< "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;
}
{
t = d_solver->mkEmptySet(s);
}
- else if (k == api::EMPTYBAG)
+ else if (k == api::BAG_EMPTY)
{
t = d_solver->mkEmptyBag(s);
}
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");
out << ")";
break;
- case kind::EMPTYBAG:
- out << "(as emptybag ";
+ case kind::BAG_EMPTY:
+ out << "(as bag.empty ";
toStreamType(out, n.getConst<EmptyBag>().getType());
out << ")";
break;
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(
// 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";
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);
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())
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)
{
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A class for BAG_MAKE operator.
+ */
+
+#include "bag_make_op.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& out, const BagMakeOp& op)
+{
+ return out << "(BagMakeOp " << op.getType() << ')';
+}
+
+size_t BagMakeOpHashFunction::operator()(const BagMakeOp& op) const
+{
+ return std::hash<TypeNode>()(op.getType());
+}
+
+BagMakeOp::BagMakeOp(const TypeNode& elementType)
+ : d_type(new TypeNode(elementType))
+{
+}
+
+BagMakeOp::BagMakeOp(const BagMakeOp& op) : d_type(new TypeNode(op.getType()))
+{
+}
+
+const TypeNode& BagMakeOp::getType() const { return *d_type; }
+
+bool BagMakeOp::operator==(const BagMakeOp& op) const
+{
+ return getType() == op.getType();
+}
+
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mudathir Mohamed, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A class for BAG_MAKE operator.
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__BAG_MAKE_OP_H
+#define CVC5__BAG_MAKE_OP_H
+
+#include <memory>
+
+namespace cvc5 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind BAG_MAKE used to construct bags.
+ * It specifies the type of the element especially when it is a constant.
+ * e.g. the type of rational 1 is Int, however
+ * (bag (BagMakeOp Real) 1) is of type (Bag Real), not (Bag Int).
+ * Note that the type passed to the constructor is the element's type, not the
+ * bag type.
+ */
+class BagMakeOp
+{
+ public:
+ explicit BagMakeOp(const TypeNode& elementType);
+ BagMakeOp(const BagMakeOp& op);
+
+ /** return the type of the current object */
+ const TypeNode& getType() const;
+
+ bool operator==(const BagMakeOp& op) const;
+
+ private:
+ /** a pointer to the type of the bag element */
+ std::unique_ptr<TypeNode> d_type;
+}; /* class BagMakeOp */
+
+std::ostream& operator<<(std::ostream& out, const BagMakeOp& op);
+
+/**
+ * Hash function for the BagMakeOpHashFunction objects.
+ */
+struct BagMakeOpHashFunction
+{
+ size_t operator()(const BagMakeOp& op) const;
+}; /* struct BagMakeOpHashFunction */
+
+} // namespace cvc5
+
+#endif /* CVC5__BAG_MAKE_OP_H */
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;
}
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);
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)
{
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)
{
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)
{
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)
{
}
}
-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);
}
}
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)
{
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]);
/** 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.
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;
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);
}
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);
}
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);
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);
}
}
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);
}
}
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);
}
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);
}
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);
}
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);
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);
}
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);
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);
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;
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);
}
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;
/**
* 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
*/
/**
* 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
*/
/**
* 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;
/**
* 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;
/**
* 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))
*
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
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());
/*
*/
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);
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);
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];
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];
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];
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];
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];
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];
* (= (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);
/**
* (>= 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
properties check presolve
# constants
-constant EMPTYBAG \
+constant BAG_EMPTY \
class \
EmptyBag \
::cvc5::EmptyBagHashFunction \
"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
# 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
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mudathir Mohamed
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for MK_BAG operator.
- */
-
-#include "make_bag_op.h"
-
-#include <iostream>
-
-#include "expr/type_node.h"
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, const MakeBagOp& op)
-{
- return out << "(mkBag_op " << op.getType() << ')';
-}
-
-size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const
-{
- return std::hash<TypeNode>()(op.getType());
-}
-
-MakeBagOp::MakeBagOp(const TypeNode& elementType)
- : d_type(new TypeNode(elementType))
-{
-}
-
-MakeBagOp::MakeBagOp(const MakeBagOp& op) : d_type(new TypeNode(op.getType()))
-{
-}
-
-const TypeNode& MakeBagOp::getType() const { return *d_type; }
-
-bool MakeBagOp::operator==(const MakeBagOp& op) const
-{
- return getType() == op.getType();
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Mudathir Mohamed, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * A class for MK_BAG operator.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__MAKE_BAG_OP_H
-#define CVC5__MAKE_BAG_OP_H
-
-#include <memory>
-
-namespace cvc5 {
-
-class TypeNode;
-
-/**
- * The class is an operator for kind MK_BAG used to construct bags.
- * It specifies the type of the element especially when it is a constant.
- * e.g. the type of rational 1 is Int, however
- * (mkBag (mkBag_op Real) 1) is of type (Bag Real), not (Bag Int).
- * Note that the type passed to the constructor is the element's type, not the
- * bag type.
- */
-class MakeBagOp
-{
- public:
- explicit MakeBagOp(const TypeNode& elementType);
- MakeBagOp(const MakeBagOp& op);
-
- /** return the type of the current object */
- const TypeNode& getType() const;
-
- bool operator==(const MakeBagOp& op) const;
-
- private:
- /** a pointer to the type of the bag element */
- std::unique_ptr<TypeNode> d_type;
-}; /* class MakeBagOp */
-
-std::ostream& operator<<(std::ostream& out, const MakeBagOp& op);
-
-/**
- * Hash function for the MakeBagOpHashFunction objects.
- */
-struct MakeBagOpHashFunction
-{
- size_t operator()(const MakeBagOp& op) const;
-}; /* struct MakeBagOpHashFunction */
-
-} // namespace cvc5
-
-#endif /* CVC5__MAKE_BAG_OP_H */
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;
// 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;
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;
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;
}
}
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);
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;
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;
}
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;
}
{
// 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;
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]);
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
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,
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,
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,
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,
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,
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];
}
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);
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);
}
// 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 =
// 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]);
// 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)
/**
* 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);
/**
* 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.
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);
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
*/
/**
* 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);
{
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";
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";
{
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,
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,
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))
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
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);
// (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
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);
#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"
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)
{
{
// 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);
}
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)
if (!bagType.isComparableTo(secondBagType))
{
throw TypeCheckingExceptionPrivate(
- n, "SUBBAG operating on bags of different types");
+ n, "BAG_SUBBAG operating on bags of different types");
}
}
}
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;
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)
{
{
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;
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()
TNode n,
bool check)
{
- Assert(n.getKind() == kind::EMPTYBAG);
+ Assert(n.getKind() == kind::BAG_EMPTY);
EmptyBag emptyBag = n.getConst<EmptyBag>();
return emptyBag.getType();
}
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
{
}; /* 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
{
}; /* 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
{
* 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.
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
{
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";
// ---------------------------------- bags theory
BAGS_NON_NEGATIVE_COUNT,
- BAGS_MK_BAG,
+ BAGS_BAG_MAKE,
BAGS_EQUALITY,
BAGS_DISEQUALITY,
BAGS_EMPTY,
(set-info :status sat)
(declare-fun A () (Bag Int))
(declare-fun a () Int)
-(assert (not (= A (as emptybag (Bag Int)))))
+(assert (not (= A (as bag.empty (Bag Int)))))
(assert (= (bag.choose A) 10))
(assert (= a (bag.choose A)))
(assert (exists ((x Int)) (and (= x (bag.choose A)) (= x a))))
(set-info :status sat)
(declare-fun A () (Bag Int))
(assert (= (bag.choose A) 10))
-(assert (= A (as emptybag (Bag Int))))
+(assert (= A (as bag.empty (Bag Int))))
(check-sat)
(set-info :status sat)
(declare-fun A () (Bag Int))
(declare-fun a () Int)
-(assert (not (= A (as emptybag (Bag Int)))))
+(assert (not (= A (as bag.empty (Bag Int)))))
(assert (> (bag.count 10 A) 0))
(assert (= a (bag.choose A)))
(check-sat)
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_disjoint B (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_disjoint B (bag y 2))))
(assert (= x y))
(check-sat)
(set-option :produce-models true)
(declare-fun A () (Bag String))
(declare-fun B () (Bag String))
-(assert (= B (duplicate_removal A)))
-(assert (distinct (as emptybag (Bag String)) A B))
+(assert (= B (bag.duplicate_removal A)))
+(assert (distinct (as bag.empty (Bag String)) A B))
(check-sat)
(set-info :status unsat)
(declare-fun A () (Bag String))
(declare-fun B () (Bag String))
-(assert (= B (duplicate_removal A)))
-(assert (distinct (as emptybag (Bag String)) A B))
-(assert (= B (union_max A B)))
+(assert (= B (bag.duplicate_removal A)))
+(assert (distinct (as bag.empty (Bag String)) A B))
+(assert (= B (bag.union_max A B)))
(check-sat)
\ No newline at end of file
(declare-fun x () String)
(declare-fun y () Int)
(assert (= x "x"))
-(assert (= A (as emptybag (Bag String))))
+(assert (= A (as bag.empty (Bag String))))
(assert (= (bag.count x A) y))
(assert(> y 1))
(check-sat)
(declare-fun c () Int) ; c here is zero
(assert
(and
- (= b (difference_subtract b a)) ; b is empty
+ (= b (bag.difference_subtract b a)) ; b is empty
(= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|}
(check-sat)
(let ((D (bag d c))) ; when c = zero, then D is empty
(and
(= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty
- (= a (union_max a D))
- (= a (difference_subtract a (bag d 1)))
- (= a (union_disjoint a D))
- (= a (intersection_min a D)))))
+ (= a (bag.union_max a D))
+ (= a (bag.difference_subtract a (bag d 1)))
+ (= a (bag.union_disjoint a D))
+ (= a (bag.inter_min a D)))))
(check-sat)
(assert
(not
(=
- (= A (difference_remove (bag d c) A))
+ (= A (bag.difference_remove (bag d c) A))
(= A (bag (tuple c c) c)))))
(check-sat)
(assert
(not
(=
- (= A (bag d (+ c (bag.count d (union_disjoint A A)))))
- (= A (difference_remove (bag d c) A)))))
+ (= A (bag d (+ c (bag.count d (bag.union_disjoint A A)))))
+ (= A (bag.difference_remove (bag d c) A)))))
(assert (= A (bag (tuple 0 0) 5)))
(assert (= c (- 5)))
(assert (= d (tuple 0 0)))
(and
(not
(= (= A (bag (tuple 0 c) (+ c c)))
- (= A (difference_remove (bag d c) A))))
+ (= A (bag.difference_remove (bag d c) A))))
(not
(= (= A (bag (tuple 0 1) c_plus_1))
(= A (bag (tuple c 1) c_plus_1)))))))
(declare-fun A () (Bag String))
(declare-fun B () (Bag String))
(declare-fun C () (Bag String))
-(assert (= C (intersection_min A B)))
-(assert (distinct (as emptybag (Bag String)) C))
+(assert (= C (bag.inter_min A B)))
+(assert (distinct (as bag.empty (Bag String)) C))
(assert (distinct A B C))
(check-sat)
\ No newline at end of file
(declare-fun A () (Bag String))
(declare-fun B () (Bag String))
(declare-fun C () (Bag String))
-(assert (= C (intersection_min A B)))
-(assert (= C (union_disjoint A B)))
-(assert (distinct (as emptybag (Bag String)) C))
+(assert (= C (bag.inter_min A B)))
+(assert (= C (bag.union_disjoint A B)))
+(assert (distinct (as bag.empty (Bag String)) C))
(check-sat)
(declare-fun A () (Bag Int))
(declare-fun B () (Bag Int))
(declare-fun x () Int)
-(assert (not (= A (union_max (bag x 1) (bag 0 1)))))
-(assert (= A (union_disjoint B (bag 0 1))))
+(assert (not (= A (bag.union_max (bag x 1) (bag 0 1)))))
+(assert (= A (bag.union_disjoint B (bag 0 1))))
(assert (= x 1))
(check-sat)
\ No newline at end of file
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun f (Int) Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
(assert (= B (bag.map f A)))
(assert (distinct (f x) (f y) x y))
(check-sat)
(define-fun f ((x Int)) Int (+ x 1))
(assert (= B (bag.map f A)))
(assert (= (bag.count (- 2) B) 57))
-(assert (= A (as emptybag (Bag Int)) ))
+(assert (= A (as bag.empty (Bag Int)) ))
(check-sat)
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(assert (= x 1))
-(assert (subbag A B))
-(assert (subbag B A))
+(assert (bag.subbag A B))
+(assert (bag.subbag B A))
(assert (= (bag.count x A) 5))
(assert (= (bag.count x B) 10))
(check-sat)
\ No newline at end of file
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (subbag A B))
-(assert (subbag B A))
+(assert (bag.subbag A B))
+(assert (bag.subbag B A))
(assert (= (bag.count x A) x))
(assert (= (bag.count y A) x))
(assert (distinct x y))
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (= A (union_disjoint (bag x 1) (bag y 2))))
-(assert (= A (union_disjoint B (bag y 2))))
+(assert (= A (bag.union_disjoint (bag x 1) (bag y 2))))
+(assert (= A (bag.union_disjoint B (bag y 2))))
(assert (= x y))
(check-sat)
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_disjoint B (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_disjoint B (bag y 2))))
(assert (= x y))
(check-sat)
\ No newline at end of file
(declare-fun B () (Bag Int))
(declare-fun x () Int)
(declare-fun y () Int)
-(assert (= A (union_max (bag x 1) (bag y 2))))
-(assert (= A (union_disjoint B (bag y 2))))
+(assert (= A (bag.union_max (bag x 1) (bag y 2))))
+(assert (= A (bag.union_disjoint B (bag y 2))))
(assert (= x y))
-(assert (distinct (as emptybag (Bag Int)) B))
+(assert (distinct (as bag.empty (Bag Int)) B))
(check-sat)
\ No newline at end of file
{
// Examples
// -------
- // (bag.count "x" (emptybag String)) = 0
- // (bag.count "x" (mkBag "y" 5)) = 0
- // (bag.count "x" (mkBag "x" 4)) = 4
- // (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4
- // (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0
+ // (bag.count "x" (as bag.empty (Bag String))) = 0
+ // (bag.count "x" (bag "y" 5)) = 0
+ // (bag.count "x" (bag "x" 4)) = 4
+ // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4
+ // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0
Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
Node output3 = four;
ASSERT_EQ(output2, NormalForm::evaluate(input2));
- Node unionDisjointXY = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
+ Node unionDisjointXY = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5);
Node input4 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointXY);
Node output4 = four;
ASSERT_EQ(output3, NormalForm::evaluate(input3));
- Node unionDisjointYZ = d_nodeManager->mkNode(UNION_DISJOINT, y_5, z_5);
+ Node unionDisjointYZ = d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_5, z_5);
Node input5 = d_nodeManager->mkNode(BAG_COUNT, x, unionDisjointYZ);
Node output5 = zero;
ASSERT_EQ(output4, NormalForm::evaluate(input4));
{
// Examples
// --------
- // - (duplicate_removal (emptybag String)) = (emptybag String)
- // - (duplicate_removal (mkBag "x" 4)) = (emptybag "x" 1)
- // - (duplicate_removal (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
- // (disjoint_union (mkBag "x" 1) (mkBag "y" 1)
+ // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag
+ // String))
+ // - (bag.duplicate_removal (bag "x" 4)) = (bag.empty"x" 1)
+ // - (bag.duplicate_removal (bag.union_disjoint(bag "x" 3) (bag "y" 5)) =
+ // (bag.union_disjoint(bag "x" 1) (bag "y" 1)
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node input1 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, emptybag);
+ Node input1 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, emptybag);
Node output1 = emptybag;
ASSERT_EQ(output1, NormalForm::evaluate(input1));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
- Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4);
+ Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4);
Node output2 = x_1;
ASSERT_EQ(output2, NormalForm::evaluate(input2));
- Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
- Node input3 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, normalBag);
- Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
+ Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5);
+ Node input3 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, normalBag);
+ Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1);
ASSERT_EQ(output3, NormalForm::evaluate(input3));
}
{
// Example
// -------
- // input: (union_max A B)
- // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
- // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
+ // input: (bag.union_max A B)
+ // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2)))
+ // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1)))
// output:
- // (union_disjoint A B)
- // where A = (MK_BAG "x" 4)
- // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2)))
+ // (bag.union_disjoint A B)
+ // where A = (bag "x" 4)
+ // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2)))
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
- Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
- Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
- Node input = d_nodeManager->mkNode(UNION_MAX, A, B);
+ Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
+ Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
+ Node input = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
// output
Node output = d_nodeManager->mkNode(
- UNION_DISJOINT, x_4, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2));
+ BAG_UNION_DISJOINT,
+ x_4,
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2));
ASSERT_TRUE(output.isConst());
ASSERT_EQ(output, NormalForm::evaluate(input));
elements[2],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
// unionDisjointAB is already in a normal form
ASSERT_TRUE(unionDisjointAB.isConst());
ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointAB));
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
- // unionDisjointAB is is the normal form of unionDisjointBA
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
+ // unionDisjointAB is the normal form of unionDisjointBA
ASSERT_FALSE(unionDisjointBA.isConst());
ASSERT_EQ(unionDisjointAB, NormalForm::evaluate(unionDisjointBA));
Node unionDisjointAB_C =
- d_nodeManager->mkNode(UNION_DISJOINT, unionDisjointAB, C);
- Node unionDisjointBC = d_nodeManager->mkNode(UNION_DISJOINT, B, C);
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionDisjointAB, C);
+ Node unionDisjointBC = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, C);
Node unionDisjointA_BC =
- d_nodeManager->mkNode(UNION_DISJOINT, A, unionDisjointBC);
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, unionDisjointBC);
// unionDisjointA_BC is the normal form of unionDisjointAB_C
ASSERT_FALSE(unionDisjointAB_C.isConst());
ASSERT_TRUE(unionDisjointA_BC.isConst());
ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C));
- Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A);
+ Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A);
Node AA =
d_nodeManager->mkBag(d_nodeManager->stringType(),
elements[0],
{
// Example
// -------
- // input: (union_disjoint A B)
- // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
- // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
+ // input: (bag.union_disjoint A B)
+ // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2)))
+ // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1)))
// output:
- // (union_disjoint A B)
- // where A = (MK_BAG "x" 7)
- // B = (union_disjoint (MK_BAG "y" 1) (MK_BAG "z" 2)))
+ // (bag.union_disjoint A B)
+ // where A = (bag "x" 7)
+ // B = (bag.union_disjoint (bag "y" 1) (bag "z" 2)))
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
- Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
- Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
- Node input = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
+ Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
+ Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
+ Node input = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
// output
Node output = d_nodeManager->mkNode(
- UNION_DISJOINT, x_7, d_nodeManager->mkNode(UNION_DISJOINT, y_1, z_2));
+ BAG_UNION_DISJOINT,
+ x_7,
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, y_1, z_2));
ASSERT_TRUE(output.isConst());
ASSERT_EQ(output, NormalForm::evaluate(input));
{
// Example
// -------
- // input: (intersection_min A B)
- // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
- // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
+ // input: (bag.inter_min A B)
+ // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2)))
+ // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1)))
// output:
- // (MK_BAG "x" 3)
+ // (bag "x" 3)
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
- Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
- Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
- Node input = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
+ Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
+ Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
+ Node input = d_nodeManager->mkNode(BAG_INTER_MIN, A, B);
// output
Node output = x_3;
{
// Example
// -------
- // input: (difference_subtract A B)
- // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
- // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
+ // input: (bag.difference_subtract A B)
+ // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2)))
+ // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1)))
// output:
- // (union_disjoint (MK_BAG "x" 1) (MK_BAG "z" 2))
+ // (bag.union_disjoint (bag "x" 1) (bag "z" 2))
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
- Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
- Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
- Node input = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, B);
+ Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
+ Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
+ Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, B);
// output
- Node output = d_nodeManager->mkNode(UNION_DISJOINT, x_1, z_2);
+ Node output = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, z_2);
ASSERT_TRUE(output.isConst());
ASSERT_EQ(output, NormalForm::evaluate(input));
{
// Example
// -------
- // input: (difference_remove A B)
- // where A = (union_disjoint (MK_BAG "x" 4) (MK_BAG "z" 2)))
- // B = (union_disjoint (MK_BAG "x" 3) (MK_BAG "y" 1)))
+ // input: (bag.difference_remove A B)
+ // where A = (bag.union_disjoint (bag "x" 4) (bag "z" 2)))
+ // B = (bag.union_disjoint (bag "x" 3) (bag "y" 1)))
// output:
- // (MK_BAG "z" 2)
+ // (bag "z" 2)
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
y,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
- Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
- Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
- Node input = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, B);
+ Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
+ Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
+ Node input = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, B);
// output
Node output = z_2;
{
// Examples
// --------
- // - (card (emptybag String)) = 0
- // - (choose (MK_BAG "x" 4)) = 4
- // - (choose (union_disjoint (MK_BAG "x" 4) (MK_BAG "y" 1))) = 5
+ // - (bag.card (as bag.empty (Bag String))) = 0
+ // - (bag.choose (bag "x" 4)) = 4
+ // - (bag.choose (bag.union_disjoint (bag "x" 4) (bag "y" 1))) = 5
Node empty = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node x = d_nodeManager->mkConst(String("x"));
Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
ASSERT_EQ(output2, NormalForm::evaluate(input2));
- Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1);
+ Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1);
Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint);
Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
ASSERT_EQ(output3, NormalForm::evaluate(input3));
{
// Examples
// --------
- // - (bag.is_singleton (emptybag String)) = false
- // - (bag.is_singleton (MK_BAG "x" 1)) = true
- // - (bag.is_singleton (MK_BAG "x" 4)) = false
- // - (bag.is_singleton (union_disjoint (MK_BAG "x" 1) (MK_BAG "y" 1))) =
+ // - (bag.is_singleton (as bag.empty (Bag String))) = false
+ // - (bag.is_singleton (bag "x" 1)) = true
+ // - (bag.is_singleton (bag "x" 4)) = false
+ // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) =
// false
Node falseNode = d_nodeManager->mkConst(false);
Node trueNode = d_nodeManager->mkConst(true);
Node output3 = falseNode;
ASSERT_EQ(output2, NormalForm::evaluate(input2));
- Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
+ Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1);
Node input4 = d_nodeManager->mkNode(BAG_IS_SINGLETON, union_disjoint);
Node output4 = falseNode;
ASSERT_EQ(output3, NormalForm::evaluate(input3));
{
// Examples
// --------
- // - (bag.from_set (emptyset String)) = (emptybag String)
- // - (bag.from_set (singleton "x")) = (mkBag "x" 1)
- // - (bag.to_set (union (singleton "x") (singleton "y"))) =
- // (disjoint_union (mkBag "x" 1) (mkBag "y" 1))
+ // - (bag.from_set (as set.empty (Bag String))) = (as bag.empty (Bag String))
+ // - (bag.from_set (set.singleton "x")) = (bag "x" 1)
+ // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) =
+ // (bag.union_disjoint (bag "x" 1) (bag "y" 1))
Node emptyset = d_nodeManager->mkConst(
EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType())));
// for normal sets, the first node is the largest, not smallest
Node normalSet = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton);
Node input3 = d_nodeManager->mkNode(BAG_FROM_SET, normalSet);
- Node output3 = d_nodeManager->mkNode(UNION_DISJOINT, x_1, y_1);
+ Node output3 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_1, y_1);
ASSERT_EQ(output3, NormalForm::evaluate(input3));
}
{
// Examples
// --------
- // - (bag.to_set (emptybag String)) = (emptyset String)
- // - (bag.to_set (mkBag "x" 4)) = (singleton "x")
- // - (bag.to_set (disjoint_union (mkBag "x" 3) (mkBag "y" 5)) =
- // (union (singleton "x") (singleton "y")))
+ // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Bag String))
+ // - (bag.to_set (bag "x" 4)) = (set.singleton "x")
+ // - (bag.to_set (bag.union_disjoint(bag "x" 3) (bag "y" 5)) =
+ // (set.union (set.singleton "x") (set.singleton "y")))
Node emptyset = d_nodeManager->mkConst(
EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType())));
ASSERT_EQ(output2, NormalForm::evaluate(input2));
// for normal sets, the first node is the largest, not smallest
- Node normalBag = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_5);
+ Node normalBag = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_5);
Node input3 = d_nodeManager->mkNode(BAG_TO_SET, normalBag);
Node output3 = d_nodeManager->mkNode(SET_UNION, ySingleton, xSingleton);
ASSERT_EQ(output3, NormalForm::evaluate(input3));
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
- // (bag.count x emptybag) = 0
+ // (bag.count x (as bag.empty (Bag String))) = 0
Node n1 = d_nodeManager->mkNode(BAG_COUNT, skolem, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_status == REWRITE_AGAIN_FULL
&& response1.d_node == zero);
- // (bag.count x (mkBag x c) = (ite (>= c 1) c 0)
+ // (bag.count x (bag x c) = (ite (>= c 1) c 0)
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), skolem, three);
Node n2 = d_nodeManager->mkNode(BAG_COUNT, skolem, bag);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
x,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
- // (duplicate_removal (mkBag x n)) = (mkBag x 1)
- Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag);
+ // (bag.duplicate_removal (bag x n)) = (bag x 1)
+ Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag);
RewriteResponse response = d_rewriter->postRewrite(n);
Node noDuplicate =
d_nodeManager->mkBag(d_nodeManager->stringType(),
d_nodeManager->stringType(),
elements[1],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
- Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
- Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
+ Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
+ Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
- // (union_max A emptybag) = A
- Node unionMax1 = d_nodeManager->mkNode(UNION_MAX, A, emptyBag);
+ // (bag.union_max A (as bag.empty (Bag String))) = A
+ Node unionMax1 = d_nodeManager->mkNode(BAG_UNION_MAX, A, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(unionMax1);
ASSERT_TRUE(response1.d_node == A
&& response1.d_status == REWRITE_AGAIN_FULL);
- // (union_max emptybag A) = A
- Node unionMax2 = d_nodeManager->mkNode(UNION_MAX, emptyBag, A);
+ // (bag.union_max (as bag.empty (Bag String)) A) = A
+ Node unionMax2 = d_nodeManager->mkNode(BAG_UNION_MAX, emptyBag, A);
RewriteResponse response2 = d_rewriter->postRewrite(unionMax2);
ASSERT_TRUE(response2.d_node == A
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (union_max A A) = A
- Node unionMax3 = d_nodeManager->mkNode(UNION_MAX, A, A);
+ // (bag.union_max A A) = A
+ Node unionMax3 = d_nodeManager->mkNode(BAG_UNION_MAX, A, A);
RewriteResponse response3 = d_rewriter->postRewrite(unionMax3);
ASSERT_TRUE(response3.d_node == A
&& response3.d_status == REWRITE_AGAIN_FULL);
- // (union_max A (union_max A B)) = (union_max A B)
- Node unionMax4 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxAB);
+ // (bag.union_max A (bag.union_max A B)) = (bag.union_max A B)
+ Node unionMax4 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxAB);
RewriteResponse response4 = d_rewriter->postRewrite(unionMax4);
ASSERT_TRUE(response4.d_node == unionMaxAB
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (union_max A (union_max B A)) = (union_max B A)
- Node unionMax5 = d_nodeManager->mkNode(UNION_MAX, A, unionMaxBA);
+ // (bag.union_max A (bag.union_max B A)) = (bag.union_max B A)
+ Node unionMax5 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionMaxBA);
RewriteResponse response5 = d_rewriter->postRewrite(unionMax5);
ASSERT_TRUE(response5.d_node == unionMaxBA
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (union_max (union_max A B) A) = (union_max A B)
- Node unionMax6 = d_nodeManager->mkNode(UNION_MAX, unionMaxAB, A);
+ // (bag.union_max (bag.union_max A B) A) = (bag.union_max A B)
+ Node unionMax6 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxAB, A);
RewriteResponse response6 = d_rewriter->postRewrite(unionMax6);
ASSERT_TRUE(response6.d_node == unionMaxAB
&& response6.d_status == REWRITE_AGAIN_FULL);
- // (union_max (union_max B A) A) = (union_max B A)
- Node unionMax7 = d_nodeManager->mkNode(UNION_MAX, unionMaxBA, A);
+ // (bag.union_max (bag.union_max B A) A) = (bag.union_max B A)
+ Node unionMax7 = d_nodeManager->mkNode(BAG_UNION_MAX, unionMaxBA, A);
RewriteResponse response7 = d_rewriter->postRewrite(unionMax7);
ASSERT_TRUE(response7.d_node == unionMaxBA
&& response7.d_status == REWRITE_AGAIN_FULL);
- // (union_max A (union_disjoint A B)) = (union_disjoint A B)
- Node unionMax8 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointAB);
+ // (bag.union_max A (bag.union_disjoint A B)) = (bag.union_disjoint A B)
+ Node unionMax8 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointAB);
RewriteResponse response8 = d_rewriter->postRewrite(unionMax8);
ASSERT_TRUE(response8.d_node == unionDisjointAB
&& response8.d_status == REWRITE_AGAIN_FULL);
- // (union_max A (union_disjoint B A)) = (union_disjoint B A)
- Node unionMax9 = d_nodeManager->mkNode(UNION_MAX, A, unionDisjointBA);
+ // (bag.union_max A (bag.union_disjoint B A)) = (bag.union_disjoint B A)
+ Node unionMax9 = d_nodeManager->mkNode(BAG_UNION_MAX, A, unionDisjointBA);
RewriteResponse response9 = d_rewriter->postRewrite(unionMax9);
ASSERT_TRUE(response9.d_node == unionDisjointBA
&& response9.d_status == REWRITE_AGAIN_FULL);
- // (union_max (union_disjoint A B) A) = (union_disjoint A B)
- Node unionMax10 = d_nodeManager->mkNode(UNION_MAX, unionDisjointAB, A);
+ // (bag.union_max (bag.union_disjoint A B) A) = (bag.union_disjoint A B)
+ Node unionMax10 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointAB, A);
RewriteResponse response10 = d_rewriter->postRewrite(unionMax10);
ASSERT_TRUE(response10.d_node == unionDisjointAB
&& response10.d_status == REWRITE_AGAIN_FULL);
- // (union_max (union_disjoint B A) A) = (union_disjoint B A)
- Node unionMax11 = d_nodeManager->mkNode(UNION_MAX, unionDisjointBA, A);
+ // (bag.union_max (bag.union_disjoint B A) A) = (bag.union_disjoint B A)
+ Node unionMax11 = d_nodeManager->mkNode(BAG_UNION_MAX, unionDisjointBA, A);
RewriteResponse response11 = d_rewriter->postRewrite(unionMax11);
ASSERT_TRUE(response11.d_node == unionDisjointBA
&& response11.d_status == REWRITE_AGAIN_FULL);
elements[2],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2)));
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
- Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
- Node unionMaxAC = d_nodeManager->mkNode(UNION_MAX, A, C);
- Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
- Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
- Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
+ Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
+ Node unionMaxAC = d_nodeManager->mkNode(BAG_UNION_MAX, A, C);
+ Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
+ Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B);
+ Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A);
- // (union_disjoint A emptybag) = A
- Node unionDisjoint1 = d_nodeManager->mkNode(UNION_DISJOINT, A, emptyBag);
+ // (bag.union_disjoint A (as bag.empty (Bag String))) = A
+ Node unionDisjoint1 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(unionDisjoint1);
ASSERT_TRUE(response1.d_node == A
&& response1.d_status == REWRITE_AGAIN_FULL);
- // (union_disjoint emptybag A) = A
- Node unionDisjoint2 = d_nodeManager->mkNode(UNION_DISJOINT, emptyBag, A);
+ // (bag.union_disjoint (as bag.empty (Bag String)) A) = A
+ Node unionDisjoint2 = d_nodeManager->mkNode(BAG_UNION_DISJOINT, emptyBag, A);
RewriteResponse response2 = d_rewriter->postRewrite(unionDisjoint2);
ASSERT_TRUE(response2.d_node == A
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (union_disjoint (union_max A B) (intersection_min B A)) =
- // (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
+ // (bag.union_disjoint (bag.union_max A B) (bag.inter_min B A)) =
+ // (bag.union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
Node unionDisjoint3 =
- d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAB, intersectionBA);
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAB, intersectionBA);
RewriteResponse response3 = d_rewriter->postRewrite(unionDisjoint3);
ASSERT_TRUE(response3.d_node == unionDisjointAB
&& response3.d_status == REWRITE_AGAIN_FULL);
- // (union_disjoint (intersection_min B A)) (union_max A B) =
- // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
+ // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) =
+ // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
Node unionDisjoint4 =
- d_nodeManager->mkNode(UNION_DISJOINT, unionMaxBA, intersectionBA);
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxBA, intersectionBA);
RewriteResponse response4 = d_rewriter->postRewrite(unionDisjoint4);
ASSERT_TRUE(response4.d_node == unionDisjointBA
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (union_disjoint (intersection_min B A)) (union_max A B) =
- // (union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
+ // (bag.union_disjoint (bag.inter_min B A)) (bag.union_max A B) =
+ // (bag.union_disjoint B A) // sum(a,b) = max(a,b) + min(a,b)
Node unionDisjoint5 =
- d_nodeManager->mkNode(UNION_DISJOINT, unionMaxAC, intersectionAB);
+ d_nodeManager->mkNode(BAG_UNION_DISJOINT, unionMaxAC, intersectionAB);
RewriteResponse response5 = d_rewriter->postRewrite(unionDisjoint5);
ASSERT_TRUE(response5.d_node == unionDisjoint5
&& response5.d_status == REWRITE_DONE);
d_nodeManager->stringType(),
elements[1],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
- Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
- Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
-
- // (intersection_min A emptybag) = emptyBag
- Node n1 = d_nodeManager->mkNode(INTERSECTION_MIN, A, emptyBag);
+ Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
+ Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
+
+ // (bag.inter_min A (as bag.empty (Bag String)) =
+ // (as bag.empty (Bag String))
+ Node n1 = d_nodeManager->mkNode(BAG_INTER_MIN, A, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_node == emptyBag
&& response1.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min emptybag A) = emptyBag
- Node n2 = d_nodeManager->mkNode(INTERSECTION_MIN, emptyBag, A);
+ // (bag.inter_min (as bag.empty (Bag String)) A) =
+ // (as bag.empty (Bag String))
+ Node n2 = d_nodeManager->mkNode(BAG_INTER_MIN, emptyBag, A);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
ASSERT_TRUE(response2.d_node == emptyBag
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min A A) = A
- Node n3 = d_nodeManager->mkNode(INTERSECTION_MIN, A, A);
+ // (bag.inter_min A A) = A
+ Node n3 = d_nodeManager->mkNode(BAG_INTER_MIN, A, A);
RewriteResponse response3 = d_rewriter->postRewrite(n3);
ASSERT_TRUE(response3.d_node == A
&& response3.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min A (union_max A B) = A
- Node n4 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxAB);
+ // (bag.inter_min A (bag.union_max A B) = A
+ Node n4 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxAB);
RewriteResponse response4 = d_rewriter->postRewrite(n4);
ASSERT_TRUE(response4.d_node == A
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min A (union_max B A) = A
- Node n5 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionMaxBA);
+ // (bag.inter_min A (bag.union_max B A) = A
+ Node n5 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionMaxBA);
RewriteResponse response5 = d_rewriter->postRewrite(n5);
ASSERT_TRUE(response5.d_node == A
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min (union_max A B) A) = A
- Node n6 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxAB, A);
+ // (bag.inter_min (bag.union_max A B) A) = A
+ Node n6 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxAB, A);
RewriteResponse response6 = d_rewriter->postRewrite(n6);
ASSERT_TRUE(response6.d_node == A
&& response6.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min (union_max B A) A) = A
- Node n7 = d_nodeManager->mkNode(INTERSECTION_MIN, unionMaxBA, A);
+ // (bag.inter_min (bag.union_max B A) A) = A
+ Node n7 = d_nodeManager->mkNode(BAG_INTER_MIN, unionMaxBA, A);
RewriteResponse response7 = d_rewriter->postRewrite(n7);
ASSERT_TRUE(response7.d_node == A
&& response7.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min A (union_disjoint A B) = A
- Node n8 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointAB);
+ // (bag.inter_min A (bag.union_disjoint A B) = A
+ Node n8 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointAB);
RewriteResponse response8 = d_rewriter->postRewrite(n8);
ASSERT_TRUE(response8.d_node == A
&& response8.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min A (union_disjoint B A) = A
- Node n9 = d_nodeManager->mkNode(INTERSECTION_MIN, A, unionDisjointBA);
+ // (bag.inter_min A (bag.union_disjoint B A) = A
+ Node n9 = d_nodeManager->mkNode(BAG_INTER_MIN, A, unionDisjointBA);
RewriteResponse response9 = d_rewriter->postRewrite(n9);
ASSERT_TRUE(response9.d_node == A
&& response9.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min (union_disjoint A B) A) = A
- Node n10 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointAB, A);
+ // (bag.inter_min (bag.union_disjoint A B) A) = A
+ Node n10 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointAB, A);
RewriteResponse response10 = d_rewriter->postRewrite(n10);
ASSERT_TRUE(response10.d_node == A
&& response10.d_status == REWRITE_AGAIN_FULL);
- // (intersection_min (union_disjoint B A) A) = A
- Node n11 = d_nodeManager->mkNode(INTERSECTION_MIN, unionDisjointBA, A);
+ // (bag.inter_min (bag.union_disjoint B A) A) = A
+ Node n11 = d_nodeManager->mkNode(BAG_INTER_MIN, unionDisjointBA, A);
RewriteResponse response11 = d_rewriter->postRewrite(n11);
ASSERT_TRUE(response11.d_node == A
&& response11.d_status == REWRITE_AGAIN_FULL);
d_nodeManager->stringType(),
elements[1],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
- Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
- Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
- Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
- Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
-
- // (difference_subtract A emptybag) = A
- Node n1 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, emptyBag);
+ Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
+ Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
+ Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B);
+ Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A);
+
+ // (bag.difference_subtract A (as bag.empty (Bag String)) = A
+ Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_node == A
&& response1.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract emptybag A) = emptyBag
- Node n2 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, emptyBag, A);
+ // (bag.difference_subtract (as bag.empty (Bag String)) A) =
+ // (as bag.empty (Bag String))
+ Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, emptyBag, A);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
ASSERT_TRUE(response2.d_node == emptyBag
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract A A) = emptybag
- Node n3 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, A);
+ // (bag.difference_subtract A A) = (as bag.empty (Bag String))
+ Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, A);
RewriteResponse response3 = d_rewriter->postRewrite(n3);
ASSERT_TRUE(response3.d_node == emptyBag
&& response3.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract (union_disjoint A B) A) = B
- Node n4 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointAB, A);
+ // (bag.difference_subtract (bag.union_disjoint A B) A) = B
+ Node n4 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointAB, A);
RewriteResponse response4 = d_rewriter->postRewrite(n4);
ASSERT_TRUE(response4.d_node == B
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract (union_disjoint B A) A) = B
- Node n5 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, unionDisjointBA, A);
+ // (bag.difference_subtract (bag.union_disjoint B A) A) = B
+ Node n5 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, unionDisjointBA, A);
RewriteResponse response5 = d_rewriter->postRewrite(n5);
ASSERT_TRUE(response5.d_node == B
&& response4.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract A (union_disjoint A B)) = emptybag
- Node n6 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointAB);
+ // (bag.difference_subtract A (bag.union_disjoint A B)) =
+ // (as bag.empty (Bag String))
+ Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointAB);
RewriteResponse response6 = d_rewriter->postRewrite(n6);
ASSERT_TRUE(response6.d_node == emptyBag
&& response6.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract A (union_disjoint B A)) = emptybag
- Node n7 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionDisjointBA);
+ // (bag.difference_subtract A (bag.union_disjoint B A)) =
+ // (as bag.empty (Bag String))
+ Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionDisjointBA);
RewriteResponse response7 = d_rewriter->postRewrite(n7);
ASSERT_TRUE(response7.d_node == emptyBag
&& response7.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract A (union_max A B)) = emptybag
- Node n8 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxAB);
+ // (bag.difference_subtract A (bag.union_max A B)) =
+ // (as bag.empty (Bag String))
+ Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxAB);
RewriteResponse response8 = d_rewriter->postRewrite(n8);
ASSERT_TRUE(response8.d_node == emptyBag
&& response8.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract A (union_max B A)) = emptybag
- Node n9 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, A, unionMaxBA);
+ // (bag.difference_subtract A (bag.union_max B A)) =
+ // (as bag.empty (Bag String))
+ Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, A, unionMaxBA);
RewriteResponse response9 = d_rewriter->postRewrite(n9);
ASSERT_TRUE(response9.d_node == emptyBag
&& response9.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract (intersection_min A B) A) = emptybag
- Node n10 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionAB, A);
+ // (bag.difference_subtract (bag.inter_min A B) A) =
+ // (as bag.empty (Bag String))
+ Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionAB, A);
RewriteResponse response10 = d_rewriter->postRewrite(n10);
ASSERT_TRUE(response10.d_node == emptyBag
&& response10.d_status == REWRITE_AGAIN_FULL);
- // (difference_subtract (intersection_min B A) A) = emptybag
- Node n11 = d_nodeManager->mkNode(DIFFERENCE_SUBTRACT, intersectionBA, A);
+ // (bag.difference_subtract (bag.inter_min B A) A) =
+ // (as bag.empty (Bag String))
+ Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_SUBTRACT, intersectionBA, A);
RewriteResponse response11 = d_rewriter->postRewrite(n11);
ASSERT_TRUE(response11.d_node == emptyBag
&& response11.d_status == REWRITE_AGAIN_FULL);
d_nodeManager->stringType(),
elements[1],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
- Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
- Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
- Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
- Node intersectionAB = d_nodeManager->mkNode(INTERSECTION_MIN, A, B);
- Node intersectionBA = d_nodeManager->mkNode(INTERSECTION_MIN, B, A);
-
- // (difference_remove A emptybag) = A
- Node n1 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, emptyBag);
+ Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
+ Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
+ Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
+ Node intersectionAB = d_nodeManager->mkNode(BAG_INTER_MIN, A, B);
+ Node intersectionBA = d_nodeManager->mkNode(BAG_INTER_MIN, B, A);
+
+ // (bag.difference_remove A (as bag.empty (Bag String)) = A
+ Node n1 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, emptyBag);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_node == A
&& response1.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove emptybag A) = emptyBag
- Node n2 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, emptyBag, A);
+ // (bag.difference_remove (as bag.empty (Bag String)) A)=
+ // (as bag.empty (Bag String))
+ Node n2 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, emptyBag, A);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
ASSERT_TRUE(response2.d_node == emptyBag
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove A A) = emptybag
- Node n3 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, A);
+ // (bag.difference_remove A A) = (as bag.empty (Bag String))
+ Node n3 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, A);
RewriteResponse response3 = d_rewriter->postRewrite(n3);
ASSERT_TRUE(response3.d_node == emptyBag
&& response3.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove A (union_disjoint A B)) = emptybag
- Node n6 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointAB);
+ // (bag.difference_remove A (bag.union_disjoint A B)) =
+ // (as bag.empty (Bag String))
+ Node n6 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointAB);
RewriteResponse response6 = d_rewriter->postRewrite(n6);
ASSERT_TRUE(response6.d_node == emptyBag
&& response6.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove A (union_disjoint B A)) = emptybag
- Node n7 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionDisjointBA);
+ // (bag.difference_remove A (bag.union_disjoint B A)) =
+ // (as bag.empty (Bag String))
+ Node n7 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionDisjointBA);
RewriteResponse response7 = d_rewriter->postRewrite(n7);
ASSERT_TRUE(response7.d_node == emptyBag
&& response7.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove A (union_max A B)) = emptybag
- Node n8 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxAB);
+ // (bag.difference_remove A (bag.union_max A B)) =
+ // (as bag.empty (Bag String))
+ Node n8 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxAB);
RewriteResponse response8 = d_rewriter->postRewrite(n8);
ASSERT_TRUE(response8.d_node == emptyBag
&& response8.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove A (union_max B A)) = emptybag
- Node n9 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, A, unionMaxBA);
+ // (bag.difference_remove A (bag.union_max B A)) =
+ // (as bag.empty (Bag String))
+ Node n9 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, A, unionMaxBA);
RewriteResponse response9 = d_rewriter->postRewrite(n9);
ASSERT_TRUE(response9.d_node == emptyBag
&& response9.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove (intersection_min A B) A) = emptybag
- Node n10 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionAB, A);
+ // (bag.difference_remove (bag.inter_min A B) A) =
+ // (as bag.empty (Bag String))
+ Node n10 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionAB, A);
RewriteResponse response10 = d_rewriter->postRewrite(n10);
ASSERT_TRUE(response10.d_node == emptyBag
&& response10.d_status == REWRITE_AGAIN_FULL);
- // (difference_remove (intersection_min B A) A) = emptybag
- Node n11 = d_nodeManager->mkNode(DIFFERENCE_REMOVE, intersectionBA, A);
+ // (bag.difference_remove (bag.inter_min B A) A) =
+ // (as bag.empty (Bag String))
+ Node n11 = d_nodeManager->mkNode(BAG_DIFFERENCE_REMOVE, intersectionBA, A);
RewriteResponse response11 = d_rewriter->postRewrite(n11);
ASSERT_TRUE(response11.d_node == emptyBag
&& response11.d_status == REWRITE_AGAIN_FULL);
Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
- // (bag.choose (mkBag x c)) = x where c is a constant > 0
+ // (bag.choose (bag x c)) = x where c is a constant > 0
Node n1 = d_nodeManager->mkNode(BAG_CHOOSE, bag);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_node == x
d_nodeManager->mkBag(d_nodeManager->stringType(),
elements[1],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
- // TODO(projects#223): enable this test after implementing bags normal form
- // // (bag.card emptybag) = 0
- // Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag);
- // RewriteResponse response1 = d_rewriter->postRewrite(n1);
- // ASSERT_TRUE(response1.d_node == zero && response1.d_status ==
- // REWRITE_AGAIN_FULL);
+ // (bag.card (as bag.empty (Bag String)) = 0
+ Node n1 = d_nodeManager->mkNode(BAG_CARD, emptyBag);
+ RewriteResponse response1 = d_rewriter->postRewrite(n1);
+ ASSERT_TRUE(response1.d_node == zero
+ && response1.d_status == REWRITE_AGAIN_FULL);
- // (bag.card (mkBag x c)) = c where c is a constant > 0
+ // (bag.card (bag x c)) = c where c is a constant > 0
Node n2 = d_nodeManager->mkNode(BAG_CARD, bag);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
ASSERT_TRUE(response2.d_node == c
&& response2.d_status == REWRITE_AGAIN_FULL);
- // (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B))
+ // (bag.card (bag.union_disjoint A B)) = (+ (bag.card A) (bag.card B))
Node n3 = d_nodeManager->mkNode(BAG_CARD, unionDisjointAB);
Node cardA = d_nodeManager->mkNode(BAG_CARD, A);
Node cardB = d_nodeManager->mkNode(BAG_CARD, B);
Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
- // TODO(projects#223): complete this function
- // (bag.is_singleton emptybag) = false
- // Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag);
- // RewriteResponse response1 = d_rewriter->postRewrite(n1);
- // ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false)
- // && response1.d_status == REWRITE_AGAIN_FULL);
+ // (bag.is_singleton (as bag.empty (Bag String)) = false
+ Node n1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, emptybag);
+ RewriteResponse response1 = d_rewriter->postRewrite(n1);
+ ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false)
+ && response1.d_status == REWRITE_AGAIN_FULL);
- // (bag.is_singleton (mkBag x c) = (c == 1)
+ // (bag.is_singleton (bag x c) = (c == 1)
Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
- // (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
+ // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1)
Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
RewriteResponse response = d_rewriter->postRewrite(n);
Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
x,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
- // (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
+ // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x)
Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
RewriteResponse response = d_rewriter->postRewrite(n);
Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
Node bound = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, xString);
Node lambda = d_nodeManager->mkNode(LAMBDA, bound, empty);
- // (bag.map (lambda ((x U)) t) emptybag) = emptybag
+ // (bag.map (lambda ((x U)) t) (as bag.empty (Bag String)) =
+ // (as bag.empty (Bag String))
Node n1 = d_nodeManager->mkNode(BAG_MAP, lambda, emptybagString);
RewriteResponse response1 = d_rewriter->postRewrite(n1);
ASSERT_TRUE(response1.d_node == emptybagString
d_nodeManager->mkBag(d_nodeManager->stringType(),
b,
d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
- Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
+ Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
ASSERT_TRUE(unionDisjointAB.isConst());
- // (bag.map (lambda ((x Int)) "") (union_disjoint (bag "a" 3) (bag "b" 4))) =
- // (bag "" 7))
+ // (bag.map
+ // (lambda ((x Int)) "")
+ // (bag.union_disjoint (bag "a" 3) (bag "b" 4))) =
+ // (bag "" 7))
Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
-
Node rewritten = Rewriter::rewrite(n2);
Node bag =
d_nodeManager->mkBag(d_nodeManager->stringType(),
d_nodeManager->stringType(),
elements[0],
d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
- ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag));
- ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(),
+ ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag));
+ ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(),
bag.getType());
}
d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
// only positive multiplicity are constants
- ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative));
- ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero));
- ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive));
+ ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative));
+ ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, zero));
+ ASSERT_TRUE(BagMakeTypeRule::computeIsConst(d_nodeManager, positive));
}
TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)
projects / cvc5.git / commitdiff