This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
theory/quantifiers/quantifiers_inference_manager.h
theory/quantifiers/quantifiers_modules.cpp
theory/quantifiers/quantifiers_modules.h
+ theory/quantifiers/quantifiers_registry.cpp
+ theory/quantifiers/quantifiers_registry.h
theory/quantifiers/quantifiers_rewriter.cpp
theory/quantifiers/quantifiers_rewriter.h
theory/quantifiers/quantifiers_state.cpp
InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_irew(new InstRewriterCegqi(this)),
d_cbqi_set_quant_inactive(false),
d_incomplete_check(false),
void InstStrategyCegqi::checkOwnership(Node q)
{
- if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+ if (d_qreg.getOwner(q) == nullptr && doCbqi(q))
+ {
if (d_do_cbqi[q] == CEG_HANDLED)
{
//take full ownership of the quantified formula
- d_quantEngine->setOwner( q, this );
+ d_qreg.setOwner(q, this);
}
}
}
public:
InstStrategyCegqi(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~InstStrategyCegqi();
/** whether to do counterexample-guided instantiation for quantifier q */
ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_notify(*this),
d_uequalityEngine(
d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false),
public:
ConjectureGenerator(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~ConjectureGenerator();
/* needs check */
InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_instStrategies(),
d_isup(),
d_i_ag(),
}
}
if( hasPat ){
- d_quantEngine->setOwner( q, this, 1 );
+ d_qreg.setOwner(q, this, 1);
}
}
}
bool InstantiationEngine::shouldProcess(Node q)
{
- if (!d_quantEngine->hasOwnership(q, this))
+ if (!d_qreg.hasOwnership(q, this))
{
return false;
}
public:
InstantiationEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~InstantiationEngine();
void presolve() override;
bool needsCheck(Theory::Effort e) override;
BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe)
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe)
{
}
public:
BoundedIntegers(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
virtual ~BoundedIntegers();
void presolve() override;
//Model Engine constructor
ModelEngine::ModelEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_incomplete_check(true),
d_addedLemmas(0),
d_triedLemmas(0),
if( Trace.isOn("model-engine") ){
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
- if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){
+ if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this))
+ {
int totalInst = 1;
for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
TypeNode tn = f[0][j].getType();
Node q = fm->getAssertedQuantifier( i, true );
Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
//determine if we should check this quantifier
- if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
+ if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this))
+ {
exhaustiveInstantiate( q, e );
if (d_qstate.isInConflict())
{
Trace( c ) << "Quantifiers: " << std::endl;
for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- if( d_quantEngine->hasOwnership( q, this ) ){
+ if (d_qreg.hasOwnership(q, this))
+ {
Trace( c ) << " ";
if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
Trace( c ) << "*Inactive* ";
public:
ModelEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
virtual ~ModelEngine();
public:
InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
RelevantDomain* rd)
- : QuantifiersModule(qs, qim, qe), d_rd(rd), d_fullSaturateLimit(-1)
+ : QuantifiersModule(qs, qim, qr, qe), d_rd(rd), d_fullSaturateLimit(-1)
{
}
void InstStrategyEnum::presolve()
for (unsigned i = 0; i < nquant; i++)
{
Node q = fm->getAssertedQuantifier(i, true);
- bool doProcess = d_quantEngine->hasOwnership(q, this)
+ bool doProcess = d_qreg.hasOwnership(q, this)
&& fm->isQuantifierActive(q)
&& alreadyProc.find(q) == alreadyProc.end();
if (doProcess)
InstStrategyEnum(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
RelevantDomain* rd);
~InstStrategyEnum() {}
/** Presolve */
QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_conflict(qs.getSatContext(), false),
d_true(NodeManager::currentNM()->mkConst<bool>(true)),
d_false(NodeManager::currentNM()->mkConst<bool>(false)),
//-------------------------------------------------- registration
void QuantConflictFind::registerQuantifier( Node q ) {
- if( d_quantEngine->hasOwnership( q, this ) ){
+ if (d_qreg.hasOwnership(q, this))
+ {
d_quants.push_back( q );
d_quant_id[q] = d_quants.size();
if( Trace.isOn("qcf-qregister") ){
for (unsigned i = 0; i < nquant; i++)
{
Node q = fm->getAssertedQuantifier(i, true);
- if (d_quantEngine->hasOwnership(q, this)
+ if (d_qreg.hasOwnership(q, this)
&& d_irr_quant.find(q) == d_irr_quant.end()
&& fm->isQuantifierActive(q))
{
public:
QuantConflictFind(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
/** register quantifier */
void registerQuantifier(Node q) override;
QuantDSplit::QuantDSplit(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe), d_added_split(qs.getUserContext())
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe), d_added_split(qs.getUserContext())
{
}
if (takeOwnership)
{
Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
- d_quantEngine->setOwner( q, this );
+ d_qreg.setOwner(q, this);
}
// Notice we may not take ownership in some cases, meaning that both the
// original quantified formula and the split one are generated. This may
public:
QuantDSplit(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
/** determine whether this quantified formula will be reduced */
void checkOwnership(Node q) override;
/* whether this module needs to check this round */
QuantifiersModule::QuantifiersModule(
quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
QuantifiersEngine* qe)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
{
}
#include <vector>
#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
public:
QuantifiersModule(quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
QuantifiersEngine* qe);
virtual ~QuantifiersModule(){}
/** Presolve.
quantifiers::QuantifiersState& d_qstate;
/** The quantifiers inference manager */
quantifiers::QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ quantifiers::QuantifiersRegistry& d_qreg;
};/* class QuantifiersModule */
/** Quantifiers utility
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
using namespace std;
using namespace CVC4::kind;
&& !d_isInternal;
}
-QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) :
-d_quantEngine(qe) {
+QuantAttributes::QuantAttributes() {}
-}
-
void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
if (attr == "fun-def")
}
d_fun_defs[f] = true;
}
- // set ownership of quantified formula q based on the computed attributes
- d_quantEngine->setOwner(q, qa);
}
void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
-
/** Attribute true for function definition quantifiers */
struct FunDefAttributeId {};
typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
*/
class QuantAttributes
{
-public:
- QuantAttributes( QuantifiersEngine * qe );
+ public:
+ QuantAttributes();
~QuantAttributes(){}
/** set user attribute
* This function applies an attribute
static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level);
private:
- /** pointer to quantifiers engine */
- QuantifiersEngine * d_quantEngine;
/** cache of attributes */
std::map< Node, QAttributes > d_qattr;
/** function definitions */
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())
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());
}
}
void initialize(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
std::vector<QuantifiersModule*>& modules);
private:
--- /dev/null
+/********************* */
+/*! \file quantifiers_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The quantifiers registry
+ **/
+
+#include "theory/quantifiers/quantifiers_registry.h"
+
+#include "theory/quantifiers/quant_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
+{
+ std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
+ if (it == d_owner.end())
+ {
+ return nullptr;
+ }
+ return it->second;
+}
+
+void QuantifiersRegistry::setOwner(Node q,
+ QuantifiersModule* m,
+ int32_t priority)
+{
+ QuantifiersModule* mo = getOwner(q);
+ if (mo == m)
+ {
+ return;
+ }
+ if (mo != nullptr)
+ {
+ if (priority <= d_owner_priority[q])
+ {
+ Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
+ << (m ? m->identify() : "null")
+ << ", but already has owner " << mo->identify()
+ << " with higher priority!" << std::endl;
+ return;
+ }
+ }
+ d_owner[q] = m;
+ d_owner_priority[q] = priority;
+}
+
+bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
+{
+ QuantifiersModule* mo = getOwner(q);
+ return mo == m || mo == nullptr;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file quantifiers_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The quantifiers registry
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersModule;
+
+namespace quantifiers {
+
+/**
+ * The quantifiers registry, which manages basic information about which
+ * quantifiers modules have ownership of quantified formulas.
+ */
+class QuantifiersRegistry
+{
+ public:
+ QuantifiersRegistry() {}
+ ~QuantifiersRegistry() {}
+ /** get the owner of quantified formula q */
+ QuantifiersModule* getOwner(Node q) const;
+ /**
+ * Set owner of quantified formula q to module m with given priority. If
+ * the quantified formula has previously been assigned an owner with
+ * lower priority, that owner is overwritten.
+ */
+ void setOwner(Node q, QuantifiersModule* m, int32_t priority = 0);
+ /**
+ * Return true if module q has no owner registered or if its registered owner is m.
+ */
+ bool hasOwnership(Node q, QuantifiersModule* m) const;
+
+ private:
+ /**
+ * Maps quantified formulas to the module that owns them, if any module has
+ * specifically taken ownership of it.
+ */
+ std::map<Node, QuantifiersModule*> d_owner;
+ /**
+ * The priority value associated with the ownership of quantified formulas
+ * in the domain of the above map, where higher values take higher
+ * precendence.
+ */
+ std::map<Node, int32_t> d_owner_priority;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
SynthEngine::SynthEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_tds(qe->getTermDatabaseSygus()),
d_conj(nullptr),
d_sqp(qe)
d_conjs.back()->assign(q);
}
+void SynthEngine::checkOwnership(Node q)
+{
+ // take ownership of quantified formulas with sygus attribute, and function
+ // definitions when options::sygusRecFun is true.
+ QuantAttributes* qa = d_quantEngine->getQuantAttributes();
+ if (qa->isSygus(q) || (options::sygusRecFun() && qa->isFunDef(q)))
+ {
+ d_qreg.setOwner(q, this, 2);
+ }
+}
+
void SynthEngine::registerQuantifier(Node q)
{
Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
<< std::endl;
- if (d_quantEngine->getOwner(q) != this)
+ if (d_qreg.getOwner(q) != this)
{
return;
}
public:
SynthEngine(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~SynthEngine();
/** presolve
*
QEffort needsModel(Theory::Effort e) override;
/* Call during quantifier engine's check */
void check(Theory::Effort e, QEffort quant_e) override;
+ /** check ownership */
+ void checkOwnership(Node q) override;
/* Called for new quantifiers */
void registerQuantifier(Node q) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
SygusInst::SygusInst(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : QuantifiersModule(qs, qim, qe),
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : QuantifiersModule(qs, qim, qr, qe),
d_ce_lemma_added(qs.getUserContext()),
d_global_terms(qs.getUserContext()),
d_notified_assertions(qs.getUserContext())
public:
SygusInst(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~SygusInst() = default;
bool needsCheck(Theory::Effort e) override;
d_qim(qim),
d_te(nullptr),
d_decManager(nullptr),
+ d_qreg(),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
d_term_db(new quantifiers::TermDb(qstate, qim, this)),
d_eq_query(nullptr),
d_sygus_tdb(nullptr),
- d_quant_attr(new quantifiers::QuantAttributes(this)),
+ d_quant_attr(new quantifiers::QuantAttributes),
d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)),
d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
d_term_enum(new quantifiers::TermEnumeration),
d_decManager = dm;
// Initialize the modules and the utilities here.
d_qmodules.reset(new quantifiers::QuantifiersModules);
- d_qmodules->initialize(this, d_qstate, d_qim, d_modules);
+ d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
return d_tr_trie.get();
}
-QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
- std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
- if( it==d_owner.end() ){
- return NULL;
- }else{
- return it->second;
- }
-}
-
-void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
- QuantifiersModule * mo = getOwner( q );
- if( mo!=m ){
- if( mo!=NULL ){
- if( priority<=d_owner_priority[q] ){
- Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
- return;
- }
- }
- d_owner[q] = m;
- d_owner_priority[q] = priority;
- }
-}
-
-void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
-{
- if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
- {
- if (d_qmodules->d_synth_e.get() == nullptr)
- {
- Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
- << q << std::endl;
- }
- // set synth engine as owner since this is either a conjecture or a function
- // definition to be used by sygus
- setOwner(q, d_qmodules->d_synth_e.get(), 2);
- }
-}
-
-bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
- QuantifiersModule * mo = getOwner( q );
- return mo==m || mo==NULL;
-}
-
bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
{
quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
bool hasCompleteM = false;
Node q = d_model->getAssertedQuantifier( i );
- QuantifiersModule * qmd = getOwner( q );
+ QuantifiersModule* qmd = d_qreg.getOwner(q);
if( qmd!=NULL ){
hasCompleteM = qmd->checkCompleteFor( q );
}else{
<< "..." << std::endl;
mdl->checkOwnership(f);
}
- QuantifiersModule* qm = getOwner(f);
+ QuantifiersModule* qm = d_qreg.getOwner(f);
Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
<< std::endl;
// register with each module
*/
void finishInit(TheoryEngine* te, DecisionManager* dm);
//---------------------- end private initialization
- /**
- * Maps quantified formulas to the module that owns them, if any module has
- * specifically taken ownership of it.
- */
- std::map< Node, QuantifiersModule * > d_owner;
- /**
- * The priority value associated with the ownership of quantified formulas
- * in the domain of the above map, where higher values take higher
- * precendence.
- */
- std::map< Node, int > d_owner_priority;
public:
- /** get owner */
- QuantifiersModule * getOwner( Node q );
- /**
- * Set owner of quantified formula q to module m with given priority. If
- * the quantified formula has previously been assigned an owner with
- * lower priority, that owner is overwritten.
- */
- void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
- /** set owner of quantified formula q based on its attributes qa. */
- void setOwner(Node q, quantifiers::QAttributes& qa);
- /** considers */
- bool hasOwnership( Node q, QuantifiersModule * m = NULL );
/** does variable v of quantified formula q have a finite bound? */
bool isFiniteBound(Node q, Node v) const;
/** get bound var type
/** vector of modules for quantifiers */
std::vector<QuantifiersModule*> d_modules;
//------------- quantifiers utilities
+ /** The quantifiers registry */
+ quantifiers::QuantifiersRegistry d_qreg;
/** all triggers will be stored in this trie */
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
projects / cvc5.git / commitdiff