[Array] Added functors for Hashtbl and Id_dom creation

colibri2/core/colibri2_core.ml

@@ -106,16 +106,25 @@ module Dom = struct
    restricted to a singleton return the corresponding value *)
   end
 
-  module Make (L : Lattice) : sig
-    include S with type t = L.t
+  module type LS = sig
+    type t
 
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val set_dom : Egraph.wt -> Node.t -> t -> unit
     (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
 
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val upd_dom : Egraph.wt -> Node.t -> t -> unit
     (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
         [l] with the current value of the domain. *)
-  end = struct
+  end
+
+  module type DS = sig
+    type t
+
+    include S with type t := t
+    include LS with type t := t
+  end
+
+  module Make (L : Lattice) : DS with type t = L.t = struct
     type t = L.t
 
     let pp = L.pp
@@ -169,14 +178,7 @@ module Dom = struct
 
   (** [Lattice(L)] register a domain as a lattice. It returns useful function
      for setting and updating the domain *)
-  module Lattice (L : Lattice) : sig
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
-
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
-        [l] with the current value of the domain. *)
-  end = struct
+  module Lattice (L : Lattice) : LS with type t = L.t = struct
     module S = Make (L)
 
     let () = register (module S)

colibri2/core/colibri2_core.mli

@@ -566,29 +566,29 @@ and Dom : sig
         restricted to a singleton return the corresponding value *)
   end
 
-  module Make (L : Lattice) : sig
-    include S with type t = L.t
+  module type LS = sig
+    type t
 
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val set_dom : Egraph.wt -> Node.t -> t -> unit
     (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
 
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
+    val upd_dom : Egraph.wt -> Node.t -> t -> unit
     (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
         [l] with the current value of the domain. *)
   end
 
+  module type DS = sig
+    include S
+    include LS with type t := t
+  end
+
+  module Make (L : Lattice) : DS with type t = L.t
+
   val register : (module S) -> unit
 
   (** [Lattice(L)] register a domain as a lattice. It returns useful function
      for setting and updating the domain *)
-  module Lattice (L : Lattice) : sig
-    val set_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [set_dom d n l] Set the domain of [n] with [l] and set its value if it is a singleton *)
-
-    val upd_dom : Egraph.wt -> Node.t -> L.t -> unit
-    (** [upd_dom d n l] Same than {!set_dom} but set with the intersection of
-        [l] with the current value of the domain. *)
-  end
+  module Lattice (L : Lattice) : LS with type t := L.t
 end
 
 module Expr = Expr

colibri2/tests/solve/smt_array/sat/dune

@@ -18,6 +18,14 @@
     "array-res-ext array-res-aup"
     --options
     "array-diff-graph"
+    --options
+    "array-choice"
+    --options
+    "array-res-ext array-choice"
+    --options
+    "array-res-ext array-res-aup array-choice"
+    --options
+    "array-diff-graph array-choice"
     ;--options
     ;"array-diff-graph array-res-ext"
     ;--options

colibri2/tests/solve/smt_array/sat/dune.inc

@@ -34,3 +34,39 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+--dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))

colibri2/tests/solve/smt_array/unsat/dune

@@ -18,6 +18,14 @@
     "array-res-ext array-res-aup"
     --options
     "array-diff-graph"
+    --options
+    "array-choice"
+    --options
+    "array-res-ext array-choice"
+    --options
+    "array-res-ext array-res-aup array-choice"
+    --options
+    "array-diff-graph array-choice"
     ;--options
     ;"array-diff-graph array-res-ext"
     ;--options

colibri2/theories/array/DiffGraph.ml

@@ -25,38 +25,20 @@ open Popop_stdlib
 open Common
 module HT = Datastructure.Hashtbl (DInt)
 
-module NHT = struct
-  let nodes = HT.create Node.pp "diffgraph_nodes"
-  let set = HT.set nodes
-  let find = HT.find nodes
-  let find_opt = HT.find_opt nodes
-  let change ~f = HT.change f nodes
-  let remove = HT.remove nodes
-end
+module NHT = MkIHT (struct
+  type t = Node.t
 
-let pp_nid env fmt i =
-  match NHT.find_opt env i with
-  | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
-  | None -> Format.fprintf fmt "Not_found{id = %d}" i
-
-let s_remove_opt s_opt v =
-  match s_opt with
-  | Some s ->
-      let ns = DInt.S.remove v s in
-      if DInt.S.is_empty ns then None else Some ns
-  | None -> raise Not_found
+  let pp = Node.pp
+  let name = "diffgraph_nodes"
+end)
 
 module DG = struct
-  let diff_graph =
-    HT.create
-      (fun fmt (m, (_ : Node.t DInt.M.t)) -> Node.M.pp DInt.S.pp fmt m)
-      "diff_graph_db"
+  include MkIHT (struct
+    type t = DInt.S.t Node.M.t * Node.t DInt.M.t
 
-  let set = HT.set diff_graph
-  let find = HT.find diff_graph
-  let find_opt = HT.find_opt diff_graph
-  let change ~f = HT.change f diff_graph
-  let remove = HT.remove diff_graph
+    let pp fmt (m, (_ : Node.t DInt.M.t)) = Node.M.pp DInt.S.pp fmt m
+    let name = "diffgraph_nodes"
+  end)
 
   let diffgraph_opt =
     Debug.register_flag ~desc:"Print the entire DiffGraph into a dot file"
@@ -120,10 +102,7 @@ module DG = struct
                  mnp (DInt.M.remove nid m)
         | exception Not_found -> ()
       in
-      aux
-        (HT.fold
-           (fun id (_, m) acc -> DInt.M.add id m acc)
-           diff_graph env DInt.M.empty)
+      aux (fold (fun id (_, m) acc -> DInt.M.add id m acc) env DInt.M.empty)
     in
     fun env ?msg () ->
       if Debug.test_flag diffgraph_opt then (
@@ -138,85 +117,32 @@ module DG = struct
 end
 
 module Id_dom = struct
-  module IVal = struct
-    module T = struct
-      type t = DInt.t [@@deriving eq, ord, hash, show]
-    end
-
-    include T
-    include MkDatatype (T)
-
-    let name = "Array.id.value"
-  end
-
-  let merge_hooks = Datastructure.Push.create Fmt.nop "Array.Id_dom.merge_hooks"
-
-  let register_merge_hook env
-      (f : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) =
-    Datastructure.Push.push merge_hooks env f
-
-  module D = struct
-    include Dom.Make (struct
-      module Value = Value.Register (IVal)
-
-      type t = IVal.t [@@deriving eq, show]
-
-      let is_singleton _ _ = None
-
-      let key =
-        Dom.Kind.create
-          (module struct
-            type nonrec t = t
-
-            let name = "Array.id"
-          end)
-
-      let inter _ v _ = Some v
-    end)
-
-    let merge env (d1, n1) (d2, n2) b =
-      (match (d1, n1, d2, n2) with
-      | Some id1, n1, Some id2, n2 ->
-          Datastructure.Push.iter merge_hooks env ~f:(fun f ->
-              f env (n1, id1) (n2, id2) b)
-          (* id1 always stays, b allows to determine which one will become the
-             representative *)
-      | _ ->
-          (* Ideally, should be unreachable, but it is with the test
-             "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)
-          ());
-
-      merge env (d1, n1) (d2, n2) b
-  end
+  include MkIdDom (struct
+    let n1 = "Array.Id.value"
+    let n2 = "Array.Id_dom.merge_hooks"
+    let n3 = "Array.id"
+  end)
+
+  let new_id_hook env id n b =
+    if b then (
+      DG.set env id (Node.M.empty, DInt.M.empty);
+      NHT.set env id n)
+
+  let set_id env n = set_id ~new_id_hook env n
+  let get_id env n = get_id ~new_id_hook env n
+end
 
-  let () = Dom.register (module D)
+let pp_nid env fmt i =
+  match NHT.find_opt env i with
+  | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
+  | None -> Format.fprintf fmt "Not_found{id = %d}" i
 
-  let set_id, get_id =
-    let id_counter = ref 0 in
-    let set_id env n =
-      match Egraph.get_dom env D.key n with
-      | None ->
-          incr id_counter;
-          Debug.dprintf3 Common.debug "set_id of %a: none -> %d" Node.pp n
-            !id_counter;
-          D.set_dom env n !id_counter;
-          DG.set env !id_counter (Node.M.empty, DInt.M.empty);
-          NHT.set env !id_counter n
-      | Some id -> Debug.dprintf3 Common.debug "set_id of %a: %d" Node.pp n id
-    in
-    let get_id env n =
-      (* is this a good idea?
-         TODO: Find out why it crashes occasionally with
-         restricted extensionality *)
-      match Egraph.get_dom env D.key n with
-      | Some id -> id
-      | None ->
-          Debug.dprintf2 Common.debug "get_id of %a: No idea found!" Node.pp n;
-          set_id env n;
-          !id_counter
-    in
-    (set_id, get_id)
-end
+let s_remove_opt s_opt v =
+  match s_opt with
+  | Some s ->
+      let ns = DInt.S.remove v s in
+      if DInt.S.is_empty ns then None else Some ns
+  | None -> raise Not_found
 
 let are_linked env id1 id2 =
   let rec aux (seen : DInt.S.t) (m : Node.t DInt.M.t) =

colibri2/theories/array/common.ml

@@ -22,6 +22,7 @@
 open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
+module HT = Datastructure.Hashtbl (DInt)
 
 let restrict_ext =
   Options.register ~pp:Fmt.bool "Array.res-ext"
@@ -336,3 +337,104 @@ let mk_array_const env v val_gty =
 let distinct_arrays_term a b =
   let diff = Builtin.apply_array_diff a b in
   Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
+
+module MkIHT (V : sig
+  type t
+
+  val pp : t Pp.pp
+  val name : string
+end) =
+struct
+  let db = HT.create V.pp V.name
+  let set (env : Egraph.wt) = HT.set db env
+  let find (env : Egraph.wt) = HT.find db env
+  let find_opt (env : Egraph.wt) = HT.find_opt db env
+  let change ~f (env : Egraph.wt) = HT.change f db env
+  let remove (env : Egraph.wt) = HT.remove db env
+  let iter = HT.iter db
+  let fold f env acc = HT.fold f db env acc
+end
+
+module MkIdDom (N : sig
+  val n1 : string
+  val n2 : string
+  val n3 : string
+end) =
+struct
+  module IVal = struct
+    module T = struct
+      type t = DInt.t [@@deriving eq, ord, hash, show]
+    end
+
+    include T
+    include MkDatatype (T)
+
+    let name = N.n1
+  end
+
+  let merge_hooks = Datastructure.Push.create Fmt.nop N.n2
+
+  let register_merge_hook env (f : Egraph.wt -> 'a -> 'a -> bool -> unit) =
+    Datastructure.Push.push merge_hooks env f
+
+  module D = struct
+    include Dom.Make (struct
+      module Value = Value.Register (IVal)
+
+      type t = IVal.t [@@deriving eq, show]
+
+      let is_singleton _ _ = None
+
+      let key =
+        Dom.Kind.create
+          (module struct
+            type nonrec t = t
+
+            let name = N.n3
+          end)
+
+      let inter _ v _ = Some v
+    end)
+
+    let merge env (d1, n1) (d2, n2) b =
+      (match (d1, n1, d2, n2) with
+      | Some id1, n1, Some id2, n2 ->
+          Datastructure.Push.iter merge_hooks env ~f:(fun f ->
+              f env (n1, id1) (n2, id2) b)
+          (* id1 always stays, b allows to determine which one will become the
+             representative *)
+      | _ ->
+          (* Ideally, should be unreachable, but it is with the test
+             "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)
+          ());
+      merge env (d1, n1) (d2, n2) b
+  end
+
+  let () = Dom.register (module D)
+
+  let set_id, get_id =
+    let id_counter = ref 0 in
+    let set_id ?(new_id_hook = fun _ _ _ _ -> ()) env n =
+      match Egraph.get_dom env D.key n with
+      | None ->
+          incr id_counter;
+          Debug.dprintf3 debug "set_id of %a: none -> %d" Node.pp n !id_counter;
+          D.set_dom env n !id_counter;
+          new_id_hook env !id_counter n true
+      | Some id ->
+          Debug.dprintf3 debug "set_id of %a: %d" Node.pp n id;
+          new_id_hook env id n false
+    in
+    let get_id ?(new_id_hook = fun _ _ _ _ -> ()) env n =
+      (* is this a good idea?
+         TODO: Find out why it crashes occasionally with
+         restricted extensionality *)
+      match Egraph.get_dom env D.key n with
+      | Some id -> id
+      | None ->
+          Debug.dprintf2 debug "get_id of %a: No idea found!" Node.pp n;
+          set_id ~new_id_hook env n;
+          !id_counter
+    in
+    (set_id, get_id)
+end

colibri2/theories/array/common.mli

@@ -133,3 +133,43 @@ val mk_distinct_arrays :
 
 val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
 val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
+
+module MkIHT (V : sig
+  type t
+
+  val pp : t Colibri2_popop_lib.Pp.pp
+  val name : string
+end) : sig
+  val set : Egraph.wt -> int -> V.t -> unit
+  val find : Egraph.wt -> int -> V.t
+  val find_opt : Egraph.wt -> int -> V.t option
+  val change : f:(V.t option -> V.t option) -> Egraph.wt -> int -> unit
+  val remove : Egraph.wt -> int -> unit
+  val iter : f:(int -> V.t -> unit) -> Egraph.wt -> unit
+  val fold : (int -> V.t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
+end
+
+module MkIdDom (_ : sig
+  val n1 : string
+  val n2 : string
+  val n3 : string
+end) : sig
+  val register_merge_hook :
+    Egraph.wt ->
+    (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
+    unit
+
+  module D : Dom.DS with type t = int
+
+  val set_id :
+    ?new_id_hook:(Egraph.wt -> int -> Node.t -> bool -> unit) ->
+    Egraph.wt ->
+    Node.t ->
+    unit
+
+  val get_id :
+    ?new_id_hook:(Egraph.wt -> int -> Node.t -> bool -> unit) ->
+    Egraph.wt ->
+    Node.t ->
+    int
+end