diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
commit | c3e9112157320111c18b2984052abd9cd17127dc (patch) | |
tree | 1fa4ff944c86630034357994dd602486f609899e /src/theory/arrays | |
parent | c33c9d3699597abe2fbeaacb6799ba05f11f8e93 (diff) |
New model code, mostly workin
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 79 |
1 files changed, 51 insertions, 28 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e1f93158f..63b61995a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -628,47 +628,70 @@ void TheoryArrays::computeCareGraph() void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); - //must determine proper representatives for all array equivalence classes - //first, we collect all select terms and array equivalence classes - std::map< Node, std::vector< Node > > selects; - std::vector< Node > arrays; + + std::map<Node, std::vector<Node> > selects; + std::vector<Node> arrays; + + // Go through all equivalence classes eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + bool isArray, computeRep; while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( eqc.getType().isArray() ){ - arrays.push_back( eqc ); - } + isArray = eqc.getType().isArray(); + computeRep = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; - if( n.getKind()==kind::SELECT ){ - selects[ n[0] ].push_back( n ); + // 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) { + arrays.push_back(eqc); + computeRep = true; + } + // If this term is a select, record that the EC rep of its store parameter is being read from using this term + if (n.getKind()==kind::SELECT) { + selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++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; } - //for all array equivalence classes - for( size_t i=0; i<arrays.size(); i++ ){ - ArrayModel am( arrays[i], m ); - //set all values from existing select terms - eq::EqClassIterator eqc_i = eq::EqClassIterator( arrays[i], &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){ - am.setValue( m, selects[ *eqc_i ][i][1], selects[ *eqc_i ][i] ); - } - ++eqc_i; + + NodeManager* nm = NodeManager::currentNM(); + Node rep; + map<Node, Node> defValues; + map<Node, Node>::iterator it; + TypeSet defaultValuesSet; + + // Loop through all array equivalence classes that need a representative computed + 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 + 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); + defValues[mayRep] = rep; + } + else { + rep = (*it).second; } - if( fullModel ){ - ////choose a representative as the default array - //am.setDefaultArray( ... ); + // 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) { + rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]); } - //construct the representative - Node rep = am.getArrayValue(); - Assert( !rep.isNull() ); - m->assertEquality( arrays[i], rep, true ); - //communicate to the model that it is the representative - m->assertRepresentative( rep ); + m->assertEquality(n, rep, true); + m->assertRepresentative(rep); } } |