[sledge] Replace solution substitution trimming with partitioning

Summary:
Replace `Equality.Subst.trim` with `partition_valid` which has a
logical specification (and unsurprisingly fixes some corner case
bugs):

```
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν
    are maximal where ∃ks. ν is universally valid, xs ⊇ ks and ks ∩
    fv(τ) = ∅. *)
```

Reviewed By: ngorogiannis

Differential Revision: D20004974

fbshipit-source-id: 5cb3b3835

sledge/src/import/qset.ml

@@ -114,4 +114,5 @@ let fold_map m ~f ~init:s =
 let for_all m ~f = Map.for_alli m ~f:(fun ~key ~data -> f key data)
 let map_counts m ~f = Map.mapi m ~f:(fun ~key ~data -> f key data)
 let iter m ~f = Map.iteri m ~f:(fun ~key ~data -> f key data)
+let exists m ~f = Map.existsi m ~f:(fun ~key ~data -> f key data)
 let to_list m = Map.to_alist m

sledge/src/import/qset.mli

@@ -103,6 +103,9 @@ val for_all : ('a, _) t -> f:('a -> Q.t -> bool) -> bool
 val iter : ('a, _) t -> f:('a -> Q.t -> unit) -> unit
 (** Iterate over the elements in ascending order. *)
 
+val exists : ('a, _) t -> f:('a -> Q.t -> bool) -> bool
+(** Search for an element satisfying a predicate. *)
+
 val min_elt : ('a, _) t -> ('a * Q.t) option
 (** Minimum element. *)
 

sledge/src/llair/term.ml

@@ -1125,6 +1125,15 @@ let iter e ~f =
   | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> ()
 
+let exists e ~f =
+  match e with
+  | Ap1 (_, x) -> f x
+  | Ap2 (_, x, y) -> f x || f y
+  | Ap3 (_, x, y, z) -> f x || f y || f z
+  | ApN (_, xs) | RecN (_, xs) -> Vector.exists ~f xs
+  | Add args | Mul args -> Qset.exists ~f:(fun arg _ -> f arg) args
+  | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> false
+
 let fold e ~init:s ~f =
   match e with
   | Ap1 (_, x) -> f x s

sledge/src/llair/term.mli

@@ -246,6 +246,7 @@ val rename : Var.Subst.t -> t -> t
 (** Traverse *)
 
 val iter : t -> f:(t -> unit) -> unit
+val exists : t -> f:(t -> bool) -> bool
 val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
 val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
 val fold_terms : t -> init:'a -> f:('a -> t -> 'a) -> 'a

sledge/src/symbheap/equality.ml

@@ -23,14 +23,14 @@ let classify e =
 
 let interpreted e = equal_kind (classify e) Interpreted
 let non_interpreted e = not (interpreted e)
+let uninterpreted e = equal_kind (classify e) Uninterpreted
 
 let rec fold_max_solvables e ~init ~f =
-  if interpreted e then
-    Term.fold e ~init ~f:(fun d s -> fold_max_solvables ~f d ~init:s)
-  else f e init
+  if non_interpreted e then f e init
+  else Term.fold e ~init ~f:(fun d s -> fold_max_solvables ~f d ~init:s)
 
 let rec iter_max_solvables e ~f =
-  if interpreted e then Term.iter ~f:(iter_max_solvables ~f) e else f e
+  if non_interpreted e then f e else Term.iter ~f:(iter_max_solvables ~f) e
 
 (** Solution Substitutions *)
 module Subst : sig
@@ -52,7 +52,7 @@ module Subst : sig
   val extend : Term.t -> t -> t option
   val map_entries : f:(Term.t -> Term.t) -> t -> t
   val to_alist : t -> (Term.t * Term.t) list
-  val trim : bound:Var.Set.t -> Var.Set.t -> t -> t
+  val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
 end = struct
   type t = Term.t Term.Map.t [@@deriving compare, equal, sexp]
 
@@ -114,20 +114,39 @@ end = struct
           if Term.equal data' data then s else Map.set s ~key ~data:data'
         else Map.remove s key |> Map.add_exn ~key:key' ~data:data' )
 
-  (** [trim bound kills subst] is [subst] without mappings that mention
-      [kills] or [bound ∩ fv x] for removed entries [x ↦ u] *)
-  let rec trim ~bound ks s =
-    let ks', s' =
-      Map.fold s ~init:(ks, s) ~f:(fun ~key ~data (ks, s) ->
-          let fv_key = Term.fv key in
-          let fv_data = Term.fv data in
-          if Set.disjoint ks (Set.union fv_key fv_data) then (ks, s)
-          else
-            let ks = Set.union ks (Set.inter bound fv_key) in
-            let s = Map.remove s key in
-            (ks, s) )
+  (** Holds only if [true ⊢ ∃xs. e=f]. Clients assume
+      [not (is_valid_eq xs e f)] implies [not (is_valid_eq ys e f)] for
+      [ys ⊆ xs]. *)
+  let is_valid_eq xs e f =
+    let is_var_in xs e = Option.exists ~f:(Set.mem xs) (Var.of_term e) in
+    ( is_var_in xs e || is_var_in xs f
+    || (uninterpreted e && Term.exists ~f:(is_var_in xs) e)
+    || (uninterpreted f && Term.exists ~f:(is_var_in xs) f) )
+    $> fun b ->
+    [%Trace.info
+      "is_valid_eq %a%a=%a = %b" Var.Set.pp_xs xs Term.pp e Term.pp f b]
+
+  (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
+      and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
+      ks ∩ fv(τ) = ∅. *)
+  let partition_valid xs s =
+    (* Move equations e=f from s to t when ∃ks.e=f fails to be provably
+       valid. When moving an equation, reduce ks by fv(e=f) to maintain ks ∩
+       fv(t) = ∅. This reduction may cause equations in s to no longer be
+       valid, so loop until no change. *)
+    let rec partition_valid_ t ks s =
+      let t', ks', s' =
+        Map.fold s ~init:(t, ks, s) ~f:(fun ~key ~data (t, ks, s) ->
+            if is_valid_eq ks key data then (t, ks, s)
+            else
+              let t = Map.set ~key ~data t
+              and ks = Set.diff ks (Set.union (Term.fv key) (Term.fv data))
+              and s = Map.remove s key in
+              (t, ks, s) )
+      in
+      if s' != s then partition_valid_ t' ks' s' else (t', ks', s')
     in
-    if s' != s then trim ~bound ks' s' else s'
+    partition_valid_ empty xs s
 end
 
 (** Theory Solver *)

sledge/src/symbheap/equality.mli

@@ -71,7 +71,11 @@ module Subst : sig
   val is_empty : t -> bool
   val fold : t -> init:'a -> f:(key:Term.t -> data:Term.t -> 'a -> 'a) -> 'a
   val norm : t -> Term.t -> Term.t
-  val trim : bound:Var.Set.t -> Var.Set.t -> t -> t
+
+  val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
+  (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
+      and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and
+      ks ∩ fv(τ) = ∅. *)
 end
 
 val solve_for_vars : Var.Set.t list -> t -> Subst.t

sledge/src/symbheap/solver.ml

@@ -53,14 +53,14 @@ let excise_exists goal =
     in
     if Equality.Subst.is_empty solutions_for_xs then goal
     else
-      let sub = Sh.norm solutions_for_xs goal.sub in
-      let removed, survived =
-        Set.diff_inter goal.xs (Sh.fv ~ignore_cong:() sub)
+      let removed =
+        Set.diff goal.xs
+          (Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub))
       in
       if Set.is_empty removed then goal
       else
-        let witnesses =
-          Equality.Subst.trim ~bound:goal.xs survived solutions_for_xs
+        let _, removed, witnesses =
+          Equality.Subst.partition_valid removed solutions_for_xs
         in
         if Equality.Subst.is_empty witnesses then goal
         else (
@@ -68,13 +68,13 @@ let excise_exists goal =
               pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed
                 Equality.Subst.pp witnesses ) ;
           let us = Set.union goal.us removed in
-          let xs = survived in
+          let xs = Set.diff goal.xs removed in
           let min =
             Equality.Subst.fold
               ~f:(fun ~key ~data -> Sh.and_ (Term.eq key data))
               witnesses ~init:goal.min
           in
-          {goal with us; min; xs; sub; pgs= true} )
+          {goal with us; min; xs; pgs= true} )
 
 (* ad hoc treatment to drop tautologous constraints such as ∃x,y. x = y
    where x and y do not appear elsewhere *)

sledge/src/symbheap/solver_test.ml

@@ -7,13 +7,17 @@
 
 let%test_module _ =
   ( module struct
-    (* let () = Trace.init ~margin:160 ~config:all () *)
-
     let () =
       Trace.init ~margin:68
         ~config:(Result.ok_exn (Trace.parse "+Solver.infer_frame"))
         ()
 
+    (* let () =
+     *   Trace.init ~margin:160
+     *     ~config:
+     *       (Result.ok_exn (Trace.parse "+Solver.infer_frame+Solver.excise"))
+     *     () *)
+
     let infer_frame p xs q =
       Solver.infer_frame p (Var.Set.of_list xs) q
       |> (ignore : Sh.t option -> _)
@@ -267,9 +271,5 @@ let%test_module _ =
           * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
-        ) infer_frame:
-            %a_1 = %a_2
-          ∧ 2 = %n_9
-          ∧ 16 = %m_8
-          ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩ |}]
+        ) infer_frame: |}]
   end )