This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.
This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.
As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.
This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.
This also avoids the need for casting TheoryModel to FirstOrderModel.
d_sharedSolver(nullptr),
d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
: nullptr)
-{
-}
-
-CombinationEngine::~CombinationEngine() {}
-
-void CombinationEngine::finishInit()
{
// create the equality engine, model manager, and shared solver
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
Unhandled() << "CombinationEngine::finishInit: equality engine mode "
<< options::eeMode() << " not supported";
}
+}
+
+CombinationEngine::~CombinationEngine() {}
+void CombinationEngine::finishInit()
+{
Assert(d_eemanager != nullptr);
// initialize equality engines in all theories, including quantifiers engine
d_eem(eem),
d_modelEqualityEngine(nullptr),
d_modelEqualityEngineAlloc(nullptr),
- d_model(nullptr),
+ d_model(new TheoryModel(te.getUserContext(),
+ "DefaultModel",
+ options::assignFunctionValues())),
d_modelBuilder(nullptr),
d_modelBuilt(false),
d_modelBuiltSuccess(false)
QuantifiersEngine* qe = d_te.getQuantifiersEngine();
Assert(qe != nullptr);
d_modelBuilder = qe->getModelBuilder();
- d_model = qe->getModel();
- }
- else
- {
- context::Context* u = d_te.getUserContext();
- d_alocModel.reset(
- new TheoryModel(u, "DefaultModel", options::assignFunctionValues()));
- d_model = d_alocModel.get();
}
// make the default builder, e.g. in the case that the quantifiers engine does
}
Trace("model-builder-debug")
<< " PostProcessModel on theory: " << theoryId << std::endl;
- t->postProcessModel(d_model);
+ t->postProcessModel(d_model.get());
}
// also call the model builder's post-process model
- d_modelBuilder->postProcessModel(incomplete, d_model);
+ d_modelBuilder->postProcessModel(incomplete, d_model.get());
}
-theory::TheoryModel* ModelManager::getModel() { return d_model; }
+theory::TheoryModel* ModelManager::getModel() { return d_model.get(); }
bool ModelManager::collectModelBooleanVariables()
{
*/
void postProcessModel(bool incomplete);
/** Get a pointer to model object maintained by this class. */
- theory::TheoryModel* getModel();
+ TheoryModel* getModel();
//------------------------ finer grained control over model building
/**
* Prepare model, which is the manager-specific method for setting up the
eq::EqualityEngine* d_modelEqualityEngine;
/** The equality engine of the model, if we allocated it */
std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngineAlloc;
- /** The model object we are using */
- theory::TheoryModel* d_model;
/** The model object we have allocated (if one exists) */
- std::unique_ptr<theory::TheoryModel> d_alocModel;
+ std::unique_ptr<TheoryModel> d_model;
/** The model builder object we are using */
- theory::TheoryEngineModelBuilder* d_modelBuilder;
+ TheoryEngineModelBuilder* d_modelBuilder;
/** The model builder object we have allocated (if one exists) */
- std::unique_ptr<theory::TheoryEngineModelBuilder> d_alocModelBuilder;
+ std::unique_ptr<TheoryEngineModelBuilder> d_alocModelBuilder;
/** whether we have tried to build this model in the current context */
bool d_modelBuilt;
/** whether this model has been built successfully */
collectAssertedTerms(theoryId, termSet);
// also get relevant terms
t->computeRelevantTerms(termSet);
- if (!t->collectModelInfo(d_model, termSet))
+ if (!t->collectModelInfo(d_model.get(), termSet))
{
Trace("model-builder")
<< "ModelManagerDistributed: fail collect model info" << std::endl;
bool ModelManagerDistributed::finishBuildModel() const
{
// do not use relevant terms
- if (!d_modelBuilder->buildModel(d_model))
+ if (!d_modelBuilder->buildModel(d_model.get()))
{
Trace("model-builder") << "ModelManager: fail build model" << std::endl;
return false;
FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
QuantifiersRegistry& qr,
- TermRegistry& tr,
- std::string name)
- : TheoryModel(qs.getSatContext(), name, true),
- d_qe(nullptr),
+ TermRegistry& tr)
+ : d_model(nullptr),
d_qreg(qr),
d_treg(tr),
d_eq_query(qs, this),
{
}
-//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
-void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+void FirstOrderModel::finishInit(TheoryModel* m) { d_model = m; }
+
+Node FirstOrderModel::getValue(TNode n) const { return d_model->getValue(n); }
+bool FirstOrderModel::hasTerm(TNode a) { return d_model->hasTerm(a); }
+Node FirstOrderModel::getRepresentative(TNode a)
+{
+ return d_model->getRepresentative(a);
+}
+bool FirstOrderModel::areEqual(TNode a, TNode b)
+{
+ return d_model->areEqual(a, b);
+}
+bool FirstOrderModel::areDisequal(TNode a, TNode b)
+{
+ return d_model->areDisequal(a, b);
+}
+eq::EqualityEngine* FirstOrderModel::getEqualityEngine()
+{
+ return d_model->getEqualityEngine();
+}
+const RepSet* FirstOrderModel::getRepSet() const
+{
+ return d_model->getRepSet();
+}
+RepSet* FirstOrderModel::getRepSetPtr() { return d_model->getRepSetPtr(); }
+TheoryModel* FirstOrderModel::getTheoryModel() { return d_model; }
Node FirstOrderModel::getInternalRepresentative(Node a, Node q, size_t index)
{
Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
//check if there is even any domain elements at all
- if (!d_rep_set.hasType(tn) || d_rep_set.d_type_reps[tn].size() == 0)
+ RepSet* rs = d_model->getRepSetPtr();
+ if (!rs->hasType(tn) || rs->getNumRepresentatives(tn) == 0)
{
Trace("fm-debug") << "Must create domain element for " << tn << "..."
<< std::endl;
Node mbt = getModelBasisTerm(tn);
Trace("fm-debug") << "Add to representative set..." << std::endl;
- d_rep_set.add(tn, mbt);
+ rs->add(tn, mbt);
}
- return d_rep_set.d_type_reps[tn][0];
+ return rs->getRepresentative(tn, 0);
}
bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
{
+ RepSet* rs = d_model->getRepSetPtr();
if (tn.isSort())
{
// must ensure uninterpreted type is non-empty.
- if (!d_rep_set.hasType(tn))
+ if (!rs->hasType(tn))
{
// terms in rep_set are now constants which mapped to terms through
// TheoryModel. Thus, should introduce a constant and a term.
Node var = getSomeDomainElement(tn);
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn
<< std::endl;
- d_rep_set.add(tn, var);
+ rs->add(tn, var);
}
return true;
}
{
Trace("fm-debug") << " do complete, since cardinality is small ("
<< tn.getCardinality() << ")..." << std::endl;
- d_rep_set.complete(tn);
+ rs->complete(tn);
// must have succeeded
- Assert(d_rep_set.hasType(tn));
+ Assert(rs->hasType(tn));
return true;
}
Trace("fm-debug") << " variable cannot be bounded." << std::endl;
namespace cvc5 {
namespace theory {
-class QuantifiersEngine;
+class TheoryModel;
+class RepSet;
namespace quantifiers {
class QuantifiersRegistry;
// TODO (#1301) : document and refactor this class
-class FirstOrderModel : public TheoryModel
+class FirstOrderModel
{
public:
FirstOrderModel(QuantifiersState& qs,
QuantifiersRegistry& qr,
- TermRegistry& tr,
- std::string name);
+ TermRegistry& tr);
+ virtual ~FirstOrderModel() {}
- //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
- /** finish initialize */
- void finishInit(QuantifiersEngine* qe);
+ /** finish init */
+ void finishInit(TheoryModel* m);
+ //---------------------------------- access functions for underlying model
+ /** Get value in the underlying theory model */
+ Node getValue(TNode n) const;
+ /** does the equality engine of this model have term a? */
+ bool hasTerm(TNode a);
+ /** get the representative of a in the equality engine of this model */
+ Node getRepresentative(TNode a);
+ /** are a and b equal in the equality engine of this model? */
+ bool areEqual(TNode a, TNode b);
+ /** are a and b disequal in the equality engine of this model? */
+ bool areDisequal(TNode a, TNode b);
+ /** get the equality engine for this model */
+ eq::EqualityEngine* getEqualityEngine();
+ /** get the representative set object */
+ const RepSet* getRepSet() const;
+ /** get the representative set object */
+ RepSet* getRepSetPtr();
+ /** get the entire theory model */
+ TheoryModel* getTheoryModel();
+ //---------------------------------- end access functions for underlying model
/** get internal representative
*
* Choose a term that is equivalent to a in the current context that is the
EqualityQuery* getEqualityQuery();
protected:
- //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
- QuantifiersEngine* d_qe;
+ /** Pointer to the underyling theory model */
+ TheoryModel* d_model;
/** The quantifiers registry */
QuantifiersRegistry& d_qreg;
/** Reference to the term registry */
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
QuantifiersRegistry& qr,
- TermRegistry& tr,
- std::string name)
- : FirstOrderModel(qs, qr, tr, name)
+ TermRegistry& tr)
+ : FirstOrderModel(qs, qr, tr)
{
}
public:
FirstOrderModelFmc(QuantifiersState& qs,
QuantifiersRegistry& qr,
- TermRegistry& tr,
- std::string name);
+ TermRegistry& tr);
~FirstOrderModelFmc() override;
// initialize the model
void processInitialize(bool ispre) override;
}
FullModelChecker::FullModelChecker(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
- QuantifiersInferenceManager& qim)
- : QModelBuilder(qs, qr, qim)
+ TermRegistry& tr)
+ : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr))
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
+void FullModelChecker::finishInit() { d_model = d_fm.get(); }
+
bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
//standard pre-process
if( !preProcessBuildModelStd( m ) ){
return false;
}
- FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
d_preinitialized_eqc.clear();
d_preinitialized_types.clear();
//traverse equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(m->getEqualityEngine());
while( !eqcs_i.isFinished() ){
Node r = *eqcs_i;
TypeNode tr = r.getType();
//must ensure model basis terms exists in model for each relevant type
Trace("fmc") << "preInitialize types..." << std::endl;
- fm->initialize();
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
+ d_fm->initialize();
+ for (std::pair<const Node, Def*>& mp : d_fm->d_models)
+ {
+ Node op = mp.first;
Trace("fmc") << "preInitialize types for " << op << std::endl;
TypeNode tno = op.getType();
for( unsigned i=0; i<tno.getNumChildren(); i++) {
Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
- preInitializeType( fm, tno[i] );
+ preInitializeType(m, tno[i]);
Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl;
}
}
Trace("fmc") << "Finish preInitialize types" << std::endl;
//do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
- for (unsigned i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant;
+ for (unsigned i = 0, nquant = d_fm->getNumAssertedQuantifiers(); i < nquant;
i++)
{
- Node q = fm->getAssertedQuantifier(i);
+ Node q = d_fm->getAssertedQuantifier(i);
registerQuantifiedFormula(q);
if (!isHandled(q))
{
// make sure all types are set
for (const Node& v : q[0])
{
- preInitializeType(fm, v.getType());
+ preInitializeType(m, v.getType());
}
}
return true;
// nothing to do if no functions
return true;
}
- FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
+ FirstOrderModelFmc* fm = d_fm.get();
Trace("fmc") << "---Full Model Check reset() " << std::endl;
d_quant_models.clear();
d_rep_ids.clear();
d_star_insts.clear();
//process representatives
- RepSet* rs = fm->getRepSetPtr();
+ RepSet* rs = m->getRepSetPtr();
for (std::map<TypeNode, std::vector<Node> >::iterator it =
rs->d_type_reps.begin();
it != rs->d_type_reps.end();
if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
- Node r = fm->getRepresentative( it->second[a] );
+ Node r = m->getRepresentative(it->second[a]);
if( Trace.isOn("fmc-model-debug") ){
std::vector< Node > eqc;
d_qstate.getEquivalenceClass(r, eqc);
}
//now, make models
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
+ for (std::pair<const Node, Def*>& fmm : d_fm->d_models)
+ {
+ Node op = fmm.first;
//reset the model
- fm->d_models[op]->reset();
+ d_fm->d_models[op]->reset();
std::vector< Node > add_conds;
std::vector< Node > add_values;
bool needsDefault = true;
- std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
- if( itut!=fm->d_uf_terms.end() ){
- Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
- for( size_t i=0; i<itut->second.size(); i++ ){
- Node n = itut->second[i];
+ if (m->hasUfTerms(op))
+ {
+ const std::vector<Node>& uft = m->getUfTerms(op);
+ Trace("fmc-model-debug")
+ << uft.size() << " model values for " << op << " ... " << std::endl;
+ for (const Node& n : uft)
+ {
// only consider unique up to congruence (in model equality engine)?
add_conds.push_back( n );
add_values.push_back( n );
- Node r = fm->getRepresentative(n);
+ Node r = m->getRepresentative(n);
Trace("fmc-model-debug") << n << " -> " << r << std::endl;
- //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
}
}else{
Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
Trace("fmc-model-debug") << std::endl;
//possibly get default
if( needsDefault ){
- Node nmb = fm->getModelBasisOpTerm(op);
+ Node nmb = d_fm->getModelBasisOpTerm(op);
//add default value if necessary
- if( fm->hasTerm( nmb ) ){
+ if (m->hasTerm(nmb))
+ {
Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
add_conds.push_back( nmb );
add_values.push_back( nmb );
}else{
- Node vmb = getSomeDomainElement(fm, nmb.getType());
+ Node vmb = getSomeDomainElement(d_fm.get(), nmb.getType());
Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
Trace("fmc-model-debug")
- << fm->getRepSet()->getNumRepresentatives(nmb.getType())
+ << m->getRepSet()->getNumRepresentatives(nmb.getType())
<< std::endl;
add_conds.push_back( nmb );
add_values.push_back( vmb );
return TheoryEngineModelBuilder::processBuildModel( m );
}
-void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
+void FullModelChecker::preInitializeType(TheoryModel* m, TypeNode tn)
+{
if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
d_preinitialized_types[tn] = true;
if (tn.isFirstClass())
{
Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
- Node mb = fm->getModelBasisTerm(tn);
+ Node mb = d_fm->getModelBasisTerm(tn);
Trace("fmc") << "...return " << mb << std::endl;
// if the model basis term does not exist in the model,
// either add it directly to the model's equality engine if no other terms
// of this type exist, or otherwise assert that it is equal to the first
// equivalence class of its type.
- if (!fm->hasTerm(mb) && !mb.isConst())
+ if (!m->hasTerm(mb) && !mb.isConst())
{
std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
if (itpe == d_preinitialized_eqc.end())
{
Trace("fmc") << "...add model basis term to EE of model " << mb << " "
<< tn << std::endl;
- fm->d_equalityEngine->addTerm(mb);
+ m->getEqualityEngine()->addTerm(mb);
}
else
{
Trace("fmc") << "...add model basis eqc equality to model " << mb
<< " == " << itpe->second << " " << tn << std::endl;
- bool ret = fm->assertEquality(mb, itpe->second, true);
+ bool ret = m->assertEquality(mb, itpe->second, true);
AlwaysAssert(ret);
}
}
bool FullModelChecker::useSimpleModels() {
return options::fmfFmcSimple();
}
-
void FullModelChecker::registerQuantifiedFormula(Node q)
{
if (d_quant_cond.find(q) != d_quant_cond.end())
* if a bound variable is of type T, or an uninterpreted function has an
* argument or a return value of type T.
*/
- void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
+ void preInitializeType(TheoryModel* m, TypeNode tn);
/** for each type, an equivalence class of that type from the model */
std::map<TypeNode, Node> d_preinitialized_eqc;
/** map from types to whether we have called the method above */
public:
FullModelChecker(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
- QuantifiersInferenceManager& qim);
-
+ TermRegistry& tr);
+ /** finish init, which sets the model object */
+ void finishInit() override;
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
bool processBuildModel(TheoryModel* m) override;
bool useSimpleModels();
-
private:
/**
* Register quantified formula.
void registerQuantifiedFormula(Node q);
/** Is quantified formula q handled by model-based instantiation? */
bool isHandled(Node q) const;
+ /**
+ * The first order model. This is an extended form of the first order model
+ * class that is specialized for this class.
+ */
+ std::unique_ptr<FirstOrderModelFmc> d_fm;
};/* class FullModelChecker */
} // namespace fmcheck
using namespace cvc5::theory::quantifiers;
QModelBuilder::QModelBuilder(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
- QuantifiersInferenceManager& qim)
+ TermRegistry& tr)
: TheoryEngineModelBuilder(),
d_addedLemmas(0),
d_triedLemmas(0),
d_qstate(qs),
+ d_qim(qim),
d_qreg(qr),
- d_qim(qim)
+ d_treg(tr),
+ d_model(nullptr)
{
}
+void QModelBuilder::finishInit()
+{
+ // allocate the default model
+ d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg));
+ d_model = d_modelAloc.get();
+}
+
bool QModelBuilder::optUseModel() {
return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
}
d_triedLemmas = 0;
if (options::fmfFunWellDefinedRelevant())
{
- FirstOrderModel * fm = (FirstOrderModel*)m;
//traverse equality engine
std::map< TypeNode, bool > eqc_usort;
eq::EqClassesIterator eqcs_i =
- eq::EqClassesIterator(fm->getEqualityEngine());
+ eq::EqClassesIterator(m->getEqualityEngine());
while( !eqcs_i.isFinished() ){
TypeNode tr = (*eqcs_i).getType();
eqc_usort[tr] = true;
++eqcs_i;
}
//look at quantified formulas
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i, true );
- if( fm->isQuantifierActive( q ) ){
+ for (size_t i = 0, nquant = d_model->getNumAssertedQuantifiers();
+ i < nquant;
+ i++)
+ {
+ Node q = d_model->getAssertedQuantifier(i, true);
+ if (d_model->isQuantifierActive(q))
+ {
//check if any of these quantified formulas can be set inactive
if (q[0].getNumChildren() == 1)
{
{
Trace("model-engine-debug")
<< "Irrelevant function definition : " << q << std::endl;
- fm->setQuantifierActive( q, false );
+ d_model->setQuantifierActive(q, false);
}
}
}
void QModelBuilder::debugModel( TheoryModel* m ){
//debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
if( Trace.isOn("quant-check-model") ){
- FirstOrderModel* fm = (FirstOrderModel*)m;
+ FirstOrderModel* fm = d_model;
Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
int tests = 0;
int bad = 0;
vars.push_back( f[0][j] );
}
QRepBoundExt qrbe(qbi, fm);
- RepSetIterator riter(fm->getRepSet(), &qrbe);
+ RepSetIterator riter(m->getRepSet(), &qrbe);
if( riter.setQuantifier( f ) ){
while( !riter.isFinished() ){
tests++;
terms.push_back( riter.getCurrentTerm( k ) );
}
Node n = inst->getInstantiation(f, vars, terms);
- Node val = fm->getValue( n );
+ Node val = m->getValue(n);
if (!val.isConst() || !val.getConst<bool>())
{
Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl;
}
}
}
+FirstOrderModel* QModelBuilder::getModel() { return d_model; }
class QuantifiersState;
class QuantifiersRegistry;
class QuantifiersInferenceManager;
+class TermRegistry;
class QModelBuilder : public TheoryEngineModelBuilder
{
public:
QModelBuilder(QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
- QuantifiersInferenceManager& qim);
-
+ TermRegistry& tr);
+ /** finish init, which sets the model object */
+ virtual void finishInit();
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
// >0 : success
//statistics
unsigned getNumAddedLemmas() { return d_addedLemmas; }
unsigned getNumTriedLemmas() { return d_triedLemmas; }
+ /** get the model we are using */
+ FirstOrderModel* getModel();
protected:
- /** Pointer to quantifiers engine */
- QuantifiersEngine* d_qe;
/** The quantifiers state object */
QuantifiersState& d_qstate;
+ /** The quantifiers inference manager */
+ QuantifiersInferenceManager& d_qim;
/** Reference to the quantifiers registry */
QuantifiersRegistry& d_qreg;
- /** The quantifiers inference manager */
- quantifiers::QuantifiersInferenceManager& d_qim;
+ /** Term registry */
+ TermRegistry& d_treg;
+ /** Pointer to the model object we are using */
+ FirstOrderModel* d_model;
+ /** The model object we have allocated */
+ std::unique_ptr<FirstOrderModel> d_modelAloc;
};
} // namespace quantifiers
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),
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
+ QModelBuilder* builder,
std::vector<QuantifiersModule*>& modules)
{
// add quantifiers modules
d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
modules.push_back(d_bint.get());
}
+
if (options::finiteModelFind() || options::fmfBound())
{
- Trace("quant-init-debug")
- << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
- << options::fmfBound() << std::endl;
- if (tr.useFmcModel())
- {
- Trace("quant-init-debug") << "...make fmc builder." << std::endl;
- 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, qim));
- }
- d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, d_builder.get()));
+ d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
modules.push_back(d_model_engine.get());
}
if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
+ QModelBuilder* builder,
std::vector<QuantifiersModule*>& modules);
private:
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 */
TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
: d_presolve(qs.getUserContext(), true),
- d_useFmcModel(false),
d_presolveCache(qs.getUserContext()),
d_termEnum(new TermEnumeration),
d_termPools(new TermPools(qs)),
d_termDb(new TermDb(qs, qr)),
- d_sygusTdb(nullptr)
+ d_sygusTdb(nullptr),
+ d_qmodel(nullptr)
{
if (options::sygus() || options::sygusInst())
{
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())
- && (options::mbqiMode() == options::MbqiMode::FMC
- || options::mbqiMode() == options::MbqiMode::TRUST
- || options::fmfBound()))
- {
- d_useFmcModel = true;
- d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- qs, qr, *this, "FirstOrderModelFmc"));
- }
- else
- {
- d_qmodel.reset(
- new quantifiers::FirstOrderModel(qs, qr, *this, "FirstOrderModel"));
- }
}
-void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
+void TermRegistry::finishInit(FirstOrderModel* fm,
+ QuantifiersInferenceManager* qim)
{
+ d_qmodel = fm;
d_termDb->finishInit(qim);
if (d_sygusTdb.get())
{
TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
-FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); }
-
-bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
+FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; }
} // namespace quantifiers
} // namespace theory
TermRegistry(QuantifiersState& qs,
QuantifiersRegistry& qr);
/** Finish init, which sets the inference manager on modules of this class */
- void finishInit(QuantifiersInferenceManager* qim);
+ void finishInit(FirstOrderModel* fm, QuantifiersInferenceManager* qim);
/** Presolve */
void presolve();
void processInstantiation(Node q, const std::vector<Node>& terms);
void processSkolemization(Node q, const std::vector<Node>& skolems);
- /** Whether we use the full model check builder and corresponding model */
- bool useFmcModel() const;
-
/** get term database */
TermDb* getTermDatabase() const;
/** get term database sygus */
/** sygus term database */
std::unique_ptr<TermDbSygus> d_sygusTdb;
/** extended model object */
- std::unique_ptr<FirstOrderModel> d_qmodel;
+ FirstOrderModel* d_qmodel;
};
} // namespace quantifiers
out.handleUserAttribute( "quant-elim", this );
out.handleUserAttribute( "quant-elim-partial", this );
- // Finish initializing the term registry by hooking it up to the inference
- // manager. This is required due to a cyclic dependency between the term
- // database and the instantiate module. Term database needs inference manager
- // since it sends out lemmas when term indexing is inconsistent, instantiate
- // needs term database for entailment checks.
- d_treg.finishInit(&d_qim);
-
// construct the quantifiers engine
d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm));
- //!!!!!!!!!!!!!! temporary (project #15)
- d_treg.getModel()->finishInit(d_qengine.get());
-
// indicate we are using the quantifiers theory state object
d_theoryState = &d_qstate;
// use the inference manager as the official inference manager
namespace theory {
QuantifiersEngine::QuantifiersEngine(
- quantifiers::QuantifiersState& qstate,
+ quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
ProofNodeManager* pnm)
- : d_qstate(qstate),
+ : d_qstate(qs),
d_qim(qim),
d_te(nullptr),
d_pnm(pnm),
d_qreg(qr),
d_treg(tr),
- d_model(d_treg.getModel()),
- d_quants_prereg(qstate.getUserContext()),
- d_quants_red(qstate.getUserContext())
+ d_model(nullptr),
+ d_quants_prereg(qs.getUserContext()),
+ d_quants_red(qs.getUserContext())
{
+ Trace("quant-init-debug")
+ << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+ << options::fmfBound() << 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::fmfBound()
+ || (options::finiteModelFind()
+ && (options::mbqiMode() == options::MbqiMode::FMC
+ || options::mbqiMode() == options::MbqiMode::TRUST)))
+ {
+ Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+ d_builder.reset(
+ new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr));
+ }
+ else
+ {
+ Trace("quant-init-debug") << "...make default model builder." << std::endl;
+ d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr));
+ }
+ // set the model object
+ d_builder->finishInit();
+ d_model = d_builder->getModel();
+
+ // Finish initializing the term registry by hooking it up to the model and the
+ // inference manager. The former is required since theories are not given
+ // access to the model in their constructors currently.
+ // The latter is required due to a cyclic dependency between the term
+ // database and the instantiate module. Term database needs inference manager
+ // since it sends out lemmas when term indexing is inconsistent, instantiate
+ // needs term database for entailment checks.
+ d_treg.finishInit(d_model, &d_qim);
+
// initialize the utilities
d_util.push_back(d_model->getEqualityQuery());
// quantifiers registry must come before the remaining utilities
void QuantifiersEngine::finishInit(TheoryEngine* te)
{
+ // connect the quantifiers model to the underlying theory model
+ d_model->finishInit(te->getModel());
d_te = te;
// Initialize the modules and the utilities here.
d_qmodules.reset(new quantifiers::QuantifiersModules);
- d_qmodules->initialize(d_qstate, d_qim, d_qreg, d_treg, d_modules);
+ d_qmodules->initialize(
+ d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
- return d_qmodules->d_builder.get();
-}
-quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
-{
- return d_model;
+ return d_builder.get();
}
/// !!!!!!!!!!!!!! temporary (project #15)
//---------------------- utilities
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() const;
- /** get model */
- quantifiers::FirstOrderModel* getModel() const;
/** get term database sygus */
quantifiers::TermDbSygus* getTermDatabaseSygus() const;
//---------------------- end utilities
quantifiers::QuantifiersRegistry& d_qreg;
/** The term registry */
quantifiers::TermRegistry& d_treg;
+ /** model builder */
+ std::unique_ptr<quantifiers::QModelBuilder> d_builder;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
//------------- end quantifiers utilities
}
}
+bool TheoryModel::hasUfTerms(Node f) const
+{
+ return d_uf_terms.find(f) != d_uf_terms.end();
+}
+
+const std::vector<Node>& TheoryModel::getUfTerms(Node f) const
+{
+ const auto it = d_uf_terms.find(f);
+ Assert(it != d_uf_terms.end());
+ return it->second;
+}
+
bool TheoryModel::areFunctionValuesEnabled() const
{
return d_enableFuncModels;
Cardinality getCardinality(TypeNode t) const;
//---------------------------- function values
- /** a map from functions f to a list of all APPLY_UF terms with operator f */
- std::map< Node, std::vector< Node > > d_uf_terms;
- /** a map from functions f to a list of all HO_APPLY terms with first argument f */
- std::map< Node, std::vector< Node > > d_ho_uf_terms;
+ /** Does this model have terms for the given uninterpreted function? */
+ bool hasUfTerms(Node f) const;
+ /** Get the terms for uninterpreted function f */
+ const std::vector<Node>& getUfTerms(Node f) const;
/** are function values enabled? */
bool areFunctionValuesEnabled() const;
/** assign function value f to definition f_def */
//---------------------------- end separation logic
//---------------------------- function values
+ /** a map from functions f to a list of all APPLY_UF terms with operator f */
+ std::map<Node, std::vector<Node> > d_uf_terms;
+ /** a map from functions f to a list of all HO_APPLY terms with first argument
+ * f */
+ std::map<Node, std::vector<Node> > d_ho_uf_terms;
/** whether function models are enabled */
bool d_enableFuncModels;
/** map from function terms to the (lambda) definitions
projects / cvc5.git / commitdiff