cleaning up some of the equality query stuff, implemented a new representative select...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 31 Oct 2012 00:54:24 +0000 (00:54 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 31 Oct 2012 00:54:24 +0000 (00:54 +0000)
commitf40d0a7cc8d6af511cc0817caf8df3296a59f380
treea79f142c5b6fbeaec34978f8da2b2db308a33e79
parent5b4c416608bda1df62e1ffe7131648a89882ddc7
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
18 files changed:
src/theory/quantifiers/inst_match.cpp
src/theory/quantifiers/inst_match.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/instantiation_engine.h
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_builder.h
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/options
src/theory/quantifiers/quant_util.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/theory.h
src/theory/uf/inst_strategy.cpp
src/theory/uf/inst_strategy.h
src/theory/uf/theory_uf_instantiator.cpp
src/theory/uf/theory_uf_instantiator.h
src/theory/uf/theory_uf_strong_solver.cpp