From 064bce0045368fd74beee10f3545899de2d20bf9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Mar 2021 10:00:33 -0500 Subject: [PATCH] Eliminate use of quantifiers engine in enumerative instantiation (#6217) This also makes minor updates to how term tuple enumerators are constructed. --- .../quantifiers/inst_strategy_enumerative.cpp | 14 ++-- .../quantifiers/term_tuple_enumerator.cpp | 69 ++++++++++--------- .../quantifiers/term_tuple_enumerator.h | 43 +++++++----- 3 files changed, 71 insertions(+), 55 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 007c37b20..9517f1ab0 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -20,7 +20,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_tuple_enumerator.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace CVC4::context; @@ -109,7 +108,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) // at effort level r=0 but another quantified formula does). We prefer // this stratification since effort level r=1 may be highly expensive in the // case where we have a quantified formula with many entailed instances. - FirstOrderModel* fm = d_quantEngine->getModel(); + FirstOrderModel* fm = d_treg.getModel(); unsigned nquant = fm->getNumAssertedQuantifiers(); std::map alreadyProc; for (unsigned r = rstart; r <= rend; r++) @@ -182,14 +181,15 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) return false; } - TermTupleEnumeratorContext ttec; - ttec.d_quantEngine = d_quantEngine; - ttec.d_rd = d_rd; + TermTupleEnumeratorEnv ttec; ttec.d_fullEffort = fullEffort; ttec.d_increaseSum = options::fullSaturateSum(); - ttec.d_isRd = isRd; + // make the enumerator, which is either relevant domain or term database + // based on the flag isRd. std::unique_ptr enumerator( - mkTermTupleEnumerator(quantifier, &ttec)); + isRd ? mkTermTupleEnumeratorRd(quantifier, &ttec, d_rd) + : mkTermTupleEnumerator( + quantifier, &ttec, d_qstate, d_treg.getTermDatabase())); std::vector terms; std::vector failMask; Instantiate* ie = d_qim.getInstantiate(); diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 190e51c54..3ce725255 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -83,11 +83,10 @@ class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface { public: /** Initialize the class with the quantifier to be instantiated. */ - TermTupleEnumeratorBase(Node quantifier, - const TermTupleEnumeratorContext* context) + TermTupleEnumeratorBase(Node quantifier, const TermTupleEnumeratorEnv* env) : d_quantifier(quantifier), d_variableCount(d_quantifier[0].getNumChildren()), - d_context(context), + d_env(env), d_stepCounter(0), d_disabledCombinations( true) // do not record combinations with no blanks @@ -110,8 +109,8 @@ class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface const Node d_quantifier; /** number of variables in the quantifier */ const size_t d_variableCount; - /** context of structures with a longer lifespan */ - const TermTupleEnumeratorContext* const d_context; + /** env of structures with a longer lifespan */ + const TermTupleEnumeratorEnv* const d_env; /** type for each variable */ std::vector d_typeCache; /** number of candidate terms for each variable */ @@ -165,8 +164,10 @@ class TermTupleEnumeratorBasic : public TermTupleEnumeratorBase { public: TermTupleEnumeratorBasic(Node quantifier, - const TermTupleEnumeratorContext* context) - : TermTupleEnumeratorBase(quantifier, context) + const TermTupleEnumeratorEnv* env, + QuantifiersState& qs, + TermDb* td) + : TermTupleEnumeratorBase(quantifier, env), d_qs(qs), d_tdb(td) { } @@ -177,6 +178,10 @@ class TermTupleEnumeratorBasic : public TermTupleEnumeratorBase std::map > d_termDbList; virtual size_t prepareTerms(size_t variableIx) override; virtual Node getTerm(size_t variableIx, size_t term_index) override; + /** Reference to quantifiers state */ + QuantifiersState& d_qs; + /** Pointer to term database */ + TermDb* d_tdb; }; /** @@ -186,8 +191,9 @@ class TermTupleEnumeratorRD : public TermTupleEnumeratorBase { public: TermTupleEnumeratorRD(Node quantifier, - const TermTupleEnumeratorContext* context) - : TermTupleEnumeratorBase(quantifier, context) + const TermTupleEnumeratorEnv* env, + RelevantDomain* rd) + : TermTupleEnumeratorBase(quantifier, env), d_rd(rd) { } virtual ~TermTupleEnumeratorRD() = default; @@ -195,25 +201,16 @@ class TermTupleEnumeratorRD : public TermTupleEnumeratorBase protected: virtual size_t prepareTerms(size_t variableIx) override { - return d_context->d_rd->getRDomain(d_quantifier, variableIx) - ->d_terms.size(); + return d_rd->getRDomain(d_quantifier, variableIx)->d_terms.size(); } virtual Node getTerm(size_t variableIx, size_t term_index) override { - return d_context->d_rd->getRDomain(d_quantifier, variableIx) - ->d_terms[term_index]; + return d_rd->getRDomain(d_quantifier, variableIx)->d_terms[term_index]; } + /** The relevant domain */ + RelevantDomain* d_rd; }; -TermTupleEnumeratorInterface* mkTermTupleEnumerator( - Node quantifier, const TermTupleEnumeratorContext* context) -{ - return context->d_isRd ? static_cast( - new TermTupleEnumeratorRD(quantifier, context)) - : static_cast( - new TermTupleEnumeratorBasic(quantifier, context)); -} - void TermTupleEnumeratorBase::init() { Trace("inst-alg-rd") << "Initializing enumeration " << d_quantifier @@ -236,7 +233,7 @@ void TermTupleEnumeratorBase::init() const size_t termsSize = prepareTerms(variableIx); Trace("inst-alg-rd") << "Variable " << variableIx << " has " << termsSize << " in relevant domain." << std::endl; - if (termsSize == 0 && !d_context->d_fullEffort) + if (termsSize == 0 && !d_env->d_fullEffort) { d_hasNext = false; return; // give up on an empty dommain @@ -320,7 +317,7 @@ bool TermTupleEnumeratorBase::increaseStageSum() bool TermTupleEnumeratorBase::increaseStage() { d_changePrefix = d_variableCount; // simply reset upon increase stage - return d_context->d_increaseSum ? increaseStageSum() : increaseStageMax(); + return d_env->d_increaseSum ? increaseStageSum() : increaseStageMax(); } bool TermTupleEnumeratorBase::increaseStageMax() @@ -367,7 +364,7 @@ bool TermTupleEnumeratorBase::nextCombination() /** Move onto the next combination, depending on the strategy. */ bool TermTupleEnumeratorBase::nextCombinationInternal() { - return d_context->d_increaseSum ? nextCombinationSum() : nextCombinationMax(); + return d_env->d_increaseSum ? nextCombinationSum() : nextCombinationMax(); } /** Find the next lexicographically smallest combination of terms that change @@ -462,20 +459,17 @@ bool TermTupleEnumeratorBase::nextCombinationSum() size_t TermTupleEnumeratorBasic::prepareTerms(size_t variableIx) { - TermDb* const tdb = d_context->d_quantEngine->getTermDatabase(); - QuantifiersState& qs = d_context->d_quantEngine->getState(); const TypeNode type_node = d_typeCache[variableIx]; - if (!ContainsKey(d_termDbList, type_node)) { - const size_t ground_terms_count = tdb->getNumTypeGroundTerms(type_node); + const size_t ground_terms_count = d_tdb->getNumTypeGroundTerms(type_node); std::map repsFound; for (size_t j = 0; j < ground_terms_count; j++) { - Node gt = tdb->getTypeGroundTerm(type_node, j); + Node gt = d_tdb->getTypeGroundTerm(type_node, j); if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) { - Node rep = qs.getRepresentative(gt); + Node rep = d_qs.getRepresentative(gt); if (repsFound.find(rep) == repsFound.end()) { repsFound[rep] = gt; @@ -497,6 +491,19 @@ Node TermTupleEnumeratorBasic::getTerm(size_t variableIx, size_t term_index) return d_termDbList[type_node][term_index]; } +TermTupleEnumeratorInterface* mkTermTupleEnumerator( + Node q, const TermTupleEnumeratorEnv* env, QuantifiersState& qs, TermDb* td) +{ + return static_cast( + new TermTupleEnumeratorBasic(q, env, qs, td)); +} +TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( + Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd) +{ + return static_cast( + new TermTupleEnumeratorRD(q, env, rd)); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h index bd3297101..28831baf5 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.h +++ b/src/theory/quantifiers/term_tuple_enumerator.h @@ -20,17 +20,16 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { +class QuantifiersState; +class TermDb; class RelevantDomain; /** Interface for enumeration of tuples of terms. * * The interface should be used as follows. Firstly, init is called, then, - * repeatedly, verify if there are any combinations left by calling hasNext + * repeatedly, verify if there are any combinations left by calling hasNext * and obtaining the next combination by calling next. * * Optionally, if the most recent combination is determined to be undesirable @@ -53,35 +52,45 @@ class TermTupleEnumeratorInterface }; /** A struct bundling up parameters for term tuple enumerator.*/ -struct TermTupleEnumeratorContext +struct TermTupleEnumeratorEnv { - QuantifiersEngine* d_quantEngine; - RelevantDomain* d_rd; + /** + * Whether we should put full effort into finding an instantiation. If this + * is false, then we allow for incompleteness, e.g. the tuple enumerator + * may heuristically give up before it has generated all tuples. + */ bool d_fullEffort; + /** Whether we increase tuples based on sum instead of max (see below) */ bool d_increaseSum; - bool d_isRd; }; /** A function to construct a tuple enumerator. * - * Currently we support the enumerators based on the following idea. + * In the methods below, we support the enumerators based on the following idea. * The tuples are represented as tuples of * indices of terms, where the tuple has as many elements as there are - * quantified variables in the considered quantifier. + * quantified variables in the considered quantifier q. * * Like so, we see a tuple as a number, where the digits may have different * ranges. The most significant digits are stored first. * - * Tuples are enumerated in a lexicographic order in stages. There are 2 - * possible strategies, either all tuples in a given stage have the same sum of - * digits, or, the maximum over these digits is the same (controlled by - * d_increaseSum). + * Tuples are enumerated in a lexicographic order in stages. There are 2 + * possible strategies, either all tuples in a given stage have the same sum of + * digits, or, the maximum over these digits is the same (controlled by + * TermTupleEnumeratorEnv::d_increaseSum). * - * Further, an enumerator either draws ground terms from the term database or - * using the relevant domain class (controlled by d_isRd). + * In this method, the returned enumerator draws ground terms from the term + * database (provided by td). The quantifiers state (qs) is used to eliminate + * duplicates modulo equality. */ TermTupleEnumeratorInterface* mkTermTupleEnumerator( - Node quantifier, const TermTupleEnumeratorContext* context); + Node q, + const TermTupleEnumeratorEnv* env, + QuantifiersState& qs, + TermDb* td); +/** Same as above, but draws terms from the relevant domain utility (rd). */ +TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( + Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd); } // namespace quantifiers } // namespace theory -- 2.30.2