projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9f5a29e) | patch
Added more benchmarks
authorPaulMeng <baolmeng@gmail.com>
Mon, 29 Feb 2016 17:10:01 +0000 (11:10 -0600)
committerPaulMeng <baolmeng@gmail.com>
Mon, 29 Feb 2016 17:10:01 +0000 (11:10 -0600)
commit06f09df136eaf824a7cefe2e4a88f010ae6495d7
tree50e2a3db55d5188f3b8827f9dd39be31b055d127tree
parent9f5a29e3ec43821c37f8557f9215cb52a80c1b0bcommit | diff
Added more benchmarks
Fixed the problem that duplicates and split facts were sent as lemmas
causing nontermination
Fixed the computation of join and product relations without simplication
20 files changed:
src/theory/sets/theory_sets_rels.cpp diff | blob | history
src/theory/sets/theory_sets_rels.h diff | blob | history
test/regress/regress0/sets/rels/rel_join_3.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_join_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_join_4.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_join_5.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_product_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_product_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_product_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_product_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_2.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_3.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_var.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_transpose_2.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_transpose_3.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_transpose_4.cvc [new file with mode: 0644] blob