[sledge] Use fresh var for length when extracting from a variable

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

@@ -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
+  let* c, s = fresh "c" s in
-  | None -> s
+  let+ n, s =
-  | Some (c, s) ->
+    match Trm.seq_size a with Some n -> Some (n, s) | None -> fresh "n" s
-      let n = Trm.seq_size_exn a in
+  in
-      let n_c = Trm.sized ~siz:n ~seq:c in
+  let n_c = Trm.sized ~siz:n ~seq:c in
-      let o_l = Trm.add o l in
+  let o_l = Trm.add o l in
-      let n_o_l = Trm.sub n 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 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 c1 = Trm.extract ~seq:n_c ~off:o_l ~len:n_o_l in
-      let b, s =
+  let b, s =
-        match Trm.seq_size b with
+    match Trm.seq_size b with
-        | None -> (Trm.sized ~siz:l ~seq:b, s)
+    | None -> (Trm.sized ~siz:l ~seq:b, s)
-        | Some m -> (b, add_pending l m s)
+    | Some m -> (b, add_pending l m s)
-      in
+  in
-      add_pending a (Trm.concat [|c0; b; c1|]) s
+  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
    *)