simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 21:24:06 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip

Browse source
This commit is contained in:
Simon Cruanes 2016-08-24 18:23:01 +02:00
parent 41557a1509
commit bb2c931d68
6 changed files with 256 additions and 604 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

184
src/smt/literal.ml
View file

@ -1,184 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Msat
type 'a view =
| Eq of 'a * 'a
| Distinct of bool * 'a list
| Builtin of bool * ID.t * 'a list
module type OrderedType = sig
type t
val compare : t -> t -> int
val hash : t -> int
val print : Format.formatter -> t -> unit
end
module type S = sig
type elt
type t
val make : elt view -> t
val view : t -> elt view
val neg : t -> t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
module Map : Map.S with type key = t
module Set : Set.S with type elt = t
end
module Make (X : OrderedType) : S with type elt = X.t = struct
type elt = X.t
type t = {
view: X.t view;
mutable tag: int;
}
module V = struct
type t_ = t
type t = t_
let equal a1 a2 =
match a1.view, a2.view with
| Eq(t1, t2), Eq(u1, u2) ->
(X.compare t1 u1 = 0 && X.compare t2 u2 = 0) ||
(X.compare t1 u2 = 0 && X.compare t2 u1 = 0)
| Distinct (b1,lt1), Distinct (b2,lt2) ->
(try
b1 = b2 &&
List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2
with Invalid_argument _ -> false)
| Builtin(b1, n1, l1), Builtin(b2, n2, l2) ->
(try
b1 = b2 && ID.equal n1 n2
&&
List.for_all2 (fun x y -> X.compare x y = 0) l1 l2
with Invalid_argument _ -> false)
| _ -> false
let hash a = match a.view with
| Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2))
| Distinct (b,lt) ->
let x = if b then 7 else 23 in
abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt)
| Builtin(b, n, l) ->
let x = if b then 7 else 23 in
abs
(List.fold_left
(fun acc t-> acc*13 + X.hash t) (ID.hash n+x) l)
let set_id t tag = t.tag <- tag
end
module H = Hashcons.Make(V)
let compare a1 a2 = Pervasives.compare a1.tag a2.tag
let equal a1 a2 = a1 == a2
let hash a1 = a1.tag
module T = struct
type t_ = t
type t = t_
let compare=compare
end
let make t = H.hashcons {view=t; tag= -1}
let view a = a.view
let neg a = match view a with
| Eq(x, y) -> make (Distinct (false,[x; y]))
| Distinct (false, [x; y]) -> make (Eq (x, y))
| Distinct (true, [x; y]) -> make (Distinct (false,[x; y]))
| Distinct (false, l) -> make (Distinct (true,l))
| Distinct _ -> assert false
| Builtin(b, n, l) -> make (Builtin (not b, n, l))
let print_list fmt = function
| [] -> ()
| z :: l ->
Format.fprintf fmt "%a" X.print z;
List.iter (Format.fprintf fmt ", %a" X.print) l
let print fmt a = match view a with
| Eq (z1, z2) ->
if equal z1 z2 then Format.fprintf fmt "True"
else Format.fprintf fmt "%a=%a" X.print z1 X.print z2
| Distinct (b,(z::l)) ->
let b = if b then "~" else "" in
Format.fprintf fmt "%s%a" b X.print z;
List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l
| Builtin (b, n, l) ->
let b = if b then "" else "~" in
Format.fprintf fmt "%s%s(%a)" b (ID.to_string n) print_list l
| _ -> assert false
module Set = Set.Make(T)
module Map = Map.Make(T)
end
module type S_Term = sig
include S with type elt = Term.t
val mk_pred : Term.t -> t
val true_ : t
val false_ : t
(* val terms_of : t -> Term.Set.t
val vars_of : t -> Symbols.Set.t
*)
(* module SetEq : Set.S with type elt = t * Term.t * Term.t*)
end
module LT : S_Term = struct
module L = Make(Term)
include L
let mk_pred t = make (Eq (t, Term.true_) )
let true_ = mk_pred Term.true_
let false_ = mk_pred Term.false_
let neg a = match view a with
| Eq(t1, t2) when Term.equal t2 Term.false_ ->
make (Eq (t1, Term.true_))
| Eq(t1, t2) when Term.equal t2 Term.true_ ->
make (Eq (t1, Term.false_))
| _ -> L.neg a
(* let terms_of a =
let l = match view a with
| Eq (t1, t2) -> [t1; t2]
| Distinct (_, l) | Builtin (_, _, l) -> l
in
List.fold_left Term.subterms Term.Set.empty l
*)
module SS = Symbols.Set
(* let vars_of a =
Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty
*)
end

62
src/smt/literal.mli
View file

@ -1,62 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Msat
module type OrderedType = sig
type t
val compare : t -> t -> int
val hash : t -> int
val print : Format.formatter -> t -> unit
end
type 'a view =
| Eq of 'a * 'a
| Distinct of bool * 'a list
| Builtin of bool * ID.t * 'a list
module type S = sig
type elt
type t
val make : elt view -> t
val view : t -> elt view
val neg : t -> t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
module Map : Map.S with type key = t
module Set : Set.S with type elt = t
end
module Make ( X : OrderedType ) : S with type elt = X.t
module type S_Term = sig
include S with type elt = Term.t
val mk_pred : Term.t -> t
val true_ : t
val false_ : t
end
module LT : S_Term

1
src/smt/term.ml
View file

@ -59,6 +59,7 @@ end
module T = Hashcons.Make(H) module T = Hashcons.Make(H)
let view t = t let view t = t
let head t = t.head
let rec print fmt t = match t.head with let rec print fmt t = match t.head with
| Ite (a,b,c) -> | Ite (a,b,c) ->

1
src/smt/term.mli
View file

@ -26,6 +26,7 @@ and head =
| Ite of t * t * t | Ite of t * t * t
val view : t -> view val view : t -> view
val head : t -> head
val app : Symbols.t -> t list -> Ty.t -> t val app : Symbols.t -> t list -> Ty.t -> t
val const : Symbols.t -> Ty.t -> t val const : Symbols.t -> Ty.t -> t

157
src/smt/uf.ml
View file

@ -21,93 +21,44 @@ type 'a literal =
exception Inconsistent of Explanation.t exception Inconsistent of Explanation.t
exception Unsolvable exception Unsolvable
module type ELT = sig module Ex = Explanation
type r module Sy = Symbols
module T = Term
module MapT = Term.Map
module SetT = Term.Set
val make : Term.t -> r * Literal.LT.t list module Lit = Literal.Make(T)
module MapL = Lit.Map
val compare : r -> r -> int module MapR = MapT
module SetR = SetT
val equal : r -> r -> bool module R = struct
include T
type r = t
val hash : r -> int let leaves t : r list = match T.head t with
| T.Ite (a, _, _) -> [a]
val leaves : r -> r list | T.App (_, l) -> l
val subst : r -> r -> r -> r
val can_be_equal : r -> r -> bool
val term_embed : Term.t -> r
val term_extract : r -> Term.t option
val unsolvable : r -> bool
val fully_interpreted : Symbols.t -> bool
val print : Format.formatter -> r -> unit
end end
module type S = sig type r = R.r
type t
module R : ELT module SetRR = Set.Make(struct
type t = r * r
val empty : t
val add : t -> Term.t -> t * Literal.LT.t list
val mem : t -> Term.t -> bool
val find : t -> Term.t -> R.r * Explanation.t
val find_r : t -> R.r -> R.r * Explanation.t
val union :
t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t
val are_equal : t -> Term.t -> Term.t -> Sig.answer
val are_distinct : t -> Term.t -> Term.t -> Sig.answer
val already_distinct : t -> R.r list -> bool
val class_of : t -> Term.t -> Term.t list
end
module Make ( R : ELT ) = struct
module Ex = Explanation
module R = R
module Sy = Symbols
module T = Term
module MapT = Term.Map
module SetT = Term.Set
module Lit = Literal.Make(struct type t = R.r include R end)
module MapL = Lit.Map
module MapR = Map.Make(struct type t = R.r let compare = R.compare end)
module SetR = Set.Make(struct type t = R.r let compare = R.compare end)
module SetRR = Set.Make(struct
type t = R.r * R.r
let compare (r1, r1') (r2, r2') = let compare (r1, r1') (r2, r2') =
let c = R.compare r1 r2 in let c = T.compare r1 r2 in
if c <> 0 then c if c <> 0 then c
else R.compare r1' r2' else T.compare r1' r2'
end) end)
type t = { type t = {
(* term -> [t] *) (* term -> [t] *)
make : R.r MapT.t; make : r MapT.t;
(* representative table *) (* representative table *)
repr : (R.r * Ex.t) MapR.t; repr : (r * Ex.t) MapR.t;
(* r -> class (of terms) *) (* r -> class (of terms) *)
classes : SetT.t MapR.t; classes : SetT.t MapR.t;
@ -119,18 +70,17 @@ module Make ( R : ELT ) = struct
(* the disequations map *) (* the disequations map *)
neqs: Ex.t MapL.t MapR.t; neqs: Ex.t MapL.t MapR.t;
} }
let empty = { let empty = {
make = MapT.empty; make = MapT.empty;
repr = MapR.empty; repr = MapR.empty;
classes = MapR.empty; classes = MapR.empty;
gamma = MapR.empty; gamma = MapR.empty;
neqs = MapR.empty; neqs = MapR.empty;
} }
module Env = struct
module Env = struct
let mem env t = MapT.mem t env.make let mem env t = MapT.mem t env.make
let lookup_by_t t env = let lookup_by_t t env =
@ -159,7 +109,8 @@ module Make ( R : ELT ) = struct
(fun gamma x -> (fun gamma x ->
let s = try MapR.find x gamma with Not_found -> SetR.empty in let s = try MapR.find x gamma with Not_found -> SetR.empty in
MapR.add x (SetR.add r s) gamma) MapR.add x (SetR.add r s) gamma)
gamma (R.leaves c) gamma
(R.leaves c)
(* r1 = r2 => neqs(r1) \uplus neqs(r2) *) (* r1 = r2 => neqs(r1) \uplus neqs(r2) *)
let update_neqs r1 r2 dep env = let update_neqs r1 r2 dep env =
@ -181,26 +132,8 @@ module Make ( R : ELT ) = struct
let filter_leaves r = let filter_leaves r =
List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r)
let canon_empty st env =
SetR.fold
(fun p ((z, ex) as acc) ->
let q, ex_q = lookup_by_r p env in
if R.equal p q then acc else (p,q)::z, Ex.union ex_q ex)
st ([], Ex.empty)
let canon_aux rx = List.fold_left (fun r (p,v) -> R.subst p v r) rx
let rec canon env r ex_r =
let se = filter_leaves r in
let subst, ex_subst = canon_empty se env in
let r2 = canon_aux r subst in
let ex_r2 = Ex.union ex_r ex_subst in
if R.equal r r2 then r2, ex_r2 else canon env r2 ex_r2
let normal_form env r = canon env r Ex.empty
let find_or_normal_form env r = let find_or_normal_form env r =
try MapR.find r env.repr with Not_found -> normal_form env r try MapR.find r env.repr with Not_found -> r, Ex.empty
let init_leaf env p = let init_leaf env p =
let in_repr = MapR.mem p env.repr in let in_repr = MapR.mem p env.repr in
@ -266,13 +199,12 @@ module Make ( R : ELT ) = struct
let env = init_leaf env p in let env = init_leaf env p in
let env, touched = apply_sigma_uf env sigma in let env, touched = apply_sigma_uf env sigma in
env, ((p, touched, v) :: tch) env, ((p, touched, v) :: tch)
end
end let add env t =
let add env t =
if MapT.mem t env.make then env, [] else Env.init_term env t if MapT.mem t env.make then env, [] else Env.init_term env t
let ac_solve eqs dep (env, tch) (p, v) = let ac_solve eqs dep (env, tch) (p, v) =
(* pourquoi recuperer le representant de rv? r = rv d'apres testopt *) (* pourquoi recuperer le representant de rv? r = rv d'apres testopt *)
(* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *) (* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *)
let rv, ex_rv = Env.find_or_normal_form env v in let rv, ex_rv = Env.find_or_normal_form env v in
@ -281,7 +213,7 @@ module Make ( R : ELT ) = struct
let dep = Ex.union ex_rv dep in let dep = Ex.union ex_rv dep in
Env.apply_sigma eqs env tch (p, rv, dep) Env.apply_sigma eqs env tch (p, rv, dep)
let check_consistent env r1 r2 dep : unit = let check_consistent env r1 r2 dep : unit =
let rr1, ex_r1 = Env.find_or_normal_form env r1 in let rr1, ex_r1 = Env.find_or_normal_form env r1 in
let rr2, ex_r2 = Env.find_or_normal_form env r2 in let rr2, ex_r2 = Env.find_or_normal_form env r2 in
if R.equal rr1 rr2 if R.equal rr1 rr2
@ -295,11 +227,11 @@ module Make ( R : ELT ) = struct
else raise (Inconsistent dep) else raise (Inconsistent dep)
end end
let union env r1 r2 dep = let union env r1 r2 dep =
check_consistent env r1 r2 dep; check_consistent env r1 r2 dep;
() ()
let rec distinct env rl dep = let rec distinct env rl dep =
let d = Lit.make (Literal.Distinct (false,rl)) in let d = Lit.make (Literal.Distinct (false,rl)) in
let env, _, newds = let env, _, newds =
List.fold_left List.fold_left
@ -341,12 +273,12 @@ module Make ( R : ELT ) = struct
with Unsolvable -> env) mapr env) with Unsolvable -> env) mapr env)
env newds env newds
let are_equal env t1 t2 = let are_equal env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in let r2, ex_r2 = Env.lookup_by_t t2 env in
if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No
let are_distinct env t1 t2 = let are_distinct env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in let r2, ex_r2 = Env.lookup_by_t t2 env in
try try
@ -354,7 +286,7 @@ module Make ( R : ELT ) = struct
No No
with Inconsistent ex -> Yes(ex) with Inconsistent ex -> Yes(ex)
let already_distinct env lr = let already_distinct env lr =
let d = Lit.make (Literal.Distinct (false,lr)) in let d = Lit.make (Literal.Distinct (false,lr)) in
try try
List.iter (fun r -> List.iter (fun r ->
@ -364,18 +296,15 @@ module Make ( R : ELT ) = struct
true true
with Not_found -> false with Not_found -> false
let find env t = let find env t =
Env.lookup_by_t t env Env.lookup_by_t t env
let find_r = Env.find_or_normal_form let find_r = Env.find_or_normal_form
let mem = Env.mem let mem = Env.mem
let class_of env t = let class_of env t =
try try
let rt, _ = MapR.find (MapT.find t env.make) env.repr in let rt, _ = MapR.find (MapT.find t env.make) env.repr in
SetT.elements (MapR.find rt env.classes) SetT.elements (MapR.find rt env.classes)
with Not_found -> [t] with Not_found -> [t]
end

65
src/smt/uf.mli
View file

@ -18,61 +18,28 @@ type 'a literal =
| LSem of 'a Literal.view | LSem of 'a Literal.view
| LTerm of Literal.LT.t | LTerm of Literal.LT.t
module type ELT = sig type t
type r
val make : Term.t -> r * Literal.LT.t list type r
(** representative *)
val type_info : r -> Ty.t val empty : t
val add : t -> Term.t -> t * Literal.LT.t list
val compare : r -> r -> int val mem : t -> Term.t -> bool
val equal : r -> r -> bool val find : t -> Term.t -> r * Explanation.t
val hash : r -> int val find_r : t -> r -> r * Explanation.t
val leaves : r -> r list val union :
t -> r -> r -> Explanation.t ->
t * (r * (r * r * Explanation.t) list * r) list
val subst : r -> r -> r -> r val distinct : t -> r list -> Explanation.t -> t
val solve : r -> r -> (r * r) list val are_equal : t -> Term.t -> Term.t -> Sig.answer
val are_distinct : t -> Term.t -> Term.t -> Sig.answer
val already_distinct : t -> r list -> bool
val term_embed : Term.t -> r val class_of : t -> Term.t -> Term.t list
val term_extract : r -> Term.t option
val unsolvable : r -> bool
val fully_interpreted : Symbols.t -> bool
val print : Format.formatter -> r -> unit
end
module type S = sig
type t
module R : ELT
val empty : t
val add : t -> Term.t -> t * Literal.LT.t list
val mem : t -> Term.t -> bool
val find : t -> Term.t -> R.r * Explanation.t
val find_r : t -> R.r -> R.r * Explanation.t
val union :
t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t
val are_equal : t -> Term.t -> Term.t -> Sig.answer
val are_distinct : t -> Term.t -> Term.t -> Sig.answer
val already_distinct : t -> R.r list -> bool
val class_of : t -> Term.t -> Term.t list
end
module Make ( X : ELT ) : S with module R = X