From 6b32a003df947b27ff3bdeaf9d48b911ce3d784c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 9 Apr 2021 08:13:35 -0700
Subject: [PATCH] [sledge] Use fresh var for length when extracting from a
 variable
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
When solving equations such as `α[o,l) = β`, the memory theory solver
computes a term to represent the length of α. This fails if α is a
variable (which might itself be equal to a sized term elsewhere in the
formula). This diff fixes such failures by generating a fresh variable
for the length in such situations.

Reviewed By: ngorogiannis

Differential Revision: D27564871

fbshipit-source-id: e5e066b77
---
 sledge/src/fol/theory.ml | 35 ++++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index 4fe6e1eea..a47ce9592 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -135,23 +135,23 @@ let solve_extract a o l b s =
   [%trace]
     ~call:(fun {pf} ->
       pf "@ %a = %a" Trm.pp (Trm.extract ~seq:a ~off:o ~len:l) Trm.pp b )
-    ~retn:(fun {pf} -> pf "%a" pp)
+    ~retn:(fun {pf} -> pf "%a" (Option.pp "%a" pp))
   @@ fun () ->
-  match fresh "c" s with
-  | None -> s
-  | Some (c, s) ->
-      let n = Trm.seq_size_exn a in
-      let n_c = Trm.sized ~siz:n ~seq:c in
-      let o_l = Trm.add o l in
-      let n_o_l = Trm.sub n o_l in
-      let c0 = Trm.extract ~seq:n_c ~off:Trm.zero ~len:o in
-      let c1 = Trm.extract ~seq:n_c ~off:o_l ~len:n_o_l in
-      let b, s =
-        match Trm.seq_size b with
-        | None -> (Trm.sized ~siz:l ~seq:b, s)
-        | Some m -> (b, add_pending l m s)
-      in
-      add_pending a (Trm.concat [|c0; b; c1|]) s
+  let* c, s = fresh "c" s in
+  let+ n, s =
+    match Trm.seq_size a with Some n -> Some (n, s) | None -> fresh "n" s
+  in
+  let n_c = Trm.sized ~siz:n ~seq:c in
+  let o_l = Trm.add o l in
+  let n_o_l = Trm.sub n o_l in
+  let c0 = Trm.extract ~seq:n_c ~off:Trm.zero ~len:o in
+  let c1 = Trm.extract ~seq:n_c ~off:o_l ~len:n_o_l in
+  let b, s =
+    match Trm.seq_size b with
+    | None -> (Trm.sized ~siz:l ~seq:b, s)
+    | Some m -> (b, add_pending l m s)
+  in
+  add_pending a (Trm.concat [|c0; b; c1|]) s
 
 (* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ …
    where nₓ ≡ |αₓ| and m = |β| *)
@@ -221,7 +221,8 @@ let solve d e s =
         (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
         add_solved ~var:e ~rep:(Trm.sized ~siz:l ~seq:v) s
   (* α[o,l) = β ==> … ∧ α = _^β^_ *)
-  | Some (Extract {seq= a; off= o; len= l}, e) -> solve_extract a o l e s
+  | Some (Extract {seq= a; off= o; len= l}, e) ->
+      Option.value (solve_extract a o l e s) ~default:s
   (*
    * Sized
    *)