d_alpha_equiv(nullptr),
d_inst_engine(nullptr),
d_model_engine(nullptr),
+ d_builder(nullptr),
d_bint(nullptr),
d_qcf(nullptr),
d_sg_gen(nullptr),
{
d_model_engine.reset(new ModelEngine(qe, qs, qim, qr));
modules.push_back(d_model_engine.get());
+ Trace("quant-init-debug")
+ << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+ << options::fmfBound() << std::endl;
+ if (useFmcModel())
+ {
+ Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+ d_builder.reset(new fmcheck::FullModelChecker(qs, qr));
+ }
+ else
+ {
+ Trace("quant-init-debug")
+ << "...make default model builder." << std::endl;
+ d_builder.reset(new QModelBuilder(qs, qr));
+ }
+ // !!!!!!!!!!!!! temporary (project #15)
+ d_builder->finishInit(qe);
}
if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
{
}
}
+bool QuantifiersModules::useFmcModel()
+{
+ return options::mbqiMode() == options::MbqiMode::FMC
+ || options::mbqiMode() == options::MbqiMode::TRUST
+ || options::fmfBound();
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#include "theory/quantifiers/conjecture_generator.h"
#include "theory/quantifiers/ematching/instantiation_engine.h"
#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/inst_strategy_enumerative.h"
#include "theory/quantifiers/quant_conflict_find.h"
DecisionManager* dm,
std::vector<QuantifiersModule*>& modules);
+ /** Whether we use the full model check builder and corresponding model */
+ static bool useFmcModel();
+
private:
//------------------------------ quantifier utilities
/** relevant domain */
std::unique_ptr<InstantiationEngine> d_inst_engine;
/** model engine */
std::unique_ptr<ModelEngine> d_model_engine;
+ /** model builder */
+ std::unique_ptr<quantifiers::QModelBuilder> d_builder;
/** bounded integers utility */
std::unique_ptr<BoundedIntegers> d_bint;
/** Conflict find mechanism for quantifiers */
#include "theory/quantifiers/theory_quantifiers.h"
-#include "base/check.h"
-#include "expr/kind.h"
#include "expr/proof_node_manager.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/first_order_model_fmc.h"
+#include "theory/quantifiers/quantifiers_modules.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/valuation.h"
using namespace CVC4::kind;
d_qstate(c, u, valuation, logicInfo),
d_qreg(),
d_treg(d_qstate, d_qreg),
- d_qim(*this, d_qstate, pnm),
- d_qengine(d_qstate, d_qreg, d_treg, d_qim, pnm)
+ d_qim(*this, d_qstate, pnm)
{
// Finish initializing the term registry by hooking it up to the inference
// manager. This is required due to a cyclic dependency between the term
// use the inference manager as the official inference manager
d_inferManager = &d_qim;
+ Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
+ Trace("quant-engine-debug")
+ << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
+ // Finite model finding requires specialized ways of building the model.
+ // We require constructing the model here, since it is required for
+ // initializing the CombinationEngine and the rest of quantifiers engine.
+ if (options::finiteModelFind() || options::fmfBound())
+ {
+ if (QuantifiersModules::useFmcModel())
+ {
+ d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+ d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
+ }
+ else
+ {
+ d_qmodel.reset(new quantifiers::FirstOrderModel(
+ d_qstate, d_qreg, d_treg, "FirstOrderModel"));
+ }
+ }
+ else
+ {
+ d_qmodel.reset(new quantifiers::FirstOrderModel(
+ d_qstate, d_qreg, d_treg, "FirstOrderModel"));
+ }
+
+ // construct the quantifiers engine
+ d_qengine.reset(new QuantifiersEngine(
+ d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm));
+
+ //!!!!!!!!!!!!!! temporary (project #15)
+ d_qmodel->finishInit(d_qengine.get());
+
// Set the pointer to the quantifiers engine, which this theory owns. This
// pointer will be retreived by TheoryEngine and set to all theories
// post-construction.
- d_quantEngine = &d_qengine;
+ d_quantEngine = d_qengine.get();
}
TheoryQuantifiers::~TheoryQuantifiers() {
#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#include "expr/node.h"
+#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/proof_checker.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_registry.h"
/** The quantifiers state */
QuantifiersState d_qstate;
/** The quantifiers registry */
- quantifiers::QuantifiersRegistry d_qreg;
+ QuantifiersRegistry d_qreg;
+ /** extended model object */
+ std::unique_ptr<FirstOrderModel> d_qmodel;
/** The term registry */
- quantifiers::TermRegistry d_treg;
+ TermRegistry d_treg;
/** The quantifiers inference manager */
QuantifiersInferenceManager d_qim;
/** The quantifiers engine, which lives here */
- QuantifiersEngine d_qengine;
+ std::unique_ptr<QuantifiersEngine> d_qengine;
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::FirstOrderModel* qm,
ProofNodeManager* pnm)
: d_qstate(qstate),
d_qim(qim),
d_qreg(qr),
d_treg(tr),
d_tr_trie(new inst::TriggerTrie),
- d_model(nullptr),
- d_builder(nullptr),
- d_eq_query(nullptr),
+ d_model(qm),
+ d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(qstate, qm)),
d_instantiate(
new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext())
{
- //---- utilities
- // quantifiers registry must come before the other utilities
+ // initialize the utilities
+ d_util.push_back(d_eq_query.get());
+ // quantifiers registry must come before the remaining utilities
d_util.push_back(&d_qreg);
d_util.push_back(tr.getTermDatabase());
-
d_util.push_back(d_instantiate.get());
-
- Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
- Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
-
- //---- end utilities
-
- // Finite model finding requires specialized ways of building the model.
- // We require constructing the model and model builder here, since it is
- // required for initializing the CombinationEngine.
- if (options::finiteModelFind() || options::fmfBound())
- {
- Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
- if (options::mbqiMode() == options::MbqiMode::FMC
- || options::mbqiMode() == options::MbqiMode::TRUST
- || options::fmfBound())
- {
- Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
- d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- qstate, qr, tr, "FirstOrderModelFmc"));
- d_builder.reset(new quantifiers::fmcheck::FullModelChecker(qstate, qr));
- }else{
- Trace("quant-engine-debug") << "...make default model builder." << std::endl;
- d_model.reset(
- new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
- d_builder.reset(new quantifiers::QModelBuilder(qstate, qr));
- }
- d_builder->finishInit(this);
- }else{
- d_model.reset(
- new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
- }
- //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
- d_model->finishInit(this);
- // initialize the equality query
- d_eq_query.reset(
- new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
- d_util.insert(d_util.begin(), d_eq_query.get());
}
QuantifiersEngine::~QuantifiersEngine() {}
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
- return d_builder.get();
+ return d_qmodules->d_builder.get();
}
quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
{
- return d_model.get();
+ return d_model;
}
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
{
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::FirstOrderModel* qm,
ProofNodeManager* pnm);
~QuantifiersEngine();
//---------------------- external interface
/** all triggers will be stored in this trie */
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
- std::unique_ptr<quantifiers::FirstOrderModel> d_model;
- /** model builder */
- std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+ quantifiers::FirstOrderModel* d_model;
/** equality query class */
std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
/** instantiate utility */
d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
Assert(d_quantEngine != nullptr);
}
+ // finish initializing the quantifiers engine, which must come before
+ // initializing theory combination, since quantifiers engine may have a
+ // special model builder object
+ if (d_logicInfo.isQuantified())
+ {
+ d_quantEngine->finishInit(this, d_decManager.get());
+ }
// initialize the theory combination manager, which decides and allocates the
// equality engines to use for all theories.
d_tc->finishInit();
// get pointer to the shared solver
d_sharedSolver = d_tc->getSharedSolver();
- // finish initializing the quantifiers engine
- if (d_logicInfo.isQuantified())
- {
- d_quantEngine->finishInit(this, d_decManager.get());
- }
-
// finish initializing the theories by linking them with the appropriate
// utilities and then calling their finishInit method.
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
projects / cvc5.git / commitdiff