[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

@@ -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