From: Clark Barrett Date: Tue, 13 Nov 2012 22:51:27 +0000 (+0000) Subject: More bugfixes for models X-Git-Tag: cvc5-1.0.0~7604 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b1bc92ea30fd851e35db6728939cc0b33f03397;p=cvc5.git More bugfixes for models --- diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b9f027afa..342e67654 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -664,23 +664,40 @@ void TheoryArrays::collectReads(TNode n, set& readSet, set& cache) } +void TheoryArrays::collectArrays(TNode n, set& arraySet, set& cache) +{ + if (cache.find(n) != cache.end()) { + return; + } + if (n.getType().isArray()) { + arraySet.insert(n); + } + for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { + collectArrays(*child_it, arraySet, cache); + } + cache.insert(n); +} + + void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); std::map > selects; - set readSet; - set cache; - // Collect all selects appearing in assertions + set readSet, arraySet; + set readCache, arrayCache; + // Collect all arrays and selects appearing in assertions context::CDList::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); for (; assert_it != assert_it_end; ++assert_it) { - collectReads(*assert_it, readSet, cache); + collectReads(*assert_it, readSet, readCache); + collectArrays(*assert_it, arraySet, arrayCache); } - // Add selects that are shared terms + // Add arrays and selects that are shared terms context::CDList::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(); for (; shared_it != shared_it_end; ++ shared_it) { - collectReads(*shared_it, readSet, cache); + collectReads(*shared_it, readSet, readCache); + collectArrays(*shared_it, arraySet, arrayCache); } // Add selects that were generated internally @@ -692,16 +709,15 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ // Go through all equivalence classes and collect relevant arrays and reads std::vector arrays; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - bool isArray, computeRep; + bool computeRep; while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - isArray = eqc.getType().isArray(); computeRep = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly - if (isArray && n.getKind() != kind::STORE) { + if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) { arrays.push_back(eqc); computeRep = true; } @@ -712,11 +728,6 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ } ++eqc_i; } - // If this is an array EC but it only contains STORE nodes, then the value of this EC is derived from the others - - // no need to do extra work to compute it - if (isArray && !computeRep) { - m->assertRepresentative(eqc); - } ++eqcs_i; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 8358fe6c9..a47c8440e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -218,8 +218,9 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: - /** Helper function for collectModelInfo */ + /** Helper functions for collectModelInfo */ void collectReads(TNode n, std::set& readSet, std::set& cache); + void collectArrays(TNode n, std::set& arraySet, std::set& cache); public: void collectModelInfo( TheoryModel* m, bool fullModel ); diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 7853c2d17..a01844f77 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -410,6 +410,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // Process all terms in the equality engine, store representatives for each EC std::map< Node, Node > assertedReps, constantReps; TypeSet typeConstSet, typeRepSet, typeNoRepSet; + std::set< TypeNode > allTypes; eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative @@ -452,87 +453,131 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) } else if (!rep.isNull()) { assertedReps[eqc] = rep; - typeRepSet.add(eqct, eqc); + typeRepSet.add(eqct.getBaseType(), eqc); + allTypes.insert(eqct); } else { typeNoRepSet.add(eqct, eqc); + allTypes.insert(eqct); } } // Need to ensure that each EC has a constant representative. - // Phase 1: For types that do not have asserted reps, assign the unassigned EC's using either evaluation or type enumeration - Trace("model-builder") << "Starting phase 1..." << std::endl; + Trace("model-builder") << "Processing EC's..." << std::endl; TypeSet::iterator it; + set::iterator type_it; bool changed, unassignedAssignable, assignOne = false; // Double-fixed-point loop // Outer loop handles a special corner case (see code at end of loop for details) for (;;) { - // In this loop, we find a value for this EC using evaluation if possible. If not, and - // the EC contains a single "assignable" expression, then we assign it using type enumeration - // If the EC contains both, we wait, hoping to be able to evaluate the evaluable expression later + // Inner fixed-point loop: we are trying to learn constant values for every EC. Each time through this loop, we process all of the + // types by type and may learn some new EC values. EC's in one type may depend on EC's in another type, so we need a fixed-point loop + // to ensure that we learn as many EC values as possible do { changed = false; unassignedAssignable = false; - d_normalizedCache.clear(); - for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { - TypeNode t = TypeSet::getType(it); - Trace("model-builder") << " Working on type: " << t << endl; - set& noRepSet = TypeSet::getSet(it); - if (noRepSet.empty()) { - continue; - } + // 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::iterator i, i2; - 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; + + // 1. First normalize any non-const representative terms for this type + set* 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 { - evaluable = true; - Node normalized = normalize(tm, n, constantReps, true); - if (normalized.isConst()) { - typeConstSet.add(t.getBaseType(), normalized); - constantReps[*i2] = normalized; - Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; + if (normalized != rep) { + assertedReps[*i] = normalized; changed = true; - noRepSet.erase(i2); - break; + done = false; } + ++i; } } - if (assignable) { - if ((assignOne || !evaluable) && fullModel) { - assignOne = false; - Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); - Node n; - if (t.getCardinality().isInfinite()) { - n = typeConstSet.nextTypeEnum(t, true); + } + + // 2. Now try to evaluate or assign the EC's in this type + set* noRepSet = typeNoRepSet.getSet(t); + if (noRepSet != NULL && !noRepSet->empty()) { + Trace("model-builder") << " Eval/assign working on type: " << t << endl; + bool assignable, evaluable; + 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; + for ( ; !eqc_i.isFinished(); ++eqc_i) { + Node n = *eqc_i; + if (isAssignable(n)) { + assignable = true; } else { - TypeEnumerator te(t); - n = *te; + evaluable = true; + Node normalized = normalize(tm, n, constantReps, true); + if (normalized.isConst()) { + typeConstSet.add(t.getBaseType(), normalized); + constantReps[*i2] = normalized; + Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; + changed = true; + noRepSet->erase(i2); + break; + } } - Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " New Const: Setting constant rep of " << (*i2) << " to " << n << endl; - changed = true; - noRepSet.erase(i2); } - else { - unassignedAssignable = true; + 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); + } + else { + unassignedAssignable = true; + } } } } @@ -549,46 +594,13 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) assignOne = true; } - // Phase 2: Substitute into asserted reps using constReps. - // Iterate until a fixed point is reached. - Trace("model-builder") << "Starting phase 2..." << std::endl; - do { - changed = false; - d_normalizedCache.clear(); - for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { - set& repSet = TypeSet::getSet(it); - set::iterator i; - 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; - constantReps[*i] = normalized; - assertedReps.erase(*i); - set::iterator i2 = i; - ++i; - repSet.erase(i2); - } - else { - if (normalized != rep) { - assertedReps[*i] = normalized; - changed = true; - } - ++i; - } - } - } - } while (changed); - #ifdef CVC4_ASSERTIONS if (fullModel) { // Assert that all representatives have been converted to constants for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { set& repSet = TypeSet::getSet(it); if (!repSet.empty()) { - Trace("model-builder") << "Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl; + Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl; Assert(false); } }