From: Clark Barrett Date: Mon, 8 Oct 2012 20:19:13 +0000 (+0000) Subject: Fixed problem in assertEqualityEngine: predicates that are not false are no X-Git-Tag: cvc5-1.0.0~7727 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25375067383e9c6b48ff5ec7053894987d26c331;p=cvc5.git Fixed problem in assertEqualityEngine: predicates that are not false are no longer assumed to be true --- 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; }