From 682fb9158cda38ca704fe37a6a189f7846728926 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 02:38:16 -0700 Subject: [PATCH] [sledge] Switch from Base.Map to Containers.Map Summary: The form of the Base containers interface, in particular the way comparison functions are passed using Comparators, is slower than standard functors. Also Base.Map is missing some operations, such as efficient merge and union. Reviewed By: jvillard Differential Revision: D24306047 fbshipit-source-id: e1623b693 --- sledge/nonstdlib/map.ml | 167 ++++++++++++++++++++++--------- sledge/nonstdlib/map_intf.ml | 119 +++++++++++++++++----- sledge/nonstdlib/qset.ml | 4 +- sledge/src/test/equality_test.ml | 22 ++-- sledge/src/test/fol_test.ml | 166 +++++++++++++++--------------- sledge/src/test/sh_test.ml | 2 +- sledge/src/test/solver_test.ml | 30 +++--- sledge/src/test/term_test.ml | 63 ++++++------ 8 files changed, 356 insertions(+), 217 deletions(-) diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml index 91791740c..9acfab4b4 100644 --- a/sledge/nonstdlib/map.ml +++ b/sledge/nonstdlib/map.ml @@ -11,24 +11,39 @@ include Map_intf module Make (Key : sig type t [@@deriving compare, sexp_of] end) : S with type key = Key.t = struct - module KeyMap = Core.Map.Make_plain (Key) - module Key = KeyMap.Key + module M = CCMap.Make (Key) type key = Key.t - - include KeyMap.Tree - - let compare = compare_direct - - let to_map t = - Core.Map.Using_comparator.of_tree ~comparator:Key.comparator t - - let of_map m = Base.Map.Using_comparator.to_tree m - - let merge_skewed x y ~combine = - of_map (Core.Map.merge_skewed (to_map x) (to_map y) ~combine) - - let map_endo t ~f = map_endo map t ~f + type 'a t = 'a M.t [@@deriving compare, equal] + + let sexp_of_t sexp_of_data m = + M.to_list m + |> Sexplib.Conv.sexp_of_list + (Sexplib.Conv.sexp_of_pair Key.sexp_of_t sexp_of_data) + + module Provide_of_sexp (Key : sig + type t = key [@@deriving of_sexp] + end) = + struct + let t_of_sexp data_of_sexp s = + s + |> Sexplib.Conv.list_of_sexp + (Sexplib.Conv.pair_of_sexp Key.t_of_sexp data_of_sexp) + |> M.of_list + end + + let empty = M.empty + let singleton = M.singleton + let add_exn m ~key ~data = M.add key data m + let set m ~key ~data = M.add key data m + + let add_multi m ~key ~data = + M.update key + (function Some vs -> Some (data :: vs) | None -> Some [data]) + m + + let remove m key = M.remove key m + let merge l r ~f = M.merge_safe l r ~f:(fun key -> f ~key) let merge_endo t u ~f = let change = ref false in @@ -43,49 +58,107 @@ end) : S with type key = Key.t = struct in if !change then t' else t - let fold_until m ~init ~f ~finish = - let fold m ~init ~f = - let f ~key ~data s = f s (key, data) in - fold m ~init ~f - in - let f s (k, v) = f ~key:k ~data:v s in - Container.fold_until ~fold ~init ~f ~finish m - - let root_key_exn m = - let@ {return} = with_return in - binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data:_ -> - return key ) - |> ignore ; - raise (Not_found_s (Atom __LOC__)) - - let choose_exn m = - let@ {return} = with_return in - binary_search_segmented m `Last_on_left ~segment_of:(fun ~key ~data -> - return (key, data) ) - |> ignore ; - raise (Not_found_s (Atom __LOC__)) + let merge_skewed x y ~combine = + M.union (fun key v1 v2 -> Some (combine ~key v1 v2)) x y - let choose m = try Some (choose_exn m) with Not_found_s _ -> None - let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k)) + let union x y ~f = M.union f x y + let is_empty = M.is_empty - let pop_min_elt m = - min_elt m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k)) + let root_key m = + let exception Found in + let found = ref None in + try + M.find_first + (fun key -> + found := Some key ; + raise Found ) + m + |> ignore ; + None + with + | Found -> !found + | Not_found -> None + + let root_binding m = + let exception Found in + let found = ref None in + try + M.for_all + (fun key data -> + found := Some (key, data) ; + raise Found ) + m + |> ignore ; + None + with + | Found -> !found + | Not_found -> None let is_singleton m = - try - let l, _, r = split m (root_key_exn m) in - is_empty l && is_empty r - with Not_found_s _ -> false + match root_key m with + | Some k -> + let l, _, r = M.split k m in + is_empty l && is_empty r + | None -> false + + let length = M.cardinal + let choose_key = root_key + let choose = root_binding + let choose_exn m = CCOpt.get_exn (choose m) + let min_binding = M.min_binding_opt + let mem m k = M.mem k m + let find_exn m k = M.find k m + let find m k = M.find_opt k m + + let find_multi m k = + match M.find_opt k m with None -> [] | Some vs -> vs let find_and_remove m k = let found = ref None in let m = - change m k ~f:(fun v -> + M.update k + (fun v -> found := v ; None ) + m in Option.map ~f:(fun v -> (v, m)) !found + let pop m = choose m |> CCOpt.map (fun (k, v) -> (k, v, remove m k)) + + let pop_min_binding m = + min_binding m |> CCOpt.map (fun (k, v) -> (k, v, remove m k)) + + let change m key ~f = M.update key f m + let update m k ~f = M.update k (fun v -> Some (f v)) m + let map m ~f = M.map f m + let mapi m ~f = M.mapi (fun key data -> f ~key ~data) m + let map_endo t ~f = map_endo map t ~f + let filter_mapi m ~f = M.filter_map (fun key data -> f ~key ~data) m + let iter m ~f = M.iter (fun _ data -> f data) m + let iteri m ~f = M.iter (fun key data -> f ~key ~data) m + let existsi m ~f = M.exists (fun key data -> f ~key ~data) m + let for_alli m ~f = M.for_all (fun key data -> f ~key ~data) m + let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init + let to_alist ?key_order:_ = M.to_list + let data m = Iter.to_list (M.values m) + + let to_iter2 l r = + let seq = ref Iter.empty in + M.merge_safe l r ~f:(fun k vv -> + seq := Iter.cons (k, vv) !seq ; + None ) + |> ignore ; + !seq + + let symmetric_diff ~data_equal l r = + Iter.filter_map (to_iter2 l r) ~f:(fun (k, vv) -> + match vv with + | `Both (lv, rv) when data_equal lv rv -> None + | `Both vv -> Some (k, `Unequal vv) + | `Left lv -> Some (k, `Left lv) + | `Right rv -> Some (k, `Right rv) ) + let pp pp_k pp_v fs m = Format.fprintf fs "@[<1>[%a]@]" (List.pp ",@ " (fun fs (k, v) -> @@ -101,7 +174,7 @@ end) : S with type key = Key.t = struct | k, `Unequal vv -> Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv in - let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in + let sd = Iter.to_list (symmetric_diff ~data_equal x y) in if not (List.is_empty sd) then Format.fprintf fs "[@[%a@]];@ " (List.pp ";@ " pp_diff_elt) sd end diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml index 8966cfdb1..89026a1f4 100644 --- a/sledge/nonstdlib/map_intf.ml +++ b/sledge/nonstdlib/map_intf.ml @@ -7,60 +7,127 @@ open NS0 +exception Not_found = Stdlib.Not_found + module type S = sig type key + type +'a t [@@deriving compare, equal, sexp_of] - module Key : sig - type t = key - - include Comparator.S with type t := t + module Provide_of_sexp (_ : sig + type t = key [@@deriving of_sexp] + end) : sig + val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t end - include Core_kernel.Map_intf.Make_S_plain_tree(Key).S + (** {1 Construct} *) - val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int - val is_singleton : 'a t -> bool + val empty : 'a t + val singleton : key -> 'a -> 'a t + val add_exn : 'a t -> key:key -> data:'a -> 'a t + val set : 'a t -> key:key -> data:'a -> 'a t + val add_multi : 'a list t -> key:key -> data:'a -> 'a list t + val remove : 'a t -> key -> 'a t - val map_endo : 'a t -> f:('a -> 'a) -> 'a t - (** Like map, but specialized to require [f] to be an endofunction, which - enables preserving [==] if [f] preserves [==] of every element. *) + val merge : + 'a t + -> 'b t + -> f: + ( key:key + -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b] + -> 'c option) + -> 'c t val merge_endo : 'a t -> 'b t -> f: ( key:key - -> [`Both of 'a * 'b | `Left of 'a | `Right of 'b] + -> [`Left of 'a | `Both of 'a * 'b | `Right of 'b] -> 'a option) -> 'a t (** Like merge, but specialized to require [f] to preserve the type of the left argument, which enables preserving [==] if [f] preserves [==] of - every element. *) + every value. *) val merge_skewed : 'a t -> 'a t -> combine:(key:key -> 'a -> 'a -> 'a) -> 'a t - val fold_until : - 'v t - -> init:'a - -> f:(key:key -> data:'v -> 'a -> ('a, 'r) Continue_or_stop.t) - -> finish:('a -> 'r) - -> 'r + val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t - val choose_exn : 'a t -> key * 'a - (** Find an unspecified element. [O(1)]. *) + (** {1 Query} *) + + val is_empty : 'a t -> bool + val is_singleton : 'a t -> bool + val length : 'a t -> int + + val choose_key : 'a t -> key option + (** Find an unspecified key. Different keys may be chosen for equivalent + maps. [O(1)]. *) val choose : 'a t -> (key * 'a) option - (** Find an unspecified element. [O(1)]. *) + (** Find an unspecified binding. Different bindings may be chosen for + equivalent maps. [O(1)]. *) - val pop : 'a t -> (key * 'a * 'a t) option - (** Find and remove an unspecified element. [O(1)]. *) + val choose_exn : 'a t -> key * 'a + (** Find an unspecified binding. Different bindings may be chosen for + equivalent maps. [O(1)]. *) - val pop_min_elt : 'a t -> (key * 'a * 'a t) option - (** Find and remove minimum element. [O(log n)]. *) + val min_binding : 'a t -> (key * 'a) option + val mem : 'a t -> key -> bool + val find : 'a t -> key -> 'a option + val find_exn : 'a t -> key -> 'a + val find_multi : 'a list t -> key -> 'a list val find_and_remove : 'a t -> key -> ('a * 'a t) option - (** Find and remove an element. *) + (** Find and remove the binding for a key. *) + + val pop : 'a t -> (key * 'a * 'a t) option + (** Find and remove an unspecified binding. Different bindings may be + chosen for equivalent maps. [O(1)]. *) + + val pop_min_binding : 'a t -> (key * 'a * 'a t) option + (** Find and remove binding with minimum key. [O(log n)]. *) + + (** {1 Transform} *) + + val change : 'a t -> key -> f:('a option -> 'a option) -> 'a t + val update : 'a t -> key -> f:('a option -> 'a) -> 'a t + val map : 'a t -> f:('a -> 'b) -> 'b t + val mapi : 'a t -> f:(key:key -> data:'a -> 'b) -> 'b t + + val map_endo : 'a t -> f:('a -> 'a) -> 'a t + (** Like map, but specialized to require [f] to be an endofunction, which + enables preserving [==] if [f] preserves [==] of every value. *) + + val filter_mapi : 'a t -> f:(key:key -> data:'a -> 'b option) -> 'b t + + (** {1 Traverse} *) + + val iter : 'a t -> f:('a -> unit) -> unit + val iteri : 'a t -> f:(key:key -> data:'a -> unit) -> unit + val existsi : 'a t -> f:(key:key -> data:'a -> bool) -> bool + val for_alli : 'a t -> f:(key:key -> data:'a -> bool) -> bool + val fold : 'a t -> init:'b -> f:(key:key -> data:'a -> 'b -> 'b) -> 'b + + (** {1 Convert} *) + + val to_alist : + ?key_order:[`Increasing | `Decreasing] -> 'a t -> (key * 'a) list + + val data : 'a t -> 'a list + + val to_iter2 : + 'a t + -> 'b t + -> (key * [`Left of 'a | `Both of 'a * 'b | `Right of 'b]) iter + + val symmetric_diff : + data_equal:('a -> 'b -> bool) + -> 'a t + -> 'b t + -> (key * [> `Left of 'a | `Unequal of 'a * 'b | `Right of 'b]) iter + + (** {1 Pretty-print} *) val pp : key pp -> 'a pp -> 'a t pp diff --git a/sledge/nonstdlib/qset.ml b/sledge/nonstdlib/qset.ml index b1ff1f006..50f584178 100644 --- a/sledge/nonstdlib/qset.ml +++ b/sledge/nonstdlib/qset.ml @@ -80,8 +80,8 @@ struct let choose = M.choose let choose_exn = M.choose_exn let pop = M.pop - let min_elt = M.min_elt - let pop_min_elt = M.pop_min_elt + let min_elt = M.min_binding + let pop_min_elt = M.pop_min_binding let classify s = match pop s with diff --git a/sledge/src/test/equality_test.ml b/sledge/src/test/equality_test.ml index 7b803b2e1..f822e7d02 100644 --- a/sledge/src/test/equality_test.ml +++ b/sledge/src/test/equality_test.ml @@ -62,17 +62,17 @@ let%test_module _ = = (%y_6 rem %t_1) {sat= true; - rep= [[%t_1 ↦ ]; - [%u_2 ↦ %t_1]; - [%v_3 ↦ %t_1]; - [%w_4 ↦ %t_1]; - [%x_5 ↦ %t_1]; - [%y_6 ↦ ]; - [%z_7 ↦ %t_1]; - [(%y_6 rem %v_3) ↦ %t_1]; - [(%y_6 rem %z_7) ↦ %t_1]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [(%y_6 rem %z_7) ↦ %t_1]; + [(%y_6 rem %v_3) ↦ %t_1]; + [%z_7 ↦ %t_1]; + [%y_6 ↦ ]; + [%x_5 ↦ %t_1]; + [%w_4 ↦ %t_1]; + [%v_3 ↦ %t_1]; + [%u_2 ↦ %t_1]; + [%t_1 ↦ ]]} |}] let%test _ = implies_eq r3 t z @@ -83,7 +83,7 @@ let%test_module _ = pp r15 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [%x_5 ↦ 1]]} |}] let%test _ = implies_eq r15 b (Term.signed 1 !1) let%test _ = implies_eq r15 (Term.unsigned 1 b) !1 diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 314f4159b..6818497f4 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -66,7 +66,7 @@ let%test_module _ = let%expect_test _ = pp_raw f1 ; - [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]]} |}] let%test _ = is_unsat (add_eq !1 !1 f1) @@ -76,7 +76,7 @@ let%test_module _ = let%expect_test _ = pp_raw f2 ; - [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}] let f3 = of_eqs [(x + !0, x + !1)] @@ -84,7 +84,7 @@ let%test_module _ = let%expect_test _ = pp_raw f3 ; - [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ ]]} |}] let f4 = of_eqs [(x, y); (x + !0, y + !1)] @@ -93,7 +93,7 @@ let%test_module _ = let%expect_test _ = pp_raw f4 ; [%expect - {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}] + {| {sat= false; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}] let t1 = of_eqs [(!1, !1)] @@ -109,7 +109,7 @@ let%test_module _ = let%expect_test _ = pp_raw r0 ; - [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] + [%expect {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]]} |}] let%expect_test _ = pp r0 ; @@ -128,7 +128,7 @@ let%test_module _ = %x_5 = %y_6 - {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} |}] let%test _ = implies_eq r1 x y @@ -142,12 +142,12 @@ let%test_module _ = %x_5 = %y_6 = %z_7 = %x_5^ {sat= true; - rep= [[%x_5 ↦ ]; - [%y_6 ↦ %x_5]; - [%z_7 ↦ %x_5]; - [%x_5^ ↦ %x_5]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [%x_5^ ↦ %x_5]; + [%z_7 ↦ %x_5]; + [%y_6 ↦ %x_5]; + [%x_5 ↦ ]]} |}] let%test _ = implies_eq r2 x z let%test _ = implies_eq (inter r1 r2) x y @@ -169,12 +169,12 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]; [-1 ↦ ]; [0 ↦ ]]} + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %w_4]; [%y_6 ↦ %w_4]; [%w_4 ↦ ]]} {sat= true; - rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %x_5]; [%y_6 ↦ %x_5]; [%x_5 ↦ ]]} - {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}] let%test _ = let r = of_eqs [(w, y); (y, z)] in @@ -189,21 +189,21 @@ let%test_module _ = pp_raw r3 ; [%expect {| - %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6) - ∧ (%z_7 × (%y_6 × %y_6)) = %t_1 + (%z_7 × (%y_6 × %y_6)) = %t_1 + ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6) {sat= true; - rep= [[%t_1 ↦ (%y_6^2 × %z_7)]; - [%u_2 ↦ %z_7]; - [%v_3 ↦ %z_7]; - [%w_4 ↦ %z_7]; - [%x_5 ↦ %z_7]; - [%y_6 ↦ ]; - [%z_7 ↦ ]; - [(%y_6 × %z_7) ↦ %z_7]; - [(%y_6^2 × %z_7) ↦ ]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [(%z_7 × %y_6^2) ↦ ]; + [(%z_7 × %y_6) ↦ %z_7]; + [%z_7 ↦ ]; + [%y_6 ↦ ]; + [%x_5 ↦ %z_7]; + [%w_4 ↦ %z_7]; + [%v_3 ↦ %z_7]; + [%u_2 ↦ %z_7]; + [%t_1 ↦ (%z_7 × %y_6^2)]]} |}] let%test _ = not (implies_eq r3 t z) (* incomplete *) let%test _ = implies_eq r3 x z @@ -216,15 +216,15 @@ let%test_module _ = pp_raw r4 ; [%expect {| - (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5 + (8 + %z_7) = %x_5 ∧ (3 + %z_7) = %w_4 ∧ (-4 + %z_7) = %y_6 {sat= true; - rep= [[%w_4 ↦ (%z_7 + 3)]; - [%x_5 ↦ (%z_7 + 8)]; - [%y_6 ↦ (%z_7 + -4)]; - [%z_7 ↦ ]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [%z_7 ↦ ]; + [%y_6 ↦ (-4 + %z_7)]; + [%x_5 ↦ (8 + %z_7)]; + [%w_4 ↦ (3 + %z_7)]]} |}] let%test _ = implies_eq r4 x (w + !5) let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5)) @@ -242,7 +242,7 @@ let%test_module _ = {| 1 = %x_5 = %y_6 - {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%y_6 ↦ 1]; [%x_5 ↦ 1]]} |}] let%test _ = implies_eq r6 x y @@ -255,25 +255,25 @@ let%test_module _ = pp (add_eq x z r7) ; [%expect {| - %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7 + %w_4 = %y_6 = %z_7 ∧ %v_3 = %x_5 {sat= true; - rep= [[%v_3 ↦ ]; - [%w_4 ↦ ]; - [%x_5 ↦ %v_3]; - [%y_6 ↦ %w_4]; - [%z_7 ↦ %w_4]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} + [%z_7 ↦ %w_4]; + [%y_6 ↦ %w_4]; + [%x_5 ↦ %v_3]; + [%w_4 ↦ ]; + [%v_3 ↦ ]]} {sat= true; - rep= [[%v_3 ↦ ]; - [%w_4 ↦ %v_3]; - [%x_5 ↦ %v_3]; - [%y_6 ↦ %v_3]; - [%z_7 ↦ %v_3]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} + [%z_7 ↦ %v_3]; + [%y_6 ↦ %v_3]; + [%x_5 ↦ %v_3]; + [%w_4 ↦ %v_3]; + [%v_3 ↦ ]]} %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}] @@ -299,13 +299,13 @@ let%test_module _ = %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]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [%z_7 ↦ %v_3]; + [%y_6 ↦ %v_3]; + [%x_5 ↦ %v_3]; + [%w_4 ↦ %v_3]; + [%v_3 ↦ ]]} |}] let%test _ = normalize r7' w |> Term.equal v @@ -322,10 +322,10 @@ let%test_module _ = pp_raw r8 ; [%expect {| - 14 = %y_6 ∧ (13 × %z_7) = %x_5 + (13 × %z_7) = %x_5 ∧ 14 = %y_6 {sat= true; - rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}] let%test _ = implies_eq r8 y !14 @@ -337,10 +337,10 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} {sat= true; - rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} |}] let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8)) @@ -356,10 +356,10 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} {sat= true; - rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]} (%z_7 - (%x_5 + 8)) @@ -395,7 +395,7 @@ let%test_module _ = let%expect_test _ = pp_raw r13 ; [%expect - {| {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]; [-1 ↦ ]; [0 ↦ ]]} |}] + {| {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ %y_6]; [%y_6 ↦ ]]} |}] let%test _ = not (is_unsat r13) (* incomplete *) @@ -406,7 +406,7 @@ let%test_module _ = pp_raw r14 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) @@ -418,12 +418,12 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%x_5 ↦ 1]; - [%y_6 ↦ ]; - [(%x_5 ≠ 0) ↦ -1]; - [(%y_6 ≠ 0) ↦ -1]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [(%y_6 ≠ 0) ↦ -1]; + [(%x_5 ≠ 0) ↦ -1]; + [%y_6 ↦ ]; + [%x_5 ↦ 1]]} |}] let%test _ = implies_eq r14 a (Formula.inject Formula.tt) let%test _ = implies_eq r14 b (Formula.inject Formula.tt) @@ -435,7 +435,7 @@ let%test_module _ = pp_raw r15 ; [%expect {| - {sat= true; rep= [[%x_5 ↦ 1]; [-1 ↦ ]; [0 ↦ ]]} |}] + {sat= true; rep= [[0 ↦ ]; [-1 ↦ ]; [%x_5 ↦ 1]]} |}] (* f(x−1)−1=x+1, f(y)+1=y−1, y+1=x ⊢ false *) let r16 = @@ -446,12 +446,12 @@ let%test_module _ = [%expect {| {sat= false; - rep= [[%x_5 ↦ (%y_6 + 1)]; - [%y_6 ↦ ]; - [%y_6^ ↦ (%y_6 + -2)]; - [(%x_5 + -1)^ ↦ (%y_6 + 3)]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [(-1 + %x_5)^ ↦ (3 + %y_6)]; + [%y_6^ ↦ (-2 + %y_6)]; + [%y_6 ↦ ]; + [%x_5 ↦ (1 + %y_6)]]} |}] let%test _ = is_unsat r16 @@ -463,12 +463,12 @@ let%test_module _ = [%expect {| {sat= false; - rep= [[%x_5 ↦ ]; - [%y_6 ↦ %x_5]; - [%x_5^ ↦ %x_5]; - [%y_6^ ↦ (%x_5 + -1)]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} |}] + [%y_6^ ↦ (-1 + %x_5)]; + [%x_5^ ↦ %x_5]; + [%y_6 ↦ %x_5]; + [%x_5 ↦ ]]} |}] let%test _ = is_unsat r17 @@ -479,14 +479,14 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%x_5 ↦ ]; - [%y_6 ↦ ]; - [%x_5^ ↦ %x_5]; - [%y_6^ ↦ (%y_6 + -1)]; + rep= [[0 ↦ ]; [-1 ↦ ]; - [0 ↦ ]]} + [%y_6^ ↦ (-1 + %y_6)]; + [%x_5^ ↦ %x_5]; + [%y_6 ↦ ]; + [%x_5 ↦ ]]} - %x_5 = %x_5^ ∧ (-1 + %y_6) = %y_6^ |}] + (-1 + %y_6) = %y_6^ ∧ %x_5 = %x_5^ |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] @@ -495,7 +495,7 @@ let%test_module _ = [%expect {| {sat= true; - rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}] + rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ 0]; [%y_6 ↦ 0]; [%x_5 ↦ 0]]} |}] let%test _ = implies_eq r19 z !0 diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index b70ce7e8c..392a51b48 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -145,7 +145,7 @@ let%test_module _ = pp q' ; [%expect {| - ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp + ∃ %x_6 . (-1 + %y_7) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp ((-1 + %y_7) = %y_7^) ∧ emp diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 26663f1ba..8c096db4e 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -143,7 +143,7 @@ let%test_module _ = {| ( infer_frame: %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩ - ) infer_frame: %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) infer_frame: (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ %a_2 = _ ∧ emp |}] let%expect_test _ = check_frame @@ -159,7 +159,7 @@ let%test_module _ = \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ ) infer_frame: - %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}] let%expect_test _ = check_frame @@ -175,7 +175,7 @@ let%test_module _ = \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩ ) infer_frame: - %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ 16 = %m_8 ∧ %a_2 = _ ∧ emp |}] let%expect_test _ = check_frame @@ -194,9 +194,9 @@ let%test_module _ = %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ ) infer_frame: ∃ %a0_10, %a1_11 . - %a_2 = %a0_10 + (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 ∧ 16 = %m_8 = %n_9 - ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 + ∧ %a_2 = %a0_10 ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] let%expect_test _ = @@ -216,9 +216,9 @@ let%test_module _ = %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩ ) infer_frame: ∃ %a0_10, %a1_11 . - %a_2 = %a0_10 + (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 ∧ 16 = %m_8 = %n_9 - ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 + ∧ %a_2 = %a0_10 ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] let seg_split_symbolically = @@ -246,19 +246,19 @@ let%test_module _ = \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: - ( ( %a_1 = %a_2 + ( ( 16 = %m_8 ∧ 2 = %n_9 - ∧ 16 = %m_8 + ∧ %a_1 = %a_2 ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) - ∨ ( %a_3 = _ - ∧ 1 = %n_9 + ∨ ( (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ 16 = %m_8 - ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 + ∧ 1 = %n_9 + ∧ %a_3 = _ ∧ emp) - ∨ ( %a_3 = _ - ∧ 0 = %n_9 + ∨ ( (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ 16 = %m_8 - ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 + ∧ 0 = %n_9 + ∧ %a_3 = _ ∧ emp) ) |}] diff --git a/sledge/src/test/term_test.ml b/sledge/src/test/term_test.ml index 532a1e588..5d7b659fc 100644 --- a/sledge/src/test/term_test.ml +++ b/sledge/src/test/term_test.ml @@ -54,7 +54,7 @@ let%test_module _ = let%expect_test _ = pp (z + !42 + !13) ; - [%expect {| (%z_2 + 55) |}] + [%expect {| (55 + %z_2) |}] let%expect_test _ = pp (z + !42 + !(-42)) ; @@ -62,15 +62,15 @@ let%test_module _ = let%expect_test _ = pp (z * y) ; - [%expect {| (%y_1 × %z_2) |}] + [%expect {| (%z_2 × %y_1) |}] let%expect_test _ = pp (y * z * y) ; - [%expect {| (%y_1^2 × %z_2) |}] + [%expect {| (%z_2 × %y_1^2) |}] let%expect_test _ = pp ((!2 * z * z) + (!3 * z) + !4) ; - [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}] + [%expect {| (4 + 2 × (%z_2^2) + 3 × %z_2) |}] let%expect_test _ = pp @@ -85,9 +85,8 @@ let%test_module _ = + (!9 * z * z * z) ) ; [%expect {| - (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2) - + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3) - + 1) |}] + (1 + 9 × (%z_2^3) + 4 × (%z_2^2) + 7 × (%z_2 × %y_1^2) + 5 × (%y_1^2) + + 8 × (%z_2^2 × %y_1) + 6 × (%z_2 × %y_1) + 2 × %z_2 + 3 × %y_1) |}] let%expect_test _ = pp (!0 * z * y) ; @@ -95,19 +94,19 @@ let%test_module _ = let%expect_test _ = pp (!1 * z * y) ; - [%expect {| (%y_1 × %z_2) |}] + [%expect {| (%z_2 × %y_1) |}] let%expect_test _ = pp (!7 * z * (!2 * y)) ; - [%expect {| (14 × (%y_1 × %z_2)) |}] + [%expect {| (14 × (%z_2 × %y_1)) |}] let%expect_test _ = pp (!13 + (!42 * z)) ; - [%expect {| (42 × %z_2 + 13) |}] + [%expect {| (13 + 42 × %z_2) |}] let%expect_test _ = pp ((!13 * z) + !42) ; - [%expect {| (13 × %z_2 + 42) |}] + [%expect {| (42 + 13 × %z_2) |}] let%expect_test _ = pp ((!2 * z) - !3 + ((!(-2) * z) + !3)) ; @@ -115,31 +114,31 @@ let%test_module _ = let%expect_test _ = pp ((!3 * y) + (!13 * z) + !42) ; - [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}] + [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}] let%expect_test _ = pp ((!13 * z) + !42 + (!3 * y)) ; - [%expect {| (3 × %y_1 + 13 × %z_2 + 42) |}] + [%expect {| (42 + 13 × %z_2 + 3 × %y_1) |}] let%expect_test _ = pp ((!13 * z) + !42 + (!3 * y) + (!2 * z)) ; - [%expect {| (3 × %y_1 + 15 × %z_2 + 42) |}] + [%expect {| (42 + 15 × %z_2 + 3 × %y_1) |}] let%expect_test _ = pp ((!13 * z) + !42 + (!3 * y) + (!(-13) * z)) ; - [%expect {| (3 × %y_1 + 42) |}] + [%expect {| (42 + 3 × %y_1) |}] let%expect_test _ = pp (z + !42 + ((!3 * y) + (!(-1) * z))) ; - [%expect {| (3 × %y_1 + 42) |}] + [%expect {| (42 + 3 × %y_1) |}] let%expect_test _ = pp (!(-1) * (z + (!(-1) * y))) ; - [%expect {| (%y_1 + -1 × %z_2) |}] + [%expect {| (-1 × %z_2 + %y_1) |}] let%expect_test _ = pp (((!3 * y) + !2) * (!4 + (!5 * z))) ; - [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}] + [%expect {| (8 + 15 × (%z_2 × %y_1) + 10 × %z_2 + 12 × %y_1) |}] let%expect_test _ = pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ; @@ -147,7 +146,7 @@ let%test_module _ = let%expect_test _ = pp ((!13 * z) + !42 - ((!3 * y) + (!13 * z))) ; - [%expect {| (-3 × %y_1 + 42) |}] + [%expect {| (42 + -3 × %y_1) |}] let%expect_test _ = pp (z = y) ; @@ -183,47 +182,47 @@ let%test_module _ = let%expect_test _ = pp (y - (!(-3) * y) + !4) ; - [%expect {| (4 × %y_1 + 4) |}] + [%expect {| (4 + 4 × %y_1) |}] let%expect_test _ = pp ((!(-3) * y) + !4 - y) ; - [%expect {| (-4 × %y_1 + 4) |}] + [%expect {| (4 + -4 × %y_1) |}] let%expect_test _ = pp (y = (!(-3) * y) + !4) ; - [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] + [%expect {| (%y_1 = (4 + -3 × %y_1)) |}] let%expect_test _ = pp ((!(-3) * y) + !4 = y) ; - [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}] + [%expect {| (%y_1 = (4 + -3 × %y_1)) |}] let%expect_test _ = pp (sub true_ (z = !4)) ; - [%expect {| (-1 × (%z_2 = 4) + -1) |}] + [%expect {| (-1 + -1 × (%z_2 = 4)) |}] let%expect_test _ = pp (add true_ (z = !4) = (z = !4)) ; - [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}] + [%expect {| ((%z_2 = 4) = (-1 + (%z_2 = 4))) |}] let%expect_test _ = pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ; - [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}] + [%expect {| ((13 × %z_2 + 3 × %y_1) = (42 + 13 × %z_2)) |}] let%expect_test _ = pp ((!13 * z) + !(-42) = (!3 * y) + (!13 * z)) ; - [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}] + [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}] let%expect_test _ = pp ((!13 * z) + !42 = (!(-3) * y) + (!13 * z)) ; - [%expect {| ((-3 × %y_1 + 13 × %z_2) = (13 × %z_2 + 42)) |}] + [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 13 × %z_2)) |}] let%expect_test _ = pp ((!10 * z) + !42 = (!(-3) * y) + (!13 * z)) ; - [%expect {| ((-3 × %y_1 + 13 × %z_2) = (10 × %z_2 + 42)) |}] + [%expect {| ((13 × %z_2 + -3 × %y_1) = (42 + 10 × %z_2)) |}] let%expect_test _ = pp ~~((!13 * z) + !(-42) != (!3 * y) + (!13 * z)) ; - [%expect {| ((3 × %y_1 + 13 × %z_2) = (13 × %z_2 + -42)) |}] + [%expect {| ((13 × %z_2 + 3 × %y_1) = (-42 + 13 × %z_2)) |}] let%expect_test _ = pp ~~(!2 < y && z <= !3) ; @@ -252,7 +251,7 @@ let%test_module _ = pp (z1_2 * z1_2) ; [%expect {| - (2 × %z_2 + (%z_2^2) + 1) + (1 + (%z_2^2) + 2 × %z_2) - (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}] + (1 + (%z_2^4) + 4 × (%z_2^3) + 6 × (%z_2^2) + 4 × %z_2) |}] end )