diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 17:08:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-11 17:08:07 -0500 |
| commit | 81cd457d729f845f1b76d457359a0ae9963c0f88 (patch) | |
| tree | c521ed630f3514b26bfbce227a1e1e41b8dac01a /src/theory/quantifiers_engine.cpp | |
| parent | 3e6de62d11dcb3cf266f58e68def2f2c2ce728c3 (diff) | |
Infrastructure for instantiation rewriter (#3262)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f57667be5..def1f969c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -128,6 +128,7 @@ class QuantifiersEnginePrivate { d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); modules.push_back(d_i_cbqi.get()); + qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::ceGuidedInst()) { @@ -391,10 +392,6 @@ quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { return d_private->d_synth_e.get(); } -quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const -{ - return d_private->d_i_cbqi.get(); -} QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); |