simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-21 16:56:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Everything has now been properly indented with ocp-indent.

Browse source
This commit is contained in:
Guillaume Bury 2014-10-31 16:40:59 +01:00
parent a00506b95f
commit dc43c28a02
34 changed files with 2944 additions and 2941 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.ocp-indent Normal file
View file

@ -0,0 +1,3 @@
base=2
type=2
max_indent=4

160
common/bitv.ml
View file

@ -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

56
common/hashcons.ml
View file

@ -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}

90
common/hashcons.mli
View file

@ -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)

14
common/heap.ml
View file

@ -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

18
common/hstring.ml
View file

@ -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

62
sat/explanation.ml
View file

@ -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

26
sat/explanation_intf.ml
View file

@ -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

1690
sat/solver.ml
View file

File diff suppressed because it is too large Load diff

24
sat/solver.mli
View file

@ -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

226
sat/solver_types.ml
View file

@ -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)

94
sat/solver_types_intf.ml
View file

@ -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

12
sat/theory_intf.ml
View file

@ -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

232
smt/arith.ml
View file

@ -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 </ Int 0 then
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 </ b // (Int 2) then m else m -/ b
@ -287,22 +287,22 @@ module Make
List.fold_left
(fun (l, sb) (b, y) ->
if X.compare y x > 0 then
let k = X.term_embed (fresh_name ()) in
(b, k) :: l, (y, embed k)::sb
else (b, y) :: l, sb)
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

6
smt/arith.mli
View file

@ -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

420
smt/cc.ml
View file

@ -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 () =

154
smt/combine.ml
View file

@ -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)

832
smt/fm.ml
View file

File diff suppressed because it is too large Load diff

4
smt/fm.mli
View file

@ -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

610
smt/intervals.ml
View file

@ -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' </ 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_inf 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' >/ 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' </ 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_bornes l u =
int_of_borne_inf l, int_of_borne_sup u
@ -441,43 +441,43 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
(* fprintf fmt "intersect %a inter %a@." print uints1 print uints2; *)
let rec step (l1,l2) acc expl =
match l1, l2 with
| (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
| (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 }

118
smt/literal.ml
View file

@ -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

50
smt/polynome.ml
View file

@ -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

2
smt/polynome.mli
View file

@ -65,4 +65,4 @@ module type T = sig
end
module Make (X : S) : T with type r = X.r

6
smt/sig.mli
View file

@ -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

442
smt/smt.ml
View file

@ -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

28
smt/smt.mli
View file

@ -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

148
smt/sum.ml
View file

@ -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

2
smt/sum.mli
View file

@ -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

6
smt/symbols.ml
View file

@ -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)

22
smt/term.ml
View file

@ -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

52
smt/ty.ml
View file

@ -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)

228
smt/uf.ml
View file

@ -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

24
smt/use.ml
View file

@ -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)))

24
smt/use.mli
View file

@ -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