diff --git a/src/smt/literal.ml b/src/smt/literal.ml deleted file mode 100644 index 0d939be7..00000000 --- a/src/smt/literal.ml +++ /dev/null @@ -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 - diff --git a/src/smt/literal.mli b/src/smt/literal.mli deleted file mode 100644 index f38963ab..00000000 --- a/src/smt/literal.mli +++ /dev/null @@ -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 - - diff --git a/src/smt/term.ml b/src/smt/term.ml index 4d0db744..8a670468 100644 --- a/src/smt/term.ml +++ b/src/smt/term.ml @@ -59,6 +59,7 @@ end module T = Hashcons.Make(H) let view t = t +let head t = t.head let rec print fmt t = match t.head with | Ite (a,b,c) -> diff --git a/src/smt/term.mli b/src/smt/term.mli index c9542d3d..92defc96 100644 --- a/src/smt/term.mli +++ b/src/smt/term.mli @@ -26,6 +26,7 @@ and head = | Ite of t * t * t val view : t -> view +val head : t -> head val app : Symbols.t -> t list -> Ty.t -> t val const : Symbols.t -> Ty.t -> t diff --git a/src/smt/uf.ml b/src/smt/uf.ml index 573189c6..9ee4e98f 100644 --- a/src/smt/uf.ml +++ b/src/smt/uf.ml @@ -21,191 +21,124 @@ type 'a literal = exception Inconsistent of Explanation.t exception Unsolvable -module type ELT = sig - type r +module Ex = Explanation +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 - - val leaves : r -> r list - - 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 + let leaves t : r list = match T.head t with + | T.Ite (a, _, _) -> [a] + | T.App (_, l) -> l end -module type S = sig - type t +type r = R.r - 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 ( 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 c = R.compare r1 r2 in - if c <> 0 then c - else R.compare r1' r2' - end) +module SetRR = Set.Make(struct + type t = r * r + let compare (r1, r1') (r2, r2') = + let c = T.compare r1 r2 in + if c <> 0 then c + else T.compare r1' r2' + end) - type t = { +type t = { + (* term -> [t] *) + make : r MapT.t; - (* term -> [t] *) - make : R.r MapT.t; + (* representative table *) + repr : (r * Ex.t) MapR.t; - (* representative table *) - repr : (R.r * Ex.t) MapR.t; + (* r -> class (of terms) *) + classes : SetT.t MapR.t; - (* r -> class (of terms) *) - classes : SetT.t MapR.t; + (*associates each value r with the set of semantical values whose + representatives contains r *) + gamma : SetR.t MapR.t; - (*associates each value r with the set of semantical values whose - representatives contains r *) - gamma : SetR.t MapR.t; + (* the disequations map *) + neqs: Ex.t MapL.t MapR.t; - (* the disequations map *) - neqs: Ex.t MapL.t MapR.t; +} - } +let empty = { + make = MapT.empty; + repr = MapR.empty; + classes = MapR.empty; + gamma = MapR.empty; + neqs = MapR.empty; +} - let empty = { - make = MapT.empty; - repr = MapR.empty; - classes = MapR.empty; - gamma = MapR.empty; - neqs = MapR.empty; - } +module Env = struct + let mem env t = MapT.mem t env.make - module Env = struct + let lookup_by_t t env = + try MapR.find (MapT.find t env.make) env.repr + with Not_found -> + assert false (*R.make t, Ex.empty*) (* XXXX *) - let mem env t = MapT.mem t env.make + let lookup_by_r r env = + try MapR.find r env.repr with Not_found -> r, Ex.empty - let lookup_by_t t env = - try MapR.find (MapT.find t env.make) env.repr - with Not_found -> - assert false (*R.make t, Ex.empty*) (* XXXX *) + let lookup_for_neqs env r = + try MapR.find r env.neqs with Not_found -> MapL.empty - let lookup_by_r r env = - try MapR.find r env.repr with Not_found -> r, Ex.empty + let add_to_classes t r classes = + MapR.add r + (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) + classes - let lookup_for_neqs env r = - try MapR.find r env.neqs with Not_found -> MapL.empty + let update_classes c nc classes = + let s1 = try MapR.find c classes with Not_found -> SetT.empty in + let s2 = try MapR.find nc classes with Not_found -> SetT.empty in + MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) - let add_to_classes t r classes = - MapR.add r - (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) - classes + let add_to_gamma r c gamma = + List.fold_left + (fun gamma x -> + let s = try MapR.find x gamma with Not_found -> SetR.empty in + MapR.add x (SetR.add r s) gamma) + gamma + (R.leaves c) - let update_classes c nc classes = - let s1 = try MapR.find c classes with Not_found -> SetT.empty in - let s2 = try MapR.find nc classes with Not_found -> SetT.empty in - MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) + (* r1 = r2 => neqs(r1) \uplus neqs(r2) *) + let update_neqs r1 r2 dep env = + let nq_r1 = lookup_for_neqs env r1 in + let nq_r2 = lookup_for_neqs env r2 in + let mapl = + MapL.fold + (fun l1 ex1 mapl -> + try + let ex2 = MapL.find l1 mapl in + let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) + raise (Inconsistent ex) + with Not_found -> + MapL.add l1 (Ex.union ex1 dep) mapl) + nq_r1 nq_r2 + in + MapR.add r2 mapl (MapR.add r1 mapl env.neqs) - let add_to_gamma r c gamma = - List.fold_left - (fun gamma x -> - let s = try MapR.find x gamma with Not_found -> SetR.empty in - MapR.add x (SetR.add r s) gamma) - gamma (R.leaves c) + let filter_leaves r = + List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) - (* r1 = r2 => neqs(r1) \uplus neqs(r2) *) - let update_neqs r1 r2 dep env = - let nq_r1 = lookup_for_neqs env r1 in - let nq_r2 = lookup_for_neqs env r2 in - let mapl = - MapL.fold - (fun l1 ex1 mapl -> - try - let ex2 = MapL.find l1 mapl in - let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) - raise (Inconsistent ex) - with Not_found -> - MapL.add l1 (Ex.union ex1 dep) mapl) - nq_r1 nq_r2 - in - MapR.add r2 mapl (MapR.add r1 mapl env.neqs) + let find_or_normal_form env r = + try MapR.find r env.repr with Not_found -> r, Ex.empty - let filter_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 = - try MapR.find r env.repr with Not_found -> normal_form env r - - let init_leaf env p = - let in_repr = MapR.mem p env.repr in - let in_neqs = MapR.mem p env.neqs in - { env with + let init_leaf env p = + let in_repr = MapR.mem p env.repr in + let in_neqs = MapR.mem p env.neqs in + { env with repr = if in_repr then env.repr else MapR.add p (p, Ex.empty) env.repr; @@ -219,163 +152,159 @@ module Make ( R : ELT ) = struct if in_neqs then env.neqs else update_neqs p p Ex.empty env } - let init_term env t = - let mkr, ctx = R.make t in - let rp, ex = normal_form env mkr in - { make = MapT.add t mkr env.make; - repr = MapR.add mkr (rp,ex) env.repr; - classes = add_to_classes t rp env.classes; - gamma = add_to_gamma mkr rp env.gamma; - neqs = - if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) - else MapR.add rp MapL.empty env.neqs}, ctx + let init_term env t = + let mkr, ctx = R.make t in + let rp, ex = normal_form env mkr in + { make = MapT.add t mkr env.make; + repr = MapR.add mkr (rp,ex) env.repr; + classes = add_to_classes t rp env.classes; + gamma = add_to_gamma mkr rp env.gamma; + neqs = + if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) + else MapR.add rp MapL.empty env.neqs}, ctx - let update_aux dep set env= - SetRR.fold - (fun (rr, nrr) env -> - { env with + let update_aux dep set env= + SetRR.fold + (fun (rr, nrr) env -> + { env with neqs = update_neqs rr nrr dep env ; classes = update_classes rr nrr env.classes}) - set env + set env - let apply_sigma_uf env (p, v, dep) = - assert (MapR.mem p env.gamma); - let use_p = MapR.find p env.gamma in - try - let env, tch, neqs_to_up = SetR.fold - (fun r (env, touched, neqs_to_up) -> - let rr, ex = MapR.find r env.repr in - let nrr = R.subst p v rr in - if R.equal rr nrr then env, touched, neqs_to_up - else - let ex = Ex.union ex dep in - let env = - {env with + let apply_sigma_uf env (p, v, dep) = + assert (MapR.mem p env.gamma); + let use_p = MapR.find p env.gamma in + try + let env, tch, neqs_to_up = SetR.fold + (fun r (env, touched, neqs_to_up) -> + let rr, ex = MapR.find r env.repr in + let nrr = R.subst p v rr in + if R.equal rr nrr then env, touched, neqs_to_up + else + let ex = Ex.union ex dep in + let env = + {env with repr = MapR.add r (nrr, ex) env.repr; gamma = add_to_gamma r nrr env.gamma } - in - env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up - ) use_p (env, [], SetRR.empty) in - (* Correction : Do not update neqs twice for the same r *) - update_aux dep neqs_to_up env, tch - - with Not_found -> assert false - - let apply_sigma eqs env tch ((p, v, dep) as sigma) = - let env = init_leaf env p in - let env, touched = apply_sigma_uf env sigma in - env, ((p, touched, v) :: tch) - - end - - let add 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) = - (* 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); *) - let rv, ex_rv = Env.find_or_normal_form env v in - (* let rv = v in *) - (* assert ( let rv, _ = Env.find_or_normal_form env v in R.equal v rv); *) - let dep = Ex.union ex_rv dep in - Env.apply_sigma eqs env tch (p, rv, dep) - - let check_consistent env r1 r2 dep : unit = - let rr1, ex_r1 = Env.find_or_normal_form env r1 in - let rr2, ex_r2 = Env.find_or_normal_form env r2 in - if R.equal rr1 rr2 - then () (* Remove rule *) - else - let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in - begin - ignore (Env.update_neqs rr1 rr2 dep env); - if R.can_be_equal rr1 rr2 - then () - else raise (Inconsistent dep) - end - - let union env r1 r2 dep = - check_consistent env r1 r2 dep; - () - - let rec distinct env rl dep = - let d = Lit.make (Literal.Distinct (false,rl)) in - let env, _, newds = - List.fold_left - (fun (env, mapr, newds) r -> - let rr, ex = Env.find_or_normal_form env r in - try - let exr = MapR.find rr mapr in - raise (Inconsistent (Ex.union ex exr)) - with Not_found -> - let uex = Ex.union ex dep in - let mdis = - try MapR.find rr env.neqs with Not_found -> MapL.empty in - let mdis = - try - MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis - with Not_found -> - MapL.add d uex mdis - in - let env = Env.init_leaf env rr in - let env = {env with neqs = MapR.add rr mdis env.neqs} in - env, MapR.add rr uex mapr, (rr, ex, mapr)::newds - ) - (env, MapR.empty, []) - rl - in - List.fold_left - (fun env (r1, ex1, mapr) -> - MapR.fold (fun r2 ex2 env -> - let ex = Ex.union ex1 (Ex.union ex2 dep) in - try match R.solve r1 r2 with - | [a, b] -> - if (R.equal a r1 && R.equal b r2) || - (R.equal a r2 && R.equal b r1) then env - else - distinct env [a; b] ex - | [] -> - raise (Inconsistent ex) - | _ -> env - with Unsolvable -> env) mapr env) - env newds - - let are_equal env t1 t2 = - let r1, ex_r1 = Env.lookup_by_t t1 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 - - let are_distinct env t1 t2 = - let r1, ex_r1 = Env.lookup_by_t t1 env in - let r2, ex_r2 = Env.lookup_by_t t2 env in - try - ignore (union env r1 r2 (Ex.union ex_r1 ex_r2)); - No - with Inconsistent ex -> Yes(ex) - - let already_distinct env lr = - let d = Lit.make (Literal.Distinct (false,lr)) in - try - List.iter (fun r -> - let mdis = MapR.find r env.neqs in - ignore (MapL.find d mdis) - ) lr; - true - with Not_found -> false - - let find env t = - Env.lookup_by_t t env - - let find_r = Env.find_or_normal_form - - let mem = Env.mem - - let class_of env t = - try - let rt, _ = MapR.find (MapT.find t env.make) env.repr in - SetT.elements (MapR.find rt env.classes) - with Not_found -> [t] + in + env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up + ) use_p (env, [], SetRR.empty) in + (* Correction : Do not update neqs twice for the same r *) + update_aux dep neqs_to_up env, tch + with Not_found -> assert false + let apply_sigma eqs env tch ((p, v, dep) as sigma) = + let env = init_leaf env p in + let env, touched = apply_sigma_uf env sigma in + env, ((p, touched, v) :: tch) end + +let add 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) = + (* 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); *) + let rv, ex_rv = Env.find_or_normal_form env v in + (* let rv = v in *) + (* assert ( let rv, _ = Env.find_or_normal_form env v in R.equal v rv); *) + let dep = Ex.union ex_rv dep in + Env.apply_sigma eqs env tch (p, rv, dep) + +let check_consistent env r1 r2 dep : unit = + let rr1, ex_r1 = Env.find_or_normal_form env r1 in + let rr2, ex_r2 = Env.find_or_normal_form env r2 in + if R.equal rr1 rr2 + then () (* Remove rule *) + else + let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in + begin + ignore (Env.update_neqs rr1 rr2 dep env); + if R.can_be_equal rr1 rr2 + then () + else raise (Inconsistent dep) + end + +let union env r1 r2 dep = + check_consistent env r1 r2 dep; + () + +let rec distinct env rl dep = + let d = Lit.make (Literal.Distinct (false,rl)) in + let env, _, newds = + List.fold_left + (fun (env, mapr, newds) r -> + let rr, ex = Env.find_or_normal_form env r in + try + let exr = MapR.find rr mapr in + raise (Inconsistent (Ex.union ex exr)) + with Not_found -> + let uex = Ex.union ex dep in + let mdis = + try MapR.find rr env.neqs with Not_found -> MapL.empty in + let mdis = + try + MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis + with Not_found -> + MapL.add d uex mdis + in + let env = Env.init_leaf env rr in + let env = {env with neqs = MapR.add rr mdis env.neqs} in + env, MapR.add rr uex mapr, (rr, ex, mapr)::newds + ) + (env, MapR.empty, []) + rl + in + List.fold_left + (fun env (r1, ex1, mapr) -> + MapR.fold (fun r2 ex2 env -> + let ex = Ex.union ex1 (Ex.union ex2 dep) in + try match R.solve r1 r2 with + | [a, b] -> + if (R.equal a r1 && R.equal b r2) || + (R.equal a r2 && R.equal b r1) then env + else + distinct env [a; b] ex + | [] -> + raise (Inconsistent ex) + | _ -> env + with Unsolvable -> env) mapr env) + env newds + +let are_equal env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 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 + +let are_distinct env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 env in + let r2, ex_r2 = Env.lookup_by_t t2 env in + try + ignore (union env r1 r2 (Ex.union ex_r1 ex_r2)); + No + with Inconsistent ex -> Yes(ex) + +let already_distinct env lr = + let d = Lit.make (Literal.Distinct (false,lr)) in + try + List.iter (fun r -> + let mdis = MapR.find r env.neqs in + ignore (MapL.find d mdis) + ) lr; + true + with Not_found -> false + +let find env t = + Env.lookup_by_t t env + +let find_r = Env.find_or_normal_form + +let mem = Env.mem + +let class_of env t = + try + let rt, _ = MapR.find (MapT.find t env.make) env.repr in + SetT.elements (MapR.find rt env.classes) + with Not_found -> [t] diff --git a/src/smt/uf.mli b/src/smt/uf.mli index 3b30e261..8205e3ee 100644 --- a/src/smt/uf.mli +++ b/src/smt/uf.mli @@ -18,61 +18,28 @@ type 'a literal = | LSem of 'a Literal.view | LTerm of Literal.LT.t -module type ELT = sig - type r +type t - 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 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 +val class_of : t -> Term.t -> Term.t list