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/quantifiers/quantifiers_rewriter.h | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'src/theory/quantifiers/quantifiers_rewriter.h')

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:
-- 
cgit v1.2.3