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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 3 Nov 2017 20:36:38 +0000 (15:36 -0500)
committer	GitHub <noreply@github.com>
	Fri, 3 Nov 2017 20:36:38 +0000 (15:36 -0500)
commit	5cafed748989602263b8ad1a27ac6b9bd159a441
tree	b0e474f47251d480dce48637e73f663aba0dd179	tree
parent	3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9	commit \| diff

Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.

77 files changed:

src/main/driver_unified.cpp		diff \| blob \| history
src/options/Makefile.am		diff \| blob \| history
src/options/options.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/options_public_functions.cpp		diff \| blob \| history
src/options/quantifiers_options		diff \| blob \| history
src/options/smt_options		diff \| blob \| history
src/options/sygus_out_mode.h	[new file with mode: 0644]	blob
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
test/regress/regress0/expect/scrub.07.sy		diff \| blob \| history
test/regress/regress0/expect/scrub.08.sy		diff \| blob \| history
test/regress/regress0/sygus/General_plus10.sy		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/cegar1.sy		diff \| blob \| history
test/regress/regress0/sygus/cggmp.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/fg_polynomial3.sy		diff \| blob \| history
test/regress/regress0/sygus/hd-01-d1-prog.sy		diff \| blob \| history
test/regress/regress0/sygus/icfp_14.12.sy		diff \| blob \| history
test/regress/regress0/sygus/icfp_28_10.sy		diff \| blob \| history
test/regress/regress0/sygus/icfp_easy-ite.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/nia-max-square-ns.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/parse-bv-let.sy		diff \| blob \| history
test/regress/regress0/sygus/qe.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-concat-3-args.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-small.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-template-infer.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-trivial-simp.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-trivial.sy		diff \| blob \| history
test/regress/regress0/sygus/strings-unconstrained.sy		diff \| blob \| history
test/regress/regress0/sygus/sygus-dt.sy		diff \| blob \| history
test/regress/regress0/sygus/tl-type-0.sy		diff \| blob \| history
test/regress/regress0/sygus/tl-type-4x.sy		diff \| blob \| history
test/regress/regress0/sygus/tl-type.sy		diff \| blob \| history
test/regress/regress0/sygus/triv-type-mismatch-si.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
test/regress/regress1/sygus/MPwL_d1s3.sy		diff \| blob \| history
test/regress/regress1/sygus/VC22_a.sy		diff \| blob \| history
test/regress/regress1/sygus/array_sum_dd.sy		diff \| blob \| history
test/regress/regress1/sygus/hd-sdiv.sy		diff \| blob \| history
test/regress/regress1/sygus/icfp_easy_mt_ite.sy		diff \| blob \| history
test/regress/regress1/sygus/inv_gen_fig8.sy		diff \| blob \| history
test/regress/regress1/sygus/inv_gen_n_c11.sy		diff \| blob \| history
test/regress/regress1/sygus/mpg_guard1-dd.sy		diff \| blob \| history
test/regress/regress1/sygus/nia-max-square.sy		diff \| blob \| history
test/regress/regress1/sygus/stopwatch-bt.sy		diff \| blob \| history
test/regress/regress1/sygus/three.sy		diff \| blob \| history
test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy		diff \| blob \| history

RSS Atom