quantifiers now uses master equality engine, preparation work to cleanup code
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 30 Nov 2012 20:38:45 +0000 (20:38 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 30 Nov 2012 20:38:45 +0000 (20:38 +0000)
commitf28bab562105548413cfca93de5c9b047157a076
treebfbe95b9aed35f91b6bd9e3af50fad03ab86f23b
parent6369830eec077ef112e6cc806cd910c7209eb2db
quantifiers now uses master equality engine, preparation work to cleanup code
17 files changed:
src/theory/arith/theory_arith_instantiator.cpp
src/theory/arrays/theory_arrays_instantiator.cpp
src/theory/datatypes/theory_datatypes_instantiator.cpp
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/rewriterules/efficient_e_matching.cpp
src/theory/rewriterules/efficient_e_matching.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/inst_strategy.cpp
src/theory/uf/inst_strategy.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf_instantiator.cpp
src/theory/uf/theory_uf_instantiator.h