projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 31ab3e2) | patch
refactored the code
authorPaulMeng <baolmeng@gmail.com>
Fri, 4 Mar 2016 17:27:02 +0000 (11:27 -0600)
committerPaulMeng <baolmeng@gmail.com>
Fri, 4 Mar 2016 17:27:02 +0000 (11:27 -0600)
commit0231618679e6f2e4ae6247015fc5eb0f2f35f9fe
treefc410a58c66151968e6c52658d581525c6f7d731tree
parent31ab3e21f285b0b6a3a8de7ab352c0c6276b6695commit | diff
refactored the code

- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas
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_type_rules.h diff | blob | history
test/regress/regress0/sets/rels/rel_join_0_1.cvc diff | blob | history
test/regress/regress0/sets/rels/rel_symbolic_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_1.cvc diff | blob | history
test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_int.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/rels/rel_tp_join_var.cvc diff | blob | history