diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
commit | b4c7be882b88c6741212ecd9c6be4e91fec76087 (patch) | |
tree | 0f96427e0e6f84ff6ac60ac81ff6f13459515295 /src/theory/arrays | |
parent | ea514f2aa787998ac31f8546bd202890f6bac056 (diff) |
Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8f1ba5fca..631785437 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1133,7 +1133,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) TypeSet defaultValuesSet; // Compute all default values already in use - if (fullModel) { + //if (fullModel) { for (size_t i=0; i<arrays.size(); ++i) { TNode nrep = d_equalityEngine.getRepresentative(arrays[i]); d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already @@ -1143,14 +1143,14 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second); } } - } + //} // Loop through all array equivalence classes that need a representative computed for (size_t i=0; i<arrays.size(); ++i) { TNode n = arrays[i]; TNode nrep = d_equalityEngine.getRepresentative(n); - if (fullModel) { + //if (fullModel) { // Compute default value for this array - there is one default value for every mayEqual equivalence class TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep); it = d_defValues.find(mayRep); @@ -1171,6 +1171,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) // Build the STORE_ALL term with the default value rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr())); + /* } else { std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); @@ -1182,6 +1183,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) rep = (*it).second; } } +*/ // For each read, require that the rep stores the right value vector<Node>& reads = selects[nrep]; |