pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Compare Vars by id

Browse Source 
Summary: And make name optional.

Reviewed By: jvillard

Differential Revision: D26250538

fbshipit-source-id: 5de8a62c1
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent eef9019442
commit b45b190d05
4 changed files with 7 additions and 190 deletions
Show Stats Download Patch File Download Diff File

18
sledge/src/fol/trm.ml
Unescape View File

@ -106,7 +106,7 @@ and Trm : sig
val vars : t -> Var.t iter val vars : t -> Var.t iter
end = struct end = struct
type t = type t =
| Var of {id: int; name: string} | Var of {id: int; name: string [@ignore]}
| Z of Z.t | Z of Z.t
| Q of Q.t | Q of Q.t
| Arith of Arith.t | Arith of Arith.t
@ -117,22 +117,6 @@ end = struct
| Apply of Funsym.t * t array | Apply of Funsym.t * t array
[@@deriving compare, equal, sexp] [@@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 *) (* nul-terminated string value represented by a concatenation *)
let string_of_concat xs = let string_of_concat xs =
let exception Not_a_string in let exception Not_a_string in

2
sledge/src/fol/var0.ml
Unescape View File

@ -55,7 +55,7 @@ module Make (T : REPR) = struct
let x' = make ~id:(max + 1) ~name in let x' = make ~id:(max + 1) ~name in
(x', Set.add x' wrt) (x', Set.add x' wrt)
let program ~name ~id = let program ?(name = "") ~id =
assert (id > 0) ; assert (id > 0) ;
make ~id:(-id) ~name make ~id:(-id) ~name

6
sledge/src/fol/var_intf.ml
Unescape View File

@ -39,7 +39,11 @@ module type VAR = sig
val id : t -> int val id : t -> int
val name : t -> string 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 fresh : string -> wrt:Set.t -> t * Set.t
val identified : name:string -> id:int -> t val identified : name:string -> id:int -> t

171
sledge/src/test/context_test.ml
Unescape View File

@ -109,177 +109,6 @@ let%test_module _ =
(Sized (seq (Var (id 2) (name b))) (siz (Z 4)))))))|} ; (Sized (seq (Var (id 2) (name b))) (siz (Z 4)))))))|} ;
[%expect {| |}] [%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 _ = (* let%expect_test _ =
* replay * replay
* {||} ; * {||} ;

Write Preview
Loading…
Cancel
Save