From f20cabf7a4ed58c3ed72bb0d7cffccde26cdbe3f Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:19:36 -0700 Subject: [PATCH] [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 | 43 ++++++++++++++--------------- sledge/src/fol.mli | 62 ++++++++++++++++++++++-------------------- sledge/src/fol_test.ml | 8 +++--- sledge/src/sh.ml | 34 +++++++++++------------ 4 files changed, 75 insertions(+), 72 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index cd921d26d..4839b6d03 100644 --- a/sledge/src/fol.ml +++ b/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)) diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index b74838754..2d2784010 100644 --- a/sledge/src/fol.mli +++ b/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 *) diff --git a/sledge/src/fol_test.ml b/sledge/src/fol_test.ml index bdd9a60c1..ab41f3e99 100644 --- a/sledge/src/fol_test.ml +++ b/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)) diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index fc2e78373..f8aad2865 100644 --- a/sledge/src/sh.ml +++ b/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 |>