From cba10a096d97e82bd112b4d99a6ebe399d1369d6 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 1 Apr 2013 15:39:25 -0400
Subject: [PATCH] Fix for iff terms over equalities between the same term and
 differing constants.

---
 src/theory/booleans/theory_bool_rewriter.cpp | 75 ++++++++++++++------
 src/util/cardinality.cpp                     |  4 ++
 src/util/cardinality.h                       |  5 ++
 test/regress/regress0/Makefile.am            |  3 +-
 test/regress/regress0/constant-rewrite.smt   | 12 ++++
 5 files changed, 76 insertions(+), 23 deletions(-)
 create mode 100644 test/regress/regress0/constant-rewrite.smt

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 967126da1..7a4e91035 100644
--- 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 8abaa5611..36f09f137 100644
--- 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 c536ea065..c9d051c9e 100644
--- 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 48ac97294..b1e2f6491 100644
--- 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
index 000000000..b70b53bec
--- /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))))
+ )
+)
+
-- 
2.30.2