projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b9edba7) | patch
make skolems and tuple reduction terms as shared terms
authorPaulMeng <baolmeng@gmail.com>
Wed, 9 Mar 2016 01:26:13 +0000 (19:26 -0600)
committerPaulMeng <baolmeng@gmail.com>
Wed, 9 Mar 2016 01:26:13 +0000 (19:26 -0600)
commit7d9fe09b55eb7b9cf319594f163d1b57fc78c272
tree0ef2d01db17024dad23ed26005ba7871fa290755tree
parentb9edba75ed506427502c9d565152794669e3ae23commit | diff
make skolems and tuple reduction terms as shared terms

- added more benchmarks for pressure and theory combination tests
- fixed find terms method in trie data structure
- use a separate membership map to store positive membership terms
src/theory/sets/theory_sets_rels.cpp diff | blob | history
src/theory/sets/theory_sets_rels.h diff | blob | history
src/theory/sets/theory_sets_rewriter.cpp diff | blob | history
test/regress/regress0/sets/rels/rel_1tup_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_complex_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_complex_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_mix_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_pressure_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_transpose_5.cvc [new file with mode: 0644] blob