Skip to content

Commit f572e0b

Browse files
mudathirmahgoubmudathirmahgoub
authored
Rename BAG_DUPLICATE_REMOVAL to SETOF and cleanup unused bag operators (cvc5#10376)
Remove the operators is_singleton, from_set, to_set
1 parent 189a5dd commit f572e0b

31 files changed

+80
-613
lines changed

‎NEWS.md

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ This file contains a summary of important user-visible changes.
1111
deprecated and replaced by `std::to_string(Kind)` and
1212
`std::to_string(SortKind)`. They will be removed in the next minor release.
1313

14+
- Renamed `bag.duplicate_removal` to `bag.setof`.
15+
1416
cvc5 1.1.1
1517
==========
1618

‎docs/theories/bags.rst

+2-2
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ a `cvc5::Solver solver` object.
3333
+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
3434
| Difference subtract | ``(bag.difference_subtract X Y)`` | ``Term t = solver.mkTerm(Kind::BAG_DIFFERENCE_SUBTRACT, {X, Y});`` |
3535
+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
36-
| Duplicate elimination| ``(bag.duplicate_removal X)`` | ``Term t = solver.mkTerm(Kind::BAG_DUPLICATE_REMOVAL, {X});`` |
36+
| Duplicate elimination| ``(bag.setof X)`` | ``Term t = solver.mkTerm(Kind::BAG_SETOF, {X});`` |
3737
+----------------------+----------------------------------------------+-------------------------------------------------------------------------+
3838
| Membership | ``(bag.member x X)`` | ``Term x = solver.mkConst(solver.getStringSort(), "x");`` |
3939
| | | |
@@ -70,7 +70,7 @@ The semantics of supported bag operators is given in the table below.
7070
+-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
7171
| difference remove :math:`m_1 \setminus\setminus m_2`| bag.difference_remove | :math:`\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)` |
7272
+-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
73-
| duplicate elimination :math:`\delta(m)` | bag.duplicate_removal | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)` |
73+
| setof :math:`\delta(m)` | bag.setof | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)` |
7474
+-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+
7575
| subbag :math:`m_1 \subseteq m_2` | bag.subbag | :math:`\forall e. \; m_1(e) \leq m_2(e)` |
7676
+-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+

‎include/cvc5/cvc5_kind.h

+3-69
Original file line numberDiff line numberDiff line change
@@ -3812,7 +3812,7 @@ enum ENUM(Kind) : int32_t
38123812
*/
38133813
EVALUE(BAG_MEMBER),
38143814
/**
3815-
* Bag duplicate removal.
3815+
* Bag setof.
38163816
*
38173817
* Eliminate duplicates in a given bag. The returned bag contains exactly the
38183818
* same elements in the given bag, but with multiplicity one.
@@ -3835,7 +3835,7 @@ enum ENUM(Kind) : int32_t
38353835
* future versions.
38363836
* \endrst
38373837
*/
3838-
EVALUE(BAG_DUPLICATE_REMOVAL),
3838+
EVALUE(BAG_SETOF),
38393839
/**
38403840
* Bag make.
38413841
*
@@ -3908,73 +3908,7 @@ enum ENUM(Kind) : int32_t
39083908
* future versions.
39093909
* \endrst
39103910
*/
3911-
EVALUE(BAG_CHOOSE),
3912-
/**
3913-
* Bag is singleton tester.
3914-
*
3915-
* - Arity: ``1``
3916-
*
3917-
* - ``1:`` Term of bag Sort
3918-
*
3919-
* - Create Term of this Kind with:
3920-
*
3921-
* - Solver::mkTerm(Kind, const std::vector<Term>&) const
3922-
* - Solver::mkTerm(const Op&, const std::vector<Term>&) const
3923-
*
3924-
* - Create Op of this kind with:
3925-
*
3926-
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
3927-
*
3928-
* \rst
3929-
* .. warning:: This kind is experimental and may be changed or removed in
3930-
* future versions.
3931-
* \endrst
3932-
*/
3933-
EVALUE(BAG_IS_SINGLETON),
3934-
/**
3935-
* Conversion from set to bag.
3936-
*
3937-
* - Arity: ``1``
3938-
*
3939-
* - ``1:`` Term of set Sort
3940-
*
3941-
* - Create Term of this Kind with:
3942-
*
3943-
* - Solver::mkTerm(Kind, const std::vector<Term>&) const
3944-
* - Solver::mkTerm(const Op&, const std::vector<Term>&) const
3945-
*
3946-
* - Create Op of this kind with:
3947-
*
3948-
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
3949-
*
3950-
* \rst
3951-
* .. warning:: This kind is experimental and may be changed or removed in
3952-
* future versions.
3953-
* \endrst
3954-
*/
3955-
EVALUE(BAG_FROM_SET),
3956-
/**
3957-
* Conversion from bag to set.
3958-
*
3959-
* - Arity: ``1``
3960-
*
3961-
* - ``1:`` Term of bag Sort
3962-
*
3963-
* - Create Term of this Kind with:
3964-
*
3965-
* - Solver::mkTerm(Kind, const std::vector<Term>&) const
3966-
* - Solver::mkTerm(const Op&, const std::vector<Term>&) const
3967-
*
3968-
* - Create Op of this kind with:
3969-
*
3970-
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
3971-
*
3972-
* \rst
3973-
* .. warning:: This kind is experimental and may be changed or removed in
3974-
* future versions.
3975-
* \endrst
3976-
*/
3977-
EVALUE(BAG_TO_SET),
3911+
EVALUE(BAG_CHOOSE),
39783912
/**
39793913
* Bag map.
39803914
*

‎proofs/alf/cvc5/theories/Bags.smt3

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
(declare-const bag.member (-> (! Type :var T :implicit) T (Bag T) Bool))
1919
(declare-const bag.card (-> (! Type :var T :implicit) (Bag T) Int))
2020
(declare-const bag.choose (-> (! Type :var T :implicit) (Bag T) T))
21-
(declare-const bag.duplicate_removal (-> (! Type :var T :implicit) (Bag T) (Bag T)))
21+
(declare-const bag.setof (-> (! Type :var T :implicit) (Bag T) (Bag T)))
2222
(declare-const bag.is_singleton (-> (! Type :var T :implicit) (Bag T) Bool))
2323

2424
(declare-const bag.filter (-> (! Type :var T :implicit) (-> T Bool) (Bag T) (Bag T)))

‎proofs/lfsc/signatures/theory_def.plf

+2-2
Original file line numberDiff line numberDiff line change
@@ -545,8 +545,8 @@
545545
(define bag.count (# x term (# y term (apply (apply f_bag.count x) y))))
546546
(declare f_bag term)
547547
(define bag (# x term (# y term (apply (apply f_bag x) y))))
548-
(declare f_bag.duplicate_removal term)
549-
(define bag.duplicate_removal (# x term (apply f_bag.duplicate_removal x)))
548+
(declare f_bag.setof term)
549+
(define bag.setof (# x term (apply f_bag.setof x)))
550550
(declare f_bag.card term)
551551
(define bag.card (# x term (apply f_bag.card x)))
552552
(declare f_bag.choose term)

‎src/api/cpp/cvc5.cpp

+2-9
Original file line numberDiff line numberDiff line change
@@ -355,15 +355,11 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
355355
KIND_ENUM(Kind::BAG_SUBBAG, internal::Kind::BAG_SUBBAG),
356356
KIND_ENUM(Kind::BAG_COUNT, internal::Kind::BAG_COUNT),
357357
KIND_ENUM(Kind::BAG_MEMBER, internal::Kind::BAG_MEMBER),
358-
KIND_ENUM(Kind::BAG_DUPLICATE_REMOVAL,
359-
internal::Kind::BAG_DUPLICATE_REMOVAL),
358+
KIND_ENUM(Kind::BAG_SETOF, internal::Kind::BAG_SETOF),
360359
KIND_ENUM(Kind::BAG_MAKE, internal::Kind::BAG_MAKE),
361360
KIND_ENUM(Kind::BAG_EMPTY, internal::Kind::BAG_EMPTY),
362361
KIND_ENUM(Kind::BAG_CARD, internal::Kind::BAG_CARD),
363362
KIND_ENUM(Kind::BAG_CHOOSE, internal::Kind::BAG_CHOOSE),
364-
KIND_ENUM(Kind::BAG_IS_SINGLETON, internal::Kind::BAG_IS_SINGLETON),
365-
KIND_ENUM(Kind::BAG_FROM_SET, internal::Kind::BAG_FROM_SET),
366-
KIND_ENUM(Kind::BAG_TO_SET, internal::Kind::BAG_TO_SET),
367363
KIND_ENUM(Kind::BAG_MAP, internal::Kind::BAG_MAP),
368364
KIND_ENUM(Kind::BAG_FILTER, internal::Kind::BAG_FILTER),
369365
KIND_ENUM(Kind::BAG_FOLD, internal::Kind::BAG_FOLD),
@@ -752,14 +748,11 @@ const static std::unordered_map<internal::Kind,
752748
{internal::Kind::BAG_SUBBAG, Kind::BAG_SUBBAG},
753749
{internal::Kind::BAG_COUNT, Kind::BAG_COUNT},
754750
{internal::Kind::BAG_MEMBER, Kind::BAG_MEMBER},
755-
{internal::Kind::BAG_DUPLICATE_REMOVAL, Kind::BAG_DUPLICATE_REMOVAL},
751+
{internal::Kind::BAG_SETOF, Kind::BAG_SETOF},
756752
{internal::Kind::BAG_MAKE, Kind::BAG_MAKE},
757753
{internal::Kind::BAG_EMPTY, Kind::BAG_EMPTY},
758754
{internal::Kind::BAG_CARD, Kind::BAG_CARD},
759755
{internal::Kind::BAG_CHOOSE, Kind::BAG_CHOOSE},
760-
{internal::Kind::BAG_IS_SINGLETON, Kind::BAG_IS_SINGLETON},
761-
{internal::Kind::BAG_FROM_SET, Kind::BAG_FROM_SET},
762-
{internal::Kind::BAG_TO_SET, Kind::BAG_TO_SET},
763756
{internal::Kind::BAG_MAP, Kind::BAG_MAP},
764757
{internal::Kind::BAG_FILTER, Kind::BAG_FILTER},
765758
{internal::Kind::BAG_FOLD, Kind::BAG_FOLD},

‎src/parser/smt2/smt2_state.cpp

+1-4
Original file line numberDiff line numberDiff line change
@@ -898,13 +898,10 @@ void Smt2State::setLogic(std::string name)
898898
addOperator(Kind::BAG_SUBBAG, "bag.subbag");
899899
addOperator(Kind::BAG_COUNT, "bag.count");
900900
addOperator(Kind::BAG_MEMBER, "bag.member");
901-
addOperator(Kind::BAG_DUPLICATE_REMOVAL, "bag.duplicate_removal");
901+
addOperator(Kind::BAG_SETOF, "bag.setof");
902902
addOperator(Kind::BAG_MAKE, "bag");
903903
addOperator(Kind::BAG_CARD, "bag.card");
904904
addOperator(Kind::BAG_CHOOSE, "bag.choose");
905-
addOperator(Kind::BAG_IS_SINGLETON, "bag.is_singleton");
906-
addOperator(Kind::BAG_FROM_SET, "bag.from_set");
907-
addOperator(Kind::BAG_TO_SET, "bag.to_set");
908905
addOperator(Kind::BAG_MAP, "bag.map");
909906
addOperator(Kind::BAG_FILTER, "bag.filter");
910907
addOperator(Kind::BAG_FOLD, "bag.fold");

‎src/printer/smt2/smt2_printer.cpp

+1-4
Original file line numberDiff line numberDiff line change
@@ -1211,13 +1211,10 @@ std::string Smt2Printer::smtKindString(Kind k)
12111211
case Kind::BAG_SUBBAG: return "bag.subbag";
12121212
case Kind::BAG_COUNT: return "bag.count";
12131213
case Kind::BAG_MEMBER: return "bag.member";
1214-
case Kind::BAG_DUPLICATE_REMOVAL: return "bag.duplicate_removal";
1214+
case Kind::BAG_SETOF: return "bag.setof";
12151215
case Kind::BAG_MAKE: return "bag";
12161216
case Kind::BAG_CARD: return "bag.card";
12171217
case Kind::BAG_CHOOSE: return "bag.choose";
1218-
case Kind::BAG_IS_SINGLETON: return "bag.is_singleton";
1219-
case Kind::BAG_FROM_SET: return "bag.from_set";
1220-
case Kind::BAG_TO_SET: return "bag.to_set";
12211218
case Kind::BAG_MAP: return "bag.map";
12221219
case Kind::BAG_FILTER: return "bag.filter";
12231220
case Kind::BAG_FOLD: return "bag.fold";

‎src/theory/bags/bag_solver.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ void BagSolver::checkBasicOperations()
7575
case Kind::BAG_INTER_MIN: checkIntersectionMin(n); break;
7676
case Kind::BAG_DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break;
7777
case Kind::BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(n); break;
78-
case Kind::BAG_DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break;
78+
case Kind::BAG_SETOF: checkSetof(n); break;
7979
case Kind::BAG_FILTER: checkFilter(n); break;
8080
case Kind::TABLE_PRODUCT: checkProduct(n); break;
8181
case Kind::TABLE_JOIN: checkJoin(n); break;
@@ -258,9 +258,9 @@ void BagSolver::checkDifferenceRemove(const Node& n)
258258
}
259259
}
260260

261-
void BagSolver::checkDuplicateRemoval(Node n)
261+
void BagSolver::checkSetof(Node n)
262262
{
263-
Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL);
263+
Assert(n.getKind() == Kind::BAG_SETOF);
264264
set<Node> elements;
265265
const set<Node>& downwards = d_state.getElements(n);
266266
const set<Node>& upwards = d_state.getElements(n[0]);
@@ -270,7 +270,7 @@ void BagSolver::checkDuplicateRemoval(Node n)
270270

271271
for (const Node& e : elements)
272272
{
273-
InferInfo i = d_ig.duplicateRemoval(n, d_state.getRepresentative(e));
273+
InferInfo i = d_ig.setof(n, d_state.getRepresentative(e));
274274
d_im.lemmaTheoryInference(&i);
275275
}
276276
}

‎src/theory/bags/bag_solver.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class BagSolver : protected EnvObj
4343
/**
4444
* apply inference rules for basic bag operators without quantifiers:
4545
* BAG_MAKE, BAG_UNION_DISJOINT, BAG_UNION_MAX, BAG_INTER_MIN,
46-
* BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_REMOVE, BAG_DUPLICATE_REMOVAL
46+
* BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_REMOVE, BAG_SETOF
4747
*/
4848
void checkBasicOperations();
4949

@@ -95,7 +95,7 @@ class BagSolver : protected EnvObj
9595
/** apply inference rules for difference remove */
9696
void checkDifferenceRemove(const Node& n);
9797
/** apply inference rules for duplicate removal operator */
98-
void checkDuplicateRemoval(Node n);
98+
void checkSetof(Node n);
9999
/** apply non negative constraints for multiplicities */
100100
void checkNonNegativeCountTerms(const Node& bag, const Node& element);
101101
/** apply inference rules for disequal bag terms */

‎src/theory/bags/bags_rewriter.cpp

+5-48
Original file line numberDiff line numberDiff line change
@@ -78,9 +78,7 @@ RewriteResponse BagsRewriter::postRewrite(TNode n)
7878
{
7979
case Kind::BAG_MAKE: response = rewriteMakeBag(n); break;
8080
case Kind::BAG_COUNT: response = rewriteBagCount(n); break;
81-
case Kind::BAG_DUPLICATE_REMOVAL:
82-
response = rewriteDuplicateRemoval(n);
83-
break;
81+
case Kind::BAG_SETOF: response = rewriteSetof(n); break;
8482
case Kind::BAG_UNION_MAX: response = rewriteUnionMax(n); break;
8583
case Kind::BAG_UNION_DISJOINT: response = rewriteUnionDisjoint(n); break;
8684
case Kind::BAG_INTER_MIN: response = rewriteIntersectionMin(n); break;
@@ -91,9 +89,6 @@ RewriteResponse BagsRewriter::postRewrite(TNode n)
9189
response = rewriteDifferenceRemove(n);
9290
break;
9391
case Kind::BAG_CARD: response = rewriteCard(n); break;
94-
case Kind::BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break;
95-
case Kind::BAG_FROM_SET: response = rewriteFromSet(n); break;
96-
case Kind::BAG_TO_SET: response = rewriteToSet(n); break;
9792
case Kind::BAG_MAP: response = postRewriteMap(n); break;
9893
case Kind::BAG_FILTER: response = postRewriteFilter(n); break;
9994
case Kind::BAG_FOLD: response = postRewriteFold(n); break;
@@ -207,16 +202,16 @@ BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const
207202
return BagsRewriteResponse(n, Rewrite::NONE);
208203
}
209204

210-
BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const
205+
BagsRewriteResponse BagsRewriter::rewriteSetof(const TNode& n) const
211206
{
212-
Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL);
207+
Assert(n.getKind() == Kind::BAG_SETOF);
213208
if (n[0].getKind() == Kind::BAG_MAKE && n[0][1].isConst()
214209
&& n[0][1].getConst<Rational>().sgn() == 1)
215210
{
216-
// (bag.duplicate_removal (bag x n)) = (bag x 1)
211+
// (bag.setof (bag x n)) = (bag x 1)
217212
// where n is a positive constant
218213
Node bag = d_nm->mkNode(Kind::BAG_MAKE, n[0][0], d_one);
219-
return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE);
214+
return BagsRewriteResponse(bag, Rewrite::SETOF_BAG_MAKE);
220215
}
221216
return BagsRewriteResponse(n, Rewrite::NONE);
222217
}
@@ -472,44 +467,6 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const
472467
return BagsRewriteResponse(n, Rewrite::NONE);
473468
}
474469

475-
BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const
476-
{
477-
Assert(n.getKind() == Kind::BAG_IS_SINGLETON);
478-
if (n[0].getKind() == Kind::BAG_MAKE)
479-
{
480-
// (bag.is_singleton (bag x c)) = (c == 1)
481-
Node equal = n[0][1].eqNode(d_one);
482-
return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_BAG_MAKE);
483-
}
484-
return BagsRewriteResponse(n, Rewrite::NONE);
485-
}
486-
487-
BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const
488-
{
489-
Assert(n.getKind() == Kind::BAG_FROM_SET);
490-
if (n[0].getKind() == Kind::SET_SINGLETON)
491-
{
492-
// (bag.from_set (set.singleton x)) = (bag x 1)
493-
Node bag = d_nm->mkNode(Kind::BAG_MAKE, n[0][0], d_one);
494-
return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON);
495-
}
496-
return BagsRewriteResponse(n, Rewrite::NONE);
497-
}
498-
499-
BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const
500-
{
501-
Assert(n.getKind() == Kind::BAG_TO_SET);
502-
if (n[0].getKind() == Kind::BAG_MAKE && n[0][1].isConst()
503-
&& n[0][1].getConst<Rational>().sgn() == 1)
504-
{
505-
// (bag.to_set (bag x n)) = (set.singleton x)
506-
// where n is a positive constant and T is the type of the bag's elements
507-
Node set = d_nm->mkNode(Kind::SET_SINGLETON, n[0][0]);
508-
return BagsRewriteResponse(set, Rewrite::TO_SINGLETON);
509-
}
510-
return BagsRewriteResponse(n, Rewrite::NONE);
511-
}
512-
513470
BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const
514471
{
515472
Assert(n.getKind() == Kind::EQUAL);

‎src/theory/bags/bags_rewriter.h

+2-21
Original file line numberDiff line numberDiff line change
@@ -95,10 +95,10 @@ class BagsRewriter : public TheoryRewriter
9595

9696
/**
9797
* rewrites for n include:
98-
* - (bag.duplicate_removal (bag x n)) = (bag x 1)
98+
* - (bag.setof (bag x n)) = (bag x 1)
9999
* where n is a positive constant
100100
*/
101-
BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const;
101+
BagsRewriteResponse rewriteSetof(const TNode& n) const;
102102

103103
/**
104104
* rewrites for n include:
@@ -190,25 +190,6 @@ class BagsRewriter : public TheoryRewriter
190190
*/
191191
BagsRewriteResponse rewriteCard(const TNode& n) const;
192192

193-
/**
194-
* rewrites for n include:
195-
* - (bag.is_singleton (bag x c)) = (c == 1)
196-
*/
197-
BagsRewriteResponse rewriteIsSingleton(const TNode& n) const;
198-
199-
/**
200-
* rewrites for n include:
201-
* - (bag.from_set (set.singleton x)) = (bag x 1)
202-
*/
203-
BagsRewriteResponse rewriteFromSet(const TNode& n) const;
204-
205-
/**
206-
* rewrites for n include:
207-
* - (bag.to_set (bag x n)) = (set.singleton x)
208-
* where n is a positive constant and T is the type of the bag's elements
209-
*/
210-
BagsRewriteResponse rewriteToSet(const TNode& n) const;
211-
212193
/**
213194
* rewrites for n include:
214195
* - (= A A) = true

0 commit comments

Comments
 (0)