#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;
// 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<Node, bool> alreadyProc;
for (unsigned r = rstart; r <= rend; r++)
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<TermTupleEnumeratorInterface> enumerator(
- mkTermTupleEnumerator(quantifier, &ttec));
+ isRd ? mkTermTupleEnumeratorRd(quantifier, &ttec, d_rd)
+ : mkTermTupleEnumerator(
+ quantifier, &ttec, d_qstate, d_treg.getTermDatabase()));
std::vector<Node> terms;
std::vector<bool> failMask;
Instantiate* ie = d_qim.getInstantiate();
{
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
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<TypeNode> d_typeCache;
/** number of candidate terms for each variable */
{
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)
{
}
std::map<TypeNode, std::vector<Node> > 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;
};
/**
{
public:
TermTupleEnumeratorRD(Node quantifier,
- const TermTupleEnumeratorContext* context)
- : TermTupleEnumeratorBase(quantifier, context)
+ const TermTupleEnumeratorEnv* env,
+ RelevantDomain* rd)
+ : TermTupleEnumeratorBase(quantifier, env), d_rd(rd)
{
}
virtual ~TermTupleEnumeratorRD() = default;
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<TermTupleEnumeratorInterface*>(
- new TermTupleEnumeratorRD(quantifier, context))
- : static_cast<TermTupleEnumeratorInterface*>(
- new TermTupleEnumeratorBasic(quantifier, context));
-}
-
void TermTupleEnumeratorBase::init()
{
Trace("inst-alg-rd") << "Initializing enumeration " << d_quantifier
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
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()
/** 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
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<Node, Node> 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;
return d_termDbList[type_node][term_index];
}
+TermTupleEnumeratorInterface* mkTermTupleEnumerator(
+ Node q, const TermTupleEnumeratorEnv* env, QuantifiersState& qs, TermDb* td)
+{
+ return static_cast<TermTupleEnumeratorInterface*>(
+ new TermTupleEnumeratorBasic(q, env, qs, td));
+}
+TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
+ Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd)
+{
+ return static_cast<TermTupleEnumeratorInterface*>(
+ new TermTupleEnumeratorRD(q, env, rd));
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
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
};
/** 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
projects / cvc5.git / commitdiff