From 898cfee53ec5420baf90db7fbe4c6365d3ffee47 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 25 Jun 2015 15:45:18 +0200 Subject: [PATCH] Removed some old, unused legacy code --- TODO.md | 1 - old/.merlin | 8 - old/arith.ml | 435 ------------------------- old/arith.mli | 21 -- old/cc.ml | 524 ------------------------------ old/cc.mli | 29 -- old/combine.ml | 253 --------------- old/combine.mli | 14 - old/exception.ml | 19 -- old/exception.mli | 19 -- old/fm.ml | 806 ---------------------------------------------- old/fm.mli | 23 -- old/intervals.ml | 703 ---------------------------------------- old/intervals.mli | 57 ---- old/literal.ml | 210 ------------ old/literal.mli | 63 ---- old/polynome.ml | 257 --------------- old/polynome.mli | 68 ---- old/sig.mli | 146 --------- old/smt.ml | 790 --------------------------------------------- old/smt.mli | 338 ------------------- old/sum.ml | 240 -------------- old/sum.mli | 25 -- old/symbols.ml | 91 ------ old/symbols.mli | 43 --- old/term.ml | 82 ----- old/term.mli | 36 --- old/ty.ml | 58 ---- old/ty.mli | 24 -- old/uf.ml | 359 --------------------- old/uf.mli | 42 --- old/use.ml | 83 ----- old/use.mli | 38 --- 33 files changed, 5905 deletions(-) delete mode 100644 old/.merlin delete mode 100644 old/arith.ml delete mode 100644 old/arith.mli delete mode 100644 old/cc.ml delete mode 100644 old/cc.mli delete mode 100644 old/combine.ml delete mode 100644 old/combine.mli delete mode 100644 old/exception.ml delete mode 100644 old/exception.mli delete mode 100644 old/fm.ml delete mode 100644 old/fm.mli delete mode 100644 old/intervals.ml delete mode 100644 old/intervals.mli delete mode 100644 old/literal.ml delete mode 100644 old/literal.mli delete mode 100644 old/polynome.ml delete mode 100644 old/polynome.mli delete mode 100644 old/sig.mli delete mode 100644 old/smt.ml delete mode 100644 old/smt.mli delete mode 100644 old/sum.ml delete mode 100644 old/sum.mli delete mode 100644 old/symbols.ml delete mode 100644 old/symbols.mli delete mode 100644 old/term.ml delete mode 100644 old/term.mli delete mode 100644 old/ty.ml delete mode 100644 old/ty.mli delete mode 100644 old/uf.ml delete mode 100644 old/uf.mli delete mode 100644 old/use.ml delete mode 100644 old/use.mli diff --git a/TODO.md b/TODO.md index e070e88a..0d0f0916 100644 --- a/TODO.md +++ b/TODO.md @@ -9,7 +9,6 @@ * react upon propagation (possibly by propagating more, or side-effect) * more advanced/specific propagation (2-clauses)? * implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf ) -- Adapt old code for theories, in order to plug it into new Solver Functor ## Long term goals diff --git a/old/.merlin b/old/.merlin deleted file mode 100644 index daa95b7d..00000000 --- a/old/.merlin +++ /dev/null @@ -1,8 +0,0 @@ -S ./ -S ../sat/ -S ../common/ - -B ../_build/ -B ../_build/sat/ -B ../_build/smt/ -B ../_build/common/ diff --git a/old/arith.ml b/old/arith.ml deleted file mode 100644 index f4e85e3c..00000000 --- a/old/arith.ml +++ /dev/null @@ -1,435 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Francois Bobot, Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Format -open Sig -open Num -module A = Literal -module Sy = Symbols -module T = Term - -let ale = Hstring.make "<=" -let alt = Hstring.make "<" -let is_le n = Hstring.compare n ale = 0 -let is_lt n = Hstring.compare n alt = 0 -let is_mult h = Sy.equal (Sy.Op Sy.Mult) h -let mod_symb = Sy.name (Hstring.make "@mod") - -module Type (X:Sig.X) : Polynome.T with type r = X.r = struct - - let mult _ _ = assert false - - include Polynome.Make(struct include X let mult = mult end) - -end - -module Make - (X : Sig.X) - (P : Polynome.T with type r = X.r) - (C : Sig.C with type t = P.t and type r = X.r) = struct - - type t = P.t - - type r = P.r - - let name = "arith" - - let is_mine_a a = - match A.LT.view a with - | A.Builtin (_,p,_) -> is_le p || is_lt p - | _ -> false - - let is_mine_symb = function - | Sy.Int _ | Sy.Real _ - | Sy.Op (Sy.Plus | Sy.Minus | Sy.Mult | Sy.Div | Sy.Modulo) -> true - | _ -> false - - let is_mine_type p = - let ty = P.type_info p in - ty = Ty.Tint || ty = Ty.Treal - - let unsolvable _ = false - - let empty_polynome ty = P.create [] (Int 0) ty - - let is_mine p = match P.is_monomial p with - | Some (a,x,b) when a =/ (Int 1) && b =/ (Int 0) -> x - | _ -> C.embed p - - let embed r = match C.extract r with - | Some p -> p - | _ -> P.create [Int 1, r] (Int 0) (X.type_info r) - - let check_int exn p = - if P.type_info p = Ty.Tint then - let _, c = P.to_list p in - let ppmc = P.ppmc_denominators p in - if not (is_integer_num (ppmc */ c)) then raise exn - - let fresh_string = - let cpt = ref 0 in - fun () -> - incr cpt; - "!k" ^ (string_of_int !cpt) - - let fresh_name () = - T.make (Sy.name (Hstring.make (fresh_string()))) [] Ty.Tint - - (* t1 % t2 = md <-> - c1. 0 <= md ; - c2. md < t2 ; - c3. exists k. t1 = t2 * k + t ; - c4. t2 <> 0 (already checked) *) - let mk_modulo md t1 t2 ctx = - let zero = T.int "0" in - let c1 = A.LT.make (A.Builtin(true, ale, [zero; md])) in - let c2 = A.LT.make (A.Builtin(true, alt, [md; t2])) in - let k = fresh_name () in - let t3 = T.make (Sy.Op Sy.Mult) [t2;k] Ty.Tint in - let t3 = T.make (Sy.Op Sy.Plus) [t3;md] Ty.Tint in - let c3 = A.LT.make (A.Eq (t1, t3)) in - c3 :: c2 :: c1 :: ctx - - let mk_euc_division p p2 t1 t2 ctx = - match P.to_list p2 with - | [], coef_p2 -> - let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in - let r, ctx' = X.make md in - let rp = P.mult (P.create [] ((Int 1) //coef_p2) Ty.Tint) (embed r) in - P.sub p rp, ctx' @ ctx - | _ -> assert false - - let rec mke coef p t ctx = - let {T.f = sb ; xs = xs; ty = ty} = T.view t in - match sb, xs with - | (Sy.Int n | Sy.Real n), _ -> - let c = coef */ (num_of_string (Hstring.view n)) in - P.add (P.create [] c ty) p, ctx - - | Sy.Op Sy.Mult, [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - P.add p (P.mult p1 p2), ctx - - | Sy.Op Sy.Div, [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - let p3, ctx = - try - let p, approx = P.div p1 p2 in - if approx then mk_euc_division p p2 t1 t2 ctx - else p, ctx - with Division_by_zero | Polynome.Maybe_zero -> - P.create [coef, X.term_embed t] (Int 0) ty, ctx - in - P.add p p3, ctx - - | Sy.Op Sy.Plus , [t1;t2] -> - let p2, ctx = mke coef p t2 ctx in - mke coef p2 t1 ctx - - | Sy.Op Sy.Minus , [t1;t2] -> - let p2, ctx = mke (minus_num coef) p t2 ctx in - mke coef p2 t1 ctx - - | Sy.Op Sy.Modulo , [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - let p3, ctx = - try P.modulo p1 p2, ctx - with e -> - let t = T.make mod_symb [t1; t2] Ty.Tint in - let ctx = match e with - | Division_by_zero | Polynome.Maybe_zero -> ctx - | Polynome.Not_a_num -> mk_modulo t t1 t2 ctx - | _ -> assert false - in - P.create [coef, X.term_embed t] (Int 0) ty, ctx - in - P.add p p3, ctx - - | _ -> - let a, ctx' = X.make t in - let ctx = ctx' @ ctx in - match C.extract a with - | Some p' -> P.add p (P.mult (P.create [] coef ty) p'), ctx - | _ -> P.add p (P.create [coef, a] (Int 0) ty), ctx - - let arith_to_ac p = p -(* - match P.to_list p with - | [] , c -> p - | [Int 1, x] , Int 0 -> p - | l , c -> - let ty = P.type_info p in - let l = - List.fold_left - (fun acc (coef,x) -> - if coef =/ Int 0 then acc - else if coef =/ Int 1 || coef =/ Int (-1) then (coef,x)::acc - else match X.ac_extract x with - | Some ac when is_mult ac.h -> - let unit_coef, abs_coef = - if coef > Int 0 then Int 1, coef - else Int (-1), minus_num coef - in - let p_cst = is_mine (P.create [] abs_coef ty) in - let ac = {ac with l = Ac.add ac.h (p_cst, 1) ac.l} in - (unit_coef, X.ac_embed ac)::acc - | _ -> (coef,x)::acc - )[] l - in - P.create l c ty -*) - let make t = - let {T.ty = ty} = T.view t in - let p, ctx = mke (Int 1) (empty_polynome ty) t [] in - is_mine (arith_to_ac p), ctx - - let rec expand p n acc = - assert (n >=0); - if n = 0 then acc else expand p (n-1) (p::acc) - - let rec number_of_vars l = - List.fold_left (fun acc (r, n) -> acc + n * nb_vars_in_alien r) 0 l - - and nb_vars_in_alien r = - match C.extract r with - | Some p -> - let l, _ = P.to_list p in - List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l - | None -> 1 - - let max_list_ = function - | [] -> 0 - | [ _, x ] -> nb_vars_in_alien x - | (_, x) :: l -> - let acc = nb_vars_in_alien x in - List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l - - let type_info p = P.type_info p - - let is_int r = X.type_info r = Ty.Tint - - module XS = Set.Make(struct type t = X.r let compare = X.compare end) - - let xs_of_list = - List.fold_left (fun s x -> XS.add x s) XS.empty - - let rec leaves p = - let s = - List.fold_left - (fun s (_, a) -> XS.union (xs_of_list (X.leaves a)) s) - XS.empty (fst (P.to_list p)) - in - XS.elements s - - let subst x t p = - let p = P.subst x (embed t) p in - let ty = P.type_info p in - let l, c = P.to_list p in - let p = - List.fold_left - (fun p (ai, xi) -> - let xi' = X.subst x t xi in - let p' = match C.extract xi' with - | Some p' -> P.mult (P.create [] ai ty) p' - | _ -> P.create [ai, xi'] (Int 0) ty - in - P.add p p') - (P.create [] c ty) l - in - check_int (Exception.Unsolvable) p; - is_mine p - - - let compare = P.compare - - let hash = P.hash - - (* symmetric modulo p 131 *) - let mod_sym a b = - let m = mod_num a b in - let m = - if m =/ minus_num b then m +/ b else assert false - else - if m <=/ b then m else assert false - - in - if m - let a = f a in if a =/ Int 0 then acc else (a, x) :: acc) - [ax] l - - let apply_subst sb v = - is_mine (List.fold_left (fun v (x, p) -> embed (subst x p v)) v sb) - - (* substituer toutes variables plus grandes que x *) - let subst_bigger x l = - List.fold_left - (fun (l, sb) (b, y) -> - if X.compare y x > 0 then - let k = X.term_embed (fresh_name ()) in - (b, k) :: l, (y, embed k)::sb - else (b, y) :: l, sb) - ([], []) l - - let is_mine_p = List.map (fun (x,p) -> x, is_mine p) - - let extract_min = function - | [] -> assert false - | [c] -> c, [] - | (a, x) :: s -> - List.fold_left - (fun ((a, x), l) (b, y) -> - if abs_num a <=/ abs_num b then - (a, x), ((b, y) :: l) - else (b, y), ((a, x):: l)) ((a, x),[]) s - - - (* Decision Procedures. Page 131 *) - let rec omega l b = - - (* 1. choix d'une variable donc le |coef| est minimal *) - let (a, x), l = extract_min l in - - (* 2. substituer les aliens plus grand que x pour - assurer l'invariant sur l'ordre AC *) - let l, sbs = subst_bigger x l in - let p = P.create l b Ty.Tint in - match a with - | Int 0 -> assert false - | Int 1 -> - (* 3.1. si a = 1 alors on a une substitution entiere pour x *) - let p = mult_const p (Int (-1)) in - (x, is_mine p) :: (is_mine_p sbs) - - | Int (-1) -> - (* 3.2. si a = -1 alors on a une subst entiere pour x*) - (x,is_mine p) :: (is_mine_p sbs) - | _ -> - (* 4. sinon, (|a| <> 1) et a <> 0 *) - (* 4.1. on rend le coef a positif s'il ne l'est pas deja *) - let a, l, b = - if compare_num a (Int 0) < 0 then - (minus_num a, - List.map (fun (a,x) -> minus_num a,x) l, (minus_num b)) - else (a, l, b) - in - (* 4.2. on reduit le systeme *) - omega_sigma sbs a x l b - - and omega_sigma sbs a x l b = - - (* 1. on definie m qui vaut a + 1 *) - let m = a +/ Int 1 in - - (* 2. on introduit une variable fraiche *) - let sigma = X.term_embed (fresh_name ()) in - - (* 3. l'application de la formule (5.63) nous donne la valeur du pivot x*) - let mm_sigma = (minus_num m, sigma) in - let l_mod = map_monomes (fun a -> mod_sym a m) l mm_sigma in - - (* 3.1. Attention au signe de b : - on le passe a droite avant de faire mod_sym, d'ou minus_num *) - let b_mod = minus_num (mod_sym (minus_num b) m) in - let p = P.create l_mod b_mod Ty.Tint in - - let sbs = (x, p) :: sbs in - - (* 4. on substitue x par sa valeur dans l'equation de depart. - Voir la formule (5.64) *) - let p' = P.add (P.mult_const a p) (P.create l b Ty.Tint) in - - (* 5. on resoud sur l'equation simplifiee *) - let sbs2 = solve_int p' in - - (* 6. on normalise sbs par sbs2 *) - let sbs = List.map (fun (x, v) -> x, apply_subst sbs2 v) sbs in - - (* 7. on supprime les liaisons inutiles de sbs2 et on merge avec sbs *) - let sbs2 = List.filter (fun (y, _) -> y <> sigma) sbs2 in - List.rev_append sbs sbs2 - - and solve_int p = - if P.is_empty p then raise Not_found; - let pgcd = P.pgcd_numerators p in - let ppmc = P.ppmc_denominators p in - let p = mult_const p (ppmc // pgcd) in - let l, b = P.to_list p in - if not (is_integer_num b) then raise Exception.Unsolvable; - omega l b - - let is_null p = - if snd (P.to_list p) <>/ (Int 0) then raise Exception.Unsolvable; - [] - - let solve_int p = - try solve_int p with Not_found -> is_null p - - let solve_real p = - try - let a, x = P.choose p in - let p = - P.mult - (P.create [] ((Int (-1)) // a) (P.type_info p)) - (P.remove x p) - in - [x, is_mine p] - with Not_found -> is_null p - - let safe_distribution p = - let l, c = P.to_list p in - let ty = P.type_info p in - List.fold_left - (fun p (coef, x) -> P.add p (P.create [coef,x] (Int 0) ty)) - (P.create [] c ty) l - - let solve_aux r1 r2 = - let p1 = embed r1 in - let p2 = embed r2 in - let ty = P.type_info p2 in - let p = P.add p1 (P.mult (P.create [] (Int (-1)) ty) p2) in - let pp = safe_distribution p in - if ty = Ty.Treal then solve_real pp else solve_int pp - - let solve r1 r2 = - let sbs = solve_aux r1 r2 in - List.fast_sort (fun (a,_) (x,y) -> X.compare x a) sbs - - let print = P.print - - let fully_interpreted sb = - match sb with - | Sy.Op (Sy.Plus | Sy.Minus) -> true - | _ -> false - - let term_extract _ = None - - module Rel = Fm.Make (X) - (struct - include P - let poly_of = embed - let alien_of = is_mine - end) - -end diff --git a/old/arith.mli b/old/arith.mli deleted file mode 100644 index 10afffe4..00000000 --- a/old/arith.mli +++ /dev/null @@ -1,21 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Francois Bobot, Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module Type (X : Sig.X ): Polynome.T with type r = X.r - -module Make - (X : Sig.X) - (P : Polynome.T with type r = X.r) - (C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY - with type r = X.r and type t = P.t diff --git a/old/cc.ml b/old/cc.ml deleted file mode 100644 index 192c2acd..00000000 --- a/old/cc.ml +++ /dev/null @@ -1,524 +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 Format -open Sig -open Exception - -let max_split = Num.Int 1000000 - -let cc_active = ref true - -module type S = sig - type t - - module TimerCC : Timer.S - - 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 (X : Sig.X) = struct - - module TimerCC = Timer.Make(struct end) - - module Ex = Explanation - module SetA = Use.SA - module Use = Use.Make(X) - module Uf = Uf.Make(X) - 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 = { - use : Use.t; - 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 (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/old/cc.mli b/old/cc.mli deleted file mode 100644 index 50ddb980..00000000 --- a/old/cc.mli +++ /dev/null @@ -1,29 +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 *) -(* *) -(**************************************************************************) - -val cc_active : bool ref - -module type S = sig - type t - - module TimerCC : Timer.S - - 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 -> Sig.answer - val class_of : t -> Term.t -> Term.t list -end - -module Make (X:Sig.X) : S diff --git a/old/combine.ml b/old/combine.ml deleted file mode 100644 index c75664ce..00000000 --- a/old/combine.ml +++ /dev/null @@ -1,253 +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 Format -open Sig - -module rec CX : sig - include Sig.X - - val extract1 : r -> X1.t option - val embed1 : X1.t -> r - - val extract5 : r -> X5.t option - val embed5 : X5.t -> r - -end = -struct - - type r = - | Term of Term.t - | X1 of X1.t - | X5 of X5.t - - let extract1 = function X1 r -> Some r | _ -> None - let extract5 = function X5 r -> Some r | _ -> None - - let embed1 x = X1 x - let embed5 x = X5 x - - let is_int v = - let ty = match v with - | X1 x -> X1.type_info x - | X5 x -> X5.type_info x - | Term t -> (Term.view t).Term.ty - in - ty = Ty.Tint - - let rec compare a b = - let c = compare_tag a b in - if c = 0 then comparei a b else c - - and compare_tag a b = - Pervasives.compare (theory_num a) (theory_num b) - - and comparei a b = - match a, b with - | X1 x, X1 y -> X1.compare x y - | X5 x, X5 y -> X5.compare x y - | Term x , Term y -> Term.compare x y - | _ -> assert false - - and theory_num x = Obj.tag (Obj.repr x) - - let equal a b = compare a b = 0 - - let hash = function - | Term t -> Term.hash t - | X1 x -> X1.hash x - | X5 x -> X5.hash x - - module MR = Map.Make(struct type t = r let compare = compare end) - - let print fmt r = - match r with - | X1 t -> fprintf fmt "%a" X1.print t - | X5 t -> fprintf fmt "%a" X5.print t - | Term t -> fprintf fmt "%a" Term.print t - - let leaves r = - match r with - | X1 t -> X1.leaves t - | X5 t -> X5.leaves t - | Term _ -> [r] - - let term_embed t = Term t - - let term_extract r = - match r with - | X1 _ -> X1.term_extract r - | X5 _ -> X5.term_extract r - | Term t -> Some t - - let subst p v r = - if equal p v then r - else match r with - | X1 t -> X1.subst p v t - | X5 t -> X5.subst p v t - | Term _ -> if equal p r then v else r - - let make t = - let {Term.f=sb} = Term.view t in - match X1.is_mine_symb sb, X5.is_mine_symb sb with - | true, false -> X1.make t - | false, true -> X5.make t - | false, false -> Term t, [] - | _ -> assert false - - let fully_interpreted sb = - match X1.is_mine_symb sb, X5.is_mine_symb sb with - | true, false -> X1.fully_interpreted sb - | false, true -> X5.fully_interpreted sb - | false, false -> false - | _ -> assert false - - let add_mr = - List.fold_left - (fun solved (p,v) -> - MR.add p (v::(try MR.find p solved with Not_found -> [])) solved) - - let unsolvable = function - | X1 x -> X1.unsolvable x - | X5 x -> X5.unsolvable x - | Term _ -> true - - let partition tag = - List.partition - (fun (u,t) -> - (theory_num u = tag || unsolvable u) && - (theory_num t = tag || unsolvable t)) - - let rec solve_list solved l = - List.fold_left - (fun solved (a,b) -> - let cmp = compare a b in - if cmp = 0 then solved else - match a , b with - (* both sides are empty *) - | Term _ , Term _ -> - add_mr solved (unsolvable_values cmp a b) - - (* only one side is empty *) - | (a, b) - when unsolvable a || unsolvable b || compare_tag a b = 0 -> - let a,b = if unsolvable a then b,a else a,b in - let cp , sol = partition (theory_num a) (solvei b a) in - solve_list (add_mr solved cp) sol - - (* both sides are not empty *) - | a , b -> solve_theoryj solved a b - ) solved l - - and unsolvable_values cmp a b = - match a, b with - (* Clash entre theories: On peut avoir ces pbs ? *) - | X1 _, X5 _ - | X5 _, X1 _ - -> assert false - - (* theorie d'un cote, vide de l'autre *) - | X1 _, _ | _, X1 _ -> X1.solve a b - | X5 _, _ | _, X5 _ -> X5.solve a b - | Term _, Term _ -> [if cmp > 0 then a,b else b,a] - - and solve_theoryj solved xi xj = - let cp , sol = partition (theory_num xj) (solvei xi xj) in - solve_list (add_mr solved cp) (List.rev_map (fun (x,y) -> y,x) sol) - - and solvei a b = - match b with - | X1 _ -> X1.solve a b - | X5 _ -> X5.solve a b - | Term _ -> assert false - - let rec solve_rec mt ab = - let mr = solve_list mt ab in - let mr , ab = - MR.fold - (fun p lr ((mt,ab) as acc) -> match lr with - [] -> assert false - | [_] -> acc - | x::lx -> - MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx) - mr (mr,[]) - in - if ab = [] then mr else solve_rec mr ab - - let solve a b = - MR.fold - (fun p lr ret -> - match lr with [r] -> (p ,r)::ret | _ -> assert false) - (solve_rec MR.empty [a,b]) [] - - let rec type_info = function - | X1 t -> X1.type_info t - | X5 t -> X5.type_info t - | Term t -> let {Term.ty = ty} = Term.view t in ty - - module Rel = struct - type elt = r - type r = elt - - type t = { - r1: X1.Rel.t; - r5: X5.Rel.t; - } - - let empty _ = { - r1=X1.Rel.empty (); - r5=X5.Rel.empty (); - } - - let assume env sa = - let env1, { assume = a1; remove = rm1} = X1.Rel.assume env.r1 sa in - let env5, { assume = a5; remove = rm5} = X5.Rel.assume env.r5 sa in - {r1=env1; r5=env5}, - { assume = a1@a5; remove = rm1@rm5;} - - let query env a = - match X1.Rel.query env.r1 a with - | Yes _ as ans -> ans - | No -> X5.Rel.query env.r5 a - - let case_split env = - let seq1 = X1.Rel.case_split env.r1 in - let seq5 = X5.Rel.case_split env.r5 in - seq1 @ seq5 - - let add env r = - {r1=X1.Rel.add env.r1 r; - r5=X5.Rel.add env.r5 r } - end - -end - -and TX1 : Polynome.T with type r = CX.r = Arith.Type(CX) - -and X1 : Sig.THEORY with type t = TX1.t and type r = CX.r = - Arith.Make(CX)(TX1) - (struct - type t = TX1.t - type r = CX.r - let extract = CX.extract1 - let embed = CX.embed1 - let assume env _ _ = env, {Sig.assume = []; remove = []} - end) - -and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract = - Sum.Make - (struct - include CX - let extract = extract5 - let embed = embed5 - end) diff --git a/old/combine.mli b/old/combine.mli deleted file mode 100644 index 8570a377..00000000 --- a/old/combine.mli +++ /dev/null @@ -1,14 +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 *) -(* *) -(**************************************************************************) - -module CX : Sig.X diff --git a/old/exception.ml b/old/exception.ml deleted file mode 100644 index b0a38d72..00000000 --- a/old/exception.ml +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -exception Unsolvable -exception Inconsistent of Explanation.t -exception Progress -exception NotCongruent -exception Trivial -exception Interpreted_Symbol diff --git a/old/exception.mli b/old/exception.mli deleted file mode 100644 index b0a38d72..00000000 --- a/old/exception.mli +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -exception Unsolvable -exception Inconsistent of Explanation.t -exception Progress -exception NotCongruent -exception Trivial -exception Interpreted_Symbol diff --git a/old/fm.ml b/old/fm.ml deleted file mode 100644 index 19d778a0..00000000 --- a/old/fm.ml +++ /dev/null @@ -1,806 +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 Num -open Format -open Sig - -let ale = Hstring.make "<=" -let alt = Hstring.make "<" -let is_le n = Hstring.compare n ale = 0 -let is_lt n = Hstring.compare n alt = 0 - -let (-@) l1 l2 = List.rev_append l1 l2 - -module L = Literal -module Sy = Symbols - -exception NotConsistent of Literal.LT.Set.t - -module type EXTENDED_Polynome = sig - include Polynome.T - val poly_of : r -> t - val alien_of : t -> r -end - -module Make - (X : Sig.X) - (P : EXTENDED_Polynome with type r = X.r) = struct - - module MP = Map.Make(P) - module SP = Set.Make(P) - module SX = Set.Make(struct type t = X.r include X end) - module MX = Map.Make(struct type t = X.r include X end) - - type r = P.r - - module LR = Literal.Make(struct type t = X.r include X end) - - module Seq = - Set.Make - (struct - type t = r L.view * L.LT.t option * Explanation.t - let compare (a, _, _) (b, _, _) = - LR.compare (LR.make a) (LR.make b) - end) - - module Inequation = struct - type t = { - ple0 : P.t; - is_le : bool; - dep : (Literal.LT.t * num * P.t * bool) list; - expl : Explanation.t - } - - let print fmt ineq = fprintf fmt "%a %s 0" P.print ineq.ple0 - (if ineq.is_le then "<=" else "<") - - let create p1 p2 is_le a expl = - let p = P.add p1 (P.mult (P.create [] (Int (-1)) (P.type_info p1)) p2) in - { ple0 = p; is_le = is_le; dep = [a, Int 1, p, is_le]; expl = expl } - - let choose ineq = snd (P.choose ineq.ple0) - - let find x ineq = P.find x ineq.ple0 - - let is_monomial ineq = P.is_monomial ineq.ple0 - - let pos_neg mx { ple0 = p } = - List.fold_left (fun m (c,x) -> - let cmp = compare_num c (Int 0) in - if cmp = 0 then m - else - let (pos, neg) = try MX.find x m with Not_found -> (0,0) in - if cmp > 0 then MX.add x (pos+1, neg) m - else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p)) - - end - - type t = { - inequations : (Literal.LT.t * Inequation.t) list ; - monomes: (Intervals.t * SX.t) MX.t; - polynomes : Intervals.t MP.t; - known_eqs : SX.t; - improved : SP.t; - } - - module Debug = struct - - let list_of_ineqs fmt = List.iter (fprintf fmt "%a " Inequation.print) - - let assume a = () - - let cross x cpos cneg others ninqs = () - - let print_use fmt use = - SX.iter (fprintf fmt "%a, " X.print) use - - let env env = () - - let implied_equalities l = () - end - - let empty _ = { - inequations = [] ; - monomes = MX.empty ; - polynomes = MP.empty ; - known_eqs = SX.empty ; - improved = SP.empty ; - } - - let replace_inequation env x ineq = - { env with - inequations = (x, ineq)::(List.remove_assoc x env.inequations) } - - - let up_improved env p oldi newi = - if Intervals.is_strict_smaller newi oldi then - { env with improved = SP.add p env.improved } - else env - -(* - let oldify_inequations env = - { env with - inequations = env.inequations@env.new_inequations; - new_inequations = [] } *) - - let mult_bornes_vars vars monomes ty= - List.fold_left - (fun ui (y,n) -> - let ui' = try - fst (MX.find y monomes) - with Not_found -> Intervals.undefined ty - in - Intervals.mult ui (Intervals.power n ui') - ) (Intervals.point (Int 1) ty Explanation.empty) vars - - - let intervals_from_monomes env p = - let pl, v = P.to_list p in - List.fold_left - (fun i (a, x) -> - let i_x, _ = MX.find x env.monomes in - Intervals.add (Intervals.scale a i_x) i - ) (Intervals.point v (P.type_info p) Explanation.empty) pl - - let rec add_monome expl use_x env x = - try - let u, old_use_x = MX.find x env.monomes in - { env with monomes = MX.add x (u, SX.union old_use_x use_x) env.monomes } - with Not_found -> - update_monome expl use_x env x - - and init_monomes env p use_p expl = - List.fold_left - (fun env (_, x) -> add_monome expl use_p env x) - env (fst (P.to_list p)) - - and init_alien expl p (normal_p, c, d) ty use_x env = - let env = init_monomes env p use_x expl in - let i = intervals_from_monomes env p in - let i = - try - let old_i = MP.find normal_p env.polynomes in - let old_i = Intervals.scale d - (Intervals.add old_i (Intervals.point c ty Explanation.empty)) in - Intervals.intersect i old_i - with Not_found -> i - in - env, i - - - - and update_monome expl use_x env x = - let ty = X.type_info x in - let ui, env = - match X.term_extract x with - | Some t -> - let use_x = SX.singleton x in - begin - match Term.view t with - | {Term.f = (Sy.Op Sy.Div); xs = [a; b]} -> - let pa = P.poly_of (fst (X.make a)) in - let pb = P.poly_of (fst (X.make b)) in - let (pa', ca, da) as npa = P.normal_form_pos pa in - let (pb', cb, db) as npb = P.normal_form_pos pb in - let env, ia = init_alien expl pa npa ty use_x env in - let env, ib = init_alien expl pb npb ty use_x env in - let ia, ib = match Intervals.doesnt_contain_0 ib with - | Yes ex when Num.compare_num ca cb = 0 - && P.compare pa' pb' = 0 -> - let expl = Explanation.union ex expl in - Intervals.point da ty expl, Intervals.point db ty expl - | _ -> ia, ib - in - Intervals.div ia ib, env - | _ -> Intervals.undefined ty, env - end - | _ -> Intervals.undefined ty, env - in - let u, use_x' = - try MX.find x env.monomes - with Not_found -> Intervals.undefined (X.type_info x), use_x in - let ui = Intervals.intersect ui u in - { env with monomes = MX.add x (ui, (SX.union use_x use_x')) env.monomes } - - and tighten_div x env expl = env - - and tighten_non_lin x use_x env expl = - let env = tighten_div x env expl in - SX.fold - (fun x acc -> - let _, use = MX.find x acc.monomes in - update_monome expl use acc x) - use_x env - - let update_monomes_from_poly p i polynomes monomes = - let lp, _ = P.to_list p in - let ty = P.type_info p in - List.fold_left (fun monomes (a,x) -> - let np = P.remove x p in - let (np,c,d) = P.normal_form_pos np in - try - let inp = MP.find np polynomes in - let new_ix = - Intervals.scale - ((Int 1) // a) - (Intervals.add i - (Intervals.scale (minus_num d) - (Intervals.add inp - (Intervals.point c ty Explanation.empty)))) in - let old_ix, ux = MX.find x monomes in - let ix = Intervals.intersect old_ix new_ix in - MX.add x (ix, ux) monomes - with Not_found -> monomes) - monomes lp - - let update_polynomes env expl = - let polynomes, monomes, improved = MP.fold - (fun p ip (polynomes, monomes, improved) -> - let new_i = intervals_from_monomes env p in - let i = Intervals.intersect new_i ip in - if Intervals.is_strict_smaller i ip then - let monomes = update_monomes_from_poly p i polynomes monomes in - let improved = SP.add p improved in - MP.add p i polynomes, monomes, improved - else polynomes, monomes, improved - ) env.polynomes (env.polynomes, env.monomes, env.improved) in - {env with polynomes = polynomes; monomes = monomes ; improved = improved} - - - let find_one_eq x u = - match Intervals.is_point u with - | Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v -> - let eq = - L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in - Some (eq, None, ex) - | _ -> None - - let find_eq eqs x u env = - match find_one_eq x u with - | None -> eqs - | Some eq1 -> eq1::eqs - - type ineq_status = - | Trivial_eq - | Trivial_ineq of num - | Bottom - | Monome of num * P.r * num - | Other - - let ineq_status ({Inequation.ple0 = p ; is_le = is_le} as ineq) = - match Inequation.is_monomial ineq with - Some (a, x, v) -> Monome (a, x, v) - | None -> - if P.is_empty p then - let _, v = P.to_list p in - let c = compare_num v (Int 0) in - if c > 0 || (c >=0 && not is_le) then Bottom - else - if c = 0 && is_le then Trivial_eq - else Trivial_ineq v - else Other - - (*let ineqs_from_dep dep borne_inf is_le = - List.map - (fun {poly_orig = p; coef = c} -> - let (m,v,ty) = P.mult_const minusone p in - (* quelle valeur pour le ?????? *) - { ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ; - dep = []} - )dep*) - - let mk_equality p = - let r1 = P.alien_of p in - let r2 = P.alien_of (P.create [] (Int 0) (P.type_info p)) in - L.Eq (r1, r2) - - let fm_equalities env eqs { Inequation.ple0 = p; dep = dep; expl = ex } = - let inqs, eqs = - List.fold_left - (fun (inqs, eqs) (a, _, p, _) -> - List.remove_assoc a inqs, (mk_equality p, Some a, ex) :: eqs - ) (env.inequations, eqs) dep - in - { env with inequations = inqs }, eqs - - let update_intervals env eqs expl (a, x, v) is_le = - let uints, use_x = MX.find x env.monomes in - let b = ((Int (-1)) */ v) // a in - let u = - if a >/ (Int 0) then - Intervals.new_borne_sup expl b is_le uints - else - Intervals.new_borne_inf expl b is_le uints in - let env = { env with monomes = MX.add x (u, use_x) env.monomes } in - let env = tighten_non_lin x use_x env expl in - env, (find_eq eqs x u env) - - let update_ple0 env p0 is_le expl = - if P.is_empty p0 then env - else - let ty = P.type_info p0 in - let a, _ = P.choose p0 in - let p, change = - if a u, Intervals.undefined ty - in - let env = - if Intervals.is_strict_smaller u pu then - let polynomes = MP.add p u env.polynomes in - let monomes = update_monomes_from_poly p u polynomes env.monomes in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved } - else env - in - match P.to_list p0 with - | [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le) - | _ -> env - - let add_inequations acc lin expl = - List.fold_left - (fun (env, eqs) ineq -> - (* let expl = List.fold_left - (fun expl (l,_,_,_) -> - Explanation.union (*Explanation.everything*) - (Explanation.singleton (Formula.mk_lit l)) - expl - ) expl ineq.Inequation.dep - in *) - let expl = Explanation.union ineq.Inequation.expl expl in - match ineq_status ineq with - | Bottom -> - raise (Exception.Inconsistent expl) - - | Trivial_eq -> - fm_equalities env eqs ineq - - | Trivial_ineq c -> - let n, pp = - List.fold_left - (fun ((n, pp) as acc) (_, _, p, is_le) -> - if is_le then acc else - match pp with - | Some _ -> n+1, None - | None when n=0 -> 1, Some p - | _ -> n+1, None) (0,None) ineq.Inequation.dep - in - let env = - List.fold_left - (fun env (_, coef, p, is_le) -> - let ty = P.type_info p in - let is_le = - match pp with - Some x -> P.compare x p = 0 | _ -> is_le && n=0 - in - let p' = P.sub (P.create [] (c // coef) ty) p in - update_ple0 env p' is_le expl - ) env ineq.Inequation.dep - in - env, eqs - - | Monome (a, x, v) -> - let env, eqs = - update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le - in - - (*let env,eqs = update_bornes env eqs ((a,x),c) ineq.ple0.le in - let env,eqs = update_polynomes env eqs ineq in - env, pers_ineqs, eqs*) - env, eqs - - | Other -> - env, eqs - (*t env,eqs = update_polynomes env eqs ineq in - env, pers_ineqs, eqs*) - - - ) acc lin - - let mult_list c = - List.map (fun (a, coef, p, is_le) -> (a, coef */ c, p, is_le)) - - let div_by_pgcd (a, b) ty = - try - if ty = Ty.Tint then - let p = Big_int.gcd_big_int (big_int_of_num a) (big_int_of_num b) in - let p = num_of_big_int p in - a // p, b // p - else a, b - with Failure "big_int_of_ratio" -> a, b - - let cross x cpos cneg = - let rec cross_rec acc = function - | [] -> acc - | { Inequation.ple0 = p1; is_le = k1; dep = d1; expl = ex1 } :: l -> - let n1 = abs_num (P.find x p1) in - (* let ty = P.type_info p1 in *) - let acc = - List.fold_left - (fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} -> - let n2 = abs_num (P.find x p2) in - (* let n1, n2 = div_by_pgcd (n1, n2) ty in *) - let p = P.add - (P.mult (P.create [] n2 (P.type_info p2)) p1) - (P.mult (P.create [] n1 (P.type_info p1)) p2) in - let d1 = mult_list n2 d1 in - let d2 = mult_list n1 d2 in - let ni = - { Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2; - expl = Explanation.union ex1 ex2 } - in - ni::acc - ) acc cpos - in - cross_rec acc l - in - cross_rec [] cneg - - let split x l = - let rec split_rec (cp, cn, co) ineq = - try - let a = Inequation.find x ineq in - if a >/ (Int 0) then ineq::cp, cn, co - else cp, ineq::cn, co - with Not_found -> cp, cn, ineq::co - in - List.fold_left split_rec ([], [], []) l - - let length s = SX.fold (fun _ acc -> acc+1) s 0 - - let choose_var l = - let pos_neg = List.fold_left Inequation.pos_neg MX.empty l in - let xopt = MX.fold (fun x (pos, neg) acc -> - match acc with - | None -> Some (x, pos * neg) - | Some (y, c') -> - let c = pos * neg in - if c < c' then Some (x, c) else acc - ) pos_neg None in - match xopt with - | Some (x, _) -> x - | None -> raise Not_found - - let rec fourier ( (env, eqs) as acc) l expl = - match l with - | [] -> acc - | ineq :: l' -> - try - (* let x = Inequation.choose ineq in *) - let x = choose_var l in - let cpos, cneg, others = split x l in - let ninqs = cross x cpos cneg in - Debug.cross x cpos cneg others ninqs; - let acc = add_inequations acc cpos expl in - let acc = add_inequations acc cneg expl in - fourier acc (ninqs -@ others) expl - with Not_found -> add_inequations acc l expl - - (* - let fm env eqs expl = - fourier (env, eqs) - (List.map snd env.inequations) - (List.map snd env.new_inequations) expl -*) - - let fm env eqs expl = - fourier (env, eqs) (List.map snd env.inequations) expl - - let is_num r = - let ty = X.type_info r in ty = Ty.Tint || ty = Ty.Treal - - let add_disequality env eqs p expl = - let ty = P.type_info p in - match P.to_list p with - | ([], (Int 0)) -> - raise (Exception.Inconsistent expl) - | ([], v) -> - env, eqs - | ([a, x], v) -> - let b = (minus_num v) // a in - let i1 = Intervals.point b ty expl in - let i2, use2 = - try - MX.find x env.monomes - with Not_found -> Intervals.undefined ty, SX.empty - in - let i = Intervals.exclude i1 i2 in - let env ={ env with monomes = MX.add x (i,use2) env.monomes } in - let env = tighten_non_lin x use2 env expl in - env, find_eq eqs x i env - | _ -> - let a, _ = P.choose p in - let p = if a >=/ Int 0 then p - else P.mult (P.create [] (Int (-1)) ty) p in - let p, c, _ = P.normal_form p in - let i1 = Intervals.point (minus_num c) ty expl in - let i2 = - try - MP.find p env.polynomes - with Not_found -> Intervals.undefined ty - in - let i = Intervals.exclude i1 i2 in - let env = - if Intervals.is_strict_smaller i i2 then - let polynomes = MP.add p i env.polynomes in - let monomes = update_monomes_from_poly p i polynomes env.monomes - in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved} - else env - in - env, eqs - - let add_equality env eqs p expl = - let ty = P.type_info p in - match P.to_list p with - | ([], Int 0) -> env, eqs - | ([], v) -> - raise (Exception.Inconsistent expl) - | ([a, x], v) -> - let b = (minus_num v) // a in - let i = Intervals.point b ty expl in - let i, use = - try - let i', use' = MX.find x env.monomes in - Intervals.intersect i i', use' - with Not_found -> i, SX.empty - in - let env = { env with monomes = MX.add x (i, use) env.monomes} in - let env = tighten_non_lin x use env expl in - env, find_eq eqs x i env - | _ -> - let a, _ = P.choose p in - let p = if a >=/ Int 0 then p - else P.mult (P.create [] (Int (-1)) ty) p in - let p, c, _ = P.normal_form p in - let i = Intervals.point (minus_num c) ty expl in - let i, ip = - try - let ip = MP.find p env.polynomes in - Intervals.intersect i ip, ip - with Not_found -> i, Intervals.undefined ty - in - let env = - if Intervals.is_strict_smaller i ip then - let polynomes = MP.add p i env.polynomes in - let monomes = update_monomes_from_poly p i polynomes env.monomes - in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved } - else env - in - let env = - { env with - known_eqs = SX.add (P.alien_of p) env.known_eqs - } in - env, eqs - - let normal_form a = match a with - | L.Builtin (false, n, [r1; r2]) when is_le n && X.type_info r1 = Ty.Tint -> - let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in - L.Builtin (true, n, [r2; P.alien_of pred_r1]) - - | L.Builtin (true, n, [r1; r2]) when - not (is_le n) && X.type_info r1 = Ty.Tint -> - let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in - L.Builtin (true, ale, [r1; P.alien_of pred_r2]) - - | L.Builtin (false, n, [r1; r2]) when is_le n -> - L.Builtin (true, alt, [r2; r1]) - - | L.Builtin (false, n, [r1; r2]) when is_lt n -> - L.Builtin (true, ale, [r2; r1]) - - | _ -> a - - let remove_trivial_eqs eqs la = - let set_of l = - List.fold_left (fun s e -> Seq.add e s) Seq.empty l - in - Seq.elements (Seq.diff (set_of eqs) (set_of la)) - - - let equalities_from_polynomes env eqs = - let known, eqs = - MP.fold - (fun p i (knw, eqs) -> - let xp = P.alien_of p in - if SX.mem xp knw then knw, eqs - else - match Intervals.is_point i with - | Some (num, ex) -> - let r2 = P.alien_of (P.create [] num (P.type_info p)) in - SX.add xp knw, (L.Eq(xp, r2), None, ex) :: eqs - | None -> knw, eqs - ) env.polynomes (env.known_eqs, eqs) - in {env with known_eqs= known}, eqs - - - - let equalities_from_monomes env eqs = - let known, eqs = - MX.fold - (fun x (i,_) (knw, eqs) -> - if SX.mem x knw then knw, eqs - else - match Intervals.is_point i with - | Some (num, ex) -> - let r2 = P.alien_of (P.create [] num (X.type_info x)) in - SX.add x knw, (L.Eq(x, r2), None, ex) :: eqs - | None -> knw, eqs - ) env.monomes (env.known_eqs, eqs) - in {env with known_eqs= known}, eqs - - let equalities_from_intervals env eqs = - let env, eqs = equalities_from_polynomes env eqs in - equalities_from_monomes env eqs - - let assume env la = - let env = {env with improved = SP.empty} in - Debug.env env; - let env, eqs, new_ineqs, expl = - List.fold_left - (fun (env, eqs, new_ineqs, expl) (a, root, e) -> - let a = normal_form a in - let expl = Explanation.union e expl in - try - match a with - | L.Builtin(_, n, [r1;r2]) when is_le n || is_lt n -> - let root = match root with - | Some a -> a | None -> assert false in - let p1 = P.poly_of r1 in - let p2 = P.poly_of r2 in - let ineq = Inequation.create p1 p2 (is_le n) root expl in - let env = - init_monomes env ineq.Inequation.ple0 SX.empty expl in - let env = - update_ple0 env ineq.Inequation.ple0 (is_le n) expl in - let env = replace_inequation env root ineq in - env, eqs, true, expl - - | L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 -> - let p = P.sub (P.poly_of r1) (P.poly_of r2) in - let env = init_monomes env p SX.empty expl in - let env, eqs = add_disequality env eqs p expl in - env, eqs, new_ineqs, expl - - | L.Eq(r1, r2) when is_num r1 && is_num r2 -> - let p = P.sub (P.poly_of r1) (P.poly_of r2) in - let env = init_monomes env p SX.empty expl in - let env, eqs = add_equality env eqs p expl in - env, eqs, new_ineqs, expl - - | _ -> (env, eqs, new_ineqs, expl) - - with Intervals.NotConsistent expl -> - raise (Exception.Inconsistent expl) - ) - (env, [], false, Explanation.empty) la - - in - if new_ineqs then - if false then - (); - try - (* we only call fm when new ineqs are assumed *) - let env, eqs = if new_ineqs then fm env eqs expl else env, eqs in - (* let env = oldify_inequations env in *) - let env = update_polynomes env expl in - let env, eqs = equalities_from_intervals env eqs in - Debug.env env; - let eqs = remove_trivial_eqs eqs la in - Debug.implied_equalities eqs; - let result = - List.fold_left - (fun r (a_sem, a_term, ex) -> - { assume = (LSem(a_sem), ex) :: r.assume; - remove = - match a_term with - | None -> r.remove - | Some t -> (LTerm(t), ex)::r.remove - } ) { assume = []; remove = [] } eqs - in - env, result - - with Intervals.NotConsistent expl -> - raise (Exception.Inconsistent expl) - - let query env a_ex = - try - ignore(assume env [a_ex]); - No - with Exception.Inconsistent expl -> Yes expl - - let case_split_polynomes env = - let o = MP.fold - (fun p i o -> - match Intervals.finite_size i with - | Some s when s >/ (Int 1) -> - begin - match o with - | Some (s', _, _, _) when s' <=/ s -> o - | _ -> - let n, ex = Intervals.borne_inf i in - Some (s, p, n, ex) - end - | _ -> o - ) env.polynomes None in - match o with - | Some (s, p, n, ex) -> - let r1 = P.alien_of p in - let r2 = P.alien_of (P.create [] n (P.type_info p)) in - [L.Eq(r1, r2), ex, s] - | None -> - [] - - let case_split_monomes env = - let o = MX.fold - (fun x (i,_) o -> - match Intervals.finite_size i with - | Some s when s >/ (Int 1) -> - begin - match o with - | Some (s', _, _, _) when s' <=/ s -> o - | _ -> - let n, ex = Intervals.borne_inf i in - Some (s, x, n, ex) - end - | _ -> o - ) env.monomes None in - match o with - | Some (s,x,n,ex) -> - let ty = X.type_info x in - let r1 = x in - let r2 = P.alien_of (P.create [] n ty) in - [L.Eq(r1, r2), ex, s] - | None -> - [] - - let case_split env = - match case_split_polynomes env with - | [] -> case_split_monomes env - | choices -> choices - - let add env _ = env - - let extract_improved env = - SP.fold - (fun p acc -> - MP.add p (MP.find p env.polynomes) acc) - env.improved MP.empty - -end diff --git a/old/fm.mli b/old/fm.mli deleted file mode 100644 index fbae100f..00000000 --- a/old/fm.mli +++ /dev/null @@ -1,23 +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 *) -(* *) -(**************************************************************************) - -module type EXTENDED_Polynome = sig - include Polynome.T - val poly_of : r -> t - val alien_of : t -> r -end - -module Make - (X : Sig.X) - (P : EXTENDED_Polynome with type r = X.r) - : Sig.RELATION with type r = X.r diff --git a/old/intervals.ml b/old/intervals.ml deleted file mode 100644 index ed304ee3..00000000 --- a/old/intervals.ml +++ /dev/null @@ -1,703 +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 Num -open Format - -module Ex = Explanation - -type borne = - | Strict of (num * Ex.t) - | Large of (num * Ex.t) - | Pinfty | Minfty - -let compare_bornes b1 b2 = - match b1, b2 with - | Minfty, Minfty | Pinfty, Pinfty -> 0 - | Minfty, _ | _, Pinfty -> -1 - | Pinfty, _ | _, Minfty -> 1 - | Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _) - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - compare_num v1 v2 - -let compare_bu_bl b1 b2 = - match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c - -let compare_bl_bu b1 b2 = - match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c - -let compare_bl_bl b1 b2 = - match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c - | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c - -let compare_bu_bu b1 b2 = - match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c - | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c - -type t = { - ints : (borne * borne) list; - is_int : bool; - expl: Ex.t -} - -exception EmptyInterval of Ex.t -exception NotConsistent of Ex.t -exception Not_a_float - -let print_borne fmt = function - | Minfty -> fprintf fmt "-inf" - | Pinfty -> fprintf fmt "+inf" - | Strict (v, e) | Large (v, e) -> - fprintf fmt "%s" (string_of_num v) - -let print_interval fmt (b1,b2) = - let c1, c2 = match b1, b2 with - | Large _, Large _ -> '[', ']' - | Large _, _ -> '[', '[' - | _, Large _ -> ']', ']' - | _, _ -> ']', '[' - in - fprintf fmt "%c%a;%a%c" c1 print_borne b1 print_borne b2 c2 - -let print fmt {ints = ints; is_int = b; expl = e } = - List.iter (fun i -> fprintf fmt "%a" print_interval i) ints - - -let undefined ty = { - ints = [Minfty, Pinfty]; - is_int = ty = Ty.Tint; - expl = Ex.empty -} - -let point b ty e = { - ints = [Large (b, e), Large (b, e)]; - is_int = ty = Ty.Tint; - expl = Ex.empty -} - -let explain_borne = function - | Large (_, e) | Strict (_, e) -> e - | _ -> Ex.empty - -let add_expl_to_borne b e = - match b with - | Large (n, e') -> Large (n, Ex.union e e') - | Strict (n, e') -> Strict (n, Ex.union e e') - | Pinfty | Minfty -> b - -let borne_of k e n = if k then Large (n, e) else Strict (n, e) - -let is_point { ints = l; expl = e } = - match l with - | [Large (v1, e1) , Large (v2, e2)] when v1 =/ v2 -> - Some (v1, Ex.union e2 (Ex.union e1 e)) - | _ -> None - -let add_expl_zero i expl = - let res = List.map (fun x -> - match x with - | (Large ((Num.Int 0), e1) , Large ((Num.Int 0), e2)) -> - (Large ((Num.Int 0), Ex.union e1 expl), - Large ((Num.Int 0), Ex.union e2 expl)) - | _ -> x) i.ints in - { i with ints = res } - -let check_one_interval b1 b2 is_int = - match b1, b2 with - | Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty) - | (Strict (v1, e1) | Large (v1,e1)), - (Strict (v2, e2) | Large (v2, e2)) -> - let c = compare_num v1 v2 in - if c > 0 then raise - (EmptyInterval (Ex.union e2 e1)); - if c = 0 then begin - match b1, b2 with - | Large _, Large _ when not is_int || is_integer_num v1 -> - () - | _ -> raise (EmptyInterval (Ex.union e2 e1)) - end - | _ -> () - -let min_borne b1 b2 = - match b1, b2 with - | Minfty , _ | _ , Minfty -> Minfty - | b , Pinfty | Pinfty, b -> b - | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> - let c = compare_num v1 v2 in - if c < 0 then b1 - else if c > 0 then b2 - else match b1, b2 with - | (Strict _ as b) , _ | _, (Strict _ as b) -> b - | _, _ -> b1 - -let max_borne b1 b2 = - match b1, b2 with - | Pinfty , _ | _ , Pinfty -> Pinfty - | b , Minfty | Minfty, b -> b - | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> - let c = compare_num v1 v2 in - if c > 0 then b1 - else if c < 0 then b2 - else match b1, b2 with - | (Strict _ as b) , _ | _, (Strict _ as b) -> b - | _, _ -> b1 - -let pos_borne b1 = - compare_bornes b1 (borne_of true Ex.empty (Int 0)) >= 0 -let pos_borne_strict b1 = - compare_bornes b1 (borne_of true Ex.empty (Int 0)) > 0 -let neg_borne b1 = - compare_bornes b1 (borne_of true Ex.empty (Int 0)) <= 0 -let neg_borne_strict b1 = - compare_bornes b1 (borne_of true Ex.empty (Int 0)) < 0 -let zero_borne b1 = - compare_bornes b1 (borne_of true Ex.empty (Int 0)) = 0 - -exception Found of Sig.answer - -let doesnt_contain_0 {ints=l} = - try - let max = List.fold_left - (fun old_u (l, u) -> - if neg_borne l && pos_borne u then raise (Found Sig.No); - if neg_borne_strict old_u && pos_borne_strict l then - raise (Found - (Sig.Yes - (Ex.union - (explain_borne old_u) (explain_borne l)))); - u) Minfty l in - if neg_borne_strict max then Sig.Yes (explain_borne max) - else Sig.No - with Found ans -> ans - -let is_strict_smaller i1 i2 = - match i1, i2 with - | _, [] -> false - | [], _ -> true - | _ -> - try - List.iter2 (fun (l1, u1) (l2, u2) -> - if compare_bornes l1 l2 > 0 || compare_bornes u1 u2 < 0 - then raise Exit - ) i1 i2; - false - with - | Exit -> true - | Invalid_argument _ -> List.length i1 > List.length i2 - -let is_strict_smaller {ints=i1} {ints=i2} = - is_strict_smaller i1 i2 - - -let rec union_bornes l = - match l with - | [] | [_] -> l - | (l1, u1)::((l2, u2)::r as r2) -> - if compare_bornes u1 l2 < 0 then - (l1, u1)::(union_bornes r2) - else if compare_bornes u1 u2 > 0 then - union_bornes ((l1, u1)::r) - else - union_bornes ((l1, u2)::r) - -let union ({ints = l} as uints) = - let l = List.sort (fun (l1, _) (l2, _) -> compare_bornes l1 l2) l in - { uints with ints = union_bornes l } - -let add_borne b1 b2 = - match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> assert false - | Minfty, _ | _, Minfty -> Minfty - | Pinfty, _ | _, Pinfty -> Pinfty - | Large (v1, e1), Large (v2, e2) -> - Large (v1 +/ v2, Ex.union e1 e2) - | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) -> - Strict (v1 +/ v2, Ex.union e1 e2) - -let add_interval l (b1,b2) = - List.fold_right - (fun (b1', b2') l -> - let l1 = ((add_borne b1 b1'),(add_borne b2 b2'))::l in - union_bornes (l1) - ) l [] - -let add {ints = l1; is_int = is_int; expl = e1} {ints = l2; expl = e2}= - let l = - List.fold_left - (fun l bs -> let i = add_interval l1 bs in i@l) [] l2 - in - union { ints = l ; is_int = is_int; expl = Ex.union e1 e2 } - -let minus_borne = function - | Minfty -> Pinfty - | Pinfty -> Minfty - | Large (v, e) -> Large (minus_num v, e) - | Strict (v, e) -> Strict (minus_num v, e) - -let scale_borne n b = - assert (n >=/ Int 0); - if n =/ Int 0 then - match b with - | Pinfty | Minfty -> Large (Int 0, Ex.empty) - | Large (_, e) | Strict (_, e) -> Large (Int 0, e) - else match b with - | Pinfty | Minfty -> b - | Large (v, e) -> Large (n */ v, e) - | Strict (v, e) -> Strict (n */ v, e) - -let scale_interval n (b1,b2) = - if n assert false - | Minfty, b | b, Minfty -> - if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 - then b - else if pos_borne b then Minfty - else Pinfty - | Pinfty, b | b, Pinfty -> - if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 - then b - else if pos_borne b then Pinfty - else Minfty - | Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2) - | Large (v1, e1), Strict (v2, e2) -> - Strict (v1 */ v2, Ex.union e1 e2) - | Large (v1, e1), Large (v2, e2) -> - Large (v1 */ v2, Ex.union e1 e2) - -let mult_borne_inf b1 b2 = - match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> Minfty - | _, _ -> mult_borne b1 b2 - -let mult_borne_sup b1 b2 = - match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> Pinfty - | _, _ -> mult_borne b1 b2 - -type interval_class = - | P of Ex.t - | M of Ex.t - | N of Ex.t - | Z - -let class_of (l,u) = - if zero_borne l && zero_borne u then Z - else if pos_borne l && pos_borne u then P (explain_borne l) - else if neg_borne l && neg_borne u then N (explain_borne u) - else M (Ex.union (explain_borne l) (explain_borne u)) - -let mult_bornes (a,b) (c,d) = - (* see util/intervals_mult.png *) - match class_of (a,b), class_of (c,d) with - | P e1, P e2 -> - mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, M e2 -> - mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, N e2 -> - mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2 - | M e1, P e2 -> - mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2 - | M e1, M e2 -> - min_borne (mult_borne_inf a d) (mult_borne_inf b c), - max_borne (mult_borne_sup a c) (mult_borne_sup b d), - Ex.union e1 e2 - | M e1, N e2 -> - mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2 - | N e1, P e2 -> - mult_borne_inf a d, mult_borne_sup b c, Ex.union e1 e2 - | N e1, M e2 -> - mult_borne_inf a d, mult_borne_sup a c, Ex.union e1 e2 - | N e1, N e2 -> - mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2 - | Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty) - | (P _ | M _ | N _ ), Z -> (c, d, Ex.empty) - -let rec power_borne_inf p b = - match p with - | 1 -> b - | p -> mult_borne_inf b (power_borne_inf (p-1) b) - -let rec power_borne_sup p b = - match p with - | 1 -> b - | p -> mult_borne_sup b (power_borne_sup (p-1) b) - -let max_merge b1 b2 = - let ex = Ex.union (explain_borne b1) (explain_borne b2) in - let max = max_borne b1 b2 in - match max with - | Minfty | Pinfty -> max - | Large (v, e) -> Large (v, ex) - | Strict (v, e) -> Strict (v, ex) - -let power_bornes p (b1,b2) = - if neg_borne b1 && pos_borne b2 then - match p with - | 0 -> assert false - | p when p mod 2 = 0 -> - (* max_merge to have explanations !!! *) - let m = max_merge (power_borne_sup p b1) (power_borne_sup p b2) in - (Large (Int 0, Ex.empty), m) - | _ -> (power_borne_inf p b1, power_borne_sup p b2) - else if pos_borne b1 && pos_borne b2 then - (power_borne_inf p b1, power_borne_sup p b2) - else if neg_borne b1 && neg_borne b2 then - match p with - | 0 -> assert false - | p when p mod 2 = 0 -> (power_borne_inf p b2, power_borne_sup p b1) - | _ -> (power_borne_inf p b1, power_borne_sup p b2) - else assert false - -let int_of_borne_inf b = - match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (ceiling_num v, e) - | Strict (v, e) -> - let v' = ceiling_num v in - if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) - -let int_of_borne_sup b = - match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) - -let int_div_of_borne_sup b = - match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' - let (lo1,up1), (lo2,up2) = - if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2) - else (lo1,up1), (lo2,up2) in - let cll = compare_bl_bl lo1 lo2 in - let cuu = compare_bu_bu up1 up2 in - let clu = compare_bl_bu lo1 up2 in - let cul = compare_bu_bl up1 lo2 in - if cul < 0 then - let nexpl = Ex.union (explain_borne up1) (explain_borne lo2) in - match r1 with - | [] -> step (r1, l2) acc (Ex.union nexpl expl) - | (lor1,upr1)::rr1 -> - let lor1 = add_expl_to_borne lor1 nexpl in - let r1 = (lor1,upr1)::rr1 in - step (r1, l2) acc expl - else if clu > 0 then - let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in - match r2 with - | [] -> step (l1, r2) acc (Ex.union nexpl expl) - | (lor2,upr2)::rr2 -> - let lor2 = add_expl_to_borne lor2 nexpl in - let r2 = (lor2,upr2)::rr2 in - step (l1, r2) acc expl - else if cll = 0 && cuu = 0 then - step (r1, r2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu >= 0 then - step (l1, r2) ((lo2,up2)::acc) expl - else if cll >= 0 && cuu <= 0 then - step (r1, l2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu <= 0 && cul >= 0 then - step (r1, l2) ((lo2,up1)::acc) expl - else if cll >= 0 && cuu >= 0 && clu <= 0 then - step (l1, r2) ((lo1,up2)::acc) expl - else assert false - | [], _ | _, [] -> List.rev acc, expl - in - let l, expl = step (l1,l2) [] (Ex.union e1 e2) in - if l = [] then raise (NotConsistent expl) - else { uints1 with ints = l; expl = expl } - - -let new_borne_sup expl b ~is_le uints = - intersect - { ints = [Minfty, (borne_of is_le expl b)]; - is_int = uints.is_int; - expl = Ex.empty } uints - -let new_borne_inf expl b ~is_le uints = - intersect - { ints = [(borne_of is_le expl b), Pinfty]; - is_int = uints.is_int; - expl = Ex.empty } uints - -let complement ({ints=l; expl=e} as uints) = - let rec step l prev acc = - match l with - | (b1,b2)::r -> - let bu = match b1 with - | Strict v -> Large v - | Large v -> Strict v - | _ -> b1 in - let bl = match b2 with - | Strict v -> Large v - | Large v -> Strict v - | _ -> b2 in - if bu = Minfty then step r bl acc - else step r bl ((prev, bu)::acc) - | [] -> - if prev = Pinfty then List.rev acc - else List.rev ((prev, Pinfty)::acc) - in - { uints with ints = step l Minfty [] } - - -let exclude uints1 uints2 = - intersect (complement uints1) uints2 - -let mult u1 u2 = - let resl, expl = - List.fold_left - (fun (l', expl) b1 -> - List.fold_left - (fun (l, ex) b2 -> - let bl, bu, ex' = mult_bornes b1 b2 in - (bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints) - ([], Ex.empty) u1.ints - in - union { ints=resl; is_int = u1.is_int; - expl = Ex.union expl - (Ex.union u1.expl u2.expl) } - -let power n u = - let l = List.map (power_bornes n) u.ints in - union { u with ints = l } - - -let num_of_float x = - if x = infinity || x = neg_infinity then raise Not_a_float; - let (f, n) = frexp x in - let z = - Big_int.big_int_of_string - (Int64.to_string (Int64.of_float (f *. 2. ** 52.))) in - (* - Si on a ocaml >= 3.11 on peut mettre (mieux) : - let z = - Big_int.big_int_of_int64 - (Int64.of_float (f *. 2. ** 52.)) in - *) - let factor = (Int 2) **/ (Int (n - 52)) in - (Big_int z) */ factor - -let root_num a n = - if a =/ (Int 0) then s else a // (s **/ ((Int n) -/ (Int 1))) - -let root_exces_num a n = - let s = root_num a n in - let d = a -/ (s **/ (Int n)) in - if d <=/ (Int 0) then s else a // (s **/ ((Int n) -/ (Int 1))) - -let root_default_borne is_int x n = - match x with - | Pinfty -> Pinfty - | Minfty -> Minfty - | Large (v, e) | Strict (v, e) -> - let s = if v >=/ (Int 0) then root_default_num v n - else (minus_num (root_exces_num (minus_num v) n)) in - if is_int then - let cs = ceiling_num s in - let cs2 = cs **/ (Int n) in - if v <=/ cs2 then Large (cs, e) - else Large (cs +/ (Int 1), e) - else Large (s, e) - -let root_exces_borne is_int x n = - match x with - | Pinfty -> Pinfty - | Minfty -> Minfty - | Large (v, e) | Strict (v, e) -> - let s = if v >=/ (Int 0) then root_exces_num v n - else (minus_num (root_default_num (minus_num v) n)) in - if is_int then - let cs = floor_num s in - let cs2 = cs **/ (Int n) in - if v >=/ cs2 then Large (cs, e) - else Large (cs -/ (Int 1), e) - else Large (s, e) - -let sqrt_interval is_int (b1,b2) = - let l1, u1 = (minus_borne (root_exces_borne is_int b2 2), - minus_borne (root_default_borne is_int b1 2)) in - let l2, u2 = (root_default_borne is_int b1 2, - root_exces_borne is_int b2 2) in - if compare_bornes l1 u1 > 0 then - if compare_bornes l2 u2 > 0 then [] - else [l2,u2] - else if compare_bornes l2 u2 > 0 then [l1, u1] - else union_bornes [(l1,u1); (l2, u2)] - -let root_interval is_int (b1,b2) n = - let u,l = (root_default_borne is_int b1 n, root_exces_borne is_int b2 n) in - if compare_bornes u l > 0 then [] else [u,l] - -let sqrt {ints = l; is_int = is_int; expl = e } = - let l = - List.fold_left - (fun l' bs -> - (sqrt_interval is_int bs)@l' - ) [] l in - union { ints = l; is_int = is_int; expl = e } - -let rec root n ({ints = l; is_int = is_int; expl = e} as u) = - if n mod 2 = 0 then root (n/2) (sqrt u) - else - let l = - List.fold_left - (fun l' bs -> - (root_interval is_int bs n)@l' - ) [] l in - union { ints = l; is_int = is_int; expl = e } - -let finite_size {ints = l; is_int = is_int} = - if (not is_int) then None - else - try - let n = - List.fold_left - (fun n (b1,b2) -> - match b1, b2 with - | Minfty, _ | _, Pinfty -> raise Exit - | Large (v1, _) , Large (v2, _) -> n +/ (v2 -/ v1 +/ (Int 1)) - | _, _ -> assert false - ) (Int 0) l in - Some n - with Exit -> None - -let borne_inf = function - | {ints = (Large (v, ex), _)::_} -> v, ex - | _ -> invalid_arg "Intervals.borne_inf : No finite lower bound" - - - -let inv_borne_inf b is_int ~other = - match b with - | Pinfty -> assert false - | Minfty -> - if is_int then Large (Int 0, explain_borne other) - else Strict (Int 0, explain_borne other) - | Strict (Int 0, e) | Large (Int 0, e) -> Pinfty - | Strict (v, e) -> Strict (Int 1 // v, e) - | Large (v, e) -> Large (Int 1 // v, e) - -let inv_borne_sup b is_int ~other = - match b with - | Minfty -> assert false - | Pinfty -> - if is_int then Large (Int 0, explain_borne other) - else Strict (Int 0, explain_borne other) - | Strict (Int 0, e) | Large (Int 0, e) -> Minfty - | Strict (v, e) -> Strict (Int 1 // v, e) - | Large (v, e) -> Large (Int 1 // v, e) - -let inv_bornes (l, u) is_int = - inv_borne_sup u is_int ~other:l, inv_borne_inf l is_int ~other:u - - -let inv ({ints=l; is_int=is_int} as u) = - try - let l' = List.fold_left - (fun acc (l,u) -> - if (pos_borne_strict l && pos_borne_strict u) - || (neg_borne_strict l && neg_borne_strict u) then - (inv_bornes (l, u) is_int) :: acc - else raise Exit - ) [] l in - union { u with ints=l' } - with Exit -> { u with ints = [Minfty, Pinfty] } - -let div i1 i2 = - let inv_i2 = inv i2 in - if inv_i2.ints = [Minfty, Pinfty] then inv_i2 - else - let i1 = match doesnt_contain_0 i2 with - | Sig.Yes ex -> add_expl_zero i1 ex - | Sig.No -> i1 - in - let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in - let l = - if is_int then - List.map (fun (l,u) -> int_div_bornes l u) l - else l in - { i with ints = l } diff --git a/old/intervals.mli b/old/intervals.mli deleted file mode 100644 index 44c876c5..00000000 --- a/old/intervals.mli +++ /dev/null @@ -1,57 +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 Num - -type t - -exception NotConsistent of Explanation.t -exception Not_a_float - -val undefined : Ty.t -> t - -val point : num -> Ty.t -> Explanation.t -> t - -val doesnt_contain_0 : t -> Sig.answer - -val is_strict_smaller : t -> t -> bool - -val new_borne_sup : Explanation.t -> num -> is_le : bool -> t -> t - -val new_borne_inf : Explanation.t -> num -> is_le : bool -> t -> t - -val is_point : t -> (num * Explanation.t) option - -val intersect : t -> t -> t - -val exclude : t -> t -> t - -val mult : t -> t -> t - -val power : int -> t -> t - -val sqrt : t -> t - -val root : int -> t -> t - -val add : t -> t -> t - -val scale : num -> t -> t - -val print : Format.formatter -> t -> unit - -val finite_size : t -> num option - -val borne_inf : t -> num * Explanation.t - -val div : t -> t -> t diff --git a/old/literal.ml b/old/literal.ml deleted file mode 100644 index 464a5ed7..00000000 --- a/old/literal.ml +++ /dev/null @@ -1,210 +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 Hashcons - -type 'a view = - | Eq of 'a * 'a - | Distinct of bool * 'a list - | Builtin of bool * Hstring.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 add_label : Hstring.t -> t -> unit - val label : t -> Hstring.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 = (X.t view) hash_consed - - module V = struct - type t = X.t view - - let equal a1 a2 = - match a1, a2 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 && Hstring.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 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) (Hstring.hash n+x) l) - end - - module H = Make_consed(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 - let equal = equal - let hash = hash - end - - let make t = H.hashcons t - let view a = a.node - - 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)) - - module Labels = Hashtbl.Make(T) - - let labels = Labels.create 100007 - - let add_label lbl t = Labels.replace labels t lbl - - let label t = try Labels.find labels t with Not_found -> Hstring.empty - - let print_list fmt = function - | [] -> () - | z :: l -> - Format.fprintf fmt "%a" X.print z; - List.iter (Format.fprintf fmt ", %a" X.print) l - - let ale = Hstring.make "<=" - let alt = Hstring.make "<" - - let print fmt a = - let lbl = Hstring.view (label a) in - let lbl = if lbl = "" then lbl else lbl^":" in - match view a with - | Eq (z1, z2) -> - if equal z1 z2 then Format.fprintf fmt "True" - else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2 - | Distinct (b,(z::l)) -> - let b = if b then "~" else "" in - Format.fprintf fmt "%s%s%a" lbl b X.print z; - List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l - - | Builtin (true, n, [v1;v2]) when Hstring.equal n ale -> - Format.fprintf fmt "%s %a <= %a" lbl X.print v1 X.print v2 - - | Builtin (true, n, [v1;v2]) when Hstring.equal n alt -> - Format.fprintf fmt "%s %a < %a" lbl X.print v1 X.print v2 - - | Builtin (false, n, [v1;v2]) when Hstring.equal n ale -> - Format.fprintf fmt "%s %a > %a" lbl X.print v1 X.print v2 - - | Builtin (false, n, [v1;v2]) when Hstring.equal n alt -> - Format.fprintf fmt "%s %a >= %a" lbl X.print v1 X.print v2 - - | Builtin (b, n, l) -> - let b = if b then "" else "~" in - Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view 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/old/literal.mli b/old/literal.mli deleted file mode 100644 index b4c3d9ef..00000000 --- a/old/literal.mli +++ /dev/null @@ -1,63 +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 *) -(* *) -(**************************************************************************) - -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 * Hstring.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 add_label : Hstring.t -> t -> unit - val label : t -> Hstring.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/old/polynome.ml b/old/polynome.ml deleted file mode 100644 index 05bc97ec..00000000 --- a/old/polynome.ml +++ /dev/null @@ -1,257 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Format -open Num - -exception Not_a_num -exception Maybe_zero - -module type S = sig - type r - val compare : r -> r -> int - val term_embed : Term.t -> r - val mult : r -> r -> r - val print : Format.formatter -> r -> unit -end - -module type T = sig - - type r - type t - - val compare : t -> t -> int - val hash : t -> int - val create : (num * r) list -> num -> Ty.t-> t - val add : t -> t -> t - val sub : t -> t -> t - val mult : t -> t -> t - val mult_const : num -> t -> t - val div : t -> t -> t * bool - val modulo : t -> t -> t - - val is_empty : t -> bool - val find : r -> t -> num - val choose : t -> num * r - val subst : r -> t -> t -> t - val remove : r -> t -> t - val to_list : t -> (num * r) list * num - - val print : Format.formatter -> t -> unit - val type_info : t -> Ty.t - val is_monomial : t -> (num * r * num) option - - val ppmc_denominators : t -> num - val pgcd_numerators : t -> num - val normal_form : t -> t * num * num - val normal_form_pos : t -> t * num * num -end - -module Make (X : S) = struct - - type r = X.r - - module M : Map.S with type key = r = - Map.Make(struct type t = r let compare x y = X.compare y x end) - - type t = { m : num M.t; c : num; ty : Ty.t } - - let compare p1 p2 = - let c = Ty.compare p1.ty p2.ty in - if c <> 0 then c - else - let c = compare_num p1.c p2.c in - if c = 0 then M.compare compare_num p1.m p2.m else c - - let hash p = - abs (Hashtbl.hash p.m + 19*Hashtbl.hash p.c + 17 * Ty.hash p.ty) - - let pprint fmt p = - M.iter - (fun x n -> - let s, n, op = match n with - | Int 1 -> "+", "", "" - | Int -1 -> "-", "", "" - | n -> - if n >/ Int 0 then "+", string_of_num n, "*" - else "-", string_of_num (minus_num n), "*" - in - fprintf fmt "%s%s%s%a" s n op X.print x - )p.m; - let s, n = if p.c >=/ Int 0 then "+", string_of_num p.c - else "-", string_of_num (minus_num p.c) in - fprintf fmt "%s%s" s n - - - let print fmt p = - M.iter - (fun t n -> fprintf fmt "%s*%a " (string_of_num n) X.print t) p.m; - fprintf fmt "%s" (string_of_num p.c); - fprintf fmt " [%a]" Ty.print p.ty - - let is_num p = M.is_empty p.m - - let find x m = try M.find x m with Not_found -> Int 0 - - let create l c ty = - let m = - List.fold_left - (fun m (n, x) -> - let n' = n +/ (find x m) in - if n' =/ (Int 0) then M.remove x m else M.add x n' m) M.empty l - in - { m = m; c = c; ty = ty } - - let add p1 p2 = - let m = - M.fold - (fun x a m -> - let a' = (find x m) +/ a in - if a' =/ (Int 0) then M.remove x m else M.add x a' m) - p2.m p1.m - in - { m = m; c = p1.c +/ p2.c; ty = p1.ty } - - let mult_const n p = - if n =/ (Int 0) then { m = M.empty; c = Int 0; ty = p.ty } - else { p with m = M.map (mult_num n) p.m; c = n */ p.c } - - let mult_monome a x p = - let ax = { m = M.add x a M.empty; c = (Int 0); ty = p.ty} in - let acx = mult_const p.c ax in - let m = - M.fold - (fun xi ai m -> M.add (X.mult x xi) (a */ ai) m) p.m acx.m - in - { acx with m = m} - - let mult p1 p2 = - let p = mult_const p1.c p2 in - M.fold (fun x a p -> add (mult_monome a x p2) p) p1.m p - - let sub p1 p2 = - add p1 (mult (create [] (Int (-1)) p1.ty) p2) - - let div p1 p2 = - if M.is_empty p2.m then - if p2.c =/ Int 0 then raise Division_by_zero - else - let p = mult_const ((Int 1) // p2.c) p1 in - match M.is_empty p.m, p.ty with - | true, Ty.Tint -> {p with c = floor_num p.c}, false - | true, Ty.Treal -> p, false - | false, Ty.Tint -> p, true - | false, Ty.Treal -> p, false - | _ -> assert false - else raise Maybe_zero - - - let modulo p1 p2 = - if M.is_empty p2.m then - if p2.c =/ Int 0 then raise Division_by_zero - else - if M.is_empty p1.m then { p1 with c = mod_num p1.c p2.c } - else raise Not_a_num - else raise Maybe_zero - - let find x p = M.find x p.m - - let is_empty p = M.is_empty p.m - - let choose p = - let tn= ref None in - (*version I : prend le premier element de la table*) - (try M.iter - (fun x a -> tn := Some (a, x); raise Exit) p.m with Exit -> ()); - (*version II : prend le dernier element de la table i.e. le plus grand - M.iter (fun x a -> tn := Some (a, x)) p.m;*) - match !tn with Some p -> p | _ -> raise Not_found - - let subst x p1 p2 = - try - let a = M.find x p2.m in - add (mult_const a p1) { p2 with m = M.remove x p2.m} - with Not_found -> p2 - - let remove x p = { p with m = M.remove x p.m } - - let to_list p = - let l = M.fold (fun x a aliens -> (a, x)::aliens ) p.m [] in - List.rev l, p.c - - let type_info p = p.ty - - let is_monomial p = - try - M.fold - (fun x a r -> - match r with - | None -> Some (a, x, p.c) - | _ -> raise Exit) - p.m None - with Exit -> None - - let denominator = function - | Num.Int _ | Num.Big_int _ -> Big_int.unit_big_int - | Num.Ratio rat -> Ratio.denominator_ratio rat - - let numerator = function - | Num.Int i -> Big_int.big_int_of_int i - | Num.Big_int b -> b - | Num.Ratio rat -> Ratio.numerator_ratio rat - - let pgcd_bi a b = Big_int.gcd_big_int a b - - let ppmc_bi a b = Big_int.div_big_int (Big_int.mult_big_int a b) (pgcd_bi a b) - - let abs_big_int_to_num b = - let b = - try Int (Big_int.int_of_big_int b) - with Failure "int_of_big_int" -> Big_int b - in - abs_num b - - let ppmc_denominators {m=m} = - let res = - M.fold - (fun k c acc -> ppmc_bi (denominator c) acc) - m Big_int.unit_big_int in - abs_num (num_of_big_int res) - - let pgcd_numerators {m=m} = - let res = - M.fold - (fun k c acc -> pgcd_bi (numerator c) acc) - m Big_int.zero_big_int in - abs_num (num_of_big_int res) - - let normal_form ({ m = m; c = c } as p) = - if M.is_empty m then - { p with c = Int 0 }, p.c, (Int 1) - else - let ppcm = ppmc_denominators p in - let pgcd = pgcd_numerators p in - let p = mult_const (ppcm // pgcd) p in - { p with c = Int 0 }, p.c, (pgcd // ppcm) - - let normal_form_pos p = - let p, c, d = normal_form p in - try - let a,x = choose p in - if a >/ (Int 0) then p, c, d - else mult_const (Int (-1)) p, minus_num c, minus_num d - with Not_found -> p, c, d - -end - diff --git a/old/polynome.mli b/old/polynome.mli deleted file mode 100644 index 8c171659..00000000 --- a/old/polynome.mli +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Num - -exception Not_a_num -exception Maybe_zero - -module type S = sig - type r - val compare : r -> r-> int - val term_embed : Term.t -> r - val mult : r -> r -> r - val print : Format.formatter -> r -> unit -end - -module type T = sig - - type r - type t - - val compare : t -> t -> int - val hash : t -> int - - val create : (num * r) list -> num -> Ty.t-> t - val add : t -> t -> t - val sub : t -> t -> t - val mult : t -> t -> t - val mult_const : num -> t -> t - val div : t -> t -> t * bool - val modulo : t -> t -> t - - val is_empty : t -> bool - val find : r -> t -> num - val choose : t -> num * r - val subst : r -> t -> t -> t - val remove : r -> t -> t - val to_list : t -> (num * r) list * num - - val print : Format.formatter -> t -> unit - val type_info : t -> Ty.t - val is_monomial : t -> (num * r * num) option - - (* PPMC des denominateurs des coefficients excepte la constante *) - val ppmc_denominators : t -> num - (* PGCD des numerateurs des coefficients excepte la constante *) - val pgcd_numerators : t -> num - (* retourne un polynome sans constante et sa constante - et la constante multiplicative: - normal_form p = (p',c,d) <=> p = (p' + c) * d *) - val normal_form : t -> t * num * num - (* comme normal_form mais le signe est aussi normalise *) - val normal_form_pos : t -> t * num * num -end - -module Make (X : S) : T with type r = X.r - diff --git a/old/sig.mli b/old/sig.mli deleted file mode 100644 index 7f173abc..00000000 --- a/old/sig.mli +++ /dev/null @@ -1,146 +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 *) -(* *) -(**************************************************************************) - -type answer = Yes of Explanation.t | No - -type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t - -type 'a input = - 'a Literal.view * Literal.LT.t option * Explanation.t - -type 'a result = { - assume : ('a literal * Explanation.t) list; - remove: ('a literal * Explanation.t) list; -} - -module type RELATION = sig - type t - type r - - val empty : unit -> t - - val assume : t -> (r input) list -> t * r result - - val query : t -> r input -> answer - - val case_split : t -> (r Literal.view * Explanation.t * Num.num) list - (** case_split env returns a list of equalities *) - - val add : t -> r -> t - (** add a representant to take into account *) - -end - -module type THEORY = sig - - (**Type of terms of the theory*) - type t - - (**Type of representants of terms of the theory*) - type r - - (** Name of the theory*) - val name : string - - (** return true if the symbol is owned by the theory*) - val is_mine_symb : Symbols.t -> bool - - (** return true when the argument is an unsolvable function of the theory *) - val unsolvable : t -> bool - - (** Give a representant of a term of the theory*) - val make : Term.t -> r * Literal.LT.t list - - val term_extract : r -> Term.t option - - val type_info : t -> Ty.t - - val embed : r -> t - - (** Give the leaves of a term of the theory *) - val leaves : t -> r list - - val subst : r -> r -> t -> r - - val compare : t -> t -> int - - val hash : t -> int - (** solve r1 r2, solve the equality r1=r2 and return the substitution *) - - val solve : r -> r -> (r * r) list - - val print : Format.formatter -> t -> unit - - val fully_interpreted : Symbols.t -> bool - - module Rel : RELATION with type r = r -end - -module type COMBINATOR = sig - type r - type th - - val extract : r -> th - val make : Term.t -> r * Literal.LT.t list - val type_info : r -> Ty.t - val compare : r -> r -> int - val leaves : r -> r list - val subst : r -> r -> r -> r - val solve : r -> r -> (r * r) list - val empty_embedding : Term.t -> r - val normal_form : Literal.LT.t -> Literal.LT.t - val print : Format.formatter -> r -> unit - module Rel : RELATION with type r = r - -end - -module type X = sig - type r - - val make : Term.t -> r * Literal.LT.t list - - val type_info : r -> Ty.t - - val compare : r -> r -> int - - val equal : r -> r -> bool - - val hash : r -> int - - val leaves : r -> r list - - val subst : r -> r -> r -> r - - val solve : r -> r -> (r * r) list - - 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 - - module Rel : RELATION with type r = r - -end - -module type C = sig - type t - type r - val extract : r -> t option - val embed : t -> r -end - diff --git a/old/smt.ml b/old/smt.ml deleted file mode 100644 index 75bcb2fd..00000000 --- a/old/smt.ml +++ /dev/null @@ -1,790 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* 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 Format - -type error = - | DuplicateTypeName of Hstring.t - | DuplicateSymb of Hstring.t - | UnknownType of Hstring.t - | UnknownSymb of Hstring.t - -exception Error of error - -module AETerm = Term -module H = Hstring.H -module HSet = Hstring.HSet - -let decl_types = H.create 17 -let decl_symbs = H.create 17 - -let htrue = Hstring.make "True" -let hfalse = Hstring.make "False" - -module Type = struct - - type t = Hstring.t - - let equal = Hstring.equal - - let type_int = - let tint = Hstring.make "int" in - H.add decl_types tint Ty.Tint; - tint - - let type_real = - let treal = Hstring.make "real" in - H.add decl_types treal Ty.Treal; - treal - - let type_bool = - let tbool = Hstring.make "bool" in - H.add decl_types tbool Ty.Tbool; - tbool - - let type_proc = - let tproc = Hstring.make "proc" in - H.add decl_types tproc Ty.Tint; - tproc - - let declare_constructor ty c = - if H.mem decl_symbs c then raise (Error (DuplicateSymb c)); - H.add decl_symbs c - (Symbols.name ~kind:Symbols.Constructor c, [], ty) - - let declare t constrs = - if H.mem decl_types t then raise (Error (DuplicateTypeName t)); - match constrs with - | [] -> - H.add decl_types t (Ty.Tabstract t) - | _ -> - let ty = Ty.Tsum (t, constrs) in - H.add decl_types t ty; - List.iter (fun c -> declare_constructor t c) constrs - - let all_constructors () = - H.fold (fun _ c acc -> match c with - | Symbols.Name (h, Symbols.Constructor), _, _ -> h :: acc - | _ -> acc - ) decl_symbs [htrue; hfalse] - - let constructors ty = - if Hstring.equal ty type_bool then [htrue; hfalse] - else match H.find decl_types ty with - | Ty.Tsum (_ , cstrs) -> cstrs - | _ -> raise Not_found - -end - -module Symbol = struct - - type t = Hstring.t - - let declare f args ret = - if H.mem decl_symbs f then raise (Error (DuplicateTypeName f)); - List.iter - (fun t -> - if not (H.mem decl_types t) then raise (Error (UnknownType t)) ) - (ret::args); - H.add decl_symbs f (Symbols.name f, args, ret) - - let type_of s = let _, args, ret = H.find decl_symbs s in args, ret - - let declared s = - let res = H.mem decl_symbs s in - if not res then begin - eprintf "Not declared : %a in@." Hstring.print s; - H.iter (fun hs (sy, _, _) -> - eprintf "%a (=?%b) -> %a@." Hstring.print hs - (Hstring.compare hs s = 0) - Symbols.print sy) - decl_symbs; - end; - res - - let not_builtin ty = Hstring.equal ty Type.type_proc || - not (Hstring.equal ty Type.type_int || Hstring.equal ty Type.type_real || - Hstring.equal ty Type.type_bool || Hstring.equal ty Type.type_proc) - - let has_abstract_type s = - let _, ret = type_of s in - match H.find decl_types ret with - | Ty.Tabstract _ -> true - | _ -> false - - let has_type_proc s = - Hstring.equal (snd (type_of s)) Type.type_proc - - let _ = - H.add decl_symbs htrue (Symbols.True, [], Type.type_bool); - H.add decl_symbs hfalse (Symbols.False, [], Type.type_bool); - -end - - -module Variant = struct - - let constructors = H.create 17 - let assignments = H.create 17 - - let find t x = try H.find t x with Not_found -> HSet.empty - - let add t x v = - let s = find t x in - H.replace t x (HSet.add v s) - - let assign_constr = add constructors - - let assign_var x y = - if not (Hstring.equal x y) then - add assignments x y - - let rec compute () = - let flag = ref false in - let visited = ref HSet.empty in - let rec dfs x s = - if not (HSet.mem x !visited) then - begin - visited := HSet.add x !visited; - HSet.iter - (fun y -> - let c_x = find constructors x in - let c_y = find constructors y in - let c = HSet.union c_x c_y in - if not (HSet.equal c c_x) then - begin - H.replace constructors x c; - flag := true - end; - dfs y (find assignments y) - ) s - end - in - H.iter dfs assignments; - if !flag then compute () - - let hset_print fmt s = - HSet.iter (fun c -> Format.eprintf "%a, " Hstring.print c) s - - let print () = - H.iter - (fun x c -> - Format.eprintf "%a = {%a}@." Hstring.print x hset_print c) - constructors - - - let get_variants = H.find constructors - - let set_of_list = List.fold_left (fun s x -> HSet.add x s) HSet.empty - - let init l = - compute (); - List.iter - (fun (x, nty) -> - if not (H.mem constructors x) then - let ty = H.find decl_types nty in - match ty with - | Ty.Tsum (_, l) -> - H.add constructors x (set_of_list l) - | _ -> ()) l; - H.clear assignments - - let update_decl_types s = - let nty = ref "" in - let l = ref [] in - HSet.iter - (fun x -> - l := x :: !l; - let vx = Hstring.view x in - nty := if !nty = "" then vx else !nty ^ "|" ^ vx) s; - let nty = Hstring.make !nty in - let ty = Ty.Tsum (nty, List.rev !l) in - H.replace decl_types nty ty; - nty - - let close () = - compute (); - H.iter - (fun x s -> - let nty = update_decl_types s in - let sy, args, _ = H.find decl_symbs x in - H.replace decl_symbs x (sy, args, nty)) - constructors - -end - - -module rec Term : sig - - type t = T of AETerm.t | Tite of Formula.t * t * t - - type operator = Plus | Minus | Mult | Div | Modulo - - val first_ite : t list -> t list * (Formula.t * t * t) * t list - val make_int : Num.num -> t - val make_real : Num.num -> t - val make_app : Symbol.t -> t list -> t - val make_arith : operator -> t -> t -> t - val make_ite : Formula.t -> t -> t -> t - val is_int : t -> bool - val is_real : t -> bool - val t_true : t - val t_false : t - -end -= struct - - type t = T of AETerm.t | Tite of Formula.t * t * t - type operator = Plus | Minus | Mult | Div | Modulo - - let make_int i = T (AETerm.int (Num.string_of_num i)) - - let make_real r = T (AETerm.real (Num.string_of_num r)) - - let rec first_ite = function - | [] -> raise Not_found - | Tite (c, t1, t2) :: l -> [], (c, t1, t2), l - | x :: l -> - let left, triplet, right = first_ite l in - x::left, triplet, right - - let rec lift_ite sb l ty = - try - let left, (c, t1, t2), right = first_ite l in - let l = lift_ite sb (left@(t1::right)) ty in - let r = lift_ite sb (left@(t2::right)) ty in - Tite (c, l, r) - with Not_found -> - let l = List.map (function T x -> x | _ -> assert false) l in - T (AETerm.make sb l ty) - - let make_app s l = - try - let (sb, _, nty) = H.find decl_symbs s in - let ty = H.find decl_types nty in - lift_ite sb l ty - with Not_found -> raise (Error (UnknownSymb s)) - - let t_true = T AETerm.true_ - let t_false = T AETerm.false_ - - let rec is_int = function - | T t -> AETerm.is_int t - | Tite(_, t1, t2) -> is_int t1 && is_int t2 - - let rec is_real = function - | T t -> AETerm.is_real t - | Tite(_, t1, t2) -> is_real t1 && is_real t2 - - let make_arith op t1 t2 = - let op = - match op with - | Plus -> Symbols.Plus - | Minus -> Symbols.Minus - | Mult -> Symbols.Mult - | Div -> Symbols.Div - | Modulo -> Symbols.Modulo - in - let ty = - if is_int t1 && is_int t2 then Ty.Tint - else if is_real t1 && is_real t2 then Ty.Treal - else assert false - in - lift_ite (Symbols.Op op) [t1; t2] ty - - let make_ite l t1 t2 = Tite (l, t1, t2) - - -end - -and Formula : sig - - type comparator = Eq | Neq | Le | Lt - type combinator = And | Or | Imp | Not - type t = - | Lit of Literal.LT.t - | Comb of combinator * t list - - val f_true : t - val f_false : t - val make_lit : comparator -> Term.t list -> t - val make : combinator -> t list -> t - val make_cnf : t -> Literal.LT.t list list - - val make_pred : ?sign:bool -> Term.t -> t - val make_not : t -> t - val make_and : t list -> t - val make_or : t list -> t - val make_imply : t -> t -> t - val make_equiv : t -> t -> t - val make_xor : t -> t -> t - val make_eq : Term.t -> Term.t -> t - val make_neq : Term.t -> Term.t -> t - val make_le : Term.t -> Term.t -> t - val make_lt : Term.t -> Term.t -> t - val make_ge : Term.t -> Term.t -> t - val make_gt : Term.t -> Term.t -> t - - val print_list : string -> Format.formatter -> t list -> unit - val print : Format.formatter -> t -> unit - - module Tseitin (Dymmy : sig end) : - sig val make_cnf : t -> Literal.LT.t list list end - -end -= struct - - type comparator = Eq | Neq | Le | Lt - type combinator = And | Or | Imp | Not - - type t = - | Lit of Literal.LT.t - | Comb of combinator * t list - - let rec print fmt phi = - match phi with - | Lit a -> Literal.LT.print fmt a - | Comb (Not, [f]) -> - fprintf fmt "not (%a)" print f - | Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l - | Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l - | Comb (Imp, [f1; f2]) -> - fprintf fmt "(%a => %a)" print f1 print f2 - | _ -> assert false - and print_list sep fmt = function - | [] -> () - | [f] -> print fmt f - | f::l -> fprintf fmt "%a %s %a" print f sep (print_list sep) l - - let f_true = Lit Literal.LT.true_ - let f_false = Lit Literal.LT.false_ - - let make comb l = Comb (comb, l) - - let value env c = - if List.mem c env then Some true - else if List.mem (make Not [c]) env then Some false - else None - - let rec lift_ite env op l = - try - let left, (c, t1, t2), right = Term.first_ite l in - begin - match value env c with - | Some true -> - lift_ite (c::env) op (left@(t1::right)) - | Some false -> - lift_ite ((make Not [c])::env) op (left@(t2::right)) - | None -> - Comb - (And, - [Comb - (Imp, [c; lift_ite (c::env) op (left@(t1::right))]); - Comb (Imp, - [(make Not [c]); - lift_ite - ((make Not [c])::env) op (left@(t2::right))])]) - end - with Not_found -> - begin - let lit = - match op, l with - | Eq, [Term.T t1; Term.T t2] -> - Literal.Eq (t1, t2) - | Neq, ts -> - let ts = - List.rev_map (function Term.T x -> x | _ -> assert false) ts in - Literal.Distinct (false, ts) - | Le, [Term.T t1; Term.T t2] -> - Literal.Builtin (true, Hstring.make "<=", [t1; t2]) - | Lt, [Term.T t1; Term.T t2] -> - Literal.Builtin (true, Hstring.make "<", [t1; t2]) - | _ -> assert false - in - Lit (Literal.LT.make lit) - end - - let make_lit op l = lift_ite [] op l - - let make_pred ?(sign=true) p = - if sign - then make_lit Eq [p; Term.t_true] - else make_lit Eq [p; Term.t_false] - - let make_eq t1 t2 = make_lit Eq [t1; t2] - let make_neq t1 t2 = make_lit Neq [t1; t2] - let make_le t1 t2 = make_lit Le [t1; t2] - let make_lt t1 t2 = make_lit Lt [t1; t2] - let make_ge t1 t2 = make_lit Le [t2; t1] - let make_gt t1 t2 = make_lit Lt [t2; t1] - let make_not f = make Not [f] - let make_and l = make And l - let make_imply f1 f2 = make Imp [f1; f2] - let make_equiv f1 f2 = make And [ make_imply f1 f2; make_imply f2 f1] - let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ]; - make And [ f1; make Not [f2] ] ] - - (* simplify formula *) - let rec sform = function - | Comb (Not, [Lit a]) -> Lit (Literal.LT.neg a) - | Comb (Not, [Comb (Not, [f])]) -> sform f - | Comb (Not, [Comb (Or, l)]) -> - let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in - Comb (And, nl) - | Comb (Not, [Comb (And, l)]) -> - let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in - Comb (Or, nl) - | Comb (Not, [Comb (Imp, [f1; f2])]) -> - Comb (And, [sform f1; sform (Comb (Not, [f2]))]) - | Comb (And, l) -> - Comb (And, List.rev_map sform l) - | Comb (Or, l) -> - Comb (Or, List.rev_map sform l) - | Comb (Imp, [f1; f2]) -> - Comb (Or, [sform (Comb (Not, [f1])); sform f2]) - | Comb ((Imp | Not), _) -> assert false - | Lit _ as f -> f - - - let ( @@ ) l1 l2 = List.rev_append l1 l2 - let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) - - let make_or = function - | [] -> f_false - | [a] -> a - | l -> Comb (Or, l) - - let distrib l_and l_or = - let l = - if l_or = [] then l_and - else - List.rev_map - (fun x -> - match x with - | Lit _ -> Comb (Or, x::l_or) - | Comb (Or, l) -> Comb (Or, l @@ l_or) - | _ -> assert false - ) l_and - in - Comb (And, l) - - let rec flatten_or = function - | [] -> [] - | Comb (Or, l)::r -> l @@ (flatten_or r) - | Lit a :: r -> (Lit a)::(flatten_or r) - | _ -> assert false - - let rec flatten_and = function - | [] -> [] - | Comb (And, l)::r -> l @@ (flatten_and r) - | a :: r -> a::(flatten_and r) - - - let rec cnf f = - match f with - | Comb (Or, l) -> - begin - let l = List.rev_map cnf l in - let l_and, l_or = - List.partition (function Comb(And,_) -> true | _ -> false) l in - match l_and with - | [ Comb(And, l_conj) ] -> - let u = flatten_or l_or in - distrib l_conj u - - | Comb(And, l_conj) :: r -> - let u = flatten_or l_or in - cnf (Comb(Or, (distrib l_conj u)::r)) - - | _ -> - begin - match flatten_or l_or with - | [] -> assert false - | [r] -> r - | v -> Comb (Or, v) - end - end - | Comb (And, l) -> - Comb (And, List.rev_map cnf l) - | f -> f - - let rec mk_cnf = function - | Comb (And, l) -> - List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l - - | Comb (Or, [f1;f2]) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf f2 in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Comb (Or, f1 :: l) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf (Comb (Or, l)) in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Lit a -> [[a]] - | Comb (Not, [Lit a]) -> [[Literal.LT.neg a]] - | _ -> assert false - - - let rec unfold mono f = - match f with - | Lit a -> a::mono - | Comb (Not, [Lit a]) -> - (Literal.LT.neg a)::mono - | Comb (Or, l) -> - List.fold_left unfold mono l - | _ -> assert false - - let rec init monos f = - match f with - | Comb (And, l) -> - List.fold_left init monos l - | f -> (unfold [] f)::monos - - let make_cnf f = - let sfnc = cnf (sform f) in - init [] sfnc - - let mk_proxy = - let cpt = ref 0 in - fun () -> - let t = AETerm.make - (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt)))) - [] Ty.Tbool - in - incr cpt; - Literal.LT.make (Literal.Eq (t, AETerm.true_)) - - module Tseitin (Dummy : sig end)= struct - let acc_or = ref [] - let acc_and = ref [] - - (* build a clause by flattening (if sub-formulas have the - same combinator) and proxy-ing sub-formulas that have the - opposite operator. *) - let rec cnf f = match f with - | Lit a -> None, [a] - | Comb (Not, [Lit a]) -> None, [Literal.LT.neg a] - - | Comb (And, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | cmb, [a] -> Some And, a :: acc - | Some And, l -> - Some And, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_and := (proxy, l) :: !acc_and; *) - (* proxy :: acc *) - | Some Or, l -> - let proxy = mk_proxy () in - acc_or := (proxy, l) :: !acc_or; - Some And, proxy :: acc - | None, l -> Some And, l @@ acc - | _ -> assert false - ) (None, []) l - - | Comb (Or, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | cmb, [a] -> Some Or, a :: acc - | Some Or, l -> - Some Or, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_or := (proxy, l) :: !acc_or; *) - (* proxy :: acc *) - | Some And, l -> - let proxy = mk_proxy () in - acc_and := (proxy, l) :: !acc_and; - Some Or, proxy :: acc - | None, l -> Some Or, l @@ acc - | _ -> assert false - ) (None, []) l - - | _ -> assert false - - let cnf f = - let acc = match f with - | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l - | _ -> [snd (cnf f)] - in - let proxies = ref [] in - (* encore clauses that make proxies in !acc_and equivalent to - their clause *) - let acc = - List.fold_left - (fun acc (p,l) -> - proxies := p :: !proxies; - let np = Literal.LT.neg p in - (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]] - also add clauses [p => l1], [p => l2], etc. *) - let cl, acc = - List.fold_left - (fun (cl,acc) a -> (Literal.LT.neg a :: cl), [np; a] :: acc) - ([p],acc) l in - cl :: acc - )acc !acc_and - in - (* encore clauses that make proxies in !acc_or equivalent to - their clause *) - let acc = - List.fold_left - (fun acc (p,l) -> - proxies := p :: !proxies; - (* add clause [p => l1 | l2 | ... | ln], and add clauses - [l1 => p], [l2 => p], etc. *) - let acc = List.fold_left (fun acc a -> [p; Literal.LT.neg a]::acc) - acc l in - (Literal.LT.neg p :: l) :: acc - ) acc !acc_or - in - acc - - let make_cnf f = - acc_or := []; - acc_and := []; - cnf (sform f) - end - - (* Naive CNF XXX remove??? - let make_cnf f = mk_cnf (sform f) - *) -end - -exception Unsat of int list - -let set_cc b = Cc.cc_active := b - -module type Solver = sig - type state - - val get_time : unit -> float - val get_calls : unit -> int - - val clear : unit -> unit - val assume : ?profiling:bool -> id:int -> Formula.t -> unit - val check : ?profiling:bool -> unit -> unit - - - val eval : Term.t -> bool - val save_state : unit -> state - val restore_state : state -> unit - val entails : ?profiling:bool -> id:int -> Formula.t -> bool -end - -module Make (Dummy : sig end) = struct - - let calls = ref 0 - module Time = Timer.Make (Dummy) - - let get_time = Time.get - let get_calls () = !calls - - module Tseitin = Formula.Tseitin (Dummy) - module CSolver = Solver.Make (Dummy) - - let clear () = CSolver.clear () - - let check_unsatcore uc = - eprintf "Unsat Core : @."; - List.iter - (fun c -> - eprintf "%a@." (Formula.print_list "or") - (List.rev_map (fun x -> Formula.Lit x) c)) uc; - eprintf "@."; - try - clear (); - CSolver.assume uc 0; - CSolver.solve (); - eprintf "Not an unsat core !!!@."; - assert false - with - | Solver.Unsat _ -> (); - | Solver.Sat -> - eprintf "Sat: Not an unsat core !!!@."; - assert false - - let export_unsatcore cl = - let uc = List.rev_map (fun {Solver_types.atoms=atoms} -> - let l = ref [] in - for i = 0 to Vec.size atoms - 1 do - l := (Vec.get atoms i).Solver_types.lit :: !l - done; - !l) cl - in (* check_unsatcore uc; *) - uc - - module SInt = - Set.Make (struct type t = int let compare = Pervasives.compare end) - - let export_unsatcore2 cl = - let s = - List.fold_left - (fun s {Solver_types.name = n} -> - try SInt.add (int_of_string n) s with _ -> s) SInt.empty cl - in - SInt.elements s - - let assume ?(profiling = false) ~id f = - if profiling then Time.start (); - try - CSolver.assume (Tseitin.make_cnf f) id; - if profiling then Time.pause () - with Solver.Unsat ex -> - if profiling then Time.pause (); - raise (Unsat (export_unsatcore2 ex)) - - let check ?(profiling = false) () = - incr calls; - if profiling then Time.start (); - try - CSolver.solve (); - if profiling then Time.pause () - with - | Solver.Sat -> if profiling then Time.pause () - | Solver.Unsat ex -> - if profiling then Time.pause (); - raise (Unsat (export_unsatcore2 ex)) - - type state = CSolver.state - - let eval t = - match t with - | Term.T t' -> - let lit = Literal.LT.mk_pred t' in - CSolver.eval lit - | Term.Tite _ -> - failwith "cannot evaluate \"if-then-else\" term" - - let save_state = CSolver.save - - let restore_state = CSolver.restore - - let entails ?(profiling=false) ~id f = - let st = save_state () in - let ans = - try - assume ~profiling ~id (Formula.make Formula.Not [f]) ; - check ~profiling (); - false - with Unsat _ -> true - in - restore_state st; - ans - -end diff --git a/old/smt.mli b/old/smt.mli deleted file mode 100644 index bbc04e19..00000000 --- a/old/smt.mli +++ /dev/null @@ -1,338 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* 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 *) -(* *) -(**************************************************************************) - -(** {b The Alt-Ergo Zero SMT library} - - This SMT solver is derived from {{:http://alt-ergo.lri.fr} Alt-Ergo}. It - uses an efficient SAT solver and supports the following quantifier free - theories: - - Equality and uninterpreted functions - - Arithmetic (linear, non-linear, integer, reals) - - Enumerated data-types - - This API makes heavy use of hash-consed strings. Please take a moment to - look at {! Hstring}. -*) - -(** {2 Error handling } *) - -type error = - | DuplicateTypeName of Hstring.t (** raised when a type is already declared *) - | DuplicateSymb of Hstring.t (** raised when a symbol is already declared *) - | UnknownType of Hstring.t (** raised when the given type is not declared *) - | UnknownSymb of Hstring.t (** raised when the given symbol is not declared *) - -exception Error of error - -(** {2 Typing } *) - -(** {3 Typing } *) -module Type : sig - - type t = Hstring.t - (** The type of types in Alt-Ergo Zero *) - - (** {4 Builtin types } *) - - val type_int : t - (** The type of integers *) - - val type_real : t - (** The type of reals *) - - val type_bool : t - (** The type of booleans *) - - val type_proc : t - (** The type processes (identifiers) *) - - (** {4 Declaring new types } *) - - val declare : Hstring.t -> Hstring.t list -> unit - (** {ul {- [declare n cstrs] declares a new enumerated data-type with - name [n] and constructors [cstrs].} - {- [declare n []] declares a new abstract type with name [n].}}*) - - val all_constructors : unit -> Hstring.t list - (** [all_constructors ()] returns a list of all the defined constructors. *) - - val constructors : t -> Hstring.t list - (** [constructors ty] returns the list of constructors of [ty] when type is - an enumerated data-type, otherwise returns [[]].*) - -end - - -(** {3 Function symbols} *) -module Symbol : sig - - type t = Hstring.t - (** The type of function symbols *) - - val declare : Hstring.t -> Type.t list -> Type.t -> unit - (** [declare s [arg_1; ... ; arg_n] out] declares a new function - symbol with type [ (arg_1, ... , arg_n) -> out] *) - - val type_of : t -> Type.t list * Type.t - (** [type_of x] returns the type of x. *) - - val has_abstract_type : t -> bool - (** [has_abstract_type x] is [true] if the type of x is abstract. *) - - val has_type_proc : t -> bool - (** [has_type_proc x] is [true] if x has the type of a process - identifier. *) - - val declared : t -> bool - (** [declared x] is [true] if [x] is already declared. *) - -end - -(** {3 Variants} - - The types of symbols (when they are enumerated data types) can be refined - to substypes of their original type (i.e. a subset of their constructors). -*) -module Variant : sig - - val init : (Symbol.t * Type.t) list -> unit - (** [init l] where [l] is a list of pairs [(s, ty)] initializes the - type (and associated constructors) of each [s] to its original type [ty]. - - This function must be called with a list of all symbols before - attempting to refine the types. *) - - val close : unit -> unit - (** [close ()] will compute the smallest type possible for each symbol. - - This function must be called when all information has been added.*) - - val assign_constr : Symbol.t -> Hstring.t -> unit - (** [assign_constr s cstr] will add the constraint that the constructor - [cstr] must be in the type of [s] *) - - val assign_var : Symbol.t -> Symbol.t -> unit - (** [assign_var x y] will add the constraint that the type of [y] is a - subtype of [x] (use this function when [x := y] appear in your - program *) - - val print : unit -> unit - (** [print ()] will output the computed refined types on std_err. This - function is here only for debugging purposes. Use it afer [close ()].*) - - val get_variants : Symbol.t -> Hstring.HSet.t - (** [get_variants s] returns a set of constructors, which is the refined - type of [s].*) - -end - -(** {2 Building terms} *) - -module rec Term : sig - - type t - (** The type of terms *) - - (** The type of operators *) - type operator = - | Plus (** [+] *) - | Minus (** [-] *) - | Mult (** [*] *) - | Div (** [/] *) - | Modulo (** [mod] *) - - val make_int : Num.num -> t - (** [make_int n] creates an integer constant of value [n]. *) - - val make_real : Num.num -> t - (** [make_real n] creates an real constant of value [n]. *) - - val make_app : Symbol.t -> t list -> t - (** [make_app f l] creates the application of function symbol [f] to a list - of terms [l]. *) - - val make_arith : operator -> t -> t -> t - (** [make_arith op t1 t2] creates the term [t1 t2]. *) - - val make_ite : Formula.t -> t -> t -> t - (** [make_ite f t1 t2] creates the term [if f then t1 else t2]. *) - - val is_int : t -> bool - (** [is_int x] is [true] if the term [x] has type int *) - - val is_real : t -> bool - (** [is_real x] is [true] if the term [x] has type real *) - - val t_true : t - (** [t_true] is the boolean term [true] *) - - val t_false : t - (** [t_false] is the boolean term [false] *) - -end - - -(** {2 Building formulas} *) - -and Formula : sig - - (** The type of comparators: *) - type comparator = - | Eq (** equality ([=]) *) - | Neq (** disequality ([<>]) *) - | Le (** inequality ([<=]) *) - | Lt (** strict inequality ([<]) *) - - (** The type of operators *) - type combinator = - | And (** conjunction *) - | Or (** disjunction *) - | Imp (** implication *) - | Not (** negation *) - - (** The type of ground formulas *) - type t = - | Lit of Literal.LT.t - | Comb of combinator * t list - - val f_true : t - (** The formula which represents [true]*) - - val f_false : t - (** The formula which represents [false]*) - - val make_lit : comparator -> Term.t list -> t - (** [make_lit cmp [t1; t2]] creates the literal [(t1 t2)]. *) - - val make : combinator -> t list -> t - (** [make cmb [f_1; ...; f_n]] creates the formula - [(f_1 ... f_n)].*) - - val make_pred : ?sign:bool -> Term.t -> t - (** [make_pred p] builds the atomic formula [p = true]. - @param sign the polarity of the atomic formula *) - - val make_not : t -> t - val make_and : t list -> t - val make_or : t list -> t - val make_imply : t -> t -> t - val make_equiv : t -> t -> t - val make_xor : t -> t -> t - val make_eq : Term.t -> Term.t -> t - val make_neq : Term.t -> Term.t -> t - val make_le : Term.t -> Term.t -> t - val make_lt : Term.t -> Term.t -> t - val make_ge : Term.t -> Term.t -> t - val make_gt : Term.t -> Term.t -> t - - val make_cnf : t -> Literal.LT.t list list - (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a - list (which is a conjunction) of lists (which are disjunctions) of - literals. *) - - val print : Format.formatter -> t -> unit - (** [print fmt f] prints the formula on the formatter [fmt].*) - -end - -(** {2 The SMT solver} *) - -exception Unsat of int list -(** The exception raised by {! Smt.Solver.check} and {! Smt.Solver.assume} when - the formula is unsatisfiable. *) - -val set_cc : bool -> unit -(** set_cc [false] deactivates congruence closure algorithm - ([true] by default).*) - -module type Solver = sig - - (** This SMT solver is imperative in the sense that it maintains a global - context. To create different instances of Alt-Ergo Zero use the - functor {! Smt.Make}. - - A typical use of this solver is to do the following :{[ - clear (); - assume f_1; - ... - assume f_n; - check ();]} - *) - - type state - (** The type of the internal state of the solver (see {!save_state} and - {!restore_state}).*) - - - (** {2 Profiling functions} *) - - val get_time : unit -> float - (** [get_time ()] returns the cumulated time spent in the solver in seconds.*) - - val get_calls : unit -> int - (** [get_calls ()] returns the cumulated number of calls to {! check}.*) - - (** {2 Main API of the solver} *) - - val clear : unit -> unit - (** [clear ()] clears the context of the solver. Use this after {! check} - raised {! Unsat} or if you want to restart the solver. *) - - - val assume : ?profiling:bool -> id:int -> Formula.t -> unit - (** [assume ~profiling:b f id] adds the formula [f] to the context of the - solver with identifier [id]. - This function only performs unit propagation. - - @param profiling if set to [true] then profiling information (time) will - be computed (expensive because of system calls). - - {b Raises} {! Unsat} if the context becomes inconsistent after unit - propagation. *) - - val check : ?profiling:bool -> unit -> unit - (** [check ()] runs Alt-Ergo Zero on its context. If [()] is - returned then the context is satifiable. - - @param profiling if set to [true] then profiling information (time) will - be computed (expensive because of system calls). - - {b Raises} {! Unsat} [[id_1; ...; id_n]] if the context is unsatisfiable. - [id_1, ..., id_n] is the unsat core (returned as the identifiers of the - formulas given to the solver). *) - - val eval : Term.t -> bool - (** [eval lit] returns the current truth value for the literal. The term - must be a boolean proposition that occurred in the problem, - because the only information returned by [eval] is its boolean - truth value in the current model (no theories!). - - @raise Invalid_argument if the context is not checked or if it's - unsatisfiable. - @raise Error if the term isn't a known propositional atom. *) - - val save_state : unit -> state - (** [save_state ()] returns a {b copy} of the current state of the solver.*) - - val restore_state : state -> unit - (** [restore_state s] restores a previously saved state [s].*) - - val entails : ?profiling:bool -> id:int -> Formula.t -> bool - (** [entails ~id f] returns [true] if the context of the solver entails - the formula [f]. It doesn't modify the context of the solver (the state - is saved when this function is called and restored on exit).*) - -end - -(** Functor to create several instances of the solver *) -module Make (Dummy : sig end) : Solver - diff --git a/old/sum.ml b/old/sum.ml deleted file mode 100644 index 15939786..00000000 --- a/old/sum.ml +++ /dev/null @@ -1,240 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Format -open Sig -open Exception -module Sy = Symbols -module T = Term -module A = Literal -module L = List -module Hs = Hstring -module Ex = Explanation - -type 'a abstract = Cons of Hs.t * Ty.t | Alien of 'a - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Make(X : ALIEN) = struct - - type t = X.r abstract - type r = X.r - - let name = "Sum" - - let unsolvable _ = false - - let is_mine_a _ = false - - let is_mine_symb = function - | Sy.Name(_, Sy.Constructor) -> true - | _ -> false - - let fully_interpreted sb = true - - let type_info = function - | Cons (_, ty) -> ty - | Alien x -> X.type_info x - - let is_mine_type c = match type_info c with - | Ty.Tsum _ -> true - | _ -> false - - let color _ = assert false - - let print fmt = function - | Cons (hs,ty) -> fprintf fmt "%s" (Hs.view hs) - | Alien x -> fprintf fmt "%a" X.print x - - let embed r = - match X.extract r with - | Some c -> c - | None -> Alien r - - let is_mine = function - | Alien r -> r - | Cons(hs,ty) as c -> X.embed c - - let compare c1 c2 = - match c1 , c2 with - | Cons (h1,ty1) , Cons (h2,ty2) -> - let n = Hs.compare h1 h2 in - if n <> 0 then n else Ty.compare ty1 ty2 - | Alien r1, Alien r2 -> X.compare r1 r2 - | Alien _ , Cons _ -> 1 - | Cons _ , Alien _ -> -1 - - let hash = function - | Cons (h, ty) -> Hstring.hash h + 19 * Ty.hash ty - | Alien r -> X.hash r - - let leaves _ = [] - - let subst p v c = - let cr = is_mine c in - if X.equal p cr then v - else - match c with - | Cons(hs,t) -> cr - | Alien r -> X.subst p v r - - let make t = match T.view t with - | {T.f=Sy.Name(hs, Sy.Constructor); xs=[];ty=ty} -> - is_mine (Cons(hs,ty)), [] - | _ -> assert false - - let solve a b = - match embed a, embed b with - | Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> [] - | Cons(c1,_) , Cons(c2,_) -> raise Unsolvable - | Cons _ , Alien r2 -> [r2,a] - | Alien r1 , Cons _ -> [r1,b] - | Alien _ , Alien _ -> assert false - - let term_extract _ = None - - module Rel = struct - type r = X.r - - exception Not_Cons - - module Ex = Explanation - - module MX = Map.Make(struct type t = X.r include X end) - module HSS = Set.Make (struct type t=Hs.t let compare = Hs.compare end) - - type t = (HSS.t * Ex.t) MX.t - - let empty () = MX.empty - - module Debug = struct - - let assume bol r1 r2 = () - - let print_env env = () - - end - - let values_of r = match X.type_info r with - | Ty.Tsum (_,l) -> - Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l) - | _ -> None - - let add_diseq hss sm1 sm2 dep env eqs = - match sm1, sm2 with - | Alien r , Cons(h,ty) - | Cons (h,ty), Alien r -> - let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in - let enum = HSS.remove h enum in - let ex = Ex.union ex dep in - if HSS.is_empty enum then raise (Inconsistent ex) - else - let env = MX.add r (enum, ex) env in - if HSS.cardinal enum = 1 then - let h' = HSS.choose enum in - env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs - else env, eqs - - | Alien r1 , Alien r2 -> env, eqs - | _ -> env, eqs - - let add_eq hss sm1 sm2 dep env eqs = - match sm1, sm2 with - | Alien r, Cons(h,ty) | Cons (h,ty), Alien r -> - - let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in - let ex = Ex.union ex dep in - if not (HSS.mem h enum) then raise (Inconsistent ex); - MX.add r (HSS.singleton h, ex) env, eqs - - | Alien r1, Alien r2 -> - - let enum1,ex1 = try MX.find r1 env with Not_found -> hss, Ex.empty in - let enum2,ex2 = try MX.find r2 env with Not_found -> hss, Ex.empty in - let ex = Ex.union dep (Ex.union ex1 ex2) in - let diff = HSS.inter enum1 enum2 in - if HSS.is_empty diff then raise (Inconsistent ex); - let env = MX.add r1 (diff, ex) env in - let env = MX.add r2 (diff, ex) env in - if HSS.cardinal diff = 1 then - let h' = HSS.choose diff in - let ty = X.type_info r1 in - env, (LSem (A.Eq(r1, is_mine (Cons(h',ty)))), ex)::eqs - else env, eqs - - | _ -> env, eqs - - let assume env la = - let aux bol r1 r2 dep env eqs = function - | None -> env, eqs - | Some hss -> - Debug.assume bol r1 r2; - if bol then - add_eq hss (embed r1) (embed r2) dep env eqs - else - add_diseq hss (embed r1) (embed r2) dep env eqs - in - Debug.print_env env; - let env, eqs = - List.fold_left - (fun (env,eqs) -> function - | A.Eq(r1,r2), _, ex -> - aux true r1 r2 ex env eqs (values_of r1) - - | A.Distinct(false, [r1;r2]), _, ex -> - aux false r1 r2 ex env eqs (values_of r1) - - | _ -> env, eqs - - ) (env,[]) la - in - env, { assume = eqs; remove = [] } - - (* XXXXXX : TODO -> ajouter les explications dans les choix du - case split *) - - let case_split env = - let acc = MX.fold - (fun r (hss, ex) acc -> - let sz = HSS.cardinal hss in - if sz = 1 then acc - else match acc with - | Some (n,r,hs) when n <= sz -> acc - | _ -> Some (sz, r, HSS.choose hss) - ) env None - in - match acc with - | Some (n,r,hs) -> - let r' = is_mine (Cons(hs,X.type_info r)) in - [A.Eq(r, r'), Ex.empty, Num.Int n] - | None -> [] - - - let query env a_ex = - try ignore(assume env [a_ex]); Sig.No - with Inconsistent expl -> Sig.Yes expl - - let add env r = match embed r, values_of r with - | Alien r, Some hss -> - if MX.mem r env then env else - MX.add r (hss, Ex.empty) env - - | _ -> env - - end -end diff --git a/old/sum.mli b/old/sum.mli deleted file mode 100644 index 2cd4bdbf..00000000 --- a/old/sum.mli +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Alain Mebsout *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type 'a abstract - -module type ALIEN = sig - include Sig.X - val embed : r abstract -> r - val extract : r -> (r abstract) option -end - -module Make - (X : ALIEN) : Sig.THEORY with type r = X.r and type t = X.r abstract - diff --git a/old/symbols.ml b/old/symbols.ml deleted file mode 100644 index fba3dfdb..00000000 --- a/old/symbols.ml +++ /dev/null @@ -1,91 +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 Hashcons - -type operator = - | Plus | Minus | Mult | Div | Modulo - -type name_kind = Ac | Constructor | Other - -type t = - | True - | False - | Name of Hstring.t * name_kind - | Int of Hstring.t - | Real of Hstring.t - | Op of operator - | Var of Hstring.t - -let name ?(kind=Other) s = Name (s, kind) -let var s = Var (Hstring.make s) -let int i = Int (Hstring.make i) -let real r = Real (Hstring.make r) - - -let is_ac = function - | Name(_, Ac) -> true - | _ -> false - -let compare_kind k1 k2 = match k1, k2 with - | Ac , Ac -> 0 - | Ac , _ -> 1 - | _ , Ac -> -1 - | Other, Other -> 0 - | Other, _ -> 1 - | _ , Other -> -1 - | Constructor, Constructor -> 0 - -let compare s1 s2 = match s1, s2 with - | Name (n1,k1), Name (n2,k2) -> - let c = compare_kind k1 k2 in - if c = 0 then Hstring.compare n1 n2 else c - | Name _, _ -> -1 - | _, Name _ -> 1 - | Var n1, Var n2 -> Hstring.compare n1 n2 - | Var _, _ -> -1 - | _ ,Var _ -> 1 - | Int i1, Int i2 -> Hstring.compare i1 i2 - | Int _, _ -> -1 - | _ ,Int _ -> 1 - | _ -> Pervasives.compare s1 s2 - -let equal s1 s2 = compare s1 s2 = 0 - -let hash = function - | Name (n,Ac) -> Hstring.hash n * 19 + 1 - | Name (n,_) -> Hstring.hash n * 19 - | Var n (*| Int n*) -> Hstring.hash n * 19 + 1 - | s -> Hashtbl.hash s - -let to_string = function - | Name (n,_) -> Hstring.view n - | Var x -> "*var* "^(Hstring.view x) - | Int n -> Hstring.view n - | Real n -> Hstring.view n - | Op Plus -> "+" - | Op Minus -> "-" - | Op Mult -> "*" - | Op Div -> "/" - | Op Modulo -> "%" - | True -> "true" - | False -> "false" - -let print fmt s = Format.fprintf fmt "%s" (to_string s) - -module Map = - Map.Make(struct type t' = t type t=t' let compare=compare end) - -module Set = - Set.Make(struct type t' = t type t=t' let compare=compare end) - diff --git a/old/symbols.mli b/old/symbols.mli deleted file mode 100644 index 97494b82..00000000 --- a/old/symbols.mli +++ /dev/null @@ -1,43 +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 *) -(* *) -(**************************************************************************) - -type operator = - | Plus | Minus | Mult | Div | Modulo - -type name_kind = Ac | Constructor | Other - -type t = - | True - | False - | Name of Hstring.t * name_kind - | Int of Hstring.t - | Real of Hstring.t - | Op of operator - | Var of Hstring.t - -val name : ?kind:name_kind -> Hstring.t -> t -val var : string -> t -val int : string -> t -val real : string -> t - -val is_ac : t -> bool - -val equal : t -> t -> bool -val compare : t -> t -> int -val hash : t -> int - -val print : Format.formatter -> t -> unit - -module Map : Map.S with type key = t -module Set : Set.S with type elt = t - diff --git a/old/term.ml b/old/term.ml deleted file mode 100644 index 22062c4e..00000000 --- a/old/term.ml +++ /dev/null @@ -1,82 +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 Format -open Hashcons - -module Sy = Symbols - -type view = {f: Sy.t ; xs: t list; ty: Ty.t; tag: int} -and t = view - -module H = struct - type t = view - let equal t1 t2 = try - Sy.equal t1.f t2.f - && List.for_all2 (==) t1.xs t2.xs - && Ty.equal t1.ty t2.ty - with Invalid_argument _ -> false - - let hash t = - abs (List.fold_left - (fun acc x-> acc*19 +x.tag) (Sy.hash t.f + Ty.hash t.ty) - t.xs) - let tag tag x = {x with tag = tag} -end - -module T = Make(H) - -let view t = t - -let rec print fmt t = - let {f=x; xs=l; ty=ty} = view t in - match x, l with - | Sy.Op op, [e1; e2] -> - fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2 - | _, [] -> fprintf fmt "%a" Sy.print x - | _, _ -> fprintf fmt "%a(%a)" Sy.print x print_list l - -and print_list fmt = function - | [] -> () - | [t] -> print fmt t - | t::l -> Format.fprintf fmt "%a,%a" print t print_list l - -let compare t1 t2 = - let c = Pervasives.compare t2.tag t1.tag in - if c = 0 then c else - match (view t1).f, (view t2).f with - | (Sy.True | Sy.False ), (Sy.True | Sy.False ) -> c - | (Sy.True | Sy.False ), _ -> -1 - | _, (Sy.True | Sy.False ) -> 1 - | _,_ -> c - -let make s l ty = T.hashcons {f=s;xs=l;ty=ty;tag=0 (* dumb_value *) } - -let true_ = make (Sy.True) [] Ty.Tbool -let false_ = make (Sy.False) [] Ty.Tbool - -let int i = make (Sy.int i) [] Ty.Tint -let real r = make (Sy.real r) [] Ty.Treal - -let is_int t = (view t).ty= Ty.Tint -let is_real t = (view t).ty= Ty.Treal - -let equal t1 t2 = t1 == t2 - -let hash t = t.tag - -module Set = - Set.Make(struct type t' = t type t=t' let compare=compare end) - -module Map = - Map.Make(struct type t' = t type t=t' let compare=compare end) diff --git a/old/term.mli b/old/term.mli deleted file mode 100644 index 9d3d39cb..00000000 --- a/old/term.mli +++ /dev/null @@ -1,36 +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 *) -(* *) -(**************************************************************************) - -type t -type view = private {f: Symbols.t ; xs: t list; ty: Ty.t; tag : int} - -val view : t -> view -val make : Symbols.t -> t list -> Ty.t -> t - -val true_ : t -val false_ : t -val int : string -> t -val real : string -> t - -val is_int : t -> bool -val is_real : t -> bool - -val compare : t -> t -> int -val equal : t -> t -> bool -val hash : t -> int - -val print : Format.formatter -> t -> unit - -module Map : Map.S with type key = t -module Set : Set.S with type elt = t - diff --git a/old/ty.ml b/old/ty.ml deleted file mode 100644 index 922fc047..00000000 --- a/old/ty.ml +++ /dev/null @@ -1,58 +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 Format - -type t = - | Tint - | Treal - | Tbool - | Tabstract of Hstring.t - | Tsum of Hstring.t * Hstring.t list - -let hash t = - match t with - | Tabstract s -> Hstring.hash s - | Tsum (s, l) -> - let h = - List.fold_left - (fun h x -> 13 * h + Hstring.hash x) (Hstring.hash s) l - in - abs h - | _ -> Hashtbl.hash t - -let equal t1 t2 = - match t1, t2 with - | Tabstract s1, Tabstract s2 - | Tsum (s1, _), Tsum (s2, _) -> - Hstring.equal s1 s2 - | Tint, Tint | Treal, Treal | Tbool, Tbool -> true - | _ -> false - -let compare t1 t2 = - match t1, t2 with - | Tabstract s1, Tabstract s2 -> - Hstring.compare s1 s2 - | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 - | Tsum (s1, _), Tsum(s2, _) -> - Hstring.compare s1 s2 - | Tsum _, _ -> -1 | _ , Tsum _ -> 1 - | t1, t2 -> Pervasives.compare t1 t2 - -let print fmt ty = - match ty with - | Tint -> fprintf fmt "int" - | Treal -> fprintf fmt "real" - | Tbool -> fprintf fmt "bool" - | Tabstract s -> fprintf fmt "%s" (Hstring.view s) - | Tsum (s, _) -> fprintf fmt "%s" (Hstring.view s) diff --git a/old/ty.mli b/old/ty.mli deleted file mode 100644 index b821aeb5..00000000 --- a/old/ty.mli +++ /dev/null @@ -1,24 +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 *) -(* *) -(**************************************************************************) - -type t = - | Tint - | Treal - | Tbool - | Tabstract of Hstring.t - | Tsum of Hstring.t * Hstring.t list - -val hash : t -> int -val equal : t -> t -> bool -val compare : t -> t -> int -val print : Format.formatter -> t -> unit diff --git a/old/uf.ml b/old/uf.ml deleted file mode 100644 index bc4919c6..00000000 --- a/old/uf.ml +++ /dev/null @@ -1,359 +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 Format -open Exception -open Sig - -module type S = sig - type t - - module R : Sig.X - - 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 : Sig.X ) = struct - - module L = List - module HS = Hstring - 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) - - - type t = { - - (* term -> [t] *) - make : R.r MapT.t; - - (* representative table *) - repr : (R.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 = - L.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 = - L.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 - 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 x_solve env r1 r2 dep = - 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 dep = Ex.union dep (Ex.union ex_r1 ex_r2) in - if R.equal rr1 rr2 then begin - [] (* Remove rule *) - end - else - begin - ignore (Env.update_neqs rr1 rr2 dep env); - try R.solve rr1 rr2 - with Unsolvable -> - raise (Inconsistent dep) - end - - let rec ac_x eqs env tch = - if Queue.is_empty eqs then env, tch - else - let r1, r2, dep = Queue.pop eqs in - let sbs = x_solve env r1 r2 dep in - let env, tch = List.fold_left (ac_solve eqs dep) (env, tch) sbs in - ac_x eqs env tch - - let union env r1 r2 dep = - let equations = Queue.create () in - Queue.push (r1,r2, dep) equations; - ac_x equations env [] - - 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] - - -end diff --git a/old/uf.mli b/old/uf.mli deleted file mode 100644 index 09a70012..00000000 --- a/old/uf.mli +++ /dev/null @@ -1,42 +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 *) -(* *) -(**************************************************************************) - -module type S = sig - type t - - module R : Sig.X - - 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 : Sig.X ) : S with module R = X diff --git a/old/use.ml b/old/use.ml deleted file mode 100644 index 69d39f0f..00000000 --- a/old/use.ml +++ /dev/null @@ -1,83 +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 *) -(* *) -(**************************************************************************) - -module F = Format -module L = List -module T = Term -module S = Symbols -module ST = T.Set -(* module SA = Literal.LT.Set *) - -module SA = Set.Make(struct - type t = Literal.LT.t * Explanation.t - let compare (s1,_) (s2,_) = Literal.LT.compare s1 s2 - end) - -type elt = ST.t * SA.t - -module Make (X : Sig.X) = struct - - let inter_tpl (x1,y1) (x2,y2) = ST.inter x1 x2, SA.inter y1 y2 - let union_tpl (x1,y1) (x2,y2) = ST.union x1 x2, SA.union y1 y2 - let bottom = Hstring.make "@bottom" - let leaves r = - let one, _ = X.make (T.make (Symbols.name bottom) [] Ty.Tint) in - match X.leaves r with [] -> [one] | l -> l - - module G = Map.Make(struct type t = X.r include X end) - - open G - - type t = elt G.t - - - let find k m = try find k m with Not_found -> (ST.empty,SA.empty) - - let add_term k t mp = - let g_t,g_a = find k mp in add k (ST.add t g_t,g_a) mp - - let up_add g t rt lvs = - let g = if mem rt g then g else add rt (ST.empty, SA.empty) g in - L.fold_left (fun g x -> add_term x t g) g lvs - - let congr_add g lvs = - match lvs with - [] -> ST.empty - | x::ls -> - L.fold_left - (fun acc y -> ST.inter (fst(find y g)) acc) - (fst(find x g)) ls - - let up_close_up g p v = - let lvs = leaves v in - let g_p = find p g in - L.fold_left (fun gg l -> add l (union_tpl g_p (find l g)) gg) g lvs - - let congr_close_up g p touched = - let inter = function - [] -> (ST.empty, SA.empty) - | rx::l -> - L.fold_left (fun acc x ->inter_tpl acc (find x g))(find rx g) l - in - L.fold_left - (fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch))) - (find p g) touched - - let print g = () - - let mem = G.mem - let add = G.add - let empty = G.empty - -end diff --git a/old/use.mli b/old/use.mli deleted file mode 100644 index d6f27b1b..00000000 --- a/old/use.mli +++ /dev/null @@ -1,38 +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 *) -(* *) -(**************************************************************************) - -module T : sig type t = Term.t end -module S : sig type t = Symbols.t end -module ST : sig type elt = T.t type t = Term.Set.t end -module SA : Set.S with type elt = Literal.LT.t * Explanation.t - -type elt = ST.t * SA.t - -module Make : - functor (X : Sig.X) -> - sig - - type t - val empty : t - val find : X.r -> t -> elt - val add : X.r -> elt -> t -> t - val mem : X.r -> t -> bool - val print : t -> unit - val up_add : t -> ST.elt -> X.r -> X.r list -> t - - val congr_add : t -> X.r list -> ST.t - - val up_close_up :t -> X.r -> X.r -> t - val congr_close_up : t -> X.r -> X.r list -> elt - end