Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantif...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 9 Feb 2016 19:23:18 +0000 (13:23 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 9 Feb 2016 19:23:18 +0000 (13:23 -0600)
commit49d1898de725a5fac3f68845809ba152eae11282
tree7884934f92d895c7d76adfba1f03c0e40503a708
parent2dd6292b73e4e19be2e261c7fe5664bd2b0149bd
Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations.
src/smt/smt_engine.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers_engine.cpp
src/theory/uf/theory_uf_strong_solver.cpp
src/theory/uf/theory_uf_strong_solver.h