From dc43c28a0220fd65118e0de13cc44bf6c19f8126 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 31 Oct 2014 16:40:59 +0100 Subject: [PATCH] Everything has now been properly indented with ocp-indent. --- .ocp-indent | 3 + common/bitv.ml | 160 ++-- common/hashcons.ml | 56 +- common/hashcons.mli | 90 +- common/heap.ml | 14 +- common/hstring.ml | 18 +- sat/explanation.ml | 62 +- sat/explanation_intf.ml | 26 +- sat/solver.ml | 1690 +++++++++++++++++++------------------- sat/solver.mli | 24 +- sat/solver_types.ml | 226 ++--- sat/solver_types_intf.ml | 94 +-- sat/theory_intf.ml | 12 +- smt/arith.ml | 232 +++--- smt/arith.mli | 6 +- smt/cc.ml | 420 +++++----- smt/combine.ml | 154 ++-- smt/fm.ml | 832 +++++++++---------- smt/fm.mli | 4 +- smt/intervals.ml | 610 +++++++------- smt/literal.ml | 118 +-- smt/polynome.ml | 50 +- smt/polynome.mli | 2 +- smt/sig.mli | 6 +- smt/smt.ml | 442 +++++----- smt/smt.mli | 28 +- smt/sum.ml | 148 ++-- smt/sum.mli | 2 +- smt/symbols.ml | 6 +- smt/term.ml | 22 +- smt/ty.ml | 52 +- smt/uf.ml | 228 ++--- smt/use.ml | 24 +- smt/use.mli | 24 +- 34 files changed, 2944 insertions(+), 2941 deletions(-) create mode 100644 .ocp-indent diff --git a/.ocp-indent b/.ocp-indent new file mode 100644 index 00000000..5641e31d --- /dev/null +++ b/.ocp-indent @@ -0,0 +1,3 @@ +base=2 +type=2 +max_indent=4 diff --git a/common/bitv.ml b/common/bitv.ml index cfe6162d..af9c438a 100644 --- a/common/bitv.ml +++ b/common/bitv.ml @@ -150,15 +150,15 @@ let blit_bits a i m v n = let d = m + j - bpi in if d > 0 then begin Array.unsafe_set v i' - (((keep_lowest_bits (a lsr i) (bpi - j)) lsl j) lor - (keep_lowest_bits (Array.unsafe_get v i') j)); + (((keep_lowest_bits (a lsr i) (bpi - j)) lsl j) lor + (keep_lowest_bits (Array.unsafe_get v i') j)); Array.unsafe_set v (succ i') - ((keep_lowest_bits (a lsr (i + bpi - j)) d) lor - (keep_highest_bits (Array.unsafe_get v (succ i')) (bpi - d))) + ((keep_lowest_bits (a lsr (i + bpi - j)) d) lor + (keep_highest_bits (Array.unsafe_get v (succ i')) (bpi - d))) end else Array.unsafe_set v i' - (((keep_lowest_bits (a lsr i) m) lsl j) lor - ((Array.unsafe_get v i') land (low_mask.(j) lor high_mask.(-d)))) + (((keep_lowest_bits (a lsr i) m) lsl j) lor + ((Array.unsafe_get v i') land (low_mask.(j) lor high_mask.(-d)))) (*s [blit_int] implements [blit_bits] in the particular case when [i=0] and [m=bpi] i.e. when we blit all the bits of [a]. *) @@ -170,7 +170,7 @@ let blit_int a v n = else begin Array.unsafe_set v i ( (keep_lowest_bits (Array.unsafe_get v i) j) lor - ((keep_lowest_bits a (bpi - j)) lsl j)); + ((keep_lowest_bits a (bpi - j)) lsl j)); Array.unsafe_set v (succ i) ((keep_highest_bits (Array.unsafe_get v (succ i)) (bpi - j)) lor (a lsr (bpi - j))) @@ -193,15 +193,15 @@ let unsafe_blit v1 ofs1 v2 ofs2 len = blit_bits (Array.unsafe_get v1 bi) bj (bpi - bj) v2 ofs2; let n = ref (ofs2 + bpi - bj) in for i = succ bi to pred ei do - blit_int (Array.unsafe_get v1 i) v2 !n; - n := !n + bpi + blit_int (Array.unsafe_get v1 i) v2 !n; + n := !n + bpi done; blit_bits (Array.unsafe_get v1 ei) 0 (succ ej) v2 !n end let blit v1 ofs1 v2 ofs2 len = if len < 0 or ofs1 < 0 or ofs1 + len > v1.length - or ofs2 < 0 or ofs2 + len > v2.length + or ofs2 < 0 or ofs2 + len > v2.length then invalid_arg "Bitv.blit"; unsafe_blit v1.bits ofs1 v2.bits ofs2 len @@ -261,8 +261,8 @@ let blit_zeros v ofs len = blit_bits 0 bj (bpi - bj) v ofs; let n = ref (ofs + bpi - bj) in for i = succ bi to pred ei do - blit_int 0 v !n; - n := !n + bpi + blit_int 0 v !n; + n := !n + bpi done; blit_bits 0 0 (succ ej) v !n end @@ -277,8 +277,8 @@ let blit_ones v ofs len = blit_bits max_int bj (bpi - bj) v ofs; let n = ref (ofs + bpi - bj) in for i = succ bi to pred ei do - blit_int max_int v !n; - n := !n + bpi + blit_int max_int v !n; + n := !n + bpi done; blit_bits max_int 0 (succ ej) v !n end @@ -345,11 +345,11 @@ let foldi_right f v x = let iteri_true_naive f v = Array.iteri (fun i n -> if n != 0 then begin - let i_bpi = i * bpi in - for j = 0 to bpi - 1 do - if n land (Array.unsafe_get bit_j j) > 0 then f (i_bpi + j) - done - end) + let i_bpi = i * bpi in + for j = 0 to bpi - 1 do + if n land (Array.unsafe_get bit_j j) > 0 then f (i_bpi + j) + done + end) v.bits (*s Number of trailing zeros (on a 32-bit machine) *) @@ -364,11 +364,11 @@ let iteri_true_ntz32 f v = (fun i n -> let i_bpi = i * bpi in let rec visit x = - if x != 0 then begin - let b = x land (-x) in - f (i_bpi + ntz32 b); - visit (x - b) - end + if x != 0 then begin + let b = x land (-x) in + f (i_bpi + ntz32 b); + visit (x - b) + end in visit n) v.bits @@ -384,11 +384,11 @@ let iteri_true_ntz64 f v = (fun i n -> let i_bpi = i * bpi in let rec visit x = - if x != 0 then begin - let b = x land (-x) in - f (i_bpi + ntz64 b); - visit (x - b) - end + if x != 0 then begin + let b = x land (-x) in + f (i_bpi + ntz64 b); + visit (x - b) + end in visit n) v.bits @@ -547,9 +547,9 @@ module S(I : sig val least_first : bool end) = struct for i = 0 to n - 1 do let c = String.unsafe_get s i in if c = '1' then - unsafe_set v (if I.least_first then i else n-1-i) true + unsafe_set v (if I.least_first then i else n-1-i) true else - if c <> '0' then invalid_arg "Bitv.of_string" + if c <> '0' then invalid_arg "Bitv.of_string" done; v @@ -660,90 +660,90 @@ let to_int_s v = (* [Int32] *) let of_int32_us i = match Sys.word_size with | 32 -> { length = 31; - bits = [| (Int32.to_int i) land max_int; - let hi = Int32.shift_right_logical i 30 in - (Int32.to_int hi) land 1 |] } + bits = [| (Int32.to_int i) land max_int; + let hi = Int32.shift_right_logical i 30 in + (Int32.to_int hi) land 1 |] } | 64 -> { length = 31; bits = [| (Int32.to_int i) land 0x7fffffff |] } | _ -> assert false let to_int32_us v = if v.length < 31 then invalid_arg "Bitv.to_int32_us"; match Sys.word_size with - | 32 -> - Int32.logor (Int32.of_int v.bits.(0)) - (Int32.shift_left (Int32.of_int (v.bits.(1) land 1)) 30) - | 64 -> - Int32.of_int (v.bits.(0) land 0x7fffffff) - | _ -> assert false + | 32 -> + Int32.logor (Int32.of_int v.bits.(0)) + (Int32.shift_left (Int32.of_int (v.bits.(1) land 1)) 30) + | 64 -> + Int32.of_int (v.bits.(0) land 0x7fffffff) + | _ -> assert false (* this is 0xffffffff (ocaml >= 3.08 checks for literal overflow) *) let ffffffff = (0xffff lsl 16) lor 0xffff let of_int32_s i = match Sys.word_size with | 32 -> { length = 32; - bits = [| (Int32.to_int i) land max_int; - let hi = Int32.shift_right_logical i 30 in - (Int32.to_int hi) land 3 |] } + bits = [| (Int32.to_int i) land max_int; + let hi = Int32.shift_right_logical i 30 in + (Int32.to_int hi) land 3 |] } | 64 -> { length = 32; bits = [| (Int32.to_int i) land ffffffff |] } | _ -> assert false let to_int32_s v = if v.length < 32 then invalid_arg "Bitv.to_int32_s"; match Sys.word_size with - | 32 -> - Int32.logor (Int32.of_int v.bits.(0)) - (Int32.shift_left (Int32.of_int (v.bits.(1) land 3)) 30) - | 64 -> - Int32.of_int (v.bits.(0) land ffffffff) - | _ -> assert false + | 32 -> + Int32.logor (Int32.of_int v.bits.(0)) + (Int32.shift_left (Int32.of_int (v.bits.(1) land 3)) 30) + | 64 -> + Int32.of_int (v.bits.(0) land ffffffff) + | _ -> assert false (* [Int64] *) let of_int64_us i = match Sys.word_size with | 32 -> { length = 63; - bits = [| (Int64.to_int i) land max_int; - (let mi = Int64.shift_right_logical i 30 in - (Int64.to_int mi) land max_int); - let hi = Int64.shift_right_logical i 60 in - (Int64.to_int hi) land 1 |] } + bits = [| (Int64.to_int i) land max_int; + (let mi = Int64.shift_right_logical i 30 in + (Int64.to_int mi) land max_int); + let hi = Int64.shift_right_logical i 60 in + (Int64.to_int hi) land 1 |] } | 64 -> { length = 63; - bits = [| (Int64.to_int i) land max_int; - let hi = Int64.shift_right_logical i 62 in - (Int64.to_int hi) land 1 |] } + bits = [| (Int64.to_int i) land max_int; + let hi = Int64.shift_right_logical i 62 in + (Int64.to_int hi) land 1 |] } | _ -> assert false let to_int64_us v = if v.length < 63 then invalid_arg "Bitv.to_int64_us"; match Sys.word_size with - | 32 -> - Int64.logor (Int64.of_int v.bits.(0)) - (Int64.logor (Int64.shift_left (Int64.of_int v.bits.(1)) 30) - (Int64.shift_left (Int64.of_int (v.bits.(2) land 7)) 60)) - | 64 -> - Int64.logor (Int64.of_int v.bits.(0)) - (Int64.shift_left (Int64.of_int (v.bits.(1) land 1)) 62) - | _ -> - assert false + | 32 -> + Int64.logor (Int64.of_int v.bits.(0)) + (Int64.logor (Int64.shift_left (Int64.of_int v.bits.(1)) 30) + (Int64.shift_left (Int64.of_int (v.bits.(2) land 7)) 60)) + | 64 -> + Int64.logor (Int64.of_int v.bits.(0)) + (Int64.shift_left (Int64.of_int (v.bits.(1) land 1)) 62) + | _ -> + assert false let of_int64_s i = match Sys.word_size with | 32 -> { length = 64; - bits = [| (Int64.to_int i) land max_int; - (let mi = Int64.shift_right_logical i 30 in - (Int64.to_int mi) land max_int); - let hi = Int64.shift_right_logical i 60 in - (Int64.to_int hi) land 3 |] } + bits = [| (Int64.to_int i) land max_int; + (let mi = Int64.shift_right_logical i 30 in + (Int64.to_int mi) land max_int); + let hi = Int64.shift_right_logical i 60 in + (Int64.to_int hi) land 3 |] } | 64 -> { length = 64; bits = [| (Int64.to_int i) land max_int; let hi = Int64.shift_right_logical i 62 in - (Int64.to_int hi) land 3 |] } + (Int64.to_int hi) land 3 |] } | _ -> assert false let to_int64_s v = if v.length < 64 then invalid_arg "Bitv.to_int64_s"; match Sys.word_size with - | 32 -> - Int64.logor (Int64.of_int v.bits.(0)) - (Int64.logor (Int64.shift_left (Int64.of_int v.bits.(1)) 30) - (Int64.shift_left (Int64.of_int (v.bits.(2) land 15)) 60)) - | 64 -> - Int64.logor (Int64.of_int v.bits.(0)) - (Int64.shift_left (Int64.of_int (v.bits.(1) land 3)) 62) - | _ -> assert false + | 32 -> + Int64.logor (Int64.of_int v.bits.(0)) + (Int64.logor (Int64.shift_left (Int64.of_int v.bits.(1)) 30) + (Int64.shift_left (Int64.of_int (v.bits.(2) land 15)) 60)) + | 64 -> + Int64.logor (Int64.of_int v.bits.(0)) + (Int64.shift_left (Int64.of_int (v.bits.(1) land 3)) 62) + | _ -> assert false (* [Nativeint] *) let select_of f32 f64 = match Sys.word_size with diff --git a/common/hashcons.ml b/common/hashcons.ml index 1d44e929..c16e9e2c 100644 --- a/common/hashcons.ml +++ b/common/hashcons.ml @@ -21,20 +21,20 @@ standard library, which is copyright 1996 INRIA.) *) module type HashedType = - sig - type t - val equal : t -> t -> bool - val hash : t -> int - val tag : int -> t -> t - end +sig + type t + val equal : t -> t -> bool + val hash : t -> int + val tag : int -> t -> t +end module type S = - sig - type t - val hashcons : t -> t - val iter : (t -> unit) -> unit - val stats : unit -> int * int * int * int * int * int - end +sig + type t + val hashcons : t -> t + val iter : (t -> unit) -> unit + val stats : unit -> int * int * int * int * int * int +end module Make(H : HashedType) : (S with type t = H.t) = struct @@ -69,28 +69,28 @@ type 'a hash_consed = { node : 'a } module type HashedType_consed = - sig - type t - val equal : t -> t -> bool - val hash : t -> int - end +sig + type t + val equal : t -> t -> bool + val hash : t -> int +end module type S_consed = - sig - type key - val hashcons : key -> key hash_consed - val iter : (key hash_consed -> unit) -> unit - val stats : unit -> int * int * int * int * int * int - end +sig + type key + val hashcons : key -> key hash_consed + val iter : (key hash_consed -> unit) -> unit + val stats : unit -> int * int * int * int * int * int +end module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) = struct module M = Make(struct - type t = H.t hash_consed - let hash x = H.hash x.node - let equal x y = H.equal x.node y.node - let tag i x = {x with tag = i} - end) + type t = H.t hash_consed + let hash x = H.hash x.node + let equal x y = H.equal x.node y.node + let tag i x = {x with tag = i} + end) include M type key = H.t let hashcons x = M.hashcons {tag = -1; node = x} diff --git a/common/hashcons.mli b/common/hashcons.mli index f000e407..485b4086 100644 --- a/common/hashcons.mli +++ b/common/hashcons.mli @@ -33,33 +33,33 @@ more referenced from anywhere else can be erased by the GC. *) module type HashedType = - sig - type t - val equal : t -> t -> bool - val hash : t -> int - val tag : int -> t -> t - end +sig + type t + val equal : t -> t -> bool + val hash : t -> int + val tag : int -> t -> t +end module type S = - sig - type t +sig + type t - val hashcons : t -> t - (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns - any existing value in the table equal to [n], if any; - otherwise, creates a new value with function [f], stores it - in the table and returns it. Function [f] is passed - the node [n] as first argument and the unique id as second argument. - *) + val hashcons : t -> t + (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns + any existing value in the table equal to [n], if any; + otherwise, creates a new value with function [f], stores it + in the table and returns it. Function [f] is passed + the node [n] as first argument and the unique id as second argument. + *) - val iter : (t -> unit) -> unit - (** [iter f] iterates [f] over all elements of the table . *) - val stats : unit -> int * int * int * int * int * int - (** Return statistics on the table. The numbers are, in order: - table length, number of entries, sum of bucket lengths, - smallest bucket length, median bucket length, biggest - bucket length. *) - end + val iter : (t -> unit) -> unit + (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int + (** Return statistics on the table. The numbers are, in order: + table length, number of entries, sum of bucket lengths, + smallest bucket length, median bucket length, biggest + bucket length. *) +end module Make(H : HashedType) : (S with type t = H.t) @@ -79,31 +79,31 @@ type 'a hash_consed = private { node : 'a } module type HashedType_consed = - sig - type t - val equal : t -> t -> bool - val hash : t -> int - end +sig + type t + val equal : t -> t -> bool + val hash : t -> int +end module type S_consed = - sig - type key +sig + type key - val hashcons : key -> key hash_consed - (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns - any existing value in the table equal to [n], if any; - otherwise, creates a new value with function [f], stores it - in the table and returns it. Function [f] is passed - the node [n] as first argument and the unique id as second argument. - *) + val hashcons : key -> key hash_consed + (** [hashcons n f] hash-cons the value [n] using function [f] i.e. returns + any existing value in the table equal to [n], if any; + otherwise, creates a new value with function [f], stores it + in the table and returns it. Function [f] is passed + the node [n] as first argument and the unique id as second argument. + *) - val iter : (key hash_consed -> unit) -> unit - (** [iter f] iterates [f] over all elements of the table . *) - val stats : unit -> int * int * int * int * int * int - (** Return statistics on the table. The numbers are, in order: - table length, number of entries, sum of bucket lengths, - smallest bucket length, median bucket length, biggest - bucket length. *) - end + val iter : (key hash_consed -> unit) -> unit + (** [iter f] iterates [f] over all elements of the table . *) + val stats : unit -> int * int * int * int * int * int + (** Return statistics on the table. The numbers are, in order: + table length, number of entries, sum of bucket lengths, + smallest bucket length, median bucket length, biggest + bucket length. *) +end module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) diff --git a/common/heap.ml b/common/heap.ml index 8b0467e5..e0c7335f 100644 --- a/common/heap.ml +++ b/common/heap.ml @@ -39,16 +39,16 @@ module Make ( X : OrderType ) = struct 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) - + | _ , 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 = List.fold_left (fun h x -> fusion (Node(x, Empty, Empty)) h ) h l diff --git a/common/hstring.ml b/common/hstring.ml index 9af5b310..4a0004bf 100644 --- a/common/hstring.ml +++ b/common/hstring.ml @@ -15,8 +15,8 @@ open Hashcons module S = Hashcons.Make_consed(struct include String - let hash = Hashtbl.hash - let equal = (=) end) + let hash = Hashtbl.hash + let equal = (=) end) module HS = struct @@ -53,13 +53,13 @@ module HS = struct let rec compare_list l1 l2 = match l1, l2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::r1, y::r2 -> - let c = compare x y in - if c <> 0 then c - else compare_list r1 r2 + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | x::r1, y::r2 -> + let c = compare x y in + if c <> 0 then c + else compare_list r1 r2 let rec list_mem_couple c = function | [] -> false diff --git a/sat/explanation.ml b/sat/explanation.ml index 89e13f2c..c3a552c1 100644 --- a/sat/explanation.ml +++ b/sat/explanation.ml @@ -18,55 +18,55 @@ module type S = Explanation_intf.S module Make(Stypes : Solver_types.S) = struct - type atom = Stypes.atom + type atom = Stypes.atom - type exp = Atom of atom | Fresh of int + type exp = Atom of atom | Fresh of int - module S = Set.Make(struct - type t = exp - let compare a b = match a,b with + module S = Set.Make(struct + type t = exp + let compare a b = match a,b with | Atom _, Fresh _ -> -1 - | Fresh _, Atom _ -> 1 - | Fresh i1, Fresh i2 -> i1 - i2 - | Atom a, Atom b -> a.aid - b.aid + | Fresh _, Atom _ -> 1 + | Fresh i1, Fresh i2 -> i1 - i2 + | Atom a, Atom b -> a.aid - b.aid end) - type t = S.t + type t = S.t - let singleton e = S.singleton (Atom e) + let singleton e = S.singleton (Atom e) - let empty = S.empty + let empty = S.empty - let union s1 s2 = S.union s1 s2 + let union s1 s2 = S.union s1 s2 - let iter_atoms f s = - S.iter (fun e -> match e with + let iter_atoms f s = + S.iter (fun e -> match e with | Fresh _ -> () | Atom a -> f a) s - let fold_atoms f s acc = - S.fold (fun e acc -> match e with + let fold_atoms f s acc = + S.fold (fun e acc -> match e with | Fresh _ -> acc | Atom a -> f a acc) s acc - let merge e1 e2 = e1 + let merge e1 e2 = e1 - let fresh_exp = - let r = ref (-1) in - fun () -> incr r; !r + let fresh_exp = + let r = ref (-1) in + fun () -> incr r; !r - let remove_fresh i s = - let fi = Fresh i in - if S.mem fi s then Some (S.remove fi s) - else None + let remove_fresh i s = + let fi = Fresh i in + if S.mem fi s then Some (S.remove fi s) + else None - let add_fresh i = S.add (Fresh i) + let add_fresh i = S.add (Fresh i) - let print fmt ex = - fprintf fmt "{"; - S.iter (function - | Atom a -> fprintf fmt "%a, " Stypes.pp_atom a - | Fresh i -> fprintf fmt "Fresh%d " i) ex; - fprintf fmt "}" + let print fmt ex = + fprintf fmt "{"; + S.iter (function + | Atom a -> fprintf fmt "%a, " Stypes.pp_atom a + | Fresh i -> fprintf fmt "Fresh%d " i) ex; + fprintf fmt "}" end diff --git a/sat/explanation_intf.ml b/sat/explanation_intf.ml index 1e3e5fc0..995322e7 100644 --- a/sat/explanation_intf.ml +++ b/sat/explanation_intf.ml @@ -14,22 +14,22 @@ module type S = sig - type t - type exp - type atom + type t + type exp + type atom - val empty : t - val singleton : atom -> t + val empty : t + val singleton : atom -> t - val union : t -> t -> t - val merge : t -> t -> t + val union : t -> t -> t + val merge : t -> t -> t - val iter_atoms : (atom -> unit) -> t -> unit - val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a + val iter_atoms : (atom -> unit) -> t -> unit + val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a - val fresh_exp : unit -> int - val add_fresh : int -> t -> t - val remove_fresh : int -> t -> t option + val fresh_exp : unit -> int + val add_fresh : int -> t -> t + val remove_fresh : int -> t -> t option - val print : Format.formatter -> t -> unit + val print : Format.formatter -> t -> unit end diff --git a/sat/solver.ml b/sat/solver.ml index d5ef01ea..aa184bab 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -13,428 +13,428 @@ open Format module Make (F : Formula_intf.S) - (St : Solver_types.S with type formula = F.t) - (Ex : Explanation.S with type atom = St.atom) - (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct + (St : Solver_types.S with type formula = F.t) + (Ex : Explanation.S with type atom = St.atom) + (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) = struct - open St + open St - exception Sat - exception Unsat of clause list - exception Restart - exception Conflict of clause + exception Sat + exception Unsat of clause list + exception Restart + exception Conflict of clause - type env = { - (* si true_, les contraintes sont deja fausses *) - mutable is_unsat : bool; - mutable unsat_core : clause list; - (* 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. - C'est un index vers le trail *) - mutable qhead : int; - (* Nombre des assignements top-level depuis la derniere - execution de 'simplify()' *) - mutable simpDB_assigns : int; - (* Nombre restant de propagations a faire avant la prochaine - execution de 'simplify()' *) - mutable simpDB_props : int; - (* Un tas ordone en fonction de l'activite des variables *) - mutable order : Iheap.t; - (* estimation de progressions, mis a jour par 'search()' *) - mutable progress_estimate : float; - (* *) - remove_satisfied : bool; - (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *) - var_decay : float; - (* inverse du facteur d'activite des clauses, vaut 1/0.95 par defaut *) - clause_decay : float; - (* la limite de restart initiale, vaut 100 par defaut *) - mutable restart_first : int; - (* facteur de multiplication de restart limite, vaut 1.5 par defaut*) - restart_inc : float; - (* 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, - vaut 1.1 par defaut *) - learntsize_inc : float; - (* controler la minimisation des clauses conflit, vaut true par defaut *) - expensive_ccmin : bool; - (* controle la polarite a choisir lors de la decision *) - polarity_mode : bool; + type env = { + (* si true_, les contraintes sont deja fausses *) + mutable is_unsat : bool; + mutable unsat_core : clause list; + (* 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. + C'est un index vers le trail *) + mutable qhead : int; + (* Nombre des assignements top-level depuis la derniere + execution de 'simplify()' *) + mutable simpDB_assigns : int; + (* Nombre restant de propagations a faire avant la prochaine + execution de 'simplify()' *) + mutable simpDB_props : int; + (* Un tas ordone en fonction de l'activite des variables *) + mutable order : Iheap.t; + (* estimation de progressions, mis a jour par 'search()' *) + mutable progress_estimate : float; + (* *) + remove_satisfied : bool; + (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *) + var_decay : float; + (* inverse du facteur d'activite des clauses, vaut 1/0.95 par defaut *) + clause_decay : float; + (* la limite de restart initiale, vaut 100 par defaut *) + mutable restart_first : int; + (* facteur de multiplication de restart limite, vaut 1.5 par defaut*) + restart_inc : float; + (* 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, + vaut 1.1 par defaut *) + learntsize_inc : float; + (* controler la minimisation des clauses conflit, vaut true par defaut *) + expensive_ccmin : bool; + (* controle la polarite a choisir lors de la decision *) + polarity_mode : bool; - mutable starts : int; - mutable decisions : int; - mutable propagations : int; - mutable conflicts : int; - mutable clauses_literals : int; - mutable learnts_literals : int; - mutable max_literals : int; - mutable tot_literals : int; - 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; - } + mutable starts : int; + mutable decisions : int; + mutable propagations : int; + mutable conflicts : int; + mutable clauses_literals : int; + mutable learnts_literals : int; + mutable max_literals : int; + mutable tot_literals : int; + 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; + } - type state = { - env : env; - st_cpt_mk_var: int; - st_ma : varmap; - } + type state = { + env : env; + st_cpt_mk_var: int; + st_ma : varmap; + } - let env = { - 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; - order = Iheap.init 0; (* sera mis a jour dans solve *) - progress_estimate = 0.; - remove_satisfied = true; - var_decay = 1. /. 0.95; - clause_decay = 1. /. 0.999; - 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; - propagations = 0; - conflicts = 0; - clauses_literals = 0; - learnts_literals = 0; - max_literals = 0; - tot_literals = 0; - nb_init_vars = 0; - nb_init_clauses = 0; - model = Vec.make 0 dummy_var; - tenv = Th.empty(); - tenv_queue = Vec.make 100 (Th.empty()); - tatoms_queue = Queue.create (); - } + let env = { + 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; + order = Iheap.init 0; (* sera mis a jour dans solve *) + progress_estimate = 0.; + remove_satisfied = true; + var_decay = 1. /. 0.95; + clause_decay = 1. /. 0.999; + 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; + propagations = 0; + conflicts = 0; + clauses_literals = 0; + learnts_literals = 0; + max_literals = 0; + tot_literals = 0; + nb_init_vars = 0; + nb_init_clauses = 0; + model = Vec.make 0 dummy_var; + tenv = Th.empty(); + tenv_queue = Vec.make 100 (Th.empty()); + tatoms_queue = Queue.create (); + } - let f_weight i j = - (Vec.get env.vars j).weight < (Vec.get env.vars i).weight + 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 f_filter i = + (Vec.get env.vars i).level < 0 - let insert_var_order v = - Iheap.insert f_weight env.order v.vid + 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 var_decay_activity () = + env.var_inc <- env.var_inc *. env.var_decay - let clause_decay_activity () = - env.clause_inc <- env.clause_inc *. env.clause_decay + let clause_decay_activity () = + env.clause_inc <- env.clause_inc *. env.clause_decay - 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 - (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 - done; - env.var_inc <- env.var_inc *. 1e-100; - end; - if Iheap.in_heap env.order v.vid then - Iheap.decrease f_weight env.order v.vid + 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 + (Vec.get env.vars i).weight <- (Vec.get env.vars i).weight *. 1e-100 + done; + env.var_inc <- env.var_inc *. 1e-100; + end; + if Iheap.in_heap env.order v.vid then + Iheap.decrease f_weight env.order v.vid - 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 - (Vec.get env.learnts i).activity <- - (Vec.get env.learnts i).activity *. 1e-20; - done; - env.clause_inc <- env.clause_inc *. 1e-20 - end + 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 + (Vec.get env.learnts i).activity <- + (Vec.get env.learnts i).activity *. 1e-20; + done; + env.clause_inc <- env.clause_inc *. 1e-20 + end - let decision_level () = Vec.size env.trail_lim + let decision_level () = Vec.size env.trail_lim - let nb_assigns () = Vec.size env.trail - let nb_clauses () = Vec.size env.clauses - let nb_learnts () = Vec.size env.learnts - let nb_vars () = Vec.size env.vars + let nb_assigns () = Vec.size env.trail + 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() = - Vec.push env.trail_lim (Vec.size env.trail); - Vec.push env.tenv_queue env.tenv (* save the current tenv *) + 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 = - Vec.push (Vec.get c.atoms 0).neg.watched c; - Vec.push (Vec.get c.atoms 1).neg.watched c; - 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 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 + 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 = - c.removed <- true; + 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 - env.learnts_literals <- env.learnts_literals - Vec.size c.atoms - else - env.clauses_literals <- env.clauses_literals - Vec.size c.atoms + 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 remove_clause c = detach_clause 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 - done; - false - with Exit -> true - - (* annule tout jusqu'a lvl *exclu* *) - 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 - let a = Vec.get env.trail c in - a.is_true <- false; - a.neg.is_true <- false; - a.var.level <- -1; - a.var.reason <- None; - a.var.vpremise <- []; - insert_var_order a.var - done; - Queue.clear env.tatoms_queue; - env.tenv <- Vec.get env.tenv_queue lvl; (* recover the right tenv *) - Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); - Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); - Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) - end; - assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) - - 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 - assert (v.pa.is_true || v.na.is_true); - pick_branch_lit () - end - else v - - let enqueue a lvl reason = - 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*) - a.is_true <- true; - a.var.level <- lvl; - a.var.reason <- reason; - (*eprintf "enqueue: %a@." Debug.atom a; *) - Vec.push env.trail a - - let progress_estimate () = - let prg = ref 0. in - let nbv = to_float (nb_vars()) 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 - let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in - prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) + 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 done; - !prg /. nbv + false + with Exit -> true - let propagate_in_clause a c i watched new_sz = - let atoms = c.atoms in - let first = Vec.get atoms 0 in - if first == a.neg then begin (* le litiral false_ doit etre dans .(1) *) - Vec.set atoms 0 (Vec.get atoms 1); - Vec.set atoms 1 first - end; - 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; - incr new_sz; - end - 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 - (* Watcher Trouve: mettre a jour et sortir *) - Vec.set atoms 1 ak; - Vec.set atoms k a.neg; - Vec.push ak.neg.watched c; - raise Exit - end - done; - (* Watcher NON Trouve *) - if first.neg.is_true then begin - (* la clause est fausse *) - env.qhead <- Vec.size env.trail; - for k = i to Vec.size watched - 1 do - Vec.set watched !new_sz (Vec.get watched k); - incr new_sz; - done; - raise (Conflict c) + (* annule tout jusqu'a lvl *exclu* *) + 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 + let a = Vec.get env.trail c in + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.reason <- None; + a.var.vpremise <- []; + insert_var_order a.var + done; + Queue.clear env.tatoms_queue; + env.tenv <- Vec.get env.tenv_queue lvl; (* recover the right tenv *) + Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); + Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); + Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) + end; + assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) + + 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 + assert (v.pa.is_true || v.na.is_true); + pick_branch_lit () + end + else v + + let enqueue a lvl reason = + 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*) + a.is_true <- true; + a.var.level <- lvl; + a.var.reason <- reason; + (*eprintf "enqueue: %a@." Debug.atom a; *) + Vec.push env.trail a + + let progress_estimate () = + let prg = ref 0. in + let nbv = to_float (nb_vars()) 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 + let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in + prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) + done; + !prg /. nbv + + let propagate_in_clause a c i watched new_sz = + let atoms = c.atoms in + let first = Vec.get atoms 0 in + if first == a.neg then begin (* le litiral false_ doit etre dans .(1) *) + Vec.set atoms 0 (Vec.get atoms 1); + Vec.set atoms 1 first + end; + 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; + incr new_sz; + end + 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 + (* Watcher Trouve: mettre a jour et sortir *) + Vec.set atoms 1 ak; + Vec.set atoms k a.neg; + Vec.push ak.neg.watched c; + raise Exit end - else begin - (* la clause est unitaire *) - Vec.set watched !new_sz c; + done; + (* Watcher NON Trouve *) + if first.neg.is_true then begin + (* la clause est fausse *) + env.qhead <- Vec.size env.trail; + for k = i to Vec.size watched - 1 do + Vec.set watched !new_sz (Vec.get watched k); incr new_sz; - enqueue first (decision_level ()) (Some c) - end - with Exit -> () - - let propagate_atom a res = - let watched = a.watched in - let new_sz_w = ref 0 in - 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 - end; - let dead_part = Vec.size watched - !new_sz_w in - Vec.shrink watched dead_part + raise (Conflict c) + end + else begin + (* la clause est unitaire *) + Vec.set watched !new_sz c; + incr new_sz; + enqueue first (decision_level ()) (Some c) + end + with Exit -> () - let expensive_theory_propagate () = None - (* try *) - (* if D1.d then eprintf "expensive_theory_propagate@."; *) - (* ignore(Th.expensive_processing env.tenv); *) - (* if D1.d then eprintf "expensive_theory_propagate => None@."; *) - (* None *) - (* with Th.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 - let a = Queue.pop env.tatoms_queue in - if a.is_true then - (*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 - 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 *) - facts := (a.neg.lit, ex) :: !facts - else assert false; - done; + let propagate_atom a res = + let watched = a.watched in + let new_sz_w = ref 0 in + begin try - let full_model = nb_assigns() = env.nb_init_vars in - env.tenv <- - List.fold_left + 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 + end; + let dead_part = Vec.size watched - !new_sz_w in + Vec.shrink watched dead_part + + let expensive_theory_propagate () = None + (* try *) + (* if D1.d then eprintf "expensive_theory_propagate@."; *) + (* ignore(Th.expensive_processing env.tenv); *) + (* if D1.d then eprintf "expensive_theory_propagate => None@."; *) + (* None *) + (* with Th.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 + let a = Queue.pop env.tatoms_queue in + if a.is_true then + (*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 + 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 *) + facts := (a.neg.lit, ex) :: !facts + else assert false; + 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 !facts; - if full_model then expensive_theory_propagate () - else None - with Th.Inconsistent dep -> - (* eprintf "th inconsistent : %a @." Ex.print dep; *) - Some dep + if full_model then expensive_theory_propagate () + else None + with Th.Inconsistent dep -> + (* eprintf "th inconsistent : %a @." Ex.print dep; *) + Some dep - let propagate () = - let num_props = ref 0 in - let res = ref None in - (*assert (Queue.is_empty env.tqueue);*) - while env.qhead < Vec.size env.trail do - let a = Vec.get env.trail env.qhead in - env.qhead <- env.qhead + 1; - incr num_props; - propagate_atom a res; - Queue.push a env.tatoms_queue; - done; - env.propagations <- env.propagations + !num_props; - env.simpDB_props <- env.simpDB_props - !num_props; - !res + let propagate () = + let num_props = ref 0 in + let res = ref None in + (*assert (Queue.is_empty env.tqueue);*) + while env.qhead < Vec.size env.trail do + let a = Vec.get env.trail env.qhead in + env.qhead <- env.qhead + 1; + incr num_props; + propagate_atom a res; + Queue.push a env.tatoms_queue; + done; + env.propagations <- env.propagations + !num_props; + env.simpDB_props <- env.simpDB_props - !num_props; + !res - let analyze c_clause = - let pathC = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = ref [] in - let c = ref c_clause in - let tr_ind = ref (Vec.size env.trail - 1) in - let size = ref 1 in - let history = ref [] in - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.seen <- true; - seen := q :: !seen; - if q.var.level >= decision_level () then incr pathC - else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level - end + let analyze c_clause = + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= decision_level () then incr pathC + else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level 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, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl + end done; - List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size - 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 - if sz1 > 2 && (sz2 = 2 || c < 0) then -1 - else 1 + (* 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, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, None -> assert false + | n, Some cl -> c := cl + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, !size - let locked c = false(* + 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 + if sz1 > 2 && (sz2 = 2 || c < 0) then -1 + else 1 + + let locked c = false(* try for i = 0 to Vec.size env.vars - 1 do match (Vec.get env.vars i).reason with @@ -444,7 +444,7 @@ module Make (F : Formula_intf.S) false with Exit -> true*) - let reduce_db () = () + let reduce_db () = () (* let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in Vec.sort env.learnts f_sort_db; @@ -468,486 +468,486 @@ module Make (F : Formula_intf.S) Vec.shrink env.learnts (lim2 - !j) *) - let remove_satisfied vec = - let j = ref 0 in - let k = Vec.size vec - 1 in - for i = 0 to k do - let c = Vec.get vec i in - if satisfied c then remove_clause c - else begin - Vec.set vec !j (Vec.get vec i); - incr j - end - done; - Vec.shrink vec (k + 1 - !j) + let remove_satisfied vec = + let j = ref 0 in + let k = Vec.size vec - 1 in + for i = 0 to k do + let c = Vec.get vec i in + if satisfied c then remove_clause c + else begin + Vec.set vec !j (Vec.get vec i); + incr j + end + done; + 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) - let report_b_unsat ({atoms=atoms} as confl) = - let l = ref [confl] in - for i = 0 to Vec.size atoms - 1 do - let v = (Vec.get atoms i).var in - l := List.rev_append v.vpremise !l; - match v.reason with None -> () | Some c -> l := c :: !l - done; - if false then begin - eprintf "@.>>UNSAT Deduction made from:@."; - List.iter - (fun hc -> - eprintf " %a@." pp_clause hc - )!l; - end; - let uc = HUC.create 17 in - 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 - v.seen <- true; - roots v.vpremise; - match v.reason with None -> () | Some r -> roots [r]; - end - done; - match c.cpremise with - | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r - | prems -> roots prems; roots r - in roots !l; - let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in - if false then begin - eprintf "@.>>UNSAT_CORE:@."; - List.iter - (fun hc -> - eprintf " %a@." pp_clause hc - )unsat_core; - end; - env.is_unsat <- true; - env.unsat_core <- unsat_core; - raise (Unsat unsat_core) - - - let report_t_unsat dep = - let l = - Ex.fold_atoms - (fun {var=v} l -> - let l = List.rev_append v.vpremise l in - match v.reason with None -> l | Some c -> c :: l - ) dep [] - in - if false then begin - eprintf "@.>>T-UNSAT Deduction made from:@."; - List.iter - (fun hc -> - eprintf " %a@." pp_clause hc - )l; - end; - let uc = HUC.create 17 in - 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 - v.seen <- true; - roots v.vpremise; - match v.reason with None -> () | Some r -> roots [r]; - end - done; - match c.cpremise with - | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r - | prems -> roots prems; roots r - in roots l; - let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in - if false then begin - eprintf "@.>>T-UNSAT_CORE:@."; - List.iter - (fun hc -> - eprintf " %a@." pp_clause hc - ) unsat_core; - end; - env.is_unsat <- true; - env.unsat_core <- unsat_core; - raise (Unsat unsat_core) - - let simplify () = - assert (decision_level () = 0); - if env.is_unsat then raise (Unsat env.unsat_core); - begin - match propagate () with - | Some confl -> report_b_unsat confl - | None -> - match theory_propagate () with - Some dep -> report_t_unsat dep - | None -> () - end; - if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin - if Vec.size env.learnts > 0 then remove_satisfied env.learnts; - if env.remove_satisfied then remove_satisfied env.clauses; - (*Iheap.filter env.order f_filter f_weight;*) - env.simpDB_assigns <- nb_assigns (); - env.simpDB_props <- env.clauses_literals + env.learnts_literals; - end - - let record_learnt_clause blevel learnt history size = - begin match learnt with - | [] -> assert false - | [fuip] -> - assert (blevel = 0); - fuip.var.vpremise <- history; - enqueue fuip 0 None - | fuip :: _ -> - let name = fresh_lname () in - let lclause = make_clause name learnt size true history in - Vec.push env.learnts lclause; - attach_clause lclause; - clause_bump_activity lclause; - enqueue fuip blevel (Some lclause) - end; - var_decay_activity (); - clause_decay_activity() - - let check_inconsistence_of dep = - try - let env = ref (Th.empty()) in (); - Ex.iter_atoms - (fun atom -> - let t = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in - env := t) - dep; - (* ignore (Th.expensive_processing !env); *) - assert false - with Th.Inconsistent _ -> () - - 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 - | 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 - ) dep ([], 0, 0, []) - in - if atoms = [] then begin - (* check_inconsistence_of dep; *) - report_t_unsat dep - (* une conjonction de faits unitaires etaient deja unsat *) - end; - let name = fresh_dname() in - let c_clause = make_clause name atoms sz false c_hist in - (* eprintf "c_clause: %a@." Debug.clause c_clause; *) - c_clause.removed <- true; - - let pathC = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = ref [] in - let c = ref c_clause in - let tr_ind = ref (Vec.size env.trail - 1) in - let size = ref 1 in - let history = ref [] in - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.seen <- true; - seen := q :: !seen; - if q.var.level >= max_lvl then incr pathC - else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level - end + let report_b_unsat ({atoms=atoms} as confl) = + let l = ref [confl] in + for i = 0 to Vec.size atoms - 1 do + let v = (Vec.get atoms i).var in + l := List.rev_append v.vpremise !l; + match v.reason with None -> () | Some c -> l := c :: !l + done; + if false then begin + eprintf "@.>>UNSAT Deduction made from:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + )!l; + end; + let uc = HUC.create 17 in + 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 + v.seen <- true; + roots v.vpremise; + match v.reason with None -> () | Some r -> roots [r]; 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, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl - done; - List.iter (fun q -> q.var.seen <- false) !seen; - !blevel, !learnt, !history, !size - - - - let add_boolean_conflict confl = - env.conflicts <- env.conflicts + 1; - if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *) - let blevel, learnt, history, size = analyze confl in - cancel_until blevel; - record_learnt_clause blevel learnt history size - - let search n_of_conflicts n_of_learnts = - let conflictC = ref 0 in - env.starts <- env.starts + 1; - while (true) do - match propagate () with - | Some confl -> (* Conflict *) - incr conflictC; - add_boolean_conflict confl - - | None -> (* No Conflict *) - match theory_propagate () with - | 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 -> - if nb_assigns () = env.nb_init_vars then raise Sat; - if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then - begin - env.progress_estimate <- progress_estimate(); - cancel_until 0; - raise Restart - end; - if decision_level() = 0 then simplify (); - - if n_of_learnts >= 0 && - Vec.size env.learnts - nb_assigns() >= n_of_learnts then - reduce_db(); - - env.decisions <- env.decisions + 1; - - new_decision_level(); - let next = pick_branch_lit () in - let current_level = decision_level () in - assert (next.level < 0); - (* eprintf "decide: %a@." Debug.atom next.pa; *) - enqueue next.pa current_level None - done - - let check_clause c = - let b = ref false in - let atoms = c.atoms in - for i = 0 to Vec.size atoms - 1 do - let a = Vec.get atoms i in - b := !b || a.is_true - done; - assert (!b) - - let check_vec vec = - for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done - - let check_model () = - check_vec env.clauses; - check_vec env.learnts - - - 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 - try - while true do - (try search (to_int !n_of_conflicts) (to_int !n_of_learnts); - with Restart -> ()); - n_of_conflicts := !n_of_conflicts *. env.restart_inc; - n_of_learnts := !n_of_learnts *. env.learntsize_inc; - done; - with - | Sat -> - (*check_model ();*) - raise Sat - | (Unsat cl) as e -> - (* check_unsat_core cl; *) - raise e - - 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 - 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 - (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 - in - partition_aux [] [] [] init atoms - - - let add_clause ~cnumber atoms = - if env.is_unsat then raise (Unsat env.unsat_core); - let init_name = string_of_int cnumber in - let init0 = make_clause init_name atoms (List.length atoms) false [] in - try - let atoms, init = - if decision_level () = 0 then - let atoms, init = List.fold_left - (fun (atoms, init) a -> - if a.is_true then raise Trivial; - if a.neg.is_true then - atoms, (List.rev_append (a.var.vpremise) init) - else a::atoms, init - ) ([], [init0]) atoms in - List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init - else partition atoms [init0] - in - let size = List.length atoms in - match atoms with - | [] -> - report_b_unsat init0; - - | 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 - None -> () | Some confl -> report_b_unsat confl - with Trivial -> () - - 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; + match c.cpremise with + | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r + | prems -> roots prems; roots r + in roots !l; + let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + if false then begin + eprintf "@.>>UNSAT_CORE:@."; List.iter - (List.iter - (fun a -> - Vec.set env.vars a.var.vid a.var; - insert_var_order a.var - ) - ) cnf; - env.nb_init_vars <- nbv; - Vec.grow_to_by_double env.model nbv; - Vec.grow_to_by_double env.clauses nbc; - Vec.grow_to_by_double env.learnts nbc; - env.nb_init_clauses <- nbc; - add_clauses cnf ~cnumber + (fun hc -> + eprintf " %a@." pp_clause hc + )unsat_core; + end; + env.is_unsat <- true; + env.unsat_core <- unsat_core; + raise (Unsat unsat_core) - let assume cnf ~cnumber = - let cnf = List.map (List.map St.add_atom) cnf in - init_solver cnf ~cnumber + let report_t_unsat dep = + let l = + Ex.fold_atoms + (fun {var=v} l -> + let l = List.rev_append v.vpremise l in + match v.reason with None -> l | Some c -> c :: l + ) dep [] + in + if false then begin + eprintf "@.>>T-UNSAT Deduction made from:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + )l; + end; + let uc = HUC.create 17 in + 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 + v.seen <- true; + roots v.vpremise; + match v.reason with None -> () | Some r -> roots [r]; + end + done; + match c.cpremise with + | [] -> if not (HUC.mem uc c) then HUC.add uc c (); roots r + | prems -> roots prems; roots r + in roots l; + let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + if false then begin + eprintf "@.>>T-UNSAT_CORE:@."; + List.iter + (fun hc -> + eprintf " %a@." pp_clause hc + ) unsat_core; + end; + env.is_unsat <- true; + env.unsat_core <- unsat_core; + raise (Unsat unsat_core) - 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.clause_inc <- 1.; - env.var_inc <- 1.; - env.vars <- Vec.make 0 dummy_var; - env.qhead <- 0; - env.simpDB_assigns <- -1; - env.simpDB_props <- 0; - env.order <- Iheap.init 0; (* sera mis a jour dans solve *) - env.progress_estimate <- 0.; - env.restart_first <- 100; - env.starts <- 0; - env.decisions <- 0; - env.propagations <- 0; - env.conflicts <- 0; - env.clauses_literals <- 0; - env.learnts_literals <- 0; - env.max_literals <- 0; - env.tot_literals <- 0; - env.nb_init_vars <- 0; - env.nb_init_clauses <- 0; - env.tenv <- empty_theory; - env.model <- Vec.make 0 dummy_var; - env.trail <- Vec.make 601 dummy_atom; - env.trail_lim <- Vec.make 601 (-105); - env.tenv_queue <- Vec.make 100 (empty_theory); - env.tatoms_queue <- Queue.create (); - St.clear () + let simplify () = + assert (decision_level () = 0); + if env.is_unsat then raise (Unsat env.unsat_core); + begin + match propagate () with + | Some confl -> report_b_unsat confl + | None -> + match theory_propagate () with + Some dep -> report_t_unsat dep + | None -> () + end; + if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin + if Vec.size env.learnts > 0 then remove_satisfied env.learnts; + if env.remove_satisfied then remove_satisfied env.clauses; + (*Iheap.filter env.order f_filter f_weight;*) + env.simpDB_assigns <- nb_assigns (); + env.simpDB_props <- env.clauses_literals + env.learnts_literals; + end + + let record_learnt_clause blevel learnt history size = + begin match learnt with + | [] -> assert false + | [fuip] -> + assert (blevel = 0); + fuip.var.vpremise <- history; + enqueue fuip 0 None + | fuip :: _ -> + let name = fresh_lname () in + let lclause = make_clause name learnt size true history in + Vec.push env.learnts lclause; + attach_clause lclause; + clause_bump_activity lclause; + enqueue fuip blevel (Some lclause) + end; + var_decay_activity (); + clause_decay_activity() + + let check_inconsistence_of dep = + try + let env = ref (Th.empty()) in (); + Ex.iter_atoms + (fun atom -> + let t = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in + env := t) + dep; + (* ignore (Th.expensive_processing !env); *) + assert false + with Th.Inconsistent _ -> () + + 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 + | 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 + ) dep ([], 0, 0, []) + in + if atoms = [] then begin + (* check_inconsistence_of dep; *) + report_t_unsat dep + (* une conjonction de faits unitaires etaient deja unsat *) + end; + let name = fresh_dname() in + let c_clause = make_clause name atoms sz false c_hist in + (* eprintf "c_clause: %a@." Debug.clause c_clause; *) + c_clause.removed <- true; + + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= max_lvl then incr pathC + else begin + 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, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, None -> assert false + | n, Some cl -> c := cl + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, !size - let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0 - let save () = - let sv = - { env = env; - st_cpt_mk_var = !St.cpt_mk_var; - st_ma = !St.ma } + let add_boolean_conflict confl = + env.conflicts <- env.conflicts + 1; + if decision_level() = 0 then report_b_unsat confl; (* Top-level conflict *) + let blevel, learnt, history, size = analyze confl in + cancel_until blevel; + record_learnt_clause blevel learnt history size + + let search n_of_conflicts n_of_learnts = + let conflictC = ref 0 in + env.starts <- env.starts + 1; + while (true) do + match propagate () with + | Some confl -> (* Conflict *) + incr conflictC; + add_boolean_conflict confl + + | None -> (* No Conflict *) + match theory_propagate () with + | 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 -> + if nb_assigns () = env.nb_init_vars then raise Sat; + if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then + begin + env.progress_estimate <- progress_estimate(); + cancel_until 0; + raise Restart + end; + if decision_level() = 0 then simplify (); + + if n_of_learnts >= 0 && + Vec.size env.learnts - nb_assigns() >= n_of_learnts then + reduce_db(); + + env.decisions <- env.decisions + 1; + + new_decision_level(); + let next = pick_branch_lit () in + let current_level = decision_level () in + assert (next.level < 0); + (* eprintf "decide: %a@." Debug.atom next.pa; *) + enqueue next.pa current_level None + done + + let check_clause c = + let b = ref false in + let atoms = c.atoms in + for i = 0 to Vec.size atoms - 1 do + let a = Vec.get atoms i in + b := !b || a.is_true + done; + assert (!b) + + let check_vec vec = + for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done + + let check_model () = + check_vec env.clauses; + check_vec env.learnts + + + 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 + try + while true do + (try search (to_int !n_of_conflicts) (to_int !n_of_learnts); + with Restart -> ()); + n_of_conflicts := !n_of_conflicts *. env.restart_inc; + n_of_learnts := !n_of_learnts *. env.learntsize_inc; + done; + with + | Sat -> + (*check_model ();*) + raise Sat + | (Unsat cl) as e -> + (* check_unsat_core cl; *) + raise e + + 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 + 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 + (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 + in + partition_aux [] [] [] init atoms + + + let add_clause ~cnumber atoms = + if env.is_unsat then raise (Unsat env.unsat_core); + let init_name = string_of_int cnumber in + let init0 = make_clause init_name atoms (List.length atoms) false [] in + try + let atoms, init = + if decision_level () = 0 then + let atoms, init = List.fold_left + (fun (atoms, init) a -> + if a.is_true then raise Trivial; + if a.neg.is_true then + atoms, (List.rev_append (a.var.vpremise) init) + else a::atoms, init + ) ([], [init0]) atoms in + List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init + else partition atoms [init0] in - copy sv + let size = List.length atoms in + match atoms with + | [] -> + report_b_unsat init0; - let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = - env.is_unsat <- s_env.is_unsat; - env.unsat_core <- s_env.unsat_core; - env.clauses <- s_env.clauses; - env.learnts <- s_env.learnts; - env.clause_inc <- s_env.clause_inc; - env.var_inc <- s_env.var_inc; - env.vars <- s_env.vars; - env.qhead <- s_env.qhead; - env.simpDB_assigns <- s_env.simpDB_assigns; - env.simpDB_props <- s_env.simpDB_props; - env.order <- s_env.order; - env.progress_estimate <- s_env.progress_estimate; - env.restart_first <- s_env.restart_first; - env.starts <- s_env.starts; - env.decisions <- s_env.decisions; - env.propagations <- s_env.propagations; - env.conflicts <- s_env.conflicts; - env.clauses_literals <- s_env.clauses_literals; - env.learnts_literals <- s_env.learnts_literals; - env.max_literals <- s_env.max_literals; - env.tot_literals <- s_env.tot_literals; - env.nb_init_vars <- s_env.nb_init_vars; - env.nb_init_clauses <- s_env.nb_init_clauses; - env.tenv <- s_env.tenv; - env.model <- s_env.model; - env.trail <- s_env.trail; - env.trail_lim <- s_env.trail_lim; - env.tenv_queue <- s_env.tenv_queue; - env.tatoms_queue <- s_env.tatoms_queue; - env.learntsize_factor <- s_env.learntsize_factor; - St.cpt_mk_var := st_cpt_mk_var; - St.ma := st_ma + | a::_::_ -> + let name = fresh_name () in + let clause = make_clause name atoms size false init in + attach_clause clause; + Vec.push env.clauses clause; - let eval lit = - let var, negated = make_var lit in - let truth = var.pa.is_true in - if negated then not truth else truth + 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 + None -> () | Some confl -> report_b_unsat confl + with Trivial -> () + + 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 + (fun a -> + Vec.set env.vars a.var.vid a.var; + insert_var_order a.var + ) + ) cnf; + env.nb_init_vars <- nbv; + Vec.grow_to_by_double env.model nbv; + Vec.grow_to_by_double env.clauses nbc; + Vec.grow_to_by_double env.learnts nbc; + env.nb_init_clauses <- nbc; + add_clauses cnf ~cnumber + + + let assume cnf ~cnumber = + let cnf = List.map (List.map St.add_atom) cnf in + init_solver cnf ~cnumber + + 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.clause_inc <- 1.; + env.var_inc <- 1.; + env.vars <- Vec.make 0 dummy_var; + env.qhead <- 0; + env.simpDB_assigns <- -1; + env.simpDB_props <- 0; + env.order <- Iheap.init 0; (* sera mis a jour dans solve *) + env.progress_estimate <- 0.; + env.restart_first <- 100; + env.starts <- 0; + env.decisions <- 0; + env.propagations <- 0; + env.conflicts <- 0; + env.clauses_literals <- 0; + env.learnts_literals <- 0; + env.max_literals <- 0; + env.tot_literals <- 0; + env.nb_init_vars <- 0; + env.nb_init_clauses <- 0; + env.tenv <- empty_theory; + env.model <- Vec.make 0 dummy_var; + env.trail <- Vec.make 601 dummy_atom; + env.trail_lim <- Vec.make 601 (-105); + env.tenv_queue <- Vec.make 100 (empty_theory); + env.tatoms_queue <- Queue.create (); + St.clear () + + + let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0 + + let save () = + let sv = + { env = env; + st_cpt_mk_var = !St.cpt_mk_var; + st_ma = !St.ma } + in + copy sv + + let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = + env.is_unsat <- s_env.is_unsat; + env.unsat_core <- s_env.unsat_core; + env.clauses <- s_env.clauses; + env.learnts <- s_env.learnts; + env.clause_inc <- s_env.clause_inc; + env.var_inc <- s_env.var_inc; + env.vars <- s_env.vars; + env.qhead <- s_env.qhead; + env.simpDB_assigns <- s_env.simpDB_assigns; + env.simpDB_props <- s_env.simpDB_props; + env.order <- s_env.order; + env.progress_estimate <- s_env.progress_estimate; + env.restart_first <- s_env.restart_first; + env.starts <- s_env.starts; + env.decisions <- s_env.decisions; + env.propagations <- s_env.propagations; + env.conflicts <- s_env.conflicts; + env.clauses_literals <- s_env.clauses_literals; + env.learnts_literals <- s_env.learnts_literals; + env.max_literals <- s_env.max_literals; + env.tot_literals <- s_env.tot_literals; + env.nb_init_vars <- s_env.nb_init_vars; + env.nb_init_clauses <- s_env.nb_init_clauses; + env.tenv <- s_env.tenv; + env.model <- s_env.model; + env.trail <- s_env.trail; + env.trail_lim <- s_env.trail_lim; + env.tenv_queue <- s_env.tenv_queue; + env.tatoms_queue <- s_env.tatoms_queue; + env.learntsize_factor <- s_env.learntsize_factor; + St.cpt_mk_var := st_cpt_mk_var; + St.ma := st_ma + + let eval lit = + let var, negated = make_var lit in + let truth = var.pa.is_true in + if negated then not truth else truth end diff --git a/sat/solver.mli b/sat/solver.mli index 47641916..a723e81c 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -12,22 +12,22 @@ (**************************************************************************) module Make (F : Formula_intf.S) - (St : Solver_types.S with type formula = F.t) - (Ex : Explanation.S with type atom = St.atom) - (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) : sig + (St : Solver_types.S with type formula = F.t) + (Ex : Explanation.S with type atom = St.atom) + (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) : sig - exception Sat - exception Unsat of St.clause list + exception Sat + exception Unsat of St.clause list - type state + type state - val solve : unit -> unit - val assume : F.t list list -> cnumber : int -> unit - val clear : unit -> unit + val solve : unit -> unit + val assume : F.t list list -> cnumber : int -> unit + val clear : unit -> unit - val eval : F.t -> bool - val save : unit -> state - val restore : state -> unit + val eval : F.t -> bool + val save : unit -> state + val restore : state -> unit end diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 71102786..de5a1688 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -25,9 +25,9 @@ module type S = Solver_types_intf.S module Make (F : Formula_intf.S) = struct -type formula = F.t + type formula = F.t -type var = + type var = { vid : int; pa : atom; na : atom; @@ -37,7 +37,7 @@ type var = mutable reason: reason; mutable vpremise : premise} -and atom = + and atom = { var : var; lit : formula; neg : atom; @@ -45,7 +45,7 @@ and atom = mutable is_true : bool; aid : int } -and clause = + and clause = { name : string; mutable atoms : atom Vec.t ; mutable activity : float; @@ -53,141 +53,141 @@ and clause = learnt : bool; cpremise : premise } -and reason = clause option + and reason = clause option -and premise = clause list + and premise = clause list -let dummy_lit = F.dummy + let dummy_lit = F.dummy -let rec dummy_var = - { vid = -101; - pa = dummy_atom; - na = dummy_atom; - level = -1; - reason = None; - weight = -1.; - seen = false; - vpremise = [] } -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 = ""; - atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0}; - activity = -1.; - removed = false; - learnt = false; - cpremise = [] } + let rec dummy_var = + { vid = -101; + pa = dummy_atom; + na = dummy_atom; + level = -1; + reason = None; + weight = -1.; + seen = false; + vpremise = [] } + 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 = ""; + atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0}; + activity = -1.; + removed = false; + learnt = false; + cpremise = [] } -module MA = F.Map -type varmap = var MA.t + module MA = F.Map + type varmap = var MA.t -let ale = Hstring.make "<=" -let alt = Hstring.make "<" -let agt = Hstring.make ">" -let is_le n = Hstring.compare n ale = 0 -let is_lt n = Hstring.compare n alt = 0 -let is_gt n = Hstring.compare n agt = 0 + let ale = Hstring.make "<=" + let alt = Hstring.make "<" + let agt = Hstring.make ">" + let is_le n = Hstring.compare n ale = 0 + let is_lt n = Hstring.compare n alt = 0 + let is_gt n = Hstring.compare n agt = 0 -let normal_form = F.norm + let normal_form = F.norm -let cpt_mk_var = ref 0 -let ma = ref MA.empty -let make_var = - fun lit -> - let lit, negated = normal_form lit in - 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; - pa = pa; - na = na; - level = -1; - reason = None; - weight = 0.; - seen = false; - vpremise = []; - } - and pa = - { var = var; - lit = lit; - watched = Vec.make 10 dummy_clause; - neg = na; - is_true = false; - aid = cpt_fois_2 (* aid = vid*2 *) } - and na = - { var = var; - lit = F.neg lit; - watched = Vec.make 10 dummy_clause; - neg = pa; - is_true = false; - aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in - ma := MA.add lit var !ma; - incr cpt_mk_var; - var, negated + let cpt_mk_var = ref 0 + let ma = ref MA.empty + let make_var = + fun lit -> + let lit, negated = normal_form lit in + 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; + pa = pa; + na = na; + level = -1; + reason = None; + weight = 0.; + seen = false; + vpremise = []; + } + and pa = + { var = var; + lit = lit; + watched = Vec.make 10 dummy_clause; + neg = na; + is_true = false; + aid = cpt_fois_2 (* aid = vid*2 *) } + and na = + { var = var; + lit = F.neg lit; + watched = Vec.make 10 dummy_clause; + neg = pa; + is_true = false; + aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in + ma := MA.add lit var !ma; + incr cpt_mk_var; + var, negated -let made_vars_info () = !cpt_mk_var, MA.fold (fun lit var acc -> var::acc)!ma [] + 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 + let add_atom lit = + let var, negated = make_var lit in + if negated then var.na else var.pa -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; - removed = false; - learnt = is_learnt; - activity = 0.; - cpremise = 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; + removed = false; + learnt = is_learnt; + activity = 0.; + cpremise = premise} -let fresh_lname = - let cpt = ref 0 in - fun () -> incr cpt; "L" ^ (string_of_int !cpt) + let fresh_lname = + let cpt = ref 0 in + fun () -> incr cpt; "L" ^ (string_of_int !cpt) -let fresh_dname = - let cpt = ref 0 in - fun () -> incr cpt; "D" ^ (string_of_int !cpt) + let fresh_dname = + let cpt = ref 0 in + fun () -> incr cpt; "D" ^ (string_of_int !cpt) -let fresh_name = - let cpt = ref 0 in - fun () -> incr cpt; "C" ^ (string_of_int !cpt) + let fresh_name = + let cpt = ref 0 in + fun () -> incr cpt; "C" ^ (string_of_int !cpt) -module Clause = struct + 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 - let last c = Vec.last c.atoms - let get c i = Vec.get c.atoms i - let set c i v = Vec.set c.atoms i v + let size c = Vec.size c.atoms + let pop c = Vec.pop c.atoms + let shrink c i = Vec.shrink c.atoms i + let last c = Vec.last c.atoms + let get c i = Vec.get c.atoms i + let set c i v = Vec.set c.atoms i v -end + end -let to_float i = float_of_int i + let to_float i = float_of_int i -let to_int f = int_of_float f + let to_int f = int_of_float f -let clear () = - cpt_mk_var := 0; - ma := MA.empty + let clear () = + cpt_mk_var := 0; + ma := MA.empty let sign a = if a==a.var.pa then "" else "-" let level a = 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 + | 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 = if a.is_true then sprintf "[T%s]" (level a) diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index d339f1c2..80a9c0d3 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -12,68 +12,68 @@ (**************************************************************************) module type S = sig - type formula + type formula - type var = { - vid : int; - pa : atom; - na : atom; - mutable weight : float; - mutable seen : bool; - mutable level : int; - mutable reason : reason; - mutable vpremise : premise - } + type var = { + vid : int; + pa : atom; + na : atom; + mutable weight : float; + mutable seen : bool; + mutable level : int; + mutable reason : reason; + mutable vpremise : premise + } - and atom = { - var : var; - lit : formula; - neg : atom; - mutable watched : clause Vec.t; - mutable is_true : bool; - aid : int - } + and atom = { + var : var; + lit : formula; + neg : atom; + mutable watched : clause Vec.t; + mutable is_true : bool; + aid : int + } - and clause = { - name : string; - mutable atoms : atom Vec.t; - mutable activity : float; - mutable removed : bool; - learnt : bool; - cpremise : premise - } + and clause = { + name : string; + mutable atoms : atom Vec.t; + mutable activity : float; + mutable removed : bool; + learnt : bool; + cpremise : premise + } - and reason = clause option + and reason = clause option - and premise = clause list + and premise = clause list - val cpt_mk_var : int ref - type varmap - val ma : varmap ref + val cpt_mk_var : int ref + type varmap + val ma : varmap ref - val dummy_var : var - val dummy_atom : atom - val dummy_clause : clause + val dummy_var : var + val dummy_atom : atom + val dummy_clause : clause - val make_var : formula -> var * bool + val make_var : formula -> var * bool - val add_atom : formula -> atom + val add_atom : formula -> atom - val make_clause : string -> atom list -> int -> bool -> premise -> clause + val make_clause : string -> atom list -> int -> bool -> premise -> clause - val fresh_name : unit -> string + val fresh_name : unit -> string - val fresh_lname : unit -> string + val fresh_lname : unit -> string - val fresh_dname : unit -> string + val fresh_dname : unit -> string - val to_float : int -> float + val to_float : int -> float - val to_int : float -> int - val made_vars_info : unit -> int * var list - val clear : unit -> unit + val to_int : float -> int + val made_vars_info : unit -> int * var list + val clear : unit -> unit - val pp_atom : Format.formatter -> atom -> unit - val pp_clause : Format.formatter -> clause -> unit + val pp_atom : Format.formatter -> atom -> unit + val pp_clause : Format.formatter -> clause -> unit end diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index da38c7af..d3a0a040 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -13,13 +13,13 @@ (**************************************************************************) module type S = sig - type t - type formula - type explanation + type t + type formula + type explanation - exception Inconsistent of explanation + exception Inconsistent of explanation - val empty : unit -> t - val assume : cs:bool -> formula -> explanation -> t -> t + val empty : unit -> t + val assume : cs:bool -> formula -> explanation -> t -> t end diff --git a/smt/arith.ml b/smt/arith.ml index 3d331f07..f4e85e3c 100644 --- a/smt/arith.ml +++ b/smt/arith.ml @@ -35,9 +35,9 @@ module Type (X:Sig.X) : Polynome.T with type r = X.r = struct end module Make - (X : Sig.X) - (P : Polynome.T with type r = X.r) - (C : Sig.C with type t = P.t and type r = X.r) = struct + (X : Sig.X) + (P : Polynome.T with type r = X.r) + (C : Sig.C with type t = P.t and type r = X.r) = struct type t = P.t @@ -47,8 +47,8 @@ module Make let is_mine_a a = match A.LT.view a with - | A.Builtin (_,p,_) -> is_le p || is_lt p - | _ -> false + | A.Builtin (_,p,_) -> is_le p || is_lt p + | _ -> false let is_mine_symb = function | Sy.Int _ | Sy.Real _ @@ -60,7 +60,7 @@ module Make 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 @@ -103,68 +103,68 @@ module Make let mk_euc_division p p2 t1 t2 ctx = match P.to_list p2 with - | [], coef_p2 -> - let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in - let r, ctx' = X.make md in - let rp = P.mult (P.create [] ((Int 1) //coef_p2) Ty.Tint) (embed r) in - P.sub p rp, ctx' @ ctx - | _ -> assert false + | [], coef_p2 -> + let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in + let r, ctx' = X.make md in + let rp = P.mult (P.create [] ((Int 1) //coef_p2) Ty.Tint) (embed r) in + P.sub p rp, ctx' @ ctx + | _ -> assert false let rec mke coef p t ctx = let {T.f = sb ; xs = xs; ty = ty} = T.view t in match sb, xs with - | (Sy.Int n | Sy.Real n), _ -> - let c = coef */ (num_of_string (Hstring.view n)) in - P.add (P.create [] c ty) p, ctx + | (Sy.Int n | Sy.Real n), _ -> + let c = coef */ (num_of_string (Hstring.view n)) in + P.add (P.create [] c ty) p, ctx - | Sy.Op Sy.Mult, [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - P.add p (P.mult p1 p2), ctx + | Sy.Op Sy.Mult, [t1;t2] -> + let p1, ctx = mke coef (empty_polynome ty) t1 ctx in + let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in + P.add p (P.mult p1 p2), ctx - | Sy.Op Sy.Div, [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - let p3, ctx = - try - let p, approx = P.div p1 p2 in - if approx then mk_euc_division p p2 t1 t2 ctx - else p, ctx - with Division_by_zero | Polynome.Maybe_zero -> - P.create [coef, X.term_embed t] (Int 0) ty, ctx - in - P.add p p3, ctx - - | Sy.Op Sy.Plus , [t1;t2] -> - let p2, ctx = mke coef p t2 ctx in - mke coef p2 t1 ctx + | Sy.Op Sy.Div, [t1;t2] -> + let p1, ctx = mke coef (empty_polynome ty) t1 ctx in + let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in + let p3, ctx = + try + let p, approx = P.div p1 p2 in + if approx then mk_euc_division p p2 t1 t2 ctx + else p, ctx + with Division_by_zero | Polynome.Maybe_zero -> + P.create [coef, X.term_embed t] (Int 0) ty, ctx + in + P.add p p3, ctx - | Sy.Op Sy.Minus , [t1;t2] -> - let p2, ctx = mke (minus_num coef) p t2 ctx in - mke coef p2 t1 ctx + | Sy.Op Sy.Plus , [t1;t2] -> + let p2, ctx = mke coef p t2 ctx in + mke coef p2 t1 ctx - | Sy.Op Sy.Modulo , [t1;t2] -> - let p1, ctx = mke coef (empty_polynome ty) t1 ctx in - let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in - let p3, ctx = - try P.modulo p1 p2, ctx - with e -> - let t = T.make mod_symb [t1; t2] Ty.Tint in - let ctx = match e with - | Division_by_zero | Polynome.Maybe_zero -> ctx - | Polynome.Not_a_num -> mk_modulo t t1 t2 ctx - | _ -> assert false - in - P.create [coef, X.term_embed t] (Int 0) ty, ctx - in - P.add p p3, ctx - - | _ -> - let a, ctx' = X.make t in - let ctx = ctx' @ ctx in - match C.extract a with - | Some p' -> P.add p (P.mult (P.create [] coef ty) p'), ctx - | _ -> P.add p (P.create [coef, a] (Int 0) ty), ctx + | Sy.Op Sy.Minus , [t1;t2] -> + let p2, ctx = mke (minus_num coef) p t2 ctx in + mke coef p2 t1 ctx + + | Sy.Op Sy.Modulo , [t1;t2] -> + let p1, ctx = mke coef (empty_polynome ty) t1 ctx in + let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in + let p3, ctx = + try P.modulo p1 p2, ctx + with e -> + let t = T.make mod_symb [t1; t2] Ty.Tint in + let ctx = match e with + | Division_by_zero | Polynome.Maybe_zero -> ctx + | Polynome.Not_a_num -> mk_modulo t t1 t2 ctx + | _ -> assert false + in + P.create [coef, X.term_embed t] (Int 0) ty, ctx + in + P.add p p3, ctx + + | _ -> + let a, ctx' = X.make t in + let ctx = ctx' @ ctx in + match C.extract a with + | Some p' -> P.add p (P.mult (P.create [] coef ty) p'), ctx + | _ -> P.add p (P.create [coef, a] (Int 0) ty), ctx let arith_to_ac p = p (* @@ -206,17 +206,17 @@ module Make and nb_vars_in_alien r = match C.extract r with - | Some p -> - let l, _ = P.to_list p in - List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l - | None -> 1 + | Some p -> + let l, _ = P.to_list p in + List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l + | None -> 1 let max_list_ = function | [] -> 0 | [ _, x ] -> nb_vars_in_alien x | (_, x) :: l -> - let acc = nb_vars_in_alien x in - List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l + let acc = nb_vars_in_alien x in + List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l let type_info p = P.type_info p @@ -230,8 +230,8 @@ module Make 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)) + (fun s (_, a) -> XS.union (xs_of_list (X.leaves a)) s) + XS.empty (fst (P.to_list p)) in XS.elements s @@ -242,12 +242,12 @@ module Make let p = List.fold_left (fun p (ai, xi) -> - let xi' = X.subst x t xi in - let p' = match C.extract xi' with - | Some p' -> P.mult (P.create [] ai ty) p' - | _ -> P.create [ai, xi'] (Int 0) ty - in - P.add p p') + let xi' = X.subst x t xi in + let p' = match C.extract xi' with + | Some p' -> P.mult (P.create [] ai ty) p' + | _ -> P.create [ai, xi'] (Int 0) ty + in + P.add p p') (P.create [] c ty) l in check_int (Exception.Unsolvable) p; @@ -265,8 +265,8 @@ module Make if m =/ minus_num b then m +/ b else assert false else - if m <=/ b then m else assert false - + if m <=/ b then m else assert false + in if m if X.compare y x > 0 then - let k = X.term_embed (fresh_name ()) in - (b, k) :: l, (y, embed k)::sb - else (b, y) :: l, sb) + let k = X.term_embed (fresh_name ()) in + (b, k) :: l, (y, embed k)::sb + else (b, y) :: l, sb) ([], []) l let is_mine_p = List.map (fun (x,p) -> x, is_mine p) let extract_min = function - | [] -> assert false - | [c] -> c, [] - | (a, x) :: s -> - List.fold_left - (fun ((a, x), l) (b, y) -> - if abs_num a <=/ abs_num b then - (a, x), ((b, y) :: l) - else (b, y), ((a, x):: l)) ((a, x),[]) s + | [] -> assert false + | [c] -> c, [] + | (a, x) :: s -> + List.fold_left + (fun ((a, x), l) (b, y) -> + if abs_num a <=/ abs_num b then + (a, x), ((b, y) :: l) + else (b, y), ((a, x):: l)) ((a, x),[]) s (* Decision Procedures. Page 131 *) @@ -316,26 +316,26 @@ module Make let l, sbs = subst_bigger x l in let p = P.create l b Ty.Tint in match a with - | Int 0 -> assert false - | Int 1 -> - (* 3.1. si a = 1 alors on a une substitution entiere pour x *) - let p = mult_const p (Int (-1)) in - (x, is_mine p) :: (is_mine_p sbs) + | Int 0 -> assert false + | Int 1 -> + (* 3.1. si a = 1 alors on a une substitution entiere pour x *) + let p = mult_const p (Int (-1)) in + (x, is_mine p) :: (is_mine_p sbs) - | Int (-1) -> - (* 3.2. si a = -1 alors on a une subst entiere pour x*) - (x,is_mine p) :: (is_mine_p sbs) - | _ -> - (* 4. sinon, (|a| <> 1) et a <> 0 *) - (* 4.1. on rend le coef a positif s'il ne l'est pas deja *) - let a, l, b = - if compare_num a (Int 0) < 0 then - (minus_num a, - List.map (fun (a,x) -> minus_num a,x) l, (minus_num b)) - else (a, l, b) - in - (* 4.2. on reduit le systeme *) - omega_sigma sbs a x l b + | Int (-1) -> + (* 3.2. si a = -1 alors on a une subst entiere pour x*) + (x,is_mine p) :: (is_mine_p sbs) + | _ -> + (* 4. sinon, (|a| <> 1) et a <> 0 *) + (* 4.1. on rend le coef a positif s'il ne l'est pas deja *) + let a, l, b = + if compare_num a (Int 0) < 0 then + (minus_num a, + List.map (fun (a,x) -> minus_num a,x) l, (minus_num b)) + else (a, l, b) + in + (* 4.2. on reduit le systeme *) + omega_sigma sbs a x l b and omega_sigma sbs a x l b = @@ -390,9 +390,9 @@ module Make try let a, x = P.choose p in let p = - P.mult - (P.create [] ((Int (-1)) // a) (P.type_info p)) - (P.remove x p) + P.mult + (P.create [] ((Int (-1)) // a) (P.type_info p)) + (P.remove x p) in [x, is_mine p] with Not_found -> is_null p @@ -420,16 +420,16 @@ module Make let fully_interpreted sb = match sb with - | Sy.Op (Sy.Plus | Sy.Minus) -> true - | _ -> false + | Sy.Op (Sy.Plus | Sy.Minus) -> true + | _ -> false let term_extract _ = None module Rel = Fm.Make (X) - (struct - include P - let poly_of = embed - let alien_of = is_mine - end) + (struct + include P + let poly_of = embed + let alien_of = is_mine + end) end diff --git a/smt/arith.mli b/smt/arith.mli index 33ec6d8f..10afffe4 100644 --- a/smt/arith.mli +++ b/smt/arith.mli @@ -15,7 +15,7 @@ module Type (X : Sig.X ): Polynome.T with type r = X.r module Make - (X : Sig.X) - (P : Polynome.T with type r = X.r) - (C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY + (X : Sig.X) + (P : Polynome.T with type r = X.r) + (C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY with type r = X.r and type t = P.t diff --git a/smt/cc.ml b/smt/cc.ml index 21ad9397..192c2acd 100644 --- a/smt/cc.ml +++ b/smt/cc.ml @@ -79,11 +79,11 @@ module Make (X : Sig.X) = struct let make_cst t ctx = () let add_to_use t = () - + let lrepr fmt = List.iter (fprintf fmt "%a " X.print) let leaves t lvs = () - + let contra_congruence a ex = () let split_size sz = () @@ -108,13 +108,13 @@ module Make (X : Sig.X) = struct let concat_leaves uf l = let rec concat_rec acc t = match X.leaves (fst (Uf.find uf t)) , acc with - [] , _ -> one::acc - | res, [] -> res - | res , _ -> List.rev_append res acc + [] , _ -> one::acc + | res, [] -> res + | res , _ -> List.rev_append res acc in match List.fold_left concat_rec [] l with - [] -> [one] - | res -> res + [] -> [one] + | res -> res let are_equal env ex t1 t2 = if T.equal t1 t2 then ex @@ -128,9 +128,9 @@ module Make (X : Sig.X) = struct let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in if X.fully_interpreted f1 then acc else - let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in + let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then - try + try let ex = List.fold_left2 (are_equal env) ex xs1 xs2 in let a = A.LT.make (A.Eq(t1, t2)) in Print.congruent a ex; @@ -148,17 +148,17 @@ module Make (X : Sig.X) = struct let view find va ex_a = match va with - | A.Eq (t1, t2) -> - let r1, ex1 = find t1 in - let r2, ex2 = find t2 in - let ex = Ex.union (Ex.union ex1 ex2) ex_a in - A.Eq(r1, r2), ex - | A.Distinct (b, lt) -> - let lr, ex = fold_find_with_explanation find ex_a lt in - A.Distinct (b, lr), ex - | A.Builtin(b, s, l) -> - let lr, ex = fold_find_with_explanation find ex_a l in - A.Builtin(b, s, List.rev lr), ex + | A.Eq (t1, t2) -> + let r1, ex1 = find t1 in + let r2, ex2 = find t2 in + let ex = Ex.union (Ex.union ex1 ex2) ex_a in + A.Eq(r1, r2), ex + | A.Distinct (b, lt) -> + let lr, ex = fold_find_with_explanation find ex_a lt in + A.Distinct (b, lr), ex + | A.Builtin(b, s, l) -> + let lr, ex = fold_find_with_explanation find ex_a l in + A.Builtin(b, s, List.rev lr), ex let term_canonical_view env a ex_a = view (Uf.find env.uf) (A.LT.view a) ex_a @@ -167,86 +167,86 @@ module Make (X : Sig.X) = struct let new_facts_by_contra_congruence env r bol ex = match X.term_extract r with - | None -> [] - | Some t1 -> - match T.view t1 with - | {T.f=f1 ; xs=[x]} -> - List.fold_left - (fun acc t2 -> - match T.view t2 with - | {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> - let a = A.LT.make (A.Distinct (false, [x; y])) in - let dist = LTerm a in - begin match Uf.are_distinct env.uf t1 t2 with - | Yes ex' -> - let ex_r = Ex.union ex ex' in - Print.contra_congruence a ex_r; - (dist, ex_r) :: acc - | No -> assert false - end - | _ -> acc - ) [] (Uf.class_of env.uf bol) - | _ -> [] + | None -> [] + | Some t1 -> + match T.view t1 with + | {T.f=f1 ; xs=[x]} -> + List.fold_left + (fun acc t2 -> + match T.view t2 with + | {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> + let a = A.LT.make (A.Distinct (false, [x; y])) in + let dist = LTerm a in + begin match Uf.are_distinct env.uf t1 t2 with + | Yes ex' -> + let ex_r = Ex.union ex ex' in + Print.contra_congruence a ex_r; + (dist, ex_r) :: acc + | No -> assert false + end + | _ -> acc + ) [] (Uf.class_of env.uf bol) + | _ -> [] let contra_congruence = let true_,_ = X.make T.true_ in let false_, _ = X.make T.false_ in fun env r ex -> if X.equal (fst (Uf.find_r env.uf r)) true_ then - new_facts_by_contra_congruence env r T.false_ ex + new_facts_by_contra_congruence env r T.false_ ex else if X.equal (fst (Uf.find_r env.uf r)) false_ then - new_facts_by_contra_congruence env r T.true_ ex + new_facts_by_contra_congruence env r T.true_ ex else [] let clean_use = List.fold_left (fun env (a, ex) -> - match a with - | LSem _ -> assert false - | LTerm t -> - begin - match A.LT.view t with - | A.Distinct (_, lt) - | A.Builtin (_, _, lt) -> - let lvs = concat_leaves env.uf lt in - List.fold_left - (fun env rx -> - let st, sa = Use.find rx env.use in - let sa = SetA.remove (t, ex) sa in - { env with use = Use.add rx (st,sa) env.use } - ) env lvs - | _ -> assert false - end) + match a with + | LSem _ -> assert false + | LTerm t -> + begin + match A.LT.view t with + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let lvs = concat_leaves env.uf lt in + List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + let sa = SetA.remove (t, ex) sa in + { env with use = Use.add rx (st,sa) env.use } + ) env lvs + | _ -> assert false + end) let rec congruence_closure env r1 r2 ex = Print.cc r1 r2; let uf, res = Uf.union env.uf r1 r2 ex in List.fold_left (fun (env, l) (p, touched, v) -> - (* we look for use(p) *) - let p_t, p_a = Use.find p env.use in - - (* we compute terms and atoms to consider for congruence *) - let repr_touched = List.map (fun (_,a,_) -> a) touched in - let st_others, sa_others = Use.congr_close_up env.use p repr_touched in - - (* we update use *) - let nuse = Use.up_close_up env.use p v in - Use.print nuse; - - (* we check the congruence of the terms. *) - let env = {env with use=nuse} in - let new_eqs = - SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in - let touched_atoms = - List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched - in - let touched_atoms = SetA.fold (fun (a, ex) acc -> - (LTerm a, ex)::acc) p_a touched_atoms in - let touched_atoms = SetA.fold (fun (a, ex) acc -> - (LTerm a, ex)::acc) sa_others touched_atoms in - env, new_eqs @ touched_atoms - + (* we look for use(p) *) + let p_t, p_a = Use.find p env.use in + + (* we compute terms and atoms to consider for congruence *) + let repr_touched = List.map (fun (_,a,_) -> a) touched in + let st_others, sa_others = Use.congr_close_up env.use p repr_touched in + + (* we update use *) + let nuse = Use.up_close_up env.use p v in + Use.print nuse; + + (* we check the congruence of the terms. *) + let env = {env with use=nuse} in + let new_eqs = + SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in + let touched_atoms = + List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched + in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) p_a touched_atoms in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) sa_others touched_atoms in + env, new_eqs @ touched_atoms + ) ({env with uf=uf}, []) res let replay_atom env sa = @@ -263,8 +263,8 @@ module Make (X : Sig.X) = struct (* we add t's arguments in env *) let {T.f = f; xs = xs} = T.view t in let env, choices = - List.fold_left (fun (env, ch) t -> add_term env ch t ex) - (env, choices) xs + List.fold_left (fun (env, ch) t -> add_term env ch t ex) + (env, choices) xs in (* we update uf and use *) let nuf, ctx = Uf.add env.uf t in @@ -293,43 +293,43 @@ module Make (X : Sig.X) = struct let env = {env with uf = nuf; relation = rel} in env, choices end - + and add env choices a ex = match A.LT.view a with - | A.Eq (t1, t2) -> - let env, choices = add_term env choices t1 ex in - add_term env choices t2 ex - | A.Distinct (_, lt) - | A.Builtin (_, _, lt) -> - let env, choices = List.fold_left - (fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in - let lvs = concat_leaves env.uf lt in (* A verifier *) - let env = List.fold_left - (fun env rx -> - let st, sa = Use.find rx env.use in - { env with - use = Use.add rx (st,SetA.add (a, ex) sa) env.use } - ) env lvs - in - env, choices + | A.Eq (t1, t2) -> + let env, choices = add_term env choices t1 ex in + add_term env choices t2 ex + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let env, choices = List.fold_left + (fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in + let lvs = concat_leaves env.uf lt in (* A verifier *) + let env = List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + { env with + use = Use.add rx (st,SetA.add (a, ex) sa) env.use } + ) env lvs + in + env, choices and semantic_view env choices la = List.fold_left (fun (env, choices, lsa) (a, ex) -> - match a with - | LTerm a -> - let env, choices = add env choices a ex in - let sa, ex = term_canonical_view env a ex in - env, choices, (sa, Some a, ex)::lsa + match a with + | LTerm a -> + let env, choices = add env choices a ex in + let sa, ex = term_canonical_view env a ex in + env, choices, (sa, Some a, ex)::lsa - (* XXX si on fait canonical_view pour - A.Distinct, la theorie des tableaux - part dans les choux *) - | LSem (A.Builtin _ (*| A.Distinct _*) as sa) -> - let sa, ex = canonical_view env sa ex in - env, choices, (sa, None, ex)::lsa - | LSem sa -> - env, choices, (sa, None, ex)::lsa) + (* XXX si on fait canonical_view pour + A.Distinct, la theorie des tableaux + part dans les choux *) + | LSem (A.Builtin _ (*| A.Distinct _*) as sa) -> + let sa, ex = canonical_view env sa ex in + env, choices, (sa, None, ex)::lsa + | LSem sa -> + env, choices, (sa, None, ex)::lsa) (env, choices, []) la and assume_literal env choices la = @@ -339,24 +339,24 @@ module Make (X : Sig.X) = struct let env, choices = List.fold_left (fun (env, choices) (sa, _, ex) -> - Print.assume_literal sa; - match sa with - | A.Eq(r1, r2) -> - if !cc_active then - let env, l = congruence_closure env r1 r2 ex in - let env, choices = assume_literal env choices l in - let env, choices = - assume_literal env choices (contra_congruence env r1 ex) - in - assume_literal env choices (contra_congruence env r2 ex) - else - {env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices - | A.Distinct (false, lr) -> - if Uf.already_distinct env.uf lr then env, choices - else - {env with uf = Uf.distinct env.uf lr ex}, choices - | A.Distinct (true, _) -> assert false - | A.Builtin _ -> env, choices) + Print.assume_literal sa; + match sa with + | A.Eq(r1, r2) -> + if !cc_active then + let env, l = congruence_closure env r1 r2 ex in + let env, choices = assume_literal env choices l in + let env, choices = + assume_literal env choices (contra_congruence env r1 ex) + in + assume_literal env choices (contra_congruence env r2 ex) + else + {env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices + | A.Distinct (false, lr) -> + if Uf.already_distinct env.uf lr then env, choices + else + {env with uf = Uf.distinct env.uf lr ex}, choices + | A.Distinct (true, _) -> assert false + | A.Builtin _ -> env, choices) (env, choices) lsa in let env, l = replay_atom env lsa in @@ -366,30 +366,30 @@ module Make (X : Sig.X) = struct let rec aux ch bad_last dl base_env li = match li, bad_last with | [], _ -> - begin + begin match X.Rel.case_split base_env.relation with - | [] -> - { t with gamma_finite = base_env; choices = List.rev dl }, ch - | l -> - let l = - List.map - (fun (c, ex_c, size) -> - let exp = Ex.fresh_exp () in - let ex_c_exp = Ex.add_fresh exp ex_c in - (* A new explanation in order to track the choice *) - (c, size, CPos exp, ex_c_exp)) l in - let sz = - List.fold_left - (fun acc (a,s,_,_) -> - Num.mult_num acc s) (Num.Int 1) (l@dl) in - Print.split_size sz; - if Num.le_num sz max_split then aux ch No dl base_env l - else - { t with gamma_finite = base_env; choices = List.rev dl }, ch - end + | [] -> + { t with gamma_finite = base_env; choices = List.rev dl }, ch + | l -> + let l = + List.map + (fun (c, ex_c, size) -> + let exp = Ex.fresh_exp () in + let ex_c_exp = Ex.add_fresh exp ex_c in + (* A new explanation in order to track the choice *) + (c, size, CPos exp, ex_c_exp)) l in + let sz = + List.fold_left + (fun acc (a,s,_,_) -> + Num.mult_num acc s) (Num.Int 1) (l@dl) in + Print.split_size sz; + if Num.le_num sz max_split then aux ch No dl base_env l + else + { t with gamma_finite = base_env; choices = List.rev dl }, ch + end | ((c, size, CNeg, ex_c) as a)::l, _ -> - let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in - aux ch bad_last (a::dl) base_env l + let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in + aux ch bad_last (a::dl) base_env l (** This optimisation is not correct with the current explanation *) (* | [(c, size, CPos exp, ex_c)], Yes dep -> *) @@ -399,21 +399,21 @@ module Make (X : Sig.X) = struct (* aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, ex_c] *) | ((c, size, CPos exp, ex_c_exp) as a)::l, _ -> - try - Print.split_assume (LR.make c) ex_c_exp; - let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in - aux ch bad_last (a::dl) base_env l - with Exception.Inconsistent dep -> - match Ex.remove_fresh exp dep with - | None -> - (* The choice doesn't participate to the inconsistency *) - Print.split_backjump (LR.make c) dep; - raise (Exception.Inconsistent dep) - | Some dep -> - (* The choice participates to the inconsistency *) - let neg_c = LR.neg (LR.make c) in - Print.split_backtrack neg_c dep; - aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep] + try + Print.split_assume (LR.make c) ex_c_exp; + let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in + aux ch bad_last (a::dl) base_env l + with Exception.Inconsistent dep -> + match Ex.remove_fresh exp dep with + | None -> + (* The choice doesn't participate to the inconsistency *) + Print.split_backjump (LR.make c) dep; + raise (Exception.Inconsistent dep) + | Some dep -> + (* The choice participates to the inconsistency *) + let neg_c = LR.neg (LR.make c) in + Print.split_backtrack neg_c dep; + aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep] in aux ch bad_last (List.rev t.choices) base_env l @@ -421,45 +421,45 @@ module Make (X : Sig.X) = struct Print.begin_case_split (); let r = try - if t.choices = [] then look_for_sat [] t t.gamma [] - else - try - let env, lt = f t.gamma_finite in - look_for_sat lt t env [] - with Exception.Inconsistent dep -> - look_for_sat ~bad_last:(Yes dep) - [] { t with choices = []} t.gamma t.choices - with Exception.Inconsistent d -> - Print.end_case_split (); - raise (Exception.Inconsistent d) + if t.choices = [] then look_for_sat [] t t.gamma [] + else + try + let env, lt = f t.gamma_finite in + look_for_sat lt t env [] + with Exception.Inconsistent dep -> + look_for_sat ~bad_last:(Yes dep) + [] { t with choices = []} t.gamma t.choices + with Exception.Inconsistent d -> + Print.end_case_split (); + raise (Exception.Inconsistent d) in Print.end_case_split (); r let extract_from_semvalues = List.fold_left (fun acc r -> - match X.term_extract r with Some t -> SetT.add t acc | _ -> acc) + 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) + match a with + | A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2] + | A.Distinct (_, l) -> extract_from_semvalues acc l + | _ -> acc) let extract_terms_from_assumed = List.fold_left (fun acc (a, _) -> - match a with - | LTerm r -> begin - match Literal.LT.view r with - | Literal.Eq (t1, t2) -> - SetT.add t1 (SetT.add t2 acc) - | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> - List.fold_right SetT.add l acc - end - | _ -> acc) + match a with + | LTerm r -> begin + match Literal.LT.view r with + | Literal.Eq (t1, t2) -> + SetT.add t1 (SetT.add t2 acc) + | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> + List.fold_right SetT.add l acc + end + | _ -> acc) let assume ~cs a ex t = let a = LTerm a in @@ -487,25 +487,25 @@ module Make (X : Sig.X) = struct let query a t = Print.query a; try - match A.LT.view a with - | A.Eq (t1, t2) -> - let t = add_and_process a t in - Uf.are_equal t.gamma.uf t1 t2 + match A.LT.view a with + | A.Eq (t1, t2) -> + let t = add_and_process a t in + Uf.are_equal t.gamma.uf t1 t2 - | A.Distinct (false, [t1; t2]) -> - let na = A.LT.neg a in - let t = add_and_process na t in (* na ? *) - Uf.are_distinct t.gamma.uf t1 t2 + | A.Distinct (false, [t1; t2]) -> + let na = A.LT.neg a in + let t = add_and_process na t in (* na ? *) + Uf.are_distinct t.gamma.uf t1 t2 - | A.Distinct _ -> - assert false (* devrait etre capture par une analyse statique *) + | A.Distinct _ -> + assert false (* devrait etre capture par une analyse statique *) - | _ -> - let na = A.LT.neg a in - let t = add_and_process na t in - let env = t.gamma in - let rna, ex_rna = term_canonical_view env na Ex.empty in - X.Rel.query env.relation (rna, Some na, ex_rna) + | _ -> + let na = A.LT.neg a in + let t = add_and_process na t in + let env = t.gamma in + let rna, ex_rna = term_canonical_view env na Ex.empty in + X.Rel.query env.relation (rna, Some na, ex_rna) with Exception.Inconsistent d -> Yes d let empty () = diff --git a/smt/combine.ml b/smt/combine.ml index 1d153b78..c75664ce 100644 --- a/smt/combine.ml +++ b/smt/combine.ml @@ -36,7 +36,7 @@ struct let embed1 x = X1 x let embed5 x = X5 x - + let is_int v = let ty = match v with | X1 x -> X1.type_info x @@ -54,10 +54,10 @@ struct and comparei a b = match a, b with - | X1 x, X1 y -> X1.compare x y - | X5 x, X5 y -> X5.compare x y - | Term x , Term y -> Term.compare x y - | _ -> assert false + | X1 x, X1 y -> X1.compare x y + | X5 x, X5 y -> X5.compare x y + | Term x , Term y -> Term.compare x y + | _ -> assert false and theory_num x = Obj.tag (Obj.repr x) @@ -72,23 +72,23 @@ struct 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 + | X1 t -> fprintf fmt "%a" X1.print t + | X5 t -> fprintf fmt "%a" X5.print t + | Term t -> fprintf fmt "%a" Term.print t let leaves r = match r with - | X1 t -> X1.leaves t - | X5 t -> X5.leaves t - | Term _ -> [r] + | X1 t -> X1.leaves t + | X5 t -> X5.leaves t + | Term _ -> [r] let term_embed t = Term t let term_extract r = match r with - | X1 _ -> X1.term_extract r - | X5 _ -> X5.term_extract r - | Term t -> Some t + | 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 @@ -100,66 +100,66 @@ struct 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 - + | true, false -> X1.make t + | false, true -> X5.make t + | false, false -> Term t, [] + | _ -> assert false + let fully_interpreted sb = match X1.is_mine_symb sb, X5.is_mine_symb sb with - | true, false -> X1.fully_interpreted sb - | false, true -> X5.fully_interpreted sb - | false, false -> false - | _ -> assert false + | true, false -> X1.fully_interpreted sb + | false, true -> X5.fully_interpreted sb + | false, false -> false + | _ -> assert false let add_mr = List.fold_left (fun solved (p,v) -> - MR.add p (v::(try MR.find p solved with Not_found -> [])) solved) + MR.add p (v::(try MR.find p solved with Not_found -> [])) solved) let unsolvable = function | X1 x -> X1.unsolvable x | X5 x -> X5.unsolvable x | Term _ -> true - + let partition tag = List.partition (fun (u,t) -> - (theory_num u = tag || unsolvable u) && - (theory_num t = tag || unsolvable t)) + (theory_num u = tag || unsolvable u) && + (theory_num t = tag || unsolvable t)) let rec solve_list solved l = List.fold_left (fun solved (a,b) -> - let cmp = compare a b in - if cmp = 0 then solved else - match a , b with - (* both sides are empty *) - | Term _ , Term _ -> - add_mr solved (unsolvable_values cmp a b) - - (* only one side is empty *) - | (a, b) - when unsolvable a || unsolvable b || compare_tag a b = 0 -> - let a,b = if unsolvable a then b,a else a,b in - let cp , sol = partition (theory_num a) (solvei b a) in - solve_list (add_mr solved cp) sol - - (* both sides are not empty *) - | a , b -> solve_theoryj solved a b + let cmp = compare a b in + if cmp = 0 then solved else + match a , b with + (* both sides are empty *) + | Term _ , Term _ -> + add_mr solved (unsolvable_values cmp a b) + + (* only one side is empty *) + | (a, b) + when unsolvable a || unsolvable b || compare_tag a b = 0 -> + let a,b = if unsolvable a then b,a else a,b in + let cp , sol = partition (theory_num a) (solvei b a) in + solve_list (add_mr solved cp) sol + + (* both sides are not empty *) + | a , b -> solve_theoryj solved a b ) solved l and unsolvable_values cmp a b = match a, b with - (* Clash entre theories: On peut avoir ces pbs ? *) - | X1 _, X5 _ - | X5 _, X1 _ - -> assert false + (* Clash entre theories: On peut avoir ces pbs ? *) + | X1 _, X5 _ + | X5 _, X1 _ + -> assert false - (* theorie d'un cote, vide de l'autre *) - | X1 _, _ | _, X1 _ -> X1.solve a b - | X5 _, _ | _, X5 _ -> X5.solve a b - | Term _, Term _ -> [if cmp > 0 then a,b else b,a] + (* theorie d'un cote, vide de l'autre *) + | X1 _, _ | _, X1 _ -> X1.solve a b + | X5 _, _ | _, X5 _ -> X5.solve a b + | Term _, Term _ -> [if cmp > 0 then a,b else b,a] and solve_theoryj solved xi xj = let cp , sol = partition (theory_num xj) (solvei xi xj) in @@ -167,34 +167,34 @@ struct and solvei a b = match b with - | X1 _ -> X1.solve a b - | X5 _ -> X5.solve a b - | Term _ -> assert false + | X1 _ -> X1.solve a b + | X5 _ -> X5.solve a b + | Term _ -> assert false let rec solve_rec mt ab = let mr = solve_list mt ab in let mr , ab = MR.fold - (fun p lr ((mt,ab) as acc) -> match lr with - [] -> assert false - | [_] -> acc - | x::lx -> - MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx) - mr (mr,[]) + (fun p lr ((mt,ab) as acc) -> match lr with + [] -> assert false + | [_] -> acc + | x::lx -> + MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx) + mr (mr,[]) in if ab = [] then mr else solve_rec mr ab let solve a b = MR.fold (fun p lr ret -> - match lr with [r] -> (p ,r)::ret | _ -> assert false) + match lr with [r] -> (p ,r)::ret | _ -> assert false) (solve_rec MR.empty [a,b]) [] let rec type_info = function | X1 t -> X1.type_info t | X5 t -> X5.type_info t | Term t -> let {Term.ty = ty} = Term.view t in ty - + module Rel = struct type elt = r type r = elt @@ -203,7 +203,7 @@ struct r1: X1.Rel.t; r5: X5.Rel.t; } - + let empty _ = { r1=X1.Rel.empty (); r5=X5.Rel.empty (); @@ -214,12 +214,12 @@ struct let env5, { assume = a5; remove = rm5} = X5.Rel.assume env.r5 sa in {r1=env1; r5=env5}, { assume = a1@a5; remove = rm1@rm5;} - + let query env a = match X1.Rel.query env.r1 a with - | Yes _ as ans -> ans - | No -> X5.Rel.query env.r5 a - + | Yes _ as ans -> ans + | No -> X5.Rel.query env.r5 a + let case_split env = let seq1 = X1.Rel.case_split env.r1 in let seq5 = X5.Rel.case_split env.r5 in @@ -237,17 +237,17 @@ and TX1 : Polynome.T with type r = CX.r = Arith.Type(CX) and X1 : Sig.THEORY with type t = TX1.t and type r = CX.r = Arith.Make(CX)(TX1) (struct - type t = TX1.t - type r = CX.r - let extract = CX.extract1 - let embed = CX.embed1 - let assume env _ _ = env, {Sig.assume = []; remove = []} - end) + type t = TX1.t + type r = CX.r + let extract = CX.extract1 + let embed = CX.embed1 + let assume env _ _ = env, {Sig.assume = []; remove = []} + end) and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract = Sum.Make (struct - include CX - let extract = extract5 - let embed = embed5 - end) + include CX + let extract = extract5 + let embed = embed5 + end) diff --git a/smt/fm.ml b/smt/fm.ml index 22f16cb1..19d778a0 100644 --- a/smt/fm.ml +++ b/smt/fm.ml @@ -34,8 +34,8 @@ module type EXTENDED_Polynome = sig end module Make - (X : Sig.X) - (P : EXTENDED_Polynome with type r = X.r) = struct + (X : Sig.X) + (P : EXTENDED_Polynome with type r = X.r) = struct module MP = Map.Make(P) module SP = Set.Make(P) @@ -49,10 +49,10 @@ module Make module Seq = Set.Make (struct - type t = r L.view * L.LT.t option * Explanation.t - let compare (a, _, _) (b, _, _) = - LR.compare (LR.make a) (LR.make b) - end) + type t = r L.view * L.LT.t option * Explanation.t + let compare (a, _, _) (b, _, _) = + LR.compare (LR.make a) (LR.make b) + end) module Inequation = struct type t = { @@ -61,9 +61,9 @@ module Make dep : (Literal.LT.t * num * P.t * bool) list; expl : Explanation.t } - + let print fmt ineq = fprintf fmt "%a %s 0" P.print ineq.ple0 - (if ineq.is_le then "<=" else "<") + (if ineq.is_le then "<=" else "<") let create p1 p2 is_le a expl = let p = P.add p1 (P.mult (P.create [] (Int (-1)) (P.type_info p1)) p2) in @@ -77,12 +77,12 @@ module Make let pos_neg mx { ple0 = p } = List.fold_left (fun m (c,x) -> - let cmp = compare_num c (Int 0) in - if cmp = 0 then m - else - let (pos, neg) = try MX.find x m with Not_found -> (0,0) in - if cmp > 0 then MX.add x (pos+1, neg) m - else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p)) + let cmp = compare_num c (Int 0) in + if cmp = 0 then m + else + let (pos, neg) = try MX.find x m with Not_found -> (0,0) in + if cmp > 0 then MX.add x (pos+1, neg) m + else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p)) end @@ -99,7 +99,7 @@ module Make 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 = @@ -120,7 +120,7 @@ module Make let replace_inequation env x ineq = { env with - inequations = (x, ineq)::(List.remove_assoc x env.inequations) } + inequations = (x, ineq)::(List.remove_assoc x env.inequations) } let up_improved env p oldi newi = @@ -137,11 +137,11 @@ module Make let mult_bornes_vars vars monomes ty= List.fold_left (fun ui (y,n) -> - let ui' = try - fst (MX.find y monomes) - with Not_found -> Intervals.undefined ty - in - Intervals.mult ui (Intervals.power n ui') + let ui' = try + fst (MX.find y monomes) + with Not_found -> Intervals.undefined ty + in + Intervals.mult ui (Intervals.power n ui') ) (Intervals.point (Int 1) ty Explanation.empty) vars @@ -149,8 +149,8 @@ module Make let pl, v = P.to_list p in List.fold_left (fun i (a, x) -> - let i_x, _ = MX.find x env.monomes in - Intervals.add (Intervals.scale a i_x) i + let i_x, _ = MX.find x env.monomes in + Intervals.add (Intervals.scale a i_x) i ) (Intervals.point v (P.type_info p) Explanation.empty) pl let rec add_monome expl use_x env x = @@ -170,10 +170,10 @@ module Make let i = intervals_from_monomes env p in let i = try - let old_i = MP.find normal_p env.polynomes in - let old_i = Intervals.scale d - (Intervals.add old_i (Intervals.point c ty Explanation.empty)) in - Intervals.intersect i old_i + let old_i = MP.find normal_p env.polynomes in + let old_i = Intervals.scale d + (Intervals.add old_i (Intervals.point c ty Explanation.empty)) in + Intervals.intersect i old_i with Not_found -> i in env, i @@ -184,28 +184,28 @@ module Make let ty = X.type_info x in let ui, env = match X.term_extract x with - | Some t -> - let use_x = SX.singleton x in - begin - match Term.view t with - | {Term.f = (Sy.Op Sy.Div); xs = [a; b]} -> - let pa = P.poly_of (fst (X.make a)) in - let pb = P.poly_of (fst (X.make b)) in - let (pa', ca, da) as npa = P.normal_form_pos pa in - let (pb', cb, db) as npb = P.normal_form_pos pb in - let env, ia = init_alien expl pa npa ty use_x env in - let env, ib = init_alien expl pb npb ty use_x env in - let ia, ib = match Intervals.doesnt_contain_0 ib with - | Yes ex when Num.compare_num ca cb = 0 - && P.compare pa' pb' = 0 -> - let expl = Explanation.union ex expl in - Intervals.point da ty expl, Intervals.point db ty expl - | _ -> ia, ib - in - Intervals.div ia ib, env - | _ -> Intervals.undefined ty, env - end - | _ -> Intervals.undefined ty, env + | Some t -> + let use_x = SX.singleton x in + begin + match Term.view t with + | {Term.f = (Sy.Op Sy.Div); xs = [a; b]} -> + let pa = P.poly_of (fst (X.make a)) in + let pb = P.poly_of (fst (X.make b)) in + let (pa', ca, da) as npa = P.normal_form_pos pa in + let (pb', cb, db) as npb = P.normal_form_pos pb in + let env, ia = init_alien expl pa npa ty use_x env in + let env, ib = init_alien expl pb npb ty use_x env in + let ia, ib = match Intervals.doesnt_contain_0 ib with + | Yes ex when Num.compare_num ca cb = 0 + && P.compare pa' pb' = 0 -> + let expl = Explanation.union ex expl in + Intervals.point da ty expl, Intervals.point db ty expl + | _ -> ia, ib + in + Intervals.div ia ib, env + | _ -> Intervals.undefined ty, env + end + | _ -> Intervals.undefined ty, env in let u, use_x' = try MX.find x env.monomes @@ -219,57 +219,57 @@ module Make let env = tighten_div x env expl in SX.fold (fun x acc -> - let _, use = MX.find x acc.monomes in - update_monome expl use acc x) + let _, use = MX.find x acc.monomes in + update_monome expl use acc x) use_x env let update_monomes_from_poly p i polynomes monomes = let lp, _ = P.to_list p in let ty = P.type_info p in List.fold_left (fun monomes (a,x) -> - let np = P.remove x p in - let (np,c,d) = P.normal_form_pos np in - try - let inp = MP.find np polynomes in - let new_ix = - Intervals.scale - ((Int 1) // a) - (Intervals.add i - (Intervals.scale (minus_num d) - (Intervals.add inp - (Intervals.point c ty Explanation.empty)))) in - let old_ix, ux = MX.find x monomes in - let ix = Intervals.intersect old_ix new_ix in - MX.add x (ix, ux) monomes - with Not_found -> monomes) + let np = P.remove x p in + let (np,c,d) = P.normal_form_pos np in + try + let inp = MP.find np polynomes in + let new_ix = + Intervals.scale + ((Int 1) // a) + (Intervals.add i + (Intervals.scale (minus_num d) + (Intervals.add inp + (Intervals.point c ty Explanation.empty)))) in + let old_ix, ux = MX.find x monomes in + let ix = Intervals.intersect old_ix new_ix in + MX.add x (ix, ux) monomes + with Not_found -> monomes) monomes lp let update_polynomes env expl = let polynomes, monomes, improved = MP.fold - (fun p ip (polynomes, monomes, improved) -> - let new_i = intervals_from_monomes env p in - let i = Intervals.intersect new_i ip in - if Intervals.is_strict_smaller i ip then - let monomes = update_monomes_from_poly p i polynomes monomes in - let improved = SP.add p improved in - MP.add p i polynomes, monomes, improved - else polynomes, monomes, improved - ) env.polynomes (env.polynomes, env.monomes, env.improved) in + (fun p ip (polynomes, monomes, improved) -> + let new_i = intervals_from_monomes env p in + let i = Intervals.intersect new_i ip in + if Intervals.is_strict_smaller i ip then + let monomes = update_monomes_from_poly p i polynomes monomes in + let improved = SP.add p improved in + MP.add p i polynomes, monomes, improved + else polynomes, monomes, improved + ) env.polynomes (env.polynomes, env.monomes, env.improved) in {env with polynomes = polynomes; monomes = monomes ; improved = improved} let find_one_eq x u = match Intervals.is_point u with - | Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v -> - let eq = - L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in - Some (eq, None, ex) - | _ -> None + | Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v -> + let eq = + L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in + Some (eq, None, ex) + | _ -> None let find_eq eqs x u env = match find_one_eq x u with - | None -> eqs - | Some eq1 -> eq1::eqs + | None -> eqs + | Some eq1 -> eq1::eqs type ineq_status = | Trivial_eq @@ -280,24 +280,24 @@ module Make let ineq_status ({Inequation.ple0 = p ; is_le = is_le} as ineq) = match Inequation.is_monomial ineq with - Some (a, x, v) -> Monome (a, x, v) - | None -> - if P.is_empty p then - let _, v = P.to_list p in - let c = compare_num v (Int 0) in - if c > 0 || (c >=0 && not is_le) then Bottom - else - if c = 0 && is_le then Trivial_eq - else Trivial_ineq v - else Other - + Some (a, x, v) -> Monome (a, x, v) + | None -> + if P.is_empty p then + let _, v = P.to_list p in + let c = compare_num v (Int 0) in + if c > 0 || (c >=0 && not is_le) then Bottom + else + if c = 0 && is_le then Trivial_eq + else Trivial_ineq v + else Other + (*let ineqs_from_dep dep borne_inf is_le = List.map (fun {poly_orig = p; coef = c} -> - let (m,v,ty) = P.mult_const minusone p in - (* quelle valeur pour le ?????? *) - { ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ; - dep = []} + let (m,v,ty) = P.mult_const minusone p in + (* quelle valeur pour le ?????? *) + { ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ; + dep = []} )dep*) let mk_equality p = @@ -308,9 +308,9 @@ 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 + ) (env.inequations, eqs) dep in { env with inequations = inqs }, eqs @@ -319,9 +319,9 @@ module Make let b = ((Int (-1)) */ v) // a in let u = if a >/ (Int 0) then - Intervals.new_borne_sup expl b is_le uints + Intervals.new_borne_sup expl b is_le uints else - Intervals.new_borne_inf expl b is_le uints in + 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) @@ -332,96 +332,96 @@ module Make let ty = P.type_info p0 in let a, _ = P.choose p0 in let p, change = - if a u, Intervals.undefined ty + 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 = - if Intervals.is_strict_smaller u pu then - let polynomes = MP.add p u env.polynomes in - let monomes = update_monomes_from_poly p u polynomes env.monomes in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved } - else env + if Intervals.is_strict_smaller u pu then + let polynomes = MP.add p u env.polynomes in + let monomes = update_monomes_from_poly p u polynomes env.monomes in + let improved = SP.add p env.improved in + { env with + polynomes = polynomes; + monomes = monomes; + improved = improved } + else env in match P.to_list p0 with - | [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le) - | _ -> env + | [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le) + | _ -> env let add_inequations acc lin expl = List.fold_left (fun (env, eqs) ineq -> - (* let expl = List.fold_left - (fun expl (l,_,_,_) -> - Explanation.union (*Explanation.everything*) - (Explanation.singleton (Formula.mk_lit l)) - expl - ) expl ineq.Inequation.dep - in *) - let expl = Explanation.union ineq.Inequation.expl expl in - match ineq_status ineq with - | Bottom -> - raise (Exception.Inconsistent expl) - - | Trivial_eq -> - fm_equalities env eqs ineq - - | Trivial_ineq c -> - let n, pp = - List.fold_left - (fun ((n, pp) as acc) (_, _, p, is_le) -> - if is_le then acc else - match pp with - | Some _ -> n+1, None - | None when n=0 -> 1, Some p - | _ -> n+1, None) (0,None) ineq.Inequation.dep - in - let env = - List.fold_left - (fun env (_, coef, p, is_le) -> - let ty = P.type_info p in - let is_le = - match pp with - Some x -> P.compare x p = 0 | _ -> is_le && n=0 - in - let p' = P.sub (P.create [] (c // coef) ty) p in - update_ple0 env p' is_le expl - ) env ineq.Inequation.dep - in - env, eqs + (* let expl = List.fold_left + (fun expl (l,_,_,_) -> + Explanation.union (*Explanation.everything*) + (Explanation.singleton (Formula.mk_lit l)) + expl + ) expl ineq.Inequation.dep + in *) + let expl = Explanation.union ineq.Inequation.expl expl in + match ineq_status ineq with + | Bottom -> + raise (Exception.Inconsistent expl) - | Monome (a, x, v) -> - let env, eqs = - update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le - in + | Trivial_eq -> + fm_equalities env eqs ineq - (*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 + | Trivial_ineq c -> + let n, pp = + List.fold_left + (fun ((n, pp) as acc) (_, _, p, is_le) -> + if is_le then acc else + match pp with + | Some _ -> n+1, None + | None when n=0 -> 1, Some p + | _ -> n+1, None) (0,None) ineq.Inequation.dep + in + let env = + List.fold_left + (fun env (_, coef, p, is_le) -> + let ty = P.type_info p in + let is_le = + match pp with + Some x -> P.compare x p = 0 | _ -> is_le && n=0 + in + let p' = P.sub (P.create [] (c // coef) ty) p in + update_ple0 env p' is_le expl + ) env ineq.Inequation.dep + in + env, eqs + + | Monome (a, x, v) -> + let env, eqs = + update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le + in + + (*let env,eqs = update_bornes env eqs ((a,x),c) ineq.ple0.le in + let env,eqs = update_polynomes env eqs ineq in + env, pers_ineqs, eqs*) + env, eqs + + | Other -> + env, eqs + (*t env,eqs = update_polynomes env eqs ineq in + env, pers_ineqs, eqs*) - | Other -> - env, eqs - (*t env,eqs = update_polynomes env eqs ineq in - env, pers_ineqs, eqs*) - ) acc lin let mult_list c = @@ -430,9 +430,9 @@ module Make let div_by_pgcd (a, b) ty = try if ty = Ty.Tint then - let p = Big_int.gcd_big_int (big_int_of_num a) (big_int_of_num b) in - let p = num_of_big_int p in - a // p, b // p + let p = Big_int.gcd_big_int (big_int_of_num a) (big_int_of_num b) in + let p = num_of_big_int p in + a // p, b // p else a, b with Failure "big_int_of_ratio" -> a, b @@ -440,35 +440,35 @@ module Make let rec cross_rec acc = function | [] -> acc | { Inequation.ple0 = p1; is_le = k1; dep = d1; expl = ex1 } :: l -> - let n1 = abs_num (P.find x p1) in - (* let ty = P.type_info p1 in *) - let acc = - List.fold_left - (fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} -> - let n2 = abs_num (P.find x p2) in - (* let n1, n2 = div_by_pgcd (n1, n2) ty in *) - let p = P.add - (P.mult (P.create [] n2 (P.type_info p2)) p1) - (P.mult (P.create [] n1 (P.type_info p1)) p2) in - let d1 = mult_list n2 d1 in - let d2 = mult_list n1 d2 in - let ni = - { Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2; - expl = Explanation.union ex1 ex2 } - in - ni::acc - ) acc cpos - in - cross_rec acc l + let n1 = abs_num (P.find x p1) in + (* let ty = P.type_info p1 in *) + let acc = + List.fold_left + (fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} -> + let n2 = abs_num (P.find x p2) in + (* let n1, n2 = div_by_pgcd (n1, n2) ty in *) + let p = P.add + (P.mult (P.create [] n2 (P.type_info p2)) p1) + (P.mult (P.create [] n1 (P.type_info p1)) p2) in + let d1 = mult_list n2 d1 in + let d2 = mult_list n1 d2 in + let ni = + { Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2; + expl = Explanation.union ex1 ex2 } + in + ni::acc + ) acc cpos + in + cross_rec acc l in cross_rec [] cneg let split x l = let rec split_rec (cp, cn, co) ineq = try - let a = Inequation.find x ineq in - if a >/ (Int 0) then ineq::cp, cn, co - else cp, ineq::cn, co + let a = Inequation.find x ineq in + if a >/ (Int 0) then ineq::cp, cn, co + else cp, ineq::cn, co with Not_found -> cp, cn, ineq::co in List.fold_left split_rec ([], [], []) l @@ -478,30 +478,30 @@ module Make let choose_var l = let pos_neg = List.fold_left Inequation.pos_neg MX.empty l in let xopt = MX.fold (fun x (pos, neg) acc -> - match acc with - | None -> Some (x, pos * neg) - | Some (y, c') -> - let c = pos * neg in - if c < c' then Some (x, c) else acc - ) pos_neg None in + match acc with + | None -> Some (x, pos * neg) + | Some (y, c') -> + let c = pos * neg in + if c < c' then Some (x, c) else acc + ) pos_neg None in match xopt with - | Some (x, _) -> x - | None -> raise Not_found + | Some (x, _) -> x + | None -> raise Not_found let rec fourier ( (env, eqs) as acc) l expl = - match l with - | [] -> acc - | ineq :: l' -> - try - (* let x = Inequation.choose ineq in *) - let x = choose_var l in - let cpos, cneg, others = split x l in - let ninqs = cross x cpos cneg in - Debug.cross x cpos cneg others ninqs; - let acc = add_inequations acc cpos expl in - let acc = add_inequations acc cneg expl in - fourier acc (ninqs -@ others) expl - with Not_found -> add_inequations acc l expl + match l with + | [] -> acc + | ineq :: l' -> + try + (* let x = Inequation.choose ineq in *) + let x = choose_var l in + let cpos, cneg, others = split x l in + let ninqs = cross x cpos cneg in + Debug.cross x cpos cneg others ninqs; + let acc = add_inequations acc cpos expl in + let acc = add_inequations acc cneg expl in + fourier acc (ninqs -@ others) expl + with Not_found -> add_inequations acc l expl (* let fm env eqs expl = @@ -519,134 +519,134 @@ module Make let add_disequality env eqs p expl = let ty = P.type_info p in match P.to_list p with - | ([], (Int 0)) -> - raise (Exception.Inconsistent expl) - | ([], v) -> - env, eqs - | ([a, x], v) -> - let b = (minus_num v) // a in - let i1 = Intervals.point b ty expl in - let i2, use2 = - try - MX.find x env.monomes - with Not_found -> Intervals.undefined ty, SX.empty - in - let i = Intervals.exclude i1 i2 in - let env ={ env with monomes = MX.add x (i,use2) env.monomes } in - let env = tighten_non_lin x use2 env expl in - env, find_eq eqs x i env - | _ -> - let a, _ = P.choose p in - let p = if a >=/ Int 0 then p - else P.mult (P.create [] (Int (-1)) ty) p in - let p, c, _ = P.normal_form p in - let i1 = Intervals.point (minus_num c) ty expl in - let i2 = - try - MP.find p env.polynomes - with Not_found -> Intervals.undefined ty - in - let i = Intervals.exclude i1 i2 in - let env = - if Intervals.is_strict_smaller i i2 then - let polynomes = MP.add p i env.polynomes in - let monomes = update_monomes_from_poly p i polynomes env.monomes - in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved} - else env - in - env, eqs - + | ([], (Int 0)) -> + raise (Exception.Inconsistent expl) + | ([], v) -> + env, eqs + | ([a, x], v) -> + let b = (minus_num v) // a in + let i1 = Intervals.point b ty expl in + let i2, use2 = + try + MX.find x env.monomes + with Not_found -> Intervals.undefined ty, SX.empty + in + let i = Intervals.exclude i1 i2 in + let env ={ env with monomes = MX.add x (i,use2) env.monomes } in + let env = tighten_non_lin x use2 env expl in + env, find_eq eqs x i env + | _ -> + let a, _ = P.choose p in + let p = if a >=/ Int 0 then p + else P.mult (P.create [] (Int (-1)) ty) p in + let p, c, _ = P.normal_form p in + let i1 = Intervals.point (minus_num c) ty expl in + let i2 = + try + MP.find p env.polynomes + with Not_found -> Intervals.undefined ty + in + let i = Intervals.exclude i1 i2 in + let env = + if Intervals.is_strict_smaller i i2 then + let polynomes = MP.add p i env.polynomes in + let monomes = update_monomes_from_poly p i polynomes env.monomes + in + let improved = SP.add p env.improved in + { env with + polynomes = polynomes; + monomes = monomes; + improved = improved} + else env + in + env, eqs + let add_equality env eqs p expl = let ty = P.type_info p in match P.to_list p with - | ([], Int 0) -> env, eqs - | ([], v) -> - raise (Exception.Inconsistent expl) - | ([a, x], v) -> - let b = (minus_num v) // a in - let i = Intervals.point b ty expl in - let i, use = - try - let i', use' = MX.find x env.monomes in - Intervals.intersect i i', use' - with Not_found -> i, SX.empty - in - let env = { env with monomes = MX.add x (i, use) env.monomes} in - let env = tighten_non_lin x use env expl in - env, find_eq eqs x i env - | _ -> - let a, _ = P.choose p in - let p = if a >=/ Int 0 then p - else P.mult (P.create [] (Int (-1)) ty) p in - let p, c, _ = P.normal_form p in - let i = Intervals.point (minus_num c) ty expl in - let i, ip = - try - let ip = MP.find p env.polynomes in - Intervals.intersect i ip, ip - with Not_found -> i, Intervals.undefined ty - in - let env = - if Intervals.is_strict_smaller i ip then - let polynomes = MP.add p i env.polynomes in - let monomes = update_monomes_from_poly p i polynomes env.monomes - in - let improved = SP.add p env.improved in - { env with - polynomes = polynomes; - monomes = monomes; - improved = improved } - else env - in - let env = - { env with - known_eqs = SX.add (P.alien_of p) env.known_eqs - } in - env, eqs + | ([], Int 0) -> env, eqs + | ([], v) -> + raise (Exception.Inconsistent expl) + | ([a, x], v) -> + let b = (minus_num v) // a in + let i = Intervals.point b ty expl in + let i, use = + try + let i', use' = MX.find x env.monomes in + Intervals.intersect i i', use' + with Not_found -> i, SX.empty + in + let env = { env with monomes = MX.add x (i, use) env.monomes} in + let env = tighten_non_lin x use env expl in + env, find_eq eqs x i env + | _ -> + let a, _ = P.choose p in + let p = if a >=/ Int 0 then p + else P.mult (P.create [] (Int (-1)) ty) p in + let p, c, _ = P.normal_form p in + let i = Intervals.point (minus_num c) ty expl in + let i, ip = + try + let ip = MP.find p env.polynomes in + Intervals.intersect i ip, ip + with Not_found -> i, Intervals.undefined ty + in + let env = + if Intervals.is_strict_smaller i ip then + let polynomes = MP.add p i env.polynomes in + let monomes = update_monomes_from_poly p i polynomes env.monomes + in + let improved = SP.add p env.improved in + { env with + polynomes = polynomes; + monomes = monomes; + improved = improved } + else env + in + let env = + { env with + known_eqs = SX.add (P.alien_of p) env.known_eqs + } in + env, eqs let normal_form a = match a with | L.Builtin (false, n, [r1; r2]) when is_le n && X.type_info r1 = Ty.Tint -> - let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in - L.Builtin (true, n, [r2; P.alien_of pred_r1]) + let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in + L.Builtin (true, n, [r2; P.alien_of pred_r1]) | L.Builtin (true, n, [r1; r2]) when - not (is_le n) && X.type_info r1 = Ty.Tint -> - let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in - L.Builtin (true, ale, [r1; P.alien_of pred_r2]) + not (is_le n) && X.type_info r1 = Ty.Tint -> + let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in + L.Builtin (true, ale, [r1; P.alien_of pred_r2]) | L.Builtin (false, n, [r1; r2]) when is_le n -> - L.Builtin (true, alt, [r2; r1]) + L.Builtin (true, alt, [r2; r1]) | L.Builtin (false, n, [r1; r2]) when is_lt n -> - L.Builtin (true, ale, [r2; r1]) + 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 set_of l = + List.fold_left (fun s e -> Seq.add e s) Seq.empty l + in + Seq.elements (Seq.diff (set_of eqs) (set_of la)) let equalities_from_polynomes env eqs = let known, eqs = MP.fold - (fun p i (knw, eqs) -> - let xp = P.alien_of p in - if SX.mem xp knw then knw, eqs - else - match Intervals.is_point i with + (fun p i (knw, eqs) -> + let xp = P.alien_of p in + if SX.mem xp knw then knw, eqs + else + match Intervals.is_point i with | Some (num, ex) -> let r2 = P.alien_of (P.create [] num (P.type_info p)) in SX.add xp knw, (L.Eq(xp, r2), None, ex) :: eqs - | None -> knw, eqs - ) env.polynomes (env.known_eqs, eqs) + | None -> knw, eqs + ) env.polynomes (env.known_eqs, eqs) in {env with known_eqs= known}, eqs @@ -655,13 +655,13 @@ module Make let known, eqs = MX.fold (fun x (i,_) (knw, eqs) -> - if SX.mem x knw then knw, eqs - else - match Intervals.is_point i with - | Some (num, ex) -> - let r2 = P.alien_of (P.create [] num (X.type_info x)) in - SX.add x knw, (L.Eq(x, r2), None, ex) :: eqs - | None -> knw, eqs + if SX.mem x knw then knw, eqs + else + match Intervals.is_point i with + | Some (num, ex) -> + let r2 = P.alien_of (P.create [] num (X.type_info x)) in + SX.add x knw, (L.Eq(x, r2), None, ex) :: eqs + | None -> knw, eqs ) env.monomes (env.known_eqs, eqs) in {env with known_eqs= known}, eqs @@ -674,47 +674,47 @@ module Make Debug.env env; let env, eqs, new_ineqs, expl = List.fold_left - (fun (env, eqs, new_ineqs, expl) (a, root, e) -> - let a = normal_form a in - let expl = Explanation.union e expl in - try + (fun (env, eqs, new_ineqs, expl) (a, root, e) -> + let a = normal_form a in + let expl = Explanation.union e expl in + try match a with - | L.Builtin(_, n, [r1;r2]) when is_le n || is_lt n -> - let root = match root with - | Some a -> a | None -> assert false in - let p1 = P.poly_of r1 in - let p2 = P.poly_of r2 in - let ineq = Inequation.create p1 p2 (is_le n) root expl in - let env = - init_monomes env ineq.Inequation.ple0 SX.empty expl in - let env = - update_ple0 env ineq.Inequation.ple0 (is_le n) expl in - let env = replace_inequation env root ineq in - env, eqs, true, expl + | L.Builtin(_, n, [r1;r2]) when is_le n || is_lt n -> + let root = match root with + | Some a -> a | None -> assert false in + let p1 = P.poly_of r1 in + let p2 = P.poly_of r2 in + let ineq = Inequation.create p1 p2 (is_le n) root expl in + let env = + init_monomes env ineq.Inequation.ple0 SX.empty expl in + let env = + update_ple0 env ineq.Inequation.ple0 (is_le n) expl in + let env = replace_inequation env root ineq in + env, eqs, true, expl - | L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 -> - let p = P.sub (P.poly_of r1) (P.poly_of r2) in - let env = init_monomes env p SX.empty expl in - let env, eqs = add_disequality env eqs p expl in - env, eqs, new_ineqs, expl - - | L.Eq(r1, r2) when is_num r1 && is_num r2 -> - let p = P.sub (P.poly_of r1) (P.poly_of r2) in - let env = init_monomes env p SX.empty expl in - let env, eqs = add_equality env eqs p expl in - env, eqs, new_ineqs, expl + | L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 -> + let p = P.sub (P.poly_of r1) (P.poly_of r2) in + let env = init_monomes env p SX.empty expl in + let env, eqs = add_disequality env eqs p expl in + env, eqs, new_ineqs, expl + + | L.Eq(r1, r2) when is_num r1 && is_num r2 -> + let p = P.sub (P.poly_of r1) (P.poly_of r2) in + let env = init_monomes env p SX.empty expl in + let env, eqs = add_equality env eqs p expl in + env, eqs, new_ineqs, expl + + | _ -> (env, eqs, new_ineqs, expl) + + with Intervals.NotConsistent expl -> + raise (Exception.Inconsistent expl) + ) + (env, [], false, Explanation.empty) la - | _ -> (env, eqs, new_ineqs, expl) - - with Intervals.NotConsistent expl -> - raise (Exception.Inconsistent expl) - ) - (env, [], false, Explanation.empty) la - in if new_ineqs then if false then - (); + (); try (* we only call fm when new ineqs are assumed *) let env, eqs = if new_ineqs then fm env eqs expl else env, eqs in @@ -725,14 +725,14 @@ module Make let eqs = remove_trivial_eqs eqs la in Debug.implied_equalities eqs; let result = - List.fold_left - (fun r (a_sem, a_term, ex) -> - { assume = (LSem(a_sem), ex) :: r.assume; - remove = - match a_term with - | None -> r.remove - | Some t -> (LTerm(t), ex)::r.remove - } ) { assume = []; remove = [] } eqs + List.fold_left + (fun r (a_sem, a_term, ex) -> + { assume = (LSem(a_sem), ex) :: r.assume; + remove = + match a_term with + | None -> r.remove + | Some t -> (LTerm(t), ex)::r.remove + } ) { assume = []; remove = [] } eqs in env, result @@ -747,60 +747,60 @@ module Make let case_split_polynomes env = let o = MP.fold - (fun p i o -> - match Intervals.finite_size i with - | Some s when s >/ (Int 1) -> - begin - match o with - | Some (s', _, _, _) when s' <=/ s -> o - | _ -> - let n, ex = Intervals.borne_inf i in - Some (s, p, n, ex) - end - | _ -> o - ) env.polynomes None in + (fun p i o -> + match Intervals.finite_size i with + | Some s when s >/ (Int 1) -> + begin + match o with + | Some (s', _, _, _) when s' <=/ s -> o + | _ -> + let n, ex = Intervals.borne_inf i in + Some (s, p, n, ex) + end + | _ -> o + ) env.polynomes None in match o with - | Some (s, p, n, ex) -> - let r1 = P.alien_of p in - let r2 = P.alien_of (P.create [] n (P.type_info p)) in - [L.Eq(r1, r2), ex, s] - | None -> - [] + | Some (s, p, n, ex) -> + let r1 = P.alien_of p in + let r2 = P.alien_of (P.create [] n (P.type_info p)) in + [L.Eq(r1, r2), ex, s] + | None -> + [] let case_split_monomes env = let o = MX.fold - (fun x (i,_) o -> - match Intervals.finite_size i with - | Some s when s >/ (Int 1) -> - begin - match o with - | Some (s', _, _, _) when s' <=/ s -> o - | _ -> - let n, ex = Intervals.borne_inf i in - Some (s, x, n, ex) - end - | _ -> o - ) env.monomes None in + (fun x (i,_) o -> + match Intervals.finite_size i with + | Some s when s >/ (Int 1) -> + begin + match o with + | Some (s', _, _, _) when s' <=/ s -> o + | _ -> + let n, ex = Intervals.borne_inf i in + Some (s, x, n, ex) + end + | _ -> o + ) env.monomes None in match o with - | Some (s,x,n,ex) -> - let ty = X.type_info x in - let r1 = x in - let r2 = P.alien_of (P.create [] n ty) in - [L.Eq(r1, r2), ex, s] - | None -> - [] + | Some (s,x,n,ex) -> + let ty = X.type_info x in + let r1 = x in + let r2 = P.alien_of (P.create [] n ty) in + [L.Eq(r1, r2), ex, s] + | None -> + [] let case_split env = match case_split_polynomes env with - | [] -> case_split_monomes env - | choices -> choices + | [] -> case_split_monomes env + | choices -> choices let add env _ = env let extract_improved env = SP.fold (fun p acc -> - MP.add p (MP.find p env.polynomes) acc) + MP.add p (MP.find p env.polynomes) acc) env.improved MP.empty end diff --git a/smt/fm.mli b/smt/fm.mli index b35e56ee..fbae100f 100644 --- a/smt/fm.mli +++ b/smt/fm.mli @@ -18,6 +18,6 @@ module type EXTENDED_Polynome = sig end module Make - (X : Sig.X) - (P : EXTENDED_Polynome with type r = X.r) + (X : Sig.X) + (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 8b9d086c..ed304ee3 100644 --- a/smt/intervals.ml +++ b/smt/intervals.ml @@ -23,54 +23,54 @@ type borne = let compare_bornes b1 b2 = match b1, b2 with - | Minfty, Minfty | Pinfty, Pinfty -> 0 - | Minfty, _ | _, Pinfty -> -1 - | Pinfty, _ | _, Minfty -> 1 - | Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _) - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - compare_num v1 v2 + | Minfty, Minfty | Pinfty, Pinfty -> 0 + | Minfty, _ | _, Pinfty -> -1 + | Pinfty, _ | _, Minfty -> 1 + | Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _) + | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> + compare_num v1 v2 let compare_bu_bl b1 b2 = match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c + | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) + | Strict _, Strict _ | Large _, Large _ -> + compare_bornes b1 b2 + | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then -1 else c let compare_bl_bu b1 b2 = match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c + | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) + | Strict _, Strict _ | Large _, Large _ -> + compare_bornes b1 b2 + | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then 1 else c let compare_bl_bl b1 b2 = match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c - | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c + | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) + | Strict _, Strict _ | Large _, Large _ -> + compare_bornes b1 b2 + | Strict (v1, _), Large (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then 1 else c + | Large (v1, _), Strict (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then -1 else c let compare_bu_bu b1 b2 = match b1, b2 with - | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) - | Strict _, Strict _ | Large _, Large _ -> - compare_bornes b1 b2 - | Strict (v1, _), Large (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then -1 else c - | Large (v1, _), Strict (v2, _) -> - let c = compare_num v1 v2 in - if c = 0 then 1 else c + | (Minfty | Pinfty), _ | _,(Minfty | Pinfty) + | Strict _, Strict _ | Large _, Large _ -> + compare_bornes b1 b2 + | Strict (v1, _), Large (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then -1 else c + | Large (v1, _), Strict (v2, _) -> + let c = compare_num v1 v2 in + if c = 0 then 1 else c type t = { ints : (borne * borne) list; @@ -86,7 +86,7 @@ let print_borne fmt = function | Minfty -> fprintf fmt "-inf" | Pinfty -> fprintf fmt "+inf" | Strict (v, e) | Large (v, e) -> - fprintf fmt "%s" (string_of_num v) + fprintf fmt "%s" (string_of_num v) let print_interval fmt (b1,b2) = let c1, c2 = match b1, b2 with @@ -119,21 +119,21 @@ let explain_borne = function let add_expl_to_borne b e = match b with - | Large (n, e') -> Large (n, Ex.union e e') - | Strict (n, e') -> Strict (n, Ex.union e e') - | Pinfty | Minfty -> b + | Large (n, e') -> Large (n, Ex.union e e') + | Strict (n, e') -> Strict (n, Ex.union e e') + | Pinfty | Minfty -> b let borne_of k e n = if k then Large (n, e) else Strict (n, e) let is_point { ints = l; expl = e } = match l with - | [Large (v1, e1) , Large (v2, e2)] when v1 =/ v2 -> - Some (v1, Ex.union e2 (Ex.union e1 e)) - | _ -> None + | [Large (v1, e1) , Large (v2, e2)] when v1 =/ v2 -> + Some (v1, Ex.union e2 (Ex.union e1 e)) + | _ -> None let add_expl_zero i expl = let res = List.map (fun x -> - match x with + match x with | (Large ((Num.Int 0), e1) , Large ((Num.Int 0), e2)) -> (Large ((Num.Int 0), Ex.union e1 expl), Large ((Num.Int 0), Ex.union e2 expl)) @@ -141,45 +141,45 @@ let add_expl_zero i expl = { i with ints = res } let check_one_interval b1 b2 is_int = - match b1, b2 with - | Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty) - | (Strict (v1, e1) | Large (v1,e1)), - (Strict (v2, e2) | Large (v2, e2)) -> - let c = compare_num v1 v2 in - if c > 0 then raise - (EmptyInterval (Ex.union e2 e1)); - if c = 0 then begin - match b1, b2 with - | Large _, Large _ when not is_int || is_integer_num v1 -> - () - | _ -> raise (EmptyInterval (Ex.union e2 e1)) - end - | _ -> () + match b1, b2 with + | Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty) + | (Strict (v1, e1) | Large (v1,e1)), + (Strict (v2, e2) | Large (v2, e2)) -> + let c = compare_num v1 v2 in + if c > 0 then raise + (EmptyInterval (Ex.union e2 e1)); + if c = 0 then begin + match b1, b2 with + | Large _, Large _ when not is_int || is_integer_num v1 -> + () + | _ -> raise (EmptyInterval (Ex.union e2 e1)) + end + | _ -> () let min_borne b1 b2 = match b1, b2 with - | Minfty , _ | _ , Minfty -> Minfty - | b , Pinfty | Pinfty, b -> b - | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> - let c = compare_num v1 v2 in - if c < 0 then b1 - else if c > 0 then b2 - else match b1, b2 with - | (Strict _ as b) , _ | _, (Strict _ as b) -> b - | _, _ -> b1 + | Minfty , _ | _ , Minfty -> Minfty + | b , Pinfty | Pinfty, b -> b + | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> + let c = compare_num v1 v2 in + if c < 0 then b1 + else if c > 0 then b2 + else match b1, b2 with + | (Strict _ as b) , _ | _, (Strict _ as b) -> b + | _, _ -> b1 let max_borne b1 b2 = match b1, b2 with - | Pinfty , _ | _ , Pinfty -> Pinfty - | b , Minfty | Minfty, b -> b - | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> - let c = compare_num v1 v2 in - if c > 0 then b1 - else if c < 0 then b2 - else match b1, b2 with - | (Strict _ as b) , _ | _, (Strict _ as b) -> b - | _, _ -> b1 - + | Pinfty , _ | _ , Pinfty -> Pinfty + | b , Minfty | Minfty, b -> b + | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> + let c = compare_num v1 v2 in + if c > 0 then b1 + else if c < 0 then b2 + else match b1, b2 with + | (Strict _ as b) , _ | _, (Strict _ as b) -> b + | _, _ -> b1 + let pos_borne b1 = compare_bornes b1 (borne_of true Ex.empty (Int 0)) >= 0 let pos_borne_strict b1 = @@ -196,32 +196,32 @@ exception Found of Sig.answer let doesnt_contain_0 {ints=l} = try let max = List.fold_left - (fun old_u (l, u) -> - if neg_borne l && pos_borne u then raise (Found Sig.No); - if neg_borne_strict old_u && pos_borne_strict l then - raise (Found - (Sig.Yes - (Ex.union - (explain_borne old_u) (explain_borne l)))); - u) Minfty l in + (fun old_u (l, u) -> + if neg_borne l && pos_borne u then raise (Found Sig.No); + if neg_borne_strict old_u && pos_borne_strict l then + raise (Found + (Sig.Yes + (Ex.union + (explain_borne old_u) (explain_borne l)))); + u) Minfty l in if neg_borne_strict max then Sig.Yes (explain_borne max) else Sig.No with Found ans -> ans let is_strict_smaller i1 i2 = match i1, i2 with - | _, [] -> false - | [], _ -> true - | _ -> - try - List.iter2 (fun (l1, u1) (l2, u2) -> - if compare_bornes l1 l2 > 0 || compare_bornes u1 u2 < 0 - then raise Exit - ) i1 i2; - false - with - | Exit -> true - | Invalid_argument _ -> List.length i1 > List.length i2 + | _, [] -> false + | [], _ -> true + | _ -> + try + List.iter2 (fun (l1, u1) (l2, u2) -> + if compare_bornes l1 l2 > 0 || compare_bornes u1 u2 < 0 + then raise Exit + ) i1 i2; + false + with + | Exit -> true + | Invalid_argument _ -> List.length i1 > List.length i2 let is_strict_smaller {ints=i1} {ints=i2} = is_strict_smaller i1 i2 @@ -229,14 +229,14 @@ let is_strict_smaller {ints=i1} {ints=i2} = let rec union_bornes l = match l with - | [] | [_] -> l - | (l1, u1)::((l2, u2)::r as r2) -> - if compare_bornes u1 l2 < 0 then - (l1, u1)::(union_bornes r2) - else if compare_bornes u1 u2 > 0 then - union_bornes ((l1, u1)::r) - else - union_bornes ((l1, u2)::r) + | [] | [_] -> l + | (l1, u1)::((l2, u2)::r as r2) -> + if compare_bornes u1 l2 < 0 then + (l1, u1)::(union_bornes r2) + else if compare_bornes u1 u2 > 0 then + union_bornes ((l1, u1)::r) + else + union_bornes ((l1, u2)::r) let union ({ints = l} as uints) = let l = List.sort (fun (l1, _) (l2, _) -> compare_bornes l1 l2) l in @@ -244,13 +244,13 @@ let union ({ints = l} as uints) = let add_borne b1 b2 = match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> assert false - | Minfty, _ | _, Minfty -> Minfty - | Pinfty, _ | _, Pinfty -> Pinfty - | Large (v1, e1), Large (v2, e2) -> - Large (v1 +/ v2, Ex.union e1 e2) - | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) -> - Strict (v1 +/ v2, Ex.union e1 e2) + | Minfty, Pinfty | Pinfty, Minfty -> assert false + | Minfty, _ | _, Minfty -> Minfty + | Pinfty, _ | _, Pinfty -> Pinfty + | Large (v1, e1), Large (v2, e2) -> + Large (v1 +/ v2, Ex.union e1 e2) + | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) -> + Strict (v1 +/ v2, Ex.union e1 e2) let add_interval l (b1,b2) = List.fold_right @@ -293,35 +293,35 @@ 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 - then b - else if pos_borne b then Minfty - else Pinfty - | Pinfty, b | b, Pinfty -> - if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 - then b - else if pos_borne b then Pinfty - else Minfty - | Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2) - | Large (v1, e1), Strict (v2, e2) -> - Strict (v1 */ v2, Ex.union e1 e2) - | Large (v1, e1), Large (v2, e2) -> - Large (v1 */ v2, Ex.union e1 e2) + | Minfty, Pinfty | Pinfty, Minfty -> assert false + | Minfty, b | b, Minfty -> + if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 + then b + else if pos_borne b then Minfty + else Pinfty + | Pinfty, b | b, Pinfty -> + if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 + then b + else if pos_borne b then Pinfty + else Minfty + | Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2) + | Large (v1, e1), Strict (v2, e2) -> + Strict (v1 */ v2, Ex.union e1 e2) + | Large (v1, e1), Large (v2, e2) -> + Large (v1 */ v2, Ex.union e1 e2) let mult_borne_inf b1 b2 = match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> Minfty - | _, _ -> mult_borne b1 b2 + | Minfty, Pinfty | Pinfty, Minfty -> Minfty + | _, _ -> mult_borne b1 b2 let mult_borne_sup b1 b2 = match b1,b2 with - | Minfty, Pinfty | Pinfty, Minfty -> Pinfty - | _, _ -> mult_borne b1 b2 + | Minfty, Pinfty | Pinfty, Minfty -> Pinfty + | _, _ -> mult_borne b1 b2 type interval_class = | P of Ex.t @@ -338,96 +338,96 @@ 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 -> - mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, M e2 -> - mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2 - | P e1, N e2 -> - mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2 - | M e1, P e2 -> - mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2 - | M e1, M e2 -> - min_borne (mult_borne_inf a d) (mult_borne_inf b c), - max_borne (mult_borne_sup a c) (mult_borne_sup b d), - Ex.union e1 e2 - | M e1, N e2 -> - mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2 - | N e1, P e2 -> - mult_borne_inf a d, mult_borne_sup b c, Ex.union e1 e2 - | N e1, M e2 -> - mult_borne_inf a d, mult_borne_sup a c, Ex.union e1 e2 - | N e1, N e2 -> - mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2 - | Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty) - | (P _ | M _ | N _ ), Z -> (c, d, Ex.empty) + | P e1, P e2 -> + mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2 + | P e1, M e2 -> + mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2 + | P e1, N e2 -> + mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2 + | M e1, P e2 -> + mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2 + | M e1, M e2 -> + min_borne (mult_borne_inf a d) (mult_borne_inf b c), + max_borne (mult_borne_sup a c) (mult_borne_sup b d), + Ex.union e1 e2 + | M e1, N e2 -> + mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2 + | N e1, P e2 -> + mult_borne_inf a d, mult_borne_sup b c, Ex.union e1 e2 + | N e1, M e2 -> + mult_borne_inf a d, mult_borne_sup a c, Ex.union e1 e2 + | N e1, N e2 -> + mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2 + | Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty) + | (P _ | M _ | N _ ), Z -> (c, d, Ex.empty) let rec power_borne_inf p b = match p with - | 1 -> b - | p -> mult_borne_inf b (power_borne_inf (p-1) b) + | 1 -> b + | p -> mult_borne_inf b (power_borne_inf (p-1) b) let rec power_borne_sup p b = match p with - | 1 -> b - | p -> mult_borne_sup b (power_borne_sup (p-1) b) + | 1 -> b + | p -> mult_borne_sup b (power_borne_sup (p-1) b) let max_merge b1 b2 = let ex = Ex.union (explain_borne b1) (explain_borne b2) in let max = max_borne b1 b2 in match max with - | Minfty | Pinfty -> max - | Large (v, e) -> Large (v, ex) - | Strict (v, e) -> Strict (v, ex) + | Minfty | Pinfty -> max + | Large (v, e) -> Large (v, ex) + | Strict (v, e) -> Strict (v, ex) let power_bornes p (b1,b2) = if neg_borne b1 && pos_borne b2 then match p with - | 0 -> assert false - | p when p mod 2 = 0 -> - (* max_merge to have explanations !!! *) - let m = max_merge (power_borne_sup p b1) (power_borne_sup p b2) in - (Large (Int 0, Ex.empty), m) - | _ -> (power_borne_inf p b1, power_borne_sup p b2) + | 0 -> assert false + | p when p mod 2 = 0 -> + (* max_merge to have explanations !!! *) + let m = max_merge (power_borne_sup p b1) (power_borne_sup p b2) in + (Large (Int 0, Ex.empty), m) + | _ -> (power_borne_inf p b1, power_borne_sup p b2) else if pos_borne b1 && pos_borne b2 then (power_borne_inf p b1, power_borne_sup p b2) else if neg_borne b1 && neg_borne b2 then match p with - | 0 -> assert false - | p when p mod 2 = 0 -> (power_borne_inf p b2, power_borne_sup p b1) - | _ -> (power_borne_inf p b1, power_borne_sup p b2) + | 0 -> assert false + | p when p mod 2 = 0 -> (power_borne_inf p b2, power_borne_sup p b1) + | _ -> (power_borne_inf p b1, power_borne_sup p b2) else assert false let int_of_borne_inf b = match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (ceiling_num v, e) - | Strict (v, e) -> - let v' = ceiling_num v in - if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) + | Minfty | Pinfty -> b + | Large (v, e) -> Large (ceiling_num v, e) + | Strict (v, e) -> + let v' = ceiling_num v in + if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) let int_of_borne_sup b = match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' b + | Large (v, e) -> Large (floor_num v, e) + | Strict (v, e) -> + let v' = floor_num v in + if v' b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) + | Minfty | Pinfty -> b + | Large (v, e) -> Large (floor_num v, e) + | Strict (v, e) -> + let v' = floor_num v in + if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) let int_div_of_borne_sup b = match b with - | Minfty | Pinfty -> b - | Large (v, e) -> Large (floor_num v, e) - | Strict (v, e) -> - let v' = floor_num v in - if v' b + | Large (v, e) -> Large (floor_num v, e) + | Strict (v, e) -> + let v' = floor_num v in + if v' - let (lo1,up1), (lo2,up2) = - if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2) - else (lo1,up1), (lo2,up2) in - let cll = compare_bl_bl lo1 lo2 in - let cuu = compare_bu_bu up1 up2 in - let clu = compare_bl_bu lo1 up2 in - let cul = compare_bu_bl up1 lo2 in - if cul < 0 then - let nexpl = Ex.union (explain_borne up1) (explain_borne lo2) in - match r1 with - | [] -> step (r1, l2) acc (Ex.union nexpl expl) - | (lor1,upr1)::rr1 -> - let lor1 = add_expl_to_borne lor1 nexpl in - let r1 = (lor1,upr1)::rr1 in - step (r1, l2) acc expl - else if clu > 0 then - let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in - match r2 with - | [] -> step (l1, r2) acc (Ex.union nexpl expl) - | (lor2,upr2)::rr2 -> - let lor2 = add_expl_to_borne lor2 nexpl in - let r2 = (lor2,upr2)::rr2 in - step (l1, r2) acc expl - else if cll = 0 && cuu = 0 then - step (r1, r2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu >= 0 then - step (l1, r2) ((lo2,up2)::acc) expl - else if cll >= 0 && cuu <= 0 then - step (r1, l2) ((lo1,up1)::acc) expl - else if cll <= 0 && cuu <= 0 && cul >= 0 then - step (r1, l2) ((lo2,up1)::acc) expl - else if cll >= 0 && cuu >= 0 && clu <= 0 then - step (l1, r2) ((lo1,up2)::acc) expl - else assert false - | [], _ | _, [] -> List.rev acc, expl - in + | (lo1,up1)::r1, (lo2,up2)::r2 -> + let (lo1,up1), (lo2,up2) = + if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2) + else (lo1,up1), (lo2,up2) in + let cll = compare_bl_bl lo1 lo2 in + let cuu = compare_bu_bu up1 up2 in + let clu = compare_bl_bu lo1 up2 in + let cul = compare_bu_bl up1 lo2 in + if cul < 0 then + let nexpl = Ex.union (explain_borne up1) (explain_borne lo2) in + match r1 with + | [] -> step (r1, l2) acc (Ex.union nexpl expl) + | (lor1,upr1)::rr1 -> + let lor1 = add_expl_to_borne lor1 nexpl in + let r1 = (lor1,upr1)::rr1 in + step (r1, l2) acc expl + else if clu > 0 then + let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in + match r2 with + | [] -> step (l1, r2) acc (Ex.union nexpl expl) + | (lor2,upr2)::rr2 -> + let lor2 = add_expl_to_borne lor2 nexpl in + let r2 = (lor2,upr2)::rr2 in + step (l1, r2) acc expl + else if cll = 0 && cuu = 0 then + step (r1, r2) ((lo1,up1)::acc) expl + else if cll <= 0 && cuu >= 0 then + step (l1, r2) ((lo2,up2)::acc) expl + else if cll >= 0 && cuu <= 0 then + step (r1, l2) ((lo1,up1)::acc) expl + else if cll <= 0 && cuu <= 0 && cul >= 0 then + step (r1, l2) ((lo2,up1)::acc) expl + else if cll >= 0 && cuu >= 0 && clu <= 0 then + step (l1, r2) ((lo1,up2)::acc) expl + else assert false + | [], _ | _, [] -> List.rev acc, expl + in let l, expl = step (l1,l2) [] (Ex.union e1 e2) in if l = [] then raise (NotConsistent expl) else { uints1 with ints = l; expl = expl } @@ -498,20 +498,20 @@ let new_borne_inf expl b ~is_le uints = let complement ({ints=l; expl=e} as uints) = let rec step l prev acc = match l with - | (b1,b2)::r -> - let bu = match b1 with - | Strict v -> Large v - | Large v -> Strict v - | _ -> b1 in - let bl = match b2 with - | Strict v -> Large v - | Large v -> Strict v - | _ -> b2 in - if bu = Minfty then step r bl acc - else step r bl ((prev, bu)::acc) - | [] -> - if prev = Pinfty then List.rev acc - else List.rev ((prev, Pinfty)::acc) + | (b1,b2)::r -> + let bu = match b1 with + | Strict v -> Large v + | Large v -> Strict v + | _ -> b1 in + let bl = match b2 with + | Strict v -> Large v + | Large v -> Strict v + | _ -> b2 in + if bu = Minfty then step r bl acc + else step r bl ((prev, bu)::acc) + | [] -> + if prev = Pinfty then List.rev acc + else List.rev ((prev, Pinfty)::acc) in { uints with ints = step l Minfty [] } @@ -523,15 +523,15 @@ let mult u1 u2 = let resl, expl = List.fold_left (fun (l', expl) b1 -> - List.fold_left - (fun (l, ex) b2 -> - let bl, bu, ex' = mult_bornes b1 b2 in - (bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints) + List.fold_left + (fun (l, ex) b2 -> + let bl, bu, ex' = mult_bornes b1 b2 in + (bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints) ([], Ex.empty) u1.ints in union { ints=resl; is_int = u1.is_int; - expl = Ex.union expl - (Ex.union u1.expl u2.expl) } + expl = Ex.union expl + (Ex.union u1.expl u2.expl) } let power n u = let l = List.map (power_bornes n) u.ints in @@ -571,37 +571,37 @@ let root_exces_num a n = let root_default_borne is_int x n = match x with - | Pinfty -> Pinfty - | Minfty -> Minfty - | Large (v, e) | Strict (v, e) -> - let s = if v >=/ (Int 0) then root_default_num v n - else (minus_num (root_exces_num (minus_num v) n)) in - if is_int then - let cs = ceiling_num s in - let cs2 = cs **/ (Int n) in - if v <=/ cs2 then Large (cs, e) - else Large (cs +/ (Int 1), e) - else Large (s, e) + | Pinfty -> Pinfty + | Minfty -> Minfty + | Large (v, e) | Strict (v, e) -> + let s = if v >=/ (Int 0) then root_default_num v n + else (minus_num (root_exces_num (minus_num v) n)) in + if is_int then + let cs = ceiling_num s in + let cs2 = cs **/ (Int n) in + if v <=/ cs2 then Large (cs, e) + else Large (cs +/ (Int 1), e) + else Large (s, e) let root_exces_borne is_int x n = match x with - | Pinfty -> Pinfty - | Minfty -> Minfty - | Large (v, e) | Strict (v, e) -> - let s = if v >=/ (Int 0) then root_exces_num v n - else (minus_num (root_default_num (minus_num v) n)) in - if is_int then - let cs = floor_num s in - let cs2 = cs **/ (Int n) in - if v >=/ cs2 then Large (cs, e) - else Large (cs -/ (Int 1), e) - else Large (s, e) + | Pinfty -> Pinfty + | Minfty -> Minfty + | Large (v, e) | Strict (v, e) -> + let s = if v >=/ (Int 0) then root_exces_num v n + else (minus_num (root_default_num (minus_num v) n)) in + if is_int then + let cs = floor_num s in + let cs2 = cs **/ (Int n) in + if v >=/ cs2 then Large (cs, e) + else Large (cs -/ (Int 1), e) + else Large (s, e) let sqrt_interval is_int (b1,b2) = let l1, u1 = (minus_borne (root_exces_borne is_int b2 2), - minus_borne (root_default_borne is_int b1 2)) in + minus_borne (root_default_borne is_int b1 2)) in let l2, u2 = (root_default_borne is_int b1 2, - root_exces_borne is_int b2 2) in + root_exces_borne is_int b2 2) in if compare_bornes l1 u1 > 0 then if compare_bornes l2 u2 > 0 then [] else [l2,u2] @@ -616,7 +616,7 @@ let sqrt {ints = l; is_int = is_int; expl = e } = let l = List.fold_left (fun l' bs -> - (sqrt_interval is_int bs)@l' + (sqrt_interval is_int bs)@l' ) [] l in union { ints = l; is_int = is_int; expl = e } @@ -625,9 +625,9 @@ let rec root n ({ints = l; is_int = is_int; expl = e} as u) = else let l = List.fold_left - (fun l' bs -> - (root_interval is_int bs n)@l' - ) [] l in + (fun l' bs -> + (root_interval is_int bs n)@l' + ) [] l in union { ints = l; is_int = is_int; expl = e } let finite_size {ints = l; is_int = is_int} = @@ -635,16 +635,16 @@ let finite_size {ints = l; is_int = is_int} = else try let n = - List.fold_left - (fun n (b1,b2) -> - match b1, b2 with - | Minfty, _ | _, Pinfty -> raise Exit - | Large (v1, _) , Large (v2, _) -> n +/ (v2 -/ v1 +/ (Int 1)) - | _, _ -> assert false - ) (Int 0) l in + List.fold_left + (fun n (b1,b2) -> + match b1, b2 with + | Minfty, _ | _, Pinfty -> raise Exit + | Large (v1, _) , Large (v2, _) -> n +/ (v2 -/ v1 +/ (Int 1)) + | _, _ -> assert false + ) (Int 0) l in Some n with Exit -> None - + let borne_inf = function | {ints = (Large (v, ex), _)::_} -> v, ex | _ -> invalid_arg "Intervals.borne_inf : No finite lower bound" @@ -653,23 +653,23 @@ let borne_inf = function let inv_borne_inf b is_int ~other = match b with - | Pinfty -> assert false - | Minfty -> - if is_int then Large (Int 0, explain_borne other) - else Strict (Int 0, explain_borne other) - | Strict (Int 0, e) | Large (Int 0, e) -> Pinfty - | Strict (v, e) -> Strict (Int 1 // v, e) - | Large (v, e) -> Large (Int 1 // v, e) + | Pinfty -> assert false + | Minfty -> + if is_int then Large (Int 0, explain_borne other) + else Strict (Int 0, explain_borne other) + | Strict (Int 0, e) | Large (Int 0, e) -> Pinfty + | Strict (v, e) -> Strict (Int 1 // v, e) + | Large (v, e) -> Large (Int 1 // v, e) let inv_borne_sup b is_int ~other = match b with - | Minfty -> assert false - | Pinfty -> - if is_int then Large (Int 0, explain_borne other) - else Strict (Int 0, explain_borne other) - | Strict (Int 0, e) | Large (Int 0, e) -> Minfty - | Strict (v, e) -> Strict (Int 1 // v, e) - | Large (v, e) -> Large (Int 1 // v, e) + | Minfty -> assert false + | Pinfty -> + if is_int then Large (Int 0, explain_borne other) + else Strict (Int 0, explain_borne other) + | Strict (Int 0, e) | Large (Int 0, e) -> Minfty + | Strict (v, e) -> Strict (Int 1 // v, e) + | Large (v, e) -> Large (Int 1 // v, e) let inv_bornes (l, u) is_int = inv_borne_sup u is_int ~other:l, inv_borne_inf l is_int ~other:u @@ -678,12 +678,12 @@ let inv_bornes (l, u) is_int = let inv ({ints=l; is_int=is_int} as u) = try let l' = List.fold_left - (fun acc (l,u) -> - if (pos_borne_strict l && pos_borne_strict u) - || (neg_borne_strict l && neg_borne_strict u) then - (inv_bornes (l, u) is_int) :: acc - else raise Exit - ) [] l in + (fun acc (l,u) -> + if (pos_borne_strict l && pos_borne_strict u) + || (neg_borne_strict l && neg_borne_strict u) then + (inv_bornes (l, u) is_int) :: acc + else raise Exit + ) [] l in union { u with ints=l' } with Exit -> { u with ints = [Minfty, Pinfty] } @@ -698,6 +698,6 @@ let div i1 i2 = let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in let l = if is_int then - List.map (fun (l,u) -> int_div_bornes l u) l + List.map (fun (l,u) -> int_div_bornes l u) l else l in { i with ints = l } diff --git a/smt/literal.ml b/smt/literal.ml index 405cea4a..464a5ed7 100644 --- a/smt/literal.ml +++ b/smt/literal.ml @@ -55,35 +55,35 @@ module Make (X : OrderedType) : S with type elt = X.t = struct module V = struct type t = X.t view - + let equal a1 a2 = match a1, a2 with - | Eq(t1, t2), Eq(u1, u2) -> - (X.compare t1 u1 = 0 && X.compare t2 u2 = 0) || - (X.compare t1 u2 = 0 && X.compare t2 u1 = 0) - | Distinct (b1,lt1), Distinct (b2,lt2) -> - (try - b1 = b2 && - List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2 - with Invalid_argument _ -> false) - | Builtin(b1, n1, l1), Builtin(b2, n2, l2) -> - (try - b1 = b2 && Hstring.equal n1 n2 - && - List.for_all2 (fun x y -> X.compare x y = 0) l1 l2 - with Invalid_argument _ -> false) - | _ -> false - + | Eq(t1, t2), Eq(u1, u2) -> + (X.compare t1 u1 = 0 && X.compare t2 u2 = 0) || + (X.compare t1 u2 = 0 && X.compare t2 u1 = 0) + | Distinct (b1,lt1), Distinct (b2,lt2) -> + (try + b1 = b2 && + List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2 + with Invalid_argument _ -> false) + | Builtin(b1, n1, l1), Builtin(b2, n2, l2) -> + (try + b1 = b2 && Hstring.equal n1 n2 + && + List.for_all2 (fun x y -> X.compare x y = 0) l1 l2 + with Invalid_argument _ -> false) + | _ -> false + let hash a = match a with | Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2)) | Distinct (b,lt) -> - let x = if b then 7 else 23 in - abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt) + let x = if b then 7 else 23 in + abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt) | Builtin(b, n, l) -> - let x = if b then 7 else 23 in - abs - (List.fold_left - (fun acc t-> acc*13 + X.hash t) (Hstring.hash n+x) l) + let x = if b then 7 else 23 in + abs + (List.fold_left + (fun acc t-> acc*13 + X.hash t) (Hstring.hash n+x) l) end module H = Make_consed(V) @@ -122,8 +122,8 @@ module Make (X : OrderedType) : S with type elt = X.t = struct let print_list fmt = function | [] -> () | z :: l -> - Format.fprintf fmt "%a" X.print z; - List.iter (Format.fprintf fmt ", %a" X.print) l + Format.fprintf fmt "%a" X.print z; + List.iter (Format.fprintf fmt ", %a" X.print) l let ale = Hstring.make "<=" let alt = Hstring.make "<" @@ -132,30 +132,30 @@ module Make (X : OrderedType) : S with type elt = X.t = struct let lbl = Hstring.view (label a) in let lbl = if lbl = "" then lbl else lbl^":" in match view a with - | Eq (z1, z2) -> - if equal z1 z2 then Format.fprintf fmt "True" - else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2 - | Distinct (b,(z::l)) -> - let b = if b then "~" else "" in - Format.fprintf fmt "%s%s%a" lbl b X.print z; - List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l + | Eq (z1, z2) -> + if equal z1 z2 then Format.fprintf fmt "True" + else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2 + | Distinct (b,(z::l)) -> + let b = if b then "~" else "" in + Format.fprintf fmt "%s%s%a" lbl b X.print z; + List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l - | Builtin (true, n, [v1;v2]) when Hstring.equal n ale -> - Format.fprintf fmt "%s %a <= %a" lbl X.print v1 X.print v2 + | Builtin (true, n, [v1;v2]) when Hstring.equal n ale -> + Format.fprintf fmt "%s %a <= %a" lbl X.print v1 X.print v2 - | Builtin (true, n, [v1;v2]) when Hstring.equal n alt -> - Format.fprintf fmt "%s %a < %a" lbl X.print v1 X.print v2 + | Builtin (true, n, [v1;v2]) when Hstring.equal n alt -> + Format.fprintf fmt "%s %a < %a" lbl X.print v1 X.print v2 - | Builtin (false, n, [v1;v2]) when Hstring.equal n ale -> - Format.fprintf fmt "%s %a > %a" lbl X.print v1 X.print v2 + | Builtin (false, n, [v1;v2]) when Hstring.equal n ale -> + Format.fprintf fmt "%s %a > %a" lbl X.print v1 X.print v2 - | Builtin (false, n, [v1;v2]) when Hstring.equal n alt -> - Format.fprintf fmt "%s %a >= %a" lbl X.print v1 X.print v2 + | Builtin (false, n, [v1;v2]) when Hstring.equal n alt -> + Format.fprintf fmt "%s %a >= %a" lbl X.print v1 X.print v2 - | Builtin (b, n, l) -> - let b = if b then "" else "~" in - Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view n) print_list l - | _ -> assert false + | Builtin (b, n, l) -> + let b = if b then "" else "~" in + Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view n) print_list l + | _ -> assert false module Set = Set.Make(T) module Map = Map.Make(T) @@ -171,10 +171,10 @@ module type S_Term = sig val true_ : t val false_ : t -(* val terms_of : t -> Term.Set.t - val vars_of : t -> Symbols.Set.t -*) -(* module SetEq : Set.S with type elt = t * Term.t * Term.t*) + (* val terms_of : t -> Term.Set.t + val vars_of : t -> Symbols.Set.t + *) + (* module SetEq : Set.S with type elt = t * Term.t * Term.t*) end module LT : S_Term = struct @@ -194,17 +194,17 @@ module LT : S_Term = struct make (Eq (t1, Term.false_)) | _ -> L.neg a -(* let terms_of a = - let l = match view a with - | Eq (t1, t2) -> [t1; t2] - | Distinct (_, l) | Builtin (_, _, l) -> l - in - List.fold_left Term.subterms Term.Set.empty l -*) + (* let terms_of a = + let l = match view a with + | Eq (t1, t2) -> [t1; t2] + | Distinct (_, l) | Builtin (_, _, l) -> l + in + List.fold_left Term.subterms Term.Set.empty l + *) - module SS = Symbols.Set -(* let vars_of a = - Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty -*) + 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/polynome.ml b/smt/polynome.ml index f3e3fde1..05bc97ec 100644 --- a/smt/polynome.ml +++ b/smt/polynome.ml @@ -84,13 +84,13 @@ module Make (X : S) = struct | Int 1 -> "+", "", "" | Int -1 -> "-", "", "" | n -> - if n >/ Int 0 then "+", string_of_num n, "*" - else "-", string_of_num (minus_num n), "*" + if n >/ Int 0 then "+", string_of_num n, "*" + else "-", string_of_num (minus_num n), "*" in fprintf fmt "%s%s%s%a" s n op X.print x )p.m; let s, n = if p.c >=/ Int 0 then "+", string_of_num p.c - else "-", string_of_num (minus_num p.c) in + else "-", string_of_num (minus_num p.c) in fprintf fmt "%s%s" s n @@ -107,19 +107,19 @@ module Make (X : S) = struct 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 + (fun m (n, x) -> + let n' = n +/ (find x m) in + if n' =/ (Int 0) then M.remove x m else M.add x n' m) M.empty l in { m = m; c = c; ty = ty } let add p1 p2 = let m = M.fold - (fun x a m -> - let a' = (find x m) +/ a in - if a' =/ (Int 0) then M.remove x m else M.add x a' m) - p2.m p1.m + (fun x a m -> + let a' = (find x m) +/ a in + if a' =/ (Int 0) then M.remove x m else M.add x a' m) + p2.m p1.m in { m = m; c = p1.c +/ p2.c; ty = p1.ty } @@ -132,7 +132,7 @@ module Make (X : S) = struct let acx = mult_const p.c ax in let m = M.fold - (fun xi ai m -> M.add (X.mult x xi) (a */ ai) m) p.m acx.m + (fun xi ai m -> M.add (X.mult x xi) (a */ ai) m) p.m acx.m in { acx with m = m} @@ -149,11 +149,11 @@ module Make (X : S) = struct else let p = mult_const ((Int 1) // p2.c) p1 in match M.is_empty p.m, p.ty with - | true, Ty.Tint -> {p with c = floor_num p.c}, false - | true, Ty.Treal -> p, false - | false, Ty.Tint -> p, true - | false, Ty.Treal -> p, false - | _ -> assert false + | true, Ty.Tint -> {p with c = floor_num p.c}, false + | true, Ty.Treal -> p, false + | false, Ty.Tint -> p, true + | false, Ty.Treal -> p, false + | _ -> assert false else raise Maybe_zero @@ -161,8 +161,8 @@ module Make (X : S) = struct if M.is_empty p2.m then if p2.c =/ Int 0 then raise Division_by_zero else - if M.is_empty p1.m then { p1 with c = mod_num p1.c p2.c } - else raise Not_a_num + 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 @@ -173,9 +173,9 @@ module Make (X : S) = struct let tn= ref None in (*version I : prend le premier element de la table*) (try M.iter - (fun x a -> tn := Some (a, x); raise Exit) p.m with Exit -> ()); + (fun x a -> tn := Some (a, x); raise Exit) p.m with Exit -> ()); (*version II : prend le dernier element de la table i.e. le plus grand - M.iter (fun x a -> tn := Some (a, x)) p.m;*) + M.iter (fun x a -> tn := Some (a, x)) p.m;*) match !tn with Some p -> p | _ -> raise Not_found let subst x p1 p2 = @@ -195,11 +195,11 @@ module Make (X : S) = struct let is_monomial p = try M.fold - (fun x a r -> - match r with - | None -> Some (a, x, p.c) - | _ -> raise Exit) - p.m None + (fun x a r -> + match r with + | None -> Some (a, x, p.c) + | _ -> raise Exit) + p.m None with Exit -> None let denominator = function diff --git a/smt/polynome.mli b/smt/polynome.mli index 36d32c35..8c171659 100644 --- a/smt/polynome.mli +++ b/smt/polynome.mli @@ -65,4 +65,4 @@ module type T = sig end module Make (X : S) : T with type r = X.r - + diff --git a/smt/sig.mli b/smt/sig.mli index 9bd0fd56..7f173abc 100644 --- a/smt/sig.mli +++ b/smt/sig.mli @@ -16,7 +16,7 @@ type answer = Yes of Explanation.t | No type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t type 'a input = - 'a Literal.view * Literal.LT.t option * Explanation.t + 'a Literal.view * Literal.LT.t option * Explanation.t type 'a result = { assume : ('a literal * Explanation.t) list; @@ -34,10 +34,10 @@ module type RELATION = sig 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 *) + (** case_split env returns a list of equalities *) val add : t -> r -> t - (** add a representant to take into account *) + (** add a representant to take into account *) end diff --git a/smt/smt.ml b/smt/smt.ml index 24376c7d..75bcb2fd 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -64,18 +64,18 @@ module Type = struct 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 + | [] -> + H.add decl_types t (Ty.Tabstract t) + | _ -> + let ty = Ty.Tsum (t, constrs) in + H.add decl_types t ty; + List.iter (fun c -> declare_constructor t c) constrs let all_constructors () = H.fold (fun _ c acc -> match c with - | Symbols.Name (h, Symbols.Constructor), _, _ -> h :: acc - | _ -> acc - ) decl_symbs [htrue; hfalse] + | Symbols.Name (h, Symbols.Constructor), _, _ -> h :: acc + | _ -> acc + ) decl_symbs [htrue; hfalse] let constructors ty = if Hstring.equal ty type_bool then [htrue; hfalse] @@ -93,7 +93,7 @@ module Symbol = struct if H.mem decl_symbs f then raise (Error (DuplicateTypeName f)); List.iter (fun t -> - if not (H.mem decl_types t) then raise (Error (UnknownType t)) ) + if not (H.mem decl_types t) then raise (Error (UnknownType t)) ) (ret::args); H.add decl_symbs f (Symbols.name f, args, ret) @@ -104,22 +104,22 @@ module Symbol = struct if not res then begin eprintf "Not declared : %a in@." Hstring.print s; H.iter (fun hs (sy, _, _) -> - eprintf "%a (=?%b) -> %a@." Hstring.print hs - (Hstring.compare hs s = 0) - Symbols.print sy) - decl_symbs; - end; - res + eprintf "%a (=?%b) -> %a@." Hstring.print hs + (Hstring.compare hs s = 0) + Symbols.print sy) + decl_symbs; + end; + res let not_builtin ty = Hstring.equal ty Type.type_proc || - not (Hstring.equal ty Type.type_int || Hstring.equal ty Type.type_real || - Hstring.equal ty Type.type_bool || Hstring.equal ty Type.type_proc) + 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 + | Ty.Tabstract _ -> true + | _ -> false let has_type_proc s = Hstring.equal (snd (type_of s)) Type.type_proc @@ -147,27 +147,27 @@ module Variant = struct let assign_var x y = if not (Hstring.equal x y) then add assignments x y - + let rec compute () = let flag = ref false in let visited = ref HSet.empty in let rec dfs x s = if not (HSet.mem x !visited) then - begin - visited := HSet.add x !visited; - HSet.iter - (fun y -> - let c_x = find constructors x in - let c_y = find constructors y in - let c = HSet.union c_x c_y in - if not (HSet.equal c c_x) then - begin - H.replace constructors x c; - flag := true - end; - dfs y (find assignments y) - ) s - end + begin + visited := HSet.add x !visited; + HSet.iter + (fun y -> + let c_x = find constructors x in + let c_y = find constructors y in + let c = HSet.union c_x c_y in + if not (HSet.equal c c_x) then + begin + H.replace constructors x c; + flag := true + end; + dfs y (find assignments y) + ) s + end in H.iter dfs assignments; if !flag then compute () @@ -176,12 +176,12 @@ module Variant = struct HSet.iter (fun c -> Format.eprintf "%a, " Hstring.print c) s let print () = - H.iter - (fun x c -> - Format.eprintf "%a = {%a}@." Hstring.print x hset_print c) - constructors - - + 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 @@ -190,12 +190,12 @@ module Variant = struct compute (); List.iter (fun (x, nty) -> - if not (H.mem constructors x) then - let ty = H.find decl_types nty in - match ty with - | Ty.Tsum (_, l) -> - H.add constructors x (set_of_list l) - | _ -> ()) l; + if not (H.mem constructors x) then + let ty = H.find decl_types nty in + match ty with + | Ty.Tsum (_, l) -> + H.add constructors x (set_of_list l) + | _ -> ()) l; H.clear assignments let update_decl_types s = @@ -203,9 +203,9 @@ module Variant = struct let l = ref [] in HSet.iter (fun x -> - l := x :: !l; - let vx = Hstring.view x in - nty := if !nty = "" then vx else !nty ^ "|" ^ vx) s; + 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; @@ -215,9 +215,9 @@ module Variant = struct compute (); H.iter (fun x s -> - let nty = update_decl_types s in - let sy, args, _ = H.find decl_symbs x in - H.replace decl_symbs x (sy, args, nty)) + 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 @@ -288,11 +288,11 @@ end let make_arith op t1 t2 = let op = match op with - | Plus -> Symbols.Plus - | Minus -> Symbols.Minus - | Mult -> Symbols.Mult - | Div -> Symbols.Div - | Modulo -> Symbols.Modulo + | Plus -> Symbols.Plus + | Minus -> Symbols.Minus + | Mult -> Symbols.Mult + | Div -> Symbols.Div + | Modulo -> Symbols.Modulo in let ty = if is_int t1 && is_int t2 then Ty.Tint @@ -352,14 +352,14 @@ end let rec print fmt phi = match phi with - | Lit a -> Literal.LT.print fmt a - | Comb (Not, [f]) -> - fprintf fmt "not (%a)" print f - | Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l - | Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l - | Comb (Imp, [f1; f2]) -> - fprintf fmt "(%a => %a)" print f1 print f2 - | _ -> assert false + | Lit a -> Literal.LT.print fmt a + | Comb (Not, [f]) -> + fprintf fmt "not (%a)" print f + | Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l + | Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l + | Comb (Imp, [f1; f2]) -> + fprintf fmt "(%a => %a)" print f1 print f2 + | _ -> assert false and print_list sep fmt = function | [] -> () | [f] -> print fmt f @@ -379,46 +379,46 @@ end try let left, (c, t1, t2), right = Term.first_ite l in begin - match value env c with - | Some true -> - lift_ite (c::env) op (left@(t1::right)) - | Some false -> - lift_ite ((make Not [c])::env) op (left@(t2::right)) - | None -> - Comb - (And, - [Comb - (Imp, [c; lift_ite (c::env) op (left@(t1::right))]); - Comb (Imp, - [(make Not [c]); - lift_ite - ((make Not [c])::env) op (left@(t2::right))])]) + match value env c with + | Some true -> + lift_ite (c::env) op (left@(t1::right)) + | Some false -> + lift_ite ((make Not [c])::env) op (left@(t2::right)) + | None -> + Comb + (And, + [Comb + (Imp, [c; lift_ite (c::env) op (left@(t1::right))]); + Comb (Imp, + [(make Not [c]); + lift_ite + ((make Not [c])::env) op (left@(t2::right))])]) end with Not_found -> begin - let lit = - match op, l with - | Eq, [Term.T t1; Term.T t2] -> - Literal.Eq (t1, t2) - | Neq, ts -> - let ts = - List.rev_map (function Term.T x -> x | _ -> assert false) ts in - Literal.Distinct (false, ts) - | Le, [Term.T t1; Term.T t2] -> - Literal.Builtin (true, Hstring.make "<=", [t1; t2]) - | Lt, [Term.T t1; Term.T t2] -> - Literal.Builtin (true, Hstring.make "<", [t1; t2]) - | _ -> assert false - in - Lit (Literal.LT.make lit) + let lit = + match op, l with + | Eq, [Term.T t1; Term.T t2] -> + Literal.Eq (t1, t2) + | Neq, ts -> + let ts = + List.rev_map (function Term.T x -> x | _ -> assert false) ts in + Literal.Distinct (false, ts) + | Le, [Term.T t1; Term.T t2] -> + Literal.Builtin (true, Hstring.make "<=", [t1; t2]) + | Lt, [Term.T t1; Term.T t2] -> + Literal.Builtin (true, Hstring.make "<", [t1; t2]) + | _ -> assert false + in + Lit (Literal.LT.make lit) end let make_lit op l = lift_ite [] op l let make_pred ?(sign=true) p = if sign - then make_lit Eq [p; Term.t_true] - else make_lit Eq [p; Term.t_false] + then make_lit Eq [p; Term.t_true] + else make_lit Eq [p; Term.t_false] let make_eq t1 t2 = make_lit Eq [t1; t2] let make_neq t1 t2 = make_lit Neq [t1; t2] @@ -438,19 +438,19 @@ end | Comb (Not, [Lit a]) -> Lit (Literal.LT.neg a) | Comb (Not, [Comb (Not, [f])]) -> sform f | Comb (Not, [Comb (Or, l)]) -> - let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in - Comb (And, nl) + let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in + Comb (And, nl) | Comb (Not, [Comb (And, l)]) -> - let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in - Comb (Or, nl) + let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in + Comb (Or, nl) | Comb (Not, [Comb (Imp, [f1; f2])]) -> - Comb (And, [sform f1; sform (Comb (Not, [f2]))]) + Comb (And, [sform f1; sform (Comb (Not, [f2]))]) | Comb (And, l) -> - Comb (And, List.rev_map sform l) + Comb (And, List.rev_map sform l) | Comb (Or, l) -> - Comb (Or, List.rev_map sform l) + Comb (Or, List.rev_map sform l) | Comb (Imp, [f1; f2]) -> - Comb (Or, [sform (Comb (Not, [f1])); sform f2]) + Comb (Or, [sform (Comb (Not, [f1])); sform f2]) | Comb ((Imp | Not), _) -> assert false | Lit _ as f -> f @@ -467,13 +467,13 @@ end let l = if l_or = [] then l_and else - List.rev_map - (fun x -> - match x with - | Lit _ -> Comb (Or, x::l_or) - | Comb (Or, l) -> Comb (Or, l @@ l_or) - | _ -> assert false - ) l_and + List.rev_map + (fun x -> + match x with + | Lit _ -> Comb (Or, x::l_or) + | Comb (Or, l) -> Comb (Or, l @@ l_or) + | _ -> assert false + ) l_and in Comb (And, l) @@ -491,47 +491,47 @@ end let rec cnf f = match f with - | Comb (Or, l) -> - begin - let l = List.rev_map cnf l in - let l_and, l_or = - List.partition (function Comb(And,_) -> true | _ -> false) l in - match l_and with - | [ Comb(And, l_conj) ] -> - let u = flatten_or l_or in - distrib l_conj u + | Comb (Or, l) -> + begin + let l = List.rev_map cnf l in + let l_and, l_or = + List.partition (function Comb(And,_) -> true | _ -> false) l in + match l_and with + | [ Comb(And, l_conj) ] -> + let u = flatten_or l_or in + distrib l_conj u - | Comb(And, l_conj) :: r -> - let u = flatten_or l_or in - cnf (Comb(Or, (distrib l_conj u)::r)) + | Comb(And, l_conj) :: r -> + let u = flatten_or l_or in + cnf (Comb(Or, (distrib l_conj u)::r)) - | _ -> - begin - match flatten_or l_or with - | [] -> assert false - | [r] -> r - | v -> Comb (Or, v) - end - end - | Comb (And, l) -> - Comb (And, List.rev_map cnf l) - | f -> f + | _ -> + begin + match flatten_or l_or with + | [] -> assert false + | [r] -> r + | v -> Comb (Or, v) + end + end + | Comb (And, l) -> + Comb (And, List.rev_map cnf l) + | f -> f let rec mk_cnf = function | Comb (And, l) -> List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l - + | Comb (Or, [f1;f2]) -> let ll1 = mk_cnf f1 in let ll2 = mk_cnf f2 in List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 + (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 | Comb (Or, f1 :: l) -> let ll1 = mk_cnf f1 in let ll2 = mk_cnf (Comb (Or, l)) in List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 + (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 | Lit a -> [[a]] | Comb (Not, [Lit a]) -> [[Literal.LT.neg a]] @@ -540,19 +540,19 @@ end let rec unfold mono f = match f with - | Lit a -> a::mono - | Comb (Not, [Lit a]) -> - (Literal.LT.neg a)::mono - | Comb (Or, l) -> - List.fold_left unfold mono l - | _ -> assert false - + | Lit a -> a::mono + | Comb (Not, [Lit a]) -> + (Literal.LT.neg a)::mono + | Comb (Or, l) -> + List.fold_left unfold mono l + | _ -> assert false + let rec init monos f = match f with - | Comb (And, l) -> - List.fold_left init monos l - | f -> (unfold [] f)::monos - + | Comb (And, l) -> + List.fold_left init monos l + | f -> (unfold [] f)::monos + let make_cnf f = let sfnc = cnf (sform f) in init [] sfnc @@ -561,8 +561,8 @@ end let cpt = ref 0 in fun () -> let t = AETerm.make - (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt)))) - [] Ty.Tbool + (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt)))) + [] Ty.Tbool in incr cpt; Literal.LT.make (Literal.Eq (t, AETerm.true_)) @@ -579,42 +579,42 @@ end | Comb (Not, [Lit a]) -> None, [Literal.LT.neg a] | Comb (And, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | cmb, [a] -> Some And, a :: acc - | Some And, l -> - Some And, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_and := (proxy, l) :: !acc_and; *) - (* proxy :: acc *) - | Some Or, l -> - let proxy = mk_proxy () in - acc_or := (proxy, l) :: !acc_or; - Some And, proxy :: acc - | None, l -> Some And, l @@ acc - | _ -> assert false - ) (None, []) l + List.fold_left + (fun (_, acc) f -> + match cnf f with + | _, [] -> assert false + | cmb, [a] -> Some And, a :: acc + | Some And, l -> + Some And, l @@ acc + (* let proxy = mk_proxy () in *) + (* acc_and := (proxy, l) :: !acc_and; *) + (* proxy :: acc *) + | Some Or, l -> + let proxy = mk_proxy () in + acc_or := (proxy, l) :: !acc_or; + Some And, proxy :: acc + | None, l -> Some And, l @@ acc + | _ -> assert false + ) (None, []) l | Comb (Or, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | cmb, [a] -> Some Or, a :: acc - | Some Or, l -> - Some Or, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_or := (proxy, l) :: !acc_or; *) - (* proxy :: acc *) - | Some And, l -> - let proxy = mk_proxy () in - acc_and := (proxy, l) :: !acc_and; - Some Or, proxy :: acc - | None, l -> Some Or, l @@ acc - | _ -> assert false - ) (None, []) l + List.fold_left + (fun (_, acc) f -> + match cnf f with + | _, [] -> assert false + | cmb, [a] -> Some Or, a :: acc + | Some Or, l -> + Some Or, l @@ acc + (* let proxy = mk_proxy () in *) + (* acc_or := (proxy, l) :: !acc_or; *) + (* proxy :: acc *) + | Some And, l -> + let proxy = mk_proxy () in + acc_and := (proxy, l) :: !acc_and; + Some Or, proxy :: acc + | None, l -> Some Or, l @@ acc + | _ -> assert false + ) (None, []) l | _ -> assert false @@ -629,15 +629,15 @@ end let acc = List.fold_left (fun acc (p,l) -> - proxies := p :: !proxies; - let np = Literal.LT.neg p in - (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]] - also add clauses [p => l1], [p => l2], etc. *) - let cl, acc = - List.fold_left - (fun (cl,acc) a -> (Literal.LT.neg a :: cl), [np; a] :: acc) - ([p],acc) l in - cl :: acc + proxies := p :: !proxies; + let np = Literal.LT.neg p in + (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]] + also add clauses [p => l1], [p => l2], etc. *) + let cl, acc = + List.fold_left + (fun (cl,acc) a -> (Literal.LT.neg a :: cl), [np; a] :: acc) + ([p],acc) l in + cl :: acc )acc !acc_and in (* encore clauses that make proxies in !acc_or equivalent to @@ -645,12 +645,12 @@ end let acc = List.fold_left (fun acc (p,l) -> - proxies := p :: !proxies; - (* add clause [p => l1 | l2 | ... | ln], and add clauses - [l1 => p], [l2 => p], etc. *) - let acc = List.fold_left (fun acc a -> [p; Literal.LT.neg a]::acc) - acc l in - (Literal.LT.neg p :: l) :: acc + proxies := p :: !proxies; + (* add clause [p => l1 | l2 | ... | ln], and add clauses + [l1 => p], [l2 => p], etc. *) + let acc = List.fold_left (fun acc a -> [p; Literal.LT.neg a]::acc) + acc l in + (Literal.LT.neg p :: l) :: acc ) acc !acc_or in acc @@ -662,7 +662,7 @@ end end (* Naive CNF XXX remove??? - let make_cnf f = mk_cnf (sform f) + let make_cnf f = mk_cnf (sform f) *) end @@ -704,8 +704,8 @@ module Make (Dummy : sig end) = struct eprintf "Unsat Core : @."; List.iter (fun c -> - eprintf "%a@." (Formula.print_list "or") - (List.rev_map (fun x -> Formula.Lit x) c)) uc; + eprintf "%a@." (Formula.print_list "or") + (List.rev_map (fun x -> Formula.Lit x) c)) uc; eprintf "@."; try clear (); @@ -714,18 +714,18 @@ module Make (Dummy : sig end) = struct eprintf "Not an unsat core !!!@."; assert false with - | Solver.Unsat _ -> (); - | Solver.Sat -> - eprintf "Sat: Not an unsat core !!!@."; - assert false + | Solver.Unsat _ -> (); + | Solver.Sat -> + eprintf "Sat: Not an unsat core !!!@."; + assert false let export_unsatcore cl = let uc = List.rev_map (fun {Solver_types.atoms=atoms} -> - let l = ref [] in - for i = 0 to Vec.size atoms - 1 do - l := (Vec.get atoms i).Solver_types.lit :: !l - done; - !l) cl + let l = ref [] in + for i = 0 to Vec.size atoms - 1 do + l := (Vec.get atoms i).Solver_types.lit :: !l + done; + !l) cl in (* check_unsatcore uc; *) uc @@ -736,7 +736,7 @@ module Make (Dummy : sig end) = struct let s = List.fold_left (fun s {Solver_types.name = n} -> - try SInt.add (int_of_string n) s with _ -> s) SInt.empty cl + try SInt.add (int_of_string n) s with _ -> s) SInt.empty cl in SInt.elements s @@ -756,20 +756,20 @@ module Make (Dummy : sig end) = struct CSolver.solve (); if profiling then Time.pause () with - | Solver.Sat -> if profiling then Time.pause () - | Solver.Unsat ex -> - if profiling then Time.pause (); - raise (Unsat (export_unsatcore2 ex)) + | Solver.Sat -> if profiling then Time.pause () + | Solver.Unsat ex -> + if profiling then Time.pause (); + raise (Unsat (export_unsatcore2 ex)) type state = CSolver.state let eval t = match t with | Term.T t' -> - let lit = Literal.LT.mk_pred t' in - CSolver.eval lit + let lit = Literal.LT.mk_pred t' in + CSolver.eval lit | Term.Tite _ -> - failwith "cannot evaluate \"if-then-else\" term" + failwith "cannot evaluate \"if-then-else\" term" let save_state = CSolver.save diff --git a/smt/smt.mli b/smt/smt.mli index 9a57b771..bbc04e19 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -83,10 +83,10 @@ module Symbol : sig 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. *) + (** [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. *) + (** [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 @@ -117,17 +117,17 @@ 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 - [cstr] must be in the type of [s] *) + (** [assign_constr s cstr] will add the constraint that the constructor + [cstr] must be in the type of [s] *) val assign_var : Symbol.t -> Symbol.t -> unit - (** [assign_var x y] will add the constraint that the type of [y] is a - subtype of [x] (use this function when [x := y] appear in your - program *) + (** [assign_var x y] will add the constraint that the type of [y] is a + subtype of [x] (use this function when [x := y] appear in your + program *) val print : unit -> unit - (** [print ()] will output the computed refined types on std_err. This - function is here only for debugging purposes. Use it afer [close ()].*) + (** [print ()] will output the computed refined types on std_err. This + function is here only for debugging purposes. Use it afer [close ()].*) val get_variants : Symbol.t -> Hstring.HSet.t (** [get_variants s] returns a set of constructors, which is the refined @@ -261,11 +261,11 @@ module type Solver = sig functor {! Smt.Make}. A typical use of this solver is to do the following :{[ - clear (); - assume f_1; - ... - assume f_n; - check ();]} + clear (); + assume f_1; + ... + assume f_n; + check ();]} *) type state diff --git a/smt/sum.ml b/smt/sum.ml index 83b7755e..15939786 100644 --- a/smt/sum.ml +++ b/smt/sum.ml @@ -63,8 +63,8 @@ module Make(X : ALIEN) = struct let embed r = match X.extract r with - | Some c -> c - | None -> Alien r + | Some c -> c + | None -> Alien r let is_mine = function | Alien r -> r @@ -72,12 +72,12 @@ module Make(X : ALIEN) = struct let compare c1 c2 = match c1 , c2 with - | Cons (h1,ty1) , Cons (h2,ty2) -> - let n = Hs.compare h1 h2 in - if n <> 0 then n else Ty.compare ty1 ty2 - | Alien r1, Alien r2 -> X.compare r1 r2 - | Alien _ , Cons _ -> 1 - | Cons _ , Alien _ -> -1 + | 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 @@ -90,21 +90,21 @@ module Make(X : ALIEN) = struct if X.equal p cr then v else match c with - | Cons(hs,t) -> cr - | Alien r -> X.subst p v r + | 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)), [] + is_mine (Cons(hs,ty)), [] | _ -> assert false let solve a b = match embed a, embed b with - | Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> [] - | Cons(c1,_) , Cons(c2,_) -> raise Unsolvable - | Cons _ , Alien r2 -> [r2,a] - | Alien r1 , Cons _ -> [r1,b] - | Alien _ , Alien _ -> assert false + | Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> [] + | Cons(c1,_) , Cons(c2,_) -> raise Unsolvable + | Cons _ , Alien r2 -> [r2,a] + | Alien r1 , Cons _ -> [r1,b] + | Alien _ , Alien _ -> assert false let term_extract _ = None @@ -126,7 +126,7 @@ module Make(X : ALIEN) = struct let assume bol r1 r2 = () - let print_env env = () + let print_env env = () end @@ -137,70 +137,70 @@ module Make(X : ALIEN) = struct let add_diseq hss sm1 sm2 dep env eqs = match sm1, sm2 with - | Alien r , Cons(h,ty) - | Cons (h,ty), Alien r -> - let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in - let enum = HSS.remove h enum in - let ex = Ex.union ex dep in - if HSS.is_empty enum then raise (Inconsistent ex) - else - let env = MX.add r (enum, ex) env in - if HSS.cardinal enum = 1 then - let h' = HSS.choose enum in - env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs - else env, eqs + | Alien r , Cons(h,ty) + | Cons (h,ty), Alien r -> + let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in + let enum = HSS.remove h enum in + let ex = Ex.union ex dep in + if HSS.is_empty enum then raise (Inconsistent ex) + else + let env = MX.add r (enum, ex) env in + if HSS.cardinal enum = 1 then + let h' = HSS.choose enum in + env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs + else env, eqs - | Alien r1 , Alien r2 -> env, eqs - | _ -> env, eqs + | Alien r1 , Alien r2 -> env, eqs + | _ -> env, eqs let add_eq hss sm1 sm2 dep env eqs = match sm1, sm2 with - | Alien r, Cons(h,ty) | Cons (h,ty), Alien r -> + | Alien r, Cons(h,ty) | Cons (h,ty), Alien r -> - let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in - let ex = Ex.union ex dep in - if not (HSS.mem h enum) then raise (Inconsistent ex); - MX.add r (HSS.singleton h, ex) env, eqs + let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in + let ex = Ex.union ex dep in + if not (HSS.mem h enum) then raise (Inconsistent ex); + MX.add r (HSS.singleton h, ex) env, eqs - | Alien r1, Alien r2 -> + | Alien r1, Alien r2 -> - let enum1,ex1 = try MX.find r1 env with Not_found -> hss, Ex.empty in - let enum2,ex2 = try MX.find r2 env with Not_found -> hss, Ex.empty in - let ex = Ex.union dep (Ex.union ex1 ex2) in - let diff = HSS.inter enum1 enum2 in - if HSS.is_empty diff then raise (Inconsistent ex); - let env = MX.add r1 (diff, ex) env in - let env = MX.add r2 (diff, ex) env in - if HSS.cardinal diff = 1 then - let h' = HSS.choose diff in - let ty = X.type_info r1 in - env, (LSem (A.Eq(r1, is_mine (Cons(h',ty)))), ex)::eqs - else env, eqs + let enum1,ex1 = try MX.find r1 env with Not_found -> hss, Ex.empty in + let enum2,ex2 = try MX.find r2 env with Not_found -> hss, Ex.empty in + let ex = Ex.union dep (Ex.union ex1 ex2) in + let diff = HSS.inter enum1 enum2 in + if HSS.is_empty diff then raise (Inconsistent ex); + let env = MX.add r1 (diff, ex) env in + let env = MX.add r2 (diff, ex) env in + if HSS.cardinal diff = 1 then + let h' = HSS.choose diff in + let ty = X.type_info r1 in + env, (LSem (A.Eq(r1, is_mine (Cons(h',ty)))), ex)::eqs + else env, eqs - | _ -> env, eqs + | _ -> env, eqs let assume env la = let aux bol r1 r2 dep env eqs = function | None -> env, eqs | Some hss -> - Debug.assume bol r1 r2; - if bol then - add_eq hss (embed r1) (embed r2) dep env eqs - else - add_diseq hss (embed r1) (embed r2) dep env eqs + Debug.assume bol r1 r2; + if bol then + add_eq hss (embed r1) (embed r2) dep env eqs + else + add_diseq hss (embed r1) (embed r2) dep env eqs in Debug.print_env env; let env, eqs = - List.fold_left + List.fold_left (fun (env,eqs) -> function | A.Eq(r1,r2), _, ex -> - aux true r1 r2 ex env eqs (values_of r1) - + aux true r1 r2 ex env eqs (values_of r1) + | A.Distinct(false, [r1;r2]), _, ex -> - aux false r1 r2 ex env eqs (values_of r1) - + aux false r1 r2 ex env eqs (values_of r1) + | _ -> env, eqs - + ) (env,[]) la in env, { assume = eqs; remove = [] } @@ -210,19 +210,19 @@ module Make(X : ALIEN) = struct let case_split env = let acc = MX.fold - (fun r (hss, ex) acc -> - let sz = HSS.cardinal hss in - if sz = 1 then acc - else match acc with - | Some (n,r,hs) when n <= sz -> acc - | _ -> Some (sz, r, HSS.choose hss) - ) env None + (fun r (hss, ex) acc -> + let sz = HSS.cardinal hss in + if sz = 1 then acc + else match acc with + | Some (n,r,hs) when n <= sz -> acc + | _ -> Some (sz, r, HSS.choose hss) + ) env None in match acc with - | Some (n,r,hs) -> - let r' = is_mine (Cons(hs,X.type_info r)) in - [A.Eq(r, r'), Ex.empty, Num.Int n] - | None -> [] + | Some (n,r,hs) -> + let r' = is_mine (Cons(hs,X.type_info r)) in + [A.Eq(r, r'), Ex.empty, Num.Int n] + | None -> [] let query env a_ex = @@ -231,8 +231,8 @@ module Make(X : ALIEN) = struct let add env r = match embed r, values_of r with | Alien r, Some hss -> - if MX.mem r env then env else - MX.add r (hss, Ex.empty) env + 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 7402d977..2cd4bdbf 100644 --- a/smt/sum.mli +++ b/smt/sum.mli @@ -21,5 +21,5 @@ module type ALIEN = sig end module Make - (X : ALIEN) : Sig.THEORY with type r = X.r and type t = X.r abstract + (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 62570e36..fba3dfdb 100644 --- a/smt/symbols.ml +++ b/smt/symbols.ml @@ -48,8 +48,8 @@ let compare_kind k1 k2 = match k1, k2 with let compare s1 s2 = match s1, s2 with | Name (n1,k1), Name (n2,k2) -> - let c = compare_kind k1 k2 in - if c = 0 then Hstring.compare n1 n2 else c + let c = compare_kind k1 k2 in + if c = 0 then Hstring.compare n1 n2 else c | Name _, _ -> -1 | _, Name _ -> 1 | Var n1, Var n2 -> Hstring.compare n1 n2 @@ -67,7 +67,7 @@ let hash = function | Name (n,_) -> Hstring.hash n * 19 | Var n (*| Int n*) -> Hstring.hash n * 19 + 1 | s -> Hashtbl.hash s - + let to_string = function | Name (n,_) -> Hstring.view n | Var x -> "*var* "^(Hstring.view x) diff --git a/smt/term.ml b/smt/term.ml index 5c293739..22062c4e 100644 --- a/smt/term.ml +++ b/smt/term.ml @@ -22,15 +22,15 @@ and t = view module H = struct type t = view let equal t1 t2 = try - Sy.equal t1.f t2.f - && List.for_all2 (==) t1.xs t2.xs - && Ty.equal t1.ty t2.ty - with Invalid_argument _ -> false + Sy.equal t1.f t2.f + && List.for_all2 (==) t1.xs t2.xs + && Ty.equal t1.ty t2.ty + with Invalid_argument _ -> false let hash t = abs (List.fold_left - (fun acc x-> acc*19 +x.tag) (Sy.hash t.f + Ty.hash t.ty) - t.xs) + (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 @@ -41,10 +41,10 @@ let view t = t let rec print fmt t = let {f=x; xs=l; ty=ty} = view t in match x, l with - | Sy.Op op, [e1; e2] -> - fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2 - | _, [] -> fprintf fmt "%a" Sy.print x - | _, _ -> fprintf fmt "%a(%a)" Sy.print x print_list l + | Sy.Op op, [e1; e2] -> + fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2 + | _, [] -> fprintf fmt "%a" Sy.print x + | _, _ -> fprintf fmt "%a(%a)" Sy.print x print_list l and print_list fmt = function | [] -> () @@ -54,7 +54,7 @@ and print_list fmt = function let compare t1 t2 = let c = Pervasives.compare t2.tag t1.tag in if c = 0 then c else - match (view t1).f, (view t2).f with + match (view t1).f, (view t2).f with | (Sy.True | Sy.False ), (Sy.True | Sy.False ) -> c | (Sy.True | Sy.False ), _ -> -1 | _, (Sy.True | Sy.False ) -> 1 diff --git a/smt/ty.ml b/smt/ty.ml index 1bcdadf1..922fc047 100644 --- a/smt/ty.ml +++ b/smt/ty.ml @@ -22,37 +22,37 @@ type t = let hash t = match t with - | Tabstract s -> Hstring.hash s - | Tsum (s, l) -> - let h = - List.fold_left - (fun h x -> 13 * h + Hstring.hash x) (Hstring.hash s) l - in - abs h - | _ -> Hashtbl.hash t + | Tabstract s -> Hstring.hash s + | Tsum (s, l) -> + let h = + List.fold_left + (fun h x -> 13 * h + Hstring.hash x) (Hstring.hash s) l + in + abs h + | _ -> Hashtbl.hash t let equal t1 t2 = match t1, t2 with - | Tabstract s1, Tabstract s2 - | Tsum (s1, _), Tsum (s2, _) -> - Hstring.equal s1 s2 - | Tint, Tint | Treal, Treal | Tbool, Tbool -> true - | _ -> false - + | Tabstract s1, Tabstract s2 + | Tsum (s1, _), Tsum (s2, _) -> + Hstring.equal s1 s2 + | Tint, Tint | Treal, Treal | Tbool, Tbool -> true + | _ -> false + let compare t1 t2 = match t1, t2 with - | Tabstract s1, Tabstract s2 -> - Hstring.compare s1 s2 - | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 - | Tsum (s1, _), Tsum(s2, _) -> - Hstring.compare s1 s2 - | Tsum _, _ -> -1 | _ , Tsum _ -> 1 - | t1, t2 -> Pervasives.compare t1 t2 + | Tabstract s1, Tabstract s2 -> + Hstring.compare s1 s2 + | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 + | Tsum (s1, _), Tsum(s2, _) -> + Hstring.compare s1 s2 + | Tsum _, _ -> -1 | _ , Tsum _ -> 1 + | t1, t2 -> Pervasives.compare t1 t2 let print fmt ty = match ty with - | Tint -> fprintf fmt "int" - | Treal -> fprintf fmt "real" - | Tbool -> fprintf fmt "bool" - | Tabstract s -> fprintf fmt "%s" (Hstring.view s) - | Tsum (s, _) -> fprintf fmt "%s" (Hstring.view s) + | Tint -> fprintf fmt "int" + | Treal -> fprintf fmt "real" + | Tbool -> fprintf fmt "bool" + | Tabstract s -> fprintf fmt "%s" (Hstring.view s) + | Tsum (s, _) -> fprintf fmt "%s" (Hstring.view s) diff --git a/smt/uf.ml b/smt/uf.ml index 6162b540..bc4919c6 100644 --- a/smt/uf.ml +++ b/smt/uf.ml @@ -61,12 +61,12 @@ module Make ( R : Sig.X ) = struct module SetR = Set.Make(struct type t = R.r let compare = R.compare end) module SetRR = Set.Make(struct - type t = R.r * R.r - let compare (r1, r1') (r2, r2') = - let c = R.compare r1 r2 in - if c <> 0 then c - else R.compare r1' r2' - end) + type t = R.r * R.r + let compare (r1, r1') (r2, r2') = + let c = R.compare r1 r2 in + if c <> 0 then c + else R.compare r1' r2' + end) type t = { @@ -104,56 +104,56 @@ module Make ( R : Sig.X ) = struct let lookup_by_t t env = try MapR.find (MapT.find t env.make) env.repr with Not_found -> - assert false (*R.make t, Ex.empty*) (* XXXX *) - + assert false (*R.make t, Ex.empty*) (* XXXX *) + let lookup_by_r r env = try MapR.find r env.repr with Not_found -> r, Ex.empty - + let lookup_for_neqs env r = try MapR.find r env.neqs with Not_found -> MapL.empty - + let add_to_classes t r classes = MapR.add r - (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) - classes - + (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) + classes + let update_classes c nc classes = let s1 = try MapR.find c classes with Not_found -> SetT.empty in let s2 = try MapR.find nc classes with Not_found -> SetT.empty in MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) - + let add_to_gamma r c gamma = L.fold_left - (fun gamma x -> - let s = try MapR.find x gamma with Not_found -> SetR.empty in - MapR.add x (SetR.add r s) gamma) gamma (R.leaves c) - + (fun gamma x -> + let s = try MapR.find x gamma with Not_found -> SetR.empty in + MapR.add x (SetR.add r s) gamma) gamma (R.leaves c) + (* r1 = r2 => neqs(r1) \uplus neqs(r2) *) let update_neqs r1 r2 dep env = let nq_r1 = lookup_for_neqs env r1 in let nq_r2 = lookup_for_neqs env r2 in let mapl = - MapL.fold - (fun l1 ex1 mapl -> - try - let ex2 = MapL.find l1 mapl in - let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) - raise (Inconsistent ex) - with Not_found -> - MapL.add l1 (Ex.union ex1 dep) mapl) - nq_r1 nq_r2 + MapL.fold + (fun l1 ex1 mapl -> + try + let ex2 = MapL.find l1 mapl in + let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) + raise (Inconsistent ex) + with Not_found -> + MapL.add l1 (Ex.union ex1 dep) mapl) + nq_r1 nq_r2 in MapR.add r2 mapl (MapR.add r1 mapl env.neqs) let filter_leaves r = L.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) - + let canon_empty st env = SetR.fold - (fun p ((z, ex) as acc) -> - let q, ex_q = lookup_by_r p env in - if R.equal p q then acc else (p,q)::z, Ex.union ex_q ex) - st ([], Ex.empty) + (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 @@ -173,67 +173,67 @@ module Make ( R : Sig.X ) = struct let in_repr = MapR.mem p env.repr in let in_neqs = MapR.mem p env.neqs in { env with - repr = - if in_repr then env.repr - else MapR.add p (p, Ex.empty) env.repr; - classes = - if in_repr then env.classes - else update_classes p p env.classes; - gamma = - if in_repr then env.gamma - else add_to_gamma p p env.gamma ; - neqs = - if in_neqs then env.neqs - else update_neqs p p Ex.empty env } + repr = + if in_repr then env.repr + else MapR.add p (p, Ex.empty) env.repr; + classes = + if in_repr then env.classes + else update_classes p p env.classes; + gamma = + if in_repr then env.gamma + else add_to_gamma p p env.gamma ; + neqs = + if in_neqs then env.neqs + else update_neqs p p Ex.empty env } let init_term env t = let mkr, ctx = R.make t in let rp, ex = normal_form env mkr in { make = MapT.add t mkr env.make; - repr = MapR.add mkr (rp,ex) env.repr; - classes = add_to_classes t rp env.classes; - gamma = add_to_gamma mkr rp env.gamma; - neqs = - if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) - else MapR.add rp MapL.empty env.neqs}, ctx - - + repr = MapR.add mkr (rp,ex) env.repr; + classes = add_to_classes t rp env.classes; + gamma = add_to_gamma mkr rp env.gamma; + neqs = + if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) + else MapR.add rp MapL.empty env.neqs}, ctx + + let update_aux dep set env= SetRR.fold - (fun (rr, nrr) env -> - { env with - neqs = update_neqs rr nrr dep env ; - classes = update_classes rr nrr env.classes}) - set env + (fun (rr, nrr) env -> + { env with + neqs = update_neqs rr nrr dep env ; + classes = update_classes rr nrr env.classes}) + set env let apply_sigma_uf env (p, v, dep) = assert (MapR.mem p env.gamma); let use_p = MapR.find p env.gamma in try - let env, tch, neqs_to_up = SetR.fold - (fun r (env, touched, neqs_to_up) -> - let rr, ex = MapR.find r env.repr in - let nrr = R.subst p v rr in - if R.equal rr nrr then env, touched, neqs_to_up - else - let ex = Ex.union ex dep in - let env = - {env with - repr = MapR.add r (nrr, ex) env.repr; - gamma = add_to_gamma r nrr env.gamma } - in - env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up - ) use_p (env, [], SetRR.empty) in - (* Correction : Do not update neqs twice for the same r *) - update_aux dep neqs_to_up env, tch - + let env, tch, neqs_to_up = SetR.fold + (fun r (env, touched, neqs_to_up) -> + let rr, ex = MapR.find r env.repr in + let nrr = R.subst p v rr in + if R.equal rr nrr then env, touched, neqs_to_up + else + let ex = Ex.union ex dep in + let env = + {env with + repr = MapR.add r (nrr, ex) env.repr; + gamma = add_to_gamma r nrr env.gamma } + in + env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up + ) use_p (env, [], SetRR.empty) in + (* Correction : Do not update neqs twice for the same r *) + update_aux dep neqs_to_up env, tch + with Not_found -> assert false - + let apply_sigma eqs env tch ((p, v, dep) as sigma) = let env = init_leaf env p in let env, touched = apply_sigma_uf env sigma in env, ((p, touched, v) :: tch) - + end let add env t = @@ -257,10 +257,10 @@ module Make ( R : Sig.X ) = struct end else begin - ignore (Env.update_neqs rr1 rr2 dep env); + ignore (Env.update_neqs rr1 rr2 dep env); try R.solve rr1 rr2 - with Unsolvable -> - raise (Inconsistent dep) + with Unsolvable -> + raise (Inconsistent dep) end let rec ac_x eqs env tch = @@ -280,45 +280,45 @@ module Make ( R : Sig.X ) = struct let d = Lit.make (Literal.Distinct (false,rl)) in let env, _, newds = List.fold_left - (fun (env, mapr, newds) r -> - let rr, ex = Env.find_or_normal_form env r in - try - let exr = MapR.find rr mapr in - raise (Inconsistent (Ex.union ex exr)) - with Not_found -> - let uex = Ex.union ex dep in - let mdis = - try MapR.find rr env.neqs with Not_found -> MapL.empty in - let mdis = - try - MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis - with Not_found -> - MapL.add d uex mdis - in - let env = Env.init_leaf env rr in + (fun (env, mapr, newds) r -> + let rr, ex = Env.find_or_normal_form env r in + try + let exr = MapR.find rr mapr in + raise (Inconsistent (Ex.union ex exr)) + with Not_found -> + let uex = Ex.union ex dep in + let mdis = + try MapR.find rr env.neqs with Not_found -> MapL.empty in + let mdis = + try + MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis + with Not_found -> + MapL.add d uex mdis + in + let env = Env.init_leaf env rr in let env = {env with neqs = MapR.add rr mdis env.neqs} in env, MapR.add rr uex mapr, (rr, ex, mapr)::newds - ) - (env, MapR.empty, []) - rl + ) + (env, MapR.empty, []) + rl in List.fold_left (fun env (r1, ex1, mapr) -> - MapR.fold (fun r2 ex2 env -> - let ex = Ex.union ex1 (Ex.union ex2 dep) in - try match R.solve r1 r2 with - | [a, b] -> - if (R.equal a r1 && R.equal b r2) || - (R.equal a r2 && R.equal b r1) then env - else - distinct env [a; b] ex - | [] -> - raise (Inconsistent ex) - | _ -> env - with Unsolvable -> env) mapr env) + MapR.fold (fun r2 ex2 env -> + let ex = Ex.union ex1 (Ex.union ex2 dep) in + try match R.solve r1 r2 with + | [a, b] -> + if (R.equal a r1 && R.equal b r2) || + (R.equal a r2 && R.equal b r1) then env + else + distinct env [a; b] ex + | [] -> + raise (Inconsistent ex) + | _ -> env + with Unsolvable -> env) mapr env) env newds - + let are_equal env t1 t2 = let r1, ex_r1 = Env.lookup_by_t t1 env in let r2, ex_r2 = Env.lookup_by_t t2 env in @@ -336,9 +336,9 @@ module Make ( R : Sig.X ) = struct let d = Lit.make (Literal.Distinct (false,lr)) in try List.iter (fun r -> - let mdis = MapR.find r env.neqs in - ignore (MapL.find d mdis) - ) lr; + let mdis = MapR.find r env.neqs in + ignore (MapL.find d mdis) + ) lr; true with Not_found -> false diff --git a/smt/use.ml b/smt/use.ml index 0f61d70e..69d39f0f 100644 --- a/smt/use.ml +++ b/smt/use.ml @@ -20,9 +20,9 @@ module ST = T.Set (* module SA = Literal.LT.Set *) module SA = Set.Make(struct - type t = Literal.LT.t * Explanation.t - let compare (s1,_) (s2,_) = Literal.LT.compare s1 s2 -end) + type t = Literal.LT.t * Explanation.t + let compare (s1,_) (s2,_) = Literal.LT.compare s1 s2 + end) type elt = ST.t * SA.t @@ -46,19 +46,19 @@ module Make (X : Sig.X) = struct let add_term k t mp = let g_t,g_a = find k mp in add k (ST.add t g_t,g_a) mp - + let up_add g t rt lvs = let g = if mem rt g then g else add rt (ST.empty, SA.empty) g in L.fold_left (fun g x -> add_term x t g) g lvs let congr_add g lvs = match lvs with - [] -> ST.empty - | x::ls -> - L.fold_left - (fun acc y -> ST.inter (fst(find y g)) acc) - (fst(find x g)) ls - + [] -> ST.empty + | x::ls -> + L.fold_left + (fun acc y -> ST.inter (fst(find y g)) acc) + (fst(find x g)) ls + let up_close_up g p v = let lvs = leaves v in let g_p = find p g in @@ -66,9 +66,9 @@ module Make (X : Sig.X) = struct let congr_close_up g p touched = let inter = function - [] -> (ST.empty, SA.empty) + [] -> (ST.empty, SA.empty) | rx::l -> - L.fold_left (fun acc x ->inter_tpl acc (find x g))(find rx g) l + L.fold_left (fun acc x ->inter_tpl acc (find x g))(find rx g) l in L.fold_left (fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch))) diff --git a/smt/use.mli b/smt/use.mli index 651db3ab..d6f27b1b 100644 --- a/smt/use.mli +++ b/smt/use.mli @@ -21,18 +21,18 @@ type elt = ST.t * SA.t module Make : functor (X : Sig.X) -> -sig + sig - type t - val empty : t - val find : X.r -> t -> elt - val add : X.r -> elt -> t -> t - val mem : X.r -> t -> bool - val print : t -> unit - val up_add : t -> ST.elt -> X.r -> X.r list -> t + 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 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 + val up_close_up :t -> X.r -> X.r -> t + val congr_close_up : t -> X.r -> X.r list -> elt + end