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

[sledge] Refactor: Distinguish Fol term and formula types

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D22170516

fbshipit-source-id: e593123ce
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 0998ce011f
commit 0568f2ee2d
10 changed files with 223 additions and 181 deletions
Show Stats Download Patch File Download Diff File

6
sledge/src/domain_sh.ml
Unescape View File

@ -38,7 +38,7 @@ let is_false = Sh.is_false
let dnf = Sh.dnf let dnf = Sh.dnf
let exec_assume q b = let exec_assume q b =
Exec.assume q (Term.of_exp b) |> Option.map ~f:simplify Exec.assume q (Formula.of_exp b) |> Option.map ~f:simplify
let exec_kill q r = Exec.kill q (Var.of_reg r) |> simplify let exec_kill q r = Exec.kill q (Var.of_reg r) |> simplify
@ -122,7 +122,7 @@ let garbage_collect (q : t) ~wrt =
let and_eqs sub formals actuals q = let and_eqs sub formals actuals q =
let and_eq q formal actual = let and_eq q formal actual =
let actual' = Term.rename sub actual in let actual' = Term.rename sub actual in
Sh.and_ (Term.eq (Term.var formal) actual') q Sh.and_ (Formula.eq (Term.var formal) actual') q
in in
List.fold2_exn ~f:and_eq formals actuals ~init:q List.fold2_exn ~f:and_eq formals actuals ~init:q
@ -277,7 +277,7 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
Var.Set.fold formals ~init:q ~f:(fun q var -> Var.Set.fold formals ~init:q ~f:(fun q var ->
let var = Term.var var in let var = Term.var var in
let renamed_var = Term.rename subst var in let renamed_var = Term.rename subst var in
Sh.and_ (Term.eq renamed_var var) q ) Sh.and_ (Formula.eq renamed_var var) q )
in in
(* Add back the original formals name *) (* Add back the original formals name *)
let post = Sh.rename subst post in let post = Sh.rename subst post in

85
sledge/src/exec.ml
Unescape View File

@ -87,12 +87,11 @@ let gen_spec us specm =
* Instruction small axioms * Instruction small axioms
*) *)
let null_eq ptr = Sh.pure (Term.eq Term.zero ptr) let null_eq ptr = Sh.pure (Formula.eq Term.zero ptr)
let eq_concat (siz, seq) ms = let eq_concat (siz, seq) ms =
Term.( Formula.eq (Term.sized ~siz ~seq)
eq (sized ~siz ~seq) (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
(concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
open Fresh.Import open Fresh.Import
@ -110,7 +109,7 @@ let move_spec reg_exps =
let+ sub, ms = Fresh.assign ~ws ~rs in let+ sub, ms = Fresh.assign ~ws ~rs in
let post = let post =
IArray.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) -> IArray.fold reg_exps ~init:Sh.emp ~f:(fun post (reg, exp) ->
Sh.and_ (Term.eq (Term.var reg) (Term.rename sub exp)) post ) Sh.and_ (Formula.eq (Term.var reg) (Term.rename sub exp)) post )
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -124,7 +123,7 @@ let load_spec reg ptr len =
let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let post = let post =
Sh.and_ Sh.and_
(Term.eq (Term.var reg) (Term.rename sub seg.seq)) (Formula.eq (Term.var reg) (Term.rename sub seg.seq))
(Sh.rename sub foot) (Sh.rename sub foot)
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -157,7 +156,8 @@ let memcpy_eq_spec dst src len =
let+ seg = Fresh.seg dst ~len in let+ seg = Fresh.seg dst ~len in
let dst_heap = Sh.seg seg in let dst_heap = Sh.seg seg in
let foot = let foot =
Sh.and_ (Term.eq dst src) (Sh.and_ (Term.eq len Term.zero) dst_heap) Sh.and_ (Formula.eq dst src)
(Sh.and_ (Formula.eq len Term.zero) dst_heap)
in in
let post = dst_heap in let post = dst_heap in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -187,7 +187,7 @@ let memcpy_specs dst src len =
let memmov_eq_spec dst src len = let memmov_eq_spec dst src len =
let+ dst_seg = Fresh.seg dst ~len in let+ dst_seg = Fresh.seg dst ~len in
let dst_heap = Sh.seg dst_seg in let dst_heap = Sh.seg dst_seg in
let foot = Sh.and_ (Term.eq dst src) dst_heap in let foot = Sh.and_ (Formula.eq dst src) dst_heap in
let post = dst_heap in let post = dst_heap in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -221,8 +221,8 @@ let memmov_foot dst src len =
in in
let foot = let foot =
Sh.and_ eq_mem_dst_mid_src Sh.and_ eq_mem_dst_mid_src
(Sh.and_ (Term.lt dst src) (Sh.and_ (Formula.lt dst src)
(Sh.and_ (Term.lt src (Term.add dst len)) seg)) (Sh.and_ (Formula.lt src (Term.add dst len)) seg))
in in
(bas, siz, mem_dst, mem_mid, mem_src, foot) (bas, siz, mem_dst, mem_mid, mem_src, foot)
@ -336,7 +336,7 @@ let malloc_spec reg siz =
* { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ } * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ }
*) *)
let mallocx_spec reg siz = let mallocx_spec reg siz =
let foot = Sh.pure (Term.dq siz Term.zero) in let foot = Sh.pure (Formula.dq siz Term.zero) in
let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
@ -381,9 +381,9 @@ let posix_memalign_spec reg ptr siz =
let enomem = Term.integer (Z.of_int 12) in let enomem = Term.integer (Z.of_int 12) in
let post = let post =
Sh.or_ Sh.or_
(Sh.and_ (Term.eq (Term.var reg) enomem) (Sh.rename sub foot)) (Sh.and_ (Formula.eq (Term.var reg) enomem) (Sh.rename sub foot))
(Sh.and_ (Sh.and_
(Term.eq (Term.var reg) eok) (Formula.eq (Term.var reg) eok)
(Sh.rename sub (Sh.star (Sh.seg pseg') (Sh.seg qseg)))) (Sh.rename sub (Sh.star (Sh.seg pseg') (Sh.seg qseg))))
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -410,12 +410,11 @@ let realloc_spec reg ptr siz =
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.or_ Sh.or_
(Sh.and_ Term.(eq loc zero) (Sh.rename sub foot)) (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub foot))
(Sh.and_ (Sh.and_
Term.( (Formula.conditional ~cnd:(Formula.le len siz)
conditional ~cnd:(le len siz) ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
(Sh.seg rseg)) (Sh.seg rseg))
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -430,7 +429,7 @@ let rallocx_spec reg ptr siz =
let* len = Fresh.var "m" in let* len = Fresh.var "m" in
let* pseg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in let* pseg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
let pheap = Sh.seg pseg in let pheap = Sh.seg pseg in
let foot = Sh.and_ (Term.dq siz Term.zero) pheap in let foot = Sh.and_ (Formula.dq siz Term.zero) pheap in
let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
@ -440,12 +439,11 @@ let rallocx_spec reg ptr siz =
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.or_ Sh.or_
(Sh.and_ Term.(eq loc zero) (Sh.rename sub pheap)) (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub pheap))
(Sh.and_ (Sh.and_
Term.( (Formula.conditional ~cnd:(Formula.le len siz)
conditional ~cnd:(le len siz) ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|]))
(Sh.seg rseg)) (Sh.seg rseg))
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -458,7 +456,7 @@ let rallocx_spec reg ptr siz =
let xallocx_spec reg ptr siz ext = let xallocx_spec reg ptr siz ext =
let* len = Fresh.var "m" in let* len = Fresh.var "m" in
let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
let foot = Sh.and_ (Term.dq siz Term.zero) (Sh.seg seg) in let foot = Sh.and_ (Formula.dq siz Term.zero) (Sh.seg seg) in
let* sub, ms = let* sub, ms =
Fresh.assign ~ws:(Var.Set.of_ reg) Fresh.assign ~ws:(Var.Set.of_ reg)
~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext))) ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
@ -473,12 +471,12 @@ let xallocx_spec reg ptr siz ext =
let+ a2 = Fresh.var "a" in let+ a2 = Fresh.var "a" in
let post = let post =
Sh.and_ Sh.and_
Term.( (Formula.and_
and_ (Formula.conditional ~cnd:(Formula.le len siz)
(conditional ~cnd:(le len siz) ~thn:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
~thn:(eq_concat (siz, a1) [|(len, a0); (sub siz len, a2)|]) ~els:(eq_concat (len, a0) [|(siz, a1); (Term.sub len siz, a2)|]))
~els:(eq_concat (len, a0) [|(siz, a1); (sub len siz, a2)|])) (Formula.and_ (Formula.le siz reg)
(and_ (le siz reg) (le reg (add siz ext)))) (Formula.le reg (Term.add siz ext))))
(Sh.seg seg') (Sh.seg seg')
in in
{foot; sub; ms; post} {foot; sub; ms; post}
@ -492,7 +490,7 @@ let sallocx_spec reg ptr =
let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let post = Sh.and_ (Term.eq (Term.var reg) len) (Sh.rename sub foot) in let post = Sh.and_ (Formula.eq (Term.var reg) len) (Sh.rename sub foot) in
{foot; sub; ms; post} {foot; sub; ms; post}
(* { p-[p;m)->⟨m,α⟩ } (* { p-[p;m)->⟨m,α⟩ }
@ -504,7 +502,7 @@ let malloc_usable_size_spec reg ptr =
let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
let foot = Sh.seg seg in let foot = Sh.seg seg in
let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let post = Sh.and_ (Term.le len (Term.var reg)) (Sh.rename sub foot) in let post = Sh.and_ (Formula.le len (Term.var reg)) (Sh.rename sub foot) in
{foot; sub; ms; post} {foot; sub; ms; post}
(* { s≠0 } (* { s≠0 }
@ -512,11 +510,11 @@ let malloc_usable_size_spec reg ptr =
* { r=0 ∨ r=sΘ } * { r=0 ∨ r=sΘ }
*) *)
let nallocx_spec reg siz = let nallocx_spec reg siz =
let foot = Sh.pure (Term.dq siz Term.zero) in let foot = Sh.pure (Formula.dq siz Term.zero) in
let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
let loc = Term.var reg in let loc = Term.var reg in
let siz = Term.rename sub siz in let siz = Term.rename sub siz in
let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in let post = Sh.or_ (null_eq loc) (Sh.pure (Formula.eq loc siz)) in
{foot; sub; ms; post} {foot; sub; ms; post}
let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz)) let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
@ -530,9 +528,9 @@ let mallctl_read_spec r i w n =
let* rseg = Fresh.seg r ~siz:iseg.seq in let* rseg = Fresh.seg r ~siz:iseg.seq in
let+ a = Fresh.var "a" in let+ a = Fresh.var "a" in
let foot = let foot =
Sh.and_ Sh.and_ (Formula.eq w Term.zero)
Term.(eq w zero) (Sh.and_ (Formula.eq n Term.zero)
(Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg))) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
in in
let rseg' = {rseg with seq= a} in let rseg' = {rseg with seq= a} in
let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
@ -552,9 +550,8 @@ let mallctlbymib_read_spec p l r i w n =
let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
let+ a = Fresh.var "a" in let+ a = Fresh.var "a" in
let foot = let foot =
Sh.and_ Sh.and_ (Formula.eq w Term.zero)
Term.(eq w zero) (Sh.and_ (Formula.eq n Term.zero) (Sh.star const (Sh.seg rseg)))
(Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
in in
let rseg' = {rseg with seq= a} in let rseg' = {rseg with seq= a} in
let post = Sh.star (Sh.seg rseg') const in let post = Sh.star (Sh.seg rseg') const in
@ -568,7 +565,7 @@ let mallctl_write_spec r i w n =
let+ seg = Fresh.seg w ~siz:n in let+ seg = Fresh.seg w ~siz:n in
let post = Sh.seg seg in let post = Sh.seg seg in
let foot = let foot =
Sh.and_ (Term.eq r Term.zero) (Sh.and_ (Term.eq i Term.zero) post) Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
in in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -583,7 +580,7 @@ let mallctlbymib_write_spec p l r i w n =
let+ wseg = Fresh.seg w ~siz:n in let+ wseg = Fresh.seg w ~siz:n in
let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
let foot = let foot =
Sh.and_ (Term.eq r Term.zero) (Sh.and_ (Term.eq i Term.zero) post) Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
in in
{foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@ -630,7 +627,7 @@ let strlen_spec reg ptr =
let ret = Term.sub (Term.sub (Term.add b m) p) Term.one in let ret = Term.sub (Term.sub (Term.add b m) p) Term.one in
let post = let post =
Sh.and_ Sh.and_
(Term.eq (Term.var reg) (Term.rename sub ret)) (Formula.eq (Term.var reg) (Term.rename sub ret))
(Sh.rename sub foot) (Sh.rename sub foot)
in in
{foot; sub; ms; post} {foot; sub; ms; post}

2
sledge/src/exec.mli
Unescape View File

@ -9,7 +9,7 @@
open Fol open Fol
val assume : Sh.t -> Term.t -> Sh.t option val assume : Sh.t -> Formula.t -> Sh.t option
val kill : Sh.t -> Var.t -> Sh.t val kill : Sh.t -> Var.t -> Sh.t
val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option

27
sledge/src/fol.ml
Unescape View File

@ -10,10 +10,29 @@ module Var = Ses.Term.Var
module Term = struct module Term = struct
include Ses.Term include Ses.Term
type term = t
type formula = t
let ite = conditional let ite = conditional
end end
module Context = Ses.Equality module Formula = struct
include Ses.Term
let inject b = b
let project e = Some e
let of_exp e =
let b = Term.of_exp e in
match project b with Some p -> p | None -> dq Term.zero b
end
module Context = struct
include Ses.Equality
let and_formula = and_term
let normalizef = normalize
module Subst = struct
include Subst
let substf = subst
end
end

128
sledge/src/fol.mli
Unescape View File

@ -56,90 +56,110 @@ module Var : sig
end end
(** Terms *) (** Terms *)
module Term : sig module rec Term : sig
type term type t [@@deriving compare, equal, sexp]
type formula = term
val ppx : Var.strength -> term pp (* pretty-printing *)
val pp : term pp val ppx : Var.strength -> t pp
val pp : t pp
module Map : Map.S with type key := term module Map : Map.S with type key := t
(** Construct *) (** Construct *)
(** terms *)
(* variables *) (* variables *)
val var : Var.t -> term val var : Var.t -> t
(* constants *) (* constants *)
val zero : term val zero : t
val one : term val one : t
val integer : Z.t -> term val integer : Z.t -> t
val rational : Q.t -> term val rational : Q.t -> t
(* arithmetic *) (* arithmetic *)
val neg : term -> term val neg : t -> t
val add : term -> term -> term val add : t -> t -> t
val sub : term -> term -> term val sub : t -> t -> t
val mulq : Q.t -> term -> term val mulq : Q.t -> t -> t
val mul : term -> term -> term val mul : t -> t -> t
(* sequences *) (* sequences *)
val splat : term -> term val splat : t -> t
val sized : seq:term -> siz:term -> term val sized : seq:t -> siz:t -> t
val extract : seq:term -> off:term -> len:term -> term val extract : seq:t -> off:t -> len:t -> t
val concat : term array -> term val concat : t array -> t
(* if-then-else *) (* if-then-else *)
val ite : cnd:formula -> thn:term -> els:term -> term val ite : cnd:Formula.t -> thn:t -> els:t -> t
(** formulas *)
(* constants *)
val true_ : formula
val false_ : formula
(* comparisons *)
val eq : term -> term -> formula
val dq : term -> term -> formula
val lt : term -> term -> formula
val le : term -> term -> formula
(* connectives *)
val not_ : formula -> formula
val and_ : formula -> formula -> formula
val or_ : formula -> formula -> formula
val conditional : cnd:formula -> thn:formula -> els:formula -> formula
(** Convert *) (** Convert *)
val of_exp : Llair.Exp.t -> term val of_exp : Llair.Exp.t -> t
(** Destruct *) (** Destruct *)
val d_int : term -> Z.t option val d_int : t -> Z.t option
(** Access *) (** Access *)
val const_of : term -> Q.t option val const_of : t -> Q.t option
(** Transform *) (** Transform *)
val disjuncts : term -> term list val rename : Var.Subst.t -> t -> t
val rename : Var.Subst.t -> term -> term
(** Traverse *) (** Traverse *)
val fold_vars : term -> init:'a -> f:('a -> Var.t -> 'a) -> 'a val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
(** Query *) (** Query *)
val is_true : formula -> bool val fv : t -> Var.Set.t
val is_false : formula -> bool end
val fv : term -> Var.Set.t
(** Formulas *)
and Formula : sig
type t [@@deriving compare, equal, sexp]
val inject : t -> Term.t
val project : Term.t -> t option
(* pretty-printing *)
val ppx : Var.strength -> t pp
val pp : t pp
(** Construct *)
(* constants *)
val true_ : t
val false_ : t
(* comparisons *)
val eq : Term.t -> Term.t -> t
val dq : Term.t -> Term.t -> t
val lt : Term.t -> Term.t -> t
val le : Term.t -> Term.t -> t
(* connectives *)
val not_ : t -> t
val and_ : t -> t -> t
val or_ : t -> t -> t
val conditional : cnd:t -> thn:t -> els:t -> t
(** Convert *)
val of_exp : Llair.Exp.t -> t
type t = term [@@deriving compare, equal, sexp] (** Transform *)
val rename : Var.Subst.t -> t -> t
val disjuncts : t -> t list
(** Query *)
val is_true : t -> bool
val is_false : t -> bool
val fv : t -> Var.Set.t
end end
(** Inference System *) (** Inference System *)
@ -164,7 +184,7 @@ module Context : sig
val true_ : t val true_ : t
(** The diagonal relation, which only equates each term with itself. *) (** The diagonal relation, which only equates each term with itself. *)
val and_term : Var.Set.t -> Term.t -> t -> Var.Set.t * t val and_formula : Var.Set.t -> Formula.t -> t -> Var.Set.t * t
(** Conjoin a (Boolean) term to a relation. *) (** Conjoin a (Boolean) term to a relation. *)
val and_ : Var.Set.t -> t -> t -> Var.Set.t * t val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
@ -197,6 +217,8 @@ module Context : sig
relation, where [e'] and its subterms are expressed in terms of the relation, where [e'] and its subterms are expressed in terms of the
relation's canonical representatives of each equivalence class. *) relation's canonical representatives of each equivalence class. *)
val normalizef : t -> Formula.t -> Formula.t
val difference : t -> Term.t -> Term.t -> Z.t option val difference : t -> Term.t -> Term.t -> Z.t option
(** The difference as an offset. [difference r a b = Some k] if [r] (** The difference as an offset. [difference r a b = Some k] if [r]
implies [a = b+k], or [None] if [a] and [b] are not equal up to an implies [a = b+k], or [None] if [a] and [b] are not equal up to an
@ -217,6 +239,8 @@ module Context : sig
val subst : t -> Term.t -> Term.t val subst : t -> Term.t -> Term.t
(** Apply a substitution recursively to subterms. *) (** Apply a substitution recursively to subterms. *)
val substf : t -> Formula.t -> Formula.t
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks (** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks
and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks and ν are maximal where ∃ks. ν is universally valid, xs ⊇ ks

65
sledge/src/sh.ml
Unescape View File

@ -18,7 +18,7 @@ type starjunction =
{ us: Var.Set.t { us: Var.Set.t
; xs: Var.Set.t ; xs: Var.Set.t
; ctx: Context.t ; ctx: Context.t
; pure: Term.t ; pure: Formula.t
; heap: seg list ; heap: seg list
; djns: disjunction list } ; djns: disjunction list }
[@@deriving compare, equal, sexp] [@@deriving compare, equal, sexp]
@ -33,7 +33,7 @@ let emp =
{ us= Var.Set.empty { us= Var.Set.empty
; xs= Var.Set.empty ; xs= Var.Set.empty
; ctx= Context.true_ ; ctx= Context.true_
; pure= Term.true_ ; pure= Formula.true_
; heap= [] ; heap= []
; djns= [] } ; djns= [] }
@ -56,9 +56,10 @@ let map_seg ~f h =
then h then h
else {loc; bas; len; siz; seq} else {loc; bas; len; siz; seq}
let map ~f_sjn ~f_ctx ~f_trm ({us; xs= _; ctx; pure; heap; djns} as q) = let map ~f_sjn ~f_ctx ~f_trm ~f_fml ({us; xs= _; ctx; pure; heap; djns} as q)
let pure = f_trm pure in =
if Term.is_false pure then false_ us let pure = f_fml pure in
if Formula.is_false pure then false_ us
else else
let ctx = f_ctx ctx in let ctx = f_ctx ctx in
let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in
@ -78,7 +79,7 @@ let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
~init ~f = ~init ~f =
List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init) List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
|> fun init -> |> fun init ->
Term.fold_vars ~f ~init pure Term.fold_vars ~f ~init (Formula.inject pure)
|> fun init -> |> fun init ->
if Option.is_some ignore_ctx then init if Option.is_some ignore_ctx then init
else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init) else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
@ -222,12 +223,12 @@ let rec pp_ ?var_strength vs parent_xs parent_ctx fs
let pure = let pure =
if Option.is_none var_strength then [pure] if Option.is_none var_strength then [pure]
else else
let pure' = Context.normalize ctx pure in let pure' = Context.normalizef ctx pure in
if Term.is_true pure' then [] else [pure'] if Formula.is_true pure' then [] else [pure']
in in
List.pp List.pp
~pre:(if first then "@[ " else "@ @[@<2>∧ ") ~pre:(if first then "@[ " else "@ @[@<2>∧ ")
"@ @<2>∧ " (Term.ppx x) fs pure ~suf:"@]" ; "@ @<2>∧ " (Formula.ppx x) fs pure ~suf:"@]" ;
let first = first && List.is_empty pure in let first = first && List.is_empty pure in
if List.is_empty heap then if List.is_empty heap then
Format.fprintf fs Format.fprintf fs
@ -275,11 +276,7 @@ let fv ?ignore_ctx q =
in in
fv_union Var.Set.empty q fv_union Var.Set.empty q
let invariant_pure b = let invariant_pure p = assert (not (Formula.is_false p))
match Term.d_int b with
| Some data -> assert (not (Z.is_false data))
| _ -> assert true
let invariant_seg _ = () let invariant_seg _ = ()
let rec invariant q = let rec invariant q =
@ -298,7 +295,7 @@ let rec invariant q =
( match djns with ( match djns with
| [[]] -> | [[]] ->
assert (Context.is_true ctx) ; assert (Context.is_true ctx) ;
assert (Term.is_true pure) ; assert (Formula.is_true pure) ;
assert (List.is_empty heap) assert (List.is_empty heap)
| _ -> assert (not (Context.is_false ctx)) ) ; | _ -> assert (not (Context.is_false ctx)) ) ;
invariant_pure pure ; invariant_pure pure ;
@ -318,7 +315,7 @@ let rec invariant q =
let rec apply_subst sub q = let rec apply_subst sub q =
map q ~f_sjn:(rename sub) map q ~f_sjn:(rename sub)
~f_ctx:(fun r -> Context.rename r sub) ~f_ctx:(fun r -> Context.rename r sub)
~f_trm:(Term.rename sub) ~f_trm:(Term.rename sub) ~f_fml:(Formula.rename sub)
|> check (fun q' -> |> check (fun q' ->
assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) ) assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
@ -456,11 +453,11 @@ let star q1 q2 =
| {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
false_ (Var.Set.union q1.us q2.us) false_ (Var.Set.union q1.us q2.us)
| {us= _; xs= _; ctx; pure; heap= []; djns= []}, _ | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
when Context.is_true ctx && Term.is_true pure -> when Context.is_true ctx && Formula.is_true pure ->
let us = Var.Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q2.us then q2 else {q2 with us} if us == q2.us then q2 else {q2 with us}
| _, {us= _; xs= _; ctx; pure; heap= []; djns= []} | _, {us= _; xs= _; ctx; pure; heap= []; djns= []}
when Context.is_true ctx && Term.is_true pure -> when Context.is_true ctx && Formula.is_true pure ->
let us = Var.Set.union q1.us q2.us in let us = Var.Set.union q1.us q2.us in
if us == q1.us then q1 else {q1 with us} if us == q1.us then q1 else {q1 with us}
| _ -> | _ ->
@ -479,7 +476,7 @@ let star q1 q2 =
{ us { us
; xs= Var.Set.union xs1 xs2 ; xs= Var.Set.union xs1 xs2
; ctx ; ctx
; pure= Term.and_ p1 p2 ; pure= Formula.and_ p1 p2
; heap= List.append h1 h2 ; heap= List.append h1 h2
; djns= List.append d1 d2 } ) ; djns= List.append d1 d2 } )
|> |>
@ -501,17 +498,17 @@ let or_ q1 q2 =
| _, {djns= [[]]; _} -> extend_us q2.us q1 | _, {djns= [[]]; _} -> extend_us q2.us q1
| ( ({djns= []; _} as q) | ( ({djns= []; _} as q)
, ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) ) , ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) )
when Var.Set.is_empty xs && Term.is_true pure -> when Var.Set.is_empty xs && Formula.is_true pure ->
{d with us= Var.Set.union q.us d.us; djns= [q :: djn]} {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
| ( ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) | ( ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d)
, ({djns= []; _} as q) ) , ({djns= []; _} as q) )
when Var.Set.is_empty xs && Term.is_true pure -> when Var.Set.is_empty xs && Formula.is_true pure ->
{d with us= Var.Set.union q.us d.us; djns= [q :: djn]} {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
| _ -> | _ ->
{ us= Var.Set.union q1.us q2.us { us= Var.Set.union q1.us q2.us
; xs= Var.Set.empty ; xs= Var.Set.empty
; ctx= Context.true_ ; ctx= Context.true_
; pure= Term.true_ ; pure= Formula.true_
; heap= [] ; heap= []
; djns= [[q1; q2]] } ) ; djns= [[q1; q2]] } )
|> |>
@ -525,14 +522,15 @@ let orN = function
| [q] -> q | [q] -> q
| q :: qs -> List.fold ~f:or_ ~init:q qs | q :: qs -> List.fold ~f:or_ ~init:q qs
let pure (e : Term.t) = let pure (p : Formula.t) =
[%Trace.call fun {pf} -> pf "%a" Term.pp e] [%Trace.call fun {pf} -> pf "%a" Formula.pp p]
; ;
List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b -> List.fold (Formula.disjuncts p) ~init:(false_ Var.Set.empty)
let us = Term.fv b in ~f:(fun q p ->
let xs, ctx = Context.(and_term us b true_) in let us = Formula.fv p in
let xs, ctx = Context.(and_formula us p true_) in
if Context.is_false ctx then false_ us if Context.is_false ctx then false_ us
else or_ q (exists_fresh xs {emp with us; ctx; pure= b}) ) else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) )
|> |>
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
pf "%a" pp q ; pf "%a" pp q ;
@ -544,7 +542,7 @@ let and_subst subst q =
[%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q] [%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q]
; ;
Context.Subst.fold Context.Subst.fold
~f:(fun ~key ~data -> and_ (Term.eq key data)) ~f:(fun ~key ~data -> and_ (Formula.eq key data))
subst ~init:q subst ~init:q
|> |>
[%Trace.retn fun {pf} q -> [%Trace.retn fun {pf} q ->
@ -555,10 +553,10 @@ let subst sub q =
[%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q] [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
; ;
let dom, eqs = let dom, eqs =
Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_) Var.Subst.fold sub ~init:(Var.Set.empty, Formula.true_)
~f:(fun var trm (dom, eqs) -> ~f:(fun var trm (dom, eqs) ->
( Var.Set.add dom var ( Var.Set.add dom var
, Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) ) , Formula.and_ (Formula.eq (Term.var var) (Term.var trm)) eqs ) )
in in
exists dom (and_ eqs q) exists dom (and_ eqs q)
|> |>
@ -585,13 +583,13 @@ let filter_heap ~f q =
(** Query *) (** Query *)
let is_emp = function let is_emp = function
| {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Term.is_true pure | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Formula.is_true pure
| _ -> false | _ -> false
let is_false = function let is_false = function
| {djns= [[]]; _} -> true | {djns= [[]]; _} -> true
| {ctx; pure; heap; _} -> | {ctx; pure; heap; _} ->
Term.is_false (Context.normalize ctx pure) Formula.is_false (Context.normalizef ctx pure)
|| List.exists heap ~f:(fun seg -> || List.exists heap ~f:(fun seg ->
Context.entails_eq ctx seg.loc Term.zero ) Context.entails_eq ctx seg.loc Term.zero )
@ -647,6 +645,7 @@ let rec norm_ s q =
; ;
let q = let q =
map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s) map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s)
~f_fml:(Context.Subst.substf s)
in in
let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in
exists_fresh xs {q with ctx} exists_fresh xs {q with ctx}

8
sledge/src/sh.mli
Unescape View File

@ -19,7 +19,7 @@ type starjunction = private
; xs: Var.Set.t (** existentially-bound variables *) ; xs: Var.Set.t (** existentially-bound variables *)
; ctx: Context.t ; ctx: Context.t
(** first-order logical context induced by rest of formula *) (** first-order logical context induced by rest of formula *)
; pure: Term.t (** pure boolean constraints *) ; pure: Formula.t (** pure boolean constraints *)
; heap: seg list (** star-conjunction of segment atomic formulas *) ; heap: seg list (** star-conjunction of segment atomic formulas *)
; djns: disjunction list (** star-conjunction of disjunctions *) } ; djns: disjunction list (** star-conjunction of disjunctions *) }
@ -56,10 +56,10 @@ val or_ : t -> t -> t
(** Disjoin formulas, extending to a common vocabulary, and avoiding (** Disjoin formulas, extending to a common vocabulary, and avoiding
capturing existentials. *) capturing existentials. *)
val pure : Term.t -> t val pure : Formula.t -> t
(** Atomic pure boolean constraint formula. *) (** Atomic pure boolean constraint formula. *)
val and_ : Term.t -> t -> t val and_ : Formula.t -> t -> t
(** Conjoin a boolean constraint to a formula. *) (** Conjoin a boolean constraint to a formula. *)
val and_ctx : Context.t -> t -> t val and_ctx : Context.t -> t -> t
@ -72,7 +72,7 @@ val and_subst : Context.Subst.t -> t -> t
(** Update *) (** Update *)
val with_pure : Term.t -> t -> t val with_pure : Formula.t -> t -> t
(** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
[pure] are defined in the same vocabulary. Note that [ctx] is not [pure] are defined in the same vocabulary. Note that [ctx] is not
weakened, so if [pure] and [q.pure] do not induce the same context, then weakened, so if [pure] and [q.pure] do not induce the same context, then

12
sledge/src/sh_test.ml
Unescape View File

@ -24,7 +24,7 @@ let%test_module _ =
let ( ~$ ) = Var.Set.of_list let ( ~$ ) = Var.Set.of_list
let ( ! ) i = Term.integer (Z.of_int i) let ( ! ) i = Term.integer (Z.of_int i)
let ( - ) = Term.sub let ( - ) = Term.sub
let ( = ) = Term.eq let ( = ) = Formula.eq
let f = Term.splat (* any uninterpreted function *) let f = Term.splat (* any uninterpreted function *)
let wrt = Var.Set.empty let wrt = Var.Set.empty
@ -45,12 +45,12 @@ let%test_module _ =
let y = Term.var y_ let y = Term.var y_
let eq_concat (siz, seq) ms = let eq_concat (siz, seq) ms =
Term.( Formula.eq (Term.sized ~siz ~seq)
eq (sized ~siz ~seq) (Term.concat
(concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms))) (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
let of_eqs l = let of_eqs l =
List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Formula.eq a b) q) l
let%expect_test _ = let%expect_test _ =
let p = exists ~$[x_] (extend_us ~$[x_] emp) in let p = exists ~$[x_] (extend_us ~$[x_] emp) in
@ -160,7 +160,7 @@ let%test_module _ =
(star (star
(pure (eq_concat (!16, e) [|(!8, a); (!8, d)|])) (pure (eq_concat (!16, e) [|(!8, a); (!8, d)|]))
(or_ (or_
(pure (Term.dq x !0)) (pure (Formula.dq x !0))
(exists (exists
(Var.Set.of_list [b_]) (Var.Set.of_list [b_])
(pure (eq_concat (!8, a) [|(!4, c); (!4, b)|]))))) (pure (eq_concat (!8, a) [|(!4, c); (!4, b)|])))))

59
sledge/src/solver.ml
Unescape View File

@ -134,9 +134,8 @@ end
open Goal open Goal
let eq_concat (siz, seq) ms = let eq_concat (siz, seq) ms =
Term.( Formula.eq (Term.sized ~siz ~seq)
eq (sized ~siz ~seq) (Term.concat (Array.map ~f:(fun (siz, seq) -> Term.sized ~siz ~seq) ms))
(concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
let fresh_var name vs zs ~wrt = let fresh_var name vs zs ~wrt =
let v, wrt = Var.fresh name ~wrt in let v, wrt = Var.fresh name ~wrt in
@ -155,7 +154,7 @@ let excise_exists goal =
let solutions_for_xs = let solutions_for_xs =
let xs = let xs =
Var.Set.diff goal.xs Var.Set.diff goal.xs
(Sh.fv ~ignore_ctx:() (Sh.with_pure Term.true_ goal.sub)) (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.true_ goal.sub))
in in
Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
in in
@ -182,8 +181,8 @@ let excise_exists goal =
let excise_pure ({min; sub} as goal) = let excise_pure ({min; sub} as goal) =
trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ; trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
let pure' = Context.normalize min.ctx sub.pure in let pure' = Context.normalizef min.ctx sub.pure in
if Term.is_false pure' then None if Formula.is_false pure' then None
else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub)) else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
(* [k; o) (* [k; o)
@ -208,8 +207,9 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Term.eq a a') (Sh.rem_seg ssg sub))) (Sh.and_ (Formula.eq m m')
(Sh.and_ (Formula.eq a a') (Sh.rem_seg ssg sub)))
in in
goal |> with_ ~com ~min ~sub goal |> with_ ~com ~min ~sub
@ -246,9 +246,9 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Term.eq a0 a') (Sh.rem_seg ssg sub))) (Sh.and_ (Formula.eq a0 a') (Sh.rem_seg ssg sub)))
in in
goal |> with_ ~us ~com ~min ~xs ~sub ~zs goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@ -278,8 +278,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Var.Set.union us xs) in let a1', xs, zs, _ = fresh_var "a1" xs zs ~wrt:(Var.Set.union us xs) in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(o, a); (n_o, a1')|]) (eq_concat (n, a') [|(o, a); (n_o, a1')|])
(Sh.star (Sh.star
@ -324,9 +324,9 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub))) (Sh.and_ (Formula.eq a1 a') (Sh.rem_seg ssg sub)))
in in
goal |> with_ ~us ~com ~min ~xs ~sub ~zs goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@ -371,9 +371,9 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
(Sh.rem_seg msg min))) (Sh.rem_seg msg min)))
in in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Term.eq a1 a') (Sh.rem_seg ssg sub))) (Sh.and_ (Formula.eq a1 a') (Sh.rem_seg ssg sub)))
in in
goal |> with_ ~us ~com ~min ~xs ~sub ~zs goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@ -417,8 +417,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|]) (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
(Sh.star (Sh.star
@ -453,8 +453,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (o, a)|]) (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
(Sh.star (Sh.star
@ -493,8 +493,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
let com = Sh.star (Sh.seg msg) com in let com = Sh.star (Sh.seg msg) com in
let min = Sh.rem_seg msg min in let min = Sh.rem_seg msg min in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|]) (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
(Sh.star (Sh.star
@ -544,8 +544,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
(Sh.rem_seg msg min)) (Sh.rem_seg msg min))
in in
let sub = let sub =
Sh.and_ (Term.eq b b') Sh.and_ (Formula.eq b b')
(Sh.and_ (Term.eq m m') (Sh.and_ (Formula.eq m m')
(Sh.and_ (Sh.and_
(eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|]) (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
(Sh.star (Sh.star
@ -569,8 +569,9 @@ let excise_seg ({sub} as goal) msg ssg =
Some Some
( goal ( goal
|> with_ |> with_
~sub:(Sh.and_ (Term.eq b b') (Sh.and_ (Term.eq m m') goal.sub)) ~sub:
) (Sh.and_ (Formula.eq b b')
(Sh.and_ (Formula.eq m m') goal.sub)) )
else else
match Int.sign (Z.sign k_l) with match Int.sign (Z.sign k_l) with
(* k-l < 0 so k < l *) (* k-l < 0 so k < l *)

12
sledge/src/solver_test.ml
Unescape View File

@ -69,7 +69,7 @@ let%test_module _ =
) infer_frame: false |}] ) infer_frame: false |}]
let%expect_test _ = let%expect_test _ =
check_frame Sh.emp [n_; m_] (Sh.and_ (Term.eq m n) Sh.emp) ; check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ;
[%expect [%expect
{| {|
( infer_frame: emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp ( infer_frame: emp \- ∃ %m_8, %n_9 . %m_8 = %n_9 ∧ emp
@ -101,7 +101,7 @@ let%test_module _ =
let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
let minued = Sh.star common seg1 in let minued = Sh.star common seg1 in
let subtrahend = let subtrahend =
Sh.and_ (Term.eq m n) Sh.and_ (Formula.eq m n)
(Sh.exists (Sh.exists
(Var.Set.of_list [m_]) (Var.Set.of_list [m_])
(Sh.extend_us (Var.Set.of_list [m_]) common)) (Sh.extend_us (Var.Set.of_list [m_]) common))
@ -229,7 +229,7 @@ let%test_module _ =
let%expect_test _ = let%expect_test _ =
check_frame check_frame
(Sh.and_ (Sh.and_
Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2)) Formula.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
seg_split_symbolically) seg_split_symbolically)
[m_; a_] [m_; a_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
@ -263,7 +263,7 @@ let%test_module _ =
(* Incompleteness: equivalent to above but using ≤ instead of ∨ *) (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)
let%expect_test _ = let%expect_test _ =
infer_frame infer_frame
(Sh.and_ (Term.le n !2) seg_split_symbolically) (Sh.and_ (Formula.le n !2) seg_split_symbolically)
[m_; a_] [m_; a_]
(Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ; (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
[%expect [%expect
@ -278,7 +278,9 @@ let%test_module _ =
(* Incompleteness: cannot witness existentials to satisfy non-equality (* Incompleteness: cannot witness existentials to satisfy non-equality
pure constraints *) pure constraints *)
let%expect_test _ = let%expect_test _ =
let subtrahend = Sh.and_ (Term.eq m a) (Sh.pure (Term.dq m !0)) in let subtrahend =
Sh.and_ (Formula.eq m a) (Sh.pure (Formula.dq m !0))
in
let minuend = Sh.extend_us (Var.Set.of_ a_) Sh.emp in let minuend = Sh.extend_us (Var.Set.of_ a_) Sh.emp in
infer_frame minuend [m_] subtrahend ; infer_frame minuend [m_] subtrahend ;
[%expect [%expect

Write Preview
Loading…
Cancel
Save