diff options
| -rw-r--r-- | src/theory/theory_model.cpp | 66 | ||||
| -rw-r--r-- | src/theory/theory_model.h | 71 | ||||
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 385 | ||||
| -rw-r--r-- | 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<Node>& 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<Node>& aes = d_assignExcSet[n]; + aes.insert(aes.end(), eset.begin(), eset.end()); +} + +void TheoryModel::setAssignmentExclusionSetGroup( + const std::vector<TNode>& group, const std::vector<Node>& 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<Node>& 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<Node>& group, + std::vector<Node>& eset) +{ + // does it have a master? + std::map<Node, Node>::iterator itm = d_aesMaster.find(n); + if (itm != d_aesMaster.end()) + { + return getAssignmentExclusionSet(itm->second, group, eset); + } + std::map<Node, std::vector<Node> >::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<Node>& 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<TNode>& group, + const std::vector<Node>& 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<Node>& group, + std::vector<Node>& 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<Kind, kind::KindHashFunction> d_not_evaluated_kinds; /** a set of kinds that are semi-evaluated */ std::unordered_set<Kind, kind::KindHashFunction> 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<Node, Node> d_reps; + /** Map of terms to their assignment exclusion set. */ + std::map<Node, std::vector<Node> > 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<Node, Node> d_aesMaster; + /** Reverse of the above map */ + std::map<Node, std::vector<Node> > 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<Node>& 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<Node>& eset = a.d_assignExcSet; + std::map<Node, Node>::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<TypeNode, unsigned> 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<Node, Node> 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<Node, NodeHashFunction> assignableEqc; + // The set of equivalence classes that are "evaluable" + std::unordered_set<Node, NodeHashFunction> evaluableEqc; + // Assigner objects for relevant equivalence classes + std::map<Node, Assigner> eqcToAssigner; + // Maps equivalence classes to the equivalence class that maps to its assigner + // object in the above map. + std::map<Node, Node> 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<Node, Assigner>::iterator itAssigner; + std::map<Node, Node>::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<Node, NodeHashFunction>& assignableEqc, + std::unordered_set<Node, NodeHashFunction>& evaluableEqc, + std::map<Node, Assigner>& eqcToAssigner, + std::map<Node, Node>& eqcToAssignerMaster) +{ + eq::EqualityEngine* ee = tm->d_equalityEngine; + bool computeAssigners = tm->hasAssignmentExclusionSets(); + std::unordered_set<Node, NodeHashFunction> 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<Node> eset; + // the group to which this equivalence class belongs when exclusion sets + // were assigned (see the argument group of + // TheoryModel::getAssignmentExclusionSet). + std::vector<Node> 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<Node> 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<Node, Node> 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<Node>& 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<TypeEnumerator> d_te; + /** The assignment exclusion set of this Assigner */ + std::vector<Node> 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<Node, NodeHashFunction>& assignableEqc, + std::unordered_set<Node, NodeHashFunction>& evaluableEqc, + std::map<Node, Assigner>& eqcToAssigner, + std::map<Node, Node>& eqcToAssignerMaster); //------------------------------------for codatatypes /** is v an excluded codatatype value? * |