From: Clark Barrett <barrett@cs.nyu.edu>
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;
     }