diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-08 20:19:13 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-08 20:19:13 +0000 |
commit | 25375067383e9c6b48ff5ec7053894987d26c331 (patch) | |
tree | 58f7fa74813a4d224e8cda985ad14f50cc8bfd4a | |
parent | 2ad8e376c43eded3c9da313d372689514abe63e1 (diff) |
Fixed problem in assertEqualityEngine: predicates that are not false are no
longer assumed to be true
-rw-r--r-- | src/theory/model.cpp | 31 |
1 files changed, 20 insertions, 11 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 6a7d2ecef..d97781ab7 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -298,18 +298,27 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){ while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); bool predicate = false; - bool predPolarity = false; - if( eqc.getType().isBoolean() ){ + bool predTrue = false; + bool predFalse = false; + if (eqc.getType().isBoolean()) { predicate = true; - predPolarity = ee->areEqual( eqc, d_true ); - //FIXME: do we guarentee that all boolean equivalence classes contain either d_true or d_false? - } - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee ); - while( !eqc_i.isFinished() ){ - if( predicate ){ - assertPredicate( *eqc_i, predPolarity ); - }else{ - assertEquality( *eqc_i, eqc, true ); + predTrue = ee->areEqual(eqc, d_true); + predFalse = ee->areEqual(eqc, d_false); + } + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + while(!eqc_i.isFinished()) { + if (predicate) { + if (predTrue) { + assertPredicate(*eqc_i, true); + } + else if (predFalse) { + assertPredicate(*eqc_i, false); + } + else { + d_equalityEngine.addTerm(*eqc_i); + } + } else { + assertEquality(*eqc_i, eqc, true); } ++eqc_i; } |