diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
| commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
| tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) | |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 7bf7cc09b..62f15a6a6 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -37,7 +37,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {} +QuantInfo::QuantInfo() + : d_unassigned_nvar(0), d_una_index(0), d_parent(nullptr), d_mg(nullptr) +{ +} QuantInfo::~QuantInfo() { delete d_mg; @@ -49,8 +52,14 @@ QuantInfo::~QuantInfo() { d_var_mg.clear(); } +QuantifiersInferenceManager& QuantInfo::getInferenceManager() +{ + Assert(d_parent != nullptr); + return d_parent->getInferenceManager(); +} void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { + d_parent = p; d_q = q; d_extra_var.clear(); for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ @@ -588,7 +597,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, } }else{ Node inst = - p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms); + getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); inst = Rewriter::rewrite(inst); Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, options::qcfTConstraint(), true); @@ -2107,7 +2116,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } // try to make a matches making the body false or propagating Trace("qcf-check-debug") << "Get next match..." << std::endl; - Instantiate* qinst = d_quantEngine->getInstantiate(); + Instantiate* qinst = d_qim.getInstantiate(); while (qi->getNextMatch(this)) { if (d_qstate.isInConflict()) |