From 7595b05f3918c66593f84ffa37bec512a9c491b6 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 19 Mar 2019 09:26:42 -0700
Subject: [PATCH] [sledge] Classify Eq and Dq exps as Interpreted

Summary:
Eq and Dq expressions are interpreted by Equality and Exp, rather than
being considered uninterpreted functions. Classifying them as
interpreted results in stronger Equality normalization.

Reviewed By: mbouaziz

Differential Revision: D14495817

fbshipit-source-id: 44bb376c0
---
 sledge/src/llair/exp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 5078944d8..06737d336 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -1290,7 +1290,7 @@ let rec is_constant e =
   | _ -> true
 
 let classify = function
-  | Add _ | Mul _ -> `Interpreted
+  | Add _ | Mul _ | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Interpreted
   | App _ -> `Uninterpreted
   | _ -> `Atomic