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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 19 Feb 2016 04:50:05 +0000 (22:50 -0600)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 19 Feb 2016 04:50:05 +0000 (22:50 -0600)
commit	f47f24528f5d19ac0affd572f3d34c090e97f9f9
tree	6a21c1964d862f99d9137f968881a0da33c59d1d	tree
parent	793361d81f0766c6a28ff699ed5447d9b8f8c123	commit \| diff

Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.

20 files changed:

src/Makefile.am		diff \| blob \| history
src/expr/datatype.cpp		diff \| blob \| history
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/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
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_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/quant_split.h	[new file with mode: 0644]	blob
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
test/regress/regress0/fmf/Makefile.am		diff \| blob \| history
test/regress/regress0/fmf/datatypes-ufinite.smt2	[new file with mode: 0644]	blob