simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Removed trailing whitespaces

Browse source
This commit is contained in:
Guillaume Bury 2014-10-29 14:55:23 +01:00
parent 5610cb4984
commit 13060e348d
39 changed files with 1249 additions and 1249 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
common/heap.ml
View file

@ -21,8 +21,8 @@ end
module type S = sig module type S = sig
type t type t
type elem type elem
val empty : t val empty : t
val pop : t -> elem * t val pop : t -> elem * t
val add : t -> elem list -> t val add : t -> elem list -> t
@ -37,22 +37,22 @@ module Make ( X : OrderType ) = struct
let empty = Empty let empty = Empty
let rec fusion t1 t2 = let rec fusion t1 t2 =
match t1, t2 with match t1, t2 with
| _ , Empty -> t1 | _ , Empty -> t1
| Empty , _ -> t2 | Empty , _ -> t2
| Node (m1, g1, d1), Node (m2, g2, d2) -> | Node (m1, g1, d1), Node (m2, g2, d2) ->
if X.compare m1 m2 <= 0 then Node (m1, d1, fusion g1 t2) if X.compare m1 m2 <= 0 then Node (m1, d1, fusion g1 t2)
else Node (m2, d2, fusion g2 t1) else Node (m2, d2, fusion g2 t1)
let pop = function let pop = function
| Empty -> raise EmptyHeap | Empty -> raise EmptyHeap
| Node(m, g, d) -> m, fusion g d | Node(m, g, d) -> m, fusion g d
let add h l = let add h l =
List.fold_left (fun h x -> fusion (Node(x, Empty, Empty)) h ) h l List.fold_left (fun h x -> fusion (Node(x, Empty, Empty)) h ) h l
let elements h = let elements h =
let rec elements_aux acc = function let rec elements_aux acc = function
| Empty -> acc | Empty -> acc
| Node (m1 ,g1 ,d1) -> elements_aux (m1 :: acc) (fusion g1 d1) | Node (m1 ,g1 ,d1) -> elements_aux (m1 :: acc) (fusion g1 d1)

2
common/heap.mli
View file

@ -21,7 +21,7 @@ end
module type S = sig module type S = sig
type t type t
type elem type elem
val empty : t val empty : t
val pop : t -> elem * t val pop : t -> elem * t

10
common/hstring.ml
View file

@ -13,9 +13,9 @@
open Hashcons open Hashcons
module S = module S =
Hashcons.Make_consed(struct include String Hashcons.Make_consed(struct include String
let hash = Hashtbl.hash let hash = Hashtbl.hash
let equal = (=) end) let equal = (=) end)
module HS = struct module HS = struct
@ -38,7 +38,7 @@ module HS = struct
| [] -> raise Not_found | [] -> raise Not_found
| (y, v) :: l -> if equal x y then v else list_assoc x l | (y, v) :: l -> if equal x y then v else list_assoc x l
let rec list_mem_assoc x = function let rec list_mem_assoc x = function
| [] -> false | [] -> false
| (y, _) :: l -> compare x y = 0 || list_mem_assoc x l | (y, _) :: l -> compare x y = 0 || list_mem_assoc x l
@ -65,7 +65,7 @@ module HS = struct
| [] -> false | [] -> false
| d :: l -> compare_couple c d = 0 || list_mem_couple c l | d :: l -> compare_couple c d = 0 || list_mem_couple c l
let print fmt s = let print fmt s =
Format.fprintf fmt "%s" (view s) Format.fprintf fmt "%s" (view s)
end end

4
common/hstring.mli
View file

@ -14,14 +14,14 @@
(** {b Hash-consed strings} (** {b Hash-consed strings}
Hash-consing is a technique to share values that are structurally Hash-consing is a technique to share values that are structurally
equal. More details on equal. More details on
{{:http://en.wikipedia.org/wiki/Hash_consing} Wikipedia} and {{:http://en.wikipedia.org/wiki/Hash_consing} Wikipedia} and
{{:http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf} here}. {{:http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.pdf} here}.
This module provides an easy way to use hash-consing for strings. This module provides an easy way to use hash-consing for strings.
*) *)
open Hashcons open Hashcons
type t = string hash_consed type t = string hash_consed
(** The type of Hash-consed string *) (** The type of Hash-consed string *)

46
common/iheap.ml
View file

@ -12,27 +12,27 @@
(**************************************************************************) (**************************************************************************)
type t = {heap : int Vec.t; indices : int Vec.t } type t = {heap : int Vec.t; indices : int Vec.t }
let dummy = -100 let dummy = -100
let init sz = let init sz =
{ heap = Vec.init sz (fun i -> i) dummy; { heap = Vec.init sz (fun i -> i) dummy;
indices = Vec.init sz (fun i -> i) dummy} indices = Vec.init sz (fun i -> i) dummy}
let left i = (i lsl 1) + 1 (* i*2 + 1 *) let left i = (i lsl 1) + 1 (* i*2 + 1 *)
let right i = (i + 1) lsl 1 (* (i+1)*2 *) let right i = (i + 1) lsl 1 (* (i+1)*2 *)
let parent i = (i - 1) asr 1 (* (i-1) / 2 *) let parent i = (i - 1) asr 1 (* (i-1) / 2 *)
(* (*
let rec heap_property cmp ({heap=heap} as s) i = let rec heap_property cmp ({heap=heap} as s) i =
i >= (Vec.size heap) || i >= (Vec.size heap) ||
((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
&& heap_property cmp s (left i) && heap_property cmp s (right i)) && heap_property cmp s (left i) && heap_property cmp s (right i))
let heap_property cmp s = heap_property cmp s 1 let heap_property cmp s = heap_property cmp s 1
*) *)
let percolate_up cmp {heap=heap;indices=indices} i = let percolate_up cmp {heap=heap;indices=indices} i =
let x = Vec.get heap i in let x = Vec.get heap i in
let pi = ref (parent i) in let pi = ref (parent i) in
let i = ref i in let i = ref i in
@ -45,7 +45,7 @@ let percolate_up cmp {heap=heap;indices=indices} i =
Vec.set heap !i x; Vec.set heap !i x;
Vec.set indices x !i Vec.set indices x !i
let percolate_down cmp {heap=heap;indices=indices} i = let percolate_down cmp {heap=heap;indices=indices} i =
let x = Vec.get heap i in let x = Vec.get heap i in
let sz = Vec.size heap in let sz = Vec.size heap in
let li = ref (left i) in let li = ref (left i) in
@ -53,9 +53,9 @@ let percolate_down cmp {heap=heap;indices=indices} i =
let i = ref i in let i = ref i in
(try (try
while !li < sz do while !li < sz do
let child = let child =
if !ri < sz && cmp (Vec.get heap !ri) (Vec.get heap !li) then !ri if !ri < sz && cmp (Vec.get heap !ri) (Vec.get heap !li) then !ri
else !li else !li
in in
if not (cmp (Vec.get heap child) x) then raise Exit; if not (cmp (Vec.get heap child) x) then raise Exit;
Vec.set heap !i (Vec.get heap child); Vec.set heap !i (Vec.get heap child);
@ -70,13 +70,13 @@ let percolate_down cmp {heap=heap;indices=indices} i =
let in_heap s n = n < Vec.size s.indices && Vec.get s.indices n >= 0 let in_heap s n = n < Vec.size s.indices && Vec.get s.indices n >= 0
let decrease cmp s n = let decrease cmp s n =
assert (in_heap s n); percolate_up cmp s (Vec.get s.indices n) assert (in_heap s n); percolate_up cmp s (Vec.get s.indices n)
let increase cmp s n = let increase cmp s n =
assert (in_heap s n); percolate_down cmp s (Vec.get s.indices n) assert (in_heap s n); percolate_down cmp s (Vec.get s.indices n)
let filter s filt cmp = let filter s filt cmp =
let j = ref 0 in let j = ref 0 in
let lim = Vec.size s.heap in let lim = Vec.size s.heap in
for i = 0 to lim - 1 do for i = 0 to lim - 1 do
@ -93,36 +93,36 @@ let filter s filt cmp =
done done
let size s = Vec.size s.heap let size s = Vec.size s.heap
let is_empty s = Vec.is_empty s.heap let is_empty s = Vec.is_empty s.heap
let insert cmp s n = let insert cmp s n =
if not (in_heap s n) then if not (in_heap s n) then
begin begin
Vec.set s.indices n (Vec.size s.heap); Vec.set s.indices n (Vec.size s.heap);
Vec.push s.heap n; Vec.push s.heap n;
percolate_up cmp s (Vec.get s.indices n) percolate_up cmp s (Vec.get s.indices n)
end end
let grow_to_by_double s sz = let grow_to_by_double s sz =
Vec.grow_to_by_double s.indices sz; Vec.grow_to_by_double s.indices sz;
Vec.grow_to_by_double s.heap sz Vec.grow_to_by_double s.heap sz
(* (*
let update cmp s n = let update cmp s n =
assert (heap_property cmp s); assert (heap_property cmp s);
begin begin
if in_heap s n then if in_heap s n then
begin begin
percolate_up cmp s (Vec.get s.indices n); percolate_up cmp s (Vec.get s.indices n);
percolate_down cmp s (Vec.get s.indices n) percolate_down cmp s (Vec.get s.indices n)
end end
else insert cmp s n else insert cmp s n
end; end;
assert (heap_property cmp s) assert (heap_property cmp s)
*) *)
let remove_min cmp ({heap=heap; indices=indices} as s) = let remove_min cmp ({heap=heap; indices=indices} as s) =
let x = Vec.get heap 0 in let x = Vec.get heap 0 in
Vec.set heap 0 (Vec.last heap); (*heap.last()*) Vec.set heap 0 (Vec.last heap); (*heap.last()*)
Vec.set indices (Vec.get heap 0) 0; Vec.set indices (Vec.get heap 0) 0;

8
common/timer.ml
View file

@ -14,22 +14,22 @@
module type S = sig module type S = sig
val start : unit -> unit val start : unit -> unit
val pause : unit -> unit val pause : unit -> unit
val get : unit -> float val get : unit -> float
end end
module Make (X : sig end) = struct module Make (X : sig end) = struct
open Unix open Unix
let u = ref 0.0 let u = ref 0.0
let cpt = ref 0.0 let cpt = ref 0.0
let start () = u:=(times()).tms_utime let start () = u:=(times()).tms_utime
let pause () = cpt := !cpt +. ((times()).tms_utime -. !u) let pause () = cpt := !cpt +. ((times()).tms_utime -. !u)
let get () = let get () =
!cpt !cpt
end end

2
common/timer.mli
View file

@ -14,7 +14,7 @@
module type S = sig module type S = sig
val start : unit -> unit val start : unit -> unit
val pause : unit -> unit val pause : unit -> unit
val get : unit -> float val get : unit -> float
end end
module Make (X : sig end) : S module Make (X : sig end) : S

34
common/vec.ml
View file

@ -12,20 +12,20 @@
(**************************************************************************) (**************************************************************************)
type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int } type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
let make capa d = {data = Array.make capa d; sz = 0; dummy = d} let make capa d = {data = Array.make capa d; sz = 0; dummy = d}
let init capa f d = {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} let init capa f d = {data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
let from_array data sz d = {data = data; sz = sz; dummy = d} let from_array data sz d = {data = data; sz = sz; dummy = d}
let from_list l sz d = let from_list l sz d =
let l = ref l in let l = ref l in
let f_init i = match !l with [] -> assert false | e::r -> l := r; e in let f_init i = match !l with [] -> assert false | e::r -> l := r; e in
{data = Array.init sz f_init; sz = sz; dummy = d} {data = Array.init sz f_init; sz = sz; dummy = d}
let clear s = s.sz <- 0 let clear s = s.sz <- 0
let shrink t i = assert (i >= 0 && i<=t.sz); t.sz <- t.sz - i let shrink t i = assert (i >= 0 && i<=t.sz); t.sz <- t.sz - i
let pop t = assert (t.sz >=1); t.sz <- t.sz - 1 let pop t = assert (t.sz >=1); t.sz <- t.sz - 1
@ -34,14 +34,14 @@ let size t = t.sz
let is_empty t = t.sz = 0 let is_empty t = t.sz = 0
let grow_to t new_capa = let grow_to t new_capa =
let data = t.data in let data = t.data in
let capa = Array.length data in let capa = Array.length data in
t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy) t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy)
let grow_to_double_size t = grow_to t (2* Array.length t.data) let grow_to_double_size t = grow_to t (2* Array.length t.data)
let rec grow_to_by_double t new_capa = let rec grow_to_by_double t new_capa =
let data = t.data in let data = t.data in
let capa = ref (Array.length data + 1) in let capa = ref (Array.length data + 1) in
while !capa < new_capa do capa := 2 * !capa done; while !capa < new_capa do capa := 2 * !capa done;
@ -50,35 +50,35 @@ let rec grow_to_by_double t new_capa =
let is_full t = Array.length t.data = t.sz let is_full t = Array.length t.data = t.sz
let push t e = let push t e =
(*Format.eprintf "push; sz = %d et capa=%d@." t.sz (Array.length t.data);*) (*Format.eprintf "push; sz = %d et capa=%d@." t.sz (Array.length t.data);*)
if is_full t then grow_to_double_size t; if is_full t then grow_to_double_size t;
t.data.(t.sz) <- e; t.data.(t.sz) <- e;
t.sz <- t.sz + 1 t.sz <- t.sz + 1
let push_none t = let push_none t =
if is_full t then grow_to_double_size t; if is_full t then grow_to_double_size t;
t.data.(t.sz) <- t.dummy; t.data.(t.sz) <- t.dummy;
t.sz <- t.sz + 1 t.sz <- t.sz + 1
let last t = let last t =
let e = t.data.(t.sz - 1) in let e = t.data.(t.sz - 1) in
assert (not (e == t.dummy)); assert (not (e == t.dummy));
e e
let get t i = let get t i =
assert (i < t.sz); assert (i < t.sz);
let e = t.data.(i) in let e = t.data.(i) in
if e == t.dummy then raise Not_found if e == t.dummy then raise Not_found
else e else e
let set t i v = let set t i v =
t.data.(i) <- v; t.data.(i) <- v;
t.sz <- max t.sz (i + 1) t.sz <- max t.sz (i + 1)
let set_size t sz = t.sz <- sz let set_size t sz = t.sz <- sz
let copy t = let copy t =
let data = t.data in let data = t.data in
let len = Array.length data in let len = Array.length data in
let data = Array.init len (fun i -> data.(i)) in let data = Array.init len (fun i -> data.(i)) in
@ -92,15 +92,15 @@ let move_to t t' =
t'.sz <- t.sz t'.sz <- t.sz
let remove t e = let remove t e =
let j = ref 0 in let j = ref 0 in
while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; while (!j < t.sz && not (t.data.(!j) == e)) do incr j done;
assert (!j < t.sz); assert (!j < t.sz);
for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done; for i = !j to t.sz - 2 do t.data.(i) <- t.data.(i+1) done;
pop t pop t
let fast_remove t e =
let fast_remove t e =
let j = ref 0 in let j = ref 0 in
while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; while (!j < t.sz && not (t.data.(!j) == e)) do incr j done;
assert (!j < t.sz); assert (!j < t.sz);
@ -108,7 +108,7 @@ let fast_remove t e =
pop t pop t
let sort t f = let sort t f =
let sub_arr = Array.sub t.data 0 t.sz in let sub_arr = Array.sub t.data 0 t.sz in
Array.fast_sort f sub_arr; Array.fast_sort f sub_arr;
t.data <- sub_arr t.data <- sub_arr

198
smt/arith.ml
View file

@ -19,7 +19,7 @@ module A = Literal
module Sy = Symbols module Sy = Symbols
module T = Term module T = Term
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = Hstring.make "<" let alt = Hstring.make "<"
let is_le n = Hstring.compare n ale = 0 let is_le n = Hstring.compare n ale = 0
let is_lt n = Hstring.compare n alt = 0 let is_lt n = Hstring.compare n alt = 0
@ -34,7 +34,7 @@ module Type (X:Sig.X) : Polynome.T with type r = X.r = struct
end end
module Make module Make
(X : Sig.X) (X : Sig.X)
(P : Polynome.T with type r = X.r) (P : Polynome.T with type r = X.r)
(C : Sig.C with type t = P.t and type r = X.r) = struct (C : Sig.C with type t = P.t and type r = X.r) = struct
@ -42,56 +42,56 @@ module Make
type t = P.t type t = P.t
type r = P.r type r = P.r
let name = "arith" let name = "arith"
let is_mine_a a = let is_mine_a a =
match A.LT.view a with match A.LT.view a with
| A.Builtin (_,p,_) -> is_le p || is_lt p | A.Builtin (_,p,_) -> is_le p || is_lt p
| _ -> false | _ -> false
let is_mine_symb = function let is_mine_symb = function
| Sy.Int _ | Sy.Real _ | Sy.Int _ | Sy.Real _
| Sy.Op (Sy.Plus | Sy.Minus | Sy.Mult | Sy.Div | Sy.Modulo) -> true | Sy.Op (Sy.Plus | Sy.Minus | Sy.Mult | Sy.Div | Sy.Modulo) -> true
| _ -> false | _ -> false
let is_mine_type p = let is_mine_type p =
let ty = P.type_info p in let ty = P.type_info p in
ty = Ty.Tint || ty = Ty.Treal ty = Ty.Tint || ty = Ty.Treal
let unsolvable _ = false let unsolvable _ = false
let empty_polynome ty = P.create [] (Int 0) ty let empty_polynome ty = P.create [] (Int 0) ty
let is_mine p = match P.is_monomial p with let is_mine p = match P.is_monomial p with
| Some (a,x,b) when a =/ (Int 1) && b =/ (Int 0) -> x | Some (a,x,b) when a =/ (Int 1) && b =/ (Int 0) -> x
| _ -> C.embed p | _ -> C.embed p
let embed r = match C.extract r with let embed r = match C.extract r with
| Some p -> p | Some p -> p
| _ -> P.create [Int 1, r] (Int 0) (X.type_info r) | _ -> P.create [Int 1, r] (Int 0) (X.type_info r)
let check_int exn p = let check_int exn p =
if P.type_info p = Ty.Tint then if P.type_info p = Ty.Tint then
let _, c = P.to_list p in let _, c = P.to_list p in
let ppmc = P.ppmc_denominators p in let ppmc = P.ppmc_denominators p in
if not (is_integer_num (ppmc */ c)) then raise exn if not (is_integer_num (ppmc */ c)) then raise exn
let fresh_string = let fresh_string =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> fun () ->
incr cpt; incr cpt;
"!k" ^ (string_of_int !cpt) "!k" ^ (string_of_int !cpt)
let fresh_name () = let fresh_name () =
T.make (Sy.name (Hstring.make (fresh_string()))) [] Ty.Tint T.make (Sy.name (Hstring.make (fresh_string()))) [] Ty.Tint
(* t1 % t2 = md <-> (* t1 % t2 = md <->
c1. 0 <= md ; c1. 0 <= md ;
c2. md < t2 ; c2. md < t2 ;
c3. exists k. t1 = t2 * k + t ; c3. exists k. t1 = t2 * k + t ;
c4. t2 <> 0 (already checked) *) c4. t2 <> 0 (already checked) *)
let mk_modulo md t1 t2 ctx = let mk_modulo md t1 t2 ctx =
let zero = T.int "0" in let zero = T.int "0" in
let c1 = A.LT.make (A.Builtin(true, ale, [zero; md])) in let c1 = A.LT.make (A.Builtin(true, ale, [zero; md])) in
let c2 = A.LT.make (A.Builtin(true, alt, [md; t2])) in let c2 = A.LT.make (A.Builtin(true, alt, [md; t2])) in
@ -99,9 +99,9 @@ module Make
let t3 = T.make (Sy.Op Sy.Mult) [t2;k] Ty.Tint in let t3 = T.make (Sy.Op Sy.Mult) [t2;k] Ty.Tint in
let t3 = T.make (Sy.Op Sy.Plus) [t3;md] Ty.Tint in let t3 = T.make (Sy.Op Sy.Plus) [t3;md] Ty.Tint in
let c3 = A.LT.make (A.Eq (t1, t3)) in let c3 = A.LT.make (A.Eq (t1, t3)) in
c3 :: c2 :: c1 :: ctx c3 :: c2 :: c1 :: ctx
let mk_euc_division p p2 t1 t2 ctx = let mk_euc_division p p2 t1 t2 ctx =
match P.to_list p2 with match P.to_list p2 with
| [], coef_p2 -> | [], coef_p2 ->
let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in
@ -113,7 +113,7 @@ module Make
let rec mke coef p t ctx = let rec mke coef p t ctx =
let {T.f = sb ; xs = xs; ty = ty} = T.view t in let {T.f = sb ; xs = xs; ty = ty} = T.view t in
match sb, xs with match sb, xs with
| (Sy.Int n | Sy.Real n), _ -> | (Sy.Int n | Sy.Real n), _ ->
let c = coef */ (num_of_string (Hstring.view n)) in let c = coef */ (num_of_string (Hstring.view n)) in
P.add (P.create [] c ty) p, ctx P.add (P.create [] c ty) p, ctx
@ -122,43 +122,43 @@ module Make
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
P.add p (P.mult p1 p2), ctx P.add p (P.mult p1 p2), ctx
| Sy.Op Sy.Div, [t1;t2] -> | Sy.Op Sy.Div, [t1;t2] ->
let p1, ctx = mke coef (empty_polynome ty) t1 ctx in let p1, ctx = mke coef (empty_polynome ty) t1 ctx in
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
let p3, ctx = let p3, ctx =
try try
let p, approx = P.div p1 p2 in let p, approx = P.div p1 p2 in
if approx then mk_euc_division p p2 t1 t2 ctx if approx then mk_euc_division p p2 t1 t2 ctx
else p, ctx else p, ctx
with Division_by_zero | Polynome.Maybe_zero -> with Division_by_zero | Polynome.Maybe_zero ->
P.create [coef, X.term_embed t] (Int 0) ty, ctx P.create [coef, X.term_embed t] (Int 0) ty, ctx
in in
P.add p p3, ctx P.add p p3, ctx
| Sy.Op Sy.Plus , [t1;t2] -> | Sy.Op Sy.Plus , [t1;t2] ->
let p2, ctx = mke coef p t2 ctx in let p2, ctx = mke coef p t2 ctx in
mke coef p2 t1 ctx mke coef p2 t1 ctx
| Sy.Op Sy.Minus , [t1;t2] -> | Sy.Op Sy.Minus , [t1;t2] ->
let p2, ctx = mke (minus_num coef) p t2 ctx in let p2, ctx = mke (minus_num coef) p t2 ctx in
mke coef p2 t1 ctx mke coef p2 t1 ctx
| Sy.Op Sy.Modulo , [t1;t2] -> | Sy.Op Sy.Modulo , [t1;t2] ->
let p1, ctx = mke coef (empty_polynome ty) t1 ctx in let p1, ctx = mke coef (empty_polynome ty) t1 ctx in
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
let p3, ctx = let p3, ctx =
try P.modulo p1 p2, ctx try P.modulo p1 p2, ctx
with e -> with e ->
let t = T.make mod_symb [t1; t2] Ty.Tint in let t = T.make mod_symb [t1; t2] Ty.Tint in
let ctx = match e with let ctx = match e with
| Division_by_zero | Polynome.Maybe_zero -> ctx | Division_by_zero | Polynome.Maybe_zero -> ctx
| Polynome.Not_a_num -> mk_modulo t t1 t2 ctx | Polynome.Not_a_num -> mk_modulo t t1 t2 ctx
| _ -> assert false | _ -> assert false
in in
P.create [coef, X.term_embed t] (Int 0) ty, ctx P.create [coef, X.term_embed t] (Int 0) ty, ctx
in in
P.add p p3, ctx P.add p p3, ctx
| _ -> | _ ->
let a, ctx' = X.make t in let a, ctx' = X.make t in
let ctx = ctx' @ ctx in let ctx = ctx' @ ctx in
@ -173,8 +173,8 @@ module Make
| [Int 1, x] , Int 0 -> p | [Int 1, x] , Int 0 -> p
| l , c -> | l , c ->
let ty = P.type_info p in let ty = P.type_info p in
let l = let l =
List.fold_left List.fold_left
(fun acc (coef,x) -> (fun acc (coef,x) ->
if coef =/ Int 0 then acc if coef =/ Int 0 then acc
else if coef =/ Int 1 || coef =/ Int (-1) then (coef,x)::acc else if coef =/ Int 1 || coef =/ Int (-1) then (coef,x)::acc
@ -182,14 +182,14 @@ module Make
| Some ac when is_mult ac.h -> | Some ac when is_mult ac.h ->
let unit_coef, abs_coef = let unit_coef, abs_coef =
if coef > Int 0 then Int 1, coef if coef > Int 0 then Int 1, coef
else Int (-1), minus_num coef else Int (-1), minus_num coef
in in
let p_cst = is_mine (P.create [] abs_coef ty) in let p_cst = is_mine (P.create [] abs_coef ty) in
let ac = {ac with l = Ac.add ac.h (p_cst, 1) ac.l} in let ac = {ac with l = Ac.add ac.h (p_cst, 1) ac.l} in
(unit_coef, X.ac_embed ac)::acc (unit_coef, X.ac_embed ac)::acc
| _ -> (coef,x)::acc | _ -> (coef,x)::acc
)[] l )[] l
in in
P.create l c ty P.create l c ty
*) *)
let make t = let make t =
@ -201,12 +201,12 @@ module Make
assert (n >=0); assert (n >=0);
if n = 0 then acc else expand p (n-1) (p::acc) if n = 0 then acc else expand p (n-1) (p::acc)
let rec number_of_vars l = let rec number_of_vars l =
List.fold_left (fun acc (r, n) -> acc + n * nb_vars_in_alien r) 0 l List.fold_left (fun acc (r, n) -> acc + n * nb_vars_in_alien r) 0 l
and nb_vars_in_alien r = and nb_vars_in_alien r =
match C.extract r with match C.extract r with
| Some p -> | Some p ->
let l, _ = P.to_list p in let l, _ = P.to_list p in
List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l
| None -> 1 | None -> 1
@ -223,23 +223,23 @@ module Make
let is_int r = X.type_info r = Ty.Tint let is_int r = X.type_info r = Ty.Tint
module XS = Set.Make(struct type t = X.r let compare = X.compare end) module XS = Set.Make(struct type t = X.r let compare = X.compare end)
let xs_of_list = let xs_of_list =
List.fold_left (fun s x -> XS.add x s) XS.empty List.fold_left (fun s x -> XS.add x s) XS.empty
let rec leaves p = let rec leaves p =
let s = let s =
List.fold_left List.fold_left
(fun s (_, a) -> XS.union (xs_of_list (X.leaves a)) s) (fun s (_, a) -> XS.union (xs_of_list (X.leaves a)) s)
XS.empty (fst (P.to_list p)) XS.empty (fst (P.to_list p))
in in
XS.elements s XS.elements s
let subst x t p = let subst x t p =
let p = P.subst x (embed t) p in let p = P.subst x (embed t) p in
let ty = P.type_info p in let ty = P.type_info p in
let l, c = P.to_list p in let l, c = P.to_list p in
let p = let p =
List.fold_left List.fold_left
(fun p (ai, xi) -> (fun p (ai, xi) ->
let xi' = X.subst x t xi in let xi' = X.subst x t xi in
@ -249,7 +249,7 @@ module Make
in in
P.add p p') P.add p p')
(P.create [] c ty) l (P.create [] c ty) l
in in
check_int (Exception.Unsolvable) p; check_int (Exception.Unsolvable) p;
is_mine p is_mine p
@ -259,32 +259,32 @@ module Make
let hash = P.hash let hash = P.hash
(* symmetric modulo p 131 *) (* symmetric modulo p 131 *)
let mod_sym a b = let mod_sym a b =
let m = mod_num a b in let m = mod_num a b in
let m = let m =
if m </ Int 0 then if m </ Int 0 then
if m >=/ minus_num b then m +/ b else assert false if m >=/ minus_num b then m +/ b else assert false
else else
if m <=/ b then m else assert false if m <=/ b then m else assert false
in in
if m </ b // (Int 2) then m else m -/ b if m </ b // (Int 2) then m else m -/ b
let mult_const p c = let mult_const p c =
P.mult p (P.create [] c (P.type_info p)) P.mult p (P.create [] c (P.type_info p))
let map_monomes f l ax = let map_monomes f l ax =
List.fold_left List.fold_left
(fun acc (a,x) -> (fun acc (a,x) ->
let a = f a in if a =/ Int 0 then acc else (a, x) :: acc) let a = f a in if a =/ Int 0 then acc else (a, x) :: acc)
[ax] l [ax] l
let apply_subst sb v = let apply_subst sb v =
is_mine (List.fold_left (fun v (x, p) -> embed (subst x p v)) v sb) is_mine (List.fold_left (fun v (x, p) -> embed (subst x p v)) v sb)
(* substituer toutes variables plus grandes que x *) (* substituer toutes variables plus grandes que x *)
let subst_bigger x l = let subst_bigger x l =
List.fold_left List.fold_left
(fun (l, sb) (b, y) -> (fun (l, sb) (b, y) ->
if X.compare y x > 0 then if X.compare y x > 0 then
let k = X.term_embed (fresh_name ()) in let k = X.term_embed (fresh_name ()) in
@ -293,43 +293,43 @@ module Make
([], []) l ([], []) l
let is_mine_p = List.map (fun (x,p) -> x, is_mine p) let is_mine_p = List.map (fun (x,p) -> x, is_mine p)
let extract_min = function let extract_min = function
| [] -> assert false | [] -> assert false
| [c] -> c, [] | [c] -> c, []
| (a, x) :: s -> | (a, x) :: s ->
List.fold_left List.fold_left
(fun ((a, x), l) (b, y) -> (fun ((a, x), l) (b, y) ->
if abs_num a <=/ abs_num b then if abs_num a <=/ abs_num b then
(a, x), ((b, y) :: l) (a, x), ((b, y) :: l)
else (b, y), ((a, x):: l)) ((a, x),[]) s else (b, y), ((a, x):: l)) ((a, x),[]) s
(* Decision Procedures. Page 131 *) (* Decision Procedures. Page 131 *)
let rec omega l b = let rec omega l b =
(* 1. choix d'une variable donc le |coef| est minimal *)
let (a, x), l = extract_min l in
(* 2. substituer les aliens plus grand que x pour (* 1. choix d'une variable donc le |coef| est minimal *)
let (a, x), l = extract_min l in
(* 2. substituer les aliens plus grand que x pour
assurer l'invariant sur l'ordre AC *) assurer l'invariant sur l'ordre AC *)
let l, sbs = subst_bigger x l in let l, sbs = subst_bigger x l in
let p = P.create l b Ty.Tint in let p = P.create l b Ty.Tint in
match a with match a with
| Int 0 -> assert false | Int 0 -> assert false
| Int 1 -> | Int 1 ->
(* 3.1. si a = 1 alors on a une substitution entiere pour x *) (* 3.1. si a = 1 alors on a une substitution entiere pour x *)
let p = mult_const p (Int (-1)) in let p = mult_const p (Int (-1)) in
(x, is_mine p) :: (is_mine_p sbs) (x, is_mine p) :: (is_mine_p sbs)
| Int (-1) -> | Int (-1) ->
(* 3.2. si a = -1 alors on a une subst entiere pour x*) (* 3.2. si a = -1 alors on a une subst entiere pour x*)
(x,is_mine p) :: (is_mine_p sbs) (x,is_mine p) :: (is_mine_p sbs)
| _ -> | _ ->
(* 4. sinon, (|a| <> 1) et a <> 0 *) (* 4. sinon, (|a| <> 1) et a <> 0 *)
(* 4.1. on rend le coef a positif s'il ne l'est pas deja *) (* 4.1. on rend le coef a positif s'il ne l'est pas deja *)
let a, l, b = let a, l, b =
if compare_num a (Int 0) < 0 then if compare_num a (Int 0) < 0 then
(minus_num a, (minus_num a,
List.map (fun (a,x) -> minus_num a,x) l, (minus_num b)) List.map (fun (a,x) -> minus_num a,x) l, (minus_num b))
else (a, l, b) else (a, l, b)
@ -338,28 +338,28 @@ module Make
omega_sigma sbs a x l b omega_sigma sbs a x l b
and omega_sigma sbs a x l b = and omega_sigma sbs a x l b =
(* 1. on definie m qui vaut a + 1 *) (* 1. on definie m qui vaut a + 1 *)
let m = a +/ Int 1 in let m = a +/ Int 1 in
(* 2. on introduit une variable fraiche *) (* 2. on introduit une variable fraiche *)
let sigma = X.term_embed (fresh_name ()) in let sigma = X.term_embed (fresh_name ()) in
(* 3. l'application de la formule (5.63) nous donne la valeur du pivot x*) (* 3. l'application de la formule (5.63) nous donne la valeur du pivot x*)
let mm_sigma = (minus_num m, sigma) in let mm_sigma = (minus_num m, sigma) in
let l_mod = map_monomes (fun a -> mod_sym a m) l mm_sigma in let l_mod = map_monomes (fun a -> mod_sym a m) l mm_sigma in
(* 3.1. Attention au signe de b : (* 3.1. Attention au signe de b :
on le passe a droite avant de faire mod_sym, d'ou minus_num *) on le passe a droite avant de faire mod_sym, d'ou minus_num *)
let b_mod = minus_num (mod_sym (minus_num b) m) in let b_mod = minus_num (mod_sym (minus_num b) m) in
let p = P.create l_mod b_mod Ty.Tint in let p = P.create l_mod b_mod Ty.Tint in
let sbs = (x, p) :: sbs in let sbs = (x, p) :: sbs in
(* 4. on substitue x par sa valeur dans l'equation de depart. (* 4. on substitue x par sa valeur dans l'equation de depart.
Voir la formule (5.64) *) Voir la formule (5.64) *)
let p' = P.add (P.mult_const a p) (P.create l b Ty.Tint) in let p' = P.add (P.mult_const a p) (P.create l b Ty.Tint) in
(* 5. on resoud sur l'equation simplifiee *) (* 5. on resoud sur l'equation simplifiee *)
let sbs2 = solve_int p' in let sbs2 = solve_int p' in
@ -370,7 +370,7 @@ module Make
let sbs2 = List.filter (fun (y, _) -> y <> sigma) sbs2 in let sbs2 = List.filter (fun (y, _) -> y <> sigma) sbs2 in
List.rev_append sbs sbs2 List.rev_append sbs sbs2
and solve_int p = and solve_int p =
if P.is_empty p then raise Not_found; if P.is_empty p then raise Not_found;
let pgcd = P.pgcd_numerators p in let pgcd = P.pgcd_numerators p in
let ppmc = P.ppmc_denominators p in let ppmc = P.ppmc_denominators p in
@ -379,29 +379,29 @@ module Make
if not (is_integer_num b) then raise Exception.Unsolvable; if not (is_integer_num b) then raise Exception.Unsolvable;
omega l b omega l b
let is_null p = let is_null p =
if snd (P.to_list p) <>/ (Int 0) then raise Exception.Unsolvable; if snd (P.to_list p) <>/ (Int 0) then raise Exception.Unsolvable;
[] []
let solve_int p = let solve_int p =
try solve_int p with Not_found -> is_null p try solve_int p with Not_found -> is_null p
let solve_real p = let solve_real p =
try try
let a, x = P.choose p in let a, x = P.choose p in
let p = let p =
P.mult P.mult
(P.create [] ((Int (-1)) // a) (P.type_info p)) (P.create [] ((Int (-1)) // a) (P.type_info p))
(P.remove x p) (P.remove x p)
in in
[x, is_mine p] [x, is_mine p]
with Not_found -> is_null p with Not_found -> is_null p
let safe_distribution p = let safe_distribution p =
let l, c = P.to_list p in let l, c = P.to_list p in
let ty = P.type_info p in let ty = P.type_info p in
List.fold_left List.fold_left
(fun p (coef, x) -> P.add p (P.create [coef,x] (Int 0) ty)) (fun p (coef, x) -> P.add p (P.create [coef,x] (Int 0) ty))
(P.create [] c ty) l (P.create [] c ty) l
let solve_aux r1 r2 = let solve_aux r1 r2 =
@ -418,18 +418,18 @@ module Make
let print = P.print let print = P.print
let fully_interpreted sb = let fully_interpreted sb =
match sb with match sb with
| Sy.Op (Sy.Plus | Sy.Minus) -> true | Sy.Op (Sy.Plus | Sy.Minus) -> true
| _ -> false | _ -> false
let term_extract _ = None let term_extract _ = None
module Rel = Fm.Make (X) module Rel = Fm.Make (X)
(struct (struct
include P include P
let poly_of = embed let poly_of = embed
let alien_of = is_mine let alien_of = is_mine
end) end)
end end

4
smt/arith.mli
View file

@ -14,8 +14,8 @@
module Type (X : Sig.X ): Polynome.T with type r = X.r module Type (X : Sig.X ): Polynome.T with type r = X.r
module Make module Make
(X : Sig.X) (X : Sig.X)
(P : Polynome.T with type r = X.r) (P : Polynome.T with type r = X.r)
(C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY (C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY
with type r = X.r and type t = P.t with type r = X.r and type t = P.t

190
smt/cc.ml
View file

@ -26,13 +26,13 @@ module type S = sig
module TimerCC : Timer.S module TimerCC : Timer.S
val empty : unit -> t val empty : unit -> t
val assume : cs:bool -> val assume : cs:bool ->
Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int
val query : Literal.LT.t -> t -> answer val query : Literal.LT.t -> t -> answer
val class_of : t -> Term.t -> Term.t list val class_of : t -> Term.t -> Term.t list
end end
module Make (X : Sig.X) = struct module Make (X : Sig.X) = struct
module TimerCC = Timer.Make(struct end) module TimerCC = Timer.Make(struct end)
@ -47,10 +47,10 @@ module Make (X : Sig.X) = struct
module S = Symbols module S = Symbols
module SetX = Set.Make(struct type t = X.r let compare = X.compare end) module SetX = Set.Make(struct type t = X.r let compare = X.compare end)
(* module Uf = Pptarjan.Uf *) (* module Uf = Pptarjan.Uf *)
type env = { type env = {
use : Use.t; use : Use.t;
uf : Uf.t ; uf : Uf.t ;
relation : X.Rel.t relation : X.Rel.t
@ -60,16 +60,16 @@ module Make (X : Sig.X) = struct
| CPos of int (* The explication of this choice *) | CPos of int (* The explication of this choice *)
| CNeg (* The choice has been already negated *) | CNeg (* The choice has been already negated *)
type t = { type t = {
gamma : env; gamma : env;
gamma_finite : env ; gamma_finite : env ;
choices : (X.r A.view * Num.num * choice_sign * Ex.t) list; choices : (X.r A.view * Num.num * choice_sign * Ex.t) list;
(** the choice, the size, choice_sign, the explication set, (** the choice, the size, choice_sign, the explication set,
the explication for this choice. *) the explication for this choice. *)
} }
module Print = struct module Print = struct
let begin_case_split () = () let begin_case_split () = ()
let end_case_split () = () let end_case_split () = ()
@ -101,12 +101,12 @@ module Make (X : Sig.X) = struct
let query a = () let query a = ()
end end
let bottom = Hstring.make "@bottom" let bottom = Hstring.make "@bottom"
let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint) let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint)
let concat_leaves uf l = let concat_leaves uf l =
let rec concat_rec acc t = let rec concat_rec acc t =
match X.leaves (fst (Uf.find uf t)) , acc with match X.leaves (fst (Uf.find uf t)) , acc with
[] , _ -> one::acc [] , _ -> one::acc
| res, [] -> res | res, [] -> res
@ -116,18 +116,18 @@ module Make (X : Sig.X) = struct
[] -> [one] [] -> [one]
| res -> res | res -> res
let are_equal env ex t1 t2 = let are_equal env ex t1 t2 =
if T.equal t1 t2 then ex if T.equal t1 t2 then ex
else match Uf.are_equal env.uf t1 t2 with else match Uf.are_equal env.uf t1 t2 with
| Yes dep -> Ex.union ex dep | Yes dep -> Ex.union ex dep
| No -> raise Exit | No -> raise Exit
let equal_only_by_congruence env ex t1 t2 acc = let equal_only_by_congruence env ex t1 t2 acc =
if T.equal t1 t2 then acc if T.equal t1 t2 then acc
else else
let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in
if X.fully_interpreted f1 then acc if X.fully_interpreted f1 then acc
else 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 if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then
try try
@ -138,47 +138,47 @@ module Make (X : Sig.X) = struct
with Exit -> acc with Exit -> acc
else acc else acc
let congruents env t1 s acc ex = let congruents env t1 s acc ex =
SetT.fold (equal_only_by_congruence env ex t1) s acc SetT.fold (equal_only_by_congruence env ex t1) s acc
let fold_find_with_explanation find ex l = let fold_find_with_explanation find ex l =
List.fold_left List.fold_left
(fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex) (fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex)
([], ex) l ([], ex) l
let view find va ex_a = let view find va ex_a =
match va with match va with
| A.Eq (t1, t2) -> | A.Eq (t1, t2) ->
let r1, ex1 = find t1 in let r1, ex1 = find t1 in
let r2, ex2 = find t2 in let r2, ex2 = find t2 in
let ex = Ex.union (Ex.union ex1 ex2) ex_a in let ex = Ex.union (Ex.union ex1 ex2) ex_a in
A.Eq(r1, r2), ex A.Eq(r1, r2), ex
| A.Distinct (b, lt) -> | A.Distinct (b, lt) ->
let lr, ex = fold_find_with_explanation find ex_a lt in let lr, ex = fold_find_with_explanation find ex_a lt in
A.Distinct (b, lr), ex A.Distinct (b, lr), ex
| A.Builtin(b, s, l) -> | A.Builtin(b, s, l) ->
let lr, ex = fold_find_with_explanation find ex_a l in let lr, ex = fold_find_with_explanation find ex_a l in
A.Builtin(b, s, List.rev lr), ex A.Builtin(b, s, List.rev lr), ex
let term_canonical_view env a ex_a = let term_canonical_view env a ex_a =
view (Uf.find env.uf) (A.LT.view a) ex_a view (Uf.find env.uf) (A.LT.view a) ex_a
let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a
let new_facts_by_contra_congruence env r bol ex = let new_facts_by_contra_congruence env r bol ex =
match X.term_extract r with match X.term_extract r with
| None -> [] | None -> []
| Some t1 -> | Some t1 ->
match T.view t1 with match T.view t1 with
| {T.f=f1 ; xs=[x]} -> | {T.f=f1 ; xs=[x]} ->
List.fold_left List.fold_left
(fun acc t2 -> (fun acc t2 ->
match T.view t2 with match T.view t2 with
| {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> | {T.f=f2 ; xs=[y]} when S.equal f1 f2 ->
let a = A.LT.make (A.Distinct (false, [x; y])) in let a = A.LT.make (A.Distinct (false, [x; y])) in
let dist = LTerm a in let dist = LTerm a in
begin match Uf.are_distinct env.uf t1 t2 with begin match Uf.are_distinct env.uf t1 t2 with
| Yes ex' -> | Yes ex' ->
let ex_r = Ex.union ex ex' in let ex_r = Ex.union ex ex' in
Print.contra_congruence a ex_r; Print.contra_congruence a ex_r;
(dist, ex_r) :: acc (dist, ex_r) :: acc
@ -188,25 +188,25 @@ module Make (X : Sig.X) = struct
) [] (Uf.class_of env.uf bol) ) [] (Uf.class_of env.uf bol)
| _ -> [] | _ -> []
let contra_congruence = let contra_congruence =
let vrai,_ = X.make T.vrai in let vrai,_ = X.make T.vrai in
let faux, _ = X.make T.faux in let faux, _ = X.make T.faux in
fun env r ex -> fun env r ex ->
if X.equal (fst (Uf.find_r env.uf r)) vrai then if X.equal (fst (Uf.find_r env.uf r)) vrai then
new_facts_by_contra_congruence env r T.faux ex new_facts_by_contra_congruence env r T.faux ex
else if X.equal (fst (Uf.find_r env.uf r)) faux then else if X.equal (fst (Uf.find_r env.uf r)) faux then
new_facts_by_contra_congruence env r T.vrai ex new_facts_by_contra_congruence env r T.vrai ex
else [] else []
let clean_use = let clean_use =
List.fold_left List.fold_left
(fun env (a, ex) -> (fun env (a, ex) ->
match a with match a with
| LSem _ -> assert false | LSem _ -> assert false
| LTerm t -> | LTerm t ->
begin begin
match A.LT.view t with match A.LT.view t with
| A.Distinct (_, lt) | A.Distinct (_, lt)
| A.Builtin (_, _, lt) -> | A.Builtin (_, _, lt) ->
let lvs = concat_leaves env.uf lt in let lvs = concat_leaves env.uf lt in
List.fold_left List.fold_left
@ -216,40 +216,40 @@ module Make (X : Sig.X) = struct
{ env with use = Use.add rx (st,sa) env.use } { env with use = Use.add rx (st,sa) env.use }
) env lvs ) env lvs
| _ -> assert false | _ -> assert false
end) end)
let rec congruence_closure env r1 r2 ex = let rec congruence_closure env r1 r2 ex =
Print.cc r1 r2; Print.cc r1 r2;
let uf, res = Uf.union env.uf r1 r2 ex in let uf, res = Uf.union env.uf r1 r2 ex in
List.fold_left List.fold_left
(fun (env, l) (p, touched, v) -> (fun (env, l) (p, touched, v) ->
(* we look for use(p) *) (* we look for use(p) *)
let p_t, p_a = Use.find p env.use in let p_t, p_a = Use.find p env.use in
(* we compute terms and atoms to consider for congruence *) (* we compute terms and atoms to consider for congruence *)
let repr_touched = List.map (fun (_,a,_) -> a) touched in 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 let st_others, sa_others = Use.congr_close_up env.use p repr_touched in
(* we update use *) (* we update use *)
let nuse = Use.up_close_up env.use p v in let nuse = Use.up_close_up env.use p v in
Use.print nuse; Use.print nuse;
(* we check the congruence of the terms. *) (* we check the congruence of the terms. *)
let env = {env with use=nuse} in let env = {env with use=nuse} in
let new_eqs = let new_eqs =
SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in
let touched_atoms = let touched_atoms =
List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched
in in
let touched_atoms = SetA.fold (fun (a, ex) acc -> let touched_atoms = SetA.fold (fun (a, ex) acc ->
(LTerm a, ex)::acc) p_a touched_atoms in (LTerm a, ex)::acc) p_a touched_atoms in
let touched_atoms = SetA.fold (fun (a, ex) acc -> let touched_atoms = SetA.fold (fun (a, ex) acc ->
(LTerm a, ex)::acc) sa_others touched_atoms in (LTerm a, ex)::acc) sa_others touched_atoms in
env, new_eqs @ touched_atoms env, new_eqs @ touched_atoms
) ({env with uf=uf}, []) res ) ({env with uf=uf}, []) res
let replay_atom env sa = let replay_atom env sa =
let relation, result = X.Rel.assume env.relation sa in let relation, result = X.Rel.assume env.relation sa in
let env = { env with relation = relation } in let env = { env with relation = relation } in
let env = clean_use env result.remove in let env = clean_use env result.remove in
@ -262,19 +262,19 @@ module Make (X : Sig.X) = struct
Print.add_to_use t; Print.add_to_use t;
(* we add t's arguments in env *) (* we add t's arguments in env *)
let {T.f = f; xs = xs} = T.view t in let {T.f = f; xs = xs} = T.view t in
let env, choices = let env, choices =
List.fold_left (fun (env, ch) t -> add_term env ch t ex) List.fold_left (fun (env, ch) t -> add_term env ch t ex)
(env, choices) xs (env, choices) xs
in in
(* we update uf and use *) (* we update uf and use *)
let nuf, ctx = Uf.add env.uf t in let nuf, ctx = Uf.add env.uf t in
Print.make_cst t ctx; Print.make_cst t ctx;
let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *) let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *)
if !cc_active then if !cc_active then
let lvs = concat_leaves nuf xs in let lvs = concat_leaves nuf xs in
let nuse = Use.up_add env.use t rt lvs in let nuse = Use.up_add env.use t rt lvs in
(* If finitetest is used we add the term to the relation *) (* If finitetest is used we add the term to the relation *)
let rel = X.Rel.add env.relation rt in let rel = X.Rel.add env.relation rt in
Use.print nuse; Use.print nuse;
@ -282,42 +282,42 @@ module Make (X : Sig.X) = struct
(* we compute terms to consider for congruence *) (* we compute terms to consider for congruence *)
(* we do this only for non-atomic terms with uninterpreted head-symbol *) (* we do this only for non-atomic terms with uninterpreted head-symbol *)
let st_uset = Use.congr_add nuse lvs in let st_uset = Use.congr_add nuse lvs in
(* we check the congruence of each term *) (* we check the congruence of each term *)
let env = {uf = nuf; use = nuse; relation = rel} in let env = {uf = nuf; use = nuse; relation = rel} in
let ct = congruents env t st_uset [] ex in let ct = congruents env t st_uset [] ex in
let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in
assume_literal env choices ct assume_literal env choices ct
else else
let rel = X.Rel.add env.relation rt in let rel = X.Rel.add env.relation rt in
let env = {env with uf = nuf; relation = rel} in let env = {env with uf = nuf; relation = rel} in
env, choices env, choices
end end
and add env choices a ex = and add env choices a ex =
match A.LT.view a with match A.LT.view a with
| A.Eq (t1, t2) -> | A.Eq (t1, t2) ->
let env, choices = add_term env choices t1 ex in let env, choices = add_term env choices t1 ex in
add_term env choices t2 ex add_term env choices t2 ex
| A.Distinct (_, lt) | A.Distinct (_, lt)
| A.Builtin (_, _, lt) -> | A.Builtin (_, _, lt) ->
let env, choices = List.fold_left let env, choices = List.fold_left
(fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in (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 lvs = concat_leaves env.uf lt in (* A verifier *)
let env = List.fold_left let env = List.fold_left
(fun env rx -> (fun env rx ->
let st, sa = Use.find rx env.use in let st, sa = Use.find rx env.use in
{ env with { env with
use = Use.add rx (st,SetA.add (a, ex) sa) env.use } use = Use.add rx (st,SetA.add (a, ex) sa) env.use }
) env lvs ) env lvs
in in
env, choices env, choices
and semantic_view env choices la = and semantic_view env choices la =
List.fold_left List.fold_left
(fun (env, choices, lsa) (a, ex) -> (fun (env, choices, lsa) (a, ex) ->
match a with match a with
| LTerm a -> | LTerm a ->
let env, choices = add env choices a ex in let env, choices = add env choices a ex in
let sa, ex = term_canonical_view env a ex in let sa, ex = term_canonical_view env a ex in
env, choices, (sa, Some a, ex)::lsa env, choices, (sa, Some a, ex)::lsa
@ -334,7 +334,7 @@ module Make (X : Sig.X) = struct
and assume_literal env choices la = and assume_literal env choices la =
if la = [] then env, choices if la = [] then env, choices
else else
let env, choices, lsa = semantic_view env choices la in let env, choices, lsa = semantic_view env choices la in
let env, choices = let env, choices =
List.fold_left List.fold_left
@ -363,15 +363,15 @@ module Make (X : Sig.X) = struct
assume_literal env (choices@l) l assume_literal env (choices@l) l
let look_for_sat ?(bad_last=No) ch t base_env l = let look_for_sat ?(bad_last=No) ch t base_env l =
let rec aux ch bad_last dl base_env li = let rec aux ch bad_last dl base_env li =
match li, bad_last with match li, bad_last with
| [], _ -> | [], _ ->
begin begin
match X.Rel.case_split base_env.relation with match X.Rel.case_split base_env.relation with
| [] -> | [] ->
{ t with gamma_finite = base_env; choices = List.rev dl }, ch { t with gamma_finite = base_env; choices = List.rev dl }, ch
| l -> | l ->
let l = let l =
List.map List.map
(fun (c, ex_c, size) -> (fun (c, ex_c, size) ->
let exp = Ex.fresh_exp () in let exp = Ex.fresh_exp () in
@ -420,13 +420,13 @@ module Make (X : Sig.X) = struct
let try_it f t = let try_it f t =
Print.begin_case_split (); Print.begin_case_split ();
let r = let r =
try try
if t.choices = [] then look_for_sat [] t t.gamma [] if t.choices = [] then look_for_sat [] t t.gamma []
else else
try try
let env, lt = f t.gamma_finite in let env, lt = f t.gamma_finite in
look_for_sat lt t env [] look_for_sat lt t env []
with Exception.Inconsistent dep -> with Exception.Inconsistent dep ->
look_for_sat ~bad_last:(Yes dep) look_for_sat ~bad_last:(Yes dep)
[] { t with choices = []} t.gamma t.choices [] { t with choices = []} t.gamma t.choices
with Exception.Inconsistent d -> with Exception.Inconsistent d ->
@ -437,37 +437,37 @@ module Make (X : Sig.X) = struct
let extract_from_semvalues = let extract_from_semvalues =
List.fold_left List.fold_left
(fun acc r -> (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 = let extract_terms_from_choices =
List.fold_left List.fold_left
(fun acc (a, _, _, _) -> (fun acc (a, _, _, _) ->
match a with match a with
| A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2] | A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2]
| A.Distinct (_, l) -> extract_from_semvalues acc l | A.Distinct (_, l) -> extract_from_semvalues acc l
| _ -> acc) | _ -> acc)
let extract_terms_from_assumed = let extract_terms_from_assumed =
List.fold_left List.fold_left
(fun acc (a, _) -> (fun acc (a, _) ->
match a with match a with
| LTerm r -> begin | LTerm r -> begin
match Literal.LT.view r with match Literal.LT.view r with
| Literal.Eq (t1, t2) -> | Literal.Eq (t1, t2) ->
SetT.add t1 (SetT.add t2 acc) SetT.add t1 (SetT.add t2 acc)
| Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) ->
List.fold_right SetT.add l acc List.fold_right SetT.add l acc
end end
| _ -> acc) | _ -> acc)
let assume ~cs a ex t = let assume ~cs a ex t =
let a = LTerm a in let a = LTerm a in
let gamma, ch = assume_literal t.gamma [] [a, ex] in let gamma, ch = assume_literal t.gamma [] [a, ex] in
let t = { t with gamma = gamma } in let t = { t with gamma = gamma } in
let t, ch = let t, ch =
if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t
else t, ch else t, ch
in in
let choices = extract_terms_from_choices SetT.empty t.choices in let choices = extract_terms_from_choices SetT.empty t.choices in
let all_terms = extract_terms_from_assumed choices ch in let all_terms = extract_terms_from_assumed choices ch in
@ -476,13 +476,13 @@ module Make (X : Sig.X) = struct
let class_of t term = Uf.class_of t.gamma.uf term let class_of t term = Uf.class_of t.gamma.uf term
let add_and_process a t = let add_and_process a t =
let aux a ex env = let aux a ex env =
let gamma, l = add env [] a ex in assume_literal gamma [] l let gamma, l = add env [] a ex in assume_literal gamma [] l
in in
let gamma, _ = aux a Ex.empty t.gamma in let gamma, _ = aux a Ex.empty t.gamma in
let t = { t with gamma = gamma } in let t = { t with gamma = gamma } in
let t, _ = try_it (aux a Ex.empty) t in let t, _ = try_it (aux a Ex.empty) t in
Use.print t.gamma.use; t Use.print t.gamma.use; t
let query a t = let query a t =
Print.query a; Print.query a;
@ -492,15 +492,15 @@ module Make (X : Sig.X) = struct
let t = add_and_process a t in let t = add_and_process a t in
Uf.are_equal t.gamma.uf t1 t2 Uf.are_equal t.gamma.uf t1 t2
| A.Distinct (false, [t1; t2]) -> | A.Distinct (false, [t1; t2]) ->
let na = A.LT.neg a in let na = A.LT.neg a in
let t = add_and_process na t in (* na ? *) let t = add_and_process na t in (* na ? *)
Uf.are_distinct t.gamma.uf t1 t2 Uf.are_distinct t.gamma.uf t1 t2
| A.Distinct _ -> | A.Distinct _ ->
assert false (* devrait etre capture par une analyse statique *) assert false (* devrait etre capture par une analyse statique *)
| _ -> | _ ->
let na = A.LT.neg a in let na = A.LT.neg a in
let t = add_and_process na t in let t = add_and_process na t in
let env = t.gamma in let env = t.gamma in
@ -508,16 +508,16 @@ module Make (X : Sig.X) = struct
X.Rel.query env.relation (rna, Some na, ex_rna) X.Rel.query env.relation (rna, Some na, ex_rna)
with Exception.Inconsistent d -> Yes d with Exception.Inconsistent d -> Yes d
let empty () = let empty () =
let env = { let env = {
use = Use.empty ; use = Use.empty ;
uf = Uf.empty ; uf = Uf.empty ;
relation = X.Rel.empty (); relation = X.Rel.empty ();
} }
in in
let t = { gamma = env; gamma_finite = env; choices = [] } in let t = { gamma = env; gamma_finite = env; choices = [] } in
let t, _, _ = let t, _, _ =
assume ~cs:false assume ~cs:false
(A.LT.make (A.Distinct (false, [T.vrai; T.faux]))) Ex.empty t (A.LT.make (A.Distinct (false, [T.vrai; T.faux]))) Ex.empty t
in t in t

2
smt/cc.mli
View file

@ -20,7 +20,7 @@ module type S = sig
module TimerCC : Timer.S module TimerCC : Timer.S
val empty : unit -> t val empty : unit -> t
val assume : cs:bool -> val assume : cs:bool ->
Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int
val query : Literal.LT.t -> t -> Sig.answer val query : Literal.LT.t -> t -> Sig.answer
val class_of : t -> Term.t -> Term.t list val class_of : t -> Term.t -> Term.t list

124
smt/combine.ml
View file

@ -28,31 +28,31 @@ struct
type r = type r =
| Term of Term.t | Term of Term.t
| X1 of X1.t | X1 of X1.t
| X5 of X5.t | X5 of X5.t
let extract1 = function X1 r -> Some r | _ -> None let extract1 = function X1 r -> Some r | _ -> None
let extract5 = function X5 r -> Some r | _ -> None let extract5 = function X5 r -> Some r | _ -> None
let embed1 x = X1 x let embed1 x = X1 x
let embed5 x = X5 x let embed5 x = X5 x
let is_int v = let is_int v =
let ty = match v with let ty = match v with
| X1 x -> X1.type_info x | X1 x -> X1.type_info x
| X5 x -> X5.type_info x | X5 x -> X5.type_info x
| Term t -> (Term.view t).Term.ty | Term t -> (Term.view t).Term.ty
in in
ty = Ty.Tint ty = Ty.Tint
let rec compare a b = let rec compare a b =
let c = compare_tag a b in let c = compare_tag a b in
if c = 0 then comparei a b else c if c = 0 then comparei a b else c
and compare_tag a b = and compare_tag a b =
Pervasives.compare (theory_num a) (theory_num b) Pervasives.compare (theory_num a) (theory_num b)
and comparei a b = and comparei a b =
match a, b with match a, b with
| X1 x, X1 y -> X1.compare x y | X1 x, X1 y -> X1.compare x y
| X5 x, X5 y -> X5.compare x y | X5 x, X5 y -> X5.compare x y
@ -64,47 +64,47 @@ struct
let equal a b = compare a b = 0 let equal a b = compare a b = 0
let hash = function let hash = function
| Term t -> Term.hash t | Term t -> Term.hash t
| X1 x -> X1.hash x | X1 x -> X1.hash x
| X5 x -> X5.hash x | X5 x -> X5.hash x
module MR = Map.Make(struct type t = r let compare = compare end) module MR = Map.Make(struct type t = r let compare = compare end)
let print fmt r = let print fmt r =
match r with match r with
| X1 t -> fprintf fmt "%a" X1.print t | X1 t -> fprintf fmt "%a" X1.print t
| X5 t -> fprintf fmt "%a" X5.print t | X5 t -> fprintf fmt "%a" X5.print t
| Term t -> fprintf fmt "%a" Term.print t | Term t -> fprintf fmt "%a" Term.print t
let leaves r = let leaves r =
match r with match r with
| X1 t -> X1.leaves t | X1 t -> X1.leaves t
| X5 t -> X5.leaves t | X5 t -> X5.leaves t
| Term _ -> [r] | Term _ -> [r]
let term_embed t = Term t let term_embed t = Term t
let term_extract r = let term_extract r =
match r with match r with
| X1 _ -> X1.term_extract r | X1 _ -> X1.term_extract r
| X5 _ -> X5.term_extract r | X5 _ -> X5.term_extract r
| Term t -> Some t | Term t -> Some t
let subst p v r = let subst p v r =
if equal p v then r if equal p v then r
else match r with else match r with
| X1 t -> X1.subst p v t | X1 t -> X1.subst p v t
| X5 t -> X5.subst p v t | X5 t -> X5.subst p v t
| Term _ -> if equal p r then v else r | Term _ -> if equal p r then v else r
let make t = let make t =
let {Term.f=sb} = Term.view t in let {Term.f=sb} = Term.view t in
match X1.is_mine_symb sb, X5.is_mine_symb sb with match X1.is_mine_symb sb, X5.is_mine_symb sb with
| true, false -> X1.make t | true, false -> X1.make t
| false, true -> X5.make t | false, true -> X5.make t
| false, false -> Term t, [] | false, false -> Term t, []
| _ -> assert false | _ -> assert false
let fully_interpreted sb = let fully_interpreted sb =
match X1.is_mine_symb sb, X5.is_mine_symb sb with match X1.is_mine_symb sb, X5.is_mine_symb sb with
| true, false -> X1.fully_interpreted sb | true, false -> X1.fully_interpreted sb
@ -113,38 +113,38 @@ struct
| _ -> assert false | _ -> assert false
let add_mr = let add_mr =
List.fold_left List.fold_left
(fun solved (p,v) -> (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 let unsolvable = function
| X1 x -> X1.unsolvable x | X1 x -> X1.unsolvable x
| X5 x -> X5.unsolvable x | X5 x -> X5.unsolvable x
| Term _ -> true | Term _ -> true
let partition tag = let partition tag =
List.partition List.partition
(fun (u,t) -> (fun (u,t) ->
(theory_num u = tag || unsolvable u) && (theory_num u = tag || unsolvable u) &&
(theory_num t = tag || unsolvable t)) (theory_num t = tag || unsolvable t))
let rec solve_list solved l = let rec solve_list solved l =
List.fold_left List.fold_left
(fun solved (a,b) -> (fun solved (a,b) ->
let cmp = compare a b in let cmp = compare a b in
if cmp = 0 then solved else if cmp = 0 then solved else
match a , b with match a , b with
(* both sides are empty *) (* both sides are empty *)
| Term _ , Term _ -> | Term _ , Term _ ->
add_mr solved (unsolvable_values cmp a b) add_mr solved (unsolvable_values cmp a b)
(* only one side is empty *) (* only one side is empty *)
| (a, b) | (a, b)
when unsolvable a || unsolvable b || compare_tag a b = 0 -> when unsolvable a || unsolvable b || compare_tag a b = 0 ->
let a,b = if unsolvable a then b,a else a,b in let a,b = if unsolvable a then b,a else a,b in
let cp , sol = partition (theory_num a) (solvei b a) in let cp , sol = partition (theory_num a) (solvei b a) in
solve_list (add_mr solved cp) sol solve_list (add_mr solved cp) sol
(* both sides are not empty *) (* both sides are not empty *)
| a , b -> solve_theoryj solved a b | a , b -> solve_theoryj solved a b
) solved l ) solved l
@ -153,7 +153,7 @@ struct
match a, b with match a, b with
(* Clash entre theories: On peut avoir ces pbs ? *) (* Clash entre theories: On peut avoir ces pbs ? *)
| X1 _, X5 _ | X1 _, X5 _
| X5 _, X1 _ | X5 _, X1 _
-> assert false -> assert false
(* theorie d'un cote, vide de l'autre *) (* theorie d'un cote, vide de l'autre *)
@ -171,23 +171,23 @@ struct
| X5 _ -> X5.solve a b | X5 _ -> X5.solve a b
| Term _ -> assert false | Term _ -> assert false
let rec solve_rec mt ab = let rec solve_rec mt ab =
let mr = solve_list mt ab in let mr = solve_list mt ab in
let mr , ab = let mr , ab =
MR.fold MR.fold
(fun p lr ((mt,ab) as acc) -> match lr with (fun p lr ((mt,ab) as acc) -> match lr with
[] -> assert false [] -> assert false
| [_] -> acc | [_] -> acc
| x::lx -> | x::lx ->
MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx) MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx)
mr (mr,[]) mr (mr,[])
in in
if ab = [] then mr else solve_rec mr ab if ab = [] then mr else solve_rec mr ab
let solve a b = let solve a b =
MR.fold MR.fold
(fun p lr ret -> (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]) [] (solve_rec MR.empty [a,b]) []
let rec type_info = function let rec type_info = function
@ -199,28 +199,28 @@ struct
type elt = r type elt = r
type r = elt type r = elt
type t = { type t = {
r1: X1.Rel.t; r1: X1.Rel.t;
r5: X5.Rel.t; r5: X5.Rel.t;
} }
let empty _ = { let empty _ = {
r1=X1.Rel.empty (); r1=X1.Rel.empty ();
r5=X5.Rel.empty (); r5=X5.Rel.empty ();
} }
let assume env sa = let assume env sa =
let env1, { assume = a1; remove = rm1} = X1.Rel.assume env.r1 sa in let env1, { assume = a1; remove = rm1} = X1.Rel.assume env.r1 sa in
let env5, { assume = a5; remove = rm5} = X5.Rel.assume env.r5 sa in let env5, { assume = a5; remove = rm5} = X5.Rel.assume env.r5 sa in
{r1=env1; r5=env5}, {r1=env1; r5=env5},
{ assume = a1@a5; remove = rm1@rm5;} { assume = a1@a5; remove = rm1@rm5;}
let query env a = let query env a =
match X1.Rel.query env.r1 a with match X1.Rel.query env.r1 a with
| Yes _ as ans -> ans | Yes _ as ans -> ans
| No -> X5.Rel.query env.r5 a | No -> X5.Rel.query env.r5 a
let case_split env = let case_split env =
let seq1 = X1.Rel.case_split env.r1 in let seq1 = X1.Rel.case_split env.r1 in
let seq5 = X5.Rel.case_split env.r5 in let seq5 = X5.Rel.case_split env.r5 in
seq1 @ seq5 seq1 @ seq5
@ -241,7 +241,7 @@ and X1 : Sig.THEORY with type t = TX1.t and type r = CX.r =
type r = CX.r type r = CX.r
let extract = CX.extract1 let extract = CX.extract1
let embed = CX.embed1 let embed = CX.embed1
let assume env _ _ = env, {Sig.assume = []; remove = []} let assume env _ _ = env, {Sig.assume = []; remove = []}
end) end)
and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract = and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract =

22
smt/explanation.ml
View file

@ -12,14 +12,14 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Solver_types open Solver_types
open Format open Format
type exp = Atom of Solver_types.atom | Fresh of int type exp = Atom of Solver_types.atom | Fresh of int
module S = module S =
Set.Make Set.Make
(struct (struct
type t = exp type t = exp
let compare a b = match a,b with let compare a b = match a,b with
| Atom _, Fresh _ -> -1 | Atom _, Fresh _ -> -1
@ -27,25 +27,25 @@ module S =
| Fresh i1, Fresh i2 -> i1 - i2 | Fresh i1, Fresh i2 -> i1 - i2
| Atom a, Atom b -> a.aid - b.aid | Atom a, Atom b -> a.aid - b.aid
end) 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 = let iter_atoms f s =
S.iter (fun e -> match e with S.iter (fun e -> match e with
| Fresh _ -> () | Fresh _ -> ()
| Atom a -> f a) s | Atom a -> f a) s
let fold_atoms f s acc = let fold_atoms f s acc =
S.fold (fun e acc -> match e with S.fold (fun e acc -> match e with
| Fresh _ -> acc | Fresh _ -> acc
| Atom a -> f a acc) s acc | Atom a -> f a acc) s acc
let merge e1 e2 = e1 let merge e1 e2 = e1
@ -61,9 +61,9 @@ let remove_fresh i s =
let add_fresh i = S.add (Fresh i) let add_fresh i = S.add (Fresh i)
let print fmt ex = let print fmt ex =
fprintf fmt "{"; fprintf fmt "{";
S.iter (function S.iter (function
| Atom a -> fprintf fmt "%a, " Debug.atom a | Atom a -> fprintf fmt "%a, " Debug.atom a
| Fresh i -> fprintf fmt "Fresh%d " i) ex; | Fresh i -> fprintf fmt "Fresh%d " i) ex;
fprintf fmt "}" fprintf fmt "}"

308
smt/fm.ml
View file

@ -15,7 +15,7 @@ open Num
open Format open Format
open Sig open Sig
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = Hstring.make "<" let alt = Hstring.make "<"
let is_le n = Hstring.compare n ale = 0 let is_le n = Hstring.compare n ale = 0
let is_lt n = Hstring.compare n alt = 0 let is_lt n = Hstring.compare n alt = 0
@ -24,7 +24,7 @@ let (-@) l1 l2 = List.rev_append l1 l2
module L = Literal module L = Literal
module Sy = Symbols module Sy = Symbols
exception NotConsistent of Literal.LT.Set.t exception NotConsistent of Literal.LT.Set.t
module type EXTENDED_Polynome = sig module type EXTENDED_Polynome = sig
@ -33,7 +33,7 @@ module type EXTENDED_Polynome = sig
val alien_of : t -> r val alien_of : t -> r
end end
module Make module Make
(X : Sig.X) (X : Sig.X)
(P : EXTENDED_Polynome with type r = X.r) = struct (P : EXTENDED_Polynome with type r = X.r) = struct
@ -41,22 +41,22 @@ module Make
module SP = Set.Make(P) module SP = Set.Make(P)
module SX = Set.Make(struct type t = X.r include X end) module SX = Set.Make(struct type t = X.r include X end)
module MX = Map.Make(struct type t = X.r include X end) module MX = Map.Make(struct type t = X.r include X end)
type r = P.r type r = P.r
module LR = Literal.Make(struct type t = X.r include X end) module LR = Literal.Make(struct type t = X.r include X end)
module Seq = module Seq =
Set.Make Set.Make
(struct (struct
type t = r L.view * L.LT.t option * Explanation.t type t = r L.view * L.LT.t option * Explanation.t
let compare (a, _, _) (b, _, _) = let compare (a, _, _) (b, _, _) =
LR.compare (LR.make a) (LR.make b) LR.compare (LR.make a) (LR.make b)
end) end)
module Inequation = struct module Inequation = struct
type t = { type t = {
ple0 : P.t; ple0 : P.t;
is_le : bool; is_le : bool;
dep : (Literal.LT.t * num * P.t * bool) list; dep : (Literal.LT.t * num * P.t * bool) list;
expl : Explanation.t expl : Explanation.t
@ -65,7 +65,7 @@ module Make
let print fmt ineq = fprintf fmt "%a %s 0" P.print ineq.ple0 let print fmt ineq = fprintf fmt "%a %s 0" P.print ineq.ple0
(if ineq.is_le then "<=" else "<") (if ineq.is_le then "<=" else "<")
let create p1 p2 is_le a expl = let create p1 p2 is_le a expl =
let p = P.add p1 (P.mult (P.create [] (Int (-1)) (P.type_info p1)) p2) in let p = P.add p1 (P.mult (P.create [] (Int (-1)) (P.type_info p1)) p2) in
{ ple0 = p; is_le = is_le; dep = [a, Int 1, p, is_le]; expl = expl } { ple0 = p; is_le = is_le; dep = [a, Int 1, p, is_le]; expl = expl }
@ -75,18 +75,18 @@ module Make
let is_monomial ineq = P.is_monomial ineq.ple0 let is_monomial ineq = P.is_monomial ineq.ple0
let pos_neg mx { ple0 = p } = let pos_neg mx { ple0 = p } =
List.fold_left (fun m (c,x) -> List.fold_left (fun m (c,x) ->
let cmp = compare_num c (Int 0) in let cmp = compare_num c (Int 0) in
if cmp = 0 then m if cmp = 0 then m
else else
let (pos, neg) = try MX.find x m with Not_found -> (0,0) in let (pos, neg) = try MX.find x m with Not_found -> (0,0) in
if cmp > 0 then MX.add x (pos+1, neg) m if cmp > 0 then MX.add x (pos+1, neg) m
else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p)) else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p))
end end
type t = { type t = {
inequations : (Literal.LT.t * Inequation.t) list ; inequations : (Literal.LT.t * Inequation.t) list ;
monomes: (Intervals.t * SX.t) MX.t; monomes: (Intervals.t * SX.t) MX.t;
polynomes : Intervals.t MP.t; polynomes : Intervals.t MP.t;
@ -95,30 +95,30 @@ module Make
} }
module Debug = struct module Debug = struct
let list_of_ineqs fmt = List.iter (fprintf fmt "%a " Inequation.print) let list_of_ineqs fmt = List.iter (fprintf fmt "%a " Inequation.print)
let assume a = () let assume a = ()
let cross x cpos cneg others ninqs = () let cross x cpos cneg others ninqs = ()
let print_use fmt use = let print_use fmt use =
SX.iter (fprintf fmt "%a, " X.print) use SX.iter (fprintf fmt "%a, " X.print) use
let env env = () let env env = ()
let implied_equalities l = () let implied_equalities l = ()
end end
let empty _ = { let empty _ = {
inequations = [] ; inequations = [] ;
monomes = MX.empty ; monomes = MX.empty ;
polynomes = MP.empty ; polynomes = MP.empty ;
known_eqs = SX.empty ; known_eqs = SX.empty ;
improved = SP.empty ; improved = SP.empty ;
} }
let replace_inequation env x ineq = let replace_inequation env x ineq =
{ env with { env with
inequations = (x, ineq)::(List.remove_assoc x env.inequations) } inequations = (x, ineq)::(List.remove_assoc x env.inequations) }
@ -127,13 +127,13 @@ module Make
if Intervals.is_strict_smaller newi oldi then if Intervals.is_strict_smaller newi oldi then
{ env with improved = SP.add p env.improved } { env with improved = SP.add p env.improved }
else env else env
(* (*
let oldify_inequations env = let oldify_inequations env =
{ env with { env with
inequations = env.inequations@env.new_inequations; inequations = env.inequations@env.new_inequations;
new_inequations = [] } *) new_inequations = [] } *)
let mult_bornes_vars vars monomes ty= let mult_bornes_vars vars monomes ty=
List.fold_left List.fold_left
(fun ui (y,n) -> (fun ui (y,n) ->
@ -142,7 +142,7 @@ module Make
with Not_found -> Intervals.undefined ty with Not_found -> Intervals.undefined ty
in in
Intervals.mult ui (Intervals.power n ui') Intervals.mult ui (Intervals.power n ui')
) (Intervals.point (Int 1) ty Explanation.empty) vars ) (Intervals.point (Int 1) ty Explanation.empty) vars
let intervals_from_monomes env p = let intervals_from_monomes env p =
@ -154,13 +154,13 @@ module Make
) (Intervals.point v (P.type_info p) Explanation.empty) pl ) (Intervals.point v (P.type_info p) Explanation.empty) pl
let rec add_monome expl use_x env x = let rec add_monome expl use_x env x =
try try
let u, old_use_x = MX.find x env.monomes in let u, old_use_x = MX.find x env.monomes in
{ env with monomes = MX.add x (u, SX.union old_use_x use_x) env.monomes } { env with monomes = MX.add x (u, SX.union old_use_x use_x) env.monomes }
with Not_found -> with Not_found ->
update_monome expl use_x env x update_monome expl use_x env x
and init_monomes env p use_p expl = and init_monomes env p use_p expl =
List.fold_left List.fold_left
(fun env (_, x) -> add_monome expl use_p env x) (fun env (_, x) -> add_monome expl use_p env x)
env (fst (P.to_list p)) env (fst (P.to_list p))
@ -168,8 +168,8 @@ module Make
and init_alien expl p (normal_p, c, d) ty use_x env = and init_alien expl p (normal_p, c, d) ty use_x env =
let env = init_monomes env p use_x expl in let env = init_monomes env p use_x expl in
let i = intervals_from_monomes env p in let i = intervals_from_monomes env p in
let i = let i =
try try
let old_i = MP.find normal_p env.polynomes in let old_i = MP.find normal_p env.polynomes in
let old_i = Intervals.scale d let old_i = Intervals.scale d
(Intervals.add old_i (Intervals.point c ty Explanation.empty)) in (Intervals.add old_i (Intervals.point c ty Explanation.empty)) in
@ -178,11 +178,11 @@ module Make
in in
env, i env, i
and update_monome expl use_x env x = and update_monome expl use_x env x =
let ty = X.type_info x in let ty = X.type_info x in
let ui, env = let ui, env =
match X.term_extract x with match X.term_extract x with
| Some t -> | Some t ->
let use_x = SX.singleton x in let use_x = SX.singleton x in
@ -196,7 +196,7 @@ module Make
let env, ia = init_alien expl pa npa ty use_x env in let env, ia = init_alien expl pa npa ty use_x env in
let env, ib = init_alien expl pb npb ty use_x env in let env, ib = init_alien expl pb npb ty use_x env in
let ia, ib = match Intervals.doesnt_contain_0 ib with let ia, ib = match Intervals.doesnt_contain_0 ib with
| Yes ex when Num.compare_num ca cb = 0 | Yes ex when Num.compare_num ca cb = 0
&& P.compare pa' pb' = 0 -> && P.compare pa' pb' = 0 ->
let expl = Explanation.union ex expl in let expl = Explanation.union ex expl in
Intervals.point da ty expl, Intervals.point db ty expl Intervals.point da ty expl, Intervals.point db ty expl
@ -212,13 +212,13 @@ module Make
with Not_found -> Intervals.undefined (X.type_info x), use_x in with Not_found -> Intervals.undefined (X.type_info x), use_x in
let ui = Intervals.intersect ui u in let ui = Intervals.intersect ui u in
{ env with monomes = MX.add x (ui, (SX.union use_x use_x')) env.monomes } { env with monomes = MX.add x (ui, (SX.union use_x use_x')) env.monomes }
and tighten_div x env expl = env and tighten_div x env expl = env
and tighten_non_lin x use_x env expl = and tighten_non_lin x use_x env expl =
let env = tighten_div x env expl in let env = tighten_div x env expl in
SX.fold SX.fold
(fun x acc -> (fun x acc ->
let _, use = MX.find x acc.monomes in let _, use = MX.find x acc.monomes in
update_monome expl use acc x) update_monome expl use acc x)
use_x env use_x env
@ -229,14 +229,14 @@ module Make
List.fold_left (fun monomes (a,x) -> List.fold_left (fun monomes (a,x) ->
let np = P.remove x p in let np = P.remove x p in
let (np,c,d) = P.normal_form_pos np in let (np,c,d) = P.normal_form_pos np in
try try
let inp = MP.find np polynomes in let inp = MP.find np polynomes in
let new_ix = let new_ix =
Intervals.scale Intervals.scale
((Int 1) // a) ((Int 1) // a)
(Intervals.add i (Intervals.add i
(Intervals.scale (minus_num d) (Intervals.scale (minus_num d)
(Intervals.add inp (Intervals.add inp
(Intervals.point c ty Explanation.empty)))) in (Intervals.point c ty Explanation.empty)))) in
let old_ix, ux = MX.find x monomes in let old_ix, ux = MX.find x monomes in
let ix = Intervals.intersect old_ix new_ix in let ix = Intervals.intersect old_ix new_ix in
@ -261,7 +261,7 @@ module Make
let find_one_eq x u = let find_one_eq x u =
match Intervals.is_point u with match Intervals.is_point u with
| Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v -> | Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v ->
let eq = let eq =
L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in
Some (eq, None, ex) Some (eq, None, ex)
| _ -> None | _ -> None
@ -271,29 +271,29 @@ module Make
| None -> eqs | None -> eqs
| Some eq1 -> eq1::eqs | Some eq1 -> eq1::eqs
type ineq_status = type ineq_status =
| Trivial_eq | Trivial_eq
| Trivial_ineq of num | Trivial_ineq of num
| Bottom | Bottom
| Monome of num * P.r * num | Monome of num * P.r * num
| Other | Other
let ineq_status ({Inequation.ple0 = p ; is_le = is_le} as ineq) = let ineq_status ({Inequation.ple0 = p ; is_le = is_le} as ineq) =
match Inequation.is_monomial ineq with match Inequation.is_monomial ineq with
Some (a, x, v) -> Monome (a, x, v) Some (a, x, v) -> Monome (a, x, v)
| None -> | None ->
if P.is_empty p then if P.is_empty p then
let _, v = P.to_list p in let _, v = P.to_list p in
let c = compare_num v (Int 0) in let c = compare_num v (Int 0) in
if c > 0 || (c >=0 && not is_le) then Bottom if c > 0 || (c >=0 && not is_le) then Bottom
else else
if c = 0 && is_le then Trivial_eq if c = 0 && is_le then Trivial_eq
else Trivial_ineq v else Trivial_ineq v
else Other else Other
(*let ineqs_from_dep dep borne_inf is_le = (*let ineqs_from_dep dep borne_inf is_le =
List.map List.map
(fun {poly_orig = p; coef = c} -> (fun {poly_orig = p; coef = c} ->
let (m,v,ty) = P.mult_const minusone p in let (m,v,ty) = P.mult_const minusone p in
(* quelle valeur pour le ?????? *) (* quelle valeur pour le ?????? *)
{ ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ; { ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ;
@ -308,7 +308,7 @@ module Make
let fm_equalities env eqs { Inequation.ple0 = p; dep = dep; expl = ex } = let fm_equalities env eqs { Inequation.ple0 = p; dep = dep; expl = ex } =
let inqs, eqs = let inqs, eqs =
List.fold_left List.fold_left
(fun (inqs, eqs) (a, _, p, _) -> (fun (inqs, eqs) (a, _, p, _) ->
List.remove_assoc a inqs, (mk_equality p, Some a, ex) :: eqs List.remove_assoc a inqs, (mk_equality p, Some a, ex) :: eqs
) (env.inequations, eqs) dep ) (env.inequations, eqs) dep
in in
@ -320,15 +320,15 @@ module Make
let u = let u =
if a >/ (Int 0) then if a >/ (Int 0) then
Intervals.new_borne_sup expl b is_le uints Intervals.new_borne_sup expl b is_le uints
else else
Intervals.new_borne_inf expl b is_le uints in Intervals.new_borne_inf expl b is_le uints in
let env = { env with monomes = MX.add x (u, use_x) env.monomes } in let env = { env with monomes = MX.add x (u, use_x) env.monomes } in
let env = tighten_non_lin x use_x env expl in let env = tighten_non_lin x use_x env expl in
env, (find_eq eqs x u env) env, (find_eq eqs x u env)
let update_ple0 env p0 is_le expl = let update_ple0 env p0 is_le expl =
if P.is_empty p0 then env if P.is_empty p0 then env
else else
let ty = P.type_info p0 in let ty = P.type_info p0 in
let a, _ = P.choose p0 in let a, _ = P.choose p0 in
let p, change = let p, change =
@ -343,20 +343,20 @@ module Make
else else
Intervals.new_borne_sup expl c is_le (Intervals.undefined ty) in Intervals.new_borne_sup expl c is_le (Intervals.undefined ty) in
let u, pu = let u, pu =
try try
let pu = MP.find p env.polynomes in let pu = MP.find p env.polynomes in
let i = Intervals.intersect u pu in let i = Intervals.intersect u pu in
i, pu i, pu
with Not_found -> u, Intervals.undefined ty with Not_found -> u, Intervals.undefined ty
in in
let env = let env =
if Intervals.is_strict_smaller u pu then if Intervals.is_strict_smaller u pu then
let polynomes = MP.add p u env.polynomes in let polynomes = MP.add p u env.polynomes in
let monomes = update_monomes_from_poly p u polynomes env.monomes in let monomes = update_monomes_from_poly p u polynomes env.monomes in
let improved = SP.add p env.improved in let improved = SP.add p env.improved in
{ env with { env with
polynomes = polynomes; polynomes = polynomes;
monomes = monomes; monomes = monomes;
improved = improved } improved = improved }
else env else env
in in
@ -364,41 +364,41 @@ module Make
| [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le) | [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le)
| _ -> env | _ -> env
let add_inequations acc lin expl = let add_inequations acc lin expl =
List.fold_left List.fold_left
(fun (env, eqs) ineq -> (fun (env, eqs) ineq ->
(* let expl = List.fold_left (* let expl = List.fold_left
(fun expl (l,_,_,_) -> (fun expl (l,_,_,_) ->
Explanation.union (*Explanation.everything*) Explanation.union (*Explanation.everything*)
(Explanation.singleton (Formula.mk_lit l)) (Explanation.singleton (Formula.mk_lit l))
expl expl
) expl ineq.Inequation.dep ) expl ineq.Inequation.dep
in *) in *)
let expl = Explanation.union ineq.Inequation.expl expl in let expl = Explanation.union ineq.Inequation.expl expl in
match ineq_status ineq with match ineq_status ineq with
| Bottom -> | Bottom ->
raise (Exception.Inconsistent expl) raise (Exception.Inconsistent expl)
| Trivial_eq -> | Trivial_eq ->
fm_equalities env eqs ineq fm_equalities env eqs ineq
| Trivial_ineq c -> | Trivial_ineq c ->
let n, pp = let n, pp =
List.fold_left List.fold_left
(fun ((n, pp) as acc) (_, _, p, is_le) -> (fun ((n, pp) as acc) (_, _, p, is_le) ->
if is_le then acc else if is_le then acc else
match pp with match pp with
| Some _ -> n+1, None | Some _ -> n+1, None
| None when n=0 -> 1, Some p | None when n=0 -> 1, Some p
| _ -> n+1, None) (0,None) ineq.Inequation.dep | _ -> n+1, None) (0,None) ineq.Inequation.dep
in in
let env = let env =
List.fold_left List.fold_left
(fun env (_, coef, p, is_le) -> (fun env (_, coef, p, is_le) ->
let ty = P.type_info p in let ty = P.type_info p in
let is_le = let is_le =
match pp with match pp with
Some x -> P.compare x p = 0 | _ -> is_le && n=0 Some x -> P.compare x p = 0 | _ -> is_le && n=0
in in
let p' = P.sub (P.create [] (c // coef) ty) p in let p' = P.sub (P.create [] (c // coef) ty) p in
update_ple0 env p' is_le expl update_ple0 env p' is_le expl
@ -407,24 +407,24 @@ module Make
env, eqs env, eqs
| Monome (a, x, v) -> | Monome (a, x, v) ->
let env, eqs = let env, eqs =
update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le
in in
(*let env,eqs = update_bornes env eqs ((a,x),c) ineq.ple0.le in (*let env,eqs = update_bornes env eqs ((a,x),c) ineq.ple0.le in
let env,eqs = update_polynomes env eqs ineq in let env,eqs = update_polynomes env eqs ineq in
env, pers_ineqs, eqs*) env, pers_ineqs, eqs*)
env, eqs env, eqs
| Other -> | Other ->
env, eqs env, eqs
(*t env,eqs = update_polynomes env eqs ineq in (*t env,eqs = update_polynomes env eqs ineq in
env, pers_ineqs, eqs*) env, pers_ineqs, eqs*)
) acc lin ) acc lin
let mult_list c = let mult_list c =
List.map (fun (a, coef, p, is_le) -> (a, coef */ c, p, is_le)) List.map (fun (a, coef, p, is_le) -> (a, coef */ c, p, is_le))
let div_by_pgcd (a, b) ty = let div_by_pgcd (a, b) ty =
@ -436,14 +436,14 @@ module Make
else a, b else a, b
with Failure "big_int_of_ratio" -> a, b with Failure "big_int_of_ratio" -> a, b
let cross x cpos cneg = let cross x cpos cneg =
let rec cross_rec acc = function let rec cross_rec acc = function
| [] -> acc | [] -> acc
| { Inequation.ple0 = p1; is_le = k1; dep = d1; expl = ex1 } :: l -> | { Inequation.ple0 = p1; is_le = k1; dep = d1; expl = ex1 } :: l ->
let n1 = abs_num (P.find x p1) in let n1 = abs_num (P.find x p1) in
(* let ty = P.type_info p1 in *) (* let ty = P.type_info p1 in *)
let acc = let acc =
List.fold_left List.fold_left
(fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} -> (fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} ->
let n2 = abs_num (P.find x p2) in let n2 = abs_num (P.find x p2) in
(* let n1, n2 = div_by_pgcd (n1, n2) ty in *) (* let n1, n2 = div_by_pgcd (n1, n2) ty in *)
@ -452,36 +452,36 @@ module Make
(P.mult (P.create [] n1 (P.type_info p1)) p2) in (P.mult (P.create [] n1 (P.type_info p1)) p2) in
let d1 = mult_list n2 d1 in let d1 = mult_list n2 d1 in
let d2 = mult_list n1 d2 in let d2 = mult_list n1 d2 in
let ni = let ni =
{ Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2; { Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2;
expl = Explanation.union ex1 ex2 } expl = Explanation.union ex1 ex2 }
in in
ni::acc ni::acc
) acc cpos ) acc cpos
in in
cross_rec acc l cross_rec acc l
in in
cross_rec [] cneg cross_rec [] cneg
let split x l = let split x l =
let rec split_rec (cp, cn, co) ineq = let rec split_rec (cp, cn, co) ineq =
try try
let a = Inequation.find x ineq in let a = Inequation.find x ineq in
if a >/ (Int 0) then ineq::cp, cn, co if a >/ (Int 0) then ineq::cp, cn, co
else cp, ineq::cn, co else cp, ineq::cn, co
with Not_found -> cp, cn, ineq::co with Not_found -> cp, cn, ineq::co
in in
List.fold_left split_rec ([], [], []) l List.fold_left split_rec ([], [], []) l
let length s = SX.fold (fun _ acc -> acc+1) s 0 let length s = SX.fold (fun _ acc -> acc+1) s 0
let choose_var l = let choose_var l =
let pos_neg = List.fold_left Inequation.pos_neg MX.empty l in let pos_neg = List.fold_left Inequation.pos_neg MX.empty l in
let xopt = MX.fold (fun x (pos, neg) acc -> let xopt = MX.fold (fun x (pos, neg) acc ->
match acc with match acc with
| None -> Some (x, pos * neg) | None -> Some (x, pos * neg)
| Some (y, c') -> | Some (y, c') ->
let c = pos * neg in let c = pos * neg in
if c < c' then Some (x, c) else acc if c < c' then Some (x, c) else acc
) pos_neg None in ) pos_neg None in
match xopt with match xopt with
@ -504,16 +504,16 @@ module Make
with Not_found -> add_inequations acc l expl with Not_found -> add_inequations acc l expl
(* (*
let fm env eqs expl = let fm env eqs expl =
fourier (env, eqs) fourier (env, eqs)
(List.map snd env.inequations) (List.map snd env.inequations)
(List.map snd env.new_inequations) expl (List.map snd env.new_inequations) expl
*) *)
let fm env eqs expl = let fm env eqs expl =
fourier (env, eqs) (List.map snd env.inequations) expl fourier (env, eqs) (List.map snd env.inequations) expl
let is_num r = let is_num r =
let ty = X.type_info r in ty = Ty.Tint || ty = Ty.Treal let ty = X.type_info r in ty = Ty.Tint || ty = Ty.Treal
let add_disequality env eqs p expl = let add_disequality env eqs p expl =
@ -523,12 +523,12 @@ module Make
raise (Exception.Inconsistent expl) raise (Exception.Inconsistent expl)
| ([], v) -> | ([], v) ->
env, eqs env, eqs
| ([a, x], v) -> | ([a, x], v) ->
let b = (minus_num v) // a in let b = (minus_num v) // a in
let i1 = Intervals.point b ty expl in let i1 = Intervals.point b ty expl in
let i2, use2 = let i2, use2 =
try try
MX.find x env.monomes MX.find x env.monomes
with Not_found -> Intervals.undefined ty, SX.empty with Not_found -> Intervals.undefined ty, SX.empty
in in
let i = Intervals.exclude i1 i2 in let i = Intervals.exclude i1 i2 in
@ -541,37 +541,37 @@ module Make
else P.mult (P.create [] (Int (-1)) ty) p in else P.mult (P.create [] (Int (-1)) ty) p in
let p, c, _ = P.normal_form p in let p, c, _ = P.normal_form p in
let i1 = Intervals.point (minus_num c) ty expl in let i1 = Intervals.point (minus_num c) ty expl in
let i2 = let i2 =
try try
MP.find p env.polynomes MP.find p env.polynomes
with Not_found -> Intervals.undefined ty with Not_found -> Intervals.undefined ty
in in
let i = Intervals.exclude i1 i2 in let i = Intervals.exclude i1 i2 in
let env = let env =
if Intervals.is_strict_smaller i i2 then if Intervals.is_strict_smaller i i2 then
let polynomes = MP.add p i env.polynomes in let polynomes = MP.add p i env.polynomes in
let monomes = update_monomes_from_poly p i polynomes env.monomes let monomes = update_monomes_from_poly p i polynomes env.monomes
in in
let improved = SP.add p env.improved in let improved = SP.add p env.improved in
{ env with { env with
polynomes = polynomes; polynomes = polynomes;
monomes = monomes; monomes = monomes;
improved = improved} improved = improved}
else env else env
in in
env, eqs env, eqs
let add_equality env eqs p expl = let add_equality env eqs p expl =
let ty = P.type_info p in let ty = P.type_info p in
match P.to_list p with match P.to_list p with
| ([], Int 0) -> env, eqs | ([], Int 0) -> env, eqs
| ([], v) -> | ([], v) ->
raise (Exception.Inconsistent expl) raise (Exception.Inconsistent expl)
| ([a, x], v) -> | ([a, x], v) ->
let b = (minus_num v) // a in let b = (minus_num v) // a in
let i = Intervals.point b ty expl in let i = Intervals.point b ty expl in
let i, use = let i, use =
try try
let i', use' = MX.find x env.monomes in let i', use' = MX.find x env.monomes in
Intervals.intersect i i', use' Intervals.intersect i i', use'
with Not_found -> i, SX.empty with Not_found -> i, SX.empty
@ -585,26 +585,26 @@ module Make
else P.mult (P.create [] (Int (-1)) ty) p in else P.mult (P.create [] (Int (-1)) ty) p in
let p, c, _ = P.normal_form p in let p, c, _ = P.normal_form p in
let i = Intervals.point (minus_num c) ty expl in let i = Intervals.point (minus_num c) ty expl in
let i, ip = let i, ip =
try try
let ip = MP.find p env.polynomes in let ip = MP.find p env.polynomes in
Intervals.intersect i ip, ip Intervals.intersect i ip, ip
with Not_found -> i, Intervals.undefined ty with Not_found -> i, Intervals.undefined ty
in in
let env = let env =
if Intervals.is_strict_smaller i ip then if Intervals.is_strict_smaller i ip then
let polynomes = MP.add p i env.polynomes in let polynomes = MP.add p i env.polynomes in
let monomes = update_monomes_from_poly p i polynomes env.monomes let monomes = update_monomes_from_poly p i polynomes env.monomes
in in
let improved = SP.add p env.improved in let improved = SP.add p env.improved in
{ env with { env with
polynomes = polynomes; polynomes = polynomes;
monomes = monomes; monomes = monomes;
improved = improved } improved = improved }
else env else env
in in
let env = let env =
{ env with { env with
known_eqs = SX.add (P.alien_of p) env.known_eqs known_eqs = SX.add (P.alien_of p) env.known_eqs
} in } in
env, eqs env, eqs
@ -614,33 +614,33 @@ module Make
let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in
L.Builtin (true, n, [r2; P.alien_of pred_r1]) L.Builtin (true, n, [r2; P.alien_of pred_r1])
| L.Builtin (true, n, [r1; r2]) when | L.Builtin (true, n, [r1; r2]) when
not (is_le n) && X.type_info r1 = Ty.Tint -> not (is_le n) && X.type_info r1 = Ty.Tint ->
let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in
L.Builtin (true, ale, [r1; P.alien_of pred_r2]) L.Builtin (true, ale, [r1; P.alien_of pred_r2])
| L.Builtin (false, n, [r1; r2]) when is_le n -> | L.Builtin (false, n, [r1; r2]) when is_le n ->
L.Builtin (true, alt, [r2; r1]) L.Builtin (true, alt, [r2; r1])
| L.Builtin (false, n, [r1; r2]) when is_lt n -> | L.Builtin (false, n, [r1; r2]) when is_lt n ->
L.Builtin (true, ale, [r2; r1]) L.Builtin (true, ale, [r2; r1])
| _ -> a | _ -> a
let remove_trivial_eqs eqs la = let remove_trivial_eqs eqs la =
let set_of l = let set_of l =
List.fold_left (fun s e -> Seq.add e s) Seq.empty l List.fold_left (fun s e -> Seq.add e s) Seq.empty l
in in
Seq.elements (Seq.diff (set_of eqs) (set_of la)) Seq.elements (Seq.diff (set_of eqs) (set_of la))
let equalities_from_polynomes env eqs = let equalities_from_polynomes env eqs =
let known, eqs = let known, eqs =
MP.fold MP.fold
(fun p i (knw, eqs) -> (fun p i (knw, eqs) ->
let xp = P.alien_of p in let xp = P.alien_of p in
if SX.mem xp knw then knw, eqs if SX.mem xp knw then knw, eqs
else else
match Intervals.is_point i with match Intervals.is_point i with
| Some (num, ex) -> | Some (num, ex) ->
let r2 = P.alien_of (P.create [] num (P.type_info p)) in let r2 = P.alien_of (P.create [] num (P.type_info p)) in
@ -652,11 +652,11 @@ module Make
let equalities_from_monomes env eqs = let equalities_from_monomes env eqs =
let known, eqs = let known, eqs =
MX.fold MX.fold
(fun x (i,_) (knw, eqs) -> (fun x (i,_) (knw, eqs) ->
if SX.mem x knw then knw, eqs if SX.mem x knw then knw, eqs
else else
match Intervals.is_point i with match Intervals.is_point i with
| Some (num, ex) -> | Some (num, ex) ->
let r2 = P.alien_of (P.create [] num (X.type_info x)) in let r2 = P.alien_of (P.create [] num (X.type_info x)) in
@ -692,29 +692,29 @@ module Make
let env = replace_inequation env root ineq in let env = replace_inequation env root ineq in
env, eqs, true, expl env, eqs, true, expl
| L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 -> | L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 ->
let p = P.sub (P.poly_of r1) (P.poly_of r2) in let p = P.sub (P.poly_of r1) (P.poly_of r2) in
let env = init_monomes env p SX.empty expl in let env = init_monomes env p SX.empty expl in
let env, eqs = add_disequality env eqs p expl in let env, eqs = add_disequality env eqs p expl in
env, eqs, new_ineqs, expl env, eqs, new_ineqs, expl
| L.Eq(r1, r2) when is_num r1 && is_num r2 -> | L.Eq(r1, r2) when is_num r1 && is_num r2 ->
let p = P.sub (P.poly_of r1) (P.poly_of r2) in let p = P.sub (P.poly_of r1) (P.poly_of r2) in
let env = init_monomes env p SX.empty expl in let env = init_monomes env p SX.empty expl in
let env, eqs = add_equality env eqs p expl in let env, eqs = add_equality env eqs p expl in
env, eqs, new_ineqs, expl env, eqs, new_ineqs, expl
| _ -> (env, eqs, new_ineqs, expl) | _ -> (env, eqs, new_ineqs, expl)
with Intervals.NotConsistent expl -> with Intervals.NotConsistent expl ->
raise (Exception.Inconsistent expl) raise (Exception.Inconsistent expl)
) )
(env, [], false, Explanation.empty) la (env, [], false, Explanation.empty) la
in in
if new_ineqs then if new_ineqs then
if false then if false then
(); ();
try try
(* we only call fm when new ineqs are assumed *) (* we only call fm when new ineqs are assumed *)
let env, eqs = if new_ineqs then fm env eqs expl else env, eqs in let env, eqs = if new_ineqs then fm env eqs expl else env, eqs in
@ -724,13 +724,13 @@ module Make
Debug.env env; Debug.env env;
let eqs = remove_trivial_eqs eqs la in let eqs = remove_trivial_eqs eqs la in
Debug.implied_equalities eqs; Debug.implied_equalities eqs;
let result = let result =
List.fold_left List.fold_left
(fun r (a_sem, a_term, ex) -> (fun r (a_sem, a_term, ex) ->
{ assume = (LSem(a_sem), ex) :: r.assume; { assume = (LSem(a_sem), ex) :: r.assume;
remove = remove =
match a_term with match a_term with
| None -> r.remove | None -> r.remove
| Some t -> (LTerm(t), ex)::r.remove | Some t -> (LTerm(t), ex)::r.remove
} ) { assume = []; remove = [] } eqs } ) { assume = []; remove = [] } eqs
in in
@ -738,14 +738,14 @@ module Make
with Intervals.NotConsistent expl -> with Intervals.NotConsistent expl ->
raise (Exception.Inconsistent expl) raise (Exception.Inconsistent expl)
let query env a_ex = let query env a_ex =
try try
ignore(assume env [a_ex]); ignore(assume env [a_ex]);
No No
with Exception.Inconsistent expl -> Yes expl with Exception.Inconsistent expl -> Yes expl
let case_split_polynomes env = let case_split_polynomes env =
let o = MP.fold let o = MP.fold
(fun p i o -> (fun p i o ->
match Intervals.finite_size i with match Intervals.finite_size i with
@ -753,21 +753,21 @@ module Make
begin begin
match o with match o with
| Some (s', _, _, _) when s' <=/ s -> o | Some (s', _, _, _) when s' <=/ s -> o
| _ -> | _ ->
let n, ex = Intervals.borne_inf i in let n, ex = Intervals.borne_inf i in
Some (s, p, n, ex) Some (s, p, n, ex)
end end
| _ -> o | _ -> o
) env.polynomes None in ) env.polynomes None in
match o with match o with
| Some (s, p, n, ex) -> | Some (s, p, n, ex) ->
let r1 = P.alien_of p in let r1 = P.alien_of p in
let r2 = P.alien_of (P.create [] n (P.type_info p)) in let r2 = P.alien_of (P.create [] n (P.type_info p)) in
[L.Eq(r1, r2), ex, s] [L.Eq(r1, r2), ex, s]
| None -> | None ->
[] []
let case_split_monomes env = let case_split_monomes env =
let o = MX.fold let o = MX.fold
(fun x (i,_) o -> (fun x (i,_) o ->
match Intervals.finite_size i with match Intervals.finite_size i with
@ -775,26 +775,26 @@ module Make
begin begin
match o with match o with
| Some (s', _, _, _) when s' <=/ s -> o | Some (s', _, _, _) when s' <=/ s -> o
| _ -> | _ ->
let n, ex = Intervals.borne_inf i in let n, ex = Intervals.borne_inf i in
Some (s, x, n, ex) Some (s, x, n, ex)
end end
| _ -> o | _ -> o
) env.monomes None in ) env.monomes None in
match o with match o with
| Some (s,x,n,ex) -> | Some (s,x,n,ex) ->
let ty = X.type_info x in let ty = X.type_info x in
let r1 = x in let r1 = x in
let r2 = P.alien_of (P.create [] n ty) in let r2 = P.alien_of (P.create [] n ty) in
[L.Eq(r1, r2), ex, s] [L.Eq(r1, r2), ex, s]
| None -> | None ->
[] []
let case_split env = let case_split env =
match case_split_polynomes env with match case_split_polynomes env with
| [] -> case_split_monomes env | [] -> case_split_monomes env
| choices -> choices | choices -> choices
let add env _ = env let add env _ = env
let extract_improved env = let extract_improved env =

4
smt/fm.mli
View file

@ -17,7 +17,7 @@ module type EXTENDED_Polynome = sig
val alien_of : t -> r val alien_of : t -> r
end end
module Make module Make
(X : Sig.X) (X : Sig.X)
(P : EXTENDED_Polynome with type r = X.r) (P : EXTENDED_Polynome with type r = X.r)
: Sig.RELATION with type r = X.r : Sig.RELATION with type r = X.r

198
smt/intervals.ml
View file

@ -16,9 +16,9 @@ open Format
module Ex = Explanation module Ex = Explanation
type borne = type borne =
| Strict of (num * Ex.t) | Strict of (num * Ex.t)
| Large of (num * Ex.t) | Large of (num * Ex.t)
| Pinfty | Minfty | Pinfty | Minfty
let compare_bornes b1 b2 = let compare_bornes b1 b2 =
@ -26,33 +26,33 @@ let compare_bornes b1 b2 =
| Minfty, Minfty | Pinfty, Pinfty -> 0 | Minfty, Minfty | Pinfty, Pinfty -> 0
| Minfty, _ | _, Pinfty -> -1 | Minfty, _ | _, Pinfty -> -1
| Pinfty, _ | _, Minfty -> 1 | Pinfty, _ | _, Minfty -> 1
| Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _) | Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _)
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
compare_num v1 v2 compare_num v1 v2
let compare_bu_bl b1 b2 = let compare_bu_bl b1 b2 =
match b1, b2 with match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty) | (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ -> | Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2 compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c = 0 then -1 else c if c = 0 then -1 else c
let compare_bl_bu b1 b2 = let compare_bl_bu b1 b2 =
match b1, b2 with match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty) | (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ -> | Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2 compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) -> | Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c = 0 then 1 else c if c = 0 then 1 else c
let compare_bl_bl b1 b2 = let compare_bl_bl b1 b2 =
match b1, b2 with match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty) | (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ -> | Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2 compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) -> | Strict (v1, _), Large (v2, _) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c = 0 then 1 else c if c = 0 then 1 else c
@ -62,9 +62,9 @@ let compare_bl_bl b1 b2 =
let compare_bu_bu b1 b2 = let compare_bu_bu b1 b2 =
match b1, b2 with match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty) | (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ -> | Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2 compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) -> | Strict (v1, _), Large (v2, _) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c = 0 then -1 else c if c = 0 then -1 else c
@ -72,7 +72,7 @@ let compare_bu_bu b1 b2 =
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c = 0 then 1 else c if c = 0 then 1 else c
type t = { type t = {
ints : (borne * borne) list; ints : (borne * borne) list;
is_int : bool; is_int : bool;
expl: Ex.t expl: Ex.t
@ -83,23 +83,23 @@ exception NotConsistent of Ex.t
exception Not_a_float exception Not_a_float
let print_borne fmt = function let print_borne fmt = function
| Minfty -> fprintf fmt "-inf" | Minfty -> fprintf fmt "-inf"
| Pinfty -> fprintf fmt "+inf" | Pinfty -> fprintf fmt "+inf"
| Strict (v, e) | Large (v, e) -> | 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 print_interval fmt (b1,b2) =
let c1, c2 = match b1, b2 with let c1, c2 = match b1, b2 with
| Large _, Large _ -> '[', ']' | Large _, Large _ -> '[', ']'
| Large _, _ -> '[', '[' | Large _, _ -> '[', '['
| _, Large _ -> ']', ']' | _, Large _ -> ']', ']'
| _, _ -> ']', '[' | _, _ -> ']', '['
in in
fprintf fmt "%c%a;%a%c" c1 print_borne b1 print_borne b2 c2 fprintf fmt "%c%a;%a%c" c1 print_borne b1 print_borne b2 c2
let print fmt {ints = ints; is_int = b; expl = e } = let print fmt {ints = ints; is_int = b; expl = e } =
List.iter (fun i -> fprintf fmt "%a" print_interval i) ints List.iter (fun i -> fprintf fmt "%a" print_interval i) ints
let undefined ty = { let undefined ty = {
ints = [Minfty, Pinfty]; ints = [Minfty, Pinfty];
@ -108,7 +108,7 @@ let undefined ty = {
} }
let point b ty e = { let point b ty e = {
ints = [Large (b, e), Large (b, e)]; ints = [Large (b, e), Large (b, e)];
is_int = ty = Ty.Tint; is_int = ty = Ty.Tint;
expl = Ex.empty expl = Ex.empty
} }
@ -132,7 +132,7 @@ let is_point { ints = l; expl = e } =
| _ -> None | _ -> None
let add_expl_zero i expl = let add_expl_zero i expl =
let res = List.map (fun x -> 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), e1) , Large ((Num.Int 0), e2)) ->
(Large ((Num.Int 0), Ex.union e1 expl), (Large ((Num.Int 0), Ex.union e1 expl),
@ -143,10 +143,10 @@ let add_expl_zero i expl =
let check_one_interval b1 b2 is_int = let check_one_interval b1 b2 is_int =
match b1, b2 with match b1, b2 with
| Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty) | Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty)
| (Strict (v1, e1) | Large (v1,e1)), | (Strict (v1, e1) | Large (v1,e1)),
(Strict (v2, e2) | Large (v2, e2)) -> (Strict (v2, e2) | Large (v2, e2)) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c > 0 then raise if c > 0 then raise
(EmptyInterval (Ex.union e2 e1)); (EmptyInterval (Ex.union e2 e1));
if c = 0 then begin if c = 0 then begin
match b1, b2 with match b1, b2 with
@ -156,7 +156,7 @@ let check_one_interval b1 b2 is_int =
end end
| _ -> () | _ -> ()
let min_borne b1 b2 = let min_borne b1 b2 =
match b1, b2 with match b1, b2 with
| Minfty , _ | _ , Minfty -> Minfty | Minfty , _ | _ , Minfty -> Minfty
| b , Pinfty | Pinfty, b -> b | b , Pinfty | Pinfty, b -> b
@ -164,31 +164,31 @@ let min_borne b1 b2 =
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c < 0 then b1 if c < 0 then b1
else if c > 0 then b2 else if c > 0 then b2
else match b1, b2 with else match b1, b2 with
| (Strict _ as b) , _ | _, (Strict _ as b) -> b | (Strict _ as b) , _ | _, (Strict _ as b) -> b
| _, _ -> b1 | _, _ -> b1
let max_borne b1 b2 = let max_borne b1 b2 =
match b1, b2 with match b1, b2 with
| Pinfty , _ | _ , Pinfty -> Pinfty | Pinfty , _ | _ , Pinfty -> Pinfty
| b , Minfty | Minfty, b -> b | b , Minfty | Minfty, b -> b
| (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) -> | (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) ->
let c = compare_num v1 v2 in let c = compare_num v1 v2 in
if c > 0 then b1 if c > 0 then b1
else if c < 0 then b2 else if c < 0 then b2
else match b1, b2 with else match b1, b2 with
| (Strict _ as b) , _ | _, (Strict _ as b) -> b | (Strict _ as b) , _ | _, (Strict _ as b) -> b
| _, _ -> b1 | _, _ -> b1
let pos_borne b1 = let pos_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) >= 0 compare_bornes b1 (borne_of true Ex.empty (Int 0)) >= 0
let pos_borne_strict b1 = let pos_borne_strict b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) > 0 compare_bornes b1 (borne_of true Ex.empty (Int 0)) > 0
let neg_borne b1 = let neg_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) <= 0 compare_bornes b1 (borne_of true Ex.empty (Int 0)) <= 0
let neg_borne_strict b1 = let neg_borne_strict b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) < 0 compare_bornes b1 (borne_of true Ex.empty (Int 0)) < 0
let zero_borne b1 = let zero_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) = 0 compare_bornes b1 (borne_of true Ex.empty (Int 0)) = 0
exception Found of Sig.answer exception Found of Sig.answer
@ -196,12 +196,12 @@ exception Found of Sig.answer
let doesnt_contain_0 {ints=l} = let doesnt_contain_0 {ints=l} =
try try
let max = List.fold_left let max = List.fold_left
(fun old_u (l, u) -> (fun old_u (l, u) ->
if neg_borne l && pos_borne u then raise (Found Sig.No); if neg_borne l && pos_borne u then raise (Found Sig.No);
if neg_borne_strict old_u && pos_borne_strict l then if neg_borne_strict old_u && pos_borne_strict l then
raise (Found raise (Found
(Sig.Yes (Sig.Yes
(Ex.union (Ex.union
(explain_borne old_u) (explain_borne l)))); (explain_borne old_u) (explain_borne l))));
u) Minfty l in u) Minfty l in
if neg_borne_strict max then Sig.Yes (explain_borne max) if neg_borne_strict max then Sig.Yes (explain_borne max)
@ -219,11 +219,11 @@ let is_strict_smaller i1 i2 =
then raise Exit then raise Exit
) i1 i2; ) i1 i2;
false false
with with
| Exit -> true | Exit -> true
| Invalid_argument _ -> List.length i1 > List.length i2 | Invalid_argument _ -> List.length i1 > List.length i2
let is_strict_smaller {ints=i1} {ints=i2} = let is_strict_smaller {ints=i1} {ints=i2} =
is_strict_smaller i1 i2 is_strict_smaller i1 i2
@ -247,7 +247,7 @@ let add_borne b1 b2 =
| Minfty, Pinfty | Pinfty, Minfty -> assert false | Minfty, Pinfty | Pinfty, Minfty -> assert false
| Minfty, _ | _, Minfty -> Minfty | Minfty, _ | _, Minfty -> Minfty
| Pinfty, _ | _, Pinfty -> Pinfty | Pinfty, _ | _, Pinfty -> Pinfty
| Large (v1, e1), Large (v2, e2) -> | Large (v1, e1), Large (v2, e2) ->
Large (v1 +/ v2, Ex.union e1 e2) Large (v1 +/ v2, Ex.union e1 e2)
| (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) -> | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) ->
Strict (v1 +/ v2, Ex.union e1 e2) Strict (v1 +/ v2, Ex.union e1 e2)
@ -260,9 +260,9 @@ let add_interval l (b1,b2) =
) l [] ) l []
let add {ints = l1; is_int = is_int; expl = e1} {ints = l2; expl = e2}= let add {ints = l1; is_int = is_int; expl = e1} {ints = l2; expl = e2}=
let l = let l =
List.fold_left List.fold_left
(fun l bs -> let i = add_interval l1 bs in i@l) [] l2 (fun l bs -> let i = add_interval l1 bs in i@l) [] l2
in in
union { ints = l ; is_int = is_int; expl = Ex.union e1 e2 } union { ints = l ; is_int = is_int; expl = Ex.union e1 e2 }
@ -274,7 +274,7 @@ let minus_borne = function
let scale_borne n b = let scale_borne n b =
assert (n >=/ Int 0); assert (n >=/ Int 0);
if n =/ Int 0 then if n =/ Int 0 then
match b with match b with
| Pinfty | Minfty -> Large (Int 0, Ex.empty) | Pinfty | Minfty -> Large (Int 0, Ex.empty)
| Large (_, e) | Strict (_, e) -> Large (Int 0, e) | Large (_, e) | Strict (_, e) -> Large (Int 0, e)
@ -293,24 +293,24 @@ let scale_interval n (b1,b2) =
let scale n uints = let scale n uints =
let l = List.map (scale_interval n) uints.ints in let l = List.map (scale_interval n) uints.ints in
union { uints with ints = l; expl = uints.expl } union { uints with ints = l; expl = uints.expl }
let mult_borne b1 b2 = let mult_borne b1 b2 =
match b1,b2 with match b1,b2 with
| Minfty, Pinfty | Pinfty, Minfty -> assert false | Minfty, Pinfty | Pinfty, Minfty -> assert false
| Minfty, b | b, Minfty -> | Minfty, b | b, Minfty ->
if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0
then b then b
else if pos_borne b then Minfty else if pos_borne b then Minfty
else Pinfty else Pinfty
| Pinfty, b | b, Pinfty -> | Pinfty, b | b, Pinfty ->
if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0 if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0
then b then b
else if pos_borne b then Pinfty else if pos_borne b then Pinfty
else Minfty else Minfty
| Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2) | Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2)
| Large (v1, e1), Strict (v2, e2) -> | Large (v1, e1), Strict (v2, e2) ->
Strict (v1 */ v2, Ex.union e1 e2) Strict (v1 */ v2, Ex.union e1 e2)
| Large (v1, e1), Large (v2, e2) -> | Large (v1, e1), Large (v2, e2) ->
Large (v1 */ v2, Ex.union e1 e2) Large (v1 */ v2, Ex.union e1 e2)
let mult_borne_inf b1 b2 = let mult_borne_inf b1 b2 =
@ -323,10 +323,10 @@ let mult_borne_sup b1 b2 =
| Minfty, Pinfty | Pinfty, Minfty -> Pinfty | Minfty, Pinfty | Pinfty, Minfty -> Pinfty
| _, _ -> mult_borne b1 b2 | _, _ -> mult_borne b1 b2
type interval_class = type interval_class =
| P of Ex.t | P of Ex.t
| M of Ex.t | M of Ex.t
| N of Ex.t | N of Ex.t
| Z | Z
let class_of (l,u) = let class_of (l,u) =
@ -338,17 +338,17 @@ let class_of (l,u) =
let mult_bornes (a,b) (c,d) = let mult_bornes (a,b) (c,d) =
(* see util/intervals_mult.png *) (* see util/intervals_mult.png *)
match class_of (a,b), class_of (c,d) with match class_of (a,b), class_of (c,d) with
| P e1, P e2 -> | P e1, P e2 ->
mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2 mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2
| P e1, M e2 -> | P e1, M e2 ->
mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2 mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2
| P e1, N e2 -> | P e1, N e2 ->
mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2 mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2
| M e1, P e2 -> | M e1, P e2 ->
mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2 mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2
| M e1, M e2 -> | M e1, M e2 ->
min_borne (mult_borne_inf a d) (mult_borne_inf b c), min_borne (mult_borne_inf a d) (mult_borne_inf b c),
max_borne (mult_borne_sup a c) (mult_borne_sup b d), max_borne (mult_borne_sup a c) (mult_borne_sup b d),
Ex.union e1 e2 Ex.union e1 e2
| M e1, N e2 -> | M e1, N e2 ->
mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2 mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2
@ -360,7 +360,7 @@ let mult_bornes (a,b) (c,d) =
mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2 mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2
| Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty) | Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty)
| (P _ | M _ | N _ ), Z -> (c, d, Ex.empty) | (P _ | M _ | N _ ), Z -> (c, d, Ex.empty)
let rec power_borne_inf p b = let rec power_borne_inf p b =
match p with match p with
| 1 -> b | 1 -> b
@ -396,14 +396,14 @@ let power_bornes p (b1,b2) =
| p when p mod 2 = 0 -> (power_borne_inf p b2, power_borne_sup p b1) | 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) | _ -> (power_borne_inf p b1, power_borne_sup p b2)
else assert false else assert false
let int_of_borne_inf b = let int_of_borne_inf b =
match b with match b with
| Minfty | Pinfty -> b | Minfty | Pinfty -> b
| Large (v, e) -> Large (ceiling_num v, e) | Large (v, e) -> Large (ceiling_num v, e)
| Strict (v, e) -> | Strict (v, e) ->
let v' = ceiling_num v in let v' = ceiling_num v in
if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e)
let int_of_borne_sup b = let int_of_borne_sup b =
match b with match b with
@ -411,7 +411,7 @@ let int_of_borne_sup b =
| Large (v, e) -> Large (floor_num v, e) | Large (v, e) -> Large (floor_num v, e)
| Strict (v, e) -> | Strict (v, e) ->
let v' = floor_num v in let v' = floor_num v in
if v' </ v then Large (v', e) else Large (v -/ (Int 1), e) if v' </ v then Large (v', e) else Large (v -/ (Int 1), e)
let int_div_of_borne_inf b = let int_div_of_borne_inf b =
match b with match b with
@ -419,7 +419,7 @@ let int_div_of_borne_inf b =
| Large (v, e) -> Large (floor_num v, e) | Large (v, e) -> Large (floor_num v, e)
| Strict (v, e) -> | Strict (v, e) ->
let v' = floor_num v in let v' = floor_num v in
if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e) if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e)
let int_div_of_borne_sup b = let int_div_of_borne_sup b =
match b with match b with
@ -429,10 +429,10 @@ let int_div_of_borne_sup b =
let v' = floor_num v in let v' = floor_num v in
if v' </ v then Large (v', e) else Large (v -/ (Int 1), e) if v' </ v then Large (v', e) else Large (v -/ (Int 1), e)
let int_bornes l u = let int_bornes l u =
int_of_borne_inf l, int_of_borne_sup u int_of_borne_inf l, int_of_borne_sup u
let int_div_bornes l u = let int_div_bornes l u =
int_div_of_borne_inf l, int_div_of_borne_sup u int_div_of_borne_inf l, int_div_of_borne_sup u
@ -442,7 +442,7 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
let rec step (l1,l2) acc expl = let rec step (l1,l2) acc expl =
match l1, l2 with match l1, l2 with
| (lo1,up1)::r1, (lo2,up2)::r2 -> | (lo1,up1)::r1, (lo2,up2)::r2 ->
let (lo1,up1), (lo2,up2) = let (lo1,up1), (lo2,up2) =
if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2) if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2)
else (lo1,up1), (lo2,up2) in else (lo1,up1), (lo2,up2) in
let cll = compare_bl_bl lo1 lo2 in let cll = compare_bl_bl lo1 lo2 in
@ -457,7 +457,7 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
let lor1 = add_expl_to_borne lor1 nexpl in let lor1 = add_expl_to_borne lor1 nexpl in
let r1 = (lor1,upr1)::rr1 in let r1 = (lor1,upr1)::rr1 in
step (r1, l2) acc expl step (r1, l2) acc expl
else if clu > 0 then else if clu > 0 then
let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in
match r2 with match r2 with
| [] -> step (l1, r2) acc (Ex.union nexpl expl) | [] -> step (l1, r2) acc (Ex.union nexpl expl)
@ -465,15 +465,15 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
let lor2 = add_expl_to_borne lor2 nexpl in let lor2 = add_expl_to_borne lor2 nexpl in
let r2 = (lor2,upr2)::rr2 in let r2 = (lor2,upr2)::rr2 in
step (l1, r2) acc expl step (l1, r2) acc expl
else if cll = 0 && cuu = 0 then else if cll = 0 && cuu = 0 then
step (r1, r2) ((lo1,up1)::acc) expl step (r1, r2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu >= 0 then else if cll <= 0 && cuu >= 0 then
step (l1, r2) ((lo2,up2)::acc) expl step (l1, r2) ((lo2,up2)::acc) expl
else if cll >= 0 && cuu <= 0 then else if cll >= 0 && cuu <= 0 then
step (r1, l2) ((lo1,up1)::acc) expl step (r1, l2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu <= 0 && cul >= 0 then else if cll <= 0 && cuu <= 0 && cul >= 0 then
step (r1, l2) ((lo2,up1)::acc) expl step (r1, l2) ((lo2,up1)::acc) expl
else if cll >= 0 && cuu >= 0 && clu <= 0 then else if cll >= 0 && cuu >= 0 && clu <= 0 then
step (l1, r2) ((lo1,up2)::acc) expl step (l1, r2) ((lo1,up2)::acc) expl
else assert false else assert false
| [], _ | _, [] -> List.rev acc, expl | [], _ | _, [] -> List.rev acc, expl
@ -484,13 +484,13 @@ let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
let new_borne_sup expl b ~is_le uints = let new_borne_sup expl b ~is_le uints =
intersect intersect
{ ints = [Minfty, (borne_of is_le expl b)]; { ints = [Minfty, (borne_of is_le expl b)];
is_int = uints.is_int; is_int = uints.is_int;
expl = Ex.empty } uints expl = Ex.empty } uints
let new_borne_inf expl b ~is_le uints = let new_borne_inf expl b ~is_le uints =
intersect intersect
{ ints = [(borne_of is_le expl b), Pinfty]; { ints = [(borne_of is_le expl b), Pinfty];
is_int = uints.is_int; is_int = uints.is_int;
expl = Ex.empty } uints expl = Ex.empty } uints
@ -509,28 +509,28 @@ let complement ({ints=l; expl=e} as uints) =
| _ -> b2 in | _ -> b2 in
if bu = Minfty then step r bl acc if bu = Minfty then step r bl acc
else step r bl ((prev, bu)::acc) else step r bl ((prev, bu)::acc)
| [] -> | [] ->
if prev = Pinfty then List.rev acc if prev = Pinfty then List.rev acc
else List.rev ((prev, Pinfty)::acc) else List.rev ((prev, Pinfty)::acc)
in in
{ uints with ints = step l Minfty [] } { uints with ints = step l Minfty [] }
let exclude uints1 uints2 = let exclude uints1 uints2 =
intersect (complement uints1) uints2 intersect (complement uints1) uints2
let mult u1 u2 = let mult u1 u2 =
let resl, expl = let resl, expl =
List.fold_left List.fold_left
(fun (l', expl) b1 -> (fun (l', expl) b1 ->
List.fold_left List.fold_left
(fun (l, ex) b2 -> (fun (l, ex) b2 ->
let bl, bu, ex' = mult_bornes b1 b2 in let bl, bu, ex' = mult_bornes b1 b2 in
(bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints) (bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints)
([], Ex.empty) u1.ints ([], Ex.empty) u1.ints
in in
union { ints=resl; is_int = u1.is_int; union { ints=resl; is_int = u1.is_int;
expl = Ex.union expl expl = Ex.union expl
(Ex.union u1.expl u2.expl) } (Ex.union u1.expl u2.expl) }
let power n u = let power n u =
@ -553,7 +553,7 @@ let num_of_float x =
let factor = (Int 2) **/ (Int (n - 52)) in let factor = (Int 2) **/ (Int (n - 52)) in
(Big_int z) */ factor (Big_int z) */ factor
let root_num a n = let root_num a n =
if a </ (Int 0) then assert false if a </ (Int 0) then assert false
else if a =/ (Int 0) then (Int 0) else if a =/ (Int 0) then (Int 0)
else if n = 2 then num_of_float (sqrt (float_of_num a)) else if n = 2 then num_of_float (sqrt (float_of_num a))
@ -629,7 +629,7 @@ let rec root n ({ints = l; is_int = is_int; expl = e} as u) =
(root_interval is_int bs n)@l' (root_interval is_int bs n)@l'
) [] l in ) [] l in
union { ints = l; is_int = is_int; expl = e } union { ints = l; is_int = is_int; expl = e }
let finite_size {ints = l; is_int = is_int} = let finite_size {ints = l; is_int = is_int} =
if (not is_int) then None if (not is_int) then None
else else
@ -644,7 +644,7 @@ let finite_size {ints = l; is_int = is_int} =
) (Int 0) l in ) (Int 0) l in
Some n Some n
with Exit -> None with Exit -> None
let borne_inf = function let borne_inf = function
| {ints = (Large (v, ex), _)::_} -> v, ex | {ints = (Large (v, ex), _)::_} -> v, ex
| _ -> invalid_arg "Intervals.borne_inf : No finite lower bound" | _ -> invalid_arg "Intervals.borne_inf : No finite lower bound"
@ -655,7 +655,7 @@ let inv_borne_inf b is_int ~other =
match b with match b with
| Pinfty -> assert false | Pinfty -> assert false
| Minfty -> | Minfty ->
if is_int then Large (Int 0, explain_borne other) if is_int then Large (Int 0, explain_borne other)
else Strict (Int 0, explain_borne other) else Strict (Int 0, explain_borne other)
| Strict (Int 0, e) | Large (Int 0, e) -> Pinfty | Strict (Int 0, e) | Large (Int 0, e) -> Pinfty
| Strict (v, e) -> Strict (Int 1 // v, e) | Strict (v, e) -> Strict (Int 1 // v, e)
@ -677,10 +677,10 @@ let inv_bornes (l, u) is_int =
let inv ({ints=l; is_int=is_int} as u) = let inv ({ints=l; is_int=is_int} as u) =
try try
let l' = List.fold_left let l' = List.fold_left
(fun acc (l,u) -> (fun acc (l,u) ->
if (pos_borne_strict l && pos_borne_strict u) if (pos_borne_strict l && pos_borne_strict u)
|| (neg_borne_strict l && neg_borne_strict u) then || (neg_borne_strict l && neg_borne_strict u) then
(inv_bornes (l, u) is_int) :: acc (inv_bornes (l, u) is_int) :: acc
else raise Exit else raise Exit
) [] l in ) [] l in
@ -696,8 +696,8 @@ let div i1 i2 =
| Sig.No -> i1 | Sig.No -> i1
in in
let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in
let l = let l =
if is_int then 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 else l in
{ i with ints = l } { i with ints = l }

2
smt/intervals.mli
View file

@ -42,7 +42,7 @@ val power : int -> t -> t
val sqrt : t -> t val sqrt : t -> t
val root : int -> t -> t val root : int -> t -> t
val add : t -> t -> t val add : t -> t -> t

78
smt/literal.ml
View file

@ -13,8 +13,8 @@
open Hashcons open Hashcons
type 'a view = type 'a view =
| Eq of 'a * 'a | Eq of 'a * 'a
| Distinct of bool * 'a list | Distinct of bool * 'a list
| Builtin of bool * Hstring.t * 'a list | Builtin of bool * Hstring.t * 'a list
@ -45,7 +45,7 @@ module type S = sig
module Map : Map.S with type key = t module Map : Map.S with type key = t
module Set : Set.S with type elt = t module Set : Set.S with type elt = t
end end
module Make (X : OrderedType) : S with type elt = X.t = struct module Make (X : OrderedType) : S with type elt = X.t = struct
@ -53,36 +53,36 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
type elt = X.t type elt = X.t
type t = (X.t view) hash_consed type t = (X.t view) hash_consed
module V = struct module V = struct
type t = X.t view type t = X.t view
let equal a1 a2 = let equal a1 a2 =
match a1, a2 with match a1, a2 with
| Eq(t1, t2), Eq(u1, u2) -> | Eq(t1, t2), Eq(u1, u2) ->
(X.compare t1 u1 = 0 && X.compare t2 u2 = 0) || (X.compare t1 u1 = 0 && X.compare t2 u2 = 0) ||
(X.compare t1 u2 = 0 && X.compare t2 u1 = 0) (X.compare t1 u2 = 0 && X.compare t2 u1 = 0)
| Distinct (b1,lt1), Distinct (b2,lt2) -> | Distinct (b1,lt1), Distinct (b2,lt2) ->
(try (try
b1 = b2 && b1 = b2 &&
List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2 List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2
with Invalid_argument _ -> false) with Invalid_argument _ -> false)
| Builtin(b1, n1, l1), Builtin(b2, n2, l2) -> | Builtin(b1, n1, l1), Builtin(b2, n2, l2) ->
(try (try
b1 = b2 && Hstring.equal n1 n2 b1 = b2 && Hstring.equal n1 n2
&& &&
List.for_all2 (fun x y -> X.compare x y = 0) l1 l2 List.for_all2 (fun x y -> X.compare x y = 0) l1 l2
with Invalid_argument _ -> false) with Invalid_argument _ -> false)
| _ -> false | _ -> false
let hash a = match a with let hash a = match a with
| Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2)) | Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2))
| Distinct (b,lt) -> | Distinct (b,lt) ->
let x = if b then 7 else 23 in let x = if b then 7 else 23 in
abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt) abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt)
| Builtin(b, n, l) -> | Builtin(b, n, l) ->
let x = if b then 7 else 23 in let x = if b then 7 else 23 in
abs abs
(List.fold_left (List.fold_left
(fun acc t-> acc*13 + X.hash t) (Hstring.hash n+x) l) (fun acc t-> acc*13 + X.hash t) (Hstring.hash n+x) l)
end end
@ -92,9 +92,9 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
let equal a1 a2 = a1 == a2 let equal a1 a2 = a1 == a2
let hash a1 = a1.tag let hash a1 = a1.tag
module T = struct module T = struct
type t' = t type t' = t
type t = t' type t = t'
let compare=compare let compare=compare
let equal = equal let equal = equal
let hash = hash let hash = hash
@ -112,11 +112,11 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
| Builtin(b, n, l) -> make (Builtin (not b, n, l)) | Builtin(b, n, l) -> make (Builtin (not b, n, l))
module Labels = Hashtbl.Make(T) module Labels = Hashtbl.Make(T)
let labels = Labels.create 100007 let labels = Labels.create 100007
let add_label lbl t = Labels.replace labels t lbl let add_label lbl t = Labels.replace labels t lbl
let label t = try Labels.find labels t with Not_found -> Hstring.empty let label t = try Labels.find labels t with Not_found -> Hstring.empty
let print_list fmt = function let print_list fmt = function
@ -124,18 +124,18 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
| z :: l -> | z :: l ->
Format.fprintf fmt "%a" X.print z; Format.fprintf fmt "%a" X.print z;
List.iter (Format.fprintf fmt ", %a" X.print) l List.iter (Format.fprintf fmt ", %a" X.print) l
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = Hstring.make "<" let alt = Hstring.make "<"
let print fmt a = let print fmt a =
let lbl = Hstring.view (label a) in let lbl = Hstring.view (label a) in
let lbl = if lbl = "" then lbl else lbl^":" in let lbl = if lbl = "" then lbl else lbl^":" in
match view a with match view a with
| Eq (z1, z2) -> | Eq (z1, z2) ->
if equal z1 z2 then Format.fprintf fmt "True" if equal z1 z2 then Format.fprintf fmt "True"
else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2 else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2
| Distinct (b,(z::l)) -> | Distinct (b,(z::l)) ->
let b = if b then "~" else "" in let b = if b then "~" else "" in
Format.fprintf fmt "%s%s%a" lbl b X.print z; Format.fprintf fmt "%s%s%a" lbl b X.print z;
List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l
@ -156,7 +156,7 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
let b = if b then "" else "~" in let b = if b then "" else "~" in
Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view n) print_list l Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view n) print_list l
| _ -> assert false | _ -> assert false
module Set = Set.Make(T) module Set = Set.Make(T)
module Map = Map.Make(T) module Map = Map.Make(T)
@ -182,28 +182,28 @@ module LT : S_Term = struct
module L = Make(Term) module L = Make(Term)
include L include L
let mk_pred t = make (Eq (t, Term.vrai) ) let mk_pred t = make (Eq (t, Term.vrai) )
let vrai = mk_pred Term.vrai let vrai = mk_pred Term.vrai
let faux = mk_pred Term.faux let faux = mk_pred Term.faux
let neg a = match view a with let neg a = match view a with
| Eq(t1, t2) when Term.equal t2 Term.faux -> | Eq(t1, t2) when Term.equal t2 Term.faux ->
make (Eq (t1, Term.vrai)) make (Eq (t1, Term.vrai))
| Eq(t1, t2) when Term.equal t2 Term.vrai -> | Eq(t1, t2) when Term.equal t2 Term.vrai ->
make (Eq (t1, Term.faux)) make (Eq (t1, Term.faux))
| _ -> L.neg a | _ -> L.neg a
(* let terms_of a = (* let terms_of a =
let l = match view a with let l = match view a with
| Eq (t1, t2) -> [t1; t2] | Eq (t1, t2) -> [t1; t2]
| Distinct (_, l) | Builtin (_, _, l) -> l | Distinct (_, l) | Builtin (_, _, l) -> l
in in
List.fold_left Term.subterms Term.Set.empty l List.fold_left Term.subterms Term.Set.empty l
*) *)
module SS = Symbols.Set module SS = Symbols.Set
(* let vars_of a = (* let vars_of a =
Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty
*) *)
end end

4
smt/literal.mli
View file

@ -18,8 +18,8 @@ module type OrderedType = sig
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
end end
type 'a view = type 'a view =
| Eq of 'a * 'a | Eq of 'a * 'a
| Distinct of bool * 'a list | Distinct of bool * 'a list
| Builtin of bool * Hstring.t * 'a list | Builtin of bool * Hstring.t * 'a list

100
smt/polynome.ml
View file

@ -47,7 +47,7 @@ module type T = sig
val subst : r -> t -> t -> t val subst : r -> t -> t -> t
val remove : r -> t -> t val remove : r -> t -> t
val to_list : t -> (num * r) list * num val to_list : t -> (num * r) list * num
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
val type_info : t -> Ty.t val type_info : t -> Ty.t
val is_monomial : t -> (num * r * num) option val is_monomial : t -> (num * r * num) option
@ -61,41 +61,41 @@ end
module Make (X : S) = struct module Make (X : S) = struct
type r = X.r type r = X.r
module M : Map.S with type key = r = module M : Map.S with type key = r =
Map.Make(struct type t = r let compare x y = X.compare y x end) Map.Make(struct type t = r let compare x y = X.compare y x end)
type t = { m : num M.t; c : num; ty : Ty.t } type t = { m : num M.t; c : num; ty : Ty.t }
let compare p1 p2 = let compare p1 p2 =
let c = Ty.compare p1.ty p2.ty in let c = Ty.compare p1.ty p2.ty in
if c <> 0 then c if c <> 0 then c
else else
let c = compare_num p1.c p2.c in let c = compare_num p1.c p2.c in
if c = 0 then M.compare compare_num p1.m p2.m else c if c = 0 then M.compare compare_num p1.m p2.m else c
let hash p = let hash p =
abs (Hashtbl.hash p.m + 19*Hashtbl.hash p.c + 17 * Ty.hash p.ty) abs (Hashtbl.hash p.m + 19*Hashtbl.hash p.c + 17 * Ty.hash p.ty)
let pprint fmt p = let pprint fmt p =
M.iter M.iter
(fun x n -> (fun x n ->
let s, n, op = match n with let s, n, op = match n with
| Int 1 -> "+", "", "" | Int 1 -> "+", "", ""
| Int -1 -> "-", "", "" | Int -1 -> "-", "", ""
| n -> | n ->
if n >/ Int 0 then "+", string_of_num n, "*" if n >/ Int 0 then "+", string_of_num n, "*"
else "-", string_of_num (minus_num n), "*" else "-", string_of_num (minus_num n), "*"
in in
fprintf fmt "%s%s%s%a" s n op X.print x fprintf fmt "%s%s%s%a" s n op X.print x
)p.m; )p.m;
let s, n = if p.c >=/ Int 0 then "+", string_of_num p.c let s, n = if p.c >=/ Int 0 then "+", string_of_num p.c
else "-", string_of_num (minus_num p.c) in else "-", string_of_num (minus_num p.c) in
fprintf fmt "%s%s" s n fprintf fmt "%s%s" s n
let print fmt p = let print fmt p =
M.iter M.iter
(fun t n -> fprintf fmt "%s*%a " (string_of_num n) X.print t) p.m; (fun t n -> fprintf fmt "%s*%a " (string_of_num n) X.print t) p.m;
fprintf fmt "%s" (string_of_num p.c); fprintf fmt "%s" (string_of_num p.c);
fprintf fmt " [%a]" Ty.print p.ty fprintf fmt " [%a]" Ty.print p.ty
@ -104,38 +104,38 @@ module Make (X : S) = struct
let find x m = try M.find x m with Not_found -> Int 0 let find x m = try M.find x m with Not_found -> Int 0
let create l c ty = let create l c ty =
let m = let m =
List.fold_left List.fold_left
(fun m (n, x) -> (fun m (n, x) ->
let n' = n +/ (find x m) in 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 if n' =/ (Int 0) then M.remove x m else M.add x n' m) M.empty l
in in
{ m = m; c = c; ty = ty } { m = m; c = c; ty = ty }
let add p1 p2 = let add p1 p2 =
let m = let m =
M.fold M.fold
(fun x a m -> (fun x a m ->
let a' = (find x m) +/ a in let a' = (find x m) +/ a in
if a' =/ (Int 0) then M.remove x m else M.add x a' m) if a' =/ (Int 0) then M.remove x m else M.add x a' m)
p2.m p1.m p2.m p1.m
in in
{ m = m; c = p1.c +/ p2.c; ty = p1.ty } { m = m; c = p1.c +/ p2.c; ty = p1.ty }
let mult_const n p = let mult_const n p =
if n =/ (Int 0) then { m = M.empty; c = Int 0; ty = p.ty } if n =/ (Int 0) then { m = M.empty; c = Int 0; ty = p.ty }
else { p with m = M.map (mult_num n) p.m; c = n */ p.c } else { p with m = M.map (mult_num n) p.m; c = n */ p.c }
let mult_monome a x p = let mult_monome a x p =
let ax = { m = M.add x a M.empty; c = (Int 0); ty = p.ty} in let ax = { m = M.add x a M.empty; c = (Int 0); ty = p.ty} in
let acx = mult_const p.c ax in let acx = mult_const p.c ax in
let m = let m =
M.fold 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 in
{ acx with m = m} { acx with m = m}
let mult p1 p2 = let mult p1 p2 =
let p = mult_const p1.c p2 in let p = mult_const p1.c p2 in
M.fold (fun x a p -> add (mult_monome a x p2) p) p1.m p M.fold (fun x a p -> add (mult_monome a x p2) p) p1.m p
@ -146,10 +146,10 @@ module Make (X : S) = struct
let div p1 p2 = let div p1 p2 =
if M.is_empty p2.m then if M.is_empty p2.m then
if p2.c =/ Int 0 then raise Division_by_zero if p2.c =/ Int 0 then raise Division_by_zero
else else
let p = mult_const ((Int 1) // p2.c) p1 in let p = mult_const ((Int 1) // p2.c) p1 in
match M.is_empty p.m, p.ty with match M.is_empty p.m, p.ty with
| true, Ty.Tint -> {p with c = floor_num p.c}, false | true, Ty.Tint -> {p with c = floor_num p.c}, false
| true, Ty.Treal -> p, false | true, Ty.Treal -> p, false
| false, Ty.Tint -> p, true | false, Ty.Tint -> p, true
| false, Ty.Treal -> p, false | false, Ty.Treal -> p, false
@ -160,11 +160,11 @@ module Make (X : S) = struct
let modulo p1 p2 = let modulo p1 p2 =
if M.is_empty p2.m then if M.is_empty p2.m then
if p2.c =/ Int 0 then raise Division_by_zero if p2.c =/ Int 0 then raise Division_by_zero
else else
if M.is_empty p1.m then { p1 with c = mod_num p1.c p2.c } if M.is_empty p1.m then { p1 with c = mod_num p1.c p2.c }
else raise Not_a_num else raise Not_a_num
else raise Maybe_zero else raise Maybe_zero
let find x p = M.find x p.m let find x p = M.find x p.m
let is_empty p = M.is_empty p.m let is_empty p = M.is_empty p.m
@ -174,7 +174,7 @@ module Make (X : S) = struct
(*version I : prend le premier element de la table*) (*version I : prend le premier element de la table*)
(try M.iter (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 (*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 match !tn with Some p -> p | _ -> raise Not_found
@ -183,19 +183,19 @@ module Make (X : S) = struct
let a = M.find x p2.m in let a = M.find x p2.m in
add (mult_const a p1) { p2 with m = M.remove x p2.m} add (mult_const a p1) { p2 with m = M.remove x p2.m}
with Not_found -> p2 with Not_found -> p2
let remove x p = { p with m = M.remove x p.m } let remove x p = { p with m = M.remove x p.m }
let to_list p = let to_list p =
let l = M.fold (fun x a aliens -> (a, x)::aliens ) p.m [] in let l = M.fold (fun x a aliens -> (a, x)::aliens ) p.m [] in
List.rev l, p.c List.rev l, p.c
let type_info p = p.ty let type_info p = p.ty
let is_monomial p = let is_monomial p =
try try
M.fold M.fold
(fun x a r -> (fun x a r ->
match r with match r with
| None -> Some (a, x, p.c) | None -> Some (a, x, p.c)
| _ -> raise Exit) | _ -> raise Exit)
@ -207,37 +207,37 @@ module Make (X : S) = struct
| Num.Ratio rat -> Ratio.denominator_ratio rat | Num.Ratio rat -> Ratio.denominator_ratio rat
let numerator = function let numerator = function
| Num.Int i -> Big_int.big_int_of_int i | Num.Int i -> Big_int.big_int_of_int i
| Num.Big_int b -> b | Num.Big_int b -> b
| Num.Ratio rat -> Ratio.numerator_ratio rat | Num.Ratio rat -> Ratio.numerator_ratio rat
let pgcd_bi a b = Big_int.gcd_big_int a b let pgcd_bi a b = Big_int.gcd_big_int a b
let ppmc_bi a b = Big_int.div_big_int (Big_int.mult_big_int a b) (pgcd_bi a b) let ppmc_bi a b = Big_int.div_big_int (Big_int.mult_big_int a b) (pgcd_bi a b)
let abs_big_int_to_num b = let abs_big_int_to_num b =
let b = let b =
try Int (Big_int.int_of_big_int b) try Int (Big_int.int_of_big_int b)
with Failure "int_of_big_int" -> Big_int b with Failure "int_of_big_int" -> Big_int b
in in
abs_num b abs_num b
let ppmc_denominators {m=m} = let ppmc_denominators {m=m} =
let res = let res =
M.fold M.fold
(fun k c acc -> ppmc_bi (denominator c) acc) (fun k c acc -> ppmc_bi (denominator c) acc)
m Big_int.unit_big_int in m Big_int.unit_big_int in
abs_num (num_of_big_int res) abs_num (num_of_big_int res)
let pgcd_numerators {m=m} = let pgcd_numerators {m=m} =
let res = let res =
M.fold M.fold
(fun k c acc -> pgcd_bi (numerator c) acc) (fun k c acc -> pgcd_bi (numerator c) acc)
m Big_int.zero_big_int in m Big_int.zero_big_int in
abs_num (num_of_big_int res) abs_num (num_of_big_int res)
let normal_form ({ m = m; c = c } as p) = let normal_form ({ m = m; c = c } as p) =
if M.is_empty m then if M.is_empty m then
{ p with c = Int 0 }, p.c, (Int 1) { p with c = Int 0 }, p.c, (Int 1)
else else
let ppcm = ppmc_denominators p in let ppcm = ppmc_denominators p in

10
smt/polynome.mli
View file

@ -18,7 +18,7 @@ exception Not_a_num
exception Maybe_zero exception Maybe_zero
module type S = sig module type S = sig
type r type r
val compare : r -> r-> int val compare : r -> r-> int
val term_embed : Term.t -> r val term_embed : Term.t -> r
val mult : r -> r -> r val mult : r -> r -> r
@ -27,9 +27,9 @@ end
module type T = sig module type T = sig
type r type r
type t type t
val compare : t -> t -> int val compare : t -> t -> int
val hash : t -> int val hash : t -> int
@ -47,7 +47,7 @@ module type T = sig
val subst : r -> t -> t -> t val subst : r -> t -> t -> t
val remove : r -> t -> t val remove : r -> t -> t
val to_list : t -> (num * r) list * num val to_list : t -> (num * r) list * num
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
val type_info : t -> Ty.t val type_info : t -> Ty.t
val is_monomial : t -> (num * r * num) option val is_monomial : t -> (num * r * num) option
@ -56,7 +56,7 @@ module type T = sig
val ppmc_denominators : t -> num val ppmc_denominators : t -> num
(* PGCD des numerateurs des coefficients excepte la constante *) (* PGCD des numerateurs des coefficients excepte la constante *)
val pgcd_numerators : t -> num val pgcd_numerators : t -> num
(* retourne un polynome sans constante et sa constante (* retourne un polynome sans constante et sa constante
et la constante multiplicative: et la constante multiplicative:
normal_form p = (p',c,d) <=> p = (p' + c) * d *) normal_form p = (p',c,d) <=> p = (p' + c) * d *)
val normal_form : t -> t * num * num val normal_form : t -> t * num * num

34
smt/sig.mli
View file

@ -15,11 +15,11 @@ type answer = Yes of Explanation.t | No
type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t
type 'a input = type 'a input =
'a Literal.view * Literal.LT.t option * Explanation.t 'a Literal.view * Literal.LT.t option * Explanation.t
type 'a result = { type 'a result = {
assume : ('a literal * Explanation.t) list; assume : ('a literal * Explanation.t) list;
remove: ('a literal * Explanation.t) list; remove: ('a literal * Explanation.t) list;
} }
@ -28,14 +28,14 @@ module type RELATION = sig
type r type r
val empty : unit -> t val empty : unit -> t
val assume : t -> (r input) list -> t * r result val assume : t -> (r input) list -> t * r result
val query : t -> r input -> answer val query : t -> r input -> answer
val case_split : t -> (r Literal.view * Explanation.t * Num.num) list 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 val add : t -> r -> t
(** add a representant to take into account *) (** add a representant to take into account *)
@ -64,7 +64,7 @@ module type THEORY = sig
val term_extract : r -> Term.t option val term_extract : r -> Term.t option
val type_info : t -> Ty.t val type_info : t -> Ty.t
val embed : r -> t val embed : r -> t
(** Give the leaves of a term of the theory *) (** Give the leaves of a term of the theory *)
@ -108,31 +108,31 @@ module type X = sig
type r type r
val make : Term.t -> r * Literal.LT.t list val make : Term.t -> r * Literal.LT.t list
val type_info : r -> Ty.t val type_info : r -> Ty.t
val compare : r -> r -> int val compare : r -> r -> int
val equal : r -> r -> bool val equal : r -> r -> bool
val hash : r -> int val hash : r -> int
val leaves : r -> r list val leaves : r -> r list
val subst : r -> r -> r -> r val subst : r -> r -> r -> r
val solve : r -> r -> (r * r) list val solve : r -> r -> (r * r) list
val term_embed : Term.t -> r val term_embed : Term.t -> r
val term_extract : r -> Term.t option val term_extract : r -> Term.t option
val unsolvable : r -> bool val unsolvable : r -> bool
val fully_interpreted : Symbols.t -> bool val fully_interpreted : Symbols.t -> bool
val print : Format.formatter -> r -> unit val print : Format.formatter -> r -> unit
module Rel : RELATION with type r = r module Rel : RELATION with type r = r
end end

270
smt/smt.ml
View file

@ -12,7 +12,7 @@
open Format open Format
type error = type error =
| DuplicateTypeName of Hstring.t | DuplicateTypeName of Hstring.t
| DuplicateSymb of Hstring.t | DuplicateSymb of Hstring.t
| UnknownType of Hstring.t | UnknownType of Hstring.t
@ -36,37 +36,37 @@ module Type = struct
let equal = Hstring.equal let equal = Hstring.equal
let type_int = let type_int =
let tint = Hstring.make "int" in let tint = Hstring.make "int" in
H.add decl_types tint Ty.Tint; H.add decl_types tint Ty.Tint;
tint tint
let type_real = let type_real =
let treal = Hstring.make "real" in let treal = Hstring.make "real" in
H.add decl_types treal Ty.Treal; H.add decl_types treal Ty.Treal;
treal treal
let type_bool = let type_bool =
let tbool = Hstring.make "bool" in let tbool = Hstring.make "bool" in
H.add decl_types tbool Ty.Tbool; H.add decl_types tbool Ty.Tbool;
tbool tbool
let type_proc = let type_proc =
let tproc = Hstring.make "proc" in let tproc = Hstring.make "proc" in
H.add decl_types tproc Ty.Tint; H.add decl_types tproc Ty.Tint;
tproc tproc
let declare_constructor ty c = let declare_constructor ty c =
if H.mem decl_symbs c then raise (Error (DuplicateSymb c)); if H.mem decl_symbs c then raise (Error (DuplicateSymb c));
H.add decl_symbs c H.add decl_symbs c
(Symbols.name ~kind:Symbols.Constructor c, [], ty) (Symbols.name ~kind:Symbols.Constructor c, [], ty)
let declare t constrs = let declare t constrs =
if H.mem decl_types t then raise (Error (DuplicateTypeName t)); if H.mem decl_types t then raise (Error (DuplicateTypeName t));
match constrs with match constrs with
| [] -> | [] ->
H.add decl_types t (Ty.Tabstract t) H.add decl_types t (Ty.Tabstract t)
| _ -> | _ ->
let ty = Ty.Tsum (t, constrs) in let ty = Ty.Tsum (t, constrs) in
H.add decl_types t ty; H.add decl_types t ty;
List.iter (fun c -> declare_constructor t c) constrs List.iter (fun c -> declare_constructor t c) constrs
@ -82,29 +82,29 @@ module Type = struct
else match H.find decl_types ty with else match H.find decl_types ty with
| Ty.Tsum (_ , cstrs) -> cstrs | Ty.Tsum (_ , cstrs) -> cstrs
| _ -> raise Not_found | _ -> raise Not_found
end end
module Symbol = struct module Symbol = struct
type t = Hstring.t type t = Hstring.t
let declare f args ret = let declare f args ret =
if H.mem decl_symbs f then raise (Error (DuplicateTypeName f)); if H.mem decl_symbs f then raise (Error (DuplicateTypeName f));
List.iter List.iter
(fun t -> (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); (ret::args);
H.add decl_symbs f (Symbols.name f, args, ret) H.add decl_symbs f (Symbols.name f, args, ret)
let type_of s = let _, args, ret = H.find decl_symbs s in args, ret let type_of s = let _, args, ret = H.find decl_symbs s in args, ret
let declared s = let declared s =
let res = H.mem decl_symbs s in let res = H.mem decl_symbs s in
if not res then begin if not res then begin
eprintf "Not declared : %a in@." Hstring.print s; eprintf "Not declared : %a in@." Hstring.print s;
H.iter (fun hs (sy, _, _) -> H.iter (fun hs (sy, _, _) ->
eprintf "%a (=?%b) -> %a@." Hstring.print hs eprintf "%a (=?%b) -> %a@." Hstring.print hs
(Hstring.compare hs s = 0) (Hstring.compare hs s = 0)
Symbols.print sy) Symbols.print sy)
decl_symbs; decl_symbs;
@ -114,49 +114,49 @@ module Symbol = struct
let not_builtin ty = Hstring.equal ty Type.type_proc || let not_builtin ty = Hstring.equal ty Type.type_proc ||
not (Hstring.equal ty Type.type_int || Hstring.equal ty Type.type_real || 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) Hstring.equal ty Type.type_bool || Hstring.equal ty Type.type_proc)
let has_abstract_type s = let has_abstract_type s =
let _, ret = type_of s in let _, ret = type_of s in
match H.find decl_types ret with match H.find decl_types ret with
| Ty.Tabstract _ -> true | Ty.Tabstract _ -> true
| _ -> false | _ -> false
let has_type_proc s = let has_type_proc s =
Hstring.equal (snd (type_of s)) Type.type_proc Hstring.equal (snd (type_of s)) Type.type_proc
let _ = let _ =
H.add decl_symbs htrue (Symbols.True, [], Type.type_bool); H.add decl_symbs htrue (Symbols.True, [], Type.type_bool);
H.add decl_symbs hfalse (Symbols.False, [], Type.type_bool); H.add decl_symbs hfalse (Symbols.False, [], Type.type_bool);
end end
module Variant = struct module Variant = struct
let constructors = H.create 17 let constructors = H.create 17
let assignments = H.create 17 let assignments = H.create 17
let find t x = try H.find t x with Not_found -> HSet.empty let find t x = try H.find t x with Not_found -> HSet.empty
let add t x v = let add t x v =
let s = find t x in let s = find t x in
H.replace t x (HSet.add v s) H.replace t x (HSet.add v s)
let assign_constr = add constructors let assign_constr = add constructors
let assign_var x y = let assign_var x y =
if not (Hstring.equal x y) then if not (Hstring.equal x y) then
add assignments x y add assignments x y
let rec compute () = let rec compute () =
let flag = ref false in let flag = ref false in
let visited = ref HSet.empty in let visited = ref HSet.empty in
let rec dfs x s = let rec dfs x s =
if not (HSet.mem x !visited) then if not (HSet.mem x !visited) then
begin begin
visited := HSet.add x !visited; visited := HSet.add x !visited;
HSet.iter HSet.iter
(fun y -> (fun y ->
let c_x = find constructors x in let c_x = find constructors x in
let c_y = find constructors y in let c_y = find constructors y in
let c = HSet.union c_x c_y in let c = HSet.union c_x c_y in
@ -171,25 +171,25 @@ module Variant = struct
in in
H.iter dfs assignments; H.iter dfs assignments;
if !flag then compute () if !flag then compute ()
let hset_print fmt s = let hset_print fmt s =
HSet.iter (fun c -> Format.eprintf "%a, " Hstring.print c) s HSet.iter (fun c -> Format.eprintf "%a, " Hstring.print c) s
let print () = let print () =
H.iter H.iter
(fun x c -> (fun x c ->
Format.eprintf "%a = {%a}@." Hstring.print x hset_print c) Format.eprintf "%a = {%a}@." Hstring.print x hset_print c)
constructors constructors
let get_variants = H.find constructors let get_variants = H.find constructors
let set_of_list = List.fold_left (fun s x -> HSet.add x s) HSet.empty let set_of_list = List.fold_left (fun s x -> HSet.add x s) HSet.empty
let init l = let init l =
compute (); compute ();
List.iter List.iter
(fun (x, nty) -> (fun (x, nty) ->
if not (H.mem constructors x) then if not (H.mem constructors x) then
let ty = H.find decl_types nty in let ty = H.find decl_types nty in
match ty with match ty with
@ -198,30 +198,30 @@ module Variant = struct
| _ -> ()) l; | _ -> ()) l;
H.clear assignments H.clear assignments
let update_decl_types s = let update_decl_types s =
let nty = ref "" in let nty = ref "" in
let l = ref [] in let l = ref [] in
HSet.iter HSet.iter
(fun x -> (fun x ->
l := x :: !l; l := x :: !l;
let vx = Hstring.view x in let vx = Hstring.view x in
nty := if !nty = "" then vx else !nty ^ "|" ^ vx) s; nty := if !nty = "" then vx else !nty ^ "|" ^ vx) s;
let nty = Hstring.make !nty in let nty = Hstring.make !nty in
let ty = Ty.Tsum (nty, List.rev !l) in let ty = Ty.Tsum (nty, List.rev !l) in
H.replace decl_types nty ty; H.replace decl_types nty ty;
nty nty
let close () = let close () =
compute (); compute ();
H.iter H.iter
(fun x s -> (fun x s ->
let nty = update_decl_types s in let nty = update_decl_types s in
let sy, args, _ = H.find decl_symbs x in let sy, args, _ = H.find decl_symbs x in
H.replace decl_symbs x (sy, args, nty)) H.replace decl_symbs x (sy, args, nty))
constructors constructors
end end
module rec Term : sig module rec Term : sig
@ -253,17 +253,17 @@ end
let rec first_ite = function let rec first_ite = function
| [] -> raise Not_found | [] -> raise Not_found
| Tite (c, t1, t2) :: l -> [], (c, t1, t2), l | Tite (c, t1, t2) :: l -> [], (c, t1, t2), l
| x :: l -> | x :: l ->
let left, triplet, right = first_ite l in let left, triplet, right = first_ite l in
x::left, triplet, right x::left, triplet, right
let rec lift_ite sb l ty = let rec lift_ite sb l ty =
try try
let left, (c, t1, t2), right = first_ite l in let left, (c, t1, t2), right = first_ite l in
let l = lift_ite sb (left@(t1::right)) ty in let l = lift_ite sb (left@(t1::right)) ty in
let r = lift_ite sb (left@(t2::right)) ty in let r = lift_ite sb (left@(t2::right)) ty in
Tite (c, l, r) Tite (c, l, r)
with Not_found -> with Not_found ->
let l = List.map (function T x -> x | _ -> assert false) l in let l = List.map (function T x -> x | _ -> assert false) l in
T (AETerm.make sb l ty) T (AETerm.make sb l ty)
@ -285,8 +285,8 @@ end
| T t -> AETerm.is_real t | T t -> AETerm.is_real t
| Tite(_, t1, t2) -> is_real t1 && is_real t2 | Tite(_, t1, t2) -> is_real t1 && is_real t2
let make_arith op t1 t2 = let make_arith op t1 t2 =
let op = let op =
match op with match op with
| Plus -> Symbols.Plus | Plus -> Symbols.Plus
| Minus -> Symbols.Minus | Minus -> Symbols.Minus
@ -294,7 +294,7 @@ end
| Div -> Symbols.Div | Div -> Symbols.Div
| Modulo -> Symbols.Modulo | Modulo -> Symbols.Modulo
in in
let ty = let ty =
if is_int t1 && is_int t2 then Ty.Tint if is_int t1 && is_int t2 then Ty.Tint
else if is_real t1 && is_real t2 then Ty.Treal else if is_real t1 && is_real t2 then Ty.Treal
else assert false else assert false
@ -308,10 +308,10 @@ end
and Formula : sig and Formula : sig
type comparator = Eq | Neq | Le | Lt type comparator = Eq | Neq | Le | Lt
type combinator = And | Or | Imp | Not type combinator = And | Or | Imp | Not
type t = type t =
| Lit of Literal.LT.t | Lit of Literal.LT.t
| Comb of combinator * t list | Comb of combinator * t list
val f_true : t val f_true : t
@ -337,7 +337,7 @@ and Formula : sig
val print_list : string -> Format.formatter -> t list -> unit val print_list : string -> Format.formatter -> t list -> unit
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
module Tseitin (Dymmy : sig end) : module Tseitin (Dymmy : sig end) :
sig val make_cnf : t -> Literal.LT.t list list end sig val make_cnf : t -> Literal.LT.t list list end
end end
@ -346,18 +346,18 @@ end
type comparator = Eq | Neq | Le | Lt type comparator = Eq | Neq | Le | Lt
type combinator = And | Or | Imp | Not type combinator = And | Or | Imp | Not
type t = type t =
| Lit of Literal.LT.t | Lit of Literal.LT.t
| Comb of combinator * t list | Comb of combinator * t list
let rec print fmt phi = let rec print fmt phi =
match phi with match phi with
| Lit a -> Literal.LT.print fmt a | Lit a -> Literal.LT.print fmt a
| Comb (Not, [f]) -> | Comb (Not, [f]) ->
fprintf fmt "not (%a)" print f fprintf fmt "not (%a)" print f
| Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l | Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l
| Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l | Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l
| Comb (Imp, [f1; f2]) -> | Comb (Imp, [f1; f2]) ->
fprintf fmt "(%a => %a)" print f1 print f2 fprintf fmt "(%a => %a)" print f1 print f2
| _ -> assert false | _ -> assert false
and print_list sep fmt = function and print_list sep fmt = function
@ -370,38 +370,38 @@ end
let make comb l = Comb (comb, l) let make comb l = Comb (comb, l)
let value env c = let value env c =
if List.mem c env then Some true if List.mem c env then Some true
else if List.mem (make Not [c]) env then Some false else if List.mem (make Not [c]) env then Some false
else None else None
let rec lift_ite env op l = let rec lift_ite env op l =
try try
let left, (c, t1, t2), right = Term.first_ite l in let left, (c, t1, t2), right = Term.first_ite l in
begin begin
match value env c with match value env c with
| Some true -> | Some true ->
lift_ite (c::env) op (left@(t1::right)) lift_ite (c::env) op (left@(t1::right))
| Some false -> | Some false ->
lift_ite ((make Not [c])::env) op (left@(t2::right)) lift_ite ((make Not [c])::env) op (left@(t2::right))
| None -> | None ->
Comb Comb
(And, (And,
[Comb [Comb
(Imp, [c; lift_ite (c::env) op (left@(t1::right))]); (Imp, [c; lift_ite (c::env) op (left@(t1::right))]);
Comb (Imp, Comb (Imp,
[(make Not [c]); [(make Not [c]);
lift_ite lift_ite
((make Not [c])::env) op (left@(t2::right))])]) ((make Not [c])::env) op (left@(t2::right))])])
end end
with Not_found -> with Not_found ->
begin begin
let lit = let lit =
match op, l with match op, l with
| Eq, [Term.T t1; Term.T t2] -> | Eq, [Term.T t1; Term.T t2] ->
Literal.Eq (t1, t2) Literal.Eq (t1, t2)
| Neq, ts -> | Neq, ts ->
let ts = let ts =
List.rev_map (function Term.T x -> x | _ -> assert false) ts in List.rev_map (function Term.T x -> x | _ -> assert false) ts in
Literal.Distinct (false, ts) Literal.Distinct (false, ts)
| Le, [Term.T t1; Term.T t2] -> | Le, [Term.T t1; Term.T t2] ->
@ -440,16 +440,16 @@ end
| Comb (Not, [Comb (Or, l)]) -> | Comb (Not, [Comb (Or, l)]) ->
let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in
Comb (And, nl) Comb (And, nl)
| Comb (Not, [Comb (And, l)]) -> | Comb (Not, [Comb (And, l)]) ->
let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in
Comb (Or, nl) Comb (Or, nl)
| Comb (Not, [Comb (Imp, [f1; f2])]) -> | Comb (Not, [Comb (Imp, [f1; f2])]) ->
Comb (And, [sform f1; sform (Comb (Not, [f2]))]) Comb (And, [sform f1; sform (Comb (Not, [f2]))])
| Comb (And, l) -> | Comb (And, l) ->
Comb (And, List.rev_map sform l) Comb (And, List.rev_map sform l)
| Comb (Or, l) -> | Comb (Or, l) ->
Comb (Or, List.rev_map sform l) Comb (Or, List.rev_map sform l)
| Comb (Imp, [f1; f2]) -> | Comb (Imp, [f1; f2]) ->
Comb (Or, [sform (Comb (Not, [f1])); sform f2]) Comb (Or, [sform (Comb (Not, [f1])); sform f2])
| Comb ((Imp | Not), _) -> assert false | Comb ((Imp | Not), _) -> assert false
| Lit _ as f -> f | Lit _ as f -> f
@ -463,17 +463,17 @@ end
| [a] -> a | [a] -> a
| l -> Comb (Or, l) | l -> Comb (Or, l)
let distrib l_and l_or = let distrib l_and l_or =
let l = let l =
if l_or = [] then l_and if l_or = [] then l_and
else else
List.rev_map List.rev_map
(fun x -> (fun x ->
match x with match x with
| Lit _ -> Comb (Or, x::l_or) | Lit _ -> Comb (Or, x::l_or)
| Comb (Or, l) -> Comb (Or, l @@ l_or) | Comb (Or, l) -> Comb (Or, l @@ l_or)
| _ -> assert false | _ -> assert false
) l_and ) l_and
in in
Comb (And, l) Comb (And, l)
@ -482,22 +482,22 @@ end
| Comb (Or, l)::r -> l @@ (flatten_or r) | Comb (Or, l)::r -> l @@ (flatten_or r)
| Lit a :: r -> (Lit a)::(flatten_or r) | Lit a :: r -> (Lit a)::(flatten_or r)
| _ -> assert false | _ -> assert false
let rec flatten_and = function let rec flatten_and = function
| [] -> [] | [] -> []
| Comb (And, l)::r -> l @@ (flatten_and r) | Comb (And, l)::r -> l @@ (flatten_and r)
| a :: r -> a::(flatten_and r) | a :: r -> a::(flatten_and r)
let rec cnf f =
let rec cnf f =
match f with match f with
| Comb (Or, l) -> | Comb (Or, l) ->
begin begin
let l = List.rev_map cnf l in let l = List.rev_map cnf l in
let l_and, l_or = let l_and, l_or =
List.partition (function Comb(And,_) -> true | _ -> false) l in List.partition (function Comb(And,_) -> true | _ -> false) l in
match l_and with match l_and with
| [ Comb(And, l_conj) ] -> | [ Comb(And, l_conj) ] ->
let u = flatten_or l_or in let u = flatten_or l_or in
distrib l_conj u distrib l_conj u
@ -505,7 +505,7 @@ end
let u = flatten_or l_or in let u = flatten_or l_or in
cnf (Comb(Or, (distrib l_conj u)::r)) cnf (Comb(Or, (distrib l_conj u)::r))
| _ -> | _ ->
begin begin
match flatten_or l_or with match flatten_or l_or with
| [] -> assert false | [] -> assert false
@ -513,9 +513,9 @@ end
| v -> Comb (Or, v) | v -> Comb (Or, v)
end end
end end
| Comb (And, l) -> | Comb (And, l) ->
Comb (And, List.rev_map cnf l) Comb (And, List.rev_map cnf l)
| f -> f | f -> f
let rec mk_cnf = function let rec mk_cnf = function
| Comb (And, l) -> | Comb (And, l) ->
@ -524,13 +524,13 @@ end
| Comb (Or, [f1;f2]) -> | Comb (Or, [f1;f2]) ->
let ll1 = mk_cnf f1 in let ll1 = mk_cnf f1 in
let ll2 = mk_cnf f2 in let ll2 = mk_cnf f2 in
List.fold_left List.fold_left
(fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
| Comb (Or, f1 :: l) -> | Comb (Or, f1 :: l) ->
let ll1 = mk_cnf f1 in let ll1 = mk_cnf f1 in
let ll2 = mk_cnf (Comb (Or, l)) in let ll2 = mk_cnf (Comb (Or, l)) in
List.fold_left List.fold_left
(fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
| Lit a -> [[a]] | Lit a -> [[a]]
@ -538,18 +538,18 @@ end
| _ -> assert false | _ -> assert false
let rec unfold mono f = let rec unfold mono f =
match f with match f with
| Lit a -> a::mono | Lit a -> a::mono
| Comb (Not, [Lit a]) -> | Comb (Not, [Lit a]) ->
(Literal.LT.neg a)::mono (Literal.LT.neg a)::mono
| Comb (Or, l) -> | Comb (Or, l) ->
List.fold_left unfold mono l List.fold_left unfold mono l
| _ -> assert false | _ -> assert false
let rec init monos f = let rec init monos f =
match f with match f with
| Comb (And, l) -> | Comb (And, l) ->
List.fold_left init monos l List.fold_left init monos l
| f -> (unfold [] f)::monos | f -> (unfold [] f)::monos
@ -557,10 +557,10 @@ end
let sfnc = cnf (sform f) in let sfnc = cnf (sform f) in
init [] sfnc init [] sfnc
let mk_proxy = let mk_proxy =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> fun () ->
let t = AETerm.make let t = AETerm.make
(Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt)))) (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt))))
[] Ty.Tbool [] Ty.Tbool
in in
@ -615,9 +615,9 @@ end
| None, l -> Some Or, l @@ acc | None, l -> Some Or, l @@ acc
| _ -> assert false | _ -> assert false
) (None, []) l ) (None, []) l
| _ -> assert false | _ -> assert false
let cnf f = let cnf f =
let acc = match f with let acc = match f with
| Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l
@ -702,47 +702,47 @@ module Make (Dummy : sig end) = struct
let check_unsatcore uc = let check_unsatcore uc =
eprintf "Unsat Core : @."; eprintf "Unsat Core : @.";
List.iter List.iter
(fun c -> (fun c ->
eprintf "%a@." (Formula.print_list "or") eprintf "%a@." (Formula.print_list "or")
(List.rev_map (fun x -> Formula.Lit x) c)) uc; (List.rev_map (fun x -> Formula.Lit x) c)) uc;
eprintf "@."; eprintf "@.";
try try
clear (); clear ();
CSolver.assume uc 0; CSolver.assume uc 0;
CSolver.solve (); CSolver.solve ();
eprintf "Not an unsat core !!!@."; eprintf "Not an unsat core !!!@.";
assert false assert false
with with
| Solver.Unsat _ -> (); | Solver.Unsat _ -> ();
| Solver.Sat -> | Solver.Sat ->
eprintf "Sat: Not an unsat core !!!@."; eprintf "Sat: Not an unsat core !!!@.";
assert false assert false
let export_unsatcore cl = let export_unsatcore cl =
let uc = List.rev_map (fun {Solver_types.atoms=atoms} -> let uc = List.rev_map (fun {Solver_types.atoms=atoms} ->
let l = ref [] in let l = ref [] in
for i = 0 to Vec.size atoms - 1 do for i = 0 to Vec.size atoms - 1 do
l := (Vec.get atoms i).Solver_types.lit :: !l l := (Vec.get atoms i).Solver_types.lit :: !l
done; done;
!l) cl !l) cl
in (* check_unsatcore uc; *) in (* check_unsatcore uc; *)
uc uc
module SInt = module SInt =
Set.Make (struct type t = int let compare = Pervasives.compare end) Set.Make (struct type t = int let compare = Pervasives.compare end)
let export_unsatcore2 cl = let export_unsatcore2 cl =
let s = let s =
List.fold_left List.fold_left
(fun s {Solver_types.name = n} -> (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 in
SInt.elements s SInt.elements s
let assume ?(profiling = false) ~id f = let assume ?(profiling = false) ~id f =
if profiling then Time.start (); if profiling then Time.start ();
try try
CSolver.assume (Tseitin.make_cnf f) id; CSolver.assume (Tseitin.make_cnf f) id;
if profiling then Time.pause () if profiling then Time.pause ()
with Solver.Unsat ex -> with Solver.Unsat ex ->
@ -752,12 +752,12 @@ module Make (Dummy : sig end) = struct
let check ?(profiling = false) () = let check ?(profiling = false) () =
incr calls; incr calls;
if profiling then Time.start (); if profiling then Time.start ();
try try
CSolver.solve (); CSolver.solve ();
if profiling then Time.pause () if profiling then Time.pause ()
with with
| Solver.Sat -> if profiling then Time.pause () | Solver.Sat -> if profiling then Time.pause ()
| Solver.Unsat ex -> | Solver.Unsat ex ->
if profiling then Time.pause (); if profiling then Time.pause ();
raise (Unsat (export_unsatcore2 ex)) raise (Unsat (export_unsatcore2 ex))
@ -777,7 +777,7 @@ module Make (Dummy : sig end) = struct
let entails ?(profiling=false) ~id f = let entails ?(profiling=false) ~id f =
let st = save_state () in let st = save_state () in
let ans = let ans =
try try
assume ~profiling ~id (Formula.make Formula.Not [f]) ; assume ~profiling ~id (Formula.make Formula.Not [f]) ;
check ~profiling (); check ~profiling ();

46
smt/smt.mli
View file

@ -74,31 +74,31 @@ end
(** {3 Function symbols} *) (** {3 Function symbols} *)
module Symbol : sig module Symbol : sig
type t = Hstring.t type t = Hstring.t
(** The type of function symbols *) (** The type of function symbols *)
val declare : Hstring.t -> Type.t list -> Type.t -> unit val declare : Hstring.t -> Type.t list -> Type.t -> unit
(** [declare s [arg_1; ... ; arg_n] out] declares a new function (** [declare s [arg_1; ... ; arg_n] out] declares a new function
symbol with type [ (arg_1, ... , arg_n) -> out] *) symbol with type [ (arg_1, ... , arg_n) -> out] *)
val type_of : t -> Type.t list * Type.t 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 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 val has_type_proc : t -> bool
(** [has_type_proc x] is [true] if x has the type of a process (** [has_type_proc x] is [true] if x has the type of a process
identifier. *) identifier. *)
val declared : t -> bool val declared : t -> bool
(** [declared x] is [true] if [x] is already declared. *) (** [declared x] is [true] if [x] is already declared. *)
end end
(** {3 Variants} (** {3 Variants}
The types of symbols (when they are enumerated data types) can be refined The types of symbols (when they are enumerated data types) can be refined
to substypes of their original type (i.e. a subset of their constructors). to substypes of their original type (i.e. a subset of their constructors).
*) *)
@ -107,7 +107,7 @@ module Variant : sig
val init : (Symbol.t * Type.t) list -> unit val init : (Symbol.t * Type.t) list -> unit
(** [init l] where [l] is a list of pairs [(s, ty)] initializes the (** [init l] where [l] is a list of pairs [(s, ty)] initializes the
type (and associated constructors) of each [s] to its original type [ty]. type (and associated constructors) of each [s] to its original type [ty].
This function must be called with a list of all symbols before This function must be called with a list of all symbols before
attempting to refine the types. *) attempting to refine the types. *)
@ -117,12 +117,12 @@ module Variant : sig
This function must be called when all information has been added.*) This function must be called when all information has been added.*)
val assign_constr : Symbol.t -> Hstring.t -> unit val assign_constr : Symbol.t -> Hstring.t -> unit
(** [assign_constr s cstr] will add the constraint that the constructor (** [assign_constr s cstr] will add the constraint that the constructor
[cstr] must be in the type of [s] *) [cstr] must be in the type of [s] *)
val assign_var : Symbol.t -> Symbol.t -> unit val assign_var : Symbol.t -> Symbol.t -> unit
(** [assign_var x y] will add the constraint that the type of [y] is a (** [assign_var x y] will add the constraint that the type of [y] is a
subtype of [x] (use this function when [x := y] appear in your subtype of [x] (use this function when [x := y] appear in your
program *) program *)
val print : unit -> unit val print : unit -> unit
@ -143,10 +143,10 @@ module rec Term : sig
(** The type of terms *) (** The type of terms *)
(** The type of operators *) (** The type of operators *)
type operator = type operator =
| Plus (** [+] *) | Plus (** [+] *)
| Minus (** [-] *) | Minus (** [-] *)
| Mult (** [*] *) | Mult (** [*] *)
| Div (** [/] *) | Div (** [/] *)
| Modulo (** [mod] *) | Modulo (** [mod] *)
@ -186,22 +186,22 @@ end
and Formula : sig and Formula : sig
(** The type of comparators: *) (** The type of comparators: *)
type comparator = type comparator =
| Eq (** equality ([=]) *) | Eq (** equality ([=]) *)
| Neq (** disequality ([<>]) *) | Neq (** disequality ([<>]) *)
| Le (** inequality ([<=]) *) | Le (** inequality ([<=]) *)
| Lt (** strict inequality ([<]) *) | Lt (** strict inequality ([<]) *)
(** The type of operators *) (** The type of operators *)
type combinator = type combinator =
| And (** conjunction *) | And (** conjunction *)
| Or (** disjunction *) | Or (** disjunction *)
| Imp (** implication *) | Imp (** implication *)
| Not (** negation *) | Not (** negation *)
(** The type of ground formulas *) (** The type of ground formulas *)
type t = type t =
| Lit of Literal.LT.t | Lit of Literal.LT.t
| Comb of combinator * t list | Comb of combinator * t list
val f_true : t val f_true : t
@ -267,11 +267,11 @@ module type Solver = sig
assume f_n; assume f_n;
check ();]} check ();]}
*) *)
type state type state
(** The type of the internal state of the solver (see {!save_state} and (** The type of the internal state of the solver (see {!save_state} and
{!restore_state}).*) {!restore_state}).*)
(** {2 Profiling functions} *) (** {2 Profiling functions} *)
@ -292,20 +292,20 @@ module type Solver = sig
(** [assume ~profiling:b f id] adds the formula [f] to the context of the (** [assume ~profiling:b f id] adds the formula [f] to the context of the
solver with identifier [id]. solver with identifier [id].
This function only performs unit propagation. This function only performs unit propagation.
@param profiling if set to [true] then profiling information (time) will @param profiling if set to [true] then profiling information (time) will
be computed (expensive because of system calls). be computed (expensive because of system calls).
{b Raises} {! Unsat} if the context becomes inconsistent after unit {b Raises} {! Unsat} if the context becomes inconsistent after unit
propagation. *) propagation. *)
val check : ?profiling:bool -> unit -> unit val check : ?profiling:bool -> unit -> unit
(** [check ()] runs Alt-Ergo Zero on its context. If [()] is (** [check ()] runs Alt-Ergo Zero on its context. If [()] is
returned then the context is satifiable. returned then the context is satifiable.
@param profiling if set to [true] then profiling information (time) will @param profiling if set to [true] then profiling information (time) will
be computed (expensive because of system calls). be computed (expensive because of system calls).
{b Raises} {! Unsat} [[id_1; ...; id_n]] if the context is unsatisfiable. {b Raises} {! Unsat} [[id_1; ...; id_n]] if the context is unsatisfiable.
[id_1, ..., id_n] is the unsat core (returned as the identifiers of the [id_1, ..., id_n] is the unsat core (returned as the identifiers of the
formulas given to the solver). *) formulas given to the solver). *)

266
smt/solver.ml
View file

@ -22,8 +22,8 @@ exception Restart
type env = type env =
{ {
(* si vrai, les contraintes sont deja fausses *) (* si vrai, les contraintes sont deja fausses *)
mutable is_unsat : bool; mutable is_unsat : bool;
@ -31,34 +31,34 @@ type env =
(* clauses du probleme *) (* clauses du probleme *)
mutable clauses : clause Vec.t; mutable clauses : clause Vec.t;
(* clauses apprises *) (* clauses apprises *)
mutable learnts : clause Vec.t; mutable learnts : clause Vec.t;
(* valeur de l'increment pour l'activite des clauses *) (* valeur de l'increment pour l'activite des clauses *)
mutable clause_inc : float; mutable clause_inc : float;
(* valeur de l'increment pour l'activite des variables *) (* valeur de l'increment pour l'activite des variables *)
mutable var_inc : float; mutable var_inc : float;
(* un vecteur des variables du probleme *) (* un vecteur des variables du probleme *)
mutable vars : var Vec.t; mutable vars : var Vec.t;
(* la pile de decisions avec les faits impliques *) (* la pile de decisions avec les faits impliques *)
mutable trail : atom Vec.t; mutable trail : atom Vec.t;
(* une pile qui pointe vers les niveaux de decision dans trail *) (* une pile qui pointe vers les niveaux de decision dans trail *)
mutable trail_lim : int Vec.t; mutable trail_lim : int Vec.t;
(* Tete de la File des faits unitaires a propager. (* Tete de la File des faits unitaires a propager.
C'est un index vers le trail *) C'est un index vers le trail *)
mutable qhead : int; mutable qhead : int;
(* Nombre des assignements top-level depuis la derniere (* Nombre des assignements top-level depuis la derniere
execution de 'simplify()' *) execution de 'simplify()' *)
mutable simpDB_assigns : int; mutable simpDB_assigns : int;
(* Nombre restant de propagations a faire avant la prochaine (* Nombre restant de propagations a faire avant la prochaine
execution de 'simplify()' *) execution de 'simplify()' *)
mutable simpDB_props : int; mutable simpDB_props : int;
@ -82,12 +82,12 @@ type env =
(* facteur de multiplication de restart limite, vaut 1.5 par defaut*) (* facteur de multiplication de restart limite, vaut 1.5 par defaut*)
restart_inc : float; restart_inc : float;
(* limite initiale du nombre de clause apprises, vaut 1/3 (* limite initiale du nombre de clause apprises, vaut 1/3
des clauses originales par defaut *) des clauses originales par defaut *)
mutable learntsize_factor : float; mutable learntsize_factor : float;
(* multiplier learntsize_factor par cette valeur a chaque restart, (* multiplier learntsize_factor par cette valeur a chaque restart,
vaut 1.1 par defaut *) vaut 1.1 par defaut *)
learntsize_inc : float; learntsize_inc : float;
@ -96,7 +96,7 @@ type env =
(* controle la polarite a choisir lors de la decision *) (* controle la polarite a choisir lors de la decision *)
polarity_mode : bool; polarity_mode : bool;
mutable starts : int; mutable starts : int;
mutable decisions : int; mutable decisions : int;
@ -116,17 +116,17 @@ type env =
mutable nb_init_vars : int; mutable nb_init_vars : int;
mutable nb_init_clauses : int; mutable nb_init_clauses : int;
mutable model : var Vec.t; mutable model : var Vec.t;
mutable tenv : Th.t; mutable tenv : Th.t;
mutable tenv_queue : Th.t Vec.t; mutable tenv_queue : Th.t Vec.t;
mutable tatoms_queue : atom Queue.t; mutable tatoms_queue : atom Queue.t;
} }
exception Conflict of clause exception Conflict of clause
@ -136,36 +136,36 @@ module Make (Dummy : sig end) = struct
open Solver_types open Solver_types
type state = type state =
{ {
env : env; env : env;
st_cpt_mk_var: int; st_cpt_mk_var: int;
st_ma : var Literal.LT.Map.t; st_ma : var Literal.LT.Map.t;
} }
let env = let env =
{ {
is_unsat = false; is_unsat = false;
unsat_core = [] ; unsat_core = [] ;
clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) clauses = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*)
learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*) learnts = Vec.make 0 dummy_clause; (*sera mis a jour lors du parsing*)
clause_inc = 1.; clause_inc = 1.;
var_inc = 1.; var_inc = 1.;
vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*) vars = Vec.make 0 dummy_var; (*sera mis a jour lors du parsing*)
trail = Vec.make 601 dummy_atom; trail = Vec.make 601 dummy_atom;
trail_lim = Vec.make 601 (-105); trail_lim = Vec.make 601 (-105);
qhead = 0; qhead = 0;
simpDB_assigns = -1; simpDB_assigns = -1;
simpDB_props = 0; simpDB_props = 0;
@ -183,15 +183,15 @@ module Make (Dummy : sig end) = struct
restart_first = 100; restart_first = 100;
restart_inc = 1.5; restart_inc = 1.5;
learntsize_factor = 1. /. 3. ; learntsize_factor = 1. /. 3. ;
learntsize_inc = 1.1; learntsize_inc = 1.1;
expensive_ccmin = true; expensive_ccmin = true;
polarity_mode = false; polarity_mode = false;
starts = 0; starts = 0;
decisions = 0; decisions = 0;
@ -211,9 +211,9 @@ module Make (Dummy : sig end) = struct
nb_init_vars = 0; nb_init_vars = 0;
nb_init_clauses = 0; nb_init_clauses = 0;
model = Vec.make 0 dummy_var; model = Vec.make 0 dummy_var;
tenv = Th.empty(); tenv = Th.empty();
tenv_queue = Vec.make 100 (Th.empty()); tenv_queue = Vec.make 100 (Th.empty());
@ -224,18 +224,18 @@ module Make (Dummy : sig end) = struct
let f_weight i j = (Vec.get env.vars j).weight < (Vec.get env.vars i).weight let f_weight i j = (Vec.get env.vars j).weight < (Vec.get env.vars i).weight
let f_filter i = (Vec.get env.vars i).level < 0 let f_filter i = (Vec.get env.vars i).level < 0
let insert_var_order v = let insert_var_order v =
Iheap.insert f_weight env.order v.vid Iheap.insert f_weight env.order v.vid
let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay let var_decay_activity () = env.var_inc <- env.var_inc *. env.var_decay
let clause_decay_activity () = let clause_decay_activity () =
env.clause_inc <- env.clause_inc *. env.clause_decay env.clause_inc <- env.clause_inc *. env.clause_decay
let var_bump_activity v = let var_bump_activity v =
v.weight <- v.weight +. env.var_inc; v.weight <- v.weight +. env.var_inc;
if v.weight > 1e100 then begin if v.weight > 1e100 then begin
for i = 0 to env.vars.Vec.sz - 1 do for i = 0 to env.vars.Vec.sz - 1 do
@ -245,9 +245,9 @@ let var_bump_activity v =
end; end;
if Iheap.in_heap env.order v.vid then if Iheap.in_heap env.order v.vid then
Iheap.decrease f_weight env.order v.vid Iheap.decrease f_weight env.order v.vid
let clause_bump_activity c =
let clause_bump_activity c =
c.activity <- c.activity +. env.clause_inc; c.activity <- c.activity +. env.clause_inc;
if c.activity > 1e20 then begin if c.activity > 1e20 then begin
for i = 0 to env.learnts.Vec.sz - 1 do for i = 0 to env.learnts.Vec.sz - 1 do
@ -264,32 +264,32 @@ let nb_clauses () = Vec.size env.clauses
let nb_learnts () = Vec.size env.learnts let nb_learnts () = Vec.size env.learnts
let nb_vars () = Vec.size env.vars let nb_vars () = Vec.size env.vars
let new_decision_level() = let new_decision_level() =
Vec.push env.trail_lim (Vec.size env.trail); Vec.push env.trail_lim (Vec.size env.trail);
Vec.push env.tenv_queue env.tenv (* save the current tenv *) Vec.push env.tenv_queue env.tenv (* save the current tenv *)
let attach_clause c = let attach_clause c =
Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 0).neg.watched c;
Vec.push (Vec.get c.atoms 1).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c;
if c.learnt then if c.learnt then
env.learnts_literals <- env.learnts_literals + Vec.size c.atoms env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
else else
env.clauses_literals <- env.clauses_literals + Vec.size c.atoms env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
let detach_clause c = let detach_clause c =
c.removed <- true; c.removed <- true;
(* (*
Vec.remove (Vec.get c.atoms 0).neg.watched c; Vec.remove (Vec.get c.atoms 0).neg.watched c;
Vec.remove (Vec.get c.atoms 1).neg.watched c; Vec.remove (Vec.get c.atoms 1).neg.watched c;
*) *)
if c.learnt then if c.learnt then
env.learnts_literals <- env.learnts_literals - Vec.size c.atoms env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
else else
env.clauses_literals <- env.clauses_literals - Vec.size c.atoms env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
let remove_clause c = detach_clause c let remove_clause c = detach_clause c
let satisfied c = let satisfied c =
try try
for i = 0 to Vec.size c.atoms - 1 do for i = 0 to Vec.size c.atoms - 1 do
if (Vec.get c.atoms i).is_true then raise Exit if (Vec.get c.atoms i).is_true then raise Exit
@ -298,7 +298,7 @@ let satisfied c =
with Exit -> true with Exit -> true
(* annule tout jusqu'a lvl *exclu* *) (* annule tout jusqu'a lvl *exclu* *)
let cancel_until lvl = let cancel_until lvl =
if decision_level () > lvl then begin if decision_level () > lvl then begin
env.qhead <- Vec.get env.trail_lim lvl; env.qhead <- Vec.get env.trail_lim lvl;
for c = Vec.size env.trail - 1 downto env.qhead do for c = Vec.size env.trail - 1 downto env.qhead do
@ -318,7 +318,7 @@ let cancel_until lvl =
end; end;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
let rec pick_branch_lit () = let rec pick_branch_lit () =
let max = Iheap.remove_min f_weight env.order in let max = Iheap.remove_min f_weight env.order in
let v = Vec.get env.vars max in let v = Vec.get env.vars max in
if v.level>= 0 then begin if v.level>= 0 then begin
@ -328,7 +328,7 @@ let rec pick_branch_lit () =
else v else v
let enqueue a lvl reason = let enqueue a lvl reason =
assert (not a.is_true && not a.neg.is_true && assert (not a.is_true && not a.neg.is_true &&
a.var.level < 0 && a.var.reason = None && lvl >= 0); a.var.level < 0 && a.var.reason = None && lvl >= 0);
(* Garder la reason car elle est utile pour les unsat-core *) (* Garder la reason car elle est utile pour les unsat-core *)
(*let reason = if lvl = 0 then None else reason in*) (*let reason = if lvl = 0 then None else reason in*)
@ -338,10 +338,10 @@ let enqueue a lvl reason =
(*eprintf "enqueue: %a@." Debug.atom a; *) (*eprintf "enqueue: %a@." Debug.atom a; *)
Vec.push env.trail a Vec.push env.trail a
let progress_estimate () = let progress_estimate () =
let prg = ref 0. in let prg = ref 0. in
let nbv = to_float (nb_vars()) in let nbv = to_float (nb_vars()) in
let lvl = decision_level () in let lvl = decision_level () in
let _F = 1. /. nbv in let _F = 1. /. nbv in
for i = 0 to lvl do for i = 0 to lvl do
let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in
@ -360,14 +360,14 @@ let propagate_in_clause a c i watched new_sz =
let first = Vec.get atoms 0 in let first = Vec.get atoms 0 in
if first.is_true then begin if first.is_true then begin
(* clause vraie, la garder dans les watched *) (* clause vraie, la garder dans les watched *)
Vec.set watched !new_sz c; Vec.set watched !new_sz c;
incr new_sz; incr new_sz;
end end
else else
try (* chercher un nouveau watcher *) try (* chercher un nouveau watcher *)
for k = 2 to Vec.size atoms - 1 do for k = 2 to Vec.size atoms - 1 do
let ak = Vec.get atoms k in let ak = Vec.get atoms k in
if not (ak.neg.is_true) then begin if not (ak.neg.is_true) then begin
(* Watcher Trouve: mettre a jour et sortir *) (* Watcher Trouve: mettre a jour et sortir *)
Vec.set atoms 1 ak; Vec.set atoms 1 ak;
Vec.set atoms k a.neg; Vec.set atoms k a.neg;
@ -387,22 +387,22 @@ let propagate_in_clause a c i watched new_sz =
end end
else begin else begin
(* la clause est unitaire *) (* la clause est unitaire *)
Vec.set watched !new_sz c; Vec.set watched !new_sz c;
incr new_sz; incr new_sz;
enqueue first (decision_level ()) (Some c) enqueue first (decision_level ()) (Some c)
end end
with Exit -> () with Exit -> ()
let propagate_atom a res = let propagate_atom a res =
let watched = a.watched in let watched = a.watched in
let new_sz_w = ref 0 in let new_sz_w = ref 0 in
begin begin
try try
for i = 0 to Vec.size watched - 1 do for i = 0 to Vec.size watched - 1 do
let c = Vec.get watched i in let c = Vec.get watched i in
if not c.removed then propagate_in_clause a c i watched new_sz_w if not c.removed then propagate_in_clause a c i watched new_sz_w
done; done;
with Conflict c -> assert (!res = None); res := Some c with Conflict c -> assert (!res = None); res := Some c
end; end;
let dead_part = Vec.size watched - !new_sz_w in let dead_part = Vec.size watched - !new_sz_w in
Vec.shrink watched dead_part Vec.shrink watched dead_part
@ -416,7 +416,7 @@ let expensive_theory_propagate () = None
(* with Exception.Inconsistent dep -> *) (* with Exception.Inconsistent dep -> *)
(* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *)
(* Some dep *) (* Some dep *)
let theory_propagate () = let theory_propagate () =
let facts = ref [] in let facts = ref [] in
while not (Queue.is_empty env.tatoms_queue) do while not (Queue.is_empty env.tatoms_queue) do
@ -425,7 +425,7 @@ let theory_propagate () =
(*let ex = if a.var.level > 0 then Ex.singleton a else Ex.empty in*) (*let ex = if a.var.level > 0 then Ex.singleton a else Ex.empty in*)
let ex = Ex.singleton a in (* Usefull for debugging *) let ex = Ex.singleton a in (* Usefull for debugging *)
facts := (a.lit, ex) :: !facts facts := (a.lit, ex) :: !facts
else else
if a.neg.is_true then if a.neg.is_true then
(*let ex = if a.var.level > 0 then Ex.singleton a.neg else Ex.empty in*) (*let ex = if a.var.level > 0 then Ex.singleton a.neg else Ex.empty in*)
let ex = Ex.singleton a.neg in (* Usefull for debugging *) let ex = Ex.singleton a.neg in (* Usefull for debugging *)
@ -434,17 +434,17 @@ let theory_propagate () =
done; done;
try try
let full_model = nb_assigns() = env.nb_init_vars in let full_model = nb_assigns() = env.nb_init_vars in
env.tenv <- env.tenv <-
List.fold_left List.fold_left
(fun t (a,ex) -> let t,_,_ = Th.assume ~cs:true a ex t in t) (fun t (a,ex) -> let t,_,_ = Th.assume ~cs:true a ex t in t)
env.tenv !facts; env.tenv !facts;
if full_model then expensive_theory_propagate () if full_model then expensive_theory_propagate ()
else None else None
with Exception.Inconsistent dep -> with Exception.Inconsistent dep ->
(* eprintf "th inconsistent : %a @." Ex.print dep; *) (* eprintf "th inconsistent : %a @." Ex.print dep; *)
Some dep Some dep
let propagate () = let propagate () =
let num_props = ref 0 in let num_props = ref 0 in
let res = ref None in let res = ref None in
(*assert (Queue.is_empty env.tqueue);*) (*assert (Queue.is_empty env.tqueue);*)
@ -460,7 +460,7 @@ let propagate () =
!res !res
let analyze c_clause = let analyze c_clause =
let pathC = ref 0 in let pathC = ref 0 in
let learnt = ref [] in let learnt = ref [] in
let cond = ref true in let cond = ref true in
@ -490,14 +490,14 @@ let analyze c_clause =
end end
end end
done; done;
(* look for the next node to expand *) (* look for the next node to expand *)
while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done;
decr pathC; decr pathC;
let p = Vec.get env.trail !tr_ind in let p = Vec.get env.trail !tr_ind in
decr tr_ind; decr tr_ind;
match !pathC, p.var.reason with match !pathC, p.var.reason with
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, None -> assert false | n, None -> assert false
@ -506,12 +506,12 @@ let analyze c_clause =
List.iter (fun q -> q.var.seen <- false) !seen; List.iter (fun q -> q.var.seen <- false) !seen;
!blevel, !learnt, !history, !size !blevel, !learnt, !history, !size
let f_sort_db c1 c2 = let f_sort_db c1 c2 =
let sz1 = Vec.size c1.atoms in let sz1 = Vec.size c1.atoms in
let sz2 = Vec.size c2.atoms in let sz2 = Vec.size c2.atoms in
let c = compare c1.activity c2.activity in let c = compare c1.activity c2.activity in
if sz1 = sz2 && c = 0 then 0 if sz1 = sz2 && c = 0 then 0
else else
if sz1 > 2 && (sz2 = 2 || c < 0) then -1 if sz1 > 2 && (sz2 = 2 || c < 0) then -1
else 1 else 1
@ -534,22 +534,22 @@ let reduce_db () = ()
let j = ref 0 in let j = ref 0 in
for i = 0 to lim1 - 1 do for i = 0 to lim1 - 1 do
let c = Vec.get env.learnts i in let c = Vec.get env.learnts i in
if Vec.size c.atoms > 2 && not (locked c) then if Vec.size c.atoms > 2 && not (locked c) then
remove_clause c remove_clause c
else else
begin Vec.set env.learnts !j c; incr j end begin Vec.set env.learnts !j c; incr j end
done; done;
for i = lim1 to lim2 - 1 do for i = lim1 to lim2 - 1 do
let c = Vec.get env.learnts i in let c = Vec.get env.learnts i in
if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then
remove_clause c remove_clause c
else else
begin Vec.set env.learnts !j c; incr j end begin Vec.set env.learnts !j c; incr j end
done; done;
Vec.shrink env.learnts (lim2 - !j) Vec.shrink env.learnts (lim2 - !j)
*) *)
let remove_satisfied vec = let remove_satisfied vec =
let j = ref 0 in let j = ref 0 in
let k = Vec.size vec - 1 in let k = Vec.size vec - 1 in
for i = 0 to k do for i = 0 to k do
@ -563,7 +563,7 @@ let remove_satisfied vec =
Vec.shrink vec (k + 1 - !j) Vec.shrink vec (k + 1 - !j)
module HUC = Hashtbl.Make module HUC = Hashtbl.Make
(struct type t = clause let equal = (==) let hash = Hashtbl.hash end) (struct type t = clause let equal = (==) let hash = Hashtbl.hash end)
@ -580,15 +580,15 @@ let report_b_unsat ({atoms=atoms} as confl) =
(fun hc -> (fun hc ->
eprintf " %a@." Debug.clause hc eprintf " %a@." Debug.clause hc
)!l; )!l;
end; end;
let uc = HUC.create 17 in let uc = HUC.create 17 in
let rec roots todo = let rec roots todo =
match todo with match todo with
| [] -> () | [] -> ()
| c::r -> | c::r ->
for i = 0 to Vec.size c.atoms - 1 do for i = 0 to Vec.size c.atoms - 1 do
let v = (Vec.get c.atoms i).var in let v = (Vec.get c.atoms i).var in
if not v.seen then begin if not v.seen then begin
v.seen <- true; v.seen <- true;
roots v.vpremise; roots v.vpremise;
match v.reason with None -> () | Some r -> roots [r]; match v.reason with None -> () | Some r -> roots [r];
@ -612,7 +612,7 @@ let report_b_unsat ({atoms=atoms} as confl) =
let report_t_unsat dep = let report_t_unsat dep =
let l = let l =
Ex.fold_atoms Ex.fold_atoms
(fun {var=v} l -> (fun {var=v} l ->
let l = List.rev_append v.vpremise l in let l = List.rev_append v.vpremise l in
@ -627,13 +627,13 @@ let report_t_unsat dep =
)l; )l;
end; end;
let uc = HUC.create 17 in let uc = HUC.create 17 in
let rec roots todo = let rec roots todo =
match todo with match todo with
| [] -> () | [] -> ()
| c::r -> | c::r ->
for i = 0 to Vec.size c.atoms - 1 do for i = 0 to Vec.size c.atoms - 1 do
let v = (Vec.get c.atoms i).var in let v = (Vec.get c.atoms i).var in
if not v.seen then begin if not v.seen then begin
v.seen <- true; v.seen <- true;
roots v.vpremise; roots v.vpremise;
match v.reason with None -> () | Some r -> roots [r]; match v.reason with None -> () | Some r -> roots [r];
@ -655,10 +655,10 @@ let report_t_unsat dep =
env.unsat_core <- unsat_core; env.unsat_core <- unsat_core;
raise (Unsat unsat_core) raise (Unsat unsat_core)
let simplify () = let simplify () =
assert (decision_level () = 0); assert (decision_level () = 0);
if env.is_unsat then raise (Unsat env.unsat_core); if env.is_unsat then raise (Unsat env.unsat_core);
begin begin
match propagate () with match propagate () with
| Some confl -> report_b_unsat confl | Some confl -> report_b_unsat confl
| None -> | None ->
@ -674,7 +674,7 @@ let simplify () =
env.simpDB_props <- env.clauses_literals + env.learnts_literals; env.simpDB_props <- env.clauses_literals + env.learnts_literals;
end end
let record_learnt_clause blevel learnt history size = let record_learnt_clause blevel learnt history size =
begin match learnt with begin match learnt with
| [] -> assert false | [] -> assert false
| [fuip] -> | [fuip] ->
@ -692,7 +692,7 @@ let record_learnt_clause blevel learnt history size =
var_decay_activity (); var_decay_activity ();
clause_decay_activity() clause_decay_activity()
let check_inconsistence_of dep = let check_inconsistence_of dep =
try try
let env = ref (Th.empty()) in (); let env = ref (Th.empty()) in ();
Ex.iter_atoms Ex.iter_atoms
@ -704,12 +704,12 @@ let check_inconsistence_of dep =
assert false assert false
with Exception.Inconsistent _ -> () with Exception.Inconsistent _ -> ()
let theory_analyze dep = let theory_analyze dep =
let atoms, sz, max_lvl, c_hist = let atoms, sz, max_lvl, c_hist =
Ex.fold_atoms Ex.fold_atoms
(fun a (acc, sz, max_lvl, c_hist) -> (fun a (acc, sz, max_lvl, c_hist) ->
let c_hist = List.rev_append a.var.vpremise c_hist in let c_hist = List.rev_append a.var.vpremise c_hist in
let c_hist = match a.var.reason with let c_hist = match a.var.reason with
| None -> c_hist | Some r -> r:: c_hist in | None -> c_hist | Some r -> r:: c_hist in
if a.var.level = 0 then acc, sz, max_lvl, c_hist if a.var.level = 0 then acc, sz, max_lvl, c_hist
else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist else a.neg :: acc, sz + 1, max max_lvl a.var.level, c_hist
@ -748,20 +748,20 @@ let theory_analyze dep =
seen := q :: !seen; seen := q :: !seen;
if q.var.level >= max_lvl then incr pathC if q.var.level >= max_lvl then incr pathC
else begin else begin
learnt := q :: !learnt; learnt := q :: !learnt;
incr size; incr size;
blevel := max !blevel q.var.level blevel := max !blevel q.var.level
end end
end end
done; done;
(* look for the next node to expand *) (* look for the next node to expand *)
while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done;
decr pathC; decr pathC;
let p = Vec.get env.trail !tr_ind in let p = Vec.get env.trail !tr_ind in
decr tr_ind; decr tr_ind;
match !pathC, p.var.reason with match !pathC, p.var.reason with
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, None -> assert false | n, None -> assert false
@ -779,7 +779,7 @@ let add_boolean_conflict confl =
cancel_until blevel; cancel_until blevel;
record_learnt_clause blevel learnt history size record_learnt_clause blevel learnt history size
let search n_of_conflicts n_of_learnts = let search n_of_conflicts n_of_learnts =
let conflictC = ref 0 in let conflictC = ref 0 in
env.starts <- env.starts + 1; env.starts <- env.starts + 1;
while (true) do while (true) do
@ -787,20 +787,20 @@ let search n_of_conflicts n_of_learnts =
| Some confl -> (* Conflict *) | Some confl -> (* Conflict *)
incr conflictC; incr conflictC;
add_boolean_conflict confl add_boolean_conflict confl
| None -> (* No Conflict *) | None -> (* No Conflict *)
match theory_propagate () with match theory_propagate () with
| Some dep -> | Some dep ->
incr conflictC; incr conflictC;
env.conflicts <- env.conflicts + 1; env.conflicts <- env.conflicts + 1;
if decision_level() = 0 then report_t_unsat dep; (* T-L conflict *) if decision_level() = 0 then report_t_unsat dep; (* T-L conflict *)
let blevel, learnt, history, size = theory_analyze dep in let blevel, learnt, history, size = theory_analyze dep in
cancel_until blevel; cancel_until blevel;
record_learnt_clause blevel learnt history size record_learnt_clause blevel learnt history size
| None -> | None ->
if nb_assigns () = env.nb_init_vars then raise Sat; if nb_assigns () = env.nb_init_vars then raise Sat;
if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then
begin begin
env.progress_estimate <- progress_estimate(); env.progress_estimate <- progress_estimate();
cancel_until 0; cancel_until 0;
@ -808,8 +808,8 @@ let search n_of_conflicts n_of_learnts =
end; end;
if decision_level() = 0 then simplify (); if decision_level() = 0 then simplify ();
if n_of_learnts >= 0 && if n_of_learnts >= 0 &&
Vec.size env.learnts - nb_assigns() >= n_of_learnts then Vec.size env.learnts - nb_assigns() >= n_of_learnts then
reduce_db(); reduce_db();
env.decisions <- env.decisions + 1; env.decisions <- env.decisions + 1;
@ -822,7 +822,7 @@ let search n_of_conflicts n_of_learnts =
enqueue next.pa current_level None enqueue next.pa current_level None
done done
let check_clause c = let check_clause c =
let b = ref false in let b = ref false in
let atoms = c.atoms in let atoms = c.atoms in
for i = 0 to Vec.size atoms - 1 do for i = 0 to Vec.size atoms - 1 do
@ -830,16 +830,16 @@ let check_clause c =
b := !b || a.is_true b := !b || a.is_true
done; done;
assert (!b) assert (!b)
let check_vec vec = let check_vec vec =
for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
let check_model () = let check_model () =
check_vec env.clauses; check_vec env.clauses;
check_vec env.learnts check_vec env.learnts
let solve () = let solve () =
if env.is_unsat then raise (Unsat env.unsat_core); if env.is_unsat then raise (Unsat env.unsat_core);
let n_of_conflicts = ref (to_float env.restart_first) in let n_of_conflicts = ref (to_float env.restart_first) in
let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
@ -850,11 +850,11 @@ let solve () =
n_of_conflicts := !n_of_conflicts *. env.restart_inc; n_of_conflicts := !n_of_conflicts *. env.restart_inc;
n_of_learnts := !n_of_learnts *. env.learntsize_inc; n_of_learnts := !n_of_learnts *. env.learntsize_inc;
done; done;
with with
| Sat -> | Sat ->
(*check_model ();*) (*check_model ();*)
raise Sat raise Sat
| (Unsat cl) as e -> | (Unsat cl) as e ->
(* check_unsat_core cl; *) (* check_unsat_core cl; *)
raise e raise e
@ -863,13 +863,13 @@ exception Trivial
let partition atoms init = let partition atoms init =
let rec partition_aux trues unassigned falses init = function let rec partition_aux trues unassigned falses init = function
| [] -> trues @ unassigned @ falses, init | [] -> trues @ unassigned @ falses, init
| a::r -> | a::r ->
if a.is_true then if a.is_true then
if a.var.level = 0 then raise Trivial if a.var.level = 0 then raise Trivial
else (a::trues) @ unassigned @ falses @ r, init else (a::trues) @ unassigned @ falses @ r, init
else if a.neg.is_true then else if a.neg.is_true then
if a.var.level = 0 then if a.var.level = 0 then
partition_aux trues unassigned falses partition_aux trues unassigned falses
(List.rev_append (a.var.vpremise) init) r (List.rev_append (a.var.vpremise) init) r
else partition_aux trues unassigned (a::falses) init r else partition_aux trues unassigned (a::falses) init r
else partition_aux trues (a::unassigned) falses init r else partition_aux trues (a::unassigned) falses init r
@ -882,12 +882,12 @@ let add_clause ~cnumber atoms =
let init_name = string_of_int cnumber in let init_name = string_of_int cnumber in
let init0 = make_clause init_name atoms (List.length atoms) false [] in let init0 = make_clause init_name atoms (List.length atoms) false [] in
try try
let atoms, init = let atoms, init =
if decision_level () = 0 then if decision_level () = 0 then
let atoms, init = List.fold_left let atoms, init = List.fold_left
(fun (atoms, init) a -> (fun (atoms, init) a ->
if a.is_true then raise Trivial; if a.is_true then raise Trivial;
if a.neg.is_true then if a.neg.is_true then
atoms, (List.rev_append (a.var.vpremise) init) atoms, (List.rev_append (a.var.vpremise) init)
else a::atoms, init else a::atoms, init
) ([], [init0]) atoms in ) ([], [init0]) atoms in
@ -896,41 +896,41 @@ let add_clause ~cnumber atoms =
in in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with
| [] -> | [] ->
report_b_unsat init0; report_b_unsat init0;
| a::_::_ -> | a::_::_ ->
let name = fresh_name () in let name = fresh_name () in
let clause = make_clause name atoms size false init in let clause = make_clause name atoms size false init in
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;
if a.neg.is_true then begin if a.neg.is_true then begin
let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
cancel_until lvl; cancel_until lvl;
add_boolean_conflict clause add_boolean_conflict clause
end end
| [a] -> | [a] ->
cancel_until 0; cancel_until 0;
a.var.vpremise <- init; a.var.vpremise <- init;
enqueue a 0 None; enqueue a 0 None;
match propagate () with match propagate () with
None -> () | Some confl -> report_b_unsat confl None -> () | Some confl -> report_b_unsat confl
with Trivial -> () with Trivial -> ()
let add_clauses cnf ~cnumber = let add_clauses cnf ~cnumber =
List.iter (add_clause ~cnumber) cnf; List.iter (add_clause ~cnumber) cnf;
match theory_propagate () with match theory_propagate () with
None -> () | Some dep -> report_t_unsat dep None -> () | Some dep -> report_t_unsat dep
let init_solver cnf ~cnumber = let init_solver cnf ~cnumber =
let nbv, _ = made_vars_info () in let nbv, _ = made_vars_info () in
let nbc = env.nb_init_clauses + List.length cnf in let nbc = env.nb_init_clauses + List.length cnf in
Vec.grow_to_by_double env.vars nbv; Vec.grow_to_by_double env.vars nbv;
Iheap.grow_to_by_double env.order nbv; Iheap.grow_to_by_double env.order nbv;
List.iter List.iter
(List.iter (List.iter
(fun a -> (fun a ->
Vec.set env.vars a.var.vid a.var; Vec.set env.vars a.var.vid a.var;
insert_var_order a.var insert_var_order a.var
@ -952,11 +952,11 @@ let clear () =
let empty_theory = Th.empty () in let empty_theory = Th.empty () in
env.is_unsat <- false; env.is_unsat <- false;
env.unsat_core <- []; env.unsat_core <- [];
env.clauses <- Vec.make 0 dummy_clause; env.clauses <- Vec.make 0 dummy_clause;
env.learnts <- Vec.make 0 dummy_clause; env.learnts <- Vec.make 0 dummy_clause;
env.clause_inc <- 1.; env.clause_inc <- 1.;
env.var_inc <- 1.; env.var_inc <- 1.;
env.vars <- Vec.make 0 dummy_var; env.vars <- Vec.make 0 dummy_var;
env.qhead <- 0; env.qhead <- 0;
env.simpDB_assigns <- -1; env.simpDB_assigns <- -1;
env.simpDB_props <- 0; env.simpDB_props <- 0;

80
smt/solver_types.ml
View file

@ -13,7 +13,7 @@
open Format open Format
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = Hstring.make "<" let alt = Hstring.make "<"
let agt = Hstring.make ">" let agt = Hstring.make ">"
@ -31,8 +31,8 @@ type var =
mutable level : int; mutable level : int;
mutable reason: reason; mutable reason: reason;
mutable vpremise : premise} mutable vpremise : premise}
and atom = and atom =
{ var : var; { var : var;
lit : Literal.LT.t; lit : Literal.LT.t;
neg : atom; neg : atom;
@ -40,9 +40,9 @@ and atom =
mutable is_true : bool; mutable is_true : bool;
aid : int } aid : int }
and clause = and clause =
{ name : string; { name : string;
mutable atoms : atom Vec.t ; mutable atoms : atom Vec.t ;
mutable activity : float; mutable activity : float;
mutable removed : bool; mutable removed : bool;
learnt : bool; learnt : bool;
@ -59,21 +59,21 @@ let dummy_lit = Literal.LT.make (Literal.Eq(Term.vrai,Term.vrai))
let rec dummy_var = let rec dummy_var =
{ vid = -101; { vid = -101;
pa = dummy_atom; pa = dummy_atom;
na = dummy_atom; na = dummy_atom;
level = -1; level = -1;
reason = None; reason = None;
weight = -1.; weight = -1.;
seen = false; seen = false;
vpremise = [] } vpremise = [] }
and dummy_atom = and dummy_atom =
{ var = dummy_var; { var = dummy_var;
lit = dummy_lit; lit = dummy_lit;
watched = {Vec.dummy=dummy_clause; data=[||]; sz=0}; watched = {Vec.dummy=dummy_clause; data=[||]; sz=0};
neg = dummy_atom; neg = dummy_atom;
is_true = false; is_true = false;
aid = -102 } aid = -102 }
and dummy_clause = and dummy_clause =
{ name = ""; { name = "";
atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0}; atoms = {Vec.dummy=dummy_atom; data=[||]; sz=0};
activity = -1.; activity = -1.;
removed = false; removed = false;
@ -82,8 +82,8 @@ and dummy_clause =
module MA = Literal.LT.Map module MA = Literal.LT.Map
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = Hstring.make "<" let alt = Hstring.make "<"
let agt = Hstring.make ">" let agt = Hstring.make ">"
let is_le n = Hstring.compare n ale = 0 let is_le n = Hstring.compare n ale = 0
@ -132,7 +132,7 @@ let normal_form lit =
(* | Literal.Distinct(false,[_;_]) -> Literal.LT.neg lit, true *) (* | Literal.Distinct(false,[_;_]) -> Literal.LT.neg lit, true *)
(* | Literal.Builtin(true,n,[t1;t2]) when Builtin.is_gt n -> *) (* | Literal.Builtin(true,n,[t1;t2]) when Builtin.is_gt n -> *)
(* Literal.LT.neg lit, true *) (* Literal.LT.neg lit, true *)
(* | Literal.Builtin(false,n,[t1;t2]) when Builtin.is_le n -> *) (* | Literal.Builtin(false,n,[t1;t2]) when Builtin.is_le n -> *)
(* Literal.LT.neg lit, true *) (* Literal.LT.neg lit, true *)
(* | _ -> lit, false *) (* | _ -> lit, false *)
@ -143,33 +143,33 @@ let ma = ref MA.empty
let make_var = let make_var =
fun lit -> fun lit ->
let lit, negated = normal_form lit in let lit, negated = normal_form lit in
try MA.find lit !ma, negated try MA.find lit !ma, negated
with Not_found -> with Not_found ->
let cpt_fois_2 = !cpt_mk_var lsl 1 in let cpt_fois_2 = !cpt_mk_var lsl 1 in
let rec var = let rec var =
{ vid = !cpt_mk_var; { vid = !cpt_mk_var;
pa = pa; pa = pa;
na = na; na = na;
level = -1; level = -1;
reason = None; reason = None;
weight = 0.; weight = 0.;
seen = false; seen = false;
vpremise = []; vpremise = [];
} }
and pa = and pa =
{ var = var; { var = var;
lit = lit; lit = lit;
watched = Vec.make 10 dummy_clause; watched = Vec.make 10 dummy_clause;
neg = na; neg = na;
is_true = false; is_true = false;
aid = cpt_fois_2 (* aid = vid*2 *) } aid = cpt_fois_2 (* aid = vid*2 *) }
and na = and na =
{ var = var; { var = var;
lit = Literal.LT.neg lit; lit = Literal.LT.neg lit;
watched = Vec.make 10 dummy_clause; watched = Vec.make 10 dummy_clause;
neg = pa; neg = pa;
is_true = false; is_true = false;
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
ma := MA.add lit var !ma; ma := MA.add lit var !ma;
incr cpt_mk_var; incr cpt_mk_var;
var, negated var, negated
@ -178,9 +178,9 @@ let made_vars_info () = !cpt_mk_var, MA.fold (fun lit var acc -> var::acc)!ma []
let add_atom lit = let add_atom lit =
let var, negated = make_var lit in let var, negated = make_var lit in
if negated then var.na else var.pa if negated then var.na else var.pa
let make_clause name ali sz_ali is_learnt premise = let make_clause name ali sz_ali is_learnt premise =
let atoms = Vec.from_list ali sz_ali dummy_atom in let atoms = Vec.from_list ali sz_ali dummy_atom in
{ name = name; { name = name;
atoms = atoms; atoms = atoms;
@ -188,23 +188,23 @@ let make_clause name ali sz_ali is_learnt premise =
learnt = is_learnt; learnt = is_learnt;
activity = 0.; activity = 0.;
cpremise = premise} cpremise = premise}
let fresh_lname = let fresh_lname =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "L" ^ (string_of_int !cpt) fun () -> incr cpt; "L" ^ (string_of_int !cpt)
let fresh_dname = let fresh_dname =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "D" ^ (string_of_int !cpt) fun () -> incr cpt; "D" ^ (string_of_int !cpt)
let fresh_name = let fresh_name =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "C" ^ (string_of_int !cpt) fun () -> incr cpt; "C" ^ (string_of_int !cpt)
module Clause = struct module Clause = struct
let size c = Vec.size c.atoms let size c = Vec.size c.atoms
let pop c = Vec.pop c.atoms let pop c = Vec.pop c.atoms
let shrink c i = Vec.shrink c.atoms i let shrink c i = Vec.shrink c.atoms i
@ -227,32 +227,32 @@ end
module Debug = struct module Debug = struct
let sign a = if a==a.var.pa then "" else "-" let sign a = if a==a.var.pa then "" else "-"
let level a = let level a =
match a.var.level, a.var.reason with match a.var.level, a.var.reason with
| n, _ when n < 0 -> assert false | n, _ when n < 0 -> assert false
| 0, Some c -> sprintf "->0/%s" c.name | 0, Some c -> sprintf "->0/%s" c.name
| 0, None -> "@0" | 0, None -> "@0"
| n, Some c -> sprintf "->%d/%s" n c.name | n, Some c -> sprintf "->%d/%s" n c.name
| n, None -> sprintf "@@%d" n | n, None -> sprintf "@@%d" n
let value a = let value a =
if a.is_true then sprintf "[T%s]" (level a) if a.is_true then sprintf "[T%s]" (level a)
else if a.neg.is_true then sprintf "[F%s]" (level a) else if a.neg.is_true then sprintf "[F%s]" (level a)
else "" else ""
let value_ms_like a = let value_ms_like a =
if a.is_true then sprintf ":1%s" (level a) if a.is_true then sprintf ":1%s" (level a)
else if a.neg.is_true then sprintf ":0%s" (level a) else if a.neg.is_true then sprintf ":0%s" (level a)
else ":X" else ":X"
let premise fmt v = let premise fmt v =
List.iter (fun {name=name} -> fprintf fmt "%s," name) v List.iter (fun {name=name} -> fprintf fmt "%s," name) v
let atom fmt a = let atom fmt a =
fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}"
(sign a) (a.var.vid+1) (value a) Literal.LT.print a.lit (sign a) (a.var.vid+1) (value a) Literal.LT.print a.lit
premise a.var.vpremise premise a.var.vpremise
@ -260,7 +260,7 @@ module Debug = struct
let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l
let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr
let atoms_vec fmt vec = let atoms_vec fmt vec =
for i = 0 to Vec.size vec - 1 do for i = 0 to Vec.size vec - 1 do
fprintf fmt "%a ; " atom (Vec.get vec i) fprintf fmt "%a ; " atom (Vec.get vec i)
done done

14
smt/solver_types.mli
View file

@ -13,7 +13,7 @@
type var = type var =
{ vid : int; { vid : int;
pa : atom; pa : atom;
na : atom; na : atom;
@ -22,8 +22,8 @@ type var =
mutable level : int; mutable level : int;
mutable reason : reason; mutable reason : reason;
mutable vpremise : premise } mutable vpremise : premise }
and atom = and atom =
{ var : var; { var : var;
lit : Literal.LT.t; lit : Literal.LT.t;
neg : atom; neg : atom;
@ -31,7 +31,7 @@ and atom =
mutable is_true : bool; mutable is_true : bool;
aid : int } aid : int }
and clause = and clause =
{ name : string; { name : string;
mutable atoms : atom Vec.t; mutable atoms : atom Vec.t;
mutable activity : float; mutable activity : float;
@ -54,7 +54,7 @@ val dummy_clause : clause
val make_var : Literal.LT.t -> var * bool val make_var : Literal.LT.t -> var * bool
val add_atom : Literal.LT.t -> atom val add_atom : Literal.LT.t -> atom
val make_clause : string -> atom list -> int -> bool -> premise-> clause val make_clause : string -> atom list -> int -> bool -> premise-> clause
@ -73,9 +73,9 @@ val clear : unit -> unit
end end
module Debug: sig module Debug: sig
val atom : Format.formatter -> atom -> unit val atom : Format.formatter -> atom -> unit
val clause : Format.formatter -> clause -> unit val clause : Format.formatter -> clause -> unit
end end

86
smt/sum.ml
View file

@ -14,7 +14,7 @@
open Format open Format
open Sig open Sig
open Exception open Exception
module Sy = Symbols module Sy = Symbols
module T = Term module T = Term
module A = Literal module A = Literal
@ -36,27 +36,27 @@ module Make(X : ALIEN) = struct
type r = X.r type r = X.r
let name = "Sum" let name = "Sum"
let unsolvable _ = false let unsolvable _ = false
let is_mine_a _ = false let is_mine_a _ = false
let is_mine_symb = function let is_mine_symb = function
| Sy.Name(_, Sy.Constructor) -> true | Sy.Name(_, Sy.Constructor) -> true
| _ -> false | _ -> false
let fully_interpreted sb = true let fully_interpreted sb = true
let type_info = function let type_info = function
| Cons (_, ty) -> ty | Cons (_, ty) -> ty
| Alien x -> X.type_info x | Alien x -> X.type_info x
let is_mine_type c = match type_info c with let is_mine_type c = match type_info c with
| Ty.Tsum _ -> true | Ty.Tsum _ -> true
| _ -> false | _ -> false
let color _ = assert false let color _ = assert false
let print fmt = function let print fmt = function
| Cons (hs,ty) -> fprintf fmt "%s" (Hs.view hs) | Cons (hs,ty) -> fprintf fmt "%s" (Hs.view hs)
| Alien x -> fprintf fmt "%a" X.print x | Alien x -> fprintf fmt "%a" X.print x
@ -64,41 +64,41 @@ module Make(X : ALIEN) = struct
let embed r = let embed r =
match X.extract r with match X.extract r with
| Some c -> c | Some c -> c
| None -> Alien r | None -> Alien r
let is_mine = function let is_mine = function
| Alien r -> r | Alien r -> r
| Cons(hs,ty) as c -> X.embed c | Cons(hs,ty) as c -> X.embed c
let compare c1 c2 = let compare c1 c2 =
match c1 , c2 with match c1 , c2 with
| Cons (h1,ty1) , Cons (h2,ty2) -> | Cons (h1,ty1) , Cons (h2,ty2) ->
let n = Hs.compare h1 h2 in let n = Hs.compare h1 h2 in
if n <> 0 then n else Ty.compare ty1 ty2 if n <> 0 then n else Ty.compare ty1 ty2
| Alien r1, Alien r2 -> X.compare r1 r2 | Alien r1, Alien r2 -> X.compare r1 r2
| Alien _ , Cons _ -> 1 | Alien _ , Cons _ -> 1
| Cons _ , Alien _ -> -1 | Cons _ , Alien _ -> -1
let hash = function let hash = function
| Cons (h, ty) -> Hstring.hash h + 19 * Ty.hash ty | Cons (h, ty) -> Hstring.hash h + 19 * Ty.hash ty
| Alien r -> X.hash r | Alien r -> X.hash r
let leaves _ = [] let leaves _ = []
let subst p v c = let subst p v c =
let cr = is_mine c in let cr = is_mine c in
if X.equal p cr then v if X.equal p cr then v
else else
match c with match c with
| Cons(hs,t) -> cr | Cons(hs,t) -> cr
| Alien r -> X.subst p v r | Alien r -> X.subst p v r
let make t = match T.view t with let make t = match T.view t with
| {T.f=Sy.Name(hs, Sy.Constructor); xs=[];ty=ty} -> | {T.f=Sy.Name(hs, Sy.Constructor); xs=[];ty=ty} ->
is_mine (Cons(hs,ty)), [] is_mine (Cons(hs,ty)), []
| _ -> assert false | _ -> assert false
let solve a b = let solve a b =
match embed a, embed b with match embed a, embed b with
| Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> [] | Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> []
| Cons(c1,_) , Cons(c2,_) -> raise Unsolvable | Cons(c1,_) , Cons(c2,_) -> raise Unsolvable
@ -131,29 +131,29 @@ module Make(X : ALIEN) = struct
end end
let values_of r = match X.type_info r with let values_of r = match X.type_info r with
| Ty.Tsum (_,l) -> | Ty.Tsum (_,l) ->
Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l) Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l)
| _ -> None | _ -> None
let add_diseq hss sm1 sm2 dep env eqs = let add_diseq hss sm1 sm2 dep env eqs =
match sm1, sm2 with match sm1, sm2 with
| Alien r , Cons(h,ty) | Alien r , Cons(h,ty)
| Cons (h,ty), Alien r -> | Cons (h,ty), Alien r ->
let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in
let enum = HSS.remove h enum in let enum = HSS.remove h enum in
let ex = Ex.union ex dep in let ex = Ex.union ex dep in
if HSS.is_empty enum then raise (Inconsistent ex) if HSS.is_empty enum then raise (Inconsistent ex)
else else
let env = MX.add r (enum, ex) env in let env = MX.add r (enum, ex) env in
if HSS.cardinal enum = 1 then if HSS.cardinal enum = 1 then
let h' = HSS.choose enum in let h' = HSS.choose enum in
env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs
else env, eqs else env, eqs
| Alien r1 , Alien r2 -> env, eqs | Alien r1 , Alien r2 -> env, eqs
| _ -> env, eqs | _ -> env, eqs
let add_eq hss sm1 sm2 dep env eqs = let add_eq hss sm1 sm2 dep env eqs =
match sm1, sm2 with match sm1, sm2 with
| Alien r, Cons(h,ty) | Cons (h,ty), Alien r -> | Alien r, Cons(h,ty) | Cons (h,ty), Alien r ->
@ -161,13 +161,13 @@ module Make(X : ALIEN) = struct
let ex = Ex.union ex dep in let ex = Ex.union ex dep in
if not (HSS.mem h enum) then raise (Inconsistent ex); if not (HSS.mem h enum) then raise (Inconsistent ex);
MX.add r (HSS.singleton h, ex) env, eqs 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 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 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 ex = Ex.union dep (Ex.union ex1 ex2) in
let diff = HSS.inter enum1 enum2 in let diff = HSS.inter enum1 enum2 in
if HSS.is_empty diff then raise (Inconsistent ex); if HSS.is_empty diff then raise (Inconsistent ex);
let env = MX.add r1 (diff, ex) env in let env = MX.add r1 (diff, ex) env in
let env = MX.add r2 (diff, ex) env in let env = MX.add r2 (diff, ex) env in
@ -179,28 +179,28 @@ module Make(X : ALIEN) = struct
| _ -> env, eqs | _ -> env, eqs
let assume env la = let assume env la =
let aux bol r1 r2 dep env eqs = function let aux bol r1 r2 dep env eqs = function
| None -> env, eqs | None -> env, eqs
| Some hss -> | Some hss ->
Debug.assume bol r1 r2; Debug.assume bol r1 r2;
if bol then if bol then
add_eq hss (embed r1) (embed r2) dep env eqs add_eq hss (embed r1) (embed r2) dep env eqs
else else
add_diseq hss (embed r1) (embed r2) dep env eqs add_diseq hss (embed r1) (embed r2) dep env eqs
in in
Debug.print_env env; Debug.print_env env;
let env, eqs = let env, eqs =
List.fold_left List.fold_left
(fun (env,eqs) -> function (fun (env,eqs) -> function
| A.Eq(r1,r2), _, ex -> | 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 -> | 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, eqs
) (env,[]) la ) (env,[]) la
in in
env, { assume = eqs; remove = [] } env, { assume = eqs; remove = [] }
@ -223,15 +223,15 @@ module Make(X : ALIEN) = struct
let r' = is_mine (Cons(hs,X.type_info r)) in let r' = is_mine (Cons(hs,X.type_info r)) in
[A.Eq(r, r'), Ex.empty, Num.Int n] [A.Eq(r, r'), Ex.empty, Num.Int n]
| None -> [] | None -> []
let query env a_ex = let query env a_ex =
try ignore(assume env [a_ex]); Sig.No try ignore(assume env [a_ex]); Sig.No
with Inconsistent expl -> Sig.Yes expl with Inconsistent expl -> Sig.Yes expl
let add env r = match embed r, values_of r with let add env r = match embed r, values_of r with
| Alien r, Some hss -> | Alien r, Some hss ->
if MX.mem r env then env else if MX.mem r env then env else
MX.add r (hss, Ex.empty) env MX.add r (hss, Ex.empty) env
| _ -> env | _ -> env

2
smt/sum.mli
View file

@ -20,6 +20,6 @@ module type ALIEN = sig
val extract : r -> (r abstract) option val extract : r -> (r abstract) option
end end
module Make 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

18
smt/symbols.ml
View file

@ -13,13 +13,13 @@
open Hashcons open Hashcons
type operator = type operator =
| Plus | Minus | Mult | Div | Modulo | Plus | Minus | Mult | Div | Modulo
type name_kind = Ac | Constructor | Other type name_kind = Ac | Constructor | Other
type t = type t =
| True | True
| False | False
| Name of Hstring.t * name_kind | Name of Hstring.t * name_kind
| Int of Hstring.t | Int of Hstring.t
@ -47,7 +47,7 @@ let compare_kind k1 k2 = match k1, k2 with
| Constructor, Constructor -> 0 | Constructor, Constructor -> 0
let compare s1 s2 = match s1, s2 with let compare s1 s2 = match s1, s2 with
| Name (n1,k1), Name (n2,k2) -> | Name (n1,k1), Name (n2,k2) ->
let c = compare_kind k1 k2 in let c = compare_kind k1 k2 in
if c = 0 then Hstring.compare n1 n2 else c if c = 0 then Hstring.compare n1 n2 else c
| Name _, _ -> -1 | Name _, _ -> -1
@ -59,7 +59,7 @@ let compare s1 s2 = match s1, s2 with
| Int _, _ -> -1 | Int _, _ -> -1
| _ ,Int _ -> 1 | _ ,Int _ -> 1
| _ -> Pervasives.compare s1 s2 | _ -> Pervasives.compare s1 s2
let equal s1 s2 = compare s1 s2 = 0 let equal s1 s2 = compare s1 s2 = 0
let hash = function let hash = function
@ -73,8 +73,8 @@ let to_string = function
| Var x -> "*var* "^(Hstring.view x) | Var x -> "*var* "^(Hstring.view x)
| Int n -> Hstring.view n | Int n -> Hstring.view n
| Real n -> Hstring.view n | Real n -> Hstring.view n
| Op Plus -> "+" | Op Plus -> "+"
| Op Minus -> "-" | Op Minus -> "-"
| Op Mult -> "*" | Op Mult -> "*"
| Op Div -> "/" | Op Div -> "/"
| Op Modulo -> "%" | Op Modulo -> "%"
@ -86,6 +86,6 @@ let print fmt s = Format.fprintf fmt "%s" (to_string s)
module Map = module Map =
Map.Make(struct type t' = t type t=t' let compare=compare end) Map.Make(struct type t' = t type t=t' let compare=compare end)
module Set = module Set =
Set.Make(struct type t' = t type t=t' let compare=compare end) Set.Make(struct type t' = t type t=t' let compare=compare end)

8
smt/symbols.mli
View file

@ -11,13 +11,13 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
type operator = type operator =
| Plus | Minus | Mult | Div | Modulo | Plus | Minus | Mult | Div | Modulo
type name_kind = Ac | Constructor | Other type name_kind = Ac | Constructor | Other
type t = type t =
| True | True
| False | False
| Name of Hstring.t * name_kind | Name of Hstring.t * name_kind
| Int of Hstring.t | Int of Hstring.t

26
smt/term.ml
View file

@ -22,26 +22,26 @@ and t = view
module H = struct module H = struct
type t = view type t = view
let equal t1 t2 = try let equal t1 t2 = try
Sy.equal t1.f t2.f Sy.equal t1.f t2.f
&& List.for_all2 (==) t1.xs t2.xs && List.for_all2 (==) t1.xs t2.xs
&& Ty.equal t1.ty t2.ty && Ty.equal t1.ty t2.ty
with Invalid_argument _ -> false with Invalid_argument _ -> false
let hash t = let hash t =
abs (List.fold_left abs (List.fold_left
(fun acc x-> acc*19 +x.tag) (Sy.hash t.f + Ty.hash t.ty) (fun acc x-> acc*19 +x.tag) (Sy.hash t.f + Ty.hash t.ty)
t.xs) t.xs)
let tag tag x = {x with tag = tag} let tag tag x = {x with tag = tag}
end end
module T = Make(H) module T = Make(H)
let view t = t let view t = t
let rec print fmt t = let rec print fmt t =
let {f=x; xs=l; ty=ty} = view t in let {f=x; xs=l; ty=ty} = view t in
match x, l with match x, l with
| Sy.Op op, [e1; e2] -> | Sy.Op op, [e1; e2] ->
fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2 fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2
| _, [] -> fprintf fmt "%a" Sy.print x | _, [] -> fprintf fmt "%a" Sy.print x
| _, _ -> fprintf fmt "%a(%a)" Sy.print x print_list l | _, _ -> fprintf fmt "%a(%a)" Sy.print x print_list l
@ -72,11 +72,11 @@ let is_int t = (view t).ty= Ty.Tint
let is_real t = (view t).ty= Ty.Treal let is_real t = (view t).ty= Ty.Treal
let equal t1 t2 = t1 == t2 let equal t1 t2 = t1 == t2
let hash t = t.tag let hash t = t.tag
module Set = module Set =
Set.Make(struct type t' = t type t=t' let compare=compare end) Set.Make(struct type t' = t type t=t' let compare=compare end)
module Map = module Map =
Map.Make(struct type t' = t type t=t' let compare=compare end) Map.Make(struct type t' = t type t=t' let compare=compare end)

18
smt/ty.ml
View file

@ -13,7 +13,7 @@
open Format open Format
type t = type t =
| Tint | Tint
| Treal | Treal
| Tbool | Tbool
@ -23,33 +23,33 @@ type t =
let hash t = let hash t =
match t with match t with
| Tabstract s -> Hstring.hash s | Tabstract s -> Hstring.hash s
| Tsum (s, l) -> | Tsum (s, l) ->
let h = let h =
List.fold_left List.fold_left
(fun h x -> 13 * h + Hstring.hash x) (Hstring.hash s) l (fun h x -> 13 * h + Hstring.hash x) (Hstring.hash s) l
in in
abs h abs h
| _ -> Hashtbl.hash t | _ -> Hashtbl.hash t
let equal t1 t2 = let equal t1 t2 =
match t1, t2 with match t1, t2 with
| Tabstract s1, Tabstract s2 | Tabstract s1, Tabstract s2
| Tsum (s1, _), Tsum (s2, _) -> | Tsum (s1, _), Tsum (s2, _) ->
Hstring.equal s1 s2 Hstring.equal s1 s2
| Tint, Tint | Treal, Treal | Tbool, Tbool -> true | Tint, Tint | Treal, Treal | Tbool, Tbool -> true
| _ -> false | _ -> false
let compare t1 t2 = let compare t1 t2 =
match t1, t2 with match t1, t2 with
| Tabstract s1, Tabstract s2 -> | Tabstract s1, Tabstract s2 ->
Hstring.compare s1 s2 Hstring.compare s1 s2
| Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1
| Tsum (s1, _), Tsum(s2, _) -> | Tsum (s1, _), Tsum(s2, _) ->
Hstring.compare s1 s2 Hstring.compare s1 s2
| Tsum _, _ -> -1 | _ , Tsum _ -> 1 | Tsum _, _ -> -1 | _ , Tsum _ -> 1
| t1, t2 -> Pervasives.compare t1 t2 | t1, t2 -> Pervasives.compare t1 t2
let print fmt ty = let print fmt ty =
match ty with match ty with
| Tint -> fprintf fmt "int" | Tint -> fprintf fmt "int"
| Treal -> fprintf fmt "real" | Treal -> fprintf fmt "real"

2
smt/ty.mli
View file

@ -11,7 +11,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
type t = type t =
| Tint | Tint
| Treal | Treal
| Tbool | Tbool

206
smt/uf.ml
View file

@ -28,9 +28,9 @@ module type S = sig
val find : t -> Term.t -> R.r * Explanation.t val find : t -> Term.t -> R.r * Explanation.t
val find_r : t -> R.r -> R.r * Explanation.t val find_r : t -> R.r -> R.r * Explanation.t
val union : val union :
t -> R.r -> R.r -> Explanation.t -> t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t val distinct : t -> R.r list -> Explanation.t -> t
@ -41,7 +41,7 @@ module type S = sig
val class_of : t -> Term.t -> Term.t list val class_of : t -> Term.t -> Term.t list
end end
module Make ( R : Sig.X ) = struct module Make ( R : Sig.X ) = struct
module L = List module L = List
@ -52,112 +52,112 @@ module Make ( R : Sig.X ) = struct
module T = Term module T = Term
module MapT = Term.Map module MapT = Term.Map
module SetT = Term.Set module SetT = Term.Set
module Lit = Literal.Make(struct type t = R.r include R end) module Lit = Literal.Make(struct type t = R.r include R end)
module MapL = Lit.Map module MapL = Lit.Map
module MapR = Map.Make(struct type t = R.r let compare = R.compare end) module MapR = Map.Make(struct type t = R.r let compare = R.compare end)
module SetR = Set.Make(struct type t = R.r let compare = R.compare end) module SetR = Set.Make(struct type t = R.r let compare = R.compare end)
module SetRR = Set.Make(struct module SetRR = Set.Make(struct
type t = R.r * R.r type t = R.r * R.r
let compare (r1, r1') (r2, r2') = let compare (r1, r1') (r2, r2') =
let c = R.compare r1 r2 in let c = R.compare r1 r2 in
if c <> 0 then c if c <> 0 then c
else R.compare r1' r2' else R.compare r1' r2'
end) end)
type t = { type t = {
(* term -> [t] *) (* term -> [t] *)
make : R.r MapT.t; make : R.r MapT.t;
(* representative table *) (* representative table *)
repr : (R.r * Ex.t) MapR.t; repr : (R.r * Ex.t) MapR.t;
(* r -> class (of terms) *) (* r -> class (of terms) *)
classes : SetT.t MapR.t; classes : SetT.t MapR.t;
(*associates each value r with the set of semantical values whose (*associates each value r with the set of semantical values whose
representatives contains r *) representatives contains r *)
gamma : SetR.t MapR.t; gamma : SetR.t MapR.t;
(* the disequations map *) (* the disequations map *)
neqs: Ex.t MapL.t MapR.t; neqs: Ex.t MapL.t MapR.t;
} }
let empty = { let empty = {
make = MapT.empty; make = MapT.empty;
repr = MapR.empty; repr = MapR.empty;
classes = MapR.empty; classes = MapR.empty;
gamma = MapR.empty; gamma = MapR.empty;
neqs = MapR.empty; neqs = MapR.empty;
} }
module Env = struct module Env = struct
let mem env t = MapT.mem t env.make let mem env t = MapT.mem t env.make
let lookup_by_t t env = let lookup_by_t t env =
try MapR.find (MapT.find t env.make) env.repr try MapR.find (MapT.find t env.make) env.repr
with Not_found -> 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 = let lookup_by_r r env =
try MapR.find r env.repr with Not_found -> r, Ex.empty try MapR.find r env.repr with Not_found -> r, Ex.empty
let lookup_for_neqs env r = let lookup_for_neqs env r =
try MapR.find r env.neqs with Not_found -> MapL.empty try MapR.find r env.neqs with Not_found -> MapL.empty
let add_to_classes t r classes = let add_to_classes t r classes =
MapR.add r MapR.add r
(SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty))
classes classes
let update_classes c nc classes = let update_classes c nc classes =
let s1 = try MapR.find c classes with Not_found -> SetT.empty in let 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 let s2 = try MapR.find nc classes with Not_found -> SetT.empty in
MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) MapR.remove c (MapR.add nc (SetT.union s1 s2) classes)
let add_to_gamma r c gamma = let add_to_gamma r c gamma =
L.fold_left L.fold_left
(fun gamma x -> (fun gamma x ->
let s = try MapR.find x gamma with Not_found -> SetR.empty in 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) MapR.add x (SetR.add r s) gamma) gamma (R.leaves c)
(* r1 = r2 => neqs(r1) \uplus neqs(r2) *) (* r1 = r2 => neqs(r1) \uplus neqs(r2) *)
let update_neqs r1 r2 dep env = let update_neqs r1 r2 dep env =
let nq_r1 = lookup_for_neqs env r1 in let nq_r1 = lookup_for_neqs env r1 in
let nq_r2 = lookup_for_neqs env r2 in let nq_r2 = lookup_for_neqs env r2 in
let mapl = let mapl =
MapL.fold MapL.fold
(fun l1 ex1 mapl -> (fun l1 ex1 mapl ->
try try
let ex2 = MapL.find l1 mapl in let ex2 = MapL.find l1 mapl in
let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *)
raise (Inconsistent ex) raise (Inconsistent ex)
with Not_found -> with Not_found ->
MapL.add l1 (Ex.union ex1 dep) mapl) MapL.add l1 (Ex.union ex1 dep) mapl)
nq_r1 nq_r2 nq_r1 nq_r2
in in
MapR.add r2 mapl (MapR.add r1 mapl env.neqs) MapR.add r2 mapl (MapR.add r1 mapl env.neqs)
let filter_leaves r = let filter_leaves r =
L.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) L.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r)
let canon_empty st env = let canon_empty st env =
SetR.fold SetR.fold
(fun p ((z, ex) as acc) -> (fun p ((z, ex) as acc) ->
let q, ex_q = lookup_by_r p env in 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) if R.equal p q then acc else (p,q)::z, Ex.union ex_q ex)
st ([], Ex.empty) st ([], Ex.empty)
let canon_aux rx = List.fold_left (fun r (p,v) -> R.subst p v r) rx let canon_aux rx = List.fold_left (fun r (p,v) -> R.subst p v r) rx
let rec canon env r ex_r = let rec canon env r ex_r =
let se = filter_leaves r in let se = filter_leaves r in
let subst, ex_subst = canon_empty se env in let subst, ex_subst = canon_empty se env in
let r2 = canon_aux r subst in let r2 = canon_aux r subst in
@ -169,38 +169,38 @@ module Make ( R : Sig.X ) = struct
let find_or_normal_form env r = let find_or_normal_form env r =
try MapR.find r env.repr with Not_found -> normal_form env r try MapR.find r env.repr with Not_found -> normal_form env r
let init_leaf env p = let init_leaf env p =
let in_repr = MapR.mem p env.repr in let in_repr = MapR.mem p env.repr in
let in_neqs = MapR.mem p env.neqs in let in_neqs = MapR.mem p env.neqs in
{ env with { env with
repr = repr =
if in_repr then env.repr if in_repr then env.repr
else MapR.add p (p, Ex.empty) env.repr; else MapR.add p (p, Ex.empty) env.repr;
classes = classes =
if in_repr then env.classes if in_repr then env.classes
else update_classes p p env.classes; else update_classes p p env.classes;
gamma = gamma =
if in_repr then env.gamma if in_repr then env.gamma
else add_to_gamma p p env.gamma ; else add_to_gamma p p env.gamma ;
neqs = neqs =
if in_neqs then env.neqs if in_neqs then env.neqs
else update_neqs p p Ex.empty env } else update_neqs p p Ex.empty env }
let init_term env t = let init_term env t =
let mkr, ctx = R.make t in let mkr, ctx = R.make t in
let rp, ex = normal_form env mkr in let rp, ex = normal_form env mkr in
{ make = MapT.add t mkr env.make; { make = MapT.add t mkr env.make;
repr = MapR.add mkr (rp,ex) env.repr; repr = MapR.add mkr (rp,ex) env.repr;
classes = add_to_classes t rp env.classes; classes = add_to_classes t rp env.classes;
gamma = add_to_gamma mkr rp env.gamma; gamma = add_to_gamma mkr rp env.gamma;
neqs = neqs =
if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *)
else MapR.add rp MapL.empty env.neqs}, ctx else MapR.add rp MapL.empty env.neqs}, ctx
let update_aux dep set env= let update_aux dep set env=
SetRR.fold SetRR.fold
(fun (rr, nrr) env -> (fun (rr, nrr) env ->
{ env with { env with
neqs = update_neqs rr nrr dep env ; neqs = update_neqs rr nrr dep env ;
classes = update_classes rr nrr env.classes}) classes = update_classes rr nrr env.classes})
@ -209,37 +209,37 @@ module Make ( R : Sig.X ) = struct
let apply_sigma_uf env (p, v, dep) = let apply_sigma_uf env (p, v, dep) =
assert (MapR.mem p env.gamma); assert (MapR.mem p env.gamma);
let use_p = MapR.find p env.gamma in let use_p = MapR.find p env.gamma in
try try
let env, tch, neqs_to_up = SetR.fold let env, tch, neqs_to_up = SetR.fold
(fun r (env, touched, neqs_to_up) -> (fun r (env, touched, neqs_to_up) ->
let rr, ex = MapR.find r env.repr in let rr, ex = MapR.find r env.repr in
let nrr = R.subst p v rr in let nrr = R.subst p v rr in
if R.equal rr nrr then env, touched, neqs_to_up if R.equal rr nrr then env, touched, neqs_to_up
else else
let ex = Ex.union ex dep in let ex = Ex.union ex dep in
let env = let env =
{env with {env with
repr = MapR.add r (nrr, ex) env.repr; repr = MapR.add r (nrr, ex) env.repr;
gamma = add_to_gamma r nrr env.gamma } gamma = add_to_gamma r nrr env.gamma }
in in
env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up
) use_p (env, [], SetRR.empty) in ) use_p (env, [], SetRR.empty) in
(* Correction : Do not update neqs twice for the same r *) (* Correction : Do not update neqs twice for the same r *)
update_aux dep neqs_to_up env, tch update_aux dep neqs_to_up env, tch
with Not_found -> assert false with Not_found -> assert false
let apply_sigma eqs env tch ((p, v, dep) as sigma) = let apply_sigma eqs env tch ((p, v, dep) as sigma) =
let env = init_leaf env p in let env = init_leaf env p in
let env, touched = apply_sigma_uf env sigma in let env, touched = apply_sigma_uf env sigma in
env, ((p, touched, v) :: tch) env, ((p, touched, v) :: tch)
end end
let add env t = let add env t =
if MapT.mem t env.make then env, [] else Env.init_term env t if MapT.mem t env.make then env, [] else Env.init_term env t
let ac_solve eqs dep (env, tch) (p, v) = let ac_solve eqs dep (env, tch) (p, v) =
(* pourquoi recuperer le representant de rv? r = rv d'apres testopt *) (* pourquoi recuperer le representant de rv? r = rv d'apres testopt *)
(* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *) (* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *)
let rv, ex_rv = Env.find_or_normal_form env v in let rv, ex_rv = Env.find_or_normal_form env v in
@ -248,51 +248,51 @@ module Make ( R : Sig.X ) = struct
let dep = Ex.union ex_rv dep in let dep = Ex.union ex_rv dep in
Env.apply_sigma eqs env tch (p, rv, dep) Env.apply_sigma eqs env tch (p, rv, dep)
let x_solve env r1 r2 dep = let x_solve env r1 r2 dep =
let rr1, ex_r1 = Env.find_or_normal_form env r1 in let rr1, ex_r1 = Env.find_or_normal_form env r1 in
let rr2, ex_r2 = Env.find_or_normal_form env r2 in let rr2, ex_r2 = Env.find_or_normal_form env r2 in
let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in
if R.equal rr1 rr2 then begin if R.equal rr1 rr2 then begin
[] (* Remove rule *) [] (* Remove rule *)
end end
else else
begin begin
ignore (Env.update_neqs rr1 rr2 dep env); ignore (Env.update_neqs rr1 rr2 dep env);
try R.solve rr1 rr2 try R.solve rr1 rr2
with Unsolvable -> with Unsolvable ->
raise (Inconsistent dep) raise (Inconsistent dep)
end end
let rec ac_x eqs env tch = let rec ac_x eqs env tch =
if Queue.is_empty eqs then env, tch if Queue.is_empty eqs then env, tch
else else
let r1, r2, dep = Queue.pop eqs in let r1, r2, dep = Queue.pop eqs in
let sbs = x_solve env r1 r2 dep in let sbs = x_solve env r1 r2 dep in
let env, tch = List.fold_left (ac_solve eqs dep) (env, tch) sbs in let env, tch = List.fold_left (ac_solve eqs dep) (env, tch) sbs in
ac_x eqs env tch ac_x eqs env tch
let union env r1 r2 dep = let union env r1 r2 dep =
let equations = Queue.create () in let equations = Queue.create () in
Queue.push (r1,r2, dep) equations; Queue.push (r1,r2, dep) equations;
ac_x equations env [] ac_x equations env []
let rec distinct env rl dep = let rec distinct env rl dep =
let d = Lit.make (Literal.Distinct (false,rl)) in let d = Lit.make (Literal.Distinct (false,rl)) in
let env, _, newds = let env, _, newds =
List.fold_left List.fold_left
(fun (env, mapr, newds) r -> (fun (env, mapr, newds) r ->
let rr, ex = Env.find_or_normal_form env r in let rr, ex = Env.find_or_normal_form env r in
try try
let exr = MapR.find rr mapr in let exr = MapR.find rr mapr in
raise (Inconsistent (Ex.union ex exr)) raise (Inconsistent (Ex.union ex exr))
with Not_found -> with Not_found ->
let uex = Ex.union ex dep in let uex = Ex.union ex dep in
let mdis = let mdis =
try MapR.find rr env.neqs with Not_found -> MapL.empty in try MapR.find rr env.neqs with Not_found -> MapL.empty in
let mdis = let mdis =
try try
MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis
with Not_found -> with Not_found ->
MapL.add d uex mdis MapL.add d uex mdis
in in
let env = Env.init_leaf env rr in let env = Env.init_leaf env rr in
@ -302,29 +302,29 @@ module Make ( R : Sig.X ) = struct
(env, MapR.empty, []) (env, MapR.empty, [])
rl rl
in in
List.fold_left List.fold_left
(fun env (r1, ex1, mapr) -> (fun env (r1, ex1, mapr) ->
MapR.fold (fun r2 ex2 env -> MapR.fold (fun r2 ex2 env ->
let ex = Ex.union ex1 (Ex.union ex2 dep) in let ex = Ex.union ex1 (Ex.union ex2 dep) in
try match R.solve r1 r2 with try match R.solve r1 r2 with
| [a, b] -> | [a, b] ->
if (R.equal a r1 && R.equal b r2) || if (R.equal a r1 && R.equal b r2) ||
(R.equal a r2 && R.equal b r1) then env (R.equal a r2 && R.equal b r1) then env
else else
distinct env [a; b] ex distinct env [a; b] ex
| [] -> | [] ->
raise (Inconsistent ex) raise (Inconsistent ex)
| _ -> env | _ -> env
with Unsolvable -> env) mapr env) with Unsolvable -> env) mapr env)
env newds env newds
let are_equal env t1 t2 = let are_equal env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in let r2, ex_r2 = Env.lookup_by_t t2 env in
if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No
let are_distinct env t1 t2 = let are_distinct env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in let r2, ex_r2 = Env.lookup_by_t t2 env in
try try
@ -332,25 +332,25 @@ module Make ( R : Sig.X ) = struct
No No
with Inconsistent ex -> Yes(ex) with Inconsistent ex -> Yes(ex)
let already_distinct env lr = let already_distinct env lr =
let d = Lit.make (Literal.Distinct (false,lr)) in let d = Lit.make (Literal.Distinct (false,lr)) in
try try
List.iter (fun r -> List.iter (fun r ->
let mdis = MapR.find r env.neqs in let mdis = MapR.find r env.neqs in
ignore (MapL.find d mdis) ignore (MapL.find d mdis)
) lr; ) lr;
true true
with Not_found -> false with Not_found -> false
let find env t = let find env t =
Env.lookup_by_t t env Env.lookup_by_t t env
let find_r = Env.find_or_normal_form let find_r = Env.find_or_normal_form
let mem = Env.mem let mem = Env.mem
let class_of env t = let class_of env t =
try try
let rt, _ = MapR.find (MapT.find t env.make) env.repr in let rt, _ = MapR.find (MapT.find t env.make) env.repr in
SetT.elements (MapR.find rt env.classes) SetT.elements (MapR.find rt env.classes)
with Not_found -> [t] with Not_found -> [t]

4
smt/uf.mli
View file

@ -26,8 +26,8 @@ module type S = sig
val find_r : t -> R.r -> R.r * Explanation.t val find_r : t -> R.r -> R.r * Explanation.t
val union : val union :
t -> R.r -> R.r -> Explanation.t -> t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t val distinct : t -> R.r list -> Explanation.t -> t

42
smt/use.ml
View file

@ -25,13 +25,13 @@ module SA = Set.Make(struct
end) end)
type elt = ST.t * SA.t type elt = ST.t * SA.t
module Make (X : Sig.X) = struct module Make (X : Sig.X) = struct
let inter_tpl (x1,y1) (x2,y2) = ST.inter x1 x2, SA.inter y1 y2 let inter_tpl (x1,y1) (x2,y2) = ST.inter x1 x2, SA.inter y1 y2
let union_tpl (x1,y1) (x2,y2) = ST.union x1 x2, SA.union y1 y2 let union_tpl (x1,y1) (x2,y2) = ST.union x1 x2, SA.union y1 y2
let bottom = Hstring.make "@bottom" let bottom = Hstring.make "@bottom"
let leaves r = let leaves r =
let one, _ = X.make (T.make (Symbols.name bottom) [] Ty.Tint) in let one, _ = X.make (T.make (Symbols.name bottom) [] Ty.Tint) in
match X.leaves r with [] -> [one] | l -> l match X.leaves r with [] -> [one] | l -> l
@ -41,39 +41,39 @@ module Make (X : Sig.X) = struct
type t = elt G.t type t = elt G.t
let find k m = try find k m with Not_found -> (ST.empty,SA.empty) let find k m = try find k m with Not_found -> (ST.empty,SA.empty)
let add_term k t mp = 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 g_t,g_a = find k mp in add k (ST.add t g_t,g_a) mp
let up_add g t rt lvs = let up_add g t rt lvs =
let g = if mem rt g then g else add rt (ST.empty, SA.empty) g in 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 L.fold_left (fun g x -> add_term x t g) g lvs
let congr_add g lvs = let congr_add g lvs =
match lvs with match lvs with
[] -> ST.empty [] -> ST.empty
| x::ls -> | x::ls ->
L.fold_left L.fold_left
(fun acc y -> ST.inter (fst(find y g)) acc) (fun acc y -> ST.inter (fst(find y g)) acc)
(fst(find x g)) ls (fst(find x g)) ls
let up_close_up g p v = let up_close_up g p v =
let lvs = leaves v in let lvs = leaves v in
let g_p = find p g in let g_p = find p g in
L.fold_left (fun gg l -> add l (union_tpl g_p (find l g)) gg) g lvs L.fold_left (fun gg l -> add l (union_tpl g_p (find l g)) gg) g lvs
let congr_close_up g p touched = let congr_close_up g p touched =
let inter = function let inter = function
[] -> (ST.empty, SA.empty) [] -> (ST.empty, SA.empty)
| rx::l -> | 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 in
L.fold_left L.fold_left
(fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch))) (fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch)))
(find p g) touched (find p g) touched
let print g = () let print g = ()
let mem = G.mem let mem = G.mem

12
smt/use.mli
View file

@ -16,23 +16,23 @@ module T : sig type t = Term.t end
module S : sig type t = Symbols.t end module S : sig type t = Symbols.t end
module ST : sig type elt = T.t type t = Term.Set.t end module ST : sig type elt = T.t type t = Term.Set.t end
module SA : Set.S with type elt = Literal.LT.t * Explanation.t module SA : Set.S with type elt = Literal.LT.t * Explanation.t
type elt = ST.t * SA.t type elt = ST.t * SA.t
module Make : module Make :
functor (X : Sig.X) -> functor (X : Sig.X) ->
sig sig
type t type t
val empty : t val empty : t
val find : X.r -> t -> elt val find : X.r -> t -> elt
val add : X.r -> elt -> t -> t val add : X.r -> elt -> t -> t
val mem : X.r -> t -> bool val mem : X.r -> t -> bool
val print : t -> unit val print : t -> unit
val up_add : t -> ST.elt -> X.r -> X.r list -> t 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 up_close_up :t -> X.r -> X.r -> t
val congr_close_up : t -> X.r -> X.r list -> elt val congr_close_up : t -> X.r -> X.r list -> elt
end end