pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Represent equality classes explicitly

Browse Source 
Summary:
Currently the equality classes are computed from the representatives
solution substitution when needed. This diff instead maintains them as
part of the representation of the context. By itself this does not
make a huge difference, but it is necessary to make other operations
incremental.

Reviewed By: jvillard

Differential Revision: D25883715

fbshipit-source-id: 1b444a0dc
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 999710fbb7
commit 1ddb5fb249
8 changed files with 342 additions and 201 deletions
Show Stats Download Patch File Download Diff File

4
sledge/nonstdlib/list.ml
Unescape View File

@ -91,13 +91,13 @@ let rec pp ?pre ?suf sep pp_elt fs = function
| xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
Option.iter ~f:(Format.fprintf fs) suf
let pp_diff ~cmp sep pp_elt fs (xs, ys) =
let pp_diff ~cmp ?pre ?suf sep pp_elt fs (xs, ys) =
let pp_diff_elt fs (elt : _ Either.t) =
match elt with
| Left x -> Format.fprintf fs "-- %a" pp_elt x
| Right y -> Format.fprintf fs "++ %a" pp_elt y
in
pp sep pp_diff_elt fs (symmetric_diff ~cmp xs ys)
pp ?pre ?suf sep pp_diff_elt fs (symmetric_diff ~cmp xs ys)
module Assoc = struct
include Assoc

2
sledge/nonstdlib/list.mli
Unescape View File

@ -20,6 +20,8 @@ val pp :
val pp_diff :
cmp:('a -> 'a -> int)
-> ?pre:(unit, unit) fmt
-> ?suf:(unit, unit) fmt
-> (unit, unit) fmt
-> 'a pp
-> ('a list * 'a list) pp

348
sledge/src/fol/context.ml
Unescape View File

@ -12,7 +12,7 @@ open Exp
(* Solution Substitutions =================================================*)
module Subst : sig
type t [@@deriving compare, equal, sexp]
type t = Trm.t Trm.Map.t [@@deriving compare, equal, sexp]
val pp : t pp
val pp_diff : (t * t) pp
@ -34,6 +34,7 @@ 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 to_list : t -> (Trm.t * Trm.t) list
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(* direct representation manipulation *)
@ -58,6 +59,7 @@ end = struct
let iteri = Trm.Map.iteri
let for_alli = Trm.Map.for_alli
let to_iter = Trm.Map.to_iter
let to_list = Trm.Map.to_list
(** look up a term in a substitution *)
let apply s a = Trm.Map.find a s |> Option.value ~default:a
@ -92,7 +94,8 @@ end = struct
else (
assert (
Option.for_all ~f:(Trm.equal key) (Trm.Map.find key r)
|| fail "domains intersect: %a" Trm.pp key () ) ;
|| fail "domains intersect: %a ↦ %a in %a" Trm.pp key Trm.pp data
pp r () ) ;
let s = Trm.Map.singleton key data in
let r' = Trm.Map.map_endo ~f:(norm s) r in
Trm.Map.add ~key ~data r' )
@ -119,7 +122,7 @@ end = struct
if Trm.equal data' data then s else Trm.Map.add ~key ~data:data' s
else
let s = Trm.Map.remove key s in
match (key : Trm.t) with
match (key' : Trm.t) with
| Z _ | Q _ -> s
| _ -> Trm.Map.add_exn ~key:key' ~data:data' s )
@ -178,7 +181,7 @@ end
(* Equality classes =======================================================*)
module Cls : sig
type t [@@deriving equal]
type t [@@deriving compare, equal, sexp]
val empty : t
val of_ : Trm.t -> t
@ -190,14 +193,16 @@ module Cls : sig
val filter : t -> f:(Trm.t -> bool) -> t
val partition : t -> f:(Trm.t -> bool) -> t * t
val fold : t -> 's -> f:(Trm.t -> 's -> 's) -> 's
val map : t -> f:(Trm.t -> Trm.t) -> t
val to_iter : t -> Trm.t iter
val to_set : t -> Trm.Set.t
val sort : t -> t
val of_set : Trm.Set.t -> t
val ppx : Trm.Var.strength -> t pp
val pp : t pp
val pp_raw : t pp
val pp_diff : (t * t) pp
end = struct
type t = Trm.t list [@@deriving equal]
type t = Trm.t list [@@deriving compare, equal, sexp]
let empty = []
let of_ e = [e]
@ -209,11 +214,19 @@ end = struct
let filter = List.filter
let partition = List.partition
let fold = List.fold
let map = List.map_endo
let to_iter = List.to_iter
let to_set = Trm.Set.of_list
let sort = List.sort ~cmp:Trm.compare
let ppx x = List.pp "@ = " (Trm.ppx x)
let of_set s = Iter.to_list (Trm.Set.to_iter s)
let ppx x fs es =
List.pp "@ = " (Trm.ppx x) fs (List.sort_uniq ~cmp:Trm.compare es)
let pp = ppx (fun _ -> None)
let pp_raw fs es =
Trm.Set.pp_full ~pre:"{@[" ~suf:"@]}" ~sep:",@ " Trm.pp fs (to_set es)
let pp_diff = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp
end
@ -222,49 +235,41 @@ end
(** see also [invariant] *)
type t =
{ xs: Var.Set.t
(** existential variables that did not appear in input equations *)
(** existential variables that did not appear in input formulas *)
; sat: bool (** [false] only if constraints are inconsistent *)
; 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] *)
; cls: Cls.t Trm.Map.t
(** map each representative to the set of terms in its class *)
; pnd: (Trm.t * Trm.t) list
(** pending equations to add (once invariants are reestablished) *)
}
[@@deriving compare, equal, sexp]
let classes r =
Subst.fold r.rep Trm.Map.empty ~f:(fun ~key:elt ~data:rep cls ->
if Trm.equal elt rep then cls
else
Trm.Map.update rep cls ~f:(fun cls0 ->
Cls.add elt (Option.value cls0 ~default:Cls.empty) ) )
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 ========================================================*)
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; pnd} =
let pp_raw fs {sat; rep; cls; 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)
in
Format.fprintf fs "[@[<hv>%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
let pp_trm_v fs (k, v) = if not (Trm.equal k v) then Trm.pp fs v in
let pp_cls_v fs (_, cls) = Cls.pp_raw fs cls in
let pp_pnd fs pnd =
if not (List.is_empty pnd) then
Format.fprintf fs ";@ pnd= @[%a@]" pp_pnd pnd
Format.fprintf fs ";@ pnd= @[%a@]" (List.pp ";@ " pp_eq) pnd
in
Format.fprintf fs "@[{@[<hv>sat= %b;@ rep= %a%a@]}@]" sat
(pp_alist Trm.pp pp_term_v)
(Iter.to_list (Subst.to_iter rep))
pp_pnd pnd
Format.fprintf fs "@[{@[<hv>sat= %b;@ rep= %a;@ cls= %a%a@]}@]" sat
(pp_alist Trm.pp pp_trm_v)
(Subst.to_list rep)
(pp_alist Trm.pp pp_cls_v)
(Trm.Map.to_list cls) pp_pnd pnd
let pp_diff fs (r, s) =
let pp_sat fs =
@ -275,33 +280,35 @@ let pp_diff fs (r, s) =
if not (Subst.is_empty r.rep) then
Format.fprintf fs "rep= %a;@ " Subst.pp_diff (r.rep, s.rep)
in
let pp_cls fs =
if not (Trm.Map.equal Cls.equal r.cls s.cls) then
Format.fprintf fs "cls= %a;@ "
(Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp_raw Cls.pp_diff)
(r.cls, s.cls)
in
let pp_pnd fs =
Format.fprintf fs "pnd= @[%a@]"
(List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ";@ " pp_eq)
(r.pnd, s.pnd)
List.pp_diff ~cmp:[%compare: Trm.t * Trm.t] ~pre:"pnd= @[" ~suf:"@]"
";@ " pp_eq fs (r.pnd, s.pnd)
in
Format.fprintf fs "@[{@[<hv>%t%t%t@]}@]" pp_sat pp_rep pp_pnd
Format.fprintf fs "@[{@[<hv>%t%t%t%t@]}@]" pp_sat pp_rep pp_cls pp_pnd
let ppx_classes x fs clss =
List.pp "@ @<2>∧ "
(fun fs (rep, cls) ->
if not (Cls.is_empty cls) then
Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (Cls.ppx x) cls )
fs
(Iter.to_list (Trm.Map.to_iter clss))
fs (Trm.Map.to_list clss)
let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
let pp_diff_clss = Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp Cls.pp_diff
let pp_classes fs r = ppx_classes (fun _ -> None) fs r.cls
let pp fs r =
let clss = classes r in
if Trm.Map.is_empty clss then
if Trm.Map.is_empty r.cls then
Format.fprintf fs (if r.sat then "tt" else "ff")
else ppx_classes (fun _ -> None) fs clss
else pp_classes fs r
let ppx var_strength fs clss noneqs =
let without_anon_vars =
Cls.filter ~f:(fun e ->
let without_anon_vars es =
Cls.filter es ~f:(fun e ->
match Var.of_trm e with
| Some v -> Poly.(var_strength v <> Some `Anonymous)
| None -> true )
@ -309,8 +316,7 @@ let ppx var_strength fs clss noneqs =
let clss =
Trm.Map.fold clss Trm.Map.empty ~f:(fun ~key:rep ~data:cls m ->
let cls = without_anon_vars cls in
if not (Cls.is_empty cls) then
Trm.Map.add ~key:rep ~data:(Cls.sort cls) m
if not (Cls.is_empty cls) then Trm.Map.add ~key:rep ~data:cls m
else m )
in
let first = Trm.Map.is_empty clss in
@ -321,6 +327,8 @@ let ppx var_strength fs clss noneqs =
"@ @<2>∧ " (Fml.ppx var_strength) fs noneqs ~suf:"@]" ;
first && List.is_empty noneqs
let pp_diff_cls = Trm.Map.pp_diff ~eq:Cls.equal Trm.pp Cls.pp Cls.pp_diff
(* Basic queries ==========================================================*)
(** test membership in carrier *)
@ -355,12 +363,28 @@ let pre_invariant r =
let rep' = Subst.norm r.rep rep in
Trm.equal rep rep'
|| fail "not idempotent: %a != %a in@ %a" Trm.pp rep Trm.pp rep'
Subst.pp r.rep () ) )
Subst.pp r.rep () ) ;
(* every term is in the class of its rep *)
assert (
Trm.equal trm rep
|| Trm.Set.mem trm
(Cls.to_set
(Trm.Map.find rep r.cls |> Option.value ~default:Cls.empty))
|| fail "%a not in cls of %a = {%a}@ %a" Trm.pp trm Trm.pp rep
Cls.pp
(Trm.Map.find rep r.cls |> Option.value ~default:Cls.empty)
pp_raw r () ) ) ;
Trm.Map.iteri r.cls ~f:(fun ~key:rep ~data:cls ->
(* each class does not include its rep *)
assert (not (Trm.Set.mem rep (Cls.to_set cls))) ;
(* representative of every element of [rep]'s class is [rep] *)
Iter.iter (Cls.to_iter cls) ~f:(fun elt ->
assert (Option.exists ~f:(Trm.equal rep) (Subst.find elt r.rep)) ) )
let invariant r =
let@ () = Invariant.invariant [%here] r [%sexp_of: t] in
pre_invariant r ;
assert (List.is_empty r.pnd) ;
pre_invariant r ;
assert (
(not r.sat)
|| Subst.for_alli r.rep ~f:(fun ~key:a ~data:a' ->
@ -371,21 +395,67 @@ let invariant r =
|| fail "not congruent %a@ %a@ in@ %a" Trm.pp a Trm.pp b pp r
() ) ) )
(* Representation helpers =================================================*)
(* Extending the carrier ==================================================*)
let rec extend_ a s =
[%trace]
~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a Subst.pp s)
~retn:(fun {pf} s' -> pf "%a" Subst.pp_diff (s, s'))
@@ fun () ->
match (a : Trm.t) with
| Z _ | Q _ -> s
| _ -> (
if Theory.is_interpreted a then Iter.fold ~f:extend_ (Trm.trms a) s
else
(* add uninterpreted terms *)
match Subst.extend a s with
(* and their subterms if newly added *)
| Some s -> Iter.fold ~f:extend_ (Trm.trms a) s
| None -> s )
let add_to_pnd a a' x =
if Trm.equal a a' then x else {x with pnd= (a, a') :: x.pnd}
(** add a term to the carrier *)
let extend a x =
[%trace]
~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp x)
~retn:(fun {pf} x' ->
pf "%a" pp_diff (x, x') ;
pre_invariant x' )
@@ fun () ->
let rep = extend_ a x.rep in
if rep == x.rep then x else {x with rep}
(* Propagation ============================================================*)
let propagate1 (trm, rep) x =
(** add a=a' to x using a' as the representative *)
let propagate1 (a, a') x =
[%trace]
~call:(fun {pf} ->
pf "@ @[%a ↦ %a@]@ %a" Trm.pp trm Trm.pp rep pp_raw x )
~call:(fun {pf} -> pf "@ @[%a ↦ %a@]@ %a" Trm.pp a Trm.pp a' 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}
(* pending equations need not be between terms in the carrier *)
let x = extend a (extend a' x) in
let s = Trm.Map.singleton a a' in
Trm.Map.fold x.rep x ~f:(fun ~key:_ ~data:b0' x ->
let b' = Subst.norm s b0' in
if b' == b0' then x
else
let b0'_cls, cls =
Trm.Map.find_and_remove b0' x.cls
|> Option.value ~default:(Cls.empty, x.cls)
in
let b0'_cls, pnd =
if Theory.is_interpreted b0' then (b0'_cls, (b0', b') :: x.pnd)
else (Cls.add b0' b0'_cls, x.pnd)
in
let rep =
Cls.fold b0'_cls x.rep ~f:(fun c rep ->
Trm.Map.add ~key:c ~data:b' rep )
in
let cls =
Trm.Map.update b' cls ~f:(fun b'_cls ->
Cls.union b0'_cls (Option.value b'_cls ~default:Cls.empty) )
in
{x with rep; cls; pnd} )
let solve ~wrt ~xs d e pending =
[%trace]
@ -416,7 +486,8 @@ let rec propagate ~wrt x =
let empty =
let rep = Subst.empty in
{xs= Var.Set.empty; sat= true; rep; pnd= []} |> check invariant
{xs= Var.Set.empty; sat= true; rep; cls= Trm.Map.empty; pnd= []}
|> check invariant
let unsat = {empty with sat= false}
@ -453,30 +524,15 @@ let canon_f r b =
~retn:(fun {pf} -> pf "%a" Fml.pp)
@@ fun () -> Fml.map_trms ~f:(canon r) b
let rec extend_ a r =
match (a : Trm.t) with
| Z _ | Q _ -> r
| _ -> (
if Theory.is_interpreted a then Iter.fold ~f:extend_ (Trm.trms a) r
else
(* add uninterpreted terms *)
match Subst.extend a r with
(* and their subterms if newly added *)
| Some r -> Iter.fold ~f:extend_ (Trm.trms a) r
| None -> r )
(** add a term to the carrier *)
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 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)
@@ fun () ->
let x = {x with pnd= (a, b) :: x.pnd} in
propagate ~wrt x
(** find an unproved equation between congruent terms *)
let find_missing r =
@ -510,21 +566,25 @@ let close ~wrt r =
pf "%a" pp_diff (r, r') ;
invariant r']
let and_eq_ ~wrt a b r =
if not r.sat then r
let and_eq_ ~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') ;
invariant x' )
@@ fun () ->
if not x.sat then x
else
let r0 = r in
let a' = canon r a in
let b' = canon r b in
let r = extend a' r in
let r = extend b' r in
if Trm.equal a' b' then r
let x0 = x in
let a' = canon x a in
let b' = canon x b in
if Trm.equal a' b' then extend a' (extend b' x)
else
let r = merge ~wrt a' b' r in
let x = merge ~wrt a' b' x in
match (a, b) with
| (Var _ as v), _ when not (in_car r0 v) -> r
| _, (Var _ as v) when not (in_car r0 v) -> r
| _ -> close ~wrt r
| (Var _ as v), _ when not (in_car x0 v) -> x
| _, (Var _ as v) when not (in_car x0 v) -> x
| _ -> close ~wrt x
let extract_xs r = (r.xs, {r with xs= Var.Set.empty})
@ -545,6 +605,10 @@ let implies r b =
let refutes r b = Fml.equal Fml.ff (canon_f r b)
let normalize r e = Term.map_trms ~f:(canon r) e
let cls_of r e =
let e' = Subst.apply r.rep e in
Trm.Map.find e' r.cls |> Option.value ~default:(Cls.of_ e')
let class_of r e =
match Term.get_trm (normalize r e) with
| Some e' ->
@ -552,7 +616,7 @@ let class_of r e =
| None -> []
let diff_classes r s =
Trm.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
Trm.Map.filter_mapi r.cls ~f:(fun ~key:rep ~data:cls ->
let cls' =
Cls.filter cls ~f:(fun exp -> not (implies s (Fml.eq rep exp)))
in
@ -584,7 +648,7 @@ let apply_subst wrt s r =
;
( if Subst.is_empty s then r
else
Trm.Map.fold (classes r) {r with rep= Subst.empty}
Trm.Map.fold r.cls {r with rep= Subst.empty; cls= Trm.Map.empty}
~f:(fun ~key:rep ~data:cls r ->
let rep' = Subst.subst_ s rep in
Cls.fold cls r ~f:(fun trm r ->
@ -619,7 +683,7 @@ let inter wrt r s =
else if not r.sat then s
else
let merge_mems rs r s =
Trm.Map.fold (classes s) rs ~f:(fun ~key:rep ~data:cls rs ->
Trm.Map.fold s.cls rs ~f:(fun ~key:rep ~data:cls rs ->
Cls.fold cls
([rep], rs)
~f:(fun exp (reps, rs) ->
@ -673,17 +737,23 @@ let dnf f =
let bot = Iter.empty in
Fml.fold_dnf ~meet1 ~join1 ~top ~bot f
let rename r sub =
[%Trace.call fun {pf} -> pf "@ @[%a@]@ %a" Var.Subst.pp sub pp r]
;
let rep =
Subst.map_entries ~f:(Trm.map_vars ~f:(Var.Subst.apply sub)) r.rep
let rename x sub =
[%trace]
~call:(fun {pf} -> pf "@ @[%a@]@ %a" Var.Subst.pp sub pp x)
~retn:(fun {pf} x' ->
pf "%a" pp_diff (x, x') ;
invariant x' )
@@ fun () ->
let apply_sub = Trm.map_vars ~f:(Var.Subst.apply sub) in
let rep = Subst.map_entries ~f:apply_sub x.rep in
let cls =
Trm.Map.fold x.cls x.cls ~f:(fun ~key:a0' ~data:a0'_cls cls ->
let a' = apply_sub a0' in
let a'_cls = Cls.map ~f:apply_sub a0'_cls in
Trm.Map.add ~key:a' ~data:a'_cls
(if a' == a0' then cls else Trm.Map.remove a0' cls) )
in
(if rep == r.rep then r else {r with rep})
|>
[%Trace.retn fun {pf} r' ->
pf "%a" pp_diff (r, r') ;
invariant r']
if rep == x.rep && cls == x.cls then x else {x with rep; cls}
let trms r =
Iter.flat_map ~f:(fun (k, v) -> Iter.doubleton k v) (Subst.to_iter r.rep)
@ -904,6 +974,8 @@ let solve_uninterp_eqs us (cls, subst) =
let cls = Cls.add rep_xs cls_us in
let subst =
Cls.fold cls_xs subst ~f:(fun trm_xs subst ->
let trm_xs = Subst.subst_ subst trm_xs in
let rep_xs = Subst.subst_ subst rep_xs in
Subst.compose1 ~key:trm_xs ~data:rep_xs subst )
in
(cls, subst)
@ -941,7 +1013,7 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
|>
[%Trace.retn fun {pf} (classes', subst') ->
pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst')
pp_diff_clss (classes0, classes')]
pp_diff_cls (classes0, classes')]
let solve_concat_extracts_eq r x =
[%Trace.call fun {pf} -> pf "@ %a@ %a" Trm.pp x pp r]
@ -1022,7 +1094,7 @@ let solve_classes r xs (classes, subst, us) =
|>
[%Trace.retn fun {pf} (classes', subst', _) ->
pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst')
pp_diff_clss (classes, classes')]
pp_diff_cls (classes, classes')]
let pp_vss fs vss =
Format.fprintf fs "[@[%a@]]"
@ -1042,7 +1114,7 @@ let solve_for_vars vss r =
let us, vss =
match vss with us :: vss -> (us, vss) | [] -> (Var.Set.empty, vss)
in
List.fold ~f:(solve_classes r) vss (classes r, Subst.empty, us) |> snd3
List.fold ~f:(solve_classes r) vss (r.cls, Subst.empty, us) |> snd3
|>
[%Trace.retn fun {pf} subst ->
pf "%a" Subst.pp subst ;
@ -1079,57 +1151,73 @@ let trivial vs r =
Var.Set.add v ks
| _ -> ks )
let trim ks r =
let trim ks x =
[%trace]
~call:(fun {pf} -> pf "@ %a@ %a" Var.Set.pp_xs ks pp_raw r)
~retn:(fun {pf} r' ->
pf "%a" pp_raw r' ;
assert (Var.Set.disjoint ks (fv r')) )
~call:(fun {pf} -> pf "@ %a@ %a" Var.Set.pp_xs ks pp_raw x)
~retn:(fun {pf} x' ->
pf "%a" pp_raw x' ;
invariant x' ;
assert (Var.Set.disjoint ks (fv x')) )
@@ fun () ->
let kills = Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter ks)) in
(* compute classes including reps *)
(* expand classes to include reps *)
let reps =
Subst.fold r.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps ->
Subst.fold x.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps ->
Trm.Set.add rep reps )
in
let clss =
Trm.Set.fold reps (classes r) ~f:(fun rep clss ->
Trm.Set.fold reps x.cls ~f:(fun rep clss ->
Trm.Map.update rep clss ~f:(fun cls0 ->
Cls.add rep (Option.value cls0 ~default:Cls.empty) ) )
in
(* trim classes to those that intersect kills *)
let clss =
Trm.Map.filter_mapi clss ~f:(fun ~key:_ ~data:cls ->
let cls = Cls.to_set cls in
if Trm.Set.disjoint kills cls then None else Some cls )
in
(* enumerate affected classes and update solution subst *)
let rep =
Trm.Map.fold clss r.rep ~f:(fun ~key:rep ~data:cls s ->
(* remove mappings for non-rep class elements to kill *)
let drop = Trm.Set.inter cls kills in
let s = Trm.Set.fold ~f:Subst.remove drop s in
if not (Trm.Set.mem rep kills) then s
(* enumerate expanded classes and update solution subst *)
let kills = Trm.Set.of_vars ks in
Trm.Map.fold clss x ~f:(fun ~key:a' ~data:ecls x ->
(* remove mappings for non-rep class elements to kill *)
let keep, drop = Trm.Set.diff_inter (Cls.to_set ecls) kills in
if Trm.Set.is_empty drop then x
else
let rep = Trm.Set.fold ~f:Subst.remove drop x.rep in
let x = {x with rep} in
(* new class is keepers without rep *)
let keep' = Trm.Set.remove a' keep in
let ecls = Cls.of_set keep' in
if keep' != keep then
(* a' is to be kept: continue to use it as rep *)
let cls =
if Cls.is_empty ecls then Trm.Map.remove a' x.cls
else Trm.Map.add ~key:a' ~data:ecls x.cls
in
{x with cls}
else
(* if rep is to be removed, choose new one from the keepers *)
let keep = Trm.Set.diff cls drop in
(* a' is to be removed: choose new rep from the keepers *)
let cls = Trm.Map.remove a' x.cls in
let x = {x with cls} in
match
Trm.Set.reduce keep ~f:(fun x y ->
if Theory.prefer x y < 0 then x else y )
with
| Some rep' ->
| Some b' ->
(* add mappings from each keeper to the new representative *)
Trm.Set.fold keep s ~f:(fun elt s ->
Subst.add ~key:elt ~data:rep' s )
| None -> s )
in
{r with rep}
let rep =
Trm.Set.fold keep x.rep ~f:(fun elt rep ->
Subst.add ~key:elt ~data:b' rep )
in
(* add trimmed class to new rep *)
let cls =
if Cls.is_empty ecls then x.cls
else Trm.Map.add ~key:b' ~data:ecls x.cls
in
{x with rep; cls}
| None ->
(* entire class removed *)
x )
let apply_and_elim ~wrt xs s r =
[%trace]
~call:(fun {pf} -> pf "@ %a%a@ %a" Var.Set.pp_xs xs Subst.pp s pp_raw r)
~retn:(fun {pf} (zs, r', ks) ->
pf "%a@ %a@ %a" Var.Set.pp_xs zs pp_raw r' Var.Set.pp_xs ks ;
invariant r' ;
assert (Var.Set.subset ks ~of_:xs) ;
assert (Var.Set.disjoint ks (fv r')) )
@@ fun () ->

5
sledge/src/fol/trm.ml
Unescape View File

@ -393,6 +393,11 @@ module Set = struct
include Set.Make (T)
include Provide_of_sexp (T)
include Provide_pp (T)
let of_vars : Var.Set.t -> t =
fun vs ->
of_iter
(Iter.map ~f:(fun v -> (v : Var.t :> Trm.t)) (Var.Set.to_iter vs))
end
module Map = struct

1
sledge/src/fol/trm.mli
Unescape View File

@ -43,6 +43,7 @@ module Set : sig
val t_of_sexp : Sexp.t -> t
val pp : t pp
val pp_diff : (t * t) pp
val of_vars : Var.Set.t -> t
end
module Map : sig

50
sledge/src/test/context_test.ml
Unescape View File

@ -61,8 +61,8 @@ let%test_module _ =
pp r3 ;
[%expect
{|
%t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3
= %u_2
%t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %v_3)
= g(%y_6, %z_7)
{sat= true;
rep= [[%t_1 ↦ ];
@ -73,7 +73,10 @@ let%test_module _ =
[%y_6 ↦ ];
[%z_7 ↦ %t_1];
[g(%y_6, %v_3) ↦ %t_1];
[g(%y_6, %z_7) ↦ %t_1]]} |}]
[g(%y_6, %z_7) ↦ %t_1]];
cls= [[%t_1
↦ {%u_2, %v_3, %w_4, %x_5, %z_7, g(%y_6, %v_3),
g(%y_6, %z_7)}]]} |}]
let%test _ = implies_eq r3 t z
@ -82,8 +85,9 @@ let%test_module _ =
let%expect_test _ =
pp r15 ;
[%expect {|
{sat= true; rep= [[%x_5 ↦ 1]]} |}]
[%expect
{|
{sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}]
let%test _ = implies_eq r15 (Term.neg b) (Term.apply (Signed 1) [|!1|])
let%test _ = implies_eq r15 (Term.apply (Unsigned 1) [|b|]) !1
@ -91,24 +95,22 @@ 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)))))
(pnd ())))|} ;
(()
((Var (id 0) (name 0)) (Var (id 0) (name 2)) (Var (id 0) (name 4))
(Var (id 0) (name 5)) (Var (id 0) (name 7)) (Var (id 0) (name 8))
(Var (id 0) (name 9)) (Var (id 1) (name a)) (Var (id 2) (name a))
(Var (id 3) (name a)))
())
((xs ()) (sat true)
(rep
(((Apply (Uninterp g.1) ()) (Apply (Uninterp g.1) ()))
((Var (id 0) (name 4)) (Var (id 0) (name 0)))
((Var (id 0) (name 2)) (Var (id 0) (name 0)))
((Var (id 0) (name 0)) (Var (id 0) (name 0)))))
(cls
(((Var (id 0) (name 0))
((Var (id 0) (name 2)) (Var (id 0) (name 4))
(Var (id 0) (name 2))))))
(pnd ())))|} ;
[%expect {| |}]
end )

129
sledge/src/test/fol_test.ml
Unescape View File

@ -16,7 +16,10 @@ let%test_module _ =
(* let () =
* Trace.init ~margin:160
* ~config:(Result.get_ok (Trace.parse "+Fol+Context+Arithmetic"))
* ~config:
* (Result.get_ok
* (Trace.parse
* "+Fol+Context-Context.canon-Context.canon_f-Context.norm"))
* () *)
[@@@warning "-32"]
@ -66,7 +69,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f1 ;
[%expect {| {sat= false; rep= []} |}]
[%expect {| {sat= false; rep= []; cls= []} |}]
let%test _ = is_unsat (add_eq !1 !1 f1)
@ -76,7 +79,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f2 ;
[%expect {| {sat= false; rep= []} |}]
[%expect {| {sat= false; rep= []; cls= []} |}]
let f3 = of_eqs [(x + !0, x + !1)]
@ -84,7 +87,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw f3 ;
[%expect {| {sat= false; rep= []} |}]
[%expect {| {sat= false; rep= []; cls= []} |}]
let f4 = of_eqs [(x, y); (x + !0, y + !1)]
@ -92,7 +95,11 @@ let%test_module _ =
let%expect_test _ =
pp_raw f4 ;
[%expect {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
[%expect
{|
{sat= false;
rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]];
cls= [[%x_5 ↦ {%y_6}]]} |}]
let t1 = of_eqs [(!1, !1)]
@ -108,7 +115,7 @@ let%test_module _ =
let%expect_test _ =
pp_raw r0 ;
[%expect {| {sat= true; rep= []} |}]
[%expect {| {sat= true; rep= []; cls= []} |}]
let%expect_test _ =
pp r0 ;
@ -127,7 +134,7 @@ let%test_module _ =
%x_5 = %y_6
{sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
{sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]; cls= [[%x_5 ↦ {%y_6}]]} |}]
let%test _ = implies_eq r1 x y
@ -138,10 +145,11 @@ let%test_module _ =
pp_raw r2 ;
[%expect
{|
%x_5 = f(%x_5) = %z_7 = %y_6
%x_5 = %y_6 = %z_7 = f(%x_5)
{sat= true;
rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}]
rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]];
cls= [[%x_5 ↦ {%y_6, %z_7, f(%x_5)}]]} |}]
let%test _ = implies_eq r2 x z
let%test _ = implies_eq (inter r1 r2) x y
@ -162,11 +170,15 @@ let%test_module _ =
pp_raw rs ;
[%expect
{|
{sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
{sat= true;
rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]];
cls= [[%w_4 ↦ {%y_6, %z_7}]]}
{sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
{sat= true;
rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]];
cls= [[%x_5 ↦ {%y_6, %z_7}]]}
{sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}]
{sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}]
let%test _ =
let r = of_eqs [(w, y); (y, z)] in
@ -181,9 +193,9 @@ let%test_module _ =
pp_raw r3 ;
[%expect
{|
%t_1 = g(%y_6, %z_7) = g(%y_6, %v_3) = %z_7 = %x_5 = %w_4 = %v_3
= %u_2
%t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %v_3)
= g(%y_6, %z_7)
{sat= true;
rep= [[%t_1 ↦ ];
[%u_2 ↦ %t_1];
@ -193,7 +205,10 @@ let%test_module _ =
[%y_6 ↦ ];
[%z_7 ↦ %t_1];
[g(%y_6, %v_3) ↦ %t_1];
[g(%y_6, %z_7) ↦ %t_1]]} |}]
[g(%y_6, %z_7) ↦ %t_1]];
cls= [[%t_1
↦ {%u_2, %v_3, %w_4, %x_5, %z_7, g(%y_6, %v_3),
g(%y_6, %z_7)}]]} |}]
let%test _ = implies_eq r3 t z
let%test _ = implies_eq r3 x z
@ -212,7 +227,10 @@ let%test_module _ =
rep= [[%w_4 ↦ (3 + %z_7)];
[%x_5 ↦ (8 + %z_7)];
[%y_6 ↦ (-4 + %z_7)];
[%z_7 ↦ ]]} |}]
[%z_7 ↦ ]];
cls= [[(-4 + %z_7) ↦ {%y_6}];
[(3 + %z_7) ↦ {%w_4}];
[(8 + %z_7) ↦ {%x_5}]]} |}]
let%test _ = implies_eq r4 x (w + !5)
let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@ -228,9 +246,11 @@ let%test_module _ =
pp_raw r6 ;
[%expect
{|
1 = %y_6 = %x_5
1 = %x_5 = %y_6
{sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}]
{sat= true;
rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]];
cls= [[1 ↦ {%x_5, %y_6}]]} |}]
let%test _ = implies_eq r6 x y
@ -241,14 +261,15 @@ let%test_module _ =
pp_raw r7 ;
[%expect
{|
%v_3 = %x_5 ∧ %w_4 = %z_7 = %y_6
%v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
{sat= true;
rep= [[%v_3 ↦ ];
[%w_4 ↦ ];
[%x_5 ↦ %v_3];
[%y_6 ↦ %w_4];
[%z_7 ↦ %w_4]]} |}]
[%z_7 ↦ %w_4]];
cls= [[%v_3 ↦ {%x_5}]; [%w_4 ↦ {%y_6, %z_7}]]} |}]
let r7' = add_eq x z r7
@ -257,14 +278,15 @@ let%test_module _ =
pp_raw r7' ;
[%expect
{|
%v_3 = %z_7 = %y_6 = %x_5 = %w_4
%v_3 = %w_4 = %x_5 = %y_6 = %z_7
{sat= true;
rep= [[%v_3 ↦ ];
[%w_4 ↦ %v_3];
[%x_5 ↦ %v_3];
[%y_6 ↦ %v_3];
[%z_7 ↦ %v_3]]} |}]
[%z_7 ↦ %v_3]];
cls= [[%v_3 ↦ {%w_4, %x_5, %y_6, %z_7}]]} |}]
let%test _ = normalize r7' w |> Term.equal v
@ -283,7 +305,9 @@ let%test_module _ =
{|
14 = %y_6 ∧ 13×%z_7 = %x_5
{sat= true; rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]]} |}]
{sat= true;
rep= [[%x_5 ↦ 13×%z_7]; [%y_6 ↦ 14]; [%z_7 ↦ ]];
cls= [[14 ↦ {%y_6}]; [13×%z_7 ↦ {%x_5}]]} |}]
let%test _ = implies_eq r8 y !14
@ -294,9 +318,13 @@ let%test_module _ =
pp_raw r9 ;
[%expect
{|
{sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
{sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]} |}]
{sat= true;
rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]];
cls= [[(-16 + %z_7) ↦ {%x_5}]]}
{sat= true;
rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]];
cls= [[(-16 + %z_7) ↦ {%x_5}]]} |}]
let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
@ -311,16 +339,20 @@ let%test_module _ =
Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
[%expect
{|
{sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
{sat= true;
rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]];
cls= [[(-16 + %z_7) ↦ {%x_5}]]}
{sat= true; rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]]}
{sat= true;
rep= [[%x_5 ↦ (-16 + %z_7)]; [%z_7 ↦ ]];
cls= [[(-16 + %z_7) ↦ {%x_5}]]}
(-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))
@ -348,7 +380,8 @@ let%test_module _ =
let%expect_test _ =
pp_raw r13 ;
[%expect {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}]
[%expect
{| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]; cls= [[%y_6 ↦ {%z_7}]]} |}]
let%test _ = not (is_unsat r13) (* incomplete *)
@ -357,8 +390,9 @@ let%test_module _ =
let%expect_test _ =
pp_raw r14 ;
[%expect {|
{sat= true; rep= [[%x_5 ↦ 1]]} |}]
[%expect
{|
{sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}]
let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
@ -367,8 +401,9 @@ let%test_module _ =
let%expect_test _ =
pp_raw r14 ;
[%expect {|
{sat= true; rep= [[%x_5 ↦ 1]]} |}]
[%expect
{|
{sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}]
let%test _ = implies_eq r14 a (Formula.inject Formula.tt)
(* incomplete *)
@ -379,8 +414,9 @@ let%test_module _ =
let%expect_test _ =
pp_raw r15 ;
[%expect {|
{sat= true; rep= [[%x_5 ↦ 1]]} |}]
[%expect
{|
{sat= true; rep= [[%x_5 ↦ 1]]; cls= [[1 ↦ {%x_5}]]} |}]
(* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *)
let r16 =
@ -394,7 +430,10 @@ let%test_module _ =
rep= [[%x_5 ↦ (1 + %y_6)];
[%y_6 ↦ ];
[f(%y_6) ↦ (-2 + %y_6)];
[f((-1 + %x_5)) ↦ (3 + %y_6)]]} |}]
[f((-1 + %x_5)) ↦ (3 + %y_6)]];
cls= [[(-2 + %y_6) ↦ {f(%y_6)}];
[(1 + %y_6) ↦ {%x_5}];
[(3 + %y_6) ↦ {f((-1 + %x_5))}]]} |}]
let%test _ = is_unsat r16
@ -409,7 +448,8 @@ let%test_module _ =
rep= [[%x_5 ↦ ];
[%y_6 ↦ %x_5];
[f(%x_5) ↦ %x_5];
[f(%y_6) ↦ (-1 + %x_5)]]} |}]
[f(%y_6) ↦ (-1 + %x_5)]];
cls= [[%x_5 ↦ {%y_6, f(%x_5)}]; [(-1 + %x_5) ↦ {f(%y_6)}]]} |}]
let%test _ = is_unsat r17
@ -423,8 +463,9 @@ let%test_module _ =
rep= [[%x_5 ↦ ];
[%y_6 ↦ ];
[f(%x_5) ↦ %x_5];
[f(%y_6) ↦ (-1 + %y_6)]]}
[f(%y_6) ↦ (-1 + %y_6)]];
cls= [[%x_5 ↦ {f(%x_5)}]; [(-1 + %y_6) ↦ {f(%y_6)}]]}
%x_5 = f(%x_5) ∧ (-1 + %y_6) = f(%y_6) |}]
let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
@ -433,7 +474,9 @@ let%test_module _ =
pp_raw r19 ;
[%expect
{|
{sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}]
{sat= true;
rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]];
cls= [[0 ↦ {%x_5, %y_6, %z_7}]]} |}]
let%test _ = implies_eq r19 x !0
let%test _ = implies_eq r19 y !0

4
sledge/src/test/sh_test.ml
Unescape View File

@ -101,7 +101,7 @@ let%test_module _ =
( ( 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)
∨ (∃ %x_7 . 1 = %x_7 = %y_8 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp)
∨ ( 0 = %x_7 ∧ (0 = %x_7) ∧ emp)
) |}]
@ -125,7 +125,7 @@ let%test_module _ =
( (∃ %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))
1 = %y_8 = %x_9 ∧ ((1 = %y_8) ∧ (1 = %x_9))
∧ emp)
∨ (∃ %x_7 . 0 = %x_7 ∧ (0 = %x_7) ∧ emp)
) |}]

Write Preview
Loading…
Cancel
Save