Fix for iff terms over equalities between the same term and differing constants.

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 967126da188cf0b357614f76beafc6c2431a7f16..7a4e91035adea8b6980a071cabcbab53d5235fef 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -118,29 +118,60 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
       // IFF x (NOT x)
       return RewriteResponse(REWRITE_DONE, ff);
+    } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) {
+      // a : (= i x)
+      // i : (= j k)
+      // x : (= y z)
+
+      // assume wlog k, z are constants and j is the same symbol as y
+      // (iff (= j k) (= j z))
+      // if k = z
+      //  then (iff (= j k) (= j k)) => true
+      // else
+      //  (iff (= j k) (= j z)) <=> b
+      //  b : (and (not (= j k)) (not (= j z)))
+      //  (= j k) (= j z) | a b
+      //  f       f       | t t
+      //  f       t       | f f
+      //  t       f       | f f
+      //  t       t       | * f
+      // * j cannot equal both k and z in a theory model
+      TNode t,c;
+      if (n[0][0].isConst()) {
+        c = n[0][0];
+        t = n[0][1];
+      }
+      else if (n[0][1].isConst()) {
+        c = n[0][1];
+        t = n[0][0];
+      }
+      bool matchesForm = false;
+      bool constantsEqual = false;
+      if (!c.isNull()) {
+        if (n[1][0] == t && n[1][1].isConst()) {
+          matchesForm = true;
+          constantsEqual = (n[1][1] == c);
+        }
+        else if (n[1][1] == t && n[1][0].isConst()) {
+          matchesForm = true;
+          constantsEqual = (n[1][1] == c);
+        }
+      }
+      if(matchesForm){
+        if(constantsEqual){
+          return RewriteResponse(REWRITE_DONE, tt);
+        }else{
+          Cardinality kappa = t.getType().getCardinality();
+          Cardinality two(2l);
+          if(kappa.knownLessThanOrEqual(two)){
+            return RewriteResponse(REWRITE_DONE, ff);
+          }else{
+            Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode());
+            return RewriteResponse(REWRITE_AGAIN, neitherEquality);
+          }
+        }
+      }
     }
-    // This is wrong: it would rewrite c1 == x <=> c2 == x to false
-    // when this is sat for x = c3 where c3 is different from c1, and c2
-    
-    // else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) {
-    //   TNode t,c;
-    //   if (n[0][0].isConst()) {
-    //     c = n[0][0];
-    //     t = n[0][1];
-    //   }
-    //   else if (n[0][1].isConst()) {
-    //     c = n[0][1];
-    //     t = n[0][0];
-    //   }
-    //   if (!c.isNull()) {
-    //     if (n[1][0] == t && n[1][1].isConst()) {
-    //       return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff);
-    //     }
-    //     else if (n[1][1] == t && n[1][0].isConst()) {
-    //       return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff);
-    //     }
-    //   }
-    // }
     break;
   }
   case kind::XOR: {

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 8abaa5611b44c956a4cbe76d28cf17b324e613be..36f09f137c0f9c66cfe948d5a67d0a370e39aa59 100644 (file)
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -193,6 +193,10 @@ Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) co
   Unreachable();
 }
 
+bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const throw() {
+  CardinalityComparison cmp = this->compare(c);
+  return cmp == LESS || cmp == EQUAL;
+}
 
 std::string Cardinality::toString() const throw() {
   std::stringstream ss;

diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index c536ea065671a42d0028f431187b7a29905c2d32..c9d051c9e162bcbfa4dc3a1bd42419594a4f031c 100644 (file)
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -245,6 +245,11 @@ public:
    */
   std::string toString() const throw();
 
+  /**
+   * Compare two cardinalities and if it is known that the current
+   * cardinality is smaller or equal to c, it returns true.
+   */
+  bool knownLessThanOrEqual(const Cardinality& c) const throw();
 };/* class Cardinality */
 
 

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 48ac972940892ea4911afaf63473d76f37bf17ea..b1e2f64919be38166ead3a74040f489654be18a7 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -37,7 +37,8 @@ SMT_TESTS = \
        simple2.smt \
        simple-lra.smt \
        simple-rdl.smt \
-       simple-uf.smt
+       simple-uf.smt \
+       constant-rewrite.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = \

diff --git a/test/regress/regress0/constant-rewrite.smt b/test/regress/regress0/constant-rewrite.smt
new file mode 100644 (file)
index 0000000..b70b53b
--- /dev/null
+++ b/test/regress/regress0/constant-rewrite.smt
@@ -0,0 +1,12 @@
+(benchmark ConstantRewrite
+:logic QF_LRA
+:status sat
+:extrafuns ((v0 Real))
+:formula
+(and
+ (not (<= v0 0))
+ (not (iff (= v0 0)
+           (= v0 (/ 1 2))))
+ )
+)
+