diff options
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 186 |
1 files changed, 119 insertions, 67 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 72352f6d3..63772cc1f 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -415,6 +415,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::set< TypeNode > allTypes; eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { + // eqc is the equivalence class representative Node eqc = (*eqcs_i); Trace("model-builder") << "Processing EC: " << eqc << endl; @@ -470,7 +471,9 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) TypeSet::iterator it; set<TypeNode>::iterator type_it; + set<Node>::iterator i, i2; bool changed, unassignedAssignable, assignOne = false; + set<TypeNode> evaluableSet; // Double-fixed-point loop // Outer loop handles a special corner case (see code at end of loop for details) @@ -482,60 +485,26 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) do { changed = false; unassignedAssignable = false; + evaluableSet.clear(); // Iterate over all types we've seen for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) { TypeNode t = *type_it; TypeNode tb = t.getBaseType(); - set<Node>::iterator i, i2; - - // 1. First normalize any non-const representative terms for this type - set<Node>* repSet = typeRepSet.getSet(tb); - bool done = repSet == NULL || repSet->empty(); - if (!done) { - Trace("model-builder") << " Normalizing base type: " << tb << endl; - } - while (!done) { - done = true; - d_normalizedCache.clear(); - for (i = repSet->begin(); i != repSet->end(); ) { - Assert(assertedReps.find(*i) != assertedReps.end()); - Node rep = assertedReps[*i]; - Node normalized = normalize(tm, rep, constantReps, false); - Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; - if (normalized.isConst()) { - changed = true; - done = false; - typeConstSet.add(tb, normalized); - constantReps[*i] = normalized; - assertedReps.erase(*i); - i2 = i; - ++i; - repSet->erase(i2); - } - else { - if (normalized != rep) { - assertedReps[*i] = normalized; - changed = true; - done = false; - } - ++i; - } - } - } - - // 2. Now try to evaluate or assign the EC's in this type set<Node>* noRepSet = typeNoRepSet.getSet(t); + + // 1. Try to evaluate the EC's in this type if (noRepSet != NULL && !noRepSet->empty()) { - Trace("model-builder") << " Eval/assign working on type: " << t << endl; - bool assignable, evaluable; + Trace("model-builder") << " Eval phase, working on type: " << t << endl; + bool assignable, evaluable, evaluated; d_normalizedCache.clear(); for (i = noRepSet->begin(); i != noRepSet->end(); ) { i2 = i; ++i; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); assignable = false; evaluable = false; + evaluated = false; + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; if (isAssignable(n)) { @@ -545,55 +514,138 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) evaluable = true; Node normalized = normalize(tm, n, constantReps, true); if (normalized.isConst()) { - typeConstSet.add(t.getBaseType(), normalized); + typeConstSet.add(tb, normalized); constantReps[*i2] = normalized; Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; changed = true; + evaluated = true; noRepSet->erase(i2); break; } } } - if (assignable) { - // We are about to make a choice - we have to make sure we have learned everything we can first. Only make a choice if: - // 1. fullModel is true - // 2. there are no terms of this type with un-normalized representatives - // 3. there are no evaluable terms in this EC - // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode, go ahead and make one assignment - if (fullModel && (((repSet == NULL || repSet->empty()) && !evaluable) || assignOne)) { - assignOne = false; - Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); - Node n; - if (t.getCardinality().isInfinite()) { - n = typeConstSet.nextTypeEnum(t, true); - } - else { - TypeEnumerator te(t); - n = *te; - } - Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; - changed = true; - noRepSet->erase(i2); + if (!evaluated) { + if (evaluable) { + evaluableSet.insert(tb); } - else { + if (assignable) { unassignedAssignable = true; } } } } + + // 2. Normalize any non-const representative terms for this type + set<Node>* repSet = typeRepSet.getSet(t); + if (repSet != NULL && !repSet->empty()) { + Trace("model-builder") << " Normalization phase, working on type: " << t << endl; + d_normalizedCache.clear(); + for (i = repSet->begin(); i != repSet->end(); ) { + Assert(assertedReps.find(*i) != assertedReps.end()); + Node rep = assertedReps[*i]; + Node normalized = normalize(tm, rep, constantReps, false); + Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; + if (normalized.isConst()) { + changed = true; + typeConstSet.add(t.getBaseType(), normalized); + constantReps[*i] = normalized; + assertedReps.erase(*i); + i2 = i; + ++i; + repSet->erase(i2); + } + else { + if (normalized != rep) { + assertedReps[*i] = normalized; + changed = true; + } + ++i; + } + } + } } } while (changed); - if (!unassignedAssignable || !fullModel) { + + if (!fullModel || !unassignedAssignable) { break; } + + // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite + // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be + // different are different. + + // Only make assignments on a type if: + // 1. fullModel is true + // 2. there are no terms that share the same base type with un-normalized representatives + // 3. there are no terms that share teh same base type that are unevaluated evaluable terms + // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment + changed = false; + for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { + set<Node>& noRepSet = TypeSet::getSet(it); + if (noRepSet.empty()) { + continue; + } + TypeNode t = TypeSet::getType(it); + TypeNode tb = t.getBaseType(); + if (!assignOne) { + set<Node>* repSet = typeRepSet.getSet(tb); + if (repSet != NULL && !repSet->empty()) { + continue; + } + if (evaluableSet.find(tb) != evaluableSet.end()) { + continue; + } + } + Trace("model-builder") << " Assign phase, working on type: " << t << endl; + bool assignable, evaluable; + 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) { + Node n = *eqc_i; + if (isAssignable(n)) { + assignable = true; + } + else { + evaluable = true; + } + } + if (assignable) { + Assert(!evaluable || assignOne); + Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); + Node n; + if (t.getCardinality().isInfinite()) { + n = typeConstSet.nextTypeEnum(t, true); + } + else { + TypeEnumerator te(t); + n = *te; + } + Assert(!n.isNull()); + constantReps[*i2] = n; + Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; + changed = true; + noRepSet.erase(i2); + if (assignOne) { + assignOne = false; + break; + } + } + } + } + // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In this case, neither one will get assigned because we are waiting // to be able to evaluate. But we will never be able to evaluate because the variables that need to be assigned are in // these same EC's. In this case, repeat the whole fixed-point computation with the difference that the first EC // that has both assignable and evaluable expressions will get assigned. - assignOne = true; + if (!changed) { + Assert(!assignOne); // check for infinite loop! + assignOne = true; + } } #ifdef CVC4_ASSERTIONS |