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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 9 Feb 2014 22:14:31 +0000 (16:14 -0600)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 9 Feb 2014 22:14:42 +0000 (16:14 -0600)
commit	19697d530ae6eaf0165270bc3628f76124a45953
tree	baa129ef51cc45295dc9f2f7cc176ca27768f4f9	tree
parent	b3f5d2860747c2608c0d765d105c8dd32ee57e1d	commit \| diff

More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc

14 files changed:

src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
test/regress/regress0/bug512.minimized.smt2		diff \| blob \| history
test/regress/regress0/bug519.smt2		diff \| blob \| history
test/regress/regress0/decision/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/ex1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ex1.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ex7.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ex7.smt2.expect	[deleted file]	blob \| history

RSS Atom