This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
PreprocessingPassResult SortInferencePass::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference();
+ theory::SortInference* si =
+ d_preprocContext->getTheoryEngine()->getSortInference();
if (options::sortInference())
{
// not have a model builder
if (d_modelBuilder == nullptr)
{
- d_alocModelBuilder.reset(new TheoryEngineModelBuilder(&d_te));
+ d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
d_modelBuilder = d_alocModelBuilder.get();
}
// notice that the equality engine of the model has yet to be assigned.
d_theta.pop_back();
}
-CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent)
+CegInstantiator::CegInstantiator(Node q,
+ QuantifiersState& qs,
+ InstStrategyCegqi* parent)
: d_quant(q),
+ d_qstate(qs),
d_parent(parent),
d_qe(parent->getQuantifiersEngine()),
d_is_nested_quant(false),
}
}
//collect assertions for relevant theories
- for( unsigned i=0; i<d_tids.size(); i++ ){
- TheoryId tid = d_tids[i];
- Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
- if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
- Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl;
- d_curr_asserts[tid].clear();
- //collect all assertions from theory
- for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
- Node lit = (*it).d_assertion;
- Node atom = lit.getKind()==NOT ? lit[0] : lit;
- if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
- d_curr_asserts[tid].push_back( lit );
- Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
- }else{
- Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
- }
+ const LogicInfo& logicInfo = d_qstate.getLogicInfo();
+ for (TheoryId tid : d_tids)
+ {
+ if (!logicInfo.isTheoryEnabled(tid))
+ {
+ continue;
+ }
+ Trace("cegqi-proc") << "Collect assertions from theory " << tid
+ << std::endl;
+ d_curr_asserts[tid].clear();
+ // collect all assertions from theory
+ for (context::CDList<Assertion>::const_iterator
+ it = d_qstate.factsBegin(tid),
+ itEnd = d_qstate.factsEnd(tid);
+ it != itEnd;
+ ++it)
+ {
+ Node lit = (*it).d_assertion;
+ Node atom = lit.getKind() == NOT ? lit[0] : lit;
+ if (d_is_nested_quant
+ || std::find(d_ce_atoms.begin(), d_ce_atoms.end(), atom)
+ != d_ce_atoms.end())
+ {
+ d_curr_asserts[tid].push_back(lit);
+ Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
+ }
+ else
+ {
+ Trace("cegqi-proc")
+ << "...do not consider literal " << tid << " : " << lit
+ << " since it is not part of CE body." << std::endl;
}
}
}
class Instantiator;
class InstantiatorPreprocess;
class InstStrategyCegqi;
+class QuantifiersState;
/**
* Descriptions of the types of constraints that a term was solved for in.
* The instantiator will be constructing instantiations for quantified formula
* q, parent is the owner of this object.
*/
- CegInstantiator(Node q, InstStrategyCegqi* parent);
+ CegInstantiator(Node q, QuantifiersState& qs, InstStrategyCegqi* parent);
virtual ~CegInstantiator();
/** check
* This adds instantiations based on the state of d_vars in current context
private:
/** The quantified formula of this instantiator */
Node d_quant;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
/** The parent of this instantiator */
InstStrategyCegqi* d_parent;
/** quantified formula associated with this instantiator */
std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
d_cinst.find(q);
if( it==d_cinst.end() ){
- d_cinst[q].reset(new CegInstantiator(q, this));
+ d_cinst[q].reset(new CegInstantiator(q, d_qstate, this));
return d_cinst[q].get();
}
return it->second.get();
BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr)
- : QuantifiersModule(qs, qim, qr, qe)
+ QuantifiersRegistry& qr,
+ DecisionManager* dm)
+ : QuantifiersModule(qs, qim, qr, qe), d_dm(dm)
{
}
d_qstate.getUserContext(),
d_qstate.getValuation(),
isProxy));
- d_quantEngine->getTheoryEngine()
- ->getDecisionManager()
- ->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
+ d_dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
d_rms[r].get());
}
}
namespace theory {
class RepSetIterator;
+class DecisionManager;
/**
* Attribute set to 1 for literals that comprise the bounds of a quantified
BoundedIntegers(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr);
+ QuantifiersRegistry& qr,
+ DecisionManager* dm);
virtual ~BoundedIntegers();
void presolve() override;
Node matchBoundVar( Node v, Node t, Node e );
bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
+ /** Pointer to the decision manager */
+ DecisionManager* d_dm;
};
}
using namespace CVC4::theory::quantifiers;
QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs)
- : TheoryEngineModelBuilder(qe->getTheoryEngine()),
+ : TheoryEngineModelBuilder(),
d_qe(qe),
d_addedLemmas(0),
d_triedLemmas(0),
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ DecisionManager* dm,
std::vector<QuantifiersModule*>& modules)
{
// add quantifiers modules
// finite model finding
if (options::fmfBound())
{
- d_bint.reset(new BoundedIntegers(qe, qs, qim, qr));
+ d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, dm));
modules.push_back(d_bint.get());
}
if (options::finiteModelFind() || options::fmfBound())
namespace theory {
class QuantifiersEngine;
+class DecisionManager;
namespace quantifiers {
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ DecisionManager* dm,
std::vector<QuantifiersModule*>& modules);
private:
QuantifiersState::QuantifiersState(context::Context* c,
context::UserContext* u,
- Valuation val)
- : TheoryState(c, u, val), d_ierCounterc(c)
+ Valuation val,
+ const LogicInfo& logicInfo)
+ : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo)
{
// allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
}
}
+const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
class QuantifiersState : public TheoryState
{
public:
- QuantifiersState(context::Context* c, context::UserContext* u, Valuation val);
+ QuantifiersState(context::Context* c,
+ context::UserContext* u,
+ Valuation val,
+ const LogicInfo& logicInfo);
~QuantifiersState() {}
/**
* Increment the instantiation counters, called once at the beginning of when
uint64_t getInstRounds() const;
/** debug print equality engine on trace c */
void debugPrintEqualityEngine(const char* c) const;
+ /** get the logic info */
+ const LogicInfo& getLogicInfo() const;
private:
/** The number of instantiation rounds in this SAT context */
* combination.
*/
uint64_t d_instWhenPhase;
+ /** Information about the logic we're operating within. */
+ const LogicInfo& d_logicInfo;
};
} // namespace quantifiers
#include "theory/quantifiers/skolemize.h"
+#include "expr/dtype.h"
#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
#include "theory/sort_inference.h"
#include "theory/theory_engine.h"
namespace theory {
namespace quantifiers {
-Skolemize::Skolemize(QuantifiersEngine* qe,
- QuantifiersState& qs,
- ProofNodeManager* pnm)
- : d_quantEngine(qe),
+Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm)
+ : d_qstate(qs),
d_skolemized(qs.getUserContext()),
d_pnm(pnm),
d_epg(pnm == nullptr ? nullptr
}
}
Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
- if (options::sortInference())
+ SortInference* si = d_qstate.getSortInference();
+ if (si != nullptr)
{
for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
{
// carry information for sort inference
- d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
- f, f[0][i], d_skolem_constants[f][i]);
+ si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
}
}
return ret;
namespace theory {
-class QuantifiersEngine;
+class SortInference;
namespace quantifiers {
typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
public:
- Skolemize(QuantifiersEngine* qe, QuantifiersState& qs, ProofNodeManager* pnm);
+ Skolemize(QuantifiersState& qs, ProofNodeManager* pnm);
~Skolemize() {}
/** skolemize quantified formula q
* If the return value ret of this function is non-null, then ret is a trust
Node n,
TypeNode ntn,
std::vector<Node>& selfSel);
- /** quantifiers engine that owns this module */
- QuantifiersEngine* d_quantEngine;
+ /** Reference to the quantifiers state */
+ QuantifiersState& d_qstate;
/** quantified formulas that have been skolemized */
NodeNodeMap d_skolemized;
/** map from quantified formulas to the list of skolem constants */
TermDb::TermDb(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- QuantifiersEngine* qe)
- : d_quantEngine(qe),
- d_qstate(qs),
+ QuantifiersRegistry& qr)
+ : d_qstate(qs),
d_qim(qim),
d_qreg(qr),
d_termsContext(),
}
++eqcs_i;
}
- TheoryEngine* te = d_quantEngine->getTheoryEngine();
- const LogicInfo& logicInfo = te->getLogicInfo();
+ const LogicInfo& logicInfo = d_qstate.getLogicInfo();
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
{
if (!logicInfo.isTheoryEnabled(theoryId))
{
continue;
}
- Theory* theory = te->theoryOf(theoryId);
- Assert(theory != nullptr);
for (context::CDList<Assertion>::const_iterator
- it = theory->facts_begin(),
- it_end = theory->facts_end();
+ it = d_qstate.factsBegin(theoryId),
+ it_end = d_qstate.factsEnd(theoryId);
it != it_end;
++it)
{
public:
TermDb(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr,
- QuantifiersEngine* qe);
+ QuantifiersRegistry& qr);
~TermDb();
/** presolve (called once per user check-sat) */
void presolve();
Node getHoTypeMatchPredicate(TypeNode tn);
private:
- /** reference to the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
/** The quantifiers state object */
QuantifiersState& d_qstate;
/** The quantifiers inference manager */
const LogicInfo& logicInfo,
ProofNodeManager* pnm)
: Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
- d_qstate(c, u, valuation),
+ d_qstate(c, u, valuation, logicInfo),
d_qim(*this, d_qstate, pnm),
d_qengine(d_qstate, d_qim, pnm)
{
d_qim(qim),
d_te(nullptr),
d_decManager(nullptr),
+ d_pnm(pnm),
d_qreg(),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_builder(nullptr),
- d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
+ d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg)),
d_eq_query(nullptr),
d_sygus_tdb(nullptr),
d_instantiate(
new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
- d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
+ d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
d_term_enum(new quantifiers::TermEnumeration),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext()),
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_qreg, d_modules);
+ d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, dm, d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
}
}
-TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
-
DecisionManager* QuantifiersEngine::getDecisionManager()
{
return d_decManager;
}
if( Trace.isOn("quant-engine-assert") ){
Trace("quant-engine-assert") << "Assertions : " << std::endl;
- getTheoryEngine()->printAssertions("quant-engine-assert");
+ d_te->printAssertions("quant-engine-assert");
}
//reset utilities
ProofNodeManager* pnm);
~QuantifiersEngine();
//---------------------- external interface
- /** get theory engine */
- TheoryEngine* getTheoryEngine() const;
/** Get the decision manager */
DecisionManager* getDecisionManager();
/** The quantifiers state object */
TheoryEngine* d_te;
/** Reference to the decision manager of the theory engine */
DecisionManager* d_decManager;
+ /** Pointer to the proof node manager */
+ ProofNodeManager* d_pnm;
/** vector of utilities for quantifiers */
std::vector<QuantifiersUtil*> d_util;
/** vector of modules for quantifiers */
using namespace std;
namespace CVC4 {
+namespace theory {
void SortInference::UnionFind::print(const char * c){
for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){
return k == APPLY_UF && !options::ufHo();
}
-}/* CVC4 namespace */
+} // namespace theory
+} // namespace CVC4
#include "expr/type_node.h"
namespace CVC4 {
+namespace theory {
/** sort inference
*
bool isHandledApplyUf(Kind k) const;
};
+} // namespace theory
}
#endif
d_theoryOut[theoryId] = NULL;
}
+ if (options::sortInference())
+ {
+ d_sortInfer.reset(new SortInference);
+ }
+
smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
/** sort inference module */
- SortInference d_sortInfer;
+ std::unique_ptr<theory::SortInference> d_sortInfer;
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
public:
+ theory::SortInference* getSortInference() { return d_sortInfer.get(); }
- SortInference* getSortInference() { return &d_sortInfer; }
-
- /** Prints the assertions to the debug stream */
- void printAssertions(const char* tag);
+ /** Prints the assertions to the debug stream */
+ void printAssertions(const char* tag);
private:
#include "expr/dtype.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
+#include "options/theory_options.h"
#include "options/uf_options.h"
-#include "theory/theory_engine.h"
#include "theory/uf/theory_uf_model.h"
using namespace std;
return n;
}
-TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
-{
-}
+TheoryEngineModelBuilder::TheoryEngineModelBuilder() {}
Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
{
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
public:
- TheoryEngineModelBuilder(TheoryEngine* te);
+ TheoryEngineModelBuilder();
virtual ~TheoryEngineModelBuilder() {}
/**
* Should be called only on models m after they have been prepared
void postProcessModel(bool incomplete, TheoryModel* m);
protected:
- /** pointer to theory engine */
- TheoryEngine* d_te;
//-----------------------------------virtual functions
/** pre-process build model
TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
+SortInference* TheoryState::getSortInference()
+{
+ return d_valuation.getSortInference();
+}
+
bool TheoryState::hasSatValue(TNode n, bool& value) const
{
return d_valuation.hasSatValue(n, value);
}
+context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
+{
+ return d_valuation.factsBegin(tid);
+}
+context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
+{
+ return d_valuation.factsEnd(tid);
+}
+
Valuation& TheoryState::getValuation() { return d_valuation; }
} // namespace theory
* check.
*/
TheoryModel* getModel();
+ /**
+ * Returns a pointer to the sort inference module, which lives in TheoryEngine
+ * and is non-null when options::sortInference is true.
+ */
+ SortInference* getSortInference();
/** Returns true if n has a current SAT assignment and stores it in value. */
virtual bool hasSatValue(TNode n, bool& value) const;
+ //------------------------------------------- access methods for assertions
+ /**
+ * The following methods are intended only to be used in limited use cases,
+ * for cases where a theory (e.g. quantifiers) requires knowing about the
+ * assertions from other theories.
+ */
+ /** The beginning iterator of facts for theory tid.*/
+ context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
+ /** The beginning iterator of facts for theory tid.*/
+ context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
+
/** Get the underlying valuation class */
Valuation& getValuation();
Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
Trace("uf-ss-si") << "Must combine region" << std::endl;
bool recheck = false;
- SortInference* si = d_thss->getSortInference();
+ SortInference* si = d_state.getSortInference();
if (si != nullptr)
{
// If sort inference is enabled, search for regions with same sort.
AlwaysAssert(false);
}
}
- SortInference* si = d_thss->getSortInference();
- if (si != nullptr)
+ if (Trace.isOn("uf-ss-split-si"))
{
- for( int i=0; i<2; i++ ){
- int sid = si->getSortId(ss[i]);
- Trace("uf-ss-split-si") << sid << " ";
+ SortInference* si = d_state.getSortInference();
+ if (si != nullptr)
+ {
+ for (size_t i = 0; i < 2; i++)
+ {
+ int sid = si->getSortId(ss[i]);
+ Trace("uf-ss-split-si") << sid << " ";
+ }
+ Trace("uf-ss-split-si") << std::endl;
}
- Trace("uf-ss-split-si") << std::endl;
}
//Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
//Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
}
}
-SortInference* CardinalityExtension::getSortInference()
-{
- if (!options::sortInference())
- {
- return nullptr;
- }
- QuantifiersEngine* qe = d_th->getQuantifiersEngine();
- if (qe != nullptr)
- {
- return qe->getTheoryEngine()->getSortInference();
- }
- return nullptr;
-}
-
/** ensure eqc */
void CardinalityExtension::ensureEqc(SortModel* c, Node a)
{
Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
if( lit[0]==ct ){
if( options::ufssFairnessMonotone() ){
+ SortInference* si = d_state.getSortInference();
Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
if( tn!=d_tn_mono_master ){
std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
if( it==d_tn_mono_slave.end() ){
bool isMonotonic;
- SortInference* si = getSortInference();
if (si != nullptr)
{
isMonotonic = si->isMonotonic(tn);
#include "theory/decision_manager.h"
namespace CVC4 {
-
-class SortInference;
-
namespace theory {
namespace uf {
~CardinalityExtension();
/** get theory */
TheoryUF* getTheory() { return d_th; }
- /** get sort inference module */
- SortInference* getSortInference();
/** new node */
void newEqClass( Node n );
/** merge */
}
return d_engine->getModel();
}
+SortInference* Valuation::getSortInference()
+{
+ if (d_engine == nullptr)
+ {
+ // no theory engine, thus we don't have a sort inference object
+ return nullptr;
+ }
+ return d_engine->getSortInference();
+}
void Valuation::setUnevaluatedKind(Kind k)
{
bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
+context::CDList<Assertion>::const_iterator Valuation::factsBegin(TheoryId tid)
+{
+ Theory* theory = d_engine->theoryOf(tid);
+ Assert(theory != nullptr);
+ return theory->facts_begin();
+}
+context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid)
+{
+ Theory* theory = d_engine->theoryOf(tid);
+ Assert(theory != nullptr);
+ return theory->facts_end();
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#ifndef CVC4__THEORY__VALUATION_H
#define CVC4__THEORY__VALUATION_H
+#include "context/cdlist.h"
#include "expr/node.h"
#include "options/theory_options.h"
+#include "theory/assertion.h"
namespace CVC4 {
namespace theory {
class TheoryModel;
+class SortInference;
/**
* The status of an equality in the current context.
* check.
*/
TheoryModel* getModel();
+ /**
+ * Returns a pointer to the sort inference module, which lives in TheoryEngine
+ * and is non-null when options::sortInference is true.
+ */
+ SortInference* getSortInference();
//-------------------------------------- static configuration of the model
/**
* or during LAST_CALL effort.
*/
bool isRelevant(Node lit) const;
+
+ //------------------------------------------- access methods for assertions
+ /**
+ * The following methods are intended only to be used in limited use cases,
+ * for cases where a theory (e.g. quantifiers) requires knowing about the
+ * assertions from other theories.
+ */
+ /** The beginning iterator of facts for theory tid.*/
+ context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
+ /** The beginning iterator of facts for theory tid.*/
+ context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
};/* class Valuation */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff