[Logic] Rewrite identifier implementation + more tests

src/logics/Identifier.ml

@@ -2,16 +2,16 @@
  *
  * Author: Tomas Dacik (idacik@fit.vut.cz), 2024 *)
 
-let debug = ref false
+let do_debug = ref false
+let debug = Format.kasprintf (fun msg -> if !do_debug then Format.printf "%s%!" msg)
 
 type t = Int.t * String.t
 (** Identifier is represented by integer tag used for comparison and name used for printing. *)
 
 let compare (tag1, _) (tag2, _) = Int.compare tag1 tag2
-let equal (tag1, _) (tag2, _) = Int.equal tag1 tag2
-let show (tag, name) =
-  if !debug then Format.sprintf "%d:%s" tag name
-  else name
+let equal id1 id2 = compare id1 id2 = 0
+let show (tag, name) = name
+let show_debug (tag, name) = Format.sprintf "%d:%s" tag name
 let tag (id, _) = id
 let pp fmt (_, name) = Format.fprintf fmt "%s" name
 
@@ -28,44 +28,66 @@ include Datatype.Collections(Self)
 
 (** Identifier managment *)
 
-module HT = struct
+module HT = Hashtbl.Make(String)
 
-  include Hashtbl.Make(String)
+module Make () = struct
+  let counter = ref 0
 
-  let find_tag table name = fst @@ find table name
+  let tag_table = ref (HT.create 97)
+  let index_table = ref (HT.create 97)
 
-  let find_index table name = snd @@ find table name
+  let add_tag = HT.add !tag_table
+  let update_index = HT.replace !index_table
 
-end
-
-module Make () = struct
+  let find_tag = HT.find !tag_table
+  let find_index = HT.find !index_table
 
-  let counter = ref 0
-  let hash_table = ref (HT.create 97)
+  let debug_repr () =
+    let debug name n acc = Format.asprintf "%s\n  %s -> %d" acc name n in
+    let t1 = HT.fold debug !tag_table "Tag table" in
+    let t2 = HT.fold debug !index_table "Index table" in
+    t1 ^ "\n" ^ t2
 
   type nonrec t = t
 
-  let next_id () =
-    counter := !counter + 1;
-    !counter
+  let next_id () = incr counter; !counter
 
   let mk name =
-    let tag, index =
-      try HT.find !hash_table name
-      with Not_found -> next_id (), 0
+    debug "Creating identifier %s\n" name;
+    let res =
+      try (find_tag name, name)
+      with Not_found ->
+        let tag = next_id () in
+        add_tag name tag;
+        (tag, name)
     in
-    HT.add !hash_table name (tag, index);
-    (tag, name)
+    debug "%s\n" (debug_repr ());
+    res
 
   let mk_fresh name =
-    let tag, index =
-      try HT.find !hash_table name
-      with Not_found -> next_id (), 0
+    debug "Creating fresh identifier %s\n" name;
+    let base_name = match String.split_on_char '!' name with
+      | [s] -> s
+      | [s; _] -> s
+      | _ -> assert false
+    in
+    let index =
+      try find_index base_name + 1
+      with Not_found -> 1
     in
-    HT.add !hash_table name (tag, index + 1);
-    (next_id (), Format.asprintf "%s!%d" name index)
+
+    let fresh_name = Format.asprintf "%s!%d" base_name index in
+    assert (not @@ HT.mem !tag_table fresh_name);
+
+    let tag = next_id () in
+    add_tag fresh_name tag;
+    update_index base_name index;
+
+    debug "%s\n" (debug_repr ());
+    (tag, fresh_name)
 
   let show = show
+  let show_debug = show_debug
   let tag = tag
   let compare = compare
   let equal = equal

src/logics/Logic_sig.mli

@@ -58,8 +58,12 @@ module type VARIABLE = sig
 
   val describe : t -> string * Sort.t
 
+  val of_description : string * Sort.t -> t
+
   val show : t -> string
 
+  val show_debug : t -> string
+
   val equal : t -> t -> bool
 
   val compare : t -> t -> int

src/logics/Variable.ml

@@ -16,6 +16,8 @@ module Make () = struct
   module ID = Identifier.Make()
   module Sort = Sort
 
+  let debug = ID.debug_repr
+
   type nonrec t = t
 
   let hash (id, _) = ID.tag id
@@ -24,8 +26,6 @@ module Make () = struct
 
   let get_sort = snd
 
-  let describe (name, sort) = (ID.show name, sort)
-
   let has_sort sort var = Sort.equal sort @@ get_sort var
 
   let equal (name1, sort1) (name2, sort2) = ID.equal name1 name2
@@ -36,10 +36,16 @@ module Make () = struct
 
   let mk_fresh name sort = (ID.mk_fresh @@ escape name, sort)
 
+  let describe (name, sort) = (ID.show name, sort)
+
+  let of_description (name, sort) = mk name sort
+
   let refresh (name, sort) = mk_fresh (ID.show name) sort
 
   let show var = get_name var
 
+  let show_debug (name, _) = ID.show_debug @@ name
+
   let show_with_sort var = Format.asprintf "%s : %s" (show var) (Sort.show @@ get_sort var)
 
   let nil = mk "nil" Sort.loc_nil

src/logics/Variable.mli

@@ -5,6 +5,13 @@ module Make ( ) : sig
   include VARIABLE with module Sort = Sort
                     and type t = Identifier.t * Sort.t
 
+
+(** TODO: why is this necessary? *)
+
+  val debug : unit -> string
+
+  val show_debug : t -> string
+
   val nil : t
 
   val is_nil : t -> bool

tests/Variable_tests.ml

@@ -1,41 +1,69 @@
 module MakeVar () = struct
-  include Variable.Make ()
-
-  let mk name = mk name Sort.Int
-  let mk_fresh name = mk_fresh name Sort.Int
+  module Var = struct
+    include Variable.Make ()
+    let mk name = mk name Sort.int
+    let mk_fresh name = mk_fresh name Sort.int
+    let show = show_debug
+  end
+  include Var
+  include Builder.Make(Var)
 end
 
 let mk_test1 () =
   let module Var = MakeVar () in
   let x = Var.mk "x" in
   let y = Var.mk "y" in
-  assert (not @@ Var.equal x y)
+  Var.check_distinct x y
 
 let mk_test2 () =
   let module Var = MakeVar () in
   let x1 = Var.mk "x" in
   let x2 = Var.mk "x" in
-  assert (Var.equal x1 x2)
+  Var.check_equal x1 x2
 
 let mk_fresh_test1 () =
   let module Var = MakeVar () in
   let x = Var.mk "x" in
   let x' = Var.mk_fresh "x" in
-  assert (not @@ Var.equal x x')
+  Var.check_distinct x x'
 
 let mk_fresh_test2 () =
   let module Var = MakeVar () in
   let x1 = Var.mk_fresh "x" in
   let x2 = Var.mk_fresh "x" in
-  assert (not @@ Var.equal x1 x2)
+  Var.check_distinct x1 x2
 
 let mk_fresh_test3 () =
   let module Var = MakeVar () in
   let x1 = Var.mk "x" in
   let _  = Var.mk_fresh "x" in
   let x2 = Var.mk "x" in
-  assert (Var.equal x1 x2)
+  Var.check_equal x1 x2
+
+let mk_fresh_test4 () =
+  let module Var = MakeVar () in
+  let x1 = Var.mk_fresh "x" in (* name x!1 *)
+  let x2 = Var.of_description @@ Var.describe x1 in
+  Var.check_equal ~msg:(Var.debug()) x1 x2
 
+let refresh_test1 () =
+  let module Var = MakeVar () in
+  let x1 = Var.mk "x" in
+  let x2 = Var.refresh x1 in
+  Var.check_distinct x1 x2
+
+let refresh_test2 () =
+  let module Var = MakeVar () in
+  let x1 = Var.mk_fresh "x" in
+  let x2 = Var.refresh x1 in
+  Var.check_distinct x1 x2
+
+let refresh_test3 () =
+  let module Var = MakeVar () in
+  let x = Var.mk_fresh "x" in
+  let x1 = Var.refresh x in
+  let x2 = Var.refresh x in
+  Var.check_distinct x1 x2
 
 let () =
   run "Variables" [
@@ -47,5 +75,11 @@ let () =
       test_case "mk_fresh(x) != mk(x)" `Quick mk_fresh_test1;
       test_case "mk_fresh(x) != mk_fresh(x)" `Quick mk_fresh_test2;
       test_case "Fresh/used sequence" `Quick mk_fresh_test3;
+      test_case "Reusing fresh variable" `Quick mk_fresh_test4;
+    ];
+    "refresh", [
+      test_case "mk(x) != refresh(x)" `Quick refresh_test1;
+      test_case "mk_fresh(x) != refresh(x)" `Quick refresh_test2;
+      test_case "refresh(x) != refresh(x)" `Quick refresh_test3;
     ];
   ]

tests/testables/Builder.ml

@@ -15,8 +15,13 @@ module Make (T : TESTABLE_BASE) = struct
     let pp fmt x = Format.fprintf fmt "%s" (T.show x)
   end
 
-  let check_equal actual expected =
-    Alcotest.check' (module T' : TESTABLE with type t = t) ~msg:"" ~actual ~expected
+  let check_equal ?msg actual expected =
+    let msg = Option.value msg ~default:"" in
+    Alcotest.check' (module T' : TESTABLE with type t = t) ~msg ~actual ~expected
+
+  let check_distinct lhs rhs =
+    let msg = Format.asprintf "Objects %s and %s are equal (expected to be distinct)" (T.show lhs) (T.show rhs) in
+    Alcotest.check' Alcotest.bool ~msg ~actual:(T.equal lhs rhs) ~expected:false
 
   let check_apply ~input ~expected fn =
     let msg = Format.asprintf "Input: %s" (T.show input) in

tests/testables/Testable_sig.mli

@@ -8,7 +8,9 @@ module type TESTABLE_FULL = sig
   type t
   val check_apply : input:t -> expected:t -> (t -> t) -> unit
 
-  val check_equal : t -> t -> unit
+  val check_equal : ?msg:string -> t -> t -> unit
+  val check_distinct : t -> t -> unit
+
   val check : (t -> bool) -> t -> unit
   val check2 : (t -> t -> bool) -> t -> t -> unit
   val check_list : (t list -> bool) -> t list -> unit