From caae7515e85bcf65a08eac4dc372ee0e6d95ebe6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:32:43 -0800 Subject: [PATCH] [sledge] Rework first-order solver to use a list of pending equations Summary: Currently when solving an equation requires solving one or more other equations, they are handled recursively. This diff reworks the solver to instead queue pending equations in a list rather than eagerly solving them eagerly. The pending list will be needed when changing the Context.t representation since some equations will need to be delayed until representation invariants are re-established. Additionally, the solution is accumulated as an association list rather than being eagerly incorporated into the context representation. This enables the uses in equality solving and quantifier elimination to use different representations. Reviewed By: jvillard Differential Revision: D25883727 fbshipit-source-id: 2f6b5efa3 --- sledge/src/fol/context.ml | 359 ++++++++++++++++++-------------- sledge/src/test/context_test.ml | 37 ++-- sledge/src/test/fol_test.ml | 34 +-- sledge/src/test/sh_test.ml | 18 +- 4 files changed, 248 insertions(+), 200 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 4eef404b6..0d641ec05 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -9,7 +9,7 @@ open Exp -(** Classification of Terms by Theory *) +(* Classification of Terms ================================================*) type kind = Interpreted | Atomic | Uninterpreted [@@deriving compare, equal] @@ -34,7 +34,8 @@ let rec max_solvables e = let fold_max_solvables e s ~f = Iter.fold ~f (max_solvables e) s -(** Solution Substitutions *) +(* Solution Substitutions =================================================*) + module Subst : sig type t [@@deriving compare, equal, sexp] @@ -58,7 +59,6 @@ module Subst : sig val extend : Trm.t -> t -> t option val map_entries : f:(Trm.t -> Trm.t) -> t -> t val to_iter : t -> (Trm.t * Trm.t) iter - val fv : t -> Var.Set.t val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t (* direct representation manipulation *) @@ -84,14 +84,6 @@ end = struct let for_alli = Trm.Map.for_alli let to_iter = Trm.Map.to_iter - let vars s = - s - |> to_iter - |> Iter.flat_map ~f:(fun (k, v) -> - Iter.append (Trm.vars k) (Trm.vars v) ) - - let fv s = Var.Set.of_iter (vars s) - (** look up a term in a substitution *) let apply s a = Trm.Map.find a s |> Option.value ~default:a @@ -126,7 +118,7 @@ end = struct | _ when Trm.equal key data -> r | _ -> assert ( - (not (Trm.Map.mem key r)) + Option.for_all ~f:(Trm.equal key) (Trm.Map.find key r) || fail "domains intersect: %a" Trm.pp key () ) ; let s = Trm.Map.singleton key data in let r' = Trm.Map.map_endo ~f:(norm s) r in @@ -208,7 +200,7 @@ end = struct let remove = Trm.Map.remove end -(** Theory Solver *) +(* Theory Solver ==========================================================*) (** prefer representative terms that are minimal in the order s.t. Var < Sized < Extract < Concat < others, then using height of sequence @@ -235,155 +227,163 @@ let orient e f = | Zero -> None | Pos -> Some (f, e) -let norm (_, _, s) e = Subst.norm s e - -let compose1 ~var ~rep (us, xs, s) = - let s = Subst.compose1 ~key:var ~data:rep s in - Some (us, xs, s) - -let fresh name (wrt, xs, s) = - let x, wrt = Var.fresh name ~wrt in - let xs = Var.Set.add x xs in - (Trm.var x, (wrt, xs, s)) +type solve_state = + { wrt: Var.Set.t + ; no_fresh: bool + ; fresh: Var.Set.t + ; solved: (Trm.t * Trm.t) list option + ; pending: (Trm.t * Trm.t) list } + +let pp_solve_state ppf = function + | {solved= None} -> Format.fprintf ppf "unsat" + | {solved= Some solved; fresh; pending} -> + Format.fprintf ppf "%a%a : %a" Var.Set.pp_xs fresh + (List.pp ";@ " (fun ppf (var, rep) -> + Format.fprintf ppf "@[%a ↦ %a@]" Trm.pp var Trm.pp rep )) + solved + (List.pp ";@ " (fun ppf (a, b) -> + Format.fprintf ppf "@[%a = %a@]" Trm.pp a Trm.pp b )) + pending + +let add_solved ~var ~rep s = + match s with + | {solved= None} -> s + | {solved= Some solved} -> {s with solved= Some ((var, rep) :: solved)} + +let add_pending a b s = {s with pending= (a, b) :: s.pending} + +let fresh name s = + if s.no_fresh then None + else + let x, wrt = Var.fresh name ~wrt:s.wrt in + let fresh = Var.Set.add x s.fresh in + Some (Trm.var x, {s with wrt; fresh}) let solve_poly p q s = [%trace] ~call:(fun {pf} -> pf "@ %a = %a" Trm.pp p Trm.pp q) - ~retn:(fun {pf} -> function - | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s - | None -> pf "false" ) + ~retn:(fun {pf} -> pf "%a" pp_solve_state) @@ fun () -> match Trm.sub p q with - | Z z -> if Z.equal Z.zero z then Some s else None - | Var _ as var -> compose1 ~var ~rep:Trm.zero s + | Z z -> if Z.equal Z.zero z then s else {s with solved= None} + | Var _ as var -> add_solved ~var ~rep:Trm.zero s | p_q -> ( match Trm.Arith.solve_zero_eq p_q with | Some (var, rep) -> - compose1 ~var:(Trm.arith var) ~rep:(Trm.arith rep) s - | None -> compose1 ~var:p_q ~rep:Trm.zero s ) + add_solved ~var:(Trm.arith var) ~rep:(Trm.arith rep) s + | None -> add_solved ~var:p_q ~rep:Trm.zero s ) (* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n = |α| and c fresh *) -let rec solve_extract ?(no_fresh = false) a o l b s = +let solve_extract a o l b s = [%trace] ~call:(fun {pf} -> - pf "@ %a = %a@ %a%a" Trm.pp - (Trm.extract ~seq:a ~off:o ~len:l) - Trm.pp b Var.Set.pp_xs (snd3 s) Subst.pp (trd3 s) ) - ~retn:(fun {pf} -> function - | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s - | None -> pf "false" ) + pf "@ %a = %a" Trm.pp (Trm.extract ~seq:a ~off:o ~len:l) Trm.pp b ) + ~retn:(fun {pf} -> pf "%a" pp_solve_state) @@ fun () -> - if no_fresh then Some s - else - let n = Trm.seq_size_exn a in - let c, s = fresh "c" 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, Some s) - | Some m -> (b, solve_ l m s) - in - s >>= solve_ a (Trm.concat [|c0; b; c1|]) + 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 (* α₀^…^αᵢ^αⱼ^…^αᵥ = β ==> |α₀^…^αᵥ| = |β| ∧ … ∧ αⱼ = β[n₀+…+nᵢ,nⱼ) ∧ … where nₓ ≡ |αₓ| and m = |β| *) -and solve_concat ?no_fresh a0V b m s = +let solve_concat a0V b m s = [%trace] - ~call:(fun {pf} -> - pf "@ %a = %a@ %a%a" Trm.pp (Trm.concat a0V) Trm.pp b Var.Set.pp_xs - (snd3 s) Subst.pp (trd3 s) ) - ~retn:(fun {pf} -> function - | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s - | None -> pf "false" ) + ~call:(fun {pf} -> pf "@ %a = %a" Trm.pp (Trm.concat a0V) Trm.pp b) + ~retn:(fun {pf} -> pf "%a" pp_solve_state) @@ fun () -> - Iter.fold_until (Array.to_iter a0V) (s, Trm.zero) - ~f:(fun aJ (s, oI) -> - let nJ = Trm.seq_size_exn aJ in - let oJ = Trm.add oI nJ in - match solve_ ?no_fresh aJ (Trm.extract ~seq:b ~off:oI ~len:nJ) s with - | Some s -> `Continue (s, oJ) - | None -> `Stop None ) - ~finish:(fun (s, n0V) -> solve_ ?no_fresh n0V m s) - -and solve_ ?no_fresh d e s = - [%Trace.call fun {pf} -> - pf "@ %a@[%a@ %a@ %a@]" Var.Set.pp_xs (snd3 s) Trm.pp d Trm.pp e - Subst.pp (trd3 s)] - ; - ( match orient (norm s d) (norm s e) with + let s, n0V = + Iter.fold (Array.to_iter a0V) (s, Trm.zero) ~f:(fun aJ (s, oI) -> + let nJ = Trm.seq_size_exn aJ in + let oJ = Trm.add oI nJ in + let s = add_pending aJ (Trm.extract ~seq:b ~off:oI ~len:nJ) s in + (s, oJ) ) + in + add_pending n0V m s + +let solve_ d e s = + [%trace] + ~call:(fun {pf} -> pf "@ %a = %a" Trm.pp d Trm.pp e) + ~retn:(fun {pf} -> pf "%a" pp_solve_state) + @@ fun () -> + match orient d e with (* e' = f' ==> true when e' ≡ f' *) - | None -> Some s + | None -> s (* i = j ==> false when i ≠ j *) - | Some (Z _, Z _) | Some (Q _, Q _) -> None + | Some (Z _, Z _) | Some (Q _, Q _) -> {s with solved= None} (* * Concat *) (* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *) | Some (Sized {siz= n; seq= a}, b) when n == Trm.zero -> s - |> solve_ ?no_fresh a (Trm.concat [||]) - >>= solve_ ?no_fresh b (Trm.concat [||]) + |> add_pending a (Trm.concat [||]) + |> add_pending b (Trm.concat [||]) | Some (b, Sized {siz= n; seq= a}) when n == Trm.zero -> s - |> solve_ ?no_fresh a (Trm.concat [||]) - >>= solve_ ?no_fresh b (Trm.concat [||]) + |> add_pending a (Trm.concat [||]) + |> add_pending b (Trm.concat [||]) (* ⟨n,0⟩ = α₀^…^αᵥ ==> … ∧ αⱼ = ⟨n,0⟩[n₀+…+nᵢ,nⱼ) ∧ … *) | Some ((Sized {siz= n; seq} as b), Concat a0V) when seq == Trm.zero -> - solve_concat ?no_fresh a0V b n s + solve_concat a0V b n s (* ⟨n,e^⟩ = α₀^…^αᵥ ==> … ∧ αⱼ = ⟨n,e^⟩[n₀+…+nᵢ,nⱼ) ∧ … *) | Some ((Sized {siz= n; seq= Splat _} as b), Concat a0V) -> - solve_concat ?no_fresh a0V b n s + solve_concat a0V b n s | Some ((Var _ as v), (Concat a0V as c)) -> if not (Var.Set.mem (Var.of_ v) (Trm.fv c)) then (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *) - compose1 ~var:v ~rep:c s + add_solved ~var:v ~rep:c s else (* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^αᵥ when v ∈ fv(α₀^…^αᵥ) *) let m = Trm.seq_size_exn c in - solve_concat ?no_fresh a0V (Trm.sized ~siz:m ~seq:v) m s + solve_concat a0V (Trm.sized ~siz:m ~seq:v) m s (* α₀^…^αᵥ = β₀^…^βᵤ ==> … ∧ αⱼ = (β₀^…^βᵤ)[n₀+…+nᵢ,nⱼ) ∧ … *) | Some (Concat a0V, (Concat _ as c)) -> - solve_concat ?no_fresh a0V c (Trm.seq_size_exn c) s + solve_concat a0V c (Trm.seq_size_exn c) s (* α[o,l) = α₀^…^αᵥ ==> … ∧ αⱼ = α[o,l)[n₀+…+nᵢ,nⱼ) ∧ … *) - | Some ((Extract {len= l} as e), Concat a0V) -> - solve_concat ?no_fresh a0V e l s + | Some ((Extract {len= l} as e), Concat a0V) -> solve_concat a0V e l s (* * Extract *) | Some ((Var _ as v), (Extract {len= l} as e)) -> if not (Var.Set.mem (Var.of_ v) (Trm.fv e)) then (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *) - compose1 ~var:v ~rep:e s + add_solved ~var:v ~rep:e s else (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *) - compose1 ~var:e ~rep:(Trm.sized ~siz:l ~seq:v) s + 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 ?no_fresh a o l e s + | Some (Extract {seq= a; off= o; len= l}, e) -> solve_extract a o l e s (* * Sized *) (* v = ⟨n,a⟩ ==> v = a *) - | Some ((Var _ as v), Sized {seq= a}) -> s |> solve_ ?no_fresh v a + | Some ((Var _ as v), Sized {seq= a}) -> s |> add_pending v a (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *) | Some (Sized {siz= n; seq= a}, Sized {siz= m; seq= b}) -> - s |> solve_ ?no_fresh n m >>= solve_ ?no_fresh a b + s |> add_pending n m |> add_pending a b (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *) | Some (Sized {siz= n; seq= a}, b) -> - ( match Trm.seq_size b with - | None -> Some s - | Some m -> solve_ ?no_fresh n m s ) - >>= solve_ ?no_fresh a b + s + |> Option.fold ~f:(add_pending n) (Trm.seq_size b) + |> add_pending a b (* * Splat *) (* a^ = b^ ==> a = b *) - | Some (Splat a, Splat b) -> s |> solve_ ?no_fresh a b + | Some (Splat a, Splat b) -> s |> add_pending a b (* * Arithmetic *) @@ -398,27 +398,16 @@ and solve_ ?no_fresh d e s = | Some (rep, var) -> assert (not (is_interpreted var)) ; assert (not (is_interpreted rep)) ; - compose1 ~var ~rep s ) - |> - [%Trace.retn fun {pf} -> - function - | Some (_, xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s - | None -> pf "false"] + add_solved ~var ~rep s -let solve ~wrt ~xs d e = - [%Trace.call fun {pf} -> pf "@ %a@ %a" Trm.pp d Trm.pp e] - ; - ( solve_ d e (wrt, xs, Subst.empty) - |>= fun (_, xs, s) -> - let xs = Var.Set.inter xs (Subst.fv s) in - (xs, s) ) - |> - [%Trace.retn fun {pf} -> - function - | Some (xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s - | None -> pf "false"] +let solve ~wrt ~xs d e pending = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp d Trm.pp e) + ~retn:(fun {pf} -> pf "%a" pp_solve_state) + @@ fun () -> + solve_ d e {wrt; no_fresh= false; fresh= xs; solved= Some []; pending} -(** Equality classes *) +(* Equality classes =======================================================*) module Cls : sig type t [@@deriving equal] @@ -460,7 +449,7 @@ end = struct let pp_diff = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp end -(** Equality Relations *) +(* Conjunctions of atomic formula assumptions =============================*) (** see also [invariant] *) type t = @@ -470,7 +459,10 @@ type t = ; rep: Subst.t (** functional set of oriented equations: map [a] to [a'], indicating that [a = a'] holds, and that [a'] is the - 'rep(resentative)' of [a] *) } + 'rep(resentative)' of [a] *) + ; pnd: (Trm.t * Trm.t) list + (** pending equations to add (once invariants are reestablished) *) + } [@@deriving compare, equal, sexp] let classes r = @@ -484,9 +476,12 @@ let cls_of r e = let e' = Subst.apply r.rep e in Trm.Map.find e' (classes r) |> Option.value ~default:(Cls.of_ e') -(** Pretty-printing *) +(* Pretty-printing ========================================================*) + +let pp_eq fs (e, f) = Format.fprintf fs "@[%a = %a@]" Trm.pp e Trm.pp f +let pp_pnd = List.pp ";@ " pp_eq -let pp_raw fs {sat; rep} = +let pp_raw fs {sat; rep; pnd} = let pp_alist pp_k pp_v fs alist = let pp_assoc fs (k, v) = Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_k k pp_v (k, v) @@ -494,9 +489,14 @@ let pp_raw fs {sat; rep} = Format.fprintf fs "[@[%a@]]" (List.pp ";@ " pp_assoc) alist in let pp_term_v fs (k, v) = if not (Trm.equal k v) then Trm.pp fs v in - Format.fprintf fs "@[{@[sat= %b;@ rep= %a@]}@]" sat + let pp_pnd fs pnd = + if not (List.is_empty pnd) then + Format.fprintf fs ";@ pnd= @[%a@]" pp_pnd pnd + in + Format.fprintf fs "@[{@[sat= %b;@ rep= %a%a@]}@]" sat (pp_alist Trm.pp pp_term_v) (Iter.to_list (Subst.to_iter rep)) + pp_pnd pnd let pp_diff fs (r, s) = let pp_sat fs = @@ -505,9 +505,14 @@ let pp_diff fs (r, s) = in let pp_rep fs = if not (Subst.is_empty r.rep) then - Format.fprintf fs "rep= %a" Subst.pp_diff (r.rep, s.rep) + Format.fprintf fs "rep= %a;@ " Subst.pp_diff (r.rep, s.rep) in - Format.fprintf fs "@[{@[%t%t@]}@]" pp_sat pp_rep + let pp_pnd fs = + Format.fprintf fs "pnd= @[%a@]" + (List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ";@ " pp_eq) + (r.pnd, s.pnd) + in + Format.fprintf fs "@[{@[%t%t%t@]}@]" pp_sat pp_rep pp_pnd let ppx_classes x fs clss = List.pp "@ @<2>∧ " @@ -548,7 +553,7 @@ let ppx var_strength fs clss noneqs = "@ @<2>∧ " (Fml.ppx var_strength) fs noneqs ~suf:"@]" ; first && List.is_empty noneqs -(** Basic queries *) +(* Basic queries ==========================================================*) (** test membership in carrier *) let in_car r e = Subst.mem e r.rep @@ -560,7 +565,7 @@ let semi_congruent r a' b = Trm.equal a' (Trm.map ~f:(Subst.norm r.rep) b) (** terms are congruent if equal after normalizing subterms *) let congruent r a b = semi_congruent r (Trm.map ~f:(Subst.norm r.rep) a) b -(** Invariant *) +(* Invariant ==============================================================*) let pre_invariant r = let@ () = Invariant.invariant [%here] r [%sexp_of: t] in @@ -586,6 +591,7 @@ let pre_invariant r = let invariant r = let@ () = Invariant.invariant [%here] r [%sexp_of: t] in pre_invariant r ; + assert (List.is_empty r.pnd) ; assert ( (not r.sat) || Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' -> @@ -596,13 +602,44 @@ let invariant r = || fail "not congruent %a@ %a@ in@ %a" Trm.pp a Trm.pp b pp r () ) ) ) -(** Core operations *) +(* Representation helpers =================================================*) + +let add_to_pnd a a' x = + if Trm.equal a a' then x else {x with pnd= (a, a') :: x.pnd} + +(* Propagation ============================================================*) + +let propagate1 (trm, rep) x = + [%trace] + ~call:(fun {pf} -> + pf "@ @[%a ↦ %a@]@ %a" Trm.pp trm Trm.pp rep pp_raw x ) + ~retn:(fun {pf} -> pf "%a" pp_raw) + @@ fun () -> + let rep = Subst.compose1 ~key:trm ~data:rep x.rep in + {x with rep} + +let rec propagate ~wrt x = + [%trace] + ~call:(fun {pf} -> pf "@ %a" pp_raw x) + ~retn:(fun {pf} -> pf "%a" pp_raw) + @@ fun () -> + match x.pnd with + | (a, b) :: pnd -> ( + let a' = Subst.norm x.rep a in + let b' = Subst.norm x.rep b in + match solve ~wrt ~xs:x.xs a' b' pnd with + | {solved= Some solved; wrt; fresh; pending} -> + let xs = Var.Set.union x.xs fresh in + let x = {x with xs; pnd= pending} in + propagate ~wrt (List.fold ~f:propagate1 solved x) + | {solved= None} -> {x with sat= false; pnd= []} ) + | [] -> x + +(* Core operations ========================================================*) let empty = let rep = Subst.empty in - (* let rep = Option.get_exn (Subst.extend Trm.true_ rep) in - * let rep = Option.get_exn (Subst.extend Trm.false_ rep) in *) - {xs= Var.Set.empty; sat= true; rep} |> check invariant + {xs= Var.Set.empty; sat= true; rep; pnd= []} |> check invariant let unsat = {empty with sat= false} @@ -656,17 +693,13 @@ let extend a r = let rep = extend_ a r.rep in if rep == r.rep then r else {r with rep} |> check pre_invariant -let merge ~wrt a b r = - [%Trace.call fun {pf} -> pf "@ %a@ %a@ %a" Trm.pp a Trm.pp b pp r] - ; - ( match solve ~wrt ~xs:r.xs a b with - | Some (xs, s) -> - {r with xs= Var.Set.union r.xs xs; rep= Subst.compose r.rep s} - | None -> {r with sat= false} ) - |> - [%Trace.retn fun {pf} r' -> - pf "%a" pp_diff (r, r') ; - pre_invariant r'] +let merge ~wrt a b x = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a@ %a" Trm.pp a Trm.pp b pp x) + ~retn:(fun {pf} x' -> + pf "%a" pp_diff (x, x') ; + pre_invariant x' ) + @@ fun () -> propagate ~wrt (add_to_pnd a b x) (** find an unproved equation between congruent terms *) let find_missing r = @@ -684,12 +717,12 @@ let find_missing r = in Option.return_if need_a'_eq_b' (a', b') ) ) -let rec close ~wrt r = - if not r.sat then r +let rec close ~wrt x = + if not x.sat then x else - match find_missing r with - | Some (a', b') -> close ~wrt (merge ~wrt a' b' r) - | None -> r + match find_missing x with + | Some (a', b') -> close ~wrt (merge ~wrt a' b' x) + | None -> x let close ~wrt r = [%Trace.call fun {pf} -> pf "@ %a" pp r] @@ -718,7 +751,7 @@ let and_eq_ ~wrt a b r = let extract_xs r = (r.xs, {r with xs= Var.Set.empty}) -(** Exposed interface *) +(* Exposed interface ======================================================*) let is_empty {sat; rep} = sat && Subst.for_alli rep ~f:(fun ~key:a ~data:a' -> Trm.equal a a') @@ -880,7 +913,7 @@ let trms r = let vars r = Iter.flat_map ~f:Trm.vars (trms r) let fv r = Var.Set.of_iter (vars r) -(** Existential Witnessing and Elimination *) +(* Existential Witnessing and Elimination =================================*) let subst_invariant us s0 s = assert (s0 == s || not (Subst.equal s0 s)) ; @@ -922,6 +955,19 @@ let solve_poly_eq us p' q' subst = [%Trace.retn fun {pf} subst' -> pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)] +let rec solve_pending s soln = + match s.pending with + | (a, b) :: pending -> ( + let a' = Subst.norm soln a in + let b' = Subst.norm soln b in + match solve_ a' b' {s with pending} with + | {solved= Some solved} as s -> + solve_pending {s with solved= Some []} + (List.fold solved soln ~f:(fun (trm, rep) soln -> + Subst.compose1 ~key:trm ~data:rep soln )) + | {solved= None} -> None ) + | [] -> Some soln + let solve_seq_eq ~wrt us e' f' subst = [%Trace.call fun {pf} -> pf "@ %a = %a" Trm.pp e' Trm.pp f'] ; @@ -935,11 +981,14 @@ let solve_seq_eq ~wrt us e' f' subst = | Some n -> (a, n) | None -> (Trm.sized ~siz:n ~seq:a, n) in - let+ _, xs, s = - solve_concat ~no_fresh:true ms a n (wrt, Var.Set.empty, subst) - in - assert (Var.Set.is_empty xs) ; - s + solve_pending + (solve_concat ms a n + { wrt + ; no_fresh= true + ; fresh= Var.Set.empty + ; solved= Some [] + ; pending= [] }) + subst in ( match ((e' : Trm.t), (f' : Trm.t)) with | (Concat ms as c), a when x_ito_us c a -> @@ -1309,9 +1358,7 @@ let apply_and_elim ~wrt xs s r = let r = trim ks r in (zs, r, ks) -(* - * Replay debugging - *) +(* Replay debugging =======================================================*) type call = | Add of Var.Set.t * Formula.t * t diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index c28fdf03b..da14a7fe2 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -91,23 +91,24 @@ let%test_module _ = let%expect_test _ = replay {|(Solve_for_vars - (((Var (id 0) (name 2)) (Var (id 0) (name 6)) (Var (id 0) (name 8))) - ((Var (id 5) (name a0)) (Var (id 6) (name b)) (Var (id 7) (name m)) - (Var (id 8) (name a)) (Var (id 9) (name a0)))) - ((xs ()) (sat true) - (rep - (((Var (id 9) (name a0)) (Var (id 5) (name a0))) - ((Var (id 8) (name a)) - (Concat - ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) - (Sized (seq (Z 0)) (siz (Z 4)))))) - ((Var (id 7) (name m)) (Z 8)) - ((Var (id 6) (name b)) (Var (id 0) (name 2))) - ((Var (id 5) (name a0)) (Var (id 5) (name a0))) - ((Var (id 0) (name 6)) - (Concat - ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) - (Sized (seq (Z 0)) (siz (Z 4)))))) - ((Var (id 0) (name 2)) (Var (id 0) (name 2)))))))|} ; + (((Var (id 0) (name 2)) (Var (id 0) (name 6)) (Var (id 0) (name 8))) + ((Var (id 5) (name a0)) (Var (id 6) (name b)) (Var (id 7) (name m)) + (Var (id 8) (name a)) (Var (id 9) (name a0)))) + ((xs ()) (sat true) + (rep + (((Var (id 9) (name a0)) (Var (id 5) (name a0))) + ((Var (id 8) (name a)) + (Concat + ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) + (Sized (seq (Z 0)) (siz (Z 4)))))) + ((Var (id 7) (name m)) (Z 8)) + ((Var (id 6) (name b)) (Var (id 0) (name 2))) + ((Var (id 5) (name a0)) (Var (id 5) (name a0))) + ((Var (id 0) (name 6)) + (Concat + ((Sized (seq (Var (id 5) (name a0))) (siz (Z 4))) + (Sized (seq (Z 0)) (siz (Z 4)))))) + ((Var (id 0) (name 2)) (Var (id 0) (name 2))))) + (pnd ())))|} ; [%expect {| |}] end ) diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 32ea91be7..ca3293b8f 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -124,9 +124,9 @@ let%test_module _ = pp_raw r1 ; [%expect {| - + %x_5 = %y_6 - + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}] let%test _ = implies_eq r1 x y @@ -139,7 +139,7 @@ let%test_module _ = [%expect {| %x_5 = f(%x_5) = %z_7 = %y_6 - + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}] @@ -163,9 +163,9 @@ let%test_module _ = [%expect {| {sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]} - + {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]} - + {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}] let%test _ = @@ -183,7 +183,7 @@ let%test_module _ = {| %t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3 = %u_2 - + {sat= true; rep= [[%t_1 ↦ ]; [%u_2 ↦ %t_1]; @@ -207,7 +207,7 @@ let%test_module _ = [%expect {| (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5 - + {sat= true; rep= [[%w_4 ↦ (3 + %z_7)]; [%x_5 ↦ (8 + %z_7)]; @@ -229,7 +229,7 @@ let%test_module _ = [%expect {| 1 = %y_6 = %x_5 - + {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}] let%test _ = implies_eq r6 x y @@ -258,7 +258,7 @@ let%test_module _ = [%expect {| %v_3 = %z_7 = %y_6 = %x_5 = %w_4 - + {sat= true; rep= [[%v_3 ↦ ]; [%w_4 ↦ %v_3]; @@ -295,7 +295,7 @@ let%test_module _ = [%expect {| {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} - + {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} |}] let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -312,15 +312,15 @@ let%test_module _ = [%expect {| {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} - + {sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} - + (-8 + -1×%x_5 + %z_7) - + 8 - + (8 + %x_5 + -1×%z_7) - + -8 |}] let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -424,7 +424,7 @@ let%test_module _ = [%y_6 ↦ ]; [f(%x_5) ↦ %x_5]; [f(%y_6) ↦ (-1 + %y_6)]]} - + %x_5 = f(%x_5) ∧ (-1 + %y_6) = f(%y_6) |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] @@ -454,7 +454,7 @@ let%test_module _ = {| ((%x_5 = %y_6) ∧ ((5 = %w_4) ∨ (4 = %w_4)) ∧ ((0 = %x_5) ? (2 = %z_7) : (3 = %z_7))) - + (((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (5 = %w_4) ∧ (2 = %z_7)) ∨ ((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (4 = %w_4) ∧ (2 = %z_7)) ∨ ((%x_5 = %y_6) ∧ (5 = %w_4) ∧ (3 = %z_7) ∧ (0 ≠ %x_5)) diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index 3ed12cba8..e0f972940 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -78,11 +78,11 @@ let%test_module _ = pp (star p q) ; [%expect {| - ∃ %x_7 . emp + ∃ %x_7 . emp - 0 = %x_7 ∧ emp + 0 = %x_7 ∧ emp - 0 = %x_7 ∧ emp |}] + 0 = %x_7 ∧ emp |}] let%expect_test _ = let q = @@ -99,7 +99,7 @@ let%test_module _ = [%expect {| ( ( 0 = %x_7 ∧ emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( (∃ %x_7, %x_8 . 2 = %x_8 ∧ (2 = %x_8) ∧ emp) ∨ (∃ %x_7 . 1 = %y_8 = %x_7 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp) ∨ ( 0 = %x_7 ∧ (0 = %x_7) ∧ emp) @@ -122,7 +122,7 @@ let%test_module _ = [%expect {| ( ( emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( (∃ %x_7, %x_9, %x_10 . 2 = %x_10 ∧ (2 = %x_10) ∧ emp) ∨ (∃ %x_7, %x_9 . 1 = %x_9 = %y_8 ∧ ((1 = %y_8) ∧ (1 = %x_9)) @@ -147,7 +147,7 @@ let%test_module _ = [%expect {| ( ( emp) ∨ ( ( ( 1 = %y_8 ∧ emp) ∨ ( emp) )) ) - + ( ( emp) ∨ ( 1 = %y_8 ∧ emp) ∨ ( emp) ) |}] let%expect_test _ = @@ -159,9 +159,9 @@ let%test_module _ = [%expect {| ∃ %x_7 . %x_7 = f(%x_7) ∧ (-1 + %y_8) = f(%y_8) ∧ emp - + (-1 + %y_8) = f(%y_8) ∧ ((1 + f(%y_8)) = %y_8) ∧ emp - + (-1 + %y_8) = f(%y_8) ∧ emp |}] let%expect_test _ = @@ -222,7 +222,7 @@ let%test_module _ = ∧ ((%b_2 = %z_9) ∧ (%c_3 = %m_6)) ∧ emp) ) - + ∃ %b_2 . tt ∧ tt ∧ %x_7 -[ %b_2, %c_3 )-> ⟨8,0⟩