projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 55d024a) | patch
Add rel.group operator to sets (#8876)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Tue, 28 Jun 2022 17:50:41 +0000 (12:50 -0500)
committerGitHub <noreply@github.com>
Tue, 28 Jun 2022 17:50:41 +0000 (17:50 +0000)
commit61026f8e494a460906fd6d37dc0766608cce7aee
treee88eda6a2d0ce9fdc7111cc67d006914df8e132atree
parent55d024accae4abf992c9585961bd0765d9eef2abcommit | diff
Add rel.group operator to sets (#8876)

This PR is dependent on #8819 and #8867.
28 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/bags/bags_utils.cpp diff | blob | history
src/theory/bags/bags_utils.h 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/rels_utils.cpp diff | blob | history
src/theory/sets/rels_utils.h 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/sets/relation_group1.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/relation_group2.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/relation_group3.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/relation_group4.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/sets/relation_group5.smt2 [new file with mode: 0644] blob