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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 1 Dec 2012 02:57:59 +0000 (02:57 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 1 Dec 2012 02:57:59 +0000 (02:57 +0000)
commit	959f5e77f96b406a498c3b67ce22d25e39d7bd2d
tree	e3cb4518ff5156de8286f9351a827bf40636804e	tree
parent	b66fc3eac2717e8a887f1d4603c15cbcb7460e98	commit \| diff

drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

50 files changed:

src/theory/arith/Makefile.am		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_instantiator.cpp	[deleted file]	blob \| history
src/theory/arith/theory_arith_instantiator.h	[deleted file]	blob \| history
src/theory/arrays/Makefile.am		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.cpp	[deleted file]	blob \| history
src/theory/arrays/theory_arrays_instantiator.h	[deleted file]	blob \| history
src/theory/datatypes/Makefile.am		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_instantiator.cpp	[deleted file]	blob \| history
src/theory/datatypes/theory_datatypes_instantiator.h	[deleted file]	blob \| history
src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp	[new file with mode: 0755]	blob
src/theory/quantifiers/inst_strategy_cbqi.h	[new file with mode: 0755]	blob
src/theory/quantifiers/inst_strategy_e_matching.cpp	[new file with mode: 0755]	blob
src/theory/quantifiers/inst_strategy_e_matching.h	[new file with mode: 0755]	blob
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/instantiator_default.cpp	[deleted file]	blob \| history
src/theory/quantifiers/instantiator_default.h	[deleted file]	blob \| history
src/theory/quantifiers/kinds		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| 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_instantiator.cpp	[deleted file]	blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.h	[deleted file]	blob \| history
src/theory/quantifiers/trigger.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriterules/efficient_e_matching.cpp		diff \| blob \| history
src/theory/rewriterules/rr_candidate_generator.cpp		diff \| blob \| history
src/theory/rewriterules/rr_candidate_generator.h		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.cpp		diff \| blob \| history
src/theory/rewriterules/rr_trigger.cpp		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/uf/Makefile.am		diff \| blob \| history
src/theory/uf/inst_strategy.cpp	[deleted file]	blob \| history
src/theory/uf/inst_strategy.h	[deleted file]	blob \| history
src/theory/uf/kinds		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.cpp	[deleted file]	blob \| history
src/theory/uf/theory_uf_instantiator.h	[deleted file]	blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history

RSS Atom