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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 12 Jul 2012 18:30:15 +0000 (18:30 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 12 Jul 2012 18:30:15 +0000 (18:30 +0000)
commit	65798541fa437278cde0c759ab70fd9fa4fe9638
tree	27341327b8159e58a5ce6371bede6129bf67beb3	tree
parent	78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788	commit \| diff

merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

87 files changed:

README.fmf-devel	[new file with mode: 0644]	blob
src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt/Smt.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		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_instantiator.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.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/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/example/theory_uf_tim.h		diff \| blob \| history
src/theory/inst_match.cpp		diff \| blob \| history
src/theory/inst_match.h		diff \| blob \| history
src/theory/instantiator_default.cpp		diff \| blob \| history
src/theory/instantiator_default.h		diff \| blob \| history
src/theory/model.cpp	[new file with mode: 0644]	blob
src/theory/model.h	[new file with mode: 0644]	blob
src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/first_order_model.h	[new file with mode: 0644]	blob
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.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/relevant_domain.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/relevant_domain.h	[new file with mode: 0644]	blob
src/theory/quantifiers/rep_set_iterator.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/rep_set_iterator.h	[new file with mode: 0644]	blob
src/theory/quantifiers/term_database.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/term_database.h	[new file with mode: 0644]	blob
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.cpp		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/theory.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/trigger.cpp		diff \| blob \| history
src/theory/trigger.h		diff \| blob \| history
src/theory/uf/Makefile.am		diff \| blob \| history
src/theory/uf/inst_strategy.cpp		diff \| blob \| history
src/theory/uf/inst_strategy.h		diff \| blob \| history
src/theory/uf/kinds		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_candidate_generator.cpp		diff \| 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	[new file with mode: 0644]	blob
src/theory/uf/theory_uf_model.h	[new file with mode: 0644]	blob
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/Makefile.am		diff \| blob \| history
src/util/dump.h		diff \| blob \| history
src/util/model.cpp	[new file with mode: 0644]	blob
src/util/model.h	[new file with mode: 0644]	blob
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history

RSS Atom