#include "theory/quantifiers/quantifiers_modules.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_registry.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
DecisionManager* dm,
std::vector<QuantifiersModule*>& modules)
{
// add quantifiers modules
if (options::quantConflictFind())
{
- d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr));
+ d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr, tr));
modules.push_back(d_qcf.get());
}
if (options::conjectureGen())
{
- d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr));
+ d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr, tr));
modules.push_back(d_sg_gen.get());
}
if (!options::finiteModelFind() || options::fmfInstEngine())
{
- d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr));
+ d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr));
modules.push_back(d_inst_engine.get());
}
if (options::cegqi())
{
- d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr));
+ d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr, tr));
modules.push_back(d_i_cbqi.get());
- qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
+ qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
}
if (options::sygus())
{
- d_synth_e.reset(new SynthEngine(qe, qs, qim, qr));
+ d_synth_e.reset(new SynthEngine(qe, qs, qim, qr, tr));
modules.push_back(d_synth_e.get());
}
// finite model finding
if (options::fmfBound())
{
- d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
+ d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr, dm));
modules.push_back(d_bint.get());
}
if (options::finiteModelFind() || options::fmfBound())
{
- d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
+ d_model_engine.reset(new ModelEngine(qe, qs, qim, qr, tr));
modules.push_back(d_model_engine.get());
Trace("quant-init-debug")
<< "Initialize model engine, mbqi : " << options::mbqiMode() << " "
<< options::fmfBound() << std::endl;
- if (useFmcModel())
+ if (tr.useFmcModel())
{
Trace("quant-init-debug") << "...make fmc builder." << std::endl;
- d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
+ d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
}
else
{
Trace("quant-init-debug")
<< "...make default model builder." << std::endl;
- d_builder.reset(new QModelBuilder(qs, qr));
+ d_builder.reset(new QModelBuilder(qs, qr, qim));
}
- // !!!!!!!!!!!!! temporary (project #15)
- d_builder->finishInit(qe);
}
if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
{
- d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr));
+ d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr, tr));
modules.push_back(d_qsplit.get());
}
if (options::quantAlphaEquiv())
if (options::fullSaturateQuant() || options::fullSaturateInterleave())
{
d_rel_dom.reset(new RelevantDomain(qe, qr));
- d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
+ d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get()));
modules.push_back(d_fs.get());
}
if (options::sygusInst())
{
- d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr));
+ d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr, tr));
modules.push_back(d_sygus_inst.get());
}
}
-bool QuantifiersModules::useFmcModel()
-{
- return options::mbqiMode() == options::MbqiMode::FMC
- || options::mbqiMode() == options::MbqiMode::TRUST
- || options::fmfBound();
-}
-
} // namespace quantifiers
} // namespace theory
} // namespace CVC4