Add set.aggr operator to sets (#8878)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 30 Jun 2022 02:03:36 +0000 (21:03 -0500)
committerGitHub <noreply@github.com>
Thu, 30 Jun 2022 02:03:36 +0000 (02:03 +0000)
commit9e20f45b9dcbc3bb2b0ddfd96337454a3221baf2
treec234a6f8c0b5dc70c6ce12abd5fd750497270392
parentca2a39f7650fb311d5a45b5a95861605ad5a80af
Add  set.aggr operator to sets (#8878)

This PR depends on #8876
17 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5_kind.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/sets/kinds
src/theory/sets/rels_utils.cpp
src/theory/sets/rels_utils.h
src/theory/sets/set_reduction.cpp
src/theory/sets/set_reduction.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_rewriter.h
src/theory/sets/theory_sets_type_rules.cpp
src/theory/sets/theory_sets_type_rules.h
test/regress/cli/CMakeLists.txt
test/regress/cli/regress1/sets/relation_aggregate1.smt2 [new file with mode: 0644]