diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 13:34:54 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-17 13:34:54 -0600 |
| commit | 0f03dbb1378354adcfef635a93f8b13987c2d983 (patch) | |
| tree | 6c6dcc0e806b0867d19d01cb045a5a50764bf0e0 /src/theory/quantifiers/term_database.cpp | |
| parent | d107bf9b8b4dd206580681e601a033742029ec79 (diff) | |
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 61a62a820..28eb715a3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -36,10 +36,12 @@ namespace quantifiers { TermDb::TermDb(QuantifiersState& qs, QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, QuantifiersEngine* qe) : d_quantEngine(qe), d_qstate(qs), d_qim(qim), + d_qreg(qr), d_termsContext(), d_termsContextUse(options::termDbCd() ? qs.getSatContext() : &d_termsContext), @@ -65,10 +67,10 @@ TermDb::~TermDb(){ } void TermDb::registerQuantifier( Node q ) { - Assert(q[0].getNumChildren() - == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q)); - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); + Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q)); + for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) + { + Node ic = d_qreg.getInstantiationConstant(q, i); setTermInactive( ic ); } } @@ -688,10 +690,10 @@ Node TermDb::evaluateTerm2(TNode n, { if (ret.getKind() == EQUAL || ret.getKind() == GEQ) { - TheoryEngine* te = d_quantEngine->getTheoryEngine(); + Valuation& val = d_qstate.getValuation(); for (unsigned j = 0; j < 2; j++) { - std::pair<bool, Node> et = te->entailmentCheck( + std::pair<bool, Node> et = val.entailmentCheck( options::TheoryOfMode::THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate()); if (et.first) |