[sledge] Update stale comment

Summary:
This has been out of date since arithmetic was changed from a purely
uninterpreted treatment to having a solver.

Reviewed By: jvillard

Differential Revision: D16985159

fbshipit-source-id: 39e42069c

sledge/src/llair/exp.mli

@@ -10,16 +10,11 @@
     Pure (heap-independent) expressions are complex arithmetic,
     bitwise-logical, etc. operations over literal values and registers.
 
-    Expressions are represented in curried form, where the only† recursive
+    Expressions for operations that are uninterpreted in the analyzer are
-    constructor is [App], which is an application of a function symbol to an
+    represented in curried form, where [App] is an application of a function
-    argument. This is done to simplify the definition of 'subexpression' and
+    symbol to an argument. This is done to simplify the definition of
-    make it explicit, which is a significant help for treating equality
+    'subexpression' and make it explicit. The specific constructor functions
-    between expressions using congruence closure. The specific constructor
+    indicate and check the expected arity of the function symbols. *)
-    functions indicate and check the expected arity of the function symbols.
-
-    [†] [Struct_rec] is also a recursive constructor, but its values are
-    treated as atomic since, as they are recursive, doing otherwise would
-    require inductive reasoning. *)
 
 type comparator_witness