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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 31 Aug 2012 16:48:20 +0000 (16:48 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 31 Aug 2012 16:48:20 +0000 (16:48 +0000)
commit	3c4935c7c0c6774588af94c82307a960e58a1154
tree	e518c60ec182e91300fe53293c42cd4b85e49d29	tree
parent	ec9e426df607f13e5a0c0f52fbc6ed5dbb79fdf9	commit \| diff

merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

106 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.h		diff \| blob \| history
src/printer/dagification_visitor.cpp		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt/smt_printer.cpp		diff \| blob \| history
src/printer/smt/smt_printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/options		diff \| blob \| history
src/smt/Makefile.am		diff \| blob \| history
src/smt/model_format_mode.cpp	[new file with mode: 0644]	blob
src/smt/model_format_mode.h	[new file with mode: 0644]	blob
src/smt/options		diff \| blob \| history
src/smt/options_handlers.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_instantiator.cpp		diff \| blob \| history
src/theory/arith/theory_arith_instantiator.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_model.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_model.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/options		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/example/theory_uf_tim.h		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/model.h		diff \| blob \| history
src/theory/output_channel.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/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_when_mode.cpp	[deleted file]	blob \| history
src/theory/quantifiers/inst_when_mode.h	[deleted file]	blob \| history
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/kinds		diff \| blob \| history
src/theory/quantifiers/literal_match_mode.cpp	[deleted file]	blob \| history
src/theory/quantifiers/literal_match_mode.h	[deleted file]	blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/modes.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/modes.h	[new file with mode: 0644]	blob
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/options_handlers.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/quantifiers_attributes.h	[new file with mode: 0644]	blob
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
src/theory/quantifiers/rep_set_iterator.cpp	[deleted file]	blob \| history
src/theory/quantifiers/rep_set_iterator.h	[deleted file]	blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rep_set.cpp	[new file with mode: 0644]	blob
src/theory/rep_set.h	[new file with mode: 0644]	blob
src/theory/rewriterules/theory_rewriterules.cpp		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/kinds		diff \| blob \| history
src/theory/uf/options		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.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
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history
src/util/model.h		diff \| blob \| history
test/regress/regress0/quantifiers/refcount24.cvc	[new file with mode: 0644]	blob
test/unit/theory/theory_engine_white.h		diff \| blob \| history

RSS Atom