From 724c1acc2238ea1ab9821609b6fe7eae3bd07a94 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:34:54 -0800
Subject: [PATCH] [sledge] Add Theory.solvables

Reviewed By: jvillard

Differential Revision: D25883730

fbshipit-source-id: 793250146
---
 sledge/src/fol/theory.ml  | 23 +++++++++++++++++++++--
 sledge/src/fol/theory.mli | 20 ++++++++++++++++++++
 2 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index 56cb7325b..04098ff37 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -53,6 +53,25 @@ let classify e =
 let is_interpreted e = equal_kind (classify e) InterpApp
 let is_uninterpreted e = equal_kind (classify e) UninterpApp
 
+let is_noninterpreted e =
+  match classify e with
+  | InterpAtom | InterpApp -> false
+  | NonInterpAtom | UninterpApp -> true
+
+let rec solvables e =
+  match classify e with
+  | InterpAtom -> Iter.empty
+  | InterpApp -> solvable_trms e
+  | NonInterpAtom | UninterpApp -> Iter.return e
+
+and solvable_trms e = Iter.flat_map ~f:solvables (Trm.trms e)
+
+let rec map_solvables e ~f =
+  match classify e with
+  | InterpAtom -> e
+  | NonInterpAtom | UninterpApp -> f e
+  | InterpApp -> Trm.map ~f:(map_solvables ~f) e
+
 (* Solving equations ======================================================*)
 
 (** prefer representative terms that are minimal in the order s.t. Var <
@@ -231,6 +250,6 @@ let solve d e s =
    *)
   (* r = v ==> v ↦ r *)
   | Some (rep, var) ->
-      assert (not (is_interpreted var)) ;
-      assert (not (is_interpreted rep)) ;
+      assert (is_noninterpreted var) ;
+      assert (is_noninterpreted rep) ;
       add_solved ~var ~rep s
diff --git a/sledge/src/fol/theory.mli b/sledge/src/fol/theory.mli
index 4de53e50b..3323e10a8 100644
--- a/sledge/src/fol/theory.mli
+++ b/sledge/src/fol/theory.mli
@@ -16,10 +16,30 @@ type t =
 
 val pp : t pp
 
+val solvables : Trm.t -> Trm.t iter
+(** The maximal noninterpreted terms (according to {!is_noninterpreted})
+    occurring in a term. Note that for noninterpreted terms, this is the
+    single term itself. *)
+
+val solvable_trms : Trm.t -> Trm.t iter
+(** The solvables of immediate subterms. That is, maximal noninterpreted
+    strict subterms. *)
+
+val map_solvables : Trm.t -> f:(Trm.t -> Trm.t) -> Trm.t
+(** Map over the {!solvables}. *)
+
 type kind = InterpApp | NonInterpAtom | InterpAtom | UninterpApp
 [@@deriving compare, equal]
 
 val classify : Trm.t -> kind
+
+val is_noninterpreted : Trm.t -> bool
+(** Test if a term is either a variable ({!Trm.Var}) or an uninterpreted
+    function symbol application ({!Trm.Apply} or {!Trm.Arith} when
+    [{!Trm.Arith.classify} a = Uninterpreted]). That is, is not an
+    interpreted function symbol application (including constants and nullary
+    applications). *)
+
 val is_interpreted : Trm.t -> bool
 val is_uninterpreted : Trm.t -> bool
 val prefer : Trm.t -> Trm.t -> int