From 13060e348de4a09ba3e4eeb69567a14526c0a42a Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 29 Oct 2014 14:55:23 +0100 Subject: [PATCH] Removed trailing whitespaces --- common/heap.ml | 14 +- common/heap.mli | 2 +- common/hstring.ml | 10 +- common/hstring.mli | 4 +- common/iheap.ml | 46 +++---- common/timer.ml | 8 +- common/timer.mli | 2 +- common/vec.ml | 34 ++--- smt/arith.ml | 198 ++++++++++++++-------------- smt/arith.mli | 4 +- smt/cc.ml | 190 +++++++++++++------------- smt/cc.mli | 2 +- smt/combine.ml | 124 ++++++++--------- smt/explanation.ml | 22 ++-- smt/fm.ml | 308 +++++++++++++++++++++---------------------- smt/fm.mli | 4 +- smt/intervals.ml | 198 ++++++++++++++-------------- smt/intervals.mli | 2 +- smt/literal.ml | 78 +++++------ smt/literal.mli | 4 +- smt/polynome.ml | 100 +++++++------- smt/polynome.mli | 10 +- smt/sig.mli | 34 ++--- smt/smt.ml | 270 ++++++++++++++++++------------------- smt/smt.mli | 46 +++---- smt/solver.ml | 266 ++++++++++++++++++------------------- smt/solver_types.ml | 80 +++++------ smt/solver_types.mli | 14 +- smt/sum.ml | 86 ++++++------ smt/sum.mli | 2 +- smt/symbols.ml | 18 +-- smt/symbols.mli | 8 +- smt/term.ml | 26 ++-- smt/ty.ml | 18 +-- smt/ty.mli | 2 +- smt/uf.ml | 206 ++++++++++++++--------------- smt/uf.mli | 4 +- smt/use.ml | 42 +++--- smt/use.mli | 12 +- 39 files changed, 1249 insertions(+), 1249 deletions(-) diff --git a/common/heap.ml b/common/heap.ml index ac93b9b4..8b0467e5 100644 --- a/common/heap.ml +++ b/common/heap.ml @@ -21,8 +21,8 @@ end module type S = sig type t - type elem - + type elem + val empty : t val pop : t -> elem * t val add : t -> elem list -> t @@ -37,22 +37,22 @@ module Make ( X : OrderType ) = struct let empty = Empty - let rec fusion t1 t2 = + let rec fusion t1 t2 = match t1, t2 with | _ , Empty -> t1 | Empty , _ -> t2 | Node (m1, g1, d1), Node (m2, g2, d2) -> if X.compare m1 m2 <= 0 then Node (m1, d1, fusion g1 t2) else Node (m2, d2, fusion g2 t1) - + let pop = function | Empty -> raise EmptyHeap | Node(m, g, d) -> m, fusion g d - let add h l = + let add h l = List.fold_left (fun h x -> fusion (Node(x, Empty, Empty)) h ) h l - - let elements h = + + let elements h = let rec elements_aux acc = function | Empty -> acc | Node (m1 ,g1 ,d1) -> elements_aux (m1 :: acc) (fusion g1 d1) diff --git a/common/heap.mli b/common/heap.mli index 0a52ec3c..ea188db1 100644 --- a/common/heap.mli +++ b/common/heap.mli @@ -21,7 +21,7 @@ end module type S = sig type t - type elem + type elem val empty : t val pop : t -> elem * t diff --git a/common/hstring.ml b/common/hstring.ml index 88a342b2..9af5b310 100644 --- a/common/hstring.ml +++ b/common/hstring.ml @@ -13,9 +13,9 @@ open Hashcons -module S = - Hashcons.Make_consed(struct include String - let hash = Hashtbl.hash +module S = + Hashcons.Make_consed(struct include String + let hash = Hashtbl.hash let equal = (=) end) module HS = struct @@ -38,7 +38,7 @@ module HS = struct | [] -> raise Not_found | (y, v) :: l -> if equal x y then v else list_assoc x l - let rec list_mem_assoc x = function + let rec list_mem_assoc x = function | [] -> false | (y, _) :: l -> compare x y = 0 || list_mem_assoc x l @@ -65,7 +65,7 @@ module HS = struct | [] -> false | d :: l -> compare_couple c d = 0 || list_mem_couple c l - let print fmt s = + let print fmt s = Format.fprintf fmt "%s" (view s) end diff --git a/common/hstring.mli b/common/hstring.mli index 78937bd9..33a39652 100644 --- a/common/hstring.mli +++ b/common/hstring.mli @@ -14,14 +14,14 @@ (** {b Hash-consed strings} Hash-consing is a technique to share values that are structurally - equal. More details on + equal. More details on {{:http://en.wikipedia.org/wiki/Hash_consing} Wikipedia} and {{:http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf} here}. This module provides an easy way to use hash-consing for strings. *) -open Hashcons +open Hashcons type t = string hash_consed (** The type of Hash-consed string *) diff --git a/common/iheap.ml b/common/iheap.ml index 5fed4910..63e12aa5 100644 --- a/common/iheap.ml +++ b/common/iheap.ml @@ -12,27 +12,27 @@ (**************************************************************************) type t = {heap : int Vec.t; indices : int Vec.t } - + let dummy = -100 -let init sz = +let init sz = { heap = Vec.init sz (fun i -> i) dummy; indices = Vec.init sz (fun i -> i) dummy} - + let left i = (i lsl 1) + 1 (* i*2 + 1 *) let right i = (i + 1) lsl 1 (* (i+1)*2 *) let parent i = (i - 1) asr 1 (* (i-1) / 2 *) (* -let rec heap_property cmp ({heap=heap} as s) i = - i >= (Vec.size heap) || +let rec heap_property cmp ({heap=heap} as s) i = + i >= (Vec.size heap) || ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) && heap_property cmp s (left i) && heap_property cmp s (right i)) - + let heap_property cmp s = heap_property cmp s 1 *) - -let percolate_up cmp {heap=heap;indices=indices} i = + +let percolate_up cmp {heap=heap;indices=indices} i = let x = Vec.get heap i in let pi = ref (parent i) in let i = ref i in @@ -45,7 +45,7 @@ let percolate_up cmp {heap=heap;indices=indices} i = Vec.set heap !i x; Vec.set indices x !i -let percolate_down cmp {heap=heap;indices=indices} i = +let percolate_down cmp {heap=heap;indices=indices} i = let x = Vec.get heap i in let sz = Vec.size heap in let li = ref (left i) in @@ -53,9 +53,9 @@ let percolate_down cmp {heap=heap;indices=indices} i = let i = ref i in (try while !li < sz do - let child = + let child = if !ri < sz && cmp (Vec.get heap !ri) (Vec.get heap !li) then !ri - else !li + else !li in if not (cmp (Vec.get heap child) x) then raise Exit; Vec.set heap !i (Vec.get heap child); @@ -70,13 +70,13 @@ let percolate_down cmp {heap=heap;indices=indices} i = let in_heap s n = n < Vec.size s.indices && Vec.get s.indices n >= 0 -let decrease cmp s n = +let decrease cmp s n = assert (in_heap s n); percolate_up cmp s (Vec.get s.indices n) - -let increase cmp s n = + +let increase cmp s n = assert (in_heap s n); percolate_down cmp s (Vec.get s.indices n) -let filter s filt cmp = +let filter s filt cmp = let j = ref 0 in let lim = Vec.size s.heap in for i = 0 to lim - 1 do @@ -93,36 +93,36 @@ let filter s filt cmp = done let size s = Vec.size s.heap - + let is_empty s = Vec.is_empty s.heap - + let insert cmp s n = - if not (in_heap s n) then + if not (in_heap s n) then begin Vec.set s.indices n (Vec.size s.heap); Vec.push s.heap n; percolate_up cmp s (Vec.get s.indices n) end -let grow_to_by_double s sz = +let grow_to_by_double s sz = Vec.grow_to_by_double s.indices sz; Vec.grow_to_by_double s.heap sz (* -let update cmp s n = +let update cmp s n = assert (heap_property cmp s); begin - if in_heap s n then + if in_heap s n then begin percolate_up cmp s (Vec.get s.indices n); percolate_down cmp s (Vec.get s.indices n) - end + end else insert cmp s n end; assert (heap_property cmp s) *) -let remove_min cmp ({heap=heap; indices=indices} as s) = +let remove_min cmp ({heap=heap; indices=indices} as s) = let x = Vec.get heap 0 in Vec.set heap 0 (Vec.last heap); (*heap.last()*) Vec.set indices (Vec.get heap 0) 0; diff --git a/common/timer.ml b/common/timer.ml index 8f3e9a2f..4122d1ba 100644 --- a/common/timer.ml +++ b/common/timer.ml @@ -14,22 +14,22 @@ module type S = sig val start : unit -> unit val pause : unit -> unit - val get : unit -> float + val get : unit -> float end module Make (X : sig end) = struct open Unix - + let u = ref 0.0 let cpt = ref 0.0 - + let start () = u:=(times()).tms_utime let pause () = cpt := !cpt +. ((times()).tms_utime -. !u) - let get () = + let get () = !cpt end diff --git a/common/timer.mli b/common/timer.mli index 775be40b..7e244b57 100644 --- a/common/timer.mli +++ b/common/timer.mli @@ -14,7 +14,7 @@ module type S = sig val start : unit -> unit val pause : unit -> unit - val get : unit -> float + val get : unit -> float end module Make (X : sig end) : S diff --git a/common/vec.ml b/common/vec.ml index 4ac1af97..a9522789 100644 --- a/common/vec.ml +++ b/common/vec.ml @@ -12,20 +12,20 @@ (**************************************************************************) type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int } - + let make capa d = {data = Array.make capa d; sz = 0; dummy = d} let init capa f d = {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} let from_array data sz d = {data = data; sz = sz; dummy = d} -let from_list l sz d = +let from_list l sz d = let l = ref l in let f_init i = match !l with [] -> assert false | e::r -> l := r; e in {data = Array.init sz f_init; sz = sz; dummy = d} let clear s = s.sz <- 0 - + let shrink t i = assert (i >= 0 && i<=t.sz); t.sz <- t.sz - i let pop t = assert (t.sz >=1); t.sz <- t.sz - 1 @@ -34,14 +34,14 @@ let size t = t.sz let is_empty t = t.sz = 0 -let grow_to t new_capa = +let grow_to t new_capa = let data = t.data in let capa = Array.length data in t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy) let grow_to_double_size t = grow_to t (2* Array.length t.data) -let rec grow_to_by_double t new_capa = +let rec grow_to_by_double t new_capa = let data = t.data in let capa = ref (Array.length data + 1) in while !capa < new_capa do capa := 2 * !capa done; @@ -50,35 +50,35 @@ let rec grow_to_by_double t new_capa = let is_full t = Array.length t.data = t.sz -let push t e = +let push t e = (*Format.eprintf "push; sz = %d et capa=%d@." t.sz (Array.length t.data);*) if is_full t then grow_to_double_size t; t.data.(t.sz) <- e; t.sz <- t.sz + 1 -let push_none t = +let push_none t = if is_full t then grow_to_double_size t; t.data.(t.sz) <- t.dummy; t.sz <- t.sz + 1 - -let last t = + +let last t = let e = t.data.(t.sz - 1) in assert (not (e == t.dummy)); e -let get t i = +let get t i = assert (i < t.sz); let e = t.data.(i) in if e == t.dummy then raise Not_found else e - -let set t i v = + +let set t i v = t.data.(i) <- v; t.sz <- max t.sz (i + 1) let set_size t sz = t.sz <- sz -let copy t = +let copy t = let data = t.data in let len = Array.length data in let data = Array.init len (fun i -> data.(i)) in @@ -92,15 +92,15 @@ let move_to t t' = t'.sz <- t.sz -let remove t e = +let remove t e = let j = ref 0 in while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; assert (!j < t.sz); for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done; pop t - -let fast_remove t e = + +let fast_remove t e = let j = ref 0 in while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; assert (!j < t.sz); @@ -108,7 +108,7 @@ let fast_remove t e = pop t -let sort t f = +let sort t f = let sub_arr = Array.sub t.data 0 t.sz in Array.fast_sort f sub_arr; t.data <- sub_arr diff --git a/smt/arith.ml b/smt/arith.ml index fd6cf229..3d331f07 100644 --- a/smt/arith.ml +++ b/smt/arith.ml @@ -19,7 +19,7 @@ module A = Literal module Sy = Symbols module T = Term -let ale = Hstring.make "<=" +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 @@ -34,7 +34,7 @@ module Type (X:Sig.X) : Polynome.T with type r = X.r = struct end -module Make +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 @@ -42,56 +42,56 @@ module Make type t = P.t type r = P.r - + let name = "arith" - let is_mine_a a = + 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.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 + 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) + | _ -> P.create [Int 1, r] (Int 0) (X.type_info r) - let check_int exn p = + 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 fresh_string = let cpt = ref 0 in fun () -> incr cpt; "!k" ^ (string_of_int !cpt) - let fresh_name () = + let fresh_name () = T.make (Sy.name (Hstring.make (fresh_string()))) [] Ty.Tint - (* t1 % t2 = md <-> + (* 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 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 @@ -99,9 +99,9 @@ module Make 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 + c3 :: c2 :: c1 :: ctx - let mk_euc_division p p2 t1 t2 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 @@ -113,7 +113,7 @@ module Make 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), _ -> + | (Sy.Int n | Sy.Real n), _ -> let c = coef */ (num_of_string (Hstring.view n)) in P.add (P.create [] c ty) p, ctx @@ -122,43 +122,43 @@ module Make 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] -> + | 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 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 -> + 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] -> + | 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] -> + | 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] -> + | 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 = + let p3, ctx = try P.modulo p1 p2, ctx with e -> - let t = T.make mod_symb [t1; t2] Ty.Tint in + 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 + | _ -> 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 @@ -173,8 +173,8 @@ module Make | [Int 1, x] , Int 0 -> p | l , c -> let ty = P.type_info p in - let l = - List.fold_left + 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 @@ -182,14 +182,14 @@ module Make | 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 + 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 + )[] l + in P.create l c ty *) let make t = @@ -201,12 +201,12 @@ module Make 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 + 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 = + and nb_vars_in_alien r = match C.extract r with - | Some p -> + | 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 @@ -223,23 +223,23 @@ module Make 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 = + + let xs_of_list = List.fold_left (fun s x -> XS.add x s) XS.empty - - let rec leaves p = - let s = + + 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 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 = + let p = List.fold_left (fun p (ai, xi) -> let xi' = X.subst x t xi in @@ -249,7 +249,7 @@ module Make in P.add p p') (P.create [] c ty) l - in + in check_int (Exception.Unsolvable) p; is_mine p @@ -259,32 +259,32 @@ module Make let hash = P.hash (* symmetric modulo p 131 *) - let mod_sym a b = - let m = mod_num a b in - let m = + 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 + else if m <=/ b then m else assert false - + in if m + (fun acc (a,x) -> let a = f a in if a =/ Int 0 then acc else (a, x) :: acc) - [ax] l + [ax] l - let apply_subst sb v = + 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 + 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 @@ -293,43 +293,43 @@ module Make ([], []) 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 + | (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) + 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 + let rec omega l b = - (* 2. substituer les aliens plus grand que x pour + (* 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 -> + | Int 1 -> (* 3.1. si a = 1 alors on a une substitution entiere pour x *) - let p = mult_const p (Int (-1)) in + let p = mult_const p (Int (-1)) in (x, is_mine p) :: (is_mine_p sbs) - - | Int (-1) -> + + | 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 + 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) @@ -338,28 +338,28 @@ module Make 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 : + (* 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. + + (* 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 @@ -370,7 +370,7 @@ module Make let sbs2 = List.filter (fun (y, _) -> y <> sigma) sbs2 in List.rev_append sbs sbs2 - and solve_int p = + 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 @@ -379,29 +379,29 @@ module Make 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 is_null p = + if snd (P.to_list p) <>/ (Int 0) then raise Exception.Unsolvable; [] - let solve_int p = + 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 + let p = + P.mult (P.create [] ((Int (-1)) // a) (P.type_info p)) - (P.remove x p) + (P.remove x p) in [x, is_mine p] with Not_found -> is_null p - - let safe_distribution 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)) + (fun p (coef, x) -> P.add p (P.create [coef,x] (Int 0) ty)) (P.create [] c ty) l let solve_aux r1 r2 = @@ -418,18 +418,18 @@ module Make let print = P.print - let fully_interpreted sb = + let fully_interpreted sb = match sb with | Sy.Op (Sy.Plus | Sy.Minus) -> true | _ -> false let term_extract _ = None - module Rel = Fm.Make (X) + module Rel = Fm.Make (X) (struct - include P + include P let poly_of = embed let alien_of = is_mine end) - + end diff --git a/smt/arith.mli b/smt/arith.mli index 4c47b555..33ec6d8f 100644 --- a/smt/arith.mli +++ b/smt/arith.mli @@ -14,8 +14,8 @@ module Type (X : Sig.X ): Polynome.T with type r = X.r -module Make +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 + (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/smt/cc.ml b/smt/cc.ml index 68b5287a..f9cedc56 100644 --- a/smt/cc.ml +++ b/smt/cc.ml @@ -26,13 +26,13 @@ module type S = sig module TimerCC : Timer.S val empty : unit -> t - val assume : cs:bool -> + 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 Make (X : Sig.X) = struct module TimerCC = Timer.Make(struct end) @@ -47,10 +47,10 @@ module Make (X : Sig.X) = struct module S = Symbols module SetX = Set.Make(struct type t = X.r let compare = X.compare end) - + (* module Uf = Pptarjan.Uf *) - type env = { + type env = { use : Use.t; uf : Uf.t ; relation : X.Rel.t @@ -60,16 +60,16 @@ module Make (X : Sig.X) = struct | CPos of int (* The explication of this choice *) | CNeg (* The choice has been already negated *) - type t = { + type t = { gamma : env; gamma_finite : env ; - choices : (X.r A.view * Num.num * choice_sign * Ex.t) list; + 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 () = () @@ -101,12 +101,12 @@ module Make (X : Sig.X) = struct 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 = + 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 @@ -116,18 +116,18 @@ module Make (X : Sig.X) = struct [] -> [one] | res -> res - let are_equal env ex t1 t2 = + 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 = + 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 + else let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then try @@ -138,47 +138,47 @@ module Make (X : Sig.X) = struct with Exit -> acc else acc - let congruents env t1 s acc ex = + 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 + 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 = + 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, lt) -> + let lr, ex = fold_find_with_explanation find ex_a lt in A.Distinct (b, lr), ex - | A.Builtin(b, s, l) -> + | 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 = + 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 = + let new_facts_by_contra_congruence env r bol ex = match X.term_extract r with | None -> [] - | Some t1 -> + | Some t1 -> match T.view t1 with - | {T.f=f1 ; xs=[x]} -> - List.fold_left + | {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' -> + | Yes ex' -> let ex_r = Ex.union ex ex' in Print.contra_congruence a ex_r; (dist, ex_r) :: acc @@ -188,25 +188,25 @@ module Make (X : Sig.X) = struct ) [] (Uf.class_of env.uf bol) | _ -> [] - let contra_congruence = + let contra_congruence = let vrai,_ = X.make T.vrai in let faux, _ = X.make T.faux in - fun env r ex -> + fun env r ex -> if X.equal (fst (Uf.find_r env.uf r)) vrai then new_facts_by_contra_congruence env r T.faux ex else if X.equal (fst (Uf.find_r env.uf r)) faux then new_facts_by_contra_congruence env r T.vrai ex else [] - let clean_use = - List.fold_left - (fun env (a, ex) -> - match a with + let clean_use = + List.fold_left + (fun env (a, ex) -> + match a with | LSem _ -> assert false - | LTerm t -> + | LTerm t -> begin match A.LT.view t with - | A.Distinct (_, lt) + | A.Distinct (_, lt) | A.Builtin (_, _, lt) -> let lvs = concat_leaves env.uf lt in List.fold_left @@ -216,40 +216,40 @@ module Make (X : Sig.X) = struct { env with use = Use.add rx (st,sa) env.use } ) env lvs | _ -> assert false - end) + end) - let rec congruence_closure env r1 r2 ex = + 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 + 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 = + 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 + 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, new_eqs @ touched_atoms + ) ({env with uf=uf}, []) res - let replay_atom env sa = + 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 @@ -262,19 +262,19 @@ module Make (X : Sig.X) = struct 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 = + let env, choices = List.fold_left (fun (env, ch) t -> add_term env ch t ex) - (env, choices) xs + (env, choices) xs in (* we update uf and use *) - let nuf, ctx = Uf.add env.uf t in + 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; @@ -282,42 +282,42 @@ module Make (X : Sig.X) = struct (* 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 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 + 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) -> + | A.Eq (t1, t2) -> let env, choices = add_term env choices t1 ex in add_term env choices t2 ex - | A.Distinct (_, lt) + | A.Distinct (_, lt) | A.Builtin (_, _, lt) -> - let env, choices = List.fold_left + 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 + { 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 + and semantic_view env choices la = + List.fold_left (fun (env, choices, lsa) (a, ex) -> - match a with - | LTerm a -> + 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 @@ -334,7 +334,7 @@ module Make (X : Sig.X) = struct and assume_literal env choices la = if la = [] then env, choices - else + else let env, choices, lsa = semantic_view env choices la in let env, choices = List.fold_left @@ -363,15 +363,15 @@ module Make (X : Sig.X) = struct 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 = + 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 = + let l = List.map (fun (c, ex_c, size) -> let exp = Ex.fresh_exp () in @@ -420,13 +420,13 @@ module Make (X : Sig.X) = struct let try_it f t = Print.begin_case_split (); let r = - try + 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 -> + with Exception.Inconsistent dep -> look_for_sat ~bad_last:(Yes dep) [] { t with choices = []} t.gamma t.choices with Exception.Inconsistent d -> @@ -437,37 +437,37 @@ module Make (X : Sig.X) = struct 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, _, _, _) -> + (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) + | _ -> acc) - let extract_terms_from_assumed = - List.fold_left - (fun acc (a, _) -> + 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) -> + match Literal.LT.view r with + | Literal.Eq (t1, t2) -> SetT.add t1 (SetT.add t2 acc) - | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> + | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> List.fold_right SetT.add l acc end | _ -> acc) - let assume ~cs a ex t = + 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 = + let t, ch = if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t - else t, ch + 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 @@ -476,13 +476,13 @@ module Make (X : Sig.X) = struct let class_of t term = Uf.class_of t.gamma.uf term let add_and_process a t = - let aux a ex env = + 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 + Use.print t.gamma.use; t let query a t = Print.query a; @@ -492,15 +492,15 @@ module Make (X : Sig.X) = struct let t = add_and_process a t in Uf.are_equal t.gamma.uf t1 t2 - | A.Distinct (false, [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 _ -> + | 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 @@ -508,16 +508,16 @@ module Make (X : Sig.X) = struct 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 ; + 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 + let t, _, _ = + assume ~cs:false (A.LT.make (A.Distinct (false, [T.vrai; T.faux]))) Ex.empty t in t diff --git a/smt/cc.mli b/smt/cc.mli index 3812b7fb..50ddb980 100644 --- a/smt/cc.mli +++ b/smt/cc.mli @@ -20,7 +20,7 @@ module type S = sig module TimerCC : Timer.S val empty : unit -> t - val assume : cs:bool -> + 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 diff --git a/smt/combine.ml b/smt/combine.ml index e9fafcc6..1d153b78 100644 --- a/smt/combine.ml +++ b/smt/combine.ml @@ -28,31 +28,31 @@ struct type r = | Term of Term.t - | X1 of X1.t - | X5 of X5.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 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 + in ty = Ty.Tint - - let rec compare a b = - let c = compare_tag a b in + + 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 = + and compare_tag a b = Pervasives.compare (theory_num a) (theory_num b) - - and comparei a 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 @@ -64,47 +64,47 @@ struct let equal a b = compare a b = 0 let hash = function - | Term t -> Term.hash t + | 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 = + + 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 + + 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 + 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 + 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 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 @@ -113,38 +113,38 @@ struct | _ -> assert false let add_mr = - List.fold_left - (fun solved (p,v) -> + 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 + | X5 x -> X5.unsolvable x | Term _ -> true - let partition tag = - List.partition - (fun (u,t) -> - (theory_num u = tag || unsolvable u) && + 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) -> + (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 _ -> + | Term _ , Term _ -> add_mr solved (unsolvable_values cmp a b) - + (* only one side is empty *) - | (a, b) + | (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 @@ -153,7 +153,7 @@ struct match a, b with (* Clash entre theories: On peut avoir ces pbs ? *) | X1 _, X5 _ - | X5 _, X1 _ + | X5 _, X1 _ -> assert false (* theorie d'un cote, vide de l'autre *) @@ -171,23 +171,23 @@ struct | X5 _ -> X5.solve a b | Term _ -> assert false - let rec solve_rec mt ab = + let rec solve_rec mt ab = let mr = solve_list mt ab in - let mr , ab = - MR.fold + 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) + | x::lx -> + MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx) mr (mr,[]) - in + 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) + 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 @@ -199,28 +199,28 @@ struct type elt = r type r = elt - type t = { - r1: X1.Rel.t; - r5: X5.Rel.t; + type t = { + r1: X1.Rel.t; + r5: X5.Rel.t; } let empty _ = { - r1=X1.Rel.empty (); + r1=X1.Rel.empty (); r5=X5.Rel.empty (); } - - let assume env sa = + + 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}, + {r1=env1; r5=env5}, { assume = a1@a5; remove = rm1@rm5;} - let query env a = + 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 case_split env = let seq1 = X1.Rel.case_split env.r1 in let seq5 = X5.Rel.case_split env.r5 in seq1 @ seq5 @@ -241,7 +241,7 @@ and X1 : Sig.THEORY with type t = TX1.t and type r = CX.r = type r = CX.r let extract = CX.extract1 let embed = CX.embed1 - let assume env _ _ = env, {Sig.assume = []; remove = []} + let assume env _ _ = env, {Sig.assume = []; remove = []} end) and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract = diff --git a/smt/explanation.ml b/smt/explanation.ml index d1cbf410..d14f162a 100644 --- a/smt/explanation.ml +++ b/smt/explanation.ml @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -open Solver_types +open Solver_types open Format type exp = Atom of Solver_types.atom | Fresh of int -module S = +module S = Set.Make - (struct + (struct type t = exp let compare a b = match a,b with | Atom _, Fresh _ -> -1 @@ -27,25 +27,25 @@ module S = | Fresh i1, Fresh i2 -> i1 - i2 | Atom a, Atom b -> a.aid - b.aid end) - + type t = S.t let singleton e = S.singleton (Atom e) - + let empty = S.empty let union s1 s2 = S.union s1 s2 -let iter_atoms f s = +let iter_atoms f s = S.iter (fun e -> match e with | Fresh _ -> () | Atom a -> f a) s -let fold_atoms f s acc = +let fold_atoms f s acc = S.fold (fun e acc -> match e with | Fresh _ -> acc | Atom a -> f a acc) s acc - + let merge e1 e2 = e1 @@ -61,9 +61,9 @@ let remove_fresh i s = let add_fresh i = S.add (Fresh i) -let print fmt ex = +let print fmt ex = fprintf fmt "{"; - S.iter (function + S.iter (function | Atom a -> fprintf fmt "%a, " Debug.atom a - | Fresh i -> fprintf fmt "Fresh%d " i) ex; + | Fresh i -> fprintf fmt "Fresh%d " i) ex; fprintf fmt "}" diff --git a/smt/fm.ml b/smt/fm.ml index 5cdbacce..22f16cb1 100644 --- a/smt/fm.ml +++ b/smt/fm.ml @@ -15,7 +15,7 @@ open Num open Format open Sig -let ale = Hstring.make "<=" +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 @@ -24,7 +24,7 @@ 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 @@ -33,7 +33,7 @@ module type EXTENDED_Polynome = sig val alien_of : t -> r end -module Make +module Make (X : Sig.X) (P : EXTENDED_Polynome with type r = X.r) = struct @@ -41,22 +41,22 @@ module Make 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 = + module Seq = Set.Make (struct type t = r L.view * L.LT.t option * Explanation.t - let compare (a, _, _) (b, _, _) = + let compare (a, _, _) (b, _, _) = LR.compare (LR.make a) (LR.make b) end) - + module Inequation = struct - type t = { - ple0 : P.t; + type t = { + ple0 : P.t; is_le : bool; dep : (Literal.LT.t * num * P.t * bool) list; expl : Explanation.t @@ -65,7 +65,7 @@ module Make 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 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 } @@ -75,18 +75,18 @@ module Make let is_monomial ineq = P.is_monomial ineq.ple0 - let pos_neg mx { ple0 = p } = + 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 + 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 + 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 = { + type t = { inequations : (Literal.LT.t * Inequation.t) list ; monomes: (Intervals.t * SX.t) MX.t; polynomes : Intervals.t MP.t; @@ -95,30 +95,30 @@ module Make } 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 = + 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 empty _ = { + inequations = [] ; + monomes = MX.empty ; + polynomes = MP.empty ; + known_eqs = SX.empty ; + improved = SP.empty ; } - let replace_inequation env x ineq = + let replace_inequation env x ineq = { env with inequations = (x, ineq)::(List.remove_assoc x env.inequations) } @@ -127,13 +127,13 @@ module Make 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) -> @@ -142,7 +142,7 @@ module Make with Not_found -> Intervals.undefined ty in Intervals.mult ui (Intervals.power n ui') - ) (Intervals.point (Int 1) ty Explanation.empty) vars + ) (Intervals.point (Int 1) ty Explanation.empty) vars let intervals_from_monomes env p = @@ -154,13 +154,13 @@ module Make ) (Intervals.point v (P.type_info p) Explanation.empty) pl let rec add_monome expl use_x env x = - try + 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 -> + with Not_found -> update_monome expl use_x env x - and init_monomes env p use_p expl = + 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)) @@ -168,8 +168,8 @@ module Make 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 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 @@ -178,11 +178,11 @@ module Make in env, i - + and update_monome expl use_x env x = let ty = X.type_info x in - let ui, env = + let ui, env = match X.term_extract x with | Some t -> let use_x = SX.singleton x in @@ -196,7 +196,7 @@ module Make 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 + | 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 @@ -212,13 +212,13 @@ module Make 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 -> + SX.fold + (fun x acc -> let _, use = MX.find x acc.monomes in update_monome expl use acc x) use_x env @@ -229,14 +229,14 @@ module Make 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 + try let inp = MP.find np polynomes in let new_ix = - Intervals.scale + Intervals.scale ((Int 1) // a) (Intervals.add i (Intervals.scale (minus_num d) - (Intervals.add inp + (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 @@ -261,7 +261,7 @@ module Make 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 = + let eq = L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in Some (eq, None, ex) | _ -> None @@ -271,29 +271,29 @@ module Make | None -> eqs | Some eq1 -> eq1::eqs - type ineq_status = + 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) = + 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 -> + | None -> if P.is_empty p then - let _, v = P.to_list p in + 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 + 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} -> + (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} ; @@ -308,7 +308,7 @@ module Make let fm_equalities env eqs { Inequation.ple0 = p; dep = dep; expl = ex } = let inqs, eqs = List.fold_left - (fun (inqs, eqs) (a, _, p, _) -> + (fun (inqs, eqs) (a, _, p, _) -> List.remove_assoc a inqs, (mk_equality p, Some a, ex) :: eqs ) (env.inequations, eqs) dep in @@ -320,15 +320,15 @@ module Make let u = if a >/ (Int 0) then Intervals.new_borne_sup expl b is_le uints - else + 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 + else let ty = P.type_info p0 in let a, _ = P.choose p0 in let p, change = @@ -343,20 +343,20 @@ module Make else Intervals.new_borne_sup expl c is_le (Intervals.undefined ty) in let u, pu = - try + try let pu = MP.find p env.polynomes in let i = Intervals.intersect u pu in i, pu with Not_found -> u, Intervals.undefined ty in - let env = + 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; + { env with + polynomes = polynomes; + monomes = monomes; improved = improved } else env in @@ -364,41 +364,41 @@ module Make | [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le) | _ -> env - let add_inequations acc lin expl = + let add_inequations acc lin expl = List.fold_left (fun (env, eqs) ineq -> - (* let expl = List.fold_left - (fun expl (l,_,_,_) -> + (* let expl = List.fold_left + (fun expl (l,_,_,_) -> Explanation.union (*Explanation.everything*) (Explanation.singleton (Formula.mk_lit l)) expl - ) expl ineq.Inequation.dep + ) 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 -> + + | 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 + 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 = + 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 + 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 @@ -407,24 +407,24 @@ module Make env, eqs | Monome (a, x, v) -> - let env, eqs = + 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 -> + | Other -> env, eqs (*t env,eqs = update_polynomes env eqs ineq in env, pers_ineqs, eqs*) - + ) acc lin - let mult_list c = + 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 = @@ -436,14 +436,14 @@ module Make else a, b with Failure "big_int_of_ratio" -> a, b - let cross x cpos cneg = - let rec cross_rec acc = function + 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 + 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 *) @@ -452,36 +452,36 @@ module Make (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 = + let ni = { Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2; expl = Explanation.union ex1 ex2 } - in + in ni::acc ) acc cpos - in + in cross_rec acc l in cross_rec [] cneg - let split x l = + 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 + if a >/ (Int 0) then ineq::cp, cn, co else cp, ineq::cn, co with Not_found -> cp, cn, ineq::co - in + in List.fold_left split_rec ([], [], []) l - let length s = SX.fold (fun _ acc -> acc+1) s 0 + let length s = SX.fold (fun _ acc -> acc+1) s 0 - let choose_var l = + 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 + | Some (y, c') -> + let c = pos * neg in if c < c' then Some (x, c) else acc ) pos_neg None in match xopt with @@ -504,16 +504,16 @@ module Make with Not_found -> add_inequations acc l expl (* - let fm env eqs 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 = + let fm env eqs expl = fourier (env, eqs) (List.map snd env.inequations) expl - let is_num r = + let is_num r = let ty = X.type_info r in ty = Ty.Tint || ty = Ty.Treal let add_disequality env eqs p expl = @@ -523,12 +523,12 @@ module Make raise (Exception.Inconsistent expl) | ([], v) -> env, eqs - | ([a, x], v) -> + | ([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 + 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 @@ -541,37 +541,37 @@ module Make 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 + let i2 = + try + MP.find p env.polynomes with Not_found -> Intervals.undefined ty in let i = Intervals.exclude i1 i2 in - let env = + 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 + { 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) -> + | ([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 = + try let i', use' = MX.find x env.monomes in Intervals.intersect i i', use' with Not_found -> i, SX.empty @@ -585,26 +585,26 @@ module Make 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 = + 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 = + 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 + { env with polynomes = polynomes; monomes = monomes; improved = improved } else env in - let env = - { env with + let env = + { env with known_eqs = SX.add (P.alien_of p) env.known_eqs } in env, eqs @@ -614,33 +614,33 @@ module Make 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 + | 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 (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 = + 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 + else match Intervals.is_point i with | Some (num, ex) -> let r2 = P.alien_of (P.create [] num (P.type_info p)) in @@ -652,11 +652,11 @@ module Make let equalities_from_monomes env eqs = - let known, eqs = + let known, eqs = MX.fold (fun x (i,_) (knw, eqs) -> if SX.mem x knw then knw, eqs - else + else match Intervals.is_point i with | Some (num, ex) -> let r2 = P.alien_of (P.create [] num (X.type_info x)) in @@ -692,29 +692,29 @@ module Make let env = replace_inequation env root ineq in env, eqs, true, expl - | L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 -> + | 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 -> + + | 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) - + | _ -> (env, eqs, new_ineqs, expl) + with Intervals.NotConsistent expl -> raise (Exception.Inconsistent expl) ) - (env, [], false, Explanation.empty) la + (env, [], false, Explanation.empty) la in - if new_ineqs then - if false then - (); + 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 @@ -724,13 +724,13 @@ module Make 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 + 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 @@ -738,14 +738,14 @@ module Make with Intervals.NotConsistent expl -> raise (Exception.Inconsistent expl) - + let query env a_ex = - try - ignore(assume env [a_ex]); + try + ignore(assume env [a_ex]); No with Exception.Inconsistent expl -> Yes expl - let case_split_polynomes env = + let case_split_polynomes env = let o = MP.fold (fun p i o -> match Intervals.finite_size i with @@ -753,21 +753,21 @@ module Make 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) -> + 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 -> + | None -> [] - let case_split_monomes env = + let case_split_monomes env = let o = MX.fold (fun x (i,_) o -> match Intervals.finite_size i with @@ -775,26 +775,26 @@ module Make 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) -> + 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 -> + | None -> [] - - let case_split env = + + let case_split env = match case_split_polynomes env with | [] -> case_split_monomes env | choices -> choices - + let add env _ = env let extract_improved env = diff --git a/smt/fm.mli b/smt/fm.mli index d438f617..b35e56ee 100644 --- a/smt/fm.mli +++ b/smt/fm.mli @@ -17,7 +17,7 @@ module type EXTENDED_Polynome = sig val alien_of : t -> r end -module Make +module Make (X : Sig.X) - (P : EXTENDED_Polynome with type r = X.r) + (P : EXTENDED_Polynome with type r = X.r) : Sig.RELATION with type r = X.r diff --git a/smt/intervals.ml b/smt/intervals.ml index f02240e6..8b9d086c 100644 --- a/smt/intervals.ml +++ b/smt/intervals.ml @@ -16,9 +16,9 @@ open Format module Ex = Explanation -type borne = - | Strict of (num * Ex.t) - | Large of (num * Ex.t) +type borne = + | Strict of (num * Ex.t) + | Large of (num * Ex.t) | Pinfty | Minfty let compare_bornes b1 b2 = @@ -26,33 +26,33 @@ let compare_bornes b1 b2 = | 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, _) -> + | 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 + | (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 + | (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 +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 @@ -62,9 +62,9 @@ let compare_bl_bl b1 b2 = let compare_bu_bu b1 b2 = match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 + | (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 @@ -72,7 +72,7 @@ let compare_bu_bu b1 b2 = let c = compare_num v1 v2 in if c = 0 then 1 else c -type t = { +type t = { ints : (borne * borne) list; is_int : bool; expl: Ex.t @@ -83,23 +83,23 @@ exception NotConsistent of Ex.t exception Not_a_float let print_borne fmt = function - | Minfty -> fprintf fmt "-inf" + | 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 + 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 } = + +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]; @@ -108,7 +108,7 @@ let undefined ty = { } let point b ty e = { - ints = [Large (b, e), Large (b, e)]; + ints = [Large (b, e), Large (b, e)]; is_int = ty = Ty.Tint; expl = Ex.empty } @@ -132,7 +132,7 @@ let is_point { ints = l; expl = e } = | _ -> None let add_expl_zero i expl = - let res = List.map (fun x -> + 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), @@ -143,10 +143,10 @@ let add_expl_zero i expl = 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 (v1, e1) | Large (v1,e1)), (Strict (v2, e2) | Large (v2, e2)) -> - let c = compare_num v1 v2 in - if c > 0 then raise + 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 @@ -156,7 +156,7 @@ let check_one_interval b1 b2 is_int = end | _ -> () -let min_borne b1 b2 = +let min_borne b1 b2 = match b1, b2 with | Minfty , _ | _ , Minfty -> Minfty | b , Pinfty | Pinfty, b -> b @@ -164,31 +164,31 @@ let min_borne b1 b2 = let c = compare_num v1 v2 in if c < 0 then b1 else if c > 0 then b2 - else match b1, b2 with + else match b1, b2 with | (Strict _ as b) , _ | _, (Strict _ as b) -> b | _, _ -> b1 - -let max_borne b1 b2 = + +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, _)) -> + | (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 + 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 = +let pos_borne_strict b1 = compare_bornes b1 (borne_of true Ex.empty (Int 0)) > 0 -let neg_borne b1 = +let neg_borne b1 = compare_bornes b1 (borne_of true Ex.empty (Int 0)) <= 0 -let neg_borne_strict b1 = +let neg_borne_strict b1 = compare_bornes b1 (borne_of true Ex.empty (Int 0)) < 0 -let zero_borne b1 = +let zero_borne b1 = compare_bornes b1 (borne_of true Ex.empty (Int 0)) = 0 exception Found of Sig.answer @@ -196,12 +196,12 @@ exception Found of Sig.answer let doesnt_contain_0 {ints=l} = try let max = List.fold_left - (fun old_u (l, u) -> + (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 + 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) @@ -219,11 +219,11 @@ let is_strict_smaller i1 i2 = then raise Exit ) i1 i2; false - with + with | Exit -> true | Invalid_argument _ -> List.length i1 > List.length i2 -let is_strict_smaller {ints=i1} {ints=i2} = +let is_strict_smaller {ints=i1} {ints=i2} = is_strict_smaller i1 i2 @@ -247,7 +247,7 @@ let add_borne b1 b2 = | Minfty, Pinfty | Pinfty, Minfty -> assert false | Minfty, _ | _, Minfty -> Minfty | Pinfty, _ | _, Pinfty -> Pinfty - | Large (v1, e1), Large (v2, e2) -> + | 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) @@ -260,9 +260,9 @@ let add_interval l (b1,b2) = ) l [] let add {ints = l1; is_int = is_int; expl = e1} {ints = l2; expl = e2}= - let l = + let l = List.fold_left - (fun l bs -> let i = add_interval l1 bs in i@l) [] l2 + (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 } @@ -274,7 +274,7 @@ let minus_borne = function let scale_borne n b = assert (n >=/ Int 0); - if n =/ Int 0 then + if n =/ Int 0 then match b with | Pinfty | Minfty -> Large (Int 0, Ex.empty) | Large (_, e) | Strict (_, e) -> Large (Int 0, e) @@ -293,24 +293,24 @@ let scale_interval n (b1,b2) = let scale n uints = let l = List.map (scale_interval n) uints.ints in union { uints with ints = l; expl = uints.expl } - + let mult_borne b1 b2 = match b1,b2 with | Minfty, Pinfty | Pinfty, Minfty -> assert false | Minfty, b | b, Minfty -> - if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 + 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 + 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) -> + | Large (v1, e1), Strict (v2, e2) -> Strict (v1 */ v2, Ex.union e1 e2) - | Large (v1, e1), Large (v2, e2) -> + | Large (v1, e1), Large (v2, e2) -> Large (v1 */ v2, Ex.union e1 e2) let mult_borne_inf b1 b2 = @@ -323,10 +323,10 @@ let mult_borne_sup b1 b2 = | Minfty, Pinfty | Pinfty, Minfty -> Pinfty | _, _ -> mult_borne b1 b2 -type interval_class = - | P of Ex.t - | M of Ex.t - | N of Ex.t +type interval_class = + | P of Ex.t + | M of Ex.t + | N of Ex.t | Z let class_of (l,u) = @@ -338,17 +338,17 @@ let class_of (l,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 -> + | P e1, P e2 -> mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, M e2 -> + | P e1, M e2 -> mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, N e2 -> + | P e1, N e2 -> mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2 - | M e1, P e2 -> + | M e1, P e2 -> mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2 - | M e1, M 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), + 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 @@ -360,7 +360,7 @@ let mult_bornes (a,b) (c,d) = 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 @@ -396,14 +396,14 @@ let power_bornes p (b1,b2) = | 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) + if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) let int_of_borne_sup b = match b with @@ -411,7 +411,7 @@ let int_of_borne_sup b = | Large (v, e) -> Large (floor_num v, e) | Strict (v, e) -> let v' = floor_num v in - if v' 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) + if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) let int_div_of_borne_sup b = match b with @@ -429,10 +429,10 @@ let int_div_of_borne_sup b = let v' = floor_num v in if v' - let (lo1,up1), (lo2,up2) = + 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 @@ -457,7 +457,7 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1) 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 + 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) @@ -465,15 +465,15 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1) 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 + else if cll = 0 && cuu = 0 then step (r1, r2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu >= 0 then + else if cll <= 0 && cuu >= 0 then step (l1, r2) ((lo2,up2)::acc) expl - else if cll >= 0 && cuu <= 0 then + else if cll >= 0 && cuu <= 0 then step (r1, l2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu <= 0 && cul >= 0 then + 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 + else if cll >= 0 && cuu >= 0 && clu <= 0 then step (l1, r2) ((lo1,up2)::acc) expl else assert false | [], _ | _, [] -> List.rev acc, expl @@ -484,13 +484,13 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1) let new_borne_sup expl b ~is_le uints = - intersect + 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 + intersect { ints = [(borne_of is_le expl b), Pinfty]; is_int = uints.is_int; expl = Ex.empty } uints @@ -509,28 +509,28 @@ let complement ({ints=l; expl=e} as uints) = | _ -> 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 + intersect (complement uints1) uints2 let mult u1 u2 = - let resl, expl = + let resl, expl = List.fold_left (fun (l', expl) b1 -> - List.fold_left + 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 + expl = Ex.union expl (Ex.union u1.expl u2.expl) } let power n u = @@ -553,7 +553,7 @@ let num_of_float x = let factor = (Int 2) **/ (Int (n - 52)) in (Big_int z) */ factor -let root_num a n = +let root_num a n = if a None - + let borne_inf = function | {ints = (Large (v, ex), _)::_} -> v, ex | _ -> invalid_arg "Intervals.borne_inf : No finite lower bound" @@ -655,7 +655,7 @@ 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) + 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) @@ -677,10 +677,10 @@ let inv_bornes (l, u) is_int = let inv ({ints=l; is_int=is_int} as u) = try - let l' = List.fold_left + 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 + 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 @@ -696,8 +696,8 @@ let div i1 i2 = | Sig.No -> i1 in let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in - let l = - if is_int then + 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/smt/intervals.mli b/smt/intervals.mli index bf5e1e68..44c876c5 100644 --- a/smt/intervals.mli +++ b/smt/intervals.mli @@ -42,7 +42,7 @@ val power : int -> t -> t val sqrt : t -> t -val root : int -> t -> t +val root : int -> t -> t val add : t -> t -> t diff --git a/smt/literal.ml b/smt/literal.ml index 9c9285b7..ffd917c9 100644 --- a/smt/literal.ml +++ b/smt/literal.ml @@ -13,8 +13,8 @@ open Hashcons -type 'a view = - | Eq of 'a * 'a +type 'a view = + | Eq of 'a * 'a | Distinct of bool * 'a list | Builtin of bool * Hstring.t * 'a list @@ -45,7 +45,7 @@ module type S = sig 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 @@ -53,36 +53,36 @@ 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 + module V = struct + type t = X.t view - let equal a1 a2 = + let equal a1 a2 = match a1, a2 with - | Eq(t1, t2), Eq(u1, u2) -> + | 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 && + (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 - && + | 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) -> + | Builtin(b, n, l) -> let x = if b then 7 else 23 in - abs - (List.fold_left + abs + (List.fold_left (fun acc t-> acc*13 + X.hash t) (Hstring.hash n+x) l) end @@ -92,9 +92,9 @@ module Make (X : OrderedType) : S with type elt = X.t = struct let equal a1 a2 = a1 == a2 let hash a1 = a1.tag - module T = struct - type t' = t - type t = t' + module T = struct + type t' = t + type t = t' let compare=compare let equal = equal let hash = hash @@ -112,11 +112,11 @@ module Make (X : OrderedType) : S with type elt = X.t = struct | 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 @@ -124,18 +124,18 @@ module Make (X : OrderedType) : S with type elt = X.t = struct | z :: l -> Format.fprintf fmt "%a" X.print z; List.iter (Format.fprintf fmt ", %a" X.print) l - - let ale = Hstring.make "<=" + + let ale = Hstring.make "<=" let alt = Hstring.make "<" - let print fmt a = + 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) -> + | 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)) -> + | 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 @@ -156,7 +156,7 @@ module Make (X : OrderedType) : S with type elt = X.t = struct 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) @@ -182,28 +182,28 @@ module LT : S_Term = struct module L = Make(Term) include L - let mk_pred t = make (Eq (t, Term.vrai) ) - + let mk_pred t = make (Eq (t, Term.vrai) ) + let vrai = mk_pred Term.vrai let faux = mk_pred Term.faux let neg a = match view a with - | Eq(t1, t2) when Term.equal t2 Term.faux -> + | Eq(t1, t2) when Term.equal t2 Term.faux -> make (Eq (t1, Term.vrai)) - | Eq(t1, t2) when Term.equal t2 Term.vrai -> + | Eq(t1, t2) when Term.equal t2 Term.vrai -> make (Eq (t1, Term.faux)) | _ -> L.neg a -(* let terms_of a = - let l = match view a with - | Eq (t1, t2) -> [t1; t2] - | Distinct (_, l) | Builtin (_, _, l) -> l +(* 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 = + 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/smt/literal.mli b/smt/literal.mli index b4915092..773e6871 100644 --- a/smt/literal.mli +++ b/smt/literal.mli @@ -18,8 +18,8 @@ module type OrderedType = sig val print : Format.formatter -> t -> unit end -type 'a view = - | Eq of 'a * 'a +type 'a view = + | Eq of 'a * 'a | Distinct of bool * 'a list | Builtin of bool * Hstring.t * 'a list diff --git a/smt/polynome.ml b/smt/polynome.ml index d49fd56b..f3e3fde1 100644 --- a/smt/polynome.ml +++ b/smt/polynome.ml @@ -47,7 +47,7 @@ module type T = sig 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 @@ -61,41 +61,41 @@ end module Make (X : S) = struct type r = X.r - - module M : Map.S with type key = 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 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 = + 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), "*" + | 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 + 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 + 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 @@ -104,38 +104,38 @@ module Make (X : S) = struct 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 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 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 + in { m = m; c = p1.c +/ p2.c; ty = p1.ty } - let mult_const n p = + 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 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 = + let m = M.fold - (fun xi ai m -> M.add (X.mult x xi) (a */ ai) m) p.m acx.m - in + (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 @@ -146,10 +146,10 @@ module Make (X : S) = struct let div p1 p2 = if M.is_empty p2.m then if p2.c =/ Int 0 then raise Division_by_zero - else + 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.Tint -> {p with c = floor_num p.c}, false | true, Ty.Treal -> p, false | false, Ty.Tint -> p, true | false, Ty.Treal -> p, false @@ -160,11 +160,11 @@ module Make (X : S) = struct let modulo p1 p2 = if M.is_empty p2.m then if p2.c =/ Int 0 then raise Division_by_zero - else + 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 @@ -174,7 +174,7 @@ module Make (X : S) = struct (*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 + (*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 @@ -183,19 +183,19 @@ module Make (X : S) = struct 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 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 + let is_monomial p = + try M.fold - (fun x a r -> + (fun x a r -> match r with | None -> Some (a, x, p.c) | _ -> raise Exit) @@ -207,37 +207,37 @@ module Make (X : S) = struct | Num.Ratio rat -> Ratio.denominator_ratio rat let numerator = function - | Num.Int i -> Big_int.big_int_of_int i + | 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) + 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 = + + 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 = + 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 + if M.is_empty m then { p with c = Int 0 }, p.c, (Int 1) else let ppcm = ppmc_denominators p in diff --git a/smt/polynome.mli b/smt/polynome.mli index 9e7dc2c0..36d32c35 100644 --- a/smt/polynome.mli +++ b/smt/polynome.mli @@ -18,7 +18,7 @@ exception Not_a_num exception Maybe_zero module type S = sig - type r + type r val compare : r -> r-> int val term_embed : Term.t -> r val mult : r -> r -> r @@ -27,9 +27,9 @@ end module type T = sig - type r + type r type t - + val compare : t -> t -> int val hash : t -> int @@ -47,7 +47,7 @@ module type T = sig 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 @@ -56,7 +56,7 @@ module type T = sig 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 + (* 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 diff --git a/smt/sig.mli b/smt/sig.mli index 667e756f..9bd0fd56 100644 --- a/smt/sig.mli +++ b/smt/sig.mli @@ -15,11 +15,11 @@ type answer = Yes of Explanation.t | No type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t -type 'a input = +type 'a input = 'a Literal.view * Literal.LT.t option * Explanation.t -type 'a result = { - assume : ('a literal * Explanation.t) list; +type 'a result = { + assume : ('a literal * Explanation.t) list; remove: ('a literal * Explanation.t) list; } @@ -28,14 +28,14 @@ module type RELATION = sig 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 *) @@ -64,7 +64,7 @@ module type THEORY = sig 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 *) @@ -108,31 +108,31 @@ 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 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 diff --git a/smt/smt.ml b/smt/smt.ml index eb308390..ddfbd5d5 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -12,7 +12,7 @@ open Format -type error = +type error = | DuplicateTypeName of Hstring.t | DuplicateSymb of Hstring.t | UnknownType of Hstring.t @@ -36,37 +36,37 @@ module Type = struct let equal = Hstring.equal - let type_int = + let type_int = let tint = Hstring.make "int" in H.add decl_types tint Ty.Tint; tint - let type_real = + let type_real = let treal = Hstring.make "real" in H.add decl_types treal Ty.Treal; treal - let type_bool = + let type_bool = let tbool = Hstring.make "bool" in H.add decl_types tbool Ty.Tbool; tbool - let type_proc = + let type_proc = let tproc = Hstring.make "proc" in H.add decl_types tproc Ty.Tint; tproc - let declare_constructor ty c = + let declare_constructor ty c = if H.mem decl_symbs c then raise (Error (DuplicateSymb c)); - H.add decl_symbs c + H.add decl_symbs c (Symbols.name ~kind:Symbols.Constructor c, [], ty) - let declare t constrs = + 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 @@ -82,29 +82,29 @@ module Type = struct 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 = + let declare f args ret = if H.mem decl_symbs f then raise (Error (DuplicateTypeName f)); - List.iter - (fun t -> + 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 declared s = let res = H.mem decl_symbs s in - if not res then begin + 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 + eprintf "%a (=?%b) -> %a@." Hstring.print hs (Hstring.compare hs s = 0) Symbols.print sy) decl_symbs; @@ -114,49 +114,49 @@ module Symbol = struct 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 _ = + + 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 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 = + + let assign_var x y = if not (Hstring.equal x y) then add assignments x y - let rec compute () = + let rec compute () = let flag = ref false in let visited = ref HSet.empty in - let rec dfs x s = + let rec dfs x s = if not (HSet.mem x !visited) then begin visited := HSet.add x !visited; - HSet.iter - (fun y -> + 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 @@ -171,25 +171,25 @@ module Variant = struct in H.iter dfs assignments; if !flag then compute () - - let hset_print fmt s = + + 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) + + 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 = + + 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) -> + List.iter + (fun (x, nty) -> if not (H.mem constructors x) then let ty = H.find decl_types nty in match ty with @@ -198,30 +198,30 @@ module Variant = struct | _ -> ()) l; H.clear assignments - let update_decl_types s = + 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 + 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 () = + let close () = compute (); - H.iter - (fun x s -> + 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 @@ -253,17 +253,17 @@ end let rec first_ite = function | [] -> raise Not_found | Tite (c, t1, t2) :: l -> [], (c, t1, t2), l - | x :: l -> + | x :: l -> let left, triplet, right = first_ite l in x::left, triplet, right - let rec lift_ite sb l ty = + 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 -> + with Not_found -> let l = List.map (function T x -> x | _ -> assert false) l in T (AETerm.make sb l ty) @@ -285,8 +285,8 @@ end | T t -> AETerm.is_real t | Tite(_, t1, t2) -> is_real t1 && is_real t2 - let make_arith op t1 t2 = - let op = + let make_arith op t1 t2 = + let op = match op with | Plus -> Symbols.Plus | Minus -> Symbols.Minus @@ -294,7 +294,7 @@ end | Div -> Symbols.Div | Modulo -> Symbols.Modulo in - let ty = + 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 @@ -308,10 +308,10 @@ end and Formula : sig - type comparator = Eq | Neq | Le | Lt + type comparator = Eq | Neq | Le | Lt type combinator = And | Or | Imp | Not - type t = - | Lit of Literal.LT.t + type t = + | Lit of Literal.LT.t | Comb of combinator * t list val f_true : t @@ -337,7 +337,7 @@ and Formula : sig val print_list : string -> Format.formatter -> t list -> unit val print : Format.formatter -> t -> unit - module Tseitin (Dymmy : sig end) : + module Tseitin (Dymmy : sig end) : sig val make_cnf : t -> Literal.LT.t list list end end @@ -346,18 +346,18 @@ end type comparator = Eq | Neq | Le | Lt type combinator = And | Or | Imp | Not - type t = - | Lit of Literal.LT.t + type t = + | Lit of Literal.LT.t | Comb of combinator * t list - let rec print fmt phi = + let rec print fmt phi = match phi with | Lit a -> Literal.LT.print fmt a - | Comb (Not, [f]) -> + | 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]) -> + | Comb (Imp, [f1; f2]) -> fprintf fmt "(%a => %a)" print f1 print f2 | _ -> assert false and print_list sep fmt = function @@ -370,38 +370,38 @@ end let make comb l = Comb (comb, l) - let value env c = + 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 = + 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 -> + | Some true -> lift_ite (c::env) op (left@(t1::right)) - | Some false -> + | Some false -> lift_ite ((make Not [c])::env) op (left@(t2::right)) | None -> - Comb - (And, - [Comb + Comb + (And, + [Comb (Imp, [c; lift_ite (c::env) op (left@(t1::right))]); - Comb (Imp, - [(make Not [c]); - lift_ite + Comb (Imp, + [(make Not [c]); + lift_ite ((make Not [c])::env) op (left@(t2::right))])]) end - with Not_found -> + with Not_found -> begin let lit = match op, l with - | Eq, [Term.T t1; Term.T t2] -> + | Eq, [Term.T t1; Term.T t2] -> Literal.Eq (t1, t2) - | Neq, ts -> - let ts = + | 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] -> @@ -440,16 +440,16 @@ end | 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)]) -> + | 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 (Not, [Comb (Imp, [f1; f2])]) -> Comb (And, [sform f1; sform (Comb (Not, [f2]))]) - | Comb (And, l) -> + | Comb (And, l) -> Comb (And, List.rev_map sform l) - | Comb (Or, l) -> + | Comb (Or, l) -> Comb (Or, List.rev_map sform l) - | Comb (Imp, [f1; f2]) -> + | Comb (Imp, [f1; f2]) -> Comb (Or, [sform (Comb (Not, [f1])); sform f2]) | Comb ((Imp | Not), _) -> assert false | Lit _ as f -> f @@ -463,17 +463,17 @@ end | [a] -> a | l -> Comb (Or, l) - let distrib l_and l_or = - let l = + let distrib l_and l_or = + let l = if l_or = [] then l_and else List.rev_map - (fun x -> - match x with + (fun x -> + match x with | Lit _ -> Comb (Or, x::l_or) | Comb (Or, l) -> Comb (Or, l @@ l_or) | _ -> assert false - ) l_and + ) l_and in Comb (And, l) @@ -482,22 +482,22 @@ end | 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 = + + let rec cnf f = match f with - | Comb (Or, l) -> + | Comb (Or, l) -> begin let l = List.rev_map cnf l in - let l_and, l_or = + let l_and, l_or = List.partition (function Comb(And,_) -> true | _ -> false) l in match l_and with - | [ Comb(And, l_conj) ] -> + | [ Comb(And, l_conj) ] -> let u = flatten_or l_or in distrib l_conj u @@ -505,7 +505,7 @@ end let u = flatten_or l_or in cnf (Comb(Or, (distrib l_conj u)::r)) - | _ -> + | _ -> begin match flatten_or l_or with | [] -> assert false @@ -513,9 +513,9 @@ end | v -> Comb (Or, v) end end - | Comb (And, l) -> + | Comb (And, l) -> Comb (And, List.rev_map cnf l) - | f -> f + | f -> f let rec mk_cnf = function | Comb (And, l) -> @@ -524,13 +524,13 @@ end | Comb (Or, [f1;f2]) -> let ll1 = mk_cnf f1 in let ll2 = mk_cnf f2 in - List.fold_left + 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 + List.fold_left (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 | Lit a -> [[a]] @@ -538,18 +538,18 @@ end | _ -> assert false - let rec unfold mono f = + let rec unfold mono f = match f with - | Lit a -> a::mono - | Comb (Not, [Lit a]) -> + | Lit a -> a::mono + | Comb (Not, [Lit a]) -> (Literal.LT.neg a)::mono - | Comb (Or, l) -> + | Comb (Or, l) -> List.fold_left unfold mono l | _ -> assert false - - let rec init monos f = + + let rec init monos f = match f with - | Comb (And, l) -> + | Comb (And, l) -> List.fold_left init monos l | f -> (unfold [] f)::monos @@ -557,10 +557,10 @@ end let sfnc = cnf (sform f) in init [] sfnc - let mk_proxy = + let mk_proxy = let cpt = ref 0 in - fun () -> - let t = AETerm.make + fun () -> + let t = AETerm.make (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt)))) [] Ty.Tbool in @@ -615,9 +615,9 @@ end | 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 @@ -702,47 +702,47 @@ module Make (Dummy : sig end) = struct let check_unsatcore uc = eprintf "Unsat Core : @."; - List.iter - (fun c -> - eprintf "%a@." (Formula.print_list "or") + List.iter + (fun c -> + eprintf "%a@." (Formula.print_list "or") (List.rev_map (fun x -> Formula.Lit x) c)) uc; eprintf "@."; - try + try clear (); CSolver.assume uc 0; CSolver.solve (); eprintf "Not an unsat core !!!@."; assert false - with + with | Solver.Unsat _ -> (); - | Solver.Sat -> + | Solver.Sat -> eprintf "Sat: Not an unsat core !!!@."; assert false - let export_unsatcore cl = + 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; + done; !l) cl in (* check_unsatcore uc; *) uc - module SInt = + module SInt = Set.Make (struct type t = int let compare = Pervasives.compare end) let export_unsatcore2 cl = - let s = - List.fold_left + 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 + in SInt.elements s - let assume ?(profiling = false) ~id f = + let assume ?(profiling = false) ~id f = if profiling then Time.start (); - try + try CSolver.assume (Tseitin.make_cnf f) id; if profiling then Time.pause () with Solver.Unsat ex -> @@ -752,12 +752,12 @@ module Make (Dummy : sig end) = struct let check ?(profiling = false) () = incr calls; if profiling then Time.start (); - try + try CSolver.solve (); if profiling then Time.pause () with | Solver.Sat -> if profiling then Time.pause () - | Solver.Unsat ex -> + | Solver.Unsat ex -> if profiling then Time.pause (); raise (Unsat (export_unsatcore2 ex)) @@ -777,7 +777,7 @@ module Make (Dummy : sig end) = struct let entails ?(profiling=false) ~id f = let st = save_state () in - let ans = + let ans = try assume ~profiling ~id (Formula.make Formula.Not [f]) ; check ~profiling (); diff --git a/smt/smt.mli b/smt/smt.mli index 2920a1ef..9a57b771 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -74,31 +74,31 @@ 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). *) @@ -107,7 +107,7 @@ 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. *) @@ -117,12 +117,12 @@ module Variant : sig 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 + (** [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 + subtype of [x] (use this function when [x := y] appear in your program *) val print : unit -> unit @@ -143,10 +143,10 @@ module rec Term : sig (** The type of terms *) (** The type of operators *) - type operator = + type operator = | Plus (** [+] *) | Minus (** [-] *) - | Mult (** [*] *) + | Mult (** [*] *) | Div (** [/] *) | Modulo (** [mod] *) @@ -186,22 +186,22 @@ end and Formula : sig (** The type of comparators: *) - type comparator = + type comparator = | Eq (** equality ([=]) *) | Neq (** disequality ([<>]) *) | Le (** inequality ([<=]) *) | Lt (** strict inequality ([<]) *) (** The type of operators *) - type combinator = + type combinator = | And (** conjunction *) | Or (** disjunction *) | Imp (** implication *) | Not (** negation *) (** The type of ground formulas *) - type t = - | Lit of Literal.LT.t + type t = + | Lit of Literal.LT.t | Comb of combinator * t list val f_true : t @@ -267,11 +267,11 @@ module type Solver = sig assume f_n; check ();]} *) - + type state (** The type of the internal state of the solver (see {!save_state} and {!restore_state}).*) - + (** {2 Profiling functions} *) @@ -292,20 +292,20 @@ module type Solver = sig (** [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). *) diff --git a/smt/solver.ml b/smt/solver.ml index 7481ff3e..51b6fecc 100644 --- a/smt/solver.ml +++ b/smt/solver.ml @@ -22,8 +22,8 @@ exception Restart -type env = - { +type env = + { (* si vrai, les contraintes sont deja fausses *) mutable is_unsat : bool; @@ -31,34 +31,34 @@ type env = (* clauses du probleme *) mutable clauses : clause Vec.t; - + (* clauses apprises *) mutable learnts : clause Vec.t; - + (* valeur de l'increment pour l'activite des clauses *) mutable clause_inc : float; - + (* valeur de l'increment pour l'activite des variables *) mutable var_inc : float; - + (* un vecteur des variables du probleme *) mutable vars : var Vec.t; - + (* la pile de decisions avec les faits impliques *) mutable trail : atom Vec.t; (* une pile qui pointe vers les niveaux de decision dans trail *) mutable trail_lim : int Vec.t; - (* Tete de la File des faits unitaires a propager. + (* Tete de la File des faits unitaires a propager. C'est un index vers le trail *) mutable qhead : int; - - (* Nombre des assignements top-level depuis la derniere + + (* Nombre des assignements top-level depuis la derniere execution de 'simplify()' *) mutable simpDB_assigns : int; - (* Nombre restant de propagations a faire avant la prochaine + (* Nombre restant de propagations a faire avant la prochaine execution de 'simplify()' *) mutable simpDB_props : int; @@ -82,12 +82,12 @@ type env = (* facteur de multiplication de restart limite, vaut 1.5 par defaut*) restart_inc : float; - - (* limite initiale du nombre de clause apprises, vaut 1/3 + + (* limite initiale du nombre de clause apprises, vaut 1/3 des clauses originales par defaut *) mutable learntsize_factor : float; - - (* multiplier learntsize_factor par cette valeur a chaque restart, + + (* multiplier learntsize_factor par cette valeur a chaque restart, vaut 1.1 par defaut *) learntsize_inc : float; @@ -96,7 +96,7 @@ type env = (* controle la polarite a choisir lors de la decision *) polarity_mode : bool; - + mutable starts : int; mutable decisions : int; @@ -116,17 +116,17 @@ type env = mutable nb_init_vars : int; mutable nb_init_clauses : int; - + mutable model : var Vec.t; - + mutable tenv : Th.t; mutable tenv_queue : Th.t Vec.t; - + mutable tatoms_queue : atom Queue.t; } - + exception Conflict of clause @@ -136,36 +136,36 @@ module Make (Dummy : sig end) = struct open Solver_types - type state = + type state = { - env : env; + env : env; st_cpt_mk_var: int; st_ma : var Literal.LT.Map.t; } let env = - { - is_unsat = false; - + { + is_unsat = false; + unsat_core = [] ; clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) - + learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) - + clause_inc = 1.; - + var_inc = 1.; - + vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*) - + trail = Vec.make 601 dummy_atom; trail_lim = Vec.make 601 (-105); qhead = 0; - + simpDB_assigns = -1; simpDB_props = 0; @@ -183,15 +183,15 @@ module Make (Dummy : sig end) = struct restart_first = 100; restart_inc = 1.5; - + learntsize_factor = 1. /. 3. ; - + learntsize_inc = 1.1; expensive_ccmin = true; polarity_mode = false; - + starts = 0; decisions = 0; @@ -211,9 +211,9 @@ module Make (Dummy : sig end) = struct nb_init_vars = 0; nb_init_clauses = 0; - + model = Vec.make 0 dummy_var; - + tenv = Th.empty(); tenv_queue = Vec.make 100 (Th.empty()); @@ -224,18 +224,18 @@ module Make (Dummy : sig end) = struct let f_weight i j = (Vec.get env.vars j).weight < (Vec.get env.vars i).weight - + let f_filter i = (Vec.get env.vars i).level < 0 let insert_var_order v = Iheap.insert f_weight env.order v.vid let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay - -let clause_decay_activity () = + +let clause_decay_activity () = env.clause_inc <- env.clause_inc *. env.clause_decay -let var_bump_activity v = +let var_bump_activity v = v.weight <- v.weight +. env.var_inc; if v.weight > 1e100 then begin for i = 0 to env.vars.Vec.sz - 1 do @@ -245,9 +245,9 @@ let var_bump_activity v = end; if Iheap.in_heap env.order v.vid then Iheap.decrease f_weight env.order v.vid - -let clause_bump_activity c = + +let clause_bump_activity c = c.activity <- c.activity +. env.clause_inc; if c.activity > 1e20 then begin for i = 0 to env.learnts.Vec.sz - 1 do @@ -264,32 +264,32 @@ let nb_clauses () = Vec.size env.clauses let nb_learnts () = Vec.size env.learnts let nb_vars () = Vec.size env.vars -let new_decision_level() = +let new_decision_level() = Vec.push env.trail_lim (Vec.size env.trail); Vec.push env.tenv_queue env.tenv (* save the current tenv *) -let attach_clause c = +let attach_clause c = Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c; - if c.learnt then + if c.learnt then env.learnts_literals <- env.learnts_literals + Vec.size c.atoms else env.clauses_literals <- env.clauses_literals + Vec.size c.atoms - -let detach_clause c = + +let detach_clause c = c.removed <- true; (* Vec.remove (Vec.get c.atoms 0).neg.watched c; Vec.remove (Vec.get c.atoms 1).neg.watched c; *) - if c.learnt then + if c.learnt then env.learnts_literals <- env.learnts_literals - Vec.size c.atoms else env.clauses_literals <- env.clauses_literals - Vec.size c.atoms let remove_clause c = detach_clause c -let satisfied c = +let satisfied c = try for i = 0 to Vec.size c.atoms - 1 do if (Vec.get c.atoms i).is_true then raise Exit @@ -298,7 +298,7 @@ let satisfied c = with Exit -> true (* annule tout jusqu'a lvl *exclu* *) -let cancel_until lvl = +let cancel_until lvl = if decision_level () > lvl then begin env.qhead <- Vec.get env.trail_lim lvl; for c = Vec.size env.trail - 1 downto env.qhead do @@ -318,7 +318,7 @@ let cancel_until lvl = end; assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) -let rec pick_branch_lit () = +let rec pick_branch_lit () = let max = Iheap.remove_min f_weight env.order in let v = Vec.get env.vars max in if v.level>= 0 then begin @@ -328,7 +328,7 @@ let rec pick_branch_lit () = else v let enqueue a lvl reason = - assert (not a.is_true && not a.neg.is_true && + assert (not a.is_true && not a.neg.is_true && a.var.level < 0 && a.var.reason = None && lvl >= 0); (* Garder la reason car elle est utile pour les unsat-core *) (*let reason = if lvl = 0 then None else reason in*) @@ -338,10 +338,10 @@ let enqueue a lvl reason = (*eprintf "enqueue: %a@." Debug.atom a; *) Vec.push env.trail a -let progress_estimate () = +let progress_estimate () = let prg = ref 0. in let nbv = to_float (nb_vars()) in - let lvl = decision_level () in + let lvl = decision_level () in let _F = 1. /. nbv in for i = 0 to lvl do let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in @@ -360,14 +360,14 @@ let propagate_in_clause a c i watched new_sz = let first = Vec.get atoms 0 in if first.is_true then begin (* clause vraie, la garder dans les watched *) - Vec.set watched !new_sz c; + Vec.set watched !new_sz c; incr new_sz; end - else + else try (* chercher un nouveau watcher *) for k = 2 to Vec.size atoms - 1 do let ak = Vec.get atoms k in - if not (ak.neg.is_true) then begin + if not (ak.neg.is_true) then begin (* Watcher Trouve: mettre a jour et sortir *) Vec.set atoms 1 ak; Vec.set atoms k a.neg; @@ -387,22 +387,22 @@ let propagate_in_clause a c i watched new_sz = end else begin (* la clause est unitaire *) - Vec.set watched !new_sz c; + Vec.set watched !new_sz c; incr new_sz; enqueue first (decision_level ()) (Some c) end with Exit -> () - -let propagate_atom a res = + +let propagate_atom a res = let watched = a.watched in let new_sz_w = ref 0 in - begin + begin try for i = 0 to Vec.size watched - 1 do let c = Vec.get watched i in if not c.removed then propagate_in_clause a c i watched new_sz_w done; - with Conflict c -> assert (!res = None); res := Some c + with Conflict c -> assert (!res = None); res := Some c end; let dead_part = Vec.size watched - !new_sz_w in Vec.shrink watched dead_part @@ -416,7 +416,7 @@ let expensive_theory_propagate () = None (* with Exception.Inconsistent dep -> *) (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) (* Some dep *) - + let theory_propagate () = let facts = ref [] in while not (Queue.is_empty env.tatoms_queue) do @@ -425,7 +425,7 @@ let theory_propagate () = (*let ex = if a.var.level > 0 then Ex.singleton a else Ex.empty in*) let ex = Ex.singleton a in (* Usefull for debugging *) facts := (a.lit, ex) :: !facts - else + else if a.neg.is_true then (*let ex = if a.var.level > 0 then Ex.singleton a.neg else Ex.empty in*) let ex = Ex.singleton a.neg in (* Usefull for debugging *) @@ -434,17 +434,17 @@ let theory_propagate () = done; try let full_model = nb_assigns() = env.nb_init_vars in - env.tenv <- - List.fold_left - (fun t (a,ex) -> let t,_,_ = Th.assume ~cs:true a ex t in t) + env.tenv <- + List.fold_left + (fun t (a,ex) -> let t,_,_ = Th.assume ~cs:true a ex t in t) env.tenv !facts; if full_model then expensive_theory_propagate () else None - with Exception.Inconsistent dep -> + with Exception.Inconsistent dep -> (* eprintf "th inconsistent : %a @." Ex.print dep; *) Some dep -let propagate () = +let propagate () = let num_props = ref 0 in let res = ref None in (*assert (Queue.is_empty env.tqueue);*) @@ -460,7 +460,7 @@ let propagate () = !res -let analyze c_clause = +let analyze c_clause = let pathC = ref 0 in let learnt = ref [] in let cond = ref true in @@ -490,14 +490,14 @@ let analyze c_clause = end end done; - + (* look for the next node to expand *) while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; decr pathC; let p = Vec.get env.trail !tr_ind in decr tr_ind; match !pathC, p.var.reason with - | 0, _ -> + | 0, _ -> cond := false; learnt := p.neg :: (List.rev !learnt) | n, None -> assert false @@ -506,12 +506,12 @@ let analyze c_clause = List.iter (fun q -> q.var.seen <- false) !seen; !blevel, !learnt, !history, !size -let f_sort_db c1 c2 = +let f_sort_db c1 c2 = let sz1 = Vec.size c1.atoms in let sz2 = Vec.size c2.atoms in let c = compare c1.activity c2.activity in if sz1 = sz2 && c = 0 then 0 - else + else if sz1 > 2 && (sz2 = 2 || c < 0) then -1 else 1 @@ -534,22 +534,22 @@ let reduce_db () = () let j = ref 0 in for i = 0 to lim1 - 1 do let c = Vec.get env.learnts i in - if Vec.size c.atoms > 2 && not (locked c) then + if Vec.size c.atoms > 2 && not (locked c) then remove_clause c - else + else begin Vec.set env.learnts !j c; incr j end done; - for i = lim1 to lim2 - 1 do + for i = lim1 to lim2 - 1 do let c = Vec.get env.learnts i in if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then remove_clause c - else + else begin Vec.set env.learnts !j c; incr j end done; Vec.shrink env.learnts (lim2 - !j) *) -let remove_satisfied vec = +let remove_satisfied vec = let j = ref 0 in let k = Vec.size vec - 1 in for i = 0 to k do @@ -563,7 +563,7 @@ let remove_satisfied vec = Vec.shrink vec (k + 1 - !j) -module HUC = Hashtbl.Make +module HUC = Hashtbl.Make (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) @@ -580,15 +580,15 @@ let report_b_unsat ({atoms=atoms} as confl) = (fun hc -> eprintf " %a@." Debug.clause hc )!l; - end; + end; let uc = HUC.create 17 in - let rec roots todo = + let rec roots todo = match todo with | [] -> () | c::r -> for i = 0 to Vec.size c.atoms - 1 do let v = (Vec.get c.atoms i).var in - if not v.seen then begin + if not v.seen then begin v.seen <- true; roots v.vpremise; match v.reason with None -> () | Some r -> roots [r]; @@ -612,7 +612,7 @@ let report_b_unsat ({atoms=atoms} as confl) = let report_t_unsat dep = - let l = + let l = Ex.fold_atoms (fun {var=v} l -> let l = List.rev_append v.vpremise l in @@ -627,13 +627,13 @@ let report_t_unsat dep = )l; end; let uc = HUC.create 17 in - let rec roots todo = + let rec roots todo = match todo with | [] -> () | c::r -> for i = 0 to Vec.size c.atoms - 1 do let v = (Vec.get c.atoms i).var in - if not v.seen then begin + if not v.seen then begin v.seen <- true; roots v.vpremise; match v.reason with None -> () | Some r -> roots [r]; @@ -655,10 +655,10 @@ let report_t_unsat dep = env.unsat_core <- unsat_core; raise (Unsat unsat_core) -let simplify () = +let simplify () = assert (decision_level () = 0); if env.is_unsat then raise (Unsat env.unsat_core); - begin + begin match propagate () with | Some confl -> report_b_unsat confl | None -> @@ -674,7 +674,7 @@ let simplify () = env.simpDB_props <- env.clauses_literals + env.learnts_literals; end -let record_learnt_clause blevel learnt history size = +let record_learnt_clause blevel learnt history size = begin match learnt with | [] -> assert false | [fuip] -> @@ -692,7 +692,7 @@ let record_learnt_clause blevel learnt history size = var_decay_activity (); clause_decay_activity() -let check_inconsistence_of dep = +let check_inconsistence_of dep = try let env = ref (Th.empty()) in (); Ex.iter_atoms @@ -704,12 +704,12 @@ let check_inconsistence_of dep = assert false with Exception.Inconsistent _ -> () -let theory_analyze dep = - let atoms, sz, max_lvl, c_hist = +let theory_analyze dep = + let atoms, sz, max_lvl, c_hist = Ex.fold_atoms (fun a (acc, sz, max_lvl, c_hist) -> let c_hist = List.rev_append a.var.vpremise c_hist in - let c_hist = match a.var.reason with + let c_hist = match a.var.reason with | None -> c_hist | Some r -> r:: c_hist in if a.var.level = 0 then acc, sz, max_lvl, c_hist else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist @@ -748,20 +748,20 @@ let theory_analyze dep = seen := q :: !seen; if q.var.level >= max_lvl then incr pathC else begin - learnt := q :: !learnt; + learnt := q :: !learnt; incr size; blevel := max !blevel q.var.level end end done; - + (* look for the next node to expand *) while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; decr pathC; let p = Vec.get env.trail !tr_ind in decr tr_ind; match !pathC, p.var.reason with - | 0, _ -> + | 0, _ -> cond := false; learnt := p.neg :: (List.rev !learnt) | n, None -> assert false @@ -779,7 +779,7 @@ let add_boolean_conflict confl = cancel_until blevel; record_learnt_clause blevel learnt history size -let search n_of_conflicts n_of_learnts = +let search n_of_conflicts n_of_learnts = let conflictC = ref 0 in env.starts <- env.starts + 1; while (true) do @@ -787,20 +787,20 @@ let search n_of_conflicts n_of_learnts = | Some confl -> (* Conflict *) incr conflictC; add_boolean_conflict confl - + | None -> (* No Conflict *) match theory_propagate () with - | Some dep -> + | Some dep -> incr conflictC; env.conflicts <- env.conflicts + 1; if decision_level() = 0 then report_t_unsat dep; (* T-L conflict *) let blevel, learnt, history, size = theory_analyze dep in cancel_until blevel; record_learnt_clause blevel learnt history size - - | None -> + + | None -> if nb_assigns () = env.nb_init_vars then raise Sat; - if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then + if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then begin env.progress_estimate <- progress_estimate(); cancel_until 0; @@ -808,8 +808,8 @@ let search n_of_conflicts n_of_learnts = end; if decision_level() = 0 then simplify (); - if n_of_learnts >= 0 && - Vec.size env.learnts - nb_assigns() >= n_of_learnts then + if n_of_learnts >= 0 && + Vec.size env.learnts - nb_assigns() >= n_of_learnts then reduce_db(); env.decisions <- env.decisions + 1; @@ -822,7 +822,7 @@ let search n_of_conflicts n_of_learnts = enqueue next.pa current_level None done -let check_clause c = +let check_clause c = let b = ref false in let atoms = c.atoms in for i = 0 to Vec.size atoms - 1 do @@ -830,16 +830,16 @@ let check_clause c = b := !b || a.is_true done; assert (!b) - -let check_vec vec = + +let check_vec vec = for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done - -let check_model () = + +let check_model () = check_vec env.clauses; check_vec env.learnts -let solve () = +let solve () = if env.is_unsat then raise (Unsat env.unsat_core); let n_of_conflicts = ref (to_float env.restart_first) in let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in @@ -850,11 +850,11 @@ let solve () = n_of_conflicts := !n_of_conflicts *. env.restart_inc; n_of_learnts := !n_of_learnts *. env.learntsize_inc; done; - with - | Sat -> + with + | Sat -> (*check_model ();*) raise Sat - | (Unsat cl) as e -> + | (Unsat cl) as e -> (* check_unsat_core cl; *) raise e @@ -863,13 +863,13 @@ exception Trivial let partition atoms init = let rec partition_aux trues unassigned falses init = function | [] -> trues @ unassigned @ falses, init - | a::r -> - if a.is_true then + | a::r -> + if a.is_true then if a.var.level = 0 then raise Trivial else (a::trues) @ unassigned @ falses @ r, init else if a.neg.is_true then - if a.var.level = 0 then - partition_aux trues unassigned falses + if a.var.level = 0 then + partition_aux trues unassigned falses (List.rev_append (a.var.vpremise) init) r else partition_aux trues unassigned (a::falses) init r else partition_aux trues (a::unassigned) falses init r @@ -882,12 +882,12 @@ let add_clause ~cnumber atoms = let init_name = string_of_int cnumber in let init0 = make_clause init_name atoms (List.length atoms) false [] in try - let atoms, init = + let atoms, init = if decision_level () = 0 then let atoms, init = List.fold_left - (fun (atoms, init) a -> + (fun (atoms, init) a -> if a.is_true then raise Trivial; - if a.neg.is_true then + if a.neg.is_true then atoms, (List.rev_append (a.var.vpremise) init) else a::atoms, init ) ([], [init0]) atoms in @@ -896,41 +896,41 @@ let add_clause ~cnumber atoms = in let size = List.length atoms in match atoms with - | [] -> + | [] -> report_b_unsat init0; - - | a::_::_ -> + + | a::_::_ -> let name = fresh_name () in let clause = make_clause name atoms size false init in attach_clause clause; Vec.push env.clauses clause; - + if a.neg.is_true then begin let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in cancel_until lvl; add_boolean_conflict clause end - + | [a] -> cancel_until 0; a.var.vpremise <- init; enqueue a 0 None; - match propagate () with + match propagate () with None -> () | Some confl -> report_b_unsat confl with Trivial -> () -let add_clauses cnf ~cnumber = +let add_clauses cnf ~cnumber = List.iter (add_clause ~cnumber) cnf; match theory_propagate () with None -> () | Some dep -> report_t_unsat dep - + let init_solver cnf ~cnumber = let nbv, _ = made_vars_info () in let nbc = env.nb_init_clauses + List.length cnf in Vec.grow_to_by_double env.vars nbv; Iheap.grow_to_by_double env.order nbv; - List.iter - (List.iter + List.iter + (List.iter (fun a -> Vec.set env.vars a.var.vid a.var; insert_var_order a.var @@ -952,11 +952,11 @@ let clear () = let empty_theory = Th.empty () in env.is_unsat <- false; env.unsat_core <- []; - env.clauses <- Vec.make 0 dummy_clause; - env.learnts <- Vec.make 0 dummy_clause; + env.clauses <- Vec.make 0 dummy_clause; + env.learnts <- Vec.make 0 dummy_clause; env.clause_inc <- 1.; env.var_inc <- 1.; - env.vars <- Vec.make 0 dummy_var; + env.vars <- Vec.make 0 dummy_var; env.qhead <- 0; env.simpDB_assigns <- -1; env.simpDB_props <- 0; diff --git a/smt/solver_types.ml b/smt/solver_types.ml index 50519bfb..8d1cbf3d 100644 --- a/smt/solver_types.ml +++ b/smt/solver_types.ml @@ -13,7 +13,7 @@ open Format -let ale = Hstring.make "<=" +let ale = Hstring.make "<=" let alt = Hstring.make "<" let agt = Hstring.make ">" @@ -31,8 +31,8 @@ type var = mutable level : int; mutable reason: reason; mutable vpremise : premise} - -and atom = + +and atom = { var : var; lit : Literal.LT.t; neg : atom; @@ -40,9 +40,9 @@ and atom = mutable is_true : bool; aid : int } -and clause = - { name : string; - mutable atoms : atom Vec.t ; +and clause = + { name : string; + mutable atoms : atom Vec.t ; mutable activity : float; mutable removed : bool; learnt : bool; @@ -59,21 +59,21 @@ let dummy_lit = Literal.LT.make (Literal.Eq(Term.vrai,Term.vrai)) let rec dummy_var = { vid = -101; pa = dummy_atom; - na = dummy_atom; + na = dummy_atom; level = -1; reason = None; weight = -1.; seen = false; vpremise = [] } -and dummy_atom = - { var = dummy_var; +and dummy_atom = + { var = dummy_var; lit = dummy_lit; watched = {Vec.dummy=dummy_clause; data=[||]; sz=0}; neg = dummy_atom; is_true = false; aid = -102 } -and dummy_clause = - { name = ""; +and dummy_clause = + { name = ""; atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0}; activity = -1.; removed = false; @@ -82,8 +82,8 @@ and dummy_clause = module MA = Literal.LT.Map - -let ale = Hstring.make "<=" + +let ale = Hstring.make "<=" let alt = Hstring.make "<" let agt = Hstring.make ">" let is_le n = Hstring.compare n ale = 0 @@ -132,7 +132,7 @@ let normal_form lit = (* | Literal.Distinct(false,[_;_]) -> Literal.LT.neg lit, true *) (* | Literal.Builtin(true,n,[t1;t2]) when Builtin.is_gt n -> *) (* Literal.LT.neg lit, true *) - + (* | Literal.Builtin(false,n,[t1;t2]) when Builtin.is_le n -> *) (* Literal.LT.neg lit, true *) (* | _ -> lit, false *) @@ -143,33 +143,33 @@ let ma = ref MA.empty let make_var = fun lit -> let lit, negated = normal_form lit in - try MA.find lit !ma, negated + try MA.find lit !ma, negated with Not_found -> let cpt_fois_2 = !cpt_mk_var lsl 1 in - let rec var = - { vid = !cpt_mk_var; + let rec var = + { vid = !cpt_mk_var; pa = pa; - na = na; + na = na; level = -1; reason = None; weight = 0.; seen = false; vpremise = []; } - and pa = - { var = var; + and pa = + { var = var; lit = lit; - watched = Vec.make 10 dummy_clause; + watched = Vec.make 10 dummy_clause; neg = na; is_true = false; aid = cpt_fois_2 (* aid = vid*2 *) } - and na = + and na = { var = var; lit = Literal.LT.neg lit; watched = Vec.make 10 dummy_clause; neg = pa; is_true = false; - aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in + aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in ma := MA.add lit var !ma; incr cpt_mk_var; var, negated @@ -178,9 +178,9 @@ let made_vars_info () = !cpt_mk_var, MA.fold (fun lit var acc -> var::acc)!ma [] let add_atom lit = let var, negated = make_var lit in - if negated then var.na else var.pa + if negated then var.na else var.pa -let make_clause name ali sz_ali is_learnt premise = +let make_clause name ali sz_ali is_learnt premise = let atoms = Vec.from_list ali sz_ali dummy_atom in { name = name; atoms = atoms; @@ -188,23 +188,23 @@ let make_clause name ali sz_ali is_learnt premise = learnt = is_learnt; activity = 0.; cpremise = premise} - + let fresh_lname = - let cpt = ref 0 in + let cpt = ref 0 in fun () -> incr cpt; "L" ^ (string_of_int !cpt) let fresh_dname = - let cpt = ref 0 in + let cpt = ref 0 in fun () -> incr cpt; "D" ^ (string_of_int !cpt) - + let fresh_name = - let cpt = ref 0 in + let cpt = ref 0 in fun () -> incr cpt; "C" ^ (string_of_int !cpt) module Clause = struct - + let size c = Vec.size c.atoms let pop c = Vec.pop c.atoms let shrink c i = Vec.shrink c.atoms i @@ -227,32 +227,32 @@ end module Debug = struct - + let sign a = if a==a.var.pa then "" else "-" - + let level a = - match a.var.level, a.var.reason with + match a.var.level, a.var.reason with | n, _ when n < 0 -> assert false | 0, Some c -> sprintf "->0/%s" c.name | 0, None -> "@0" | n, Some c -> sprintf "->%d/%s" n c.name | n, None -> sprintf "@@%d" n - let value a = + let value a = if a.is_true then sprintf "[T%s]" (level a) else if a.neg.is_true then sprintf "[F%s]" (level a) else "" - let value_ms_like a = + let value_ms_like a = if a.is_true then sprintf ":1%s" (level a) else if a.neg.is_true then sprintf ":0%s" (level a) else ":X" - let premise fmt v = + let premise fmt v = List.iter (fun {name=name} -> fprintf fmt "%s," name) v - let atom fmt a = - fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" + let atom fmt a = + fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" (sign a) (a.var.vid+1) (value a) Literal.LT.print a.lit premise a.var.vpremise @@ -260,7 +260,7 @@ module Debug = struct let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr - let atoms_vec fmt vec = + let atoms_vec fmt vec = for i = 0 to Vec.size vec - 1 do fprintf fmt "%a ; " atom (Vec.get vec i) done diff --git a/smt/solver_types.mli b/smt/solver_types.mli index b951c2b7..78a0a230 100644 --- a/smt/solver_types.mli +++ b/smt/solver_types.mli @@ -13,7 +13,7 @@ -type var = +type var = { vid : int; pa : atom; na : atom; @@ -22,8 +22,8 @@ type var = mutable level : int; mutable reason : reason; mutable vpremise : premise } - -and atom = + +and atom = { var : var; lit : Literal.LT.t; neg : atom; @@ -31,7 +31,7 @@ and atom = mutable is_true : bool; aid : int } -and clause = +and clause = { name : string; mutable atoms : atom Vec.t; mutable activity : float; @@ -54,7 +54,7 @@ val dummy_clause : clause val make_var : Literal.LT.t -> var * bool -val add_atom : Literal.LT.t -> atom +val add_atom : Literal.LT.t -> atom val make_clause : string -> atom list -> int -> bool -> premise-> clause @@ -73,9 +73,9 @@ val clear : unit -> unit end module Debug: sig - + val atom : Format.formatter -> atom -> unit - + val clause : Format.formatter -> clause -> unit end diff --git a/smt/sum.ml b/smt/sum.ml index d9aea3c7..83b7755e 100644 --- a/smt/sum.ml +++ b/smt/sum.ml @@ -14,7 +14,7 @@ open Format open Sig -open Exception +open Exception module Sy = Symbols module T = Term module A = Literal @@ -36,27 +36,27 @@ module Make(X : ALIEN) = struct 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 + + 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 + | 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 @@ -64,41 +64,41 @@ module Make(X : ALIEN) = struct let embed r = match X.extract r with | Some c -> c - | None -> Alien r + | None -> Alien r let is_mine = function | Alien r -> r | Cons(hs,ty) as c -> X.embed c - - let compare c1 c2 = + + let compare c1 c2 = match c1 , c2 with - | Cons (h1,ty1) , Cons (h2,ty2) -> + | 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 subst p v c = let cr = is_mine c in if X.equal p cr then v - else + 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 = + + 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 @@ -131,29 +131,29 @@ module Make(X : ALIEN) = struct end let values_of r = match X.type_info r with - | Ty.Tsum (_,l) -> + | 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 = + let add_diseq hss sm1 sm2 dep env eqs = match sm1, sm2 with - | Alien r , Cons(h,ty) + | 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 + 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 = + let add_eq hss sm1 sm2 dep env eqs = match sm1, sm2 with | Alien r, Cons(h,ty) | Cons (h,ty), Alien r -> @@ -161,13 +161,13 @@ module Make(X : ALIEN) = struct 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 -> + + | 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 + 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 @@ -179,28 +179,28 @@ module Make(X : ALIEN) = struct | _ -> env, eqs - let assume env la = + let assume env la = let aux bol r1 r2 dep env eqs = function | None -> env, eqs - | Some hss -> + | Some hss -> Debug.assume bol r1 r2; - if bol then + 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 = + let env, eqs = List.fold_left (fun (env,eqs) -> function - | A.Eq(r1,r2), _, ex -> + | A.Eq(r1,r2), _, ex -> aux true r1 r2 ex env eqs (values_of r1) - - | A.Distinct(false, [r1;r2]), _, ex -> + + | 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 = [] } @@ -223,15 +223,15 @@ module Make(X : ALIEN) = struct 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 + 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 + | Alien r, Some hss -> + if MX.mem r env then env else MX.add r (hss, Ex.empty) env | _ -> env diff --git a/smt/sum.mli b/smt/sum.mli index 113fc10d..7402d977 100644 --- a/smt/sum.mli +++ b/smt/sum.mli @@ -20,6 +20,6 @@ module type ALIEN = sig val extract : r -> (r abstract) option end -module Make +module Make (X : ALIEN) : Sig.THEORY with type r = X.r and type t = X.r abstract diff --git a/smt/symbols.ml b/smt/symbols.ml index bf627e23..62570e36 100644 --- a/smt/symbols.ml +++ b/smt/symbols.ml @@ -13,13 +13,13 @@ open Hashcons -type operator = - | Plus | Minus | Mult | Div | Modulo +type operator = + | Plus | Minus | Mult | Div | Modulo type name_kind = Ac | Constructor | Other -type t = - | True +type t = + | True | False | Name of Hstring.t * name_kind | Int of Hstring.t @@ -47,7 +47,7 @@ let compare_kind k1 k2 = match k1, k2 with | Constructor, Constructor -> 0 let compare s1 s2 = match s1, s2 with - | Name (n1,k1), Name (n2,k2) -> + | 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 @@ -59,7 +59,7 @@ let compare s1 s2 = match s1, s2 with | Int _, _ -> -1 | _ ,Int _ -> 1 | _ -> Pervasives.compare s1 s2 - + let equal s1 s2 = compare s1 s2 = 0 let hash = function @@ -73,8 +73,8 @@ let to_string = function | Var x -> "*var* "^(Hstring.view x) | Int n -> Hstring.view n | Real n -> Hstring.view n - | Op Plus -> "+" - | Op Minus -> "-" + | Op Plus -> "+" + | Op Minus -> "-" | Op Mult -> "*" | Op Div -> "/" | Op Modulo -> "%" @@ -86,6 +86,6 @@ 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 = +module Set = Set.Make(struct type t' = t type t=t' let compare=compare end) diff --git a/smt/symbols.mli b/smt/symbols.mli index 68727798..97494b82 100644 --- a/smt/symbols.mli +++ b/smt/symbols.mli @@ -11,13 +11,13 @@ (* *) (**************************************************************************) -type operator = - | Plus | Minus | Mult | Div | Modulo +type operator = + | Plus | Minus | Mult | Div | Modulo type name_kind = Ac | Constructor | Other -type t = - | True +type t = + | True | False | Name of Hstring.t * name_kind | Int of Hstring.t diff --git a/smt/term.ml b/smt/term.ml index 7cf31329..c92f597d 100644 --- a/smt/term.ml +++ b/smt/term.ml @@ -22,26 +22,26 @@ 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 + 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) + 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 rec print fmt t = let {f=x; xs=l; ty=ty} = view t in match x, l with - | Sy.Op op, [e1; e2] -> + | 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 @@ -72,11 +72,11 @@ 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 = + +module Set = Set.Make(struct type t' = t type t=t' let compare=compare end) - -module Map = + +module Map = Map.Make(struct type t' = t type t=t' let compare=compare end) diff --git a/smt/ty.ml b/smt/ty.ml index 1375f1c7..1bcdadf1 100644 --- a/smt/ty.ml +++ b/smt/ty.ml @@ -13,7 +13,7 @@ open Format -type t = +type t = | Tint | Treal | Tbool @@ -23,33 +23,33 @@ type t = let hash t = match t with | Tabstract s -> Hstring.hash s - | Tsum (s, l) -> - let h = - List.fold_left + | 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 = +let equal t1 t2 = match t1, t2 with - | Tabstract s1, Tabstract s2 + | Tabstract s1, Tabstract s2 | Tsum (s1, _), Tsum (s2, _) -> Hstring.equal s1 s2 | Tint, Tint | Treal, Treal | Tbool, Tbool -> true | _ -> false -let compare t1 t2 = +let compare t1 t2 = match t1, t2 with | Tabstract s1, Tabstract s2 -> - Hstring.compare s1 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 = +let print fmt ty = match ty with | Tint -> fprintf fmt "int" | Treal -> fprintf fmt "real" diff --git a/smt/ty.mli b/smt/ty.mli index d42e3feb..b821aeb5 100644 --- a/smt/ty.mli +++ b/smt/ty.mli @@ -11,7 +11,7 @@ (* *) (**************************************************************************) -type t = +type t = | Tint | Treal | Tbool diff --git a/smt/uf.ml b/smt/uf.ml index 41591f59..6162b540 100644 --- a/smt/uf.ml +++ b/smt/uf.ml @@ -28,9 +28,9 @@ module type S = sig 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 -> + + 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 @@ -41,7 +41,7 @@ module type S = sig val class_of : t -> Term.t -> Term.t list end - + module Make ( R : Sig.X ) = struct module L = List @@ -52,112 +52,112 @@ module Make ( R : Sig.X ) = struct 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 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') = + 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 + if c <> 0 then c else R.compare r1' r2' end) - type t = { + type t = { (* term -> [t] *) - make : R.r MapT.t; - + make : R.r MapT.t; + (* representative table *) - repr : (R.r * Ex.t) MapR.t; - + 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; - + gamma : SetR.t MapR.t; + (* the disequations map *) - neqs: Ex.t MapL.t MapR.t; - + neqs: Ex.t MapL.t MapR.t; + } - - let empty = { - make = MapT.empty; + + let empty = { + make = MapT.empty; repr = MapR.empty; - classes = 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 -> + with Not_found -> assert false (*R.make t, Ex.empty*) (* XXXX *) - - let lookup_by_r r env = + + 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 + 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 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 = + let add_to_gamma r c gamma = L.fold_left - (fun gamma x -> + (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 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 = + let mapl = MapL.fold - (fun l1 ex1 mapl -> - try + (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) + 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 = + 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 + (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 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 @@ -169,38 +169,38 @@ module Make ( R : Sig.X ) = struct 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 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 + repr = + if in_repr then env.repr else MapR.add p (p, Ex.empty) env.repr; - classes = + classes = if in_repr then env.classes else update_classes p p env.classes; - gamma = + 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 = + 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; + { 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 = + 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 -> + + 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}) @@ -209,37 +209,37 @@ module Make ( R : Sig.X ) = struct 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) -> + 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 + else let ex = Ex.union ex dep in - let env = + let env = {env with repr = MapR.add r (nrr, ex) env.repr; - gamma = add_to_gamma r nrr env.gamma } + 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 + 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 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 + 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) = + 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 @@ -248,51 +248,51 @@ module Make ( R : Sig.X ) = struct 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 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 + else begin ignore (Env.update_neqs rr1 rr2 dep env); - try R.solve rr1 rr2 + try R.solve rr1 rr2 with Unsolvable -> raise (Inconsistent dep) end - - let rec ac_x eqs env tch = + + let rec ac_x eqs env tch = if Queue.is_empty eqs then env, tch - else + 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 + 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 = + let env, _, newds = List.fold_left - (fun (env, mapr, newds) r -> - let rr, ex = Env.find_or_normal_form env r in + (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 = + let mdis = try MapR.find rr env.neqs with Not_found -> MapL.empty in - let mdis = - try + let mdis = + try MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis - with Not_found -> + with Not_found -> MapL.add d uex mdis in let env = Env.init_leaf env rr in @@ -302,29 +302,29 @@ module Make ( R : Sig.X ) = struct (env, MapR.empty, []) rl in - List.fold_left - (fun env (r1, ex1, mapr) -> - MapR.fold (fun r2 ex2 env -> + 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] -> + | [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) + | [] -> + raise (Inconsistent ex) | _ -> env with Unsolvable -> env) mapr env) env newds - - let are_equal env t1 t2 = + + let are_equal env t1 t2 = let r1, ex_r1 = Env.lookup_by_t t1 env in let 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 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 @@ -332,25 +332,25 @@ module Make ( R : Sig.X ) = struct No with Inconsistent ex -> Yes(ex) - let already_distinct env lr = + let already_distinct env lr = let d = Lit.make (Literal.Distinct (false,lr)) in - try - List.iter (fun r -> + 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 = + + 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 class_of env t = + try let rt, _ = MapR.find (MapT.find t env.make) env.repr in SetT.elements (MapR.find rt env.classes) with Not_found -> [t] diff --git a/smt/uf.mli b/smt/uf.mli index 0106d5ce..09a70012 100644 --- a/smt/uf.mli +++ b/smt/uf.mli @@ -26,8 +26,8 @@ module type S = sig val find_r : t -> R.r -> R.r * Explanation.t - val union : - 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 diff --git a/smt/use.ml b/smt/use.ml index b90a7017..0f61d70e 100644 --- a/smt/use.ml +++ b/smt/use.ml @@ -25,13 +25,13 @@ module SA = Set.Make(struct 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 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 @@ -41,39 +41,39 @@ module Make (X : Sig.X) = struct 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 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 = + 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 + | 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 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 + let inter = function [] -> (ST.empty, SA.empty) - | rx::l -> + | rx::l -> L.fold_left (fun acc x ->inter_tpl acc (find x g))(find rx g) l - in - L.fold_left + in + L.fold_left (fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch))) - (find p g) touched - + (find p g) touched + let print g = () let mem = G.mem diff --git a/smt/use.mli b/smt/use.mli index 9629b540..651db3ab 100644 --- a/smt/use.mli +++ b/smt/use.mli @@ -16,23 +16,23 @@ 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 + + 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