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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 2 Dec 2016 20:25:07 +0000 (14:25 -0600)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Fri, 2 Dec 2016 20:25:07 +0000 (14:25 -0600)
commit	c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7
tree	f4a8372d8cd693df5f33e8d49cea53dbb418349e	tree
parent	623e701247ed08e3f59d57b18ebe42f4d4db221e	commit \| diff

Bug fixes and refactoring of parametric datatypes, add some regressions.

23 files changed:

src/expr/datatype.cpp		diff \| blob \| history
src/expr/datatype.h		diff \| blob \| history
src/expr/type.cpp		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/dt-param-card4-unsat.smt2	[new file with mode: 0644]	blob