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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Wed, 18 May 2016 15:06:49 +0000 (10:06 -0500)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Wed, 18 May 2016 15:06:49 +0000 (10:06 -0500)
commit	2e02c1c2fb999f2f1cdefe867f843c2c46ad0ef0
tree	e9234dd807818316a9029cab5badc62b6874fa67	tree
parent	8768c1079798599bbe27b29bc49087d45857a112	commit \| diff

Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes for inst max level.

44 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		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
test/regress/regress0/sygus/array_search_2.sy		diff \| blob \| history
test/regress/regress0/sygus/array_sum_2_5.sy		diff \| blob \| history
test/regress/regress0/sygus/clock-inc-tuple.sy		diff \| blob \| history
test/regress/regress0/sygus/commutative.sy		diff \| blob \| history
test/regress/regress0/sygus/const-var-test.sy		diff \| blob \| history
test/regress/regress0/sygus/constant.sy		diff \| blob \| history
test/regress/regress0/sygus/dt-no-syntax.sy		diff \| blob \| history
test/regress/regress0/sygus/dt-test-ns.sy		diff \| blob \| history
test/regress/regress0/sygus/dup-op.sy		diff \| blob \| history
test/regress/regress0/sygus/enum-test.sy		diff \| blob \| history
test/regress/regress0/sygus/hd-sdiv.sy		diff \| blob \| history
test/regress/regress0/sygus/icfp_28_10.sy		diff \| blob \| history
test/regress/regress0/sygus/inv-example.sy		diff \| blob \| history
test/regress/regress0/sygus/let-ringer.sy		diff \| blob \| history
test/regress/regress0/sygus/let-simp.sy		diff \| blob \| history
test/regress/regress0/sygus/list-head-x.sy		diff \| blob \| history
test/regress/regress0/sygus/max.sy		diff \| blob \| history
test/regress/regress0/sygus/max2-univ.sy		diff \| blob \| history
test/regress/regress0/sygus/multi-fun-polynomial2.sy		diff \| blob \| history
test/regress/regress0/sygus/nflat-fwd-3.sy		diff \| blob \| history
test/regress/regress0/sygus/nflat-fwd.sy		diff \| blob \| history
test/regress/regress0/sygus/no-flat-simp.sy		diff \| blob \| history
test/regress/regress0/sygus/no-mention.sy		diff \| blob \| history
test/regress/regress0/sygus/no-syntax-test-bool.sy		diff \| blob \| history
test/regress/regress0/sygus/no-syntax-test-no-si.sy		diff \| blob \| history
test/regress/regress0/sygus/no-syntax-test.sy		diff \| blob \| history
test/regress/regress0/sygus/parity-AIG-d0.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-small.sy		diff \| blob \| history
test/regress/regress0/sygus/sygus-dt.sy		diff \| blob \| history
test/regress/regress0/sygus/tl-type.sy		diff \| blob \| history
test/regress/regress0/sygus/twolets1.sy		diff \| blob \| history
test/regress/regress0/sygus/twolets2-orig.sy		diff \| blob \| history
test/regress/regress0/sygus/uminus_one.sy		diff \| blob \| history
test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy		diff \| blob \| history

RSS Atom