From ed4aac4f665ef1809fe53fdff47d7eaec14a85c6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 23 Aug 2019 07:28:36 -0700 Subject: [PATCH] [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 | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index a7edf4a6d..63ccdbaf2 100644 --- a/sledge/src/llair/exp.mli +++ b/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 - constructor is [App], which is an application of a function symbol to an - argument. This is done to simplify the definition of 'subexpression' and - make it explicit, which is a significant help for treating equality - between expressions using congruence closure. The specific constructor - 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. *) + Expressions for operations that are uninterpreted in the analyzer are + represented in curried form, where [App] is an application of a function + symbol to an argument. This is done to simplify the definition of + 'subexpression' and make it explicit. The specific constructor functions + indicate and check the expected arity of the function symbols. *) type comparator_witness