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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 3 Jan 2014 18:13:13 +0000 (12:13 -0600)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 3 Jan 2014 18:13:23 +0000 (12:13 -0600)
commit	93f084750d8a76d63fc74d242944bce0635c2194
tree	8b781cf252fb78e16158e307de973e61f6f331eb	tree
parent	9846e1db91243c3b507300dad318e81e28f9d4f4	commit \| diff

Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.

27 files changed:

proofs/signatures/smt.plf		diff \| blob \| history
proofs/signatures/th_arrays.plf	[new file with mode: 0755]	blob
proofs/signatures/th_base.plf		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/smt/smt_engine.cpp		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/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		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		diff \| blob \| history
src/theory/quantifiers/modes.h		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/options_handlers.h		diff \| blob \| history
src/theory/quantifiers/qinterval_builder.cpp	[new file with mode: 0755]	blob
src/theory/quantifiers/qinterval_builder.h	[new file with mode: 0755]	blob
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_types.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history

RSS Atom