From dd713fdbc16b07adc8011dea09b53fb3bc168662 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 14 Jun 2012 01:08:11 +0000
Subject: * 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

---
 src/theory/uf/theory_uf_rewriter.h | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'src/theory/uf')

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() {}
 
-- 
cgit v1.2.3