git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 5 Dec 2019 15:19:56 +0000 (09:19 -0600)
committer	GitHub <noreply@github.com>
	Thu, 5 Dec 2019 15:19:56 +0000 (09:19 -0600)
commit	f17b72fcdb535a5c06620900d2c35d2709abe968
tree	408a48f718858c3623afbe1d8b99cab79cedaf35	tree
parent	97c2553d0b0535bd47517f755897c441e223568e	commit \| diff

Refactor mode options for Unif+PI (#3531)

19 files changed:

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.toml		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
test/regress/regress0/sygus/let-ringer.sy		diff \| blob \| history
test/regress/regress1/quantifiers/horn-simple.smt2		diff \| blob \| history
test/regress/regress1/sygus/car_3.lus.sy		diff \| blob \| history
test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy		diff \| blob \| history
test/regress/regress1/sygus/cegisunif-depth1.sy		diff \| blob \| history
test/regress/regress1/sygus/constant-dec-tree-bug.sy		diff \| blob \| history
test/regress/regress1/sygus/planning-unif.sy		diff \| blob \| history
test/regress/regress2/sygus/cegisunif-depth1-bv.sy		diff \| blob \| history