[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

@@ -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 =

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)]. *)

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

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 )