projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e79e643) | patch
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extensi...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 26 Oct 2016 21:23:58 +0000 (16:23 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 26 Oct 2016 21:23:58 +0000 (16:23 -0500)
commit031722bee8682005bd4c8700ef78b5f893fc48fe
tree46a936a1bd20ea2cc588df0d3205cf7eb0fd4177tree
parente79e64329ce7d6df0003cab28dadb9b8bcc6f9cacommit | diff
New implementation of sets+cardinality.  Merge Paul Meng's relation solver as extension of sets solver, add regressions.
106 files changed:
src/Makefile.am diff | blob | history
src/options/sets_options diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/sets/card_unused_implementation.cpp [deleted file] blob | history
src/theory/sets/expr_patterns.h [deleted file] blob | history
src/theory/sets/kinds diff | blob | history
src/theory/sets/normal_form.h diff | blob | history
src/theory/sets/rels_utils.h [new file with mode: 0644] blob
src/theory/sets/scrutinize.h [deleted file] blob | history
src/theory/sets/term_info.h [deleted file] blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets.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_rels.cpp [new file with mode: 0644] blob
src/theory/sets/theory_sets_rels.h [new file with mode: 0644] blob
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.h diff | blob | history
test/Makefile.am diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/rels/Makefile [new file with mode: 0644] blob
test/regress/regress0/rels/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/rels/addr_book_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/addr_book_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/addr_book_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv1-unit.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv1-unitb.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv1p-sat.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv1p.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/bv2.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/garbage_collect.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/join-eq-structure-and.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/join-eq-structure.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/join-eq-structure_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/join-eq-u-sat.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/join-eq-u.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/prod-mod-eq.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/prod-mod-eq2.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_1tup_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_complex_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_complex_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_complex_3.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_complex_4.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_complex_5.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_conflict_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_2.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_3.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_4.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_5.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_6.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_join_7.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_mix_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_pressure_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_product_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_product_0_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_product_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_product_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_symbolic_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_symbolic_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_symbolic_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_symbolic_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_10_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_11.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_3.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_4.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_4_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_5_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_6.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_7.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_8.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tc_9_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_2.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_3_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_2.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_2_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_3.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_eq_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_int_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_pro_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_tp_join_var_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_0.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_1_1.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_3.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_4.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_5.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_6.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/rel_transpose_7.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/set-strat.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/strat.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/strat_0_1.cvc [new file with mode: 0644] blob