From 0db2265511cf553c793cfb150079c524bb1e6449 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Dec 2019 14:30:42 -0600 Subject: [PATCH] Extend model construction with assignment exclusion set (#3377) This extends the core model building algorithm in CVC4 with "assignment exclusion sets". This functionality is useful for assigning values to terms of finite type that have specific restrictions on what their value cannot be. In detail, previously, all unassigned terms of finite type were always assigned the first term in the type enumeration. This is done since it is assumed that theories (e.g. datatypes) always do enough work to ensure that *arbitrary* values can be assigned to terms of finite type, and *fresh* values can be assigned to terms of infinite type. However, there are compelling cases (sets+cardinality for finite element types) where one may want to impose restrictions on what values can be assigned to terms of finite types. Thus, we now provide `setAssignmentExclusionSet` as a way of communicating these restrictions. This commit also refactors a few parts of `TheoryEngineModelBuilder::buildModel` to be clearer, in particular by adding a few helper functions, and by caching certain information early in the function instead of recomputing it. This is work towards #1123. --- src/theory/theory_model.cpp | 66 +++++ src/theory/theory_model.h | 71 ++++- src/theory/theory_model_builder.cpp | 385 ++++++++++++++++++++++++---- src/theory/theory_model_builder.h | 95 ++++++- 4 files changed, 553 insertions(+), 64 deletions(-) diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index da66a2ef2..c6055ede9 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -74,6 +74,9 @@ void TheoryModel::reset(){ d_approximations.clear(); d_approx_list.clear(); d_reps.clear(); + d_assignExcSet.clear(); + d_aesMaster.clear(); + d_aesSlaves.clear(); d_rep_set.clear(); d_uf_terms.clear(); d_ho_uf_terms.clear(); @@ -520,6 +523,69 @@ void TheoryModel::assertSkeleton(TNode n) d_reps[ n ] = n; } +void TheoryModel::setAssignmentExclusionSet(TNode n, + const std::vector& eset) +{ + // should not be assigned yet + Assert(d_assignExcSet.find(n) == d_assignExcSet.end()); + Trace("model-builder-debug") + << "Exclude values of " << n << " : " << eset << std::endl; + std::vector& aes = d_assignExcSet[n]; + aes.insert(aes.end(), eset.begin(), eset.end()); +} + +void TheoryModel::setAssignmentExclusionSetGroup( + const std::vector& group, const std::vector& eset) +{ + if (group.empty()) + { + return; + } + // for efficiency, we store a single copy of eset and set a slave/master + // relationship + setAssignmentExclusionSet(group[0], eset); + std::vector& gslaves = d_aesSlaves[group[0]]; + for (unsigned i = 1, gsize = group.size(); i < gsize; ++i) + { + Node gs = group[i]; + // set master + d_aesMaster[gs] = group[0]; + // add to slaves + gslaves.push_back(gs); + } +} + +bool TheoryModel::getAssignmentExclusionSet(TNode n, + std::vector& group, + std::vector& eset) +{ + // does it have a master? + std::map::iterator itm = d_aesMaster.find(n); + if (itm != d_aesMaster.end()) + { + return getAssignmentExclusionSet(itm->second, group, eset); + } + std::map >::iterator ita = d_assignExcSet.find(n); + if (ita == d_assignExcSet.end()) + { + return false; + } + eset.insert(eset.end(), ita->second.begin(), ita->second.end()); + group.push_back(n); + // does it have slaves? + ita = d_aesSlaves.find(n); + if (ita != d_aesSlaves.end()) + { + group.insert(group.end(), ita->second.begin(), ita->second.end()); + } + return true; +} + +bool TheoryModel::hasAssignmentExclusionSets() const +{ + return !d_assignExcSet.empty(); +} + void TheoryModel::recordApproximation(TNode n, TNode pred) { Trace("model-builder-debug") diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b120b4501..0914987cc 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -139,6 +139,60 @@ public: * during Theory's collectModelInfo( ... ) functions. */ void assertSkeleton(TNode n); + /** set assignment exclusion set + * + * This method sets the "assignment exclusion set" for term n. This is a + * set of terms whose value n must be distinct from in the model. + * + * This method should be used sparingly, and in a way such that model + * building is still guaranteed to succeed. Term n is intended to be an + * assignable term, typically of finite type. Thus, for example, this method + * should not be called with a vector eset that is greater than the + * cardinality of the type of n. Additionally, this method should not be + * called in a way that introduces cyclic dependencies on the assignment order + * of terms in the model. For example, providing { y } as the assignment + * exclusion set of x and { x } as the assignment exclusion set of y will + * cause model building to fail. + * + * The vector eset should contain only terms that occur in the model, or + * are constants. + * + * Additionally, we (currently) require that an assignment exclusion set + * should not be set for two terms in the same equivalence class, or to + * equivalence classes with an assignable term. Otherwise an + * assertion will be thrown by TheoryEngineModelBuilder during model building. + */ + void setAssignmentExclusionSet(TNode n, const std::vector& eset); + /** set assignment exclusion set group + * + * Given group = { x_1, ..., x_n }, this is semantically equivalent to calling + * the above method on the following pairs of arguments: + * x1, eset + * x2, eset + { x_1 } + * ... + * xn, eset + { x_1, ..., x_{n-1} } + * Similar restrictions should be considered as above when applying this + * method to ensure that model building will succeed. Notice that for + * efficiency, the implementation of how the above information is stored + * may avoid constructing n copies of eset. + */ + void setAssignmentExclusionSetGroup(const std::vector& group, + const std::vector& eset); + /** get assignment exclusion set for term n + * + * If n has been given an assignment exclusion set, then this method returns + * true and the set is added to eset. Otherwise, the method returns false. + * + * Additionally, if n was assigned an assignment exclusion set via a call to + * setAssignmentExclusionSetGroup, it adds all members that were passed + * in the first argument of that call to the vector group. Otherwise, it + * adds n itself to group. + */ + bool getAssignmentExclusionSet(TNode n, + std::vector& group, + std::vector& eset); + /** have any assignment exclusion sets been created? */ + bool hasAssignmentExclusionSets() const; /** record approximation * * This notifies this model that the value of n was approximated in this @@ -299,9 +353,22 @@ public: std::unordered_set d_not_evaluated_kinds; /** a set of kinds that are semi-evaluated */ std::unordered_set d_semi_evaluated_kinds; - /** map of representatives of equality engine to used representatives in - * representative set */ + /** + * Map of representatives of equality engine to used representatives in + * representative set + */ std::map d_reps; + /** Map of terms to their assignment exclusion set. */ + std::map > d_assignExcSet; + /** + * Map of terms to their "assignment exclusion set master". After a call to + * setAssignmentExclusionSetGroup, the master of each term in group + * (except group[0]) is set to group[0], which stores the assignment + * exclusion set for that group in the above map. + */ + std::map d_aesMaster; + /** Reverse of the above map */ + std::map > d_aesSlaves; /** stores set of representatives for each type */ RepSet d_rep_set; /** true/false nodes */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 6df412ae3..11758f1e9 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -27,10 +27,100 @@ using namespace CVC4::context; namespace CVC4 { namespace theory { +void TheoryEngineModelBuilder::Assigner::initialize( + TypeNode tn, TypeEnumeratorProperties* tep, const std::vector& aes) +{ + d_te.reset(new TypeEnumerator(tn, tep)); + d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end()); +} + +Node TheoryEngineModelBuilder::Assigner::getNextAssignment() +{ + Assert(d_te != nullptr); + Node n; + bool success = false; + TypeEnumerator& te = *d_te; + // Check if we have run out of elements. This should never happen; if it + // does we assert false and return null. + if (te.isFinished()) + { + Assert(false); + return Node::null(); + } + // must increment until we find one that is not in the assignment + // exclusion set + do + { + n = *te; + success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n) + == d_assignExcSet.end(); + // increment regardless of fail or succeed, to set up the next value + ++te; + } while (!success); + return n; +} + TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te) { } +Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r) +{ + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine); + for (; !eqc_i.isFinished(); ++eqc_i) + { + Node n = *eqc_i; + Trace("model-builder-debug") << "Look at term : " << n << std::endl; + if (!isAssignable(n)) + { + Trace("model-builder-debug") << "...try to normalize" << std::endl; + Node normalized = normalize(m, n, true); + if (normalized.isConst()) + { + return normalized; + } + } + } + return Node::null(); +} + +bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a) +{ + if (a.d_isActive) + { + return true; + } + std::vector& eset = a.d_assignExcSet; + std::map::iterator it; + for (unsigned i = 0, size = eset.size(); i < size; i++) + { + // Members of exclusion set must have values, otherwise we are not yet + // assignable. + Node er = eset[i]; + if (er.isConst()) + { + // already processed + continue; + } + // Assignable members of assignment exclusion set should be representatives + // of their equivalence classes. This ensures we look up the constant + // representatives for assignable members of assignment exclusion sets. + Assert(er == tm->getRepresentative(er)); + it = d_constantReps.find(er); + if (it == d_constantReps.end()) + { + Trace("model-build-aes") + << "isAssignerActive: not active due to " << er << std::endl; + return false; + } + // update + eset[i] = it->second; + } + Trace("model-build-aes") << "isAssignerActive: active!" << std::endl; + a.d_isActive = true; + return true; +} + bool TheoryEngineModelBuilder::isAssignable(TNode n) { if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL) @@ -286,6 +376,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) { Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; TheoryModel* tm = (TheoryModel*)m; + eq::EqualityEngine* ee = tm->d_equalityEngine; // buildModel should only be called once per check Assert(!tm->isBuilt()); @@ -324,13 +415,12 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) // equality engine // Also, record #eqc per type (for finite model finding) std::map eqc_usort_count; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); { NodeSet cache; for (; !eqcs_i.isFinished(); ++eqcs_i) { - eq::EqClassIterator eqc_i = - eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), ee); for (; !eqc_i.isFinished(); ++eqc_i) { addAssignableSubterms(*eqc_i, tm, cache); @@ -356,6 +446,13 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) d_constantReps.clear(); std::map assertedReps; TypeSet typeConstSet, typeRepSet, typeNoRepSet; + // Compute type enumerator properties. This code ensures we do not + // enumerate terms that have uninterpreted constants that violate the + // bounds imposed by finite model finding. For example, if finite + // model finding insists that there are only 2 values { U1, U2 } of type U, + // then the type enumerator for list of U should enumerate: + // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ... + // instead of enumerating (cons U3 nil). TypeEnumeratorProperties tep; if (options::finiteModelFind()) { @@ -370,6 +467,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } typeConstSet.setTypeEnumeratorProperties(&tep); } + // AJR: build ordered list of types that ensures that base types are // enumerated first. // (I think) this is only strictly necessary for finite model finding + @@ -446,6 +544,20 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } } + Trace("model-builder") << "Compute assignable information..." << std::endl; + // The set of equivalence classes that are "assignable" + std::unordered_set assignableEqc; + // The set of equivalence classes that are "evaluable" + std::unordered_set evaluableEqc; + // Assigner objects for relevant equivalence classes + std::map eqcToAssigner; + // Maps equivalence classes to the equivalence class that maps to its assigner + // object in the above map. + std::map eqcToAssignerMaster; + // Compute the above information + computeAssignableInfo( + tm, tep, assignableEqc, evaluableEqc, eqcToAssigner, eqcToAssignerMaster); + // Need to ensure that each EC has a constant representative. Trace("model-builder") << "Processing EC's..." << std::endl; @@ -484,56 +596,40 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) { Trace("model-builder") << " Eval phase, working on type: " << t << endl; - bool assignable, evaluable, evaluated; + bool evaluable; d_normalizedCache.clear(); for (i = noRepSet->begin(); i != noRepSet->end();) { i2 = i; ++i; - assignable = false; - evaluable = false; - evaluated = false; Trace("model-builder-debug") << "Look at eqc : " << (*i2) << std::endl; - eq::EqClassIterator eqc_i = - eq::EqClassIterator(*i2, tm->d_equalityEngine); - for (; !eqc_i.isFinished(); ++eqc_i) + Node normalized; + // only possible to normalize if we are evaluable + evaluable = evaluableEqc.find(*i2) != evaluableEqc.end(); + if (evaluable) { - Node n = *eqc_i; - Trace("model-builder-debug") << "Look at term : " << n - << std::endl; - if (isAssignable(n)) - { - assignable = true; - Trace("model-builder-debug") << "...assignable" << std::endl; - } - else - { - evaluable = true; - Trace("model-builder-debug") << "...try to normalize" - << std::endl; - Node normalized = normalize(tm, n, true); - if (normalized.isConst()) - { - typeConstSet.add(tb, normalized); - assignConstantRep(tm, *i2, normalized); - Trace("model-builder") << " Eval: Setting constant rep of " - << (*i2) << " to " << normalized - << endl; - changed = true; - evaluated = true; - noRepSet->erase(i2); - break; - } - } + normalized = evaluateEqc(tm, *i2); } - if (!evaluated) + if (!normalized.isNull()) + { + Assert(normalized.isConst()); + typeConstSet.add(tb, normalized); + assignConstantRep(tm, *i2, normalized); + Trace("model-builder") << " Eval: Setting constant rep of " + << (*i2) << " to " << normalized << endl; + changed = true; + noRepSet->erase(i2); + } + else { if (evaluable) { evaluableSet.insert(tb); } - if (assignable) + // If assignable, remember there is an equivalence class that is + // not assigned and assignable. + if (assignableEqc.find(*i2) != assignableEqc.end()) { unassignedAssignable = true; } @@ -657,26 +753,34 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Trace("model-builder") << " Assign phase, working on type: " << t << endl; bool assignable, evaluable CVC4_UNUSED; + std::map::iterator itAssigner; + std::map::iterator itAssignerM; for (i = noRepSet.begin(); i != noRepSet.end();) { i2 = i; ++i; - eq::EqClassIterator eqc_i = - eq::EqClassIterator(*i2, tm->d_equalityEngine); - assignable = false; - evaluable = false; - for (; !eqc_i.isFinished(); ++eqc_i) + // check whether it has an assigner object + itAssignerM = eqcToAssignerMaster.find(*i2); + if (itAssignerM != eqcToAssignerMaster.end()) { - Node n = *eqc_i; - if (isAssignable(n)) - { - assignable = true; - } - else - { - evaluable = true; - } + // Take the master's assigner. Notice we don't care which order + // equivalence classes are assigned. For instance, the master can + // be assigned after one of its slaves. + itAssigner = eqcToAssigner.find(itAssignerM->second); + } + else + { + itAssigner = eqcToAssigner.find(*i2); } + if (itAssigner != eqcToAssigner.end()) + { + assignable = isAssignerActive(tm, itAssigner->second); + } + else + { + assignable = assignableEqc.find(*i2) != assignableEqc.end(); + } + evaluable = evaluableEqc.find(*i2) != evaluableEqc.end(); Trace("model-builder-debug") << " eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl; @@ -692,8 +796,18 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Assert(!t.isBoolean() || (*i2).isVar() || (*i2).getKind() == kind::APPLY_UF); Node n; - if (!t.isFinite()) + if (itAssigner != eqcToAssigner.end()) + { + Trace("model-builder-debug") + << "Get value from assigner for finite type..." << std::endl; + // if it has an assigner, get the value from the assigner. + n = itAssigner->second.getNextAssignment(); + Assert(!n.isNull()); + } + else if (!t.isFinite()) { + // if its infinite, we get a fresh value that does not occur in + // the model. bool success; do { @@ -743,13 +857,17 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } //--- } while (!success); + Assert(!n.isNull()); } else { + Trace("model-builder-debug") + << "Get first value from finite type..." << std::endl; + // Otherwise, we get the first value from the type enumerator. TypeEnumerator te(t); n = *te; } - Assert(!n.isNull()); + Trace("model-builder-debug") << "...got " << n << std::endl; assignConstantRep(tm, *i2, n); changed = true; noRepSet.erase(i2); @@ -830,6 +948,163 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) tm->d_modelBuiltSuccess = true; return true; } +void TheoryEngineModelBuilder::computeAssignableInfo( + TheoryModel* tm, + TypeEnumeratorProperties& tep, + std::unordered_set& assignableEqc, + std::unordered_set& evaluableEqc, + std::map& eqcToAssigner, + std::map& eqcToAssignerMaster) +{ + eq::EqualityEngine* ee = tm->d_equalityEngine; + bool computeAssigners = tm->hasAssignmentExclusionSets(); + std::unordered_set processed; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + // A flag set to true if the current equivalence class is assignable (see + // assignableEqc). + bool assignable = false; + // Set to true if the current equivalence class is evaluatable (see + // evaluableEqc). + bool evaluable = false; + // Set to true if a term in the current equivalence class has been given an + // assignment exclusion set. + bool hasESet = false; + // Set to true if we found that a term in the current equivalence class has + // been given an assignment exclusion set, and we have not seen this term + // as part of a previous assignment exclusion group. In other words, when + // this flag is true we construct a new assigner object with the current + // equivalence class as its master. + bool foundESet = false; + // Look at all equivalence classes in the model + for (; !eqcs_i.isFinished(); ++eqcs_i) + { + Node eqc = *eqcs_i; + if (d_constantReps.find(eqc) != d_constantReps.end()) + { + // already assigned above, skip + continue; + } + // reset information for the current equivalence classe + assignable = false; + evaluable = false; + hasESet = false; + foundESet = false; + // the assignment exclusion set for the current equivalence class + std::vector eset; + // the group to which this equivalence class belongs when exclusion sets + // were assigned (see the argument group of + // TheoryModel::getAssignmentExclusionSet). + std::vector group; + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + // For each term in the current equivalence class, we update the above + // information. We may terminate this loop before looking at all terms if we + // have inferred the value of all of the information above. + for (; !eqc_i.isFinished(); ++eqc_i) + { + Node n = *eqc_i; + if (!isAssignable(n)) + { + evaluable = true; + if (!computeAssigners) + { + if (assignable) + { + // both flags set, we are done + break; + } + } + // expressions that are not assignable should not be given assignment + // exclusion sets + Assert(!tm->getAssignmentExclusionSet(n, group, eset)); + continue; + } + else + { + assignable = true; + if (!computeAssigners) + { + if (evaluable) + { + // both flags set, we are done + break; + } + // we don't compute assigners, skip + continue; + } + } + // process the assignment exclusion set for term n + // was it processed as a slave of a group? + if (processed.find(n) != processed.end()) + { + // Should not have two assignment exclusion sets for the same + // equivalence class + Assert(!hasESet); + Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end()); + // already processed as a slave term + hasESet = true; + continue; + } + // was it assigned one? + if (tm->getAssignmentExclusionSet(n, group, eset)) + { + // Should not have two assignment exclusion sets for the same + // equivalence class + Assert(!hasESet); + foundESet = true; + hasESet = true; + } + } + if (assignable) + { + assignableEqc.insert(eqc); + } + if (evaluable) + { + evaluableEqc.insert(eqc); + } + // If we found an assignment exclusion set, we construct a new assigner + // object. + if (foundESet) + { + // we don't accept assignment exclusion sets for evaluable eqc + Assert(!evaluable); + // construct the assigner + Assigner& a = eqcToAssigner[eqc]; + // Take the representatives of each term in the assignment exclusion + // set, which ensures we can look up their value in d_constReps later. + std::vector aes; + for (const Node& e : eset) + { + // Should only supply terms that occur in the model or constants + // in assignment exclusion sets. + Assert(tm->hasTerm(e) || e.isConst()); + Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e; + aes.push_back(er); + } + // initialize + a.initialize(eqc.getType(), &tep, aes); + // all others in the group are slaves of this + for (const Node& g : group) + { + Assert(isAssignable(g)); + if (!tm->hasTerm(g)) + { + // Ignore those that aren't in the model, in the case the user + // has supplied an assignment exclusion set to a variable not in + // the model. + continue; + } + Node gr = tm->getRepresentative(g); + if (gr != eqc) + { + eqcToAssignerMaster[gr] = eqc; + // remember that this term has been processed + processed.insert(g); + } + } + } + } +} void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m) { diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index ce090b14d..226ac573d 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -110,18 +110,23 @@ class TheoryEngineModelBuilder : public ModelBuilder */ void debugCheckModel(TheoryModel* m); - /** is n assignable? + /** Evaluate equivalence class * - * A term n is assignable if its value - * is unconstrained by a standard model. - * Examples of assignable terms are: + * If this method returns a non-null node c, then c is a constant and some + * term in the equivalence class of r evaluates to c based on the current + * state of the model m. + */ + Node evaluateEqc(TheoryModel* m, TNode r); + /** is n an assignable expression? + * + * A term n is an assignable expression if its value is unconstrained by a + * standard model. Examples of assignable terms are: * - variables, * - applications of array select, * - applications of datatype selectors, * - applications of uninterpreted functions. - * Assignable terms must be first-order, that is, - * all instances of the above terms are not - * assignable if they have a higher-order (function) type. + * Assignable terms must be first-order, that is, all instances of the above + * terms are not assignable if they have a higher-order (function) type. */ bool isAssignable(TNode n); /** add assignable subterms @@ -210,6 +215,82 @@ class TheoryEngineModelBuilder : public ModelBuilder */ std::map d_constantReps; + /** Theory engine model builder assigner class + * + * This manages the assignment of values to terms of a given type. + * In particular, it is a wrapper around a type enumerator that is restricted + * by a set of values that it cannot generate, called an "assignment exclusion + * set". + */ + class Assigner + { + public: + Assigner() : d_te(nullptr), d_isActive(false) {} + /** + * Initialize this assigner to generate values of type tn, with properties + * tep and assignment exclusion set aes. + */ + void initialize(TypeNode tn, + TypeEnumeratorProperties* tep, + const std::vector& aes); + /** get the next term in the enumeration + * + * This method returns the next legal term based on type enumeration, where + * a term is legal it does not belong to the assignment exclusion set of + * this assigner. If no more terms exist, this method returns null. This + * should never be the case due to the conditions ensured by theory solvers + * for finite types. If it is the case, we give an assertion failure. + */ + Node getNextAssignment(); + /** The type enumerator */ + std::unique_ptr d_te; + /** The assignment exclusion set of this Assigner */ + std::vector d_assignExcSet; + /** + * Is active, flag set to true when all values in d_assignExcSet are + * constant. + */ + bool d_isActive; + }; + /** Is the given Assigner ready to assign values? + * + * This returns true if all values in the assignment exclusion set of a have + * a known value according to the state of this model builder (via a lookup + * in d_constantReps). It updates the assignment exclusion vector of a to + * these values whenever possible. + */ + bool isAssignerActive(TheoryModel* tm, Assigner& a); + /** compute assignable information + * + * This computes necessary information pertaining to how values should be + * assigned to equivalence classes in the equality engine of tm. + * + * The argument tep stores global information about how values should be + * assigned, such as information on how many uninterpreted constant + * values are available, which is restricted if finite model finding is + * enabled. + * + * In particular this method constructs the following, passed as arguments: + * (1) assignableEqc: the set of equivalence classes that are "assignable", + * i.e. those that have an assignable expression in them (see isAssignable), + * and have not already been assigned a constant, + * (2) evaluableEqc: the set of equivalence classes that are "evaluable", i.e. + * those that have an expression in them that is not assignable, and have not + * already been assigned a constant, + * (3) eqcToAssigner: assigner objects for relevant equivalence classes that + * require special ways of assigning values, e.g. those that take into + * account assignment exclusion sets, + * (4) eqcToAssignerMaster: a map from equivalence classes to the equivalence + * class that it shares an assigner object with (all elements in the range of + * this map are in the domain of eqcToAssigner). + */ + void computeAssignableInfo( + TheoryModel* tm, + TypeEnumeratorProperties& tep, + std::unordered_set& assignableEqc, + std::unordered_set& evaluableEqc, + std::map& eqcToAssigner, + std::map& eqcToAssignerMaster); //------------------------------------for codatatypes /** is v an excluded codatatype value? * -- 2.30.2