From 2a6c24b3615abbb25f1f582294f3ff49b6f7d4a2 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 17 May 2021 14:51:19 -0700
Subject: [PATCH] Recognize rewrite rules using `intEq` and `intModEq`
 relations.

This is a band-aid pending a proper solution for #1261.
---
 saw-core/src/Verifier/SAW/Rewriter.hs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 6db48c95b0..b402df2964 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -281,6 +281,12 @@ vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq"
 equalNatIdent :: Ident
 equalNatIdent = mkIdent (mkModuleName ["Prelude"]) "equalNat"
 
+intEqIdent :: Ident
+intEqIdent = mkIdent (mkModuleName ["Prelude"]) "intEq"
+
+intModEqIdent :: Ident
+intModEqIdent = mkIdent (mkModuleName ["Prelude"]) "intModEq"
+
 -- | Converts a universally quantified equality proposition from a
 -- Term representation to a RewriteRule.
 ruleOfTerm :: Term -> RewriteRule
@@ -307,7 +313,7 @@ rulePermutes lhs rhs =
 
 mkRewriteRule :: [Term] -> Term -> Term  -> RewriteRule
 mkRewriteRule c l r =
-    RewriteRule {ctxt = c, lhs = l, rhs = r , permutative = rulePermutes l r} 
+    RewriteRule {ctxt = c, lhs = l, rhs = r , permutative = rulePermutes l r}
 
 -- | Converts a universally quantified equality proposition between the
 -- two given terms to a RewriteRule.
@@ -333,6 +339,10 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) =
   Just $ mkRewriteRule [] x y
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) =
   Just $ mkRewriteRule [] x y
+ruleOfProp (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) =
+  Just $ mkRewriteRule [] x y
+ruleOfProp (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) =
+  Just $ mkRewriteRule [] x y
 ruleOfProp (unwrapTermF -> Constant _ body) = ruleOfProp body
 ruleOfProp (R.asEq -> Just (_, x, y)) =
   Just $ mkRewriteRule [] x y