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/mkrewriter | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'src/theory/mkrewriter')

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