diff --git a/Makefile b/Makefile index 8f9d6531..6fbc8a0d 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind FLAGS= -DOC=msat.docdir/index.html msat_sat.docdir/index.html msat_smt.docdir/index.html +DOC=src/msat.docdir/index.html BIN=main.native TEST_BIN=tests/test_api.native diff --git a/README.md b/README.md index a8cb7975..8be962af 100644 --- a/README.md +++ b/README.md @@ -12,6 +12,9 @@ It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero). This program is distributed under the Apache Software License version 2.0. See the enclosed file `LICENSE`. +## Documentation + +See https://gbury.github.io/mSAT/ ## USAGE diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 954c833f..ba627886 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -140,7 +140,7 @@ module type S = sig val add_atom : formula -> atom (** Returns the atom associated with the given formula *) val make_boolean_var : formula -> var * Formula_intf.negated - (** Returns the variable linked with the given formula, and wether the atom associated with the formula + (** Returns the variable linked with the given formula, and whether the atom associated with the formula is [var.pa] or [var.na] *) val empty_clause : clause diff --git a/src/msat.odocl b/src/msat.odocl index ff4f7d94..8a2003a7 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -13,7 +13,6 @@ solver/Tseitin_intf # Main modules core/Res -core/Res_intf core/Internal core/External core/Solver_types @@ -21,7 +20,6 @@ core/Solver_types solver/Solver solver/Mcsolver solver/Tseitin -solver/Tseitin_intf # Backends backend/Dot @@ -30,3 +28,20 @@ backend/Backend_intf # Auxiliary util/Hashcons + + +# SAT solver frontend +sat/Expr_sat +sat/Sat +sat/Type_sat + +# SMT solver frontend +smt/Expr_smt +smt/Smt +smt/Type_smt +smt/Unionfind + +# MCsat +mcsat/Eclosure +mcsat/Mcsat +mcsat/Plugin_mcsat diff --git a/src/msat_sat.odocl b/src/msat_sat.odocl deleted file mode 100644 index 1fb3c3bf..00000000 --- a/src/msat_sat.odocl +++ /dev/null @@ -1,3 +0,0 @@ - -smt/Sat - diff --git a/src/msat_smt.odocl b/src/msat_smt.odocl deleted file mode 100644 index ab9aa609..00000000 --- a/src/msat_smt.odocl +++ /dev/null @@ -1,17 +0,0 @@ - -smt/Smt - -# support -smt/Cc -smt/Cnf -smt/Explanation -smt/Expr -smt/ID -smt/Sat -smt/Literal -smt/Mcsat -smt/Symbols -smt/Term -smt/Ty -smt/Unionfind - diff --git a/src/smt/cc.ml b/src/smt/cc.ml deleted file mode 100644 index b0b3f19a..00000000 --- a/src/smt/cc.ml +++ /dev/null @@ -1,515 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -let max_split = 1000000 - -let cc_active = ref true - -type answer = Yes of Explanation.t | No - -module type S = sig - type t - - val empty : unit -> t - val assume : cs:bool -> - Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int - val query : Literal.LT.t -> t -> answer - val class_of : t -> Term.t -> Term.t list -end - -module Make (Dummy : sig end) = struct - - module Ex = Explanation - module Uf = Uf.Make(Term) - module T = Term - module A = Literal - module LR = A.Make(struct type t = X.r include X end) - module SetT = Term.Set - module S = Symbols - - module SetX = Set.Make(struct type t = X.r let compare = X.compare end) - - (* module Uf = Pptarjan.Uf *) - - type env = { - uf : Uf.t ; - relation : X.Rel.t - } - - type choice_sign = - | CPos of int (* The explication of this choice *) - | CNeg (* The choice has been already negated *) - - type t = { - gamma : env; - gamma_finite : env ; - choices : (X.r A.view * Num.num * choice_sign * Ex.t) list; - (** the choice, the size, choice_sign, the explication set, - the explication for this choice. *) - } - - module Print = struct - - let begin_case_split () = () - - let end_case_split () = () - - let cc r1 r2 = () - - let make_cst t ctx = () - - let add_to_use t = () - - let lrepr fmt = List.iter (Format.fprintf fmt "%a " X.print) - - let leaves t lvs = () - - let contra_congruence a ex = () - - let split_size sz = () - - let split_backtrack neg_c ex_c = () - - let split_assume c ex_c = () - - let split_backjump c dep = () - - let assume_literal sa = () - - let congruent a ex = () - - let query a = () - - end - - let bottom = Hstring.make "@bottom" - let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint) - - let concat_leaves uf l = - let rec concat_rec acc t = - match X.leaves (fst (Uf.find uf t)) , acc with - [] , _ -> one::acc - | res, [] -> res - | res , _ -> List.rev_append res acc - in - match List.fold_left concat_rec [] l with - [] -> [one] - | res -> res - - let are_equal env ex t1 t2 = - if T.equal t1 t2 then ex - else match Uf.are_equal env.uf t1 t2 with - | Yes dep -> Ex.union ex dep - | No -> raise Exit - - let equal_only_by_congruence env ex t1 t2 acc = - if T.equal t1 t2 then acc - else - let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in - if X.fully_interpreted f1 then acc - else - let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in - if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then - try - let ex = List.fold_left2 (are_equal env) ex xs1 xs2 in - let a = A.LT.make (A.Eq(t1, t2)) in - Print.congruent a ex; - (LTerm a, ex) :: acc - with Exit -> acc - else acc - - let congruents env t1 s acc ex = - SetT.fold (equal_only_by_congruence env ex t1) s acc - - let fold_find_with_explanation find ex l = - List.fold_left - (fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex) - ([], ex) l - - let view find va ex_a = - match va with - | A.Eq (t1, t2) -> - let r1, ex1 = find t1 in - let r2, ex2 = find t2 in - let ex = Ex.union (Ex.union ex1 ex2) ex_a in - A.Eq(r1, r2), ex - | A.Distinct (b, lt) -> - let lr, ex = fold_find_with_explanation find ex_a lt in - A.Distinct (b, lr), ex - | A.Builtin(b, s, l) -> - let lr, ex = fold_find_with_explanation find ex_a l in - A.Builtin(b, s, List.rev lr), ex - - let term_canonical_view env a ex_a = - view (Uf.find env.uf) (A.LT.view a) ex_a - - let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a - - let new_facts_by_contra_congruence env r bol ex = - match X.term_extract r with - | None -> [] - | Some t1 -> - match T.view t1 with - | {T.f=f1 ; xs=[x]} -> - List.fold_left - (fun acc t2 -> - match T.view t2 with - | {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> - let a = A.LT.make (A.Distinct (false, [x; y])) in - let dist = LTerm a in - begin match Uf.are_distinct env.uf t1 t2 with - | Yes ex' -> - let ex_r = Ex.union ex ex' in - Print.contra_congruence a ex_r; - (dist, ex_r) :: acc - | No -> assert false - end - | _ -> acc - ) [] (Uf.class_of env.uf bol) - | _ -> [] - - let contra_congruence = - let true_,_ = X.make T.true_ in - let false_, _ = X.make T.false_ in - fun env r ex -> - if X.equal (fst (Uf.find_r env.uf r)) true_ then - new_facts_by_contra_congruence env r T.false_ ex - else if X.equal (fst (Uf.find_r env.uf r)) false_ then - new_facts_by_contra_congruence env r T.true_ ex - else [] - - let clean_use = - List.fold_left - (fun env (a, ex) -> - match a with - | LSem _ -> assert false - | LTerm t -> - begin - match A.LT.view t with - | A.Distinct (_, lt) - | A.Builtin (_, _, lt) -> - let lvs = concat_leaves env.uf lt in - List.fold_left - (fun env rx -> - let st, sa = Use.find rx env.use in - let sa = SetA.remove (t, ex) sa in - { env with use = Use.add rx (st,sa) env.use } - ) env lvs - | _ -> assert false - end) - - let rec congruence_closure env r1 r2 ex = - Print.cc r1 r2; - let uf, res = Uf.union env.uf r1 r2 ex in - List.fold_left - (fun (env, l) (p, touched, v) -> - (* we look for use(p) *) - let p_t, p_a = Use.find p env.use in - - (* we compute terms and atoms to consider for congruence *) - let repr_touched = List.map (fun (_,a,_) -> a) touched in - let st_others, sa_others = Use.congr_close_up env.use p repr_touched in - - (* we update use *) - let nuse = Use.up_close_up env.use p v in - Use.print nuse; - - (* we check the congruence of the terms. *) - let env = {env with use=nuse} in - let new_eqs = - SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in - let touched_atoms = - List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched - in - let touched_atoms = SetA.fold (fun (a, ex) acc -> - (LTerm a, ex)::acc) p_a touched_atoms in - let touched_atoms = SetA.fold (fun (a, ex) acc -> - (LTerm a, ex)::acc) sa_others touched_atoms in - env, new_eqs @ touched_atoms - - ) ({env with uf=uf}, []) res - - let replay_atom env sa = - let relation, result = X.Rel.assume env.relation sa in - let env = { env with relation = relation } in - let env = clean_use env result.remove in - env, result.assume - - let rec add_term env choices t ex = - (* nothing to do if the term already exists *) - if Uf.mem env.uf t then env, choices - else begin - Print.add_to_use t; - (* we add t's arguments in env *) - let {T.f = f; xs = xs} = T.view t in - let env, choices = - List.fold_left (fun (env, ch) t -> add_term env ch t ex) - (env, choices) xs - in - (* we update uf and use *) - let nuf, ctx = Uf.add env.uf t in - Print.make_cst t ctx; - let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *) - - if !cc_active then - let lvs = concat_leaves nuf xs in - let nuse = Use.up_add env.use t rt lvs in - - (* If finitetest is used we add the term to the relation *) - let rel = X.Rel.add env.relation rt in - Use.print nuse; - - (* we compute terms to consider for congruence *) - (* we do this only for non-atomic terms with uninterpreted head-symbol *) - let st_uset = Use.congr_add nuse lvs in - - (* we check the congruence of each term *) - let env = {uf = nuf; use = nuse; relation = rel} in - let ct = congruents env t st_uset [] ex in - let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in - assume_literal env choices ct - else - let rel = X.Rel.add env.relation rt in - let env = {env with uf = nuf; relation = rel} in - env, choices - end - - and add env choices a ex = - match A.LT.view a with - | A.Eq (t1, t2) -> - let env, choices = add_term env choices t1 ex in - add_term env choices t2 ex - | A.Distinct (_, lt) - | A.Builtin (_, _, lt) -> - let env, choices = List.fold_left - (fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in - let lvs = concat_leaves env.uf lt in (* A verifier *) - let env = List.fold_left - (fun env rx -> - let st, sa = Use.find rx env.use in - { env with - use = Use.add rx (st,SetA.add (a, ex) sa) env.use } - ) env lvs - in - env, choices - - and semantic_view env choices la = - List.fold_left - (fun (env, choices, lsa) (a, ex) -> - match a with - | LTerm a -> - let env, choices = add env choices a ex in - let sa, ex = term_canonical_view env a ex in - env, choices, (sa, Some a, ex)::lsa - - (* XXX si on fait canonical_view pour - A.Distinct, la theorie des tableaux - part dans les choux *) - | LSem (A.Builtin _ (*| A.Distinct _*) as sa) -> - let sa, ex = canonical_view env sa ex in - env, choices, (sa, None, ex)::lsa - | LSem sa -> - env, choices, (sa, None, ex)::lsa) - (env, choices, []) la - - and assume_literal env choices la = - if la = [] then env, choices - else - let env, choices, lsa = semantic_view env choices la in - let env, choices = - List.fold_left - (fun (env, choices) (sa, _, ex) -> - Print.assume_literal sa; - match sa with - | A.Eq(r1, r2) -> - if !cc_active then - let env, l = congruence_closure env r1 r2 ex in - let env, choices = assume_literal env choices l in - let env, choices = - assume_literal env choices (contra_congruence env r1 ex) - in - assume_literal env choices (contra_congruence env r2 ex) - else - {env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices - | A.Distinct (false, lr) -> - if Uf.already_distinct env.uf lr then env, choices - else - {env with uf = Uf.distinct env.uf lr ex}, choices - | A.Distinct (true, _) -> assert false - | A.Builtin _ -> env, choices) - (env, choices) lsa - in - let env, l = replay_atom env lsa in - assume_literal env (choices@l) l - - let look_for_sat ?(bad_last=No) ch t base_env l = - let rec aux ch bad_last dl base_env li = - match li, bad_last with - | [], _ -> - begin - match X.Rel.case_split base_env.relation with - | [] -> - { t with gamma_finite = base_env; choices = List.rev dl }, ch - | l -> - let l = - List.map - (fun (c, ex_c, size) -> - let exp = Ex.fresh_exp () in - let ex_c_exp = Ex.add_fresh exp ex_c in - (* A new explanation in order to track the choice *) - (c, size, CPos exp, ex_c_exp)) l in - let sz = - List.fold_left - (fun acc (a,s,_,_) -> - Num.mult_num acc s) (Num.Int 1) (l@dl) in - Print.split_size sz; - if Num.le_num sz max_split then aux ch No dl base_env l - else - { t with gamma_finite = base_env; choices = List.rev dl }, ch - end - | ((c, size, CNeg, ex_c) as a)::l, _ -> - let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in - aux ch bad_last (a::dl) base_env l - - (** This optimisation is not correct with the current explanation *) - (* | [(c, size, CPos exp, ex_c)], Yes dep -> *) - (* let neg_c = LR.neg (LR.make c) in *) - (* let ex_c = Ex.union ex_c dep in *) - (* Print.split_backtrack neg_c ex_c; *) - (* aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, ex_c] *) - - | ((c, size, CPos exp, ex_c_exp) as a)::l, _ -> - try - Print.split_assume (LR.make c) ex_c_exp; - let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in - aux ch bad_last (a::dl) base_env l - with Exception.Inconsistent dep -> - match Ex.remove_fresh exp dep with - | None -> - (* The choice doesn't participate to the inconsistency *) - Print.split_backjump (LR.make c) dep; - raise (Exception.Inconsistent dep) - | Some dep -> - (* The choice participates to the inconsistency *) - let neg_c = LR.neg (LR.make c) in - Print.split_backtrack neg_c dep; - aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep] - in - aux ch bad_last (List.rev t.choices) base_env l - - let try_it f t = - Print.begin_case_split (); - let r = - try - if t.choices = [] then look_for_sat [] t t.gamma [] - else - try - let env, lt = f t.gamma_finite in - look_for_sat lt t env [] - with Exception.Inconsistent dep -> - look_for_sat ~bad_last:(Yes dep) - [] { t with choices = []} t.gamma t.choices - with Exception.Inconsistent d -> - Print.end_case_split (); - raise (Exception.Inconsistent d) - in - Print.end_case_split (); r - - let extract_from_semvalues = - List.fold_left - (fun acc r -> - match X.term_extract r with Some t -> SetT.add t acc | _ -> acc) - - let extract_terms_from_choices = - List.fold_left - (fun acc (a, _, _, _) -> - match a with - | A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2] - | A.Distinct (_, l) -> extract_from_semvalues acc l - | _ -> acc) - - let extract_terms_from_assumed = - List.fold_left - (fun acc (a, _) -> - match a with - | LTerm r -> begin - match Literal.LT.view r with - | Literal.Eq (t1, t2) -> - SetT.add t1 (SetT.add t2 acc) - | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> - List.fold_right SetT.add l acc - end - | _ -> acc) - - let assume ~cs a ex t = - let a = LTerm a in - let gamma, ch = assume_literal t.gamma [] [a, ex] in - let t = { t with gamma = gamma } in - let t, ch = - if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t - else t, ch - in - let choices = extract_terms_from_choices SetT.empty t.choices in - let all_terms = extract_terms_from_assumed choices ch in - t, all_terms, 1 - - let class_of t term = Uf.class_of t.gamma.uf term - - let add_and_process a t = - let aux a ex env = - let gamma, l = add env [] a ex in assume_literal gamma [] l - in - let gamma, _ = aux a Ex.empty t.gamma in - let t = { t with gamma = gamma } in - let t, _ = try_it (aux a Ex.empty) t in - Use.print t.gamma.use; t - - let query a t = - Print.query a; - try - match A.LT.view a with - | A.Eq (t1, t2) -> - let t = add_and_process a t in - Uf.are_equal t.gamma.uf t1 t2 - - | A.Distinct (false, [t1; t2]) -> - let na = A.LT.neg a in - let t = add_and_process na t in (* na ? *) - Uf.are_distinct t.gamma.uf t1 t2 - - | A.Distinct _ -> - assert false (* devrait etre capture par une analyse statique *) - - | _ -> - let na = A.LT.neg a in - let t = add_and_process na t in - let env = t.gamma in - let rna, ex_rna = term_canonical_view env na Ex.empty in - X.Rel.query env.relation (rna, Some na, ex_rna) - with Exception.Inconsistent d -> Yes d - - let empty () = - let env = { - use = Use.empty ; - uf = Uf.empty ; - relation = X.Rel.empty (); - } - in - let t = { gamma = env; gamma_finite = env; choices = [] } in - let t, _, _ = - assume ~cs:false - (A.LT.make (A.Distinct (false, [T.true_; T.false_]))) Ex.empty t - in t - -end diff --git a/src/smt/cc.mli b/src/smt/cc.mli deleted file mode 100644 index 935ed2ea..00000000 --- a/src/smt/cc.mli +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Msat - -val cc_active : bool ref - -type answer = Yes of Explanation.t | No - -module type S = sig - type t - - val empty : unit -> t - - val assume : - cs:bool -> - Literal.LT.t -> - Explanation.t -> - t -> t * Term.Set.t * int - - val query : Literal.LT.t -> t -> answer - - val class_of : t -> Term.t -> Term.t list -end - -module Make (Dummy : sig end) : S diff --git a/src/smt/explanation.ml b/src/smt/explanation.ml deleted file mode 100644 index 3646c112..00000000 --- a/src/smt/explanation.ml +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type atom = Literal.LT.t - -type exp = Atom of atom | Fresh of int - -module S = - Set.Make - (struct - type t = exp - let compare a b = match a,b with - | Atom _, Fresh _ -> -1 - | Fresh _, Atom _ -> 1 - | Fresh i1, Fresh i2 -> i1 - i2 - | Atom a, Atom b -> a.aid - b.aid - end) - -type t = S.t - -let singleton e = S.singleton (Atom e) - -let empty = S.empty - -let union s1 s2 = S.union s1 s2 - -let iter_atoms f s = - S.iter (fun e -> match e with - | Fresh _ -> () - | Atom a -> f a) s - -let fold_atoms f s acc = - S.fold (fun e acc -> match e with - | Fresh _ -> acc - | Atom a -> f a acc) s acc - -let merge e1 e2 = e1 - - -let fresh_exp = - let r = ref (-1) in - fun () -> incr r; !r - -let remove_fresh i s = - let fi = Fresh i in - if S.mem fi s then Some (S.remove fi s) - else None - -let add_fresh i = S.add (Fresh i) - - -let print fmt ex = - fprintf fmt "{"; - S.iter (function - | Atom a -> fprintf fmt "%a, " Debug.atom a - | Fresh i -> fprintf fmt "Fresh%d " i) ex; - fprintf fmt "}" diff --git a/src/smt/explanation.mli b/src/smt/explanation.mli deleted file mode 100644 index b362b0c3..00000000 --- a/src/smt/explanation.mli +++ /dev/null @@ -1,39 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type t - -type exp - -type atom = Literal.LT.t - -val empty : t - -val singleton : atom-> t - -val union : t -> t -> t - -val merge : t -> t -> t - -val iter_atoms : (atom -> unit) -> t -> unit - -val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a - -val fresh_exp : unit -> int - -val remove_fresh : int -> t -> t option - -val add_fresh : int -> t -> t - -val print : Format.formatter -> t -> unit diff --git a/src/smt/uf.ml b/src/smt/uf.ml deleted file mode 100644 index 9ee4e98f..00000000 --- a/src/smt/uf.ml +++ /dev/null @@ -1,310 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type answer = Yes of Explanation.t | No - -type 'a literal = - | LSem of 'a Literal.view - | LTerm of Literal.LT.t - -exception Inconsistent of Explanation.t -exception Unsolvable - -module Ex = Explanation -module Sy = Symbols -module T = Term -module MapT = Term.Map -module SetT = Term.Set - -module Lit = Literal.Make(T) -module MapL = Lit.Map - -module MapR = MapT -module SetR = SetT - -module R = struct - include T - type r = t - - let leaves t : r list = match T.head t with - | T.Ite (a, _, _) -> [a] - | T.App (_, l) -> l -end - -type r = R.r - -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 = { - (* term -> [t] *) - make : r MapT.t; - - (* representative table *) - repr : (r * Ex.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; - - (* 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; -} - -module Env = struct - let mem env t = MapT.mem t env.make - - 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_by_r r env = - try MapR.find r env.repr with Not_found -> r, Ex.empty - - let lookup_for_neqs env r = - try MapR.find r env.neqs with Not_found -> MapL.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 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_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) - - (* 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 filter_leaves r = - List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) - - let find_or_normal_form env r = - try MapR.find r env.repr with Not_found -> r, Ex.empty - - 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; - classes = - if in_repr then env.classes - else update_classes p p env.classes; - gamma = - if in_repr then env.gamma - else add_to_gamma p p env.gamma ; - neqs = - 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 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 - - 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] diff --git a/src/smt/uf.mli b/src/smt/uf.mli deleted file mode 100644 index 8205e3ee..00000000 --- a/src/smt/uf.mli +++ /dev/null @@ -1,45 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type answer = Yes of Explanation.t | No - -type 'a literal = - | LSem of 'a Literal.view - | LTerm of Literal.LT.t - -type t - -type r -(** representative *) - -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 * Explanation.t - -val find_r : t -> r -> r * Explanation.t - -val union : - t -> r -> r -> Explanation.t -> - t * (r * (r * r * Explanation.t) list * r) list - -val distinct : t -> 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 list -> bool - -val class_of : t -> Term.t -> Term.t list