Add set.fold operator (#8867)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Thu, 23 Jun 2022 14:18:41 +0000 (09:18 -0500)
committerGitHub <noreply@github.com>
Thu, 23 Jun 2022 14:18:41 +0000 (14:18 +0000)
commit84356320cd9f0127d23d050d0db886cd81363981
tree68068666ccbb8a11481bf6df351d85db9bef4237
parentce382efe5b7f2c31d1a4d13d06c9d9e2de270290
Add set.fold operator (#8867)
23 files changed:
proofs/lfsc/signatures/theory_def.plf
src/CMakeLists.txt
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5_kind.h
src/expr/skolem_manager.cpp
src/expr/skolem_manager.h
src/parser/smt2/smt2.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/inference_id.cpp
src/theory/inference_id.h
src/theory/sets/kinds
src/theory/sets/set_reduction.cpp [new file with mode: 0644]
src/theory/sets/set_reduction.h [new file with mode: 0644]
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets_private.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/set_fold1.smt2 [new file with mode: 0644]
test/regress/cli/regress1/sets/set_fold2.smt2 [new file with mode: 0644]
test/regress/cli/regress1/sets/set_fold3.smt2 [new file with mode: 0644]