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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Sat, 25 Jul 2015 14:40:54 +0000 (16:40 +0200)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Sat, 25 Jul 2015 14:40:54 +0000 (16:40 +0200)
commit	c0079b3110a81f2ff993b7f86782266380dd102e
tree	c39d61ecc3857ebe5af75bd41ef7c11353e0824a	tree
parent	7dcb635088e73b508dbe00ae7fe08dae99968416	commit \| diff

Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

39 files changed:

src/main/driver_unified.cpp		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/smt/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_instantiation.h		diff \| blob \| history
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/modes.h		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/options_handlers.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		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/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/dup-op.sy		diff \| blob \| history
test/regress/regress0/sygus/enum-test.sy		diff \| blob \| history
test/regress/regress0/sygus/hd-01-d1-prog.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/max.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-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/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