projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 129f72e) | patch
Add set.filter operator and its inference rules (#8856)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Tue, 7 Jun 2022 18:37:07 +0000 (13:37 -0500)
committerGitHub <noreply@github.com>
Tue, 7 Jun 2022 18:37:07 +0000 (18:37 +0000)
commita928211cee1c0e1e0cf46f28e65854c0cee94ca5
tree83f909284ab27c49d605c94f968af4ba350a4cc6tree
parent129f72e42965992e208dba89cebd5582a9ee04f3commit | diff
Add set.filter operator and its inference rules (#8856)
26 files changed:
proofs/lfsc/signatures/theory_def.plf diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bags/bag_solver.cpp diff | blob | history
src/theory/bags/inference_generator.cpp diff | blob | history
src/theory/bags/inference_generator.h diff | blob | history
src/theory/bags/kinds diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/sets/kinds diff | blob | history
src/theory/sets/solver_state.cpp diff | blob | history
src/theory/sets/solver_state.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
src/theory/sets/theory_sets_rewriter.cpp diff | blob | history
src/theory/sets/theory_sets_rewriter.h diff | blob | history
src/theory/sets/theory_sets_type_rules.cpp diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/bags/filter3.smt2 diff | blob | history
test/regress/cli/regress1/sets/set_filter1.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/set_filter2.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/set_filter3.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/set_filter4.smt2 [new file with mode: 0644] blob