diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-12 14:23:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-12 14:23:31 -0500 |
| commit | 75d70649e2d72d6d6bb46f47cf96ee523b718cb9 (patch) | |
| tree | f413238a6a8ee90d9c47327bd0a0de18906af809 /src/theory/quantifiers_engine.cpp | |
| parent | fcd3d91281891bda5d5f4fe60ebb2d282de439c6 (diff) | |
Give rewrite engine pointer to conflict-based instantiation module (#3174)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f0b0c31df..c17af1e1f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -149,7 +149,7 @@ class QuantifiersEnginePrivate } if (options::quantRewriteRules()) { - d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe)); + d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get())); modules.push_back(d_rr_engine.get()); } if (options::ltePartialInst()) @@ -408,10 +408,6 @@ quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const { return d_private->d_bint.get(); } -quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const -{ - return d_private->d_qcf.get(); -} quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { return d_private->d_synth_e.get(); |