diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_modules.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_modules.cpp | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 573824b80..f1a05f401 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -40,49 +40,50 @@ QuantifiersModules::~QuantifiersModules() {} void QuantifiersModules::initialize(QuantifiersEngine* qe, QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, std::vector<QuantifiersModule*>& modules) { // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qe, qs, qim)); + d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim)); + d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qe, qs, qim)); + d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim)); + d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr)); modules.push_back(d_i_cbqi.get()); qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new SynthEngine(qe, qs, qim)); + d_synth_e.reset(new SynthEngine(qe, qs, qim, qr)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs, qim)); + d_bint.reset(new BoundedIntegers(qe, qs, qim, qr)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new ModelEngine(qe, qs, qim)); + d_model_engine.reset(new ModelEngine(qe, qs, qim, qr)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qe, qs, qim)); + d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -93,12 +94,12 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { d_rel_dom.reset(new RelevantDomain(qe)); - d_fs.reset(new InstStrategyEnum(qe, qs, qim, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qe, qs, qim)); + d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr)); modules.push_back(d_sygus_inst.get()); } } |