[sledge] Change: Context interface to set-of-assumptions terminology

Summary:
It is more confusing than necessary to use logical formula terminology
for the Context interface, considering that Formula represents
formulas and Context represents a (solver state resulting from a) set
of assumptions.

Reviewed By: jvillard

Differential Revision: D22571136

fbshipit-source-id: 087c97a02

sledge/src/fol.ml

@@ -1257,23 +1257,23 @@ module Context = struct
 
   let pp = Ses.Equality.pp
   let invariant = Ses.Equality.invariant
-  let true_ = Ses.Equality.true_
+  let empty = Ses.Equality.true_
 
-  let and_formula vs f x =
+  let add vs f x =
     let vs', x' = Ses.Equality.and_term (vs_to_ses vs) (f_to_ses f) x in
     (vs_of_ses vs', x')
 
-  let and_ vs x y =
+  let union vs x y =
     let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
     (vs_of_ses vs', z)
 
-  let orN vs xs =
+  let interN vs xs =
     let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
     (vs_of_ses vs', z)
 
   let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
-  let is_true x = Ses.Equality.is_true x
-  let is_false x = Ses.Equality.is_false x
+  let is_empty x = Ses.Equality.is_true x
+  let is_unsat x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
 
   let refutes x b =
@@ -1369,9 +1369,9 @@ module Context = struct
 
   type call =
     | Normalize of t * exp
-    | And_formula of Var.Set.t * fml * t
-    | And_ of Var.Set.t * t * t
-    | OrN of Var.Set.t * t list
+    | Add of Var.Set.t * fml * t
+    | Union of Var.Set.t * t * t
+    | InterN of Var.Set.t * t list
     | Rename of t * Var.Subst.t
     | Apply_subst of Var.Set.t * Subst.t * t
     | Solve_for_vars of Var.Set.t list * t
@@ -1380,9 +1380,9 @@ module Context = struct
   let replay c =
     match call_of_sexp (Sexp.of_string c) with
     | Normalize (r, e) -> normalize r e |> ignore
-    | And_formula (us, e, r) -> and_formula us e r |> ignore
-    | And_ (us, r, s) -> and_ us r s |> ignore
-    | OrN (us, rs) -> orN us rs |> ignore
+    | Add (us, e, r) -> add us e r |> ignore
+    | Union (us, r, s) -> union us r s |> ignore
+    | InterN (us, rs) -> interN us rs |> ignore
     | Rename (r, s) -> rename r s |> ignore
     | Apply_subst (us, s, r) -> apply_subst us s r |> ignore
     | Solve_for_vars (vss, r) -> solve_for_vars vss r |> ignore
@@ -1412,9 +1412,9 @@ module Context = struct
       try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ()))
 
   let normalize_tmr = Timer.create "normalize" ~at_exit:report
-  let and_formula_tmr = Timer.create "and_formula" ~at_exit:report
-  let and_tmr = Timer.create "and_" ~at_exit:report
-  let orN_tmr = Timer.create "orN" ~at_exit:report
+  let add_tmr = Timer.create "add" ~at_exit:report
+  let uniontmr = Timer.create "union" ~at_exit:report
+  let interN_tmr = Timer.create "interN" ~at_exit:report
   let rename_tmr = Timer.create "rename" ~at_exit:report
   let apply_subst_tmr = Timer.create "apply_subst" ~at_exit:report
   let solve_for_vars_tmr = Timer.create "solve_for_vars" ~at_exit:report
@@ -1422,15 +1422,14 @@ module Context = struct
   let normalize r e =
     wrap normalize_tmr (fun () -> normalize r e) (fun () -> Normalize (r, e))
 
-  let and_formula us e r =
-    wrap and_formula_tmr
-      (fun () -> and_formula us e r)
-      (fun () -> And_formula (us, e, r))
+  let add us e r =
+    wrap add_tmr (fun () -> add us e r) (fun () -> Add (us, e, r))
 
-  let and_ us r s =
-    wrap and_tmr (fun () -> and_ us r s) (fun () -> And_ (us, r, s))
+  let union us r s =
+    wrap uniontmr (fun () -> union us r s) (fun () -> Union (us, r, s))
 
-  let orN us rs = wrap orN_tmr (fun () -> orN us rs) (fun () -> OrN (us, rs))
+  let interN us rs =
+    wrap interN_tmr (fun () -> interN us rs) (fun () -> InterN (us, rs))
 
   let rename r s =
     wrap rename_tmr (fun () -> rename r s) (fun () -> Rename (r, s))

sledge/src/fol.mli

@@ -185,7 +185,8 @@ and Formula : sig
   val disjuncts : t -> t list
 end
 
-(** Inference System *)
+(** Sets of assumptions, interpreted as conjunction, plus reasoning about
+    their logical consequences. *)
 module Context : sig
   type t [@@deriving sexp]
 
@@ -197,43 +198,45 @@ module Context : sig
 
   include Invariant.S with type t := t
 
-  val true_ : t
-  (** The diagonal relation, which only equates each term with itself. *)
+  val empty : t
+  (** The empty context of assumptions. *)
 
-  val and_formula : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
-  (** Conjoin a (Boolean) term to a relation. *)
+  val add : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
+  (** Add (that is, conjoin) an assumption to a context. *)
 
-  val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
-  (** Conjunction. *)
+  val union : Var.Set.t -> t -> t -> Var.Set.t * t
+  (** Union (that is, conjoin) two contexts of assumptions. *)
 
-  val orN : Var.Set.t -> t list -> Var.Set.t * t
-  (** Nary disjunction. *)
+  val interN : Var.Set.t -> t list -> Var.Set.t * t
+  (** Intersect (that is, disjoin) contexts of assumptions. *)
 
   val rename : t -> Var.Subst.t -> t
-  (** Apply a renaming substitution to the relation. *)
+  (** Apply a renaming substitution to the context. *)
 
-  val is_true : t -> bool
-  (** Test if the relation is diagonal. *)
+  val is_empty : t -> bool
+  (** Test if the context of assumptions is empty. *)
 
-  val is_false : t -> bool
-  (** Test if the relation is empty / inconsistent. *)
+  val is_unsat : t -> bool
+  (** Test if the context of assumptions is inconsistent. *)
 
   val implies : t -> Formula.t -> bool
-  (** [implies x f] holds only if [f] is a logical consequence of [x]. This
-      only checks if [f] is valid in the current state of [x], without doing
-      any further logical reasoning or propagation. *)
+  (** Holds only if a formula is a logical consequence of a context of
+      assumptions. This only checks if the formula is valid in the current
+      state of the context, without doing any further logical reasoning or
+      propagation. *)
 
   val refutes : t -> Formula.t -> bool
-  (** [refutes x f] holds only if [f] is inconsistent with [x]. *)
+  (** Holds only if a formula is inconsistent with a context of assumptions,
+      that is, conjoining the formula to the assumptions is unsatisfiable. *)
 
   val class_of : t -> Term.t -> Term.t list
-  (** Equivalence class of [e]: all the terms [f] in the relation such that
-      [e = f] is implied by the relation. *)
+  (** Equivalence class of [e]: all the terms [f] in the context such that
+      [e = f] is implied by the assumptions. *)
 
   val normalize : t -> Term.t -> Term.t
   (** Normalize a term [e] to [e'] such that [e = e'] is implied by the
-      relation, where [e'] and its subterms are expressed in terms of the
-      relation's canonical representatives of each equivalence class. *)
+      assumptions, where [e'] and its subterms are expressed in terms of the
+      canonical representatives of each equivalence class. *)
 
   val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
   (** Enumerate the variables occurring in the terms of the context. *)
@@ -263,23 +266,24 @@ module Context : sig
   end
 
   val apply_subst : Var.Set.t -> Subst.t -> t -> Var.Set.t * t
-  (** Relation induced by applying a substitution to a set of equations
-      generating the argument relation. *)
+  (** Context induced by applying a solution substitution to a set of
+      equations generating the argument context. *)
 
   val solve_for_vars : Var.Set.t list -> t -> Subst.t
-  (** [solve_for_vars vss r] is a solution substitution that is entailed by
-      [r] and consists of oriented equalities [x ↦ e] that map terms [x]
+  (** [solve_for_vars vss x] is a solution substitution that is implied by
+      [x] and consists of oriented equalities [v ↦ e] that map terms [v]
       with free variables contained in (the union of) a prefix [uss] of
       [vss] to terms [e] with free variables contained in as short a prefix
       of [uss] as possible. *)
 
   val elim : Var.Set.t -> t -> t
-  (** Weaken relation by removing oriented equations [k ↦ _] for [k] in
-      [ks]. *)
+  (** [elim ks x] is [x] weakened by removing oriented equations [k ↦ _]
+      for [k] in [ks]. *)
 
-  (* Replay debugging *)
+  (**/**)
 
   val replay : string -> unit
+  (** Replay debugging *)
 end
 
 (** Convert from Llair *)

sledge/src/fol_test.ml

@@ -49,16 +49,16 @@ let%test_module _ =
     (* let g = Term.mul u *)
 
     let of_eqs l =
-      List.fold ~init:(wrt, true_)
-        ~f:(fun (us, r) (a, b) -> and_formula us (Formula.eq a b) r)
+      List.fold ~init:(wrt, empty)
+        ~f:(fun (us, r) (a, b) -> add us (Formula.eq a b) r)
         l
       |> snd
 
     (* let and_eq a b r = and_formula wrt (Formula.eq a b) r |> snd *)
     (* let and_ r s = and_ wrt r s |> snd *)
-    let or_ r s = orN wrt [r; s] |> snd
+    let or_ r s = interN wrt [r; s] |> snd
     let difference x e f = Term.d_int (Context.normalize x (Term.sub e f))
-    let r0 = true_
+    let r0 = empty
 
     let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))
     let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1))

sledge/src/sh.ml

@@ -32,7 +32,7 @@ type t = starjunction [@@deriving compare, equal, sexp]
 let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
-  ; ctx= Context.true_
+  ; ctx= Context.empty
   ; pure= Formula.tt
   ; heap= []
   ; djns= [] }
@@ -256,13 +256,13 @@ and pp_djn ?var_strength vs xs ctx fs = function
 let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q =
   pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q
 
-let pp fs q = pp_diff_eq Context.true_ fs q
+let pp fs q = pp_diff_eq Context.empty fs q
 
 let pp_djn fs d =
-  pp_djn ?var_strength:None Var.Set.empty Var.Set.empty Context.true_ fs d
+  pp_djn ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs d
 
 let pp_raw fs q =
-  pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.true_ fs q
+  pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs q
 
 let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
 
@@ -292,10 +292,10 @@ let rec invariant q =
     Context.invariant ctx ;
     ( match djns with
     | [[]] ->
-        assert (Context.is_true ctx) ;
+        assert (Context.is_empty ctx) ;
         assert (Formula.is_true pure) ;
         assert (List.is_empty heap)
-    | _ -> assert (not (Context.is_false ctx)) ) ;
+    | _ -> assert (not (Context.is_unsat ctx)) ) ;
     invariant_pure pure ;
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
@@ -430,8 +430,8 @@ let elim_exists xs q =
 (** conjoin an FOL context assuming vocabulary is compatible *)
 let and_ctx_ ctx q =
   assert (Var.Set.is_subset (Context.fv ctx) ~of_:q.us) ;
-  let xs, ctx = Context.and_ (Var.Set.union q.us q.xs) q.ctx ctx in
-  if Context.is_false ctx then false_ q.us else exists_fresh xs {q with ctx}
+  let xs, ctx = Context.union (Var.Set.union q.us q.xs) q.ctx ctx in
+  if Context.is_unsat ctx then false_ q.us else exists_fresh xs {q with ctx}
 
 let and_ctx ctx q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp ctx pp q]
@@ -451,11 +451,11 @@ let star q1 q2 =
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
   | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
-    when Context.is_true ctx && Formula.is_true pure ->
+    when Context.is_empty ctx && Formula.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
   | _, {us= _; xs= _; ctx; pure; heap= []; djns= []}
-    when Context.is_true ctx && Formula.is_true pure ->
+    when Context.is_empty ctx && Formula.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
@@ -466,9 +466,9 @@ let star q1 q2 =
       let {us= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Var.Set.equal us (Var.Set.union us1 us2)) ;
       let xs, ctx =
-        Context.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
+        Context.union (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
       in
-      if Context.is_false ctx then false_ us
+      if Context.is_unsat ctx then false_ us
       else
         exists_fresh xs
           { us
@@ -505,7 +505,7 @@ let or_ q1 q2 =
   | _ ->
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
-      ; ctx= Context.true_
+      ; ctx= Context.empty
       ; pure= Formula.tt
       ; heap= []
       ; djns= [[q1; q2]] } )
@@ -526,8 +526,8 @@ let pure (p : Formula.t) =
   List.fold (Formula.disjuncts p) ~init:(false_ Var.Set.empty)
     ~f:(fun q p ->
       let us = Formula.fv p in
-      let xs, ctx = Context.(and_formula us p true_) in
-      if Context.is_false ctx then false_ us
+      let xs, ctx = Context.add us p Context.empty in
+      if Context.is_unsat ctx then false_ us
       else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) )
   |>
   [%Trace.retn fun {pf} q ->
@@ -701,7 +701,7 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
                let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
                (dj.ctx, dj) )
          in
-         let new_xs, djn_ctx = Context.orN ancestor_vs dj_ctxs in
+         let new_xs, djn_ctx = Context.interN ancestor_vs dj_ctxs in
          (* hoist xs appearing in disjunction's context *)
          let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
@@ -787,7 +787,7 @@ let simplify q =
   [%Trace.call fun {pf} -> pf "%a" pp_raw q]
   ;
   let q = freshen_nested_xs q in
-  let q = propagate_context Var.Set.empty Context.true_ q in
+  let q = propagate_context Var.Set.empty Context.empty q in
   let q = simplify_ q.us [] q in
   q
   |>