diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-16 00:49:04 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-16 00:49:04 +0000 |
commit | fbf887ef14272a13bf1413704d080e8496321338 (patch) | |
tree | c06172f06dbd24b0484710be95d45b630ffb096f /src | |
parent | c00efa92e9d61d808a8346e1d8bb3523e24d8ee2 (diff) |
store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/model.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 62327e4dc..c4fc0310c 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -425,10 +425,17 @@ Node DefaultModel::getInterpretedValue( TNode n ){ } } if( !ret.isNull() ){ + Node prev = n; //store the equality assertEquality( n, ret, true ); - //this is dangerous since it may cause representatives to change - Assert( getRepresentative( ret )==ret ); + //add it to the map of representatives + n = d_equalityEngine.getRepresentative( n ); + if( d_reps.find( n )==d_reps.end() ){ + d_reps[n] = ret; + } + //TODO: make sure that this doesn't affect the representatives in the equality engine + // in other words, we need to be sure that all representatives of the equality engine + // are still representatives after this function, or else d_reps should be modified. return ret; }else{ //otherwise, just return itself (this usually should not happen) |