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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 27 Jul 2012 19:27:45 +0000 (19:27 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 27 Jul 2012 19:27:45 +0000 (19:27 +0000)
commit	9a994c449d65e64d574a423ad9caad519f8c2148
tree	3c4571098d1771f8d277406c9f6e9c5b09dcd1da	tree
parent	4bfa927dac67bbcadf219f70e61f1d123e33944b	commit \| diff

merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

54 files changed:

src/parser/smt2/Smt2.g		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/arrays/Makefile.am		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.h		diff \| blob \| history
src/theory/arrays/theory_arrays_model.cpp	[new file with mode: 0644]	blob
src/theory/arrays/theory_arrays_model.h	[new file with mode: 0644]	blob
src/theory/candidate_generator.cpp	[new file with mode: 0644]	blob
src/theory/candidate_generator.h	[new file with mode: 0644]	blob
src/theory/datatypes/Makefile.am		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_instantiator.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_instantiator.h		diff \| blob \| history
src/theory/inst_match.cpp		diff \| blob \| history
src/theory/inst_match.h		diff \| blob \| history
src/theory/inst_match_impl.h	[deleted file]	blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/model.h		diff \| blob \| history
src/theory/quantifiers/Makefile.am		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/model_builder.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/model_builder.h	[new file with mode: 0644]	blob
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/rep_set_iterator.cpp		diff \| blob \| history
src/theory/quantifiers/rep_set_iterator.h		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
src/theory/rr_candidate_generator.cpp	[new file with mode: 0644]	blob
src/theory/rr_candidate_generator.h	[new file with mode: 0644]	blob
src/theory/rr_inst_match.cpp		diff \| blob \| history
src/theory/rr_inst_match_impl.h		diff \| blob \| history
src/theory/rr_trigger.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/trigger.cpp		diff \| blob \| history
src/theory/uf/Makefile.am		diff \| blob \| history
src/theory/uf/theory_uf_candidate_generator.cpp	[deleted file]	blob \| history
src/theory/uf/theory_uf_candidate_generator.h	[deleted file]	blob \| history
src/theory/uf/theory_uf_instantiator.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.h		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.h		diff \| blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/v1l20009.cvc		diff \| blob \| history
test/regress/regress0/datatypes/wrong-sel-simp.cvc	[new file with mode: 0644]	blob

RSS Atom