projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d598a96) | patch
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 10 Jul 2017 19:06:52 +0000 (14:06 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 10 Jul 2017 19:07:11 +0000 (14:07 -0500)
commitf3590092818d9eab9d961ea602093029ff472a85
tree1401f00df0d9659ba2321ea2088fe0c3f4de9f52tree
parentd598a9644862d176632071bca8448765d9cc3cc1commit | diff
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
68 files changed:
src/Makefile.am diff | blob | history
src/compat/cvc3_compat.cpp diff | blob | history
src/expr/datatype.cpp diff | blob | history
src/expr/datatype.h diff | blob | history
src/expr/node.cpp diff | blob | history
src/main/command_executor_portfolio.cpp diff | blob | history
src/options/Makefile.am diff | blob | history
src/options/datatypes_modes.h [new file with mode: 0644] blob
src/options/datatypes_options diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/options/options_handler.h diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/options/quantifiers_options diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.h diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/ce_guided_pbe.cpp [new file with mode: 0644] blob
src/theory/quantifiers/ce_guided_pbe.h [new file with mode: 0644] blob
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/sets/rels_utils.h diff | blob | history
test/regress/regress0/sygus/General_plus10.sy [new file with mode: 0755] blob
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/cggmp.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/fg_polynomial3.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/icfp_14.12.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/icfp_easy-ite.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/qe.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/strings-template-infer.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/strings-trivial-simp.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/strings-trivial.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/tl-type-0.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/tl-type-4x.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/Makefile.am diff | blob | history
test/regress/regress1/sygus/VC22_a.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/array_sum_dd.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/icfp_easy_mt_ite.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/inv_gen_fig8.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/inv_gen_n_c11.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/mpg_guard1-dd.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/three.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy [new file with mode: 0644] blob