diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-11-25 15:21:40 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-11-25 15:21:40 -0800 |
commit | a68c6b065b569c3094a08b0dbf64a263454b006d (patch) | |
tree | b8f7e2166625891356206e0dbbcbea0583c2c017 /src/theory/arrays | |
parent | 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff) |
Array collectModelInfo fix for Andy
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 47 |
1 files changed, 30 insertions, 17 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 98346d0e3..76e48aa1d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -813,27 +813,40 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) for (size_t i=0; i<arrays.size(); ++i) { TNode n = arrays[i]; - // Compute default value for this array - there is one default value for every mayEqual equivalence class - d_mayEqualEqualityEngine.addTerm(n); // add the term in case it isn't there already - TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n); - it = defValues.find(mayRep); - // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type - if (it == defValues.end()) { - TypeNode valueType = n.getType().getArrayConstituentType(); - rep = defaultValuesSet.nextTypeEnum(valueType); - if (rep.isNull()) { - Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end()); - rep = *(defaultValuesSet.getSet(valueType)->begin()); - } - Trace("arrays-models") << "New default value = " << rep << endl; - defValues[mayRep] = rep; + if (fullModel) { + // Compute default value for this array - there is one default value for every mayEqual equivalence class + d_mayEqualEqualityEngine.addTerm(n); // add the term in case it isn't there already + TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n); + it = defValues.find(mayRep); + // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type + if (it == defValues.end()) { + TypeNode valueType = n.getType().getArrayConstituentType(); + rep = defaultValuesSet.nextTypeEnum(valueType); + if (rep.isNull()) { + Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end()); + rep = *(defaultValuesSet.getSet(valueType)->begin()); + } + Trace("arrays-models") << "New default value = " << rep << endl; + defValues[mayRep] = rep; + } + else { + rep = (*it).second; + } + + // Build the STORE_ALL term with the default value + rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr())); } else { - rep = (*it).second; + std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); + if (it == d_skolemCache.end()) { + rep = nm->mkSkolem("array_collect_model_var_$$", n.getType(), "base model variable for array collectModelInfo"); + d_skolemCache[n] = rep; + } + else { + rep = (*it).second; + } } - // Build the STORE_ALL term with the default value - rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr())); // For each read, require that the rep stores the right value vector<Node>& reads = selects[n]; for (unsigned j = 0; j < reads.size(); ++j) { |