From 2c46e2b8d4895e18dcbf194e8b13d088ec1895b9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:36:13 -0800 Subject: [PATCH] [sledge] Prepare Context.extend for addition of use lists Summary: This diff changes Context.extend to not only add terms and their subterms to the carrier, but to simultaneously normalize the added term. The normalized form is currently ignored, but it will be needed when adding use lists. Reviewed By: jvillard Differential Revision: D25883709 fbshipit-source-id: bfe06f2a8 --- sledge/nonstdlib/map.ml | 13 +++++++ sledge/nonstdlib/map_intf.ml | 4 +++ sledge/src/fol/context.ml | 64 +++++++++++++++++---------------- sledge/src/test/context_test.ml | 30 ++++++++++++++++ 4 files changed, 80 insertions(+), 31 deletions(-) diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml index c52d8c3ee..0ff64b2f5 100644 --- a/sledge/nonstdlib/map.ml +++ b/sledge/nonstdlib/map.ml @@ -169,6 +169,19 @@ end) : S with type key = Key.t = struct in Option.map ~f:(fun v -> (v, m)) !found + let find_or_add k v m = + let found = ref None in + let m = + M.update k + (function + | None -> Some v + | v -> + found := v ; + v ) + m + in + match !found with Some v -> `Found v | None -> `Added m + let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove k m)) let pop_min_binding m = diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml index 4f7a4efbf..fc146c73e 100644 --- a/sledge/nonstdlib/map_intf.ml +++ b/sledge/nonstdlib/map_intf.ml @@ -88,6 +88,10 @@ module type S = sig val find_and_remove : key -> 'a t -> ('a * 'a t) option (** Find and remove the binding for a key. *) + val find_or_add : key -> 'a -> 'a t -> [`Added of 'a t | `Found of 'a] + (** Find the value bound to the given key if there is one, or otherwise + add a binding for the given key and value. *) + 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)]. *) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index fa2d79ad4..9d3d87ebf 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -31,7 +31,6 @@ module Subst : sig val for_alli : t -> f:(key:Trm.t -> data:Trm.t -> bool) -> bool val to_iter : t -> (Trm.t * Trm.t) iter val to_list : t -> (Trm.t * Trm.t) list - val extend : Trm.t -> t -> t option val compose1 : key:Trm.t -> data:Trm.t -> t -> t val compose : t -> t -> t val map_entries : f:(Trm.t -> Trm.t) -> t -> t @@ -105,17 +104,6 @@ end = struct let r' = Trm.Map.map_endo ~f:(norm s) r in Trm.Map.add ~key ~data r' ) - (** add an identity entry if the term is not already present *) - let extend e s = - let exception Found in - match - Trm.Map.update e s ~f:(function - | Some _ -> raise_notrace Found - | None -> e ) - with - | exception Found -> None - | s -> Some s - (** map over a subst, applying [f] to both domain and range, requires that [f] is injective and for any set of terms [E], [f\[E\]] is disjoint from [E] *) @@ -405,23 +393,34 @@ let invariant r = (* Extending the carrier ==================================================*) -let rec extend_ a s = +let rec norm_extend_ a x = [%trace] - ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a Subst.pp s) - ~retn:(fun {pf} s' -> pf "%a" Subst.pp_diff (s, s')) + ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x) + ~retn:(fun {pf} (a', x') -> + pf "%a@ %a" Trm.pp a' pp_diff (x, x') ; + assert (Trm.equal a' (Subst.norm x'.rep a)) ) @@ fun () -> - match Theory.classify a with - | InterpAtom -> s - | InterpApp -> Iter.fold ~f:extend_ (Trm.trms a) s - | NonInterpAtom -> - (* add uninterpreted terms if missing *) - Trm.Map.change a s ~f:(function None -> Some a | a' -> a') - | UninterpApp -> ( - (* add uninterpreted terms if missing *) - match Subst.extend a s with - | None -> s - (* and their subterms if newly added *) - | Some s -> Iter.fold ~f:extend_ (Trm.trms a) s ) + if Theory.is_noninterpreted a then + (* add noninterpreted terms *) + match Trm.Map.find_or_add a a x.rep with + | `Found a' -> (a', x) + | `Added rep -> + (* and their subterms if newly added *) + let x = {x with rep} in + let a', x = Trm.fold_map ~f:norm_extend_ a x in + (a', x) + else + (* add subterms of interpreted terms *) + Trm.fold_map ~f:norm_extend_ a x + +let norm_extend a x = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x) + ~retn:(fun {pf} (a', x') -> + pf "%a@ %a" Trm.pp a' pp_diff (x, x') ; + pre_invariant x' ; + assert (Trm.equal a' (Subst.norm x'.rep a)) ) + @@ fun () -> norm_extend_ a x (** add a term to the carrier *) let extend a x = @@ -430,9 +429,7 @@ let extend a 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} + @@ fun () -> snd (norm_extend a x) (* Propagation ============================================================*) @@ -614,7 +611,12 @@ let implies r b = [%Trace.retn fun {pf} -> pf "%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 normalize x a = + [%trace] + ~call:(fun {pf} -> pf "@ %a@ %a" Term.pp a pp x) + ~retn:(fun {pf} -> pf "%a" Term.pp) + @@ fun () -> Term.map_trms ~f:(canon x) a let cls_of r e = let e' = Subst.apply r.rep e in diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index 2ec16e59d..17b2acbe0 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -113,4 +113,34 @@ let%test_module _ = (Var (id 0) (name 2)))))) (pnd ())))|} ; [%expect {| |}] + + let%expect_test _ = + replay + {|(Dnf + (Eq0 + (Arith + (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1) + ((((Var (id 11) (name a)) 1)) -1)))))|} ; + [%expect {| |}] + + let%expect_test _ = + replay + {|(Normalize + ((xs ()) (sat true) + (rep + (((Var (id 7) (name 16)) (Z 8)) ((Var (id 0) (name 8)) (Q 3/2)) + ((Var (id 0) (name 17)) (Z 3)) ((Var (id 0) (name 12)) (Z 8)) + ((Var (id 0) (name 11)) (Z 8)) + ((Var (id 0) (name 10)) (Var (id 0) (name 10))) + ((Var (id 0) (name 1)) (Z 3)) ((Var (id 0) (name 0)) (Z 8)))) + (cls + (((Q 3/2) ((Var (id 0) (name 8)))) + ((Z 8) + ((Var (id 0) (name 12)) (Var (id 0) (name 0)) + (Var (id 7) (name 16)) (Var (id 0) (name 11)))) + ((Z 3) ((Var (id 0) (name 17)) (Var (id 0) (name 1)))))) + (pnd ())) + (Trm + (Arith (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1)))))|} ; + [%expect {| |}] end )