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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 20 Jul 2015 17:46:21 +0000 (19:46 +0200)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 20 Jul 2015 17:46:21 +0000 (19:46 +0200)
commit	f62d9456b41bf17df1d339e46776c9213cb3705a
tree	01d3448b3c9fe89ead56c72b18f8516292092e13	tree
parent	7943953741c67d8246f983e193d26812d959b4cd	commit \| diff

Squashed merge of SygusComp 2015 branch.

35 files changed:

src/Makefile.am		diff \| blob \| history
src/parser/parser.h		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/parser/smt2/smt2_input.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.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/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.h		diff \| blob \| history
src/theory/quantifiers/fun_def_engine.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/fun_def_engine.h	[new file with mode: 0644]	blob
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.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
src/theory/quantifiers_engine.h		diff \| blob \| history
test/regress/regress0/sygus/Makefile.am		diff \| blob \| history
test/regress/regress0/sygus/enum-test.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/inv-example.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/nflat-fwd-3.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/no-syntax-test-bool.sy	[new file with mode: 0644]	blob
test/regress/regress0/sygus/uminus_one.sy	[new file with mode: 0644]	blob

RSS Atom