From: Andrew Reynolds Date: Tue, 9 Mar 2021 22:31:38 +0000 (-0600) Subject: Merge initialization steps in TheoryModelBuilder (#4901) X-Git-Tag: cvc5-1.0.0~2123 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b8fc6287c49ebbcb0d5ad83f0dfaa803056448d;p=cvc5.git Merge initialization steps in TheoryModelBuilder (#4901) Currently when constructing models, we traverse the equality engine of the model 3 times during initialization. This PR merges these 3 traversals. This refactoring is necessary to update model building for the "centralized" approach for equality reasoning, where it will be important to traverse the equality engine of the model in a careful way (to skip irrelevant terms). The PR also makes a few minor optimizations for e.g. reducing map lookups, and adds more documentation. --- diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 0d83fa42d..acfd24fbc 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -192,12 +192,12 @@ void TheoryEngineModelBuilder::addAssignableSubterms(TNode n, void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm, Node eqc, - Node const_rep) + Node constRep) { - d_constantReps[eqc] = const_rep; + d_constantReps[eqc] = constRep; Trace("model-builder") << " Assign: Setting constant rep of " << eqc - << " to " << const_rep << endl; - tm->d_rep_set.setTermForRepresentative(const_rep, eqc); + << " to " << constRep << endl; + tm->d_rep_set.setTermForRepresentative(constRep, eqc); } bool TheoryEngineModelBuilder::isExcludedCdtValue( @@ -375,7 +375,6 @@ void TheoryEngineModelBuilder::addToTypeList( bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) { Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; - eq::EqualityEngine* ee = tm->d_equalityEngine; Trace("model-builder") << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl; @@ -389,124 +388,197 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } Trace("model-builder") - << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl; - // Loop through all terms and make sure that assignable sub-terms are in the - // equality engine - // Also, record #eqc per type (for finite model finding) - std::map eqc_usort_count; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); - { - NodeSet cache; - for (; !eqcs_i.isFinished(); ++eqcs_i) - { - eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), ee); - for (; !eqc_i.isFinished(); ++eqc_i) - { - addAssignableSubterms(*eqc_i, tm, cache); - } - TypeNode tn = (*eqcs_i).getType(); - if (tn.isSort()) - { - if (eqc_usort_count.find(tn) == eqc_usort_count.end()) - { - eqc_usort_count[tn] = 1; - } - else - { - eqc_usort_count[tn]++; - } - } - } - } + << "TheoryEngineModelBuilder: Add assignable subterms " + ", collect representatives and compute assignable information..." + << std::endl; + + // type enumerator properties + TypeEnumeratorProperties tep; - Trace("model-builder") << "Collect representatives..." << std::endl; + // In the first step of model building, we do a traversal of the + // equality engine and record the information in the following: - // Process all terms in the equality engine, store representatives for each EC + // The constant representatives, per equivalence class d_constantReps.clear(); + // The representatives that have been asserted by theories. This includes + // non-constant "skeletons" that have been specified by parametric theories. std::map assertedReps; + // A parition of the set of equivalence classes that have: + // (1) constant representatives, + // (2) an assigned representative specified by a theory in collectModelInfo, + // (3) no assigned representative. 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()) - { - tep.d_fixed_usort_card = true; - for (std::map::iterator it = eqc_usort_count.begin(); - it != eqc_usort_count.end(); - ++it) - { - Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " - << it->second << std::endl; - tep.d_fixed_card[it->first] = Integer(it->second); - } - 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 + - // parametric types instantiated with uninterpreted sorts, but is probably - // a good idea to do in general since it leads to models with smaller term - // sizes. + // An ordered list of types, such that T1 comes before T2 if T1 is a + // "component type" of T2, e.g. U comes before (Set U). This is only strictly + // necessary for finite model finding + parametric types instantiated with + // uninterpreted sorts, but is probably a good idea to do in general since it + // leads to models with smaller term sizes. -AJR std::vector type_list; - eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); + // The count of equivalence classes per sort (for finite model finding). + std::map eqc_usort_count; + + // 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. + std::unordered_set assignableEqc; + // 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. + std::unordered_set evaluableEqc; + // Assigner objects for relevant equivalence classes that require special + // ways of assigning values, e.g. those that take into account assignment + // exclusion sets. + std::map eqcToAssigner; + // 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). + std::map eqcToAssignerMaster; + + // Loop through equivalence classes of the equality engine of the model. + eq::EqualityEngine* ee = tm->d_equalityEngine; + NodeSet assignableCache; + std::map::iterator itm; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + // should we compute assigner objects? + bool computeAssigners = tm->hasAssignmentExclusionSets(); + // the set of exclusion sets we have processed + std::unordered_set processedExcSet; for (; !eqcs_i.isFinished(); ++eqcs_i) { - // eqc is the equivalence class representative - Node eqc = (*eqcs_i); - Trace("model-builder") << "Processing EC: " << eqc << endl; - Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc); - TypeNode eqct = eqc.getType(); - Assert(assertedReps.find(eqc) == assertedReps.end()); - Assert(d_constantReps.find(eqc) == d_constantReps.end()); + Node eqc = *eqcs_i; + + // Information computed for each equivalence class + + // The assigned represenative and constant representative + Node rep, constRep; + // 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 CVC4_UNUSED = 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; + // 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 esetGroup; // Loop through terms in this EC - Node rep, const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); for (; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; Trace("model-builder") << " Processing Term: " << n << endl; - // Record as rep if this node was specified as a representative - if (tm->d_reps.find(n) != tm->d_reps.end()) + + // For each term n in this equivalence class, below we register its + // assignable subterms, compute whether it is a constant or assigned + // representative, then if we don't have a constant representative, + // compute information regarding how we will assign values. + + // (1) Add assignable subterms, which ensures that e.g. models for + // uninterpreted functions take into account all subterms in the + // equality engine of the model + addAssignableSubterms(n, tm, assignableCache); + // model-specific processing of the term + tm->addTermInternal(n); + + // (2) Record constant representative or assign representative, if + // applicable + if (n.isConst()) { - // AJR: I believe this assertion is too strict, - // e.g. datatypes may assert representative for two constructor terms - // that are not in the care graph and are merged during - // collectModelInfo. - // Assert(rep.isNull()); - rep = tm->d_reps[n]; - Assert(!rep.isNull()); - Trace("model-builder") << " Rep( " << eqc << " ) = " << rep - << std::endl; + Assert(constRep.isNull()); + constRep = n; + Trace("model-builder") + << " ConstRep( " << eqc << " ) = " << constRep << std::endl; + // if we have a constant representative, nothing else matters + continue; } - // Record as const_rep if this node is constant - if (n.isConst()) + + // If we don't have a constant rep, check if this is an assigned rep. + itm = tm->d_reps.find(n); + if (itm != tm->d_reps.end()) { - Assert(const_rep.isNull()); - const_rep = n; - Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep - << std::endl; + // Notice that this equivalence class may contain multiple terms that + // were specified as being a representative, since e.g. datatypes may + // assert representative for two constructor terms that are not in the + // care graph and are merged during collectModeInfo due to equality + // information from another theory. We overwrite the value of rep in + // these cases here. + rep = itm->second; + Trace("model-builder") + << " Rep( " << eqc << " ) = " << rep << std::endl; + } + + // (3) Finally, process assignable information + if (!isAssignable(n)) + { + evaluable = true; + // expressions that are not assignable should not be given assignment + // exclusion sets + Assert(!tm->getAssignmentExclusionSet(n, esetGroup, eset)); + continue; + } + assignable = true; + if (!computeAssigners) + { + // we don't compute assigners, skip + continue; + } + // process the assignment exclusion set for term n + // was it processed based on a master exclusion group (see + // eqcToAssignerMaster)? + if (processedExcSet.find(n) != processedExcSet.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, esetGroup, eset)) + { + // Should not have two assignment exclusion sets for the same + // equivalence class + Assert(!hasESet); + foundESet = true; + hasESet = true; } - // model-specific processing of the term - tm->addTermInternal(n); } - // Assign representative for this EC - if (!const_rep.isNull()) + // finished traversing the equality engine + TypeNode eqct = eqc.getType(); + // count the number of equivalence classes of sorts in finite model finding + if (options::finiteModelFind()) + { + if (eqct.isSort()) + { + eqc_usort_count[eqct]++; + } + } + // Assign representative for this equivalence class + if (!constRep.isNull()) { // Theories should not specify a rep if there is already a constant in the - // EC - // AJR: I believe this assertion is too strict, eqc with asserted reps may - // merge with constant eqc - // Assert(rep.isNull() || rep == const_rep); - assignConstantRep(tm, eqc, const_rep); - typeConstSet.add(eqct.getBaseType(), const_rep); + // equivalence class. However, it may be the case that the representative + // specified by a theory may be merged with a constant based on equality + // information from another class. Thus, rep may be non-null here. + // Regardless, we assign constRep as the representative here. + assignConstantRep(tm, eqc, constRep); + typeConstSet.add(eqct.getBaseType(), constRep); + continue; } else if (!rep.isNull()) { @@ -521,21 +593,80 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) std::unordered_set visiting; addToTypeList(eqct, type_list, visiting); } + + 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 : esetGroup) + { + 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 + processedExcSet.insert(g); + } + } + } } - 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); + // Now finished initialization + + // 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). + if (options::finiteModelFind()) + { + tep.d_fixed_usort_card = true; + for (std::map::iterator it = eqc_usort_count.begin(); + it != eqc_usort_count.end(); + ++it) + { + Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " + << it->second << std::endl; + tep.d_fixed_card[it->first] = Integer(it->second); + } + typeConstSet.setTypeEnumeratorProperties(&tep); + } // Need to ensure that each EC has a constant representative. @@ -931,163 +1062,6 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl; 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 CVC4_UNUSED = 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, TheoryModel* m) { diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index ef8526be3..048b40316 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -72,6 +72,9 @@ class TheoryEngineModelBuilder * Lemmas may be sent on an output channel by this * builder in steps (2) or (5), for instance, if the model we * are building fails to satisfy a quantified formula. + * + * @param m The model to build + * @return true if the model was successfully built. */ bool buildModel(TheoryModel* m); @@ -264,37 +267,6 @@ class TheoryEngineModelBuilder * 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? *