From b45b190d053108c5cc59204f72a743d7ecdc18d4 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 8 Feb 2021 13:11:59 -0800 Subject: [PATCH] [sledge] Compare Vars by id Summary: And make name optional. Reviewed By: jvillard Differential Revision: D26250538 fbshipit-source-id: 5de8a62c1 --- sledge/src/fol/trm.ml | 18 +--- sledge/src/fol/var0.ml | 2 +- sledge/src/fol/var_intf.ml | 6 +- sledge/src/test/context_test.ml | 171 -------------------------------- 4 files changed, 7 insertions(+), 190 deletions(-) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 56e9e26f9..69cbf7d91 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -106,7 +106,7 @@ and Trm : sig val vars : t -> Var.t iter end = struct type t = - | Var of {id: int; name: string} + | Var of {id: int; name: string [@ignore]} | Z of Z.t | Q of Q.t | Arith of Arith.t @@ -117,22 +117,6 @@ end = struct | Apply of Funsym.t * t array [@@deriving compare, equal, sexp] - let compare x y = - if x == y then 0 - else - match (x, y) with - | Var {id= i; name= s}, Var {id= j; name= t} -> - if i < 0 && j < 0 then String.compare s t else Int.compare i j - | _ -> compare x y - - let equal x y = - x == y - || - match (x, y) with - | Var {id= i; name= s}, Var {id= j; name= t} -> - if i < 0 && j < 0 then String.equal s t else Int.equal i j - | _ -> equal x y - (* nul-terminated string value represented by a concatenation *) let string_of_concat xs = let exception Not_a_string in diff --git a/sledge/src/fol/var0.ml b/sledge/src/fol/var0.ml index e89977f5f..7674464ce 100644 --- a/sledge/src/fol/var0.ml +++ b/sledge/src/fol/var0.ml @@ -55,7 +55,7 @@ module Make (T : REPR) = struct let x' = make ~id:(max + 1) ~name in (x', Set.add x' wrt) - let program ~name ~id = + let program ?(name = "") ~id = assert (id > 0) ; make ~id:(-id) ~name diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml index bc6c087c5..5680aed54 100644 --- a/sledge/src/fol/var_intf.ml +++ b/sledge/src/fol/var_intf.ml @@ -39,7 +39,11 @@ module type VAR = sig val id : t -> int val name : t -> string - val program : name:string -> id:int -> t + + val program : ?name:string -> id:int -> t + (** Create a program variable with [id] and optional [name]. The [id] + uniquely identifies the variable, and must be positive. *) + val fresh : string -> wrt:Set.t -> t * Set.t val identified : name:string -> id:int -> t diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index 38ced39c6..695cd3942 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -109,177 +109,6 @@ let%test_module _ = (Sized (seq (Var (id 2) (name b))) (siz (Z 4)))))))|} ; [%expect {| |}] - let%expect_test _ = - replay - {|(Union - ((Var (id 1) (name a)) (Var (id 2) (name a)) (Var (id 3) (name a)) - (Var (id 6) (name l)) (Var (id 7) (name a1))) - ((xs ()) (sat true) - (rep - (((Var (id 7) (name a1)) (Var (id 2) (name a))) - ((Var (id 2) (name a)) (Var (id 2) (name a))))) - (cls (((Var (id 2) (name a)) ((Var (id 7) (name a1)))))) (use ()) - (pnd ())) - ((xs ()) (sat true) - (rep - (((Var (id 7) (name a1)) (Var (id 7) (name a1))) - ((Var (id 3) (name a)) - (Concat - ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) - (Sized (seq (Var (id 7) (name a1))) (siz (Z 8)))))) - ((Var (id 1) (name a)) (Var (id 1) (name a))))) - (cls - (((Concat - ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) - (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))) - ((Var (id 3) (name a)))))) - (use - (((Var (id 7) (name a1)) - ((Concat - ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) - (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))))) - ((Var (id 1) (name a)) - ((Concat - ((Sized (seq (Var (id 1) (name a))) (siz (Z 8))) - (Sized (seq (Var (id 7) (name a1))) (siz (Z 8))))))))) - (pnd ())))|} ; - [%expect {| |}] - - let%expect_test _ = - replay - {|(Union - ((Var (id 0) (name 1)) (Var (id 0) (name 4)) (Var (id 0) (name 6)) - (Var (id 0) (name 8)) (Var (id 0) (name freturn)) - (Var (id 1) (name freturn))) - ((xs ()) (sat true) - (rep - (((Apply (Signed 8) ((Var (id 0) (name 8)))) - (Var (id 0) (name freturn))) - ((Var (id 0) (name freturn)) (Var (id 0) (name freturn))) - ((Var (id 0) (name 8)) (Var (id 0) (name 8))))) - (cls - (((Var (id 0) (name freturn)) - ((Apply (Signed 8) ((Var (id 0) (name 8)))))))) - (use - (((Var (id 0) (name 8)) ((Apply (Signed 8) ((Var (id 0) (name 8)))))))) - (pnd ())) - ((xs ()) (sat true) - (rep - (((Apply (Uninterp .str) ()) (Var (id 0) (name 6))) - ((Var (id 0) (name 8)) (Z 73)) - ((Var (id 0) (name 6)) (Var (id 0) (name 6))))) - (cls - (((Z 73) ((Var (id 0) (name 8)))) - ((Var (id 0) (name 6)) ((Apply (Uninterp .str) ()))))) - (use ()) (pnd ())))|} ; - [%expect {||}] - - let%expect_test _ = - replay - {|(Apply_and_elim - ((Var (id 0) (name 12)) (Var (id 0) (name 16)) (Var (id 0) (name 19)) - (Var (id 0) (name 22)) (Var (id 0) (name 23)) (Var (id 0) (name 26)) - (Var (id 0) (name 29)) (Var (id 0) (name 33)) (Var (id 0) (name 35)) - (Var (id 0) (name 39)) (Var (id 0) (name 4)) (Var (id 0) (name 40)) - (Var (id 0) (name 41)) (Var (id 0) (name 47)) (Var (id 0) (name 5)) - (Var (id 0) (name 52)) (Var (id 0) (name 8)) (Var (id 1) (name m)) - (Var (id 2) (name a)) (Var (id 6) (name b))) - ((Var (id 1) (name m)) (Var (id 2) (name a)) (Var (id 6) (name b))) - (((Var (id 6) (name b)) (Var (id 2) (name a))) - ((Var (id 1) (name m)) - (Apply (Signed 32) - ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) - ((xs ()) (sat true) - (rep - (((Apply (Signed 32) - ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))) - (Var (id 1) (name m))) - ((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))) - (Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4)))))) - ((Apply (Signed 32) ((Var (id 0) (name 5)))) - (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) - ((Var (id 6) (name b)) (Var (id 2) (name a))) - ((Var (id 2) (name a)) (Var (id 2) (name a))) - ((Var (id 1) (name m)) (Var (id 1) (name m))) - ((Var (id 0) (name 8)) - (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) - ((Var (id 0) (name 52)) (Var (id 0) (name 26))) - ((Var (id 0) (name 5)) (Var (id 0) (name 5))) - ((Var (id 0) (name 35)) (Var (id 0) (name 23))) - ((Var (id 0) (name 33)) (Z 0)) - ((Var (id 0) (name 26)) (Var (id 0) (name 26))) - ((Var (id 0) (name 23)) (Var (id 0) (name 23))) - ((Var (id 0) (name 22)) (Var (id 0) (name 22))) - ((Var (id 0) (name 19)) - (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))) - ((Var (id 0) (name 16)) - (Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1)))))) - (cls - (((Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1))) - ((Var (id 0) (name 16)) (Var (id 0) (name 8)) - (Var (id 0) (name 19)) - (Apply (Signed 32) ((Var (id 0) (name 5)))))) - ((Z 0) ((Var (id 0) (name 33)))) - ((Var (id 2) (name a)) ((Var (id 6) (name b)))) - ((Var (id 1) (name m)) - ((Apply (Signed 32) - ((Apply (Signed 32) - ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) - ((Var (id 0) (name 26)) ((Var (id 0) (name 52)))) - ((Var (id 0) (name 23)) ((Var (id 0) (name 35)))))) - (use - (((Apply (Signed 32) ((Arith (((((Var (id 0) (name 23)) 1)) 4))))) - ((Apply (Signed 32) - ((Apply (Signed 32) - ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) - ((Var (id 0) (name 5)) - ((Apply (Signed 32) ((Var (id 0) (name 5)))))) - ((Var (id 0) (name 23)) - ((Arith ((() -1) ((((Var (id 0) (name 23)) 1)) 1))) - (Apply (Signed 32) - ((Arith (((((Var (id 0) (name 23)) 1)) 4))))))))) - (pnd ())))|} ; - [%expect {| |}] - - let%expect_test _ = - replay - {|(Add () (Eq (Var (id 2) (name u)) (Var (id 5) (name x))) - ((xs ()) (sat true) - (rep - (((Apply (Uninterp g) ((Var (id 6) (name y)) (Var (id 7) (name z)))) - (Var (id 3) (name v))) - ((Apply (Uninterp g) ((Var (id 6) (name y)) (Var (id 3) (name v)))) - (Var (id 1) (name t))) - ((Var (id 7) (name z)) (Var (id 7) (name z))) - ((Var (id 6) (name y)) (Var (id 6) (name y))) - ((Var (id 5) (name x)) (Var (id 3) (name v))) - ((Var (id 4) (name w)) (Var (id 3) (name v))) - ((Var (id 3) (name v)) (Var (id 3) (name v))) - ((Var (id 1) (name t)) (Var (id 1) (name t))))) - (cls - (((Var (id 3) (name v)) - ((Var (id 5) (name x)) - (Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 7) (name z)))) - (Var (id 4) (name w)))) - ((Var (id 1) (name t)) - ((Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 3) (name v)))))))) - (use - (((Var (id 7) (name z)) - ((Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 7) (name z)))))) - ((Var (id 6) (name y)) - ((Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 3) (name v)))) - (Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 7) (name z)))))) - ((Var (id 3) (name v)) - ((Apply (Uninterp g) - ((Var (id 6) (name y)) (Var (id 3) (name v)))))))) - (pnd ())))|} ; - [%expect {| |}] - (* let%expect_test _ = * replay * {||} ;