made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)
committerMorgan Deters <mdeters@cs.nyu.edu>
Mon, 28 Jan 2013 14:59:58 +0000 (09:59 -0500)
commit79d4733d97dfed6c1198777df5f74f976c80aaf6
tree11a980357f4787d18b20129dafebfd15207695e8
parent73aa7b9dbc5415b6904539c2dd24683e77ca9b20
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)
src/theory/quantifiers/inst_match.cpp
src/theory/quantifiers/inst_match.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/options
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/theory_engine.cpp