* removing rewriteEquality from the rewriter

* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized 

16 files changed, 35 insertions, 99 deletions

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 748ed8686..c32cc0e56 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -34,10 +34,6 @@ public:
 
   static RewriteResponse preRewrite(TNode n);
   static RewriteResponse postRewrite(TNode n);
-  static Node rewriteEquality(TNode equality) {
-    // Arithmetic owns the domain, so this is totally ok
-    return Rewriter::rewrite(equality);
-  }
 
   static void init() { }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 1bf42a105..25797dda3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -271,16 +271,14 @@ class TheoryArrays : public Theory {
           }
         }
         // Propagate equality between shared terms
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality);
+        return d_arrays.propagate(t1.eqNode(t2));
       } else {
         if (t1.getType().isArray()) {
           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
             return true;
           }
         }
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality.notNode());
+        return d_arrays.propagate(t1.eqNode(t2).notNode());
       }
       return true;
     }
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 627f34a30..c6ef5cd25 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -109,10 +109,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static Node rewriteEquality(TNode node) {
-    return postRewrite(node).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index d26a4d478..6771f775c 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -37,11 +37,6 @@ public:
     return preRewrite(node);
   }
 
-  static Node rewriteEquality(TNode node) {
-    Unreachable();
-    return node;
-  }
-
   static void init() {}
   static void shutdown() {}
 
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index e299f84e7..acf535388 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -48,11 +48,6 @@ public:
     }
   }
 
-  static inline Node rewriteEquality(TNode equality) {
-    Unreachable();
-    return equality;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 5bb906841..a9c6d2676 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -94,17 +94,15 @@ void Bitblaster::bbAtom(TNode node) {
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
-  Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
+  Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
   // asserting that the atom is true iff the definition holds
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
-  // do boolean simplifications if possible
-  Node rewritten = Rewriter::rewrite(atom_definition);
 
   if (!Options::current()->bitvectorEagerBitblast) {
-    d_cnfStream->convertAndAssert(rewritten, true, false);
+    d_cnfStream->convertAndAssert(atom_definition, true, false);
     d_bitblastedAtoms.insert(node);
   } else {
-    d_bvOutput->lemma(rewritten, false);
+    d_bvOutput->lemma(atom_definition, false);
   }
 }
 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index bfd8a2897..6b885f1ed 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -84,11 +84,6 @@ public:
 
   static RewriteResponse preRewrite(TNode node);
 
-  static Node rewriteEquality(TNode node) {
-    Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
-    return postRewrite(node).node;
-  }
-
   static void init();
   static void shutdown();
   
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 124e6870d..ea1409108 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -108,10 +108,6 @@ public:
     return RewriteResponse(REWRITE_DONE, in);
   }
 
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 780409d52..71a8ea097 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -47,8 +47,6 @@ post_rewrite_calls=
 post_rewrite_get_cache=
 post_rewrite_set_cache=
 
-rewrite_equality_calls=
-
 seen_theory=false
 seen_theory_builtin=false
 
@@ -140,9 +138,6 @@ function rewriter {
   post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
 "
 
-  rewrite_equality_calls="${rewrite_equality_calls}    case ${theory_id}: return ${class}::rewriteEquality(node);
-"
-
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -235,7 +230,6 @@ for var in \
     rewriter_includes \
     pre_rewrite_calls \
     post_rewrite_calls \
-    rewrite_equality_calls \
     pre_rewrite_get_cache \
     post_rewrite_get_cache \
     pre_rewrite_set_cache \
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 8c037d30b..4f51edab8 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -65,9 +65,6 @@ private:
 public:
   static RewriteResponse preRewrite(TNode in);
   static RewriteResponse postRewrite(TNode in);
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
   static inline void init() {}
   static inline void shutdown() {}
 private:
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index e0b1458fb..8c20c84c1 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -64,15 +64,6 @@ Node Rewriter::rewrite(TNode node) {
   return rewriteTo(theory::Theory::theoryOf(node), node);
 }
 
-Node Rewriter::rewriteEquality(theory::TheoryId theoryId, TNode node) {
-  Assert(node.getKind() == kind::EQUAL);
-  Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ")"<< std::endl;
-  Node result = Rewriter::callRewriteEquality(theoryId, node);
-  Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ") => " << result << std::endl;
-  Assert(result.getKind() == kind::EQUAL || result.isConst());
-  return result;
-}
-
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
 #ifdef CVC4_ASSERTIONS
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e80606c95..4169cb9fe 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -99,12 +99,6 @@ public:
   static Node rewrite(TNode node);
 
   /**
-   * Rewrite an equality between two terms that are already in normal form, so
-   * that the equality is in theory-normal form.
-   */
-  static Node rewriteEquality(theory::TheoryId theoryId, TNode node);
-
-  /**
    * Should be called before the rewriter gets used for the first time.
    */
   static void init();
@@ -113,6 +107,8 @@ public:
    * Should be called to clean up any state.
    */
   static void shutdown();
+
+
 };/* class Rewriter */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index cd79dcd9f..9ab98168e 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -45,14 +45,6 @@ ${post_rewrite_calls}
   }
 }
 
-Node Rewriter::callRewriteEquality(theory::TheoryId theoryId, TNode node) {
-  switch(theoryId) {
-${rewrite_equality_calls}
-  default:
-    Unreachable();
-  }
-}
-
 Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
   switch(theoryId) {
 ${pre_rewrite_get_cache}
diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
index d9da095f7..3d01dc2a5 100644
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h
@@ -57,14 +57,6 @@ public:
   }
 
   /**
-   * Rewrite an equality, in case special handling is required.
-   */
-  static Node rewriteEquality(TNode equality) {
-    // often this will suffice
-    return postRewrite(equality).node;
-  }
-
-  /**
    * Initialize the rewriter.
    */
   static inline void init() {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8abc7a0e3..060d48230 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -394,7 +394,9 @@ void TheoryEngine::combineTheories() {
     Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about");
 
     // The equality in question
-    Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b));
+    Node equality = carePair.a < carePair.b ?
+        carePair.a.eqNode(carePair.b) :
+        carePair.b.eqNode(carePair.a);
 
     // Normalize the equality
     Node normalizedEquality = Rewriter::rewrite(equality);
@@ -862,33 +864,41 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     }
     return;
   }
-  
-  // We are left with internal distribution of shared literals
-  Assert(atom.getKind() == kind::EQUAL);
-  Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom);
-  Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
-  
-  // If we normalize to true or false, it's a special case
-  if (normalizedAtom.isConst()) {
-    if (polarity == normalizedAtom.getConst<bool>()) {
-      // Trivially true, just ignore
-      return;
+
+  // See if it rewrites to true or false directly
+  Node normalizedLiteral = Rewriter::rewrite(assertion);
+  if (normalizedLiteral.isConst()) {
+    if (normalizedLiteral.getConst<bool>()) {
+      // trivially true, but theories need to share even trivially true facts
+      // unless of course it is the theory that normalized it
+      if (Theory::theoryOf(atom) == toTheoryId) {
+      	return;
+      }
     } else {
       // Mark the propagation for explanations
-      if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
+      if (markPropagation(normalizedLiteral, assertion, toTheoryId, fromTheoryId)) {
         // Get the explanation (conflict will figure out where it came from)
-        conflict(normalizedAssertion, toTheoryId);
+        conflict(normalizedLiteral, toTheoryId);
       } else {
         Unreachable();
       }
       return;
     }
   }
-  
-  // Try and assert
+
+  // Normalize to lhs < rhs
+  Assert(atom.getKind() == kind::EQUAL);
+  Assert(atom[0] != atom[1]);
+  Node normalizedAtom = atom;
+  if (atom[0] > atom[1]) {
+    normalizedAtom = atom[1].eqNode(atom[0]);
+  }
+  Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
+
+  // Try and assert (note that we assert the non-normalized one)
   if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
     // Check if has been pre-registered with the theory
-    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId;
+    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId;
     // Assert away
     theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered);
     d_factsAsserted = true;
@@ -1139,9 +1149,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Assert(properConflict(fullConflict));
     lemma(fullConflict, true, true);
   } else {
-    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "):" << std::endl;
-
     // When only one theory, the conflict should need no processing
+    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl;
     Assert(properConflict(conflict));
     lemma(conflict, true, true);
   }
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index be4906ab6..8ba39f372 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -54,10 +54,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}