Add bag.member operator to theory of bags (#7857)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Tue, 4 Jan 2022 16:49:00 +0000 (10:49 -0600)
committerGitHub <noreply@github.com>
Tue, 4 Jan 2022 16:49:00 +0000 (16:49 +0000)
commit70f007e3fbf76d47aa52b71a10f24a189311c945
tree9766b1ad311ed086116e76aec937181b4ebebf03
parentb22a7df42d9591625e9f43ea737c9fbc1658cb2a
Add bag.member operator to theory of bags (#7857)

This PR adds the predicate bag.member to be analogous to predicate set.member.
The PR is motivated by converting regressions for sets to bags, which avoids defining a predicate for each set type

(define-fun bag.member ((e E) (B (Bag E))) Bool (>= (bag.count e B) 1))
13 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5_kind.h
src/parser/smt2/smt2.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/bags/bags_rewriter.cpp
src/theory/bags/bags_rewriter.h
src/theory/bags/kinds
src/theory/bags/rewrites.cpp
src/theory/bags/rewrites.h
src/theory/bags/theory_bags_type_rules.cpp
src/theory/bags/theory_bags_type_rules.h
test/regress/CMakeLists.txt
test/regress/regress1/bags/bag_member.smt2 [new file with mode: 0644]