diff --git a/benchsresult/provedovertime.ml b/benchsresult/provedovertime.ml
index 89ff035fa3e3eb914bed417955e8fa82dbf17846..2016ab8b255c9a91065e09f063ac69a69d960432 100644
--- a/benchsresult/provedovertime.ml
+++ b/benchsresult/provedovertime.ml
@@ -56,7 +56,7 @@ let rec print_row_if_needed f next row =
else next
let compute_and_print info =
- let row = Array.create nb_shas 0 in
+ let row = Array.make nb_shas 0 in
let fold (row,next) f m =
let next = print_row_if_needed f next row in
ignore (Mint.fold_left
diff --git a/src/bool.ml b/src/bool.ml
index 68681a47c78c23e934a896cbafafc8cbaff02c54..028c715771c804606fe3e73f147e1fa990055670 100644
--- a/src/bool.ml
+++ b/src/bool.ml
@@ -217,13 +217,12 @@ module DaemonPropaNot = struct
Format.fprintf fmt "%a,%a -> %a" Th.print v Cl.print cl1 Cl.print cl2
end
- type d = Data.t
let immediate = false
let key = Demon.Fast.create "Bool.DaemonPropaNot"
let throttle = 100
let wakeup d =
function
- | Events.Fired.EventDom(_,dom',((v,cl,ncl) as x)) ->
+ | Events.Fired.EventDom(_,dom',((_,cl,ncl) as x)) ->
assert (Dom.equal dom dom');
begin match Delayed.get_dom d dom cl with
| None -> raise Impossible
@@ -371,7 +370,6 @@ end
module RDaemonPropa = Demon.Fast.Register(DaemonPropa)
module DaemonInit = struct
- type d = unit
let key = Demon.Fast.create "Bool.DaemonInit"
module Data = DUnit
@@ -383,7 +381,6 @@ module DaemonInit = struct
begin try
let clsem = ThE.coerce_clsem clsem in
let v = ThE.sem clsem in
- let own = ThE.cl clsem in
match isnot v with
| Some cl ->
Delayed.propagate d cl;
@@ -642,7 +639,7 @@ module ExpProp = struct
| ExpBCP (clsem,cl,kind,b) ->
Format.fprintf fmt "Bcp(%a,%a = %a;%t)"
ThE.print clsem Cl.print (ThE.cl clsem) Cl.print cl
- (fun t -> match kind with
+ (fun _ -> match kind with
| BCPOwnKnown -> Format.fprintf fmt "Own %b" b
| BCPLeavesKnown -> Format.fprintf fmt "Leaves %b" b
| BCP -> ())
@@ -697,14 +694,11 @@ module ExpProp = struct
fold (fun s (cl,_) ->
if kind != BCPLeavesKnown && (Cl.equal cl propa) then s
else get_dom t age cl s) s v
- | ExpUp (clsem,leaf) ->
- let v = ThE.sem clsem in
- let own = ThE.cl clsem in
+ | ExpUp (_,leaf) ->
let s = Cl.M.empty in
let s = get_dom t age leaf s in
s
| ExpDown (clsem,_,_) ->
- let v = ThE.sem clsem in
let own = ThE.cl clsem in
let s = Cl.M.empty in
let s = get_dom t age own s in
@@ -743,12 +737,10 @@ module ExpProp = struct
assert (Cl.equal cl own);
let b = (not v.topnot) in
Cl.M.singleton cl b
- | ExpDown (clsem,cl',sign) ->
- let v = ThE.sem clsem in
+ | ExpDown (_,cl',sign) ->
assert (Cl.equal cl cl');
- let b = (not v.topnot) in
Cl.M.singleton cl sign
- | ExpNot ((v,_,clto),b)->
+ | ExpNot ((_,_,clto),b)->
assert (Cl.equal cl clto);
Cl.M.singleton cl b
in
diff --git a/src/conflict.ml b/src/conflict.ml
index d16d0ce2d081d0dd2a9dbbad4bd0ea0e15fbf53b..cf2fbfbb37f8fa68a3207ba0996b88ccabae2187 100644
--- a/src/conflict.ml
+++ b/src/conflict.ml
@@ -194,17 +194,7 @@ let mk_confact con = return_rescon confact () con
let return_nothing con = return con confact ()
-type exp_iter = unit(*{
- older : tofind list array;
- mutable tage : age;
- lookformerge: domtree Age.H.t;
- lookfordom : unit Cl.H.t Dom.Vector.t;
- solver : Solver.t;
- etrail : Explanation.t;
- dom_can_be_at_current : bool Cl.H.t Dom.Vector.t;
-}
- *)
-let print_dom_can_be_at_current fmt v =
+let _print_dom_can_be_at_current fmt v =
Dom.Vector.print Pp.newline Pp.space
{Dom.Vector.printk = Dom.print}
(Pp.print_iter2 Cl.H.iter Pp.semi Pp.comma Cl.print DBool.print) fmt v
@@ -236,8 +226,6 @@ module type Con' = sig
val print: t Pp.printer
- val key: t con
-
val same_sem:
con_iter -> age -> 'a sem -> 'a ->
pexp -> Cl.t -> Cl.t -> t rescon
@@ -279,8 +267,6 @@ module type Exp' = sig
val print: t Pp.printer
- val key: t exp
-
(* val iterexp: exp_iter -> age -> t -> unit *)
val analyse : con_iter -> age ->
@@ -340,8 +326,6 @@ module type Cho' = sig
val analyse:
con_iter -> 'a con -> Key.t -> Data.t -> 'a rescon
- val key: (Key.t,Data.t) cho
-
end
@@ -357,13 +341,6 @@ let print_modif fmt = function
let () = Explanation.print_modif_ref := print_modif
-let cholearnt : (chogen list * int, Solver.Delayed.t -> dec -> unit) cho =
- Cho.create_key "Conflict.cho"
-let new_finalized_list =
- let c = ref (-1) in
- fun () -> incr c; let c = !c in fun l -> (l,c)
-
-
(** Give for explanation that something is the last before the limit.
So we generalize on that. *)
type explimit =
@@ -394,7 +371,7 @@ module ComputeConflict = struct
type t = con_iter
let before_first_dec t age = Explanation.before_first_dec t.ctrail age
- let after_last_dec t age = Age.compare t.ctrail.last_dec age <= 0
+ let _after_last_dec t age = Age.compare t.ctrail.last_dec age <= 0
type get_equal_aux =
| GEANoPath
@@ -529,7 +506,7 @@ module ComputeConflict = struct
Age.equal agemerge agemerge' ->
(** merged from not representative *)
go_down age acc hcl n1
- | Explanation.DomMerge(agemerge,_,n2), _ ->
+ | Explanation.DomMerge(_,_,n2), _ ->
go_down age acc hcl n2
| Explanation.DomPreMerge(_,cl,n1,_), _ ->
let _,hcl = get_repr_at_hist t age [] cl in
@@ -555,7 +532,7 @@ module ComputeConflict = struct
let rec go_down age hcl hdom =
match hdom,hcl with
| Explanation.DomNeverSet, _ -> raise DomNeverSet
- | Explanation.DomSet(moddom,n), _
+ | Explanation.DomSet(moddom,_), _
when Explanation.Age.compare
moddom.Explanation.modage t.ctrail.last_dec < 0 ->
let pexp =
@@ -563,7 +540,7 @@ module ComputeConflict = struct
~age:moddom.Explanation.modage
explimit (LDom (dom,moddom)) in
{moddom with modpexp = pexp}
- | Explanation.DomSet(moddom,n), _
+ | Explanation.DomSet(moddom,_), _
when Explanation.Age.compare moddom.Explanation.modage age <= 0 ->
moddom
| Explanation.DomMerge(agemerge,_,n2), _
@@ -574,7 +551,7 @@ module ComputeConflict = struct
Age.equal agemerge agemerge' ->
(** merged from not representative *)
go_down age hcl n1
- | Explanation.DomMerge(agemerge,_,n2), _ ->
+ | Explanation.DomMerge(_,_,n2), _ ->
go_down age hcl n2
| Explanation.DomPreMerge(_,cl,n1,_), _ ->
let _,hcl = get_repr_at_hist t age [] cl in
@@ -1296,9 +1273,7 @@ module ExpCho = struct
let key = expcho
- let iterexp _ _ _ = ()
-
- let analyse (type a) t _ (con: a con) (Pcho(dec,cho,k,v)) =
+ let analyse (type a) t _ (con: a con) (Pcho(_,cho,k,v)) =
let f (type k) (type d) t con (cho : (k,d) cho) k v =
let module C = (val get_cho cho) in
C.analyse t con k v in
@@ -1338,7 +1313,7 @@ module ConFact = struct
let finalize _ = assert false (** catched before *)
- let same_sem t age _ _ pexp2 _ _ =
+ let same_sem t _ _ _ pexp2 _ _ =
let get_con () t = function
| GRequested () -> ()
| GOther (con,c) -> ComputeConflict.unknown_con t con c
@@ -1347,7 +1322,7 @@ module ConFact = struct
GRequested ()
let propacl _ _ _ _ = raise Impossible
- let propadom _ _ dom cl v =
+ let _propadom _ _ dom cl v =
Debug.dprintf6 debug
"[Conflict] @[Error: Ask ConFact for the limit for %a with %a of %a @]@\n"
Cl.print cl Dom.print dom (Solver.print_dom_opt dom) v;
@@ -1364,7 +1339,6 @@ module ExpFact = struct
let key = expfact
- let iterexp _t _age () = ()
let analyse (type a) _t _age (con: a con) () =
mk_confact con
@@ -1384,7 +1358,6 @@ module ExpLimit = struct
let key = explimit
- let iterexp _t _age _limit = (** nothing to do its a leaf *) ()
let analyse (type a) t age (con: a con) limit =
match limit with
| LCl (cl,rcl) ->
@@ -1450,13 +1423,11 @@ module ExpLearnt = struct
let key = explearnt
- let iterexp _ _ _ = ()
-
let analyse (type a) t _age (con: a con) (ExpLearnt(tags)) =
t.cdeps <- Deps.add_tags t.cdeps tags;
return con ConFact.key ()
- let expdom t age _ _ con _ =
+ let expdom _ _ _ _ con _ =
return con ConFact.key ()
end
diff --git a/src/inputlang/dimacs_cnf/dimacs.mll b/src/inputlang/dimacs_cnf/dimacs.mll
index 12d648a3d19800dd627cbd486efa8f746edd81c0..4bbfc7499df30170dbd403b5f6738069e6c02b69 100644
--- a/src/inputlang/dimacs_cnf/dimacs.mll
+++ b/src/inputlang/dimacs_cnf/dimacs.mll
@@ -25,7 +25,7 @@
type vars = Types.Cl.t array
let init_vars env nb_var : vars =
- let a = Array.create nb_var (Bool._true env) in
+ let a = Array.make nb_var (Bool._true env) in
for i = 0 to nb_var - 1 do
a.(i) <- Variable.fresh env Bool.ty (Printf.sprintf "x%i" (i+1))
done;
diff --git a/src/solver.ml b/src/solver.ml
index 78d08954bfc454b2fde07a68cac4423ac3ed305d..65f1b2a2d874322c8ac864c470d2b50f7ca3d16c 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -91,8 +91,8 @@ module Events = struct
let translate_dom =
{translate = fun (cl,dom) data -> EventDom(cl,dom,data)}
- let translate_sem =
- {translate = fun (cl,sem,s) data -> EventSem(cl,sem,s,data)}
+ (* let translate_sem = *)
+ (* {translate = fun (cl,sem,s) data -> EventSem(cl,sem,s,data)} *)
let translate_propa =
{translate = fun cl data -> EventPropa(cl,data)}
let translate_propacl =
@@ -377,7 +377,7 @@ let get_table_dom : t -> 'a dom -> (module DomTable with type D.t = 'a)
: DomTable' with type D.t = a and type delayed = delayed_t)
: DomTable with type D.t = a)
-let get_table_sem : t -> 'a sem -> semtable = fun (type a) t k ->
+let get_table_sem : t -> 'a sem -> semtable = fun t k ->
assert (if sem_uninitialized k then raise UnregisteredKey else true);
VSemTable.inc_size k t.sem;
if VSemTable.is_uninitialized t.sem k
diff --git a/src/solver.mli b/src/solver.mli
index 063a9b940f201bd585b5185e8903940e425186e6..4b136dc3ad1799f92dddaf50699d05262eaa492f 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -207,7 +207,7 @@ val new_delayed :
sched_daemon:(daemon_key -> unit) ->
sched_decision:(chogen -> unit) ->
t -> Delayed.t
-(** The argument shouldn't be used anymore before
+(** The solver shouldn't be used anymore before
calling flush. (flushd doesn't count)
*)
diff --git a/src/util/IArray.ml b/src/util/IArray.ml
index 1dc170a928906cd25810254b5fd02201978006b4..e65521dcd96a6c0f366db5c11571622e87c680ba 100644
--- a/src/util/IArray.ml
+++ b/src/util/IArray.ml
@@ -26,7 +26,7 @@ let of_list = Array.of_list
let of_array = Array.copy
let of_iter l (iter : ('a -> unit) -> unit) =
if l = 0 then [||] else
- let res = Array.create l (Obj.magic 0 : 'a) in
+ let res = Array.make l (Obj.magic 0 : 'a) in
let r = ref 0 in
iter (fun v -> res.(!r) <- v; incr r);
assert (!r == l);
diff --git a/src/util/intmap.ml b/src/util/intmap.ml
index 9d878fbd278e6aa942e05b39b21bad9032e61078..1a6a30a249f71a9462ebcf9b0ea5b68127dcce46 100644
--- a/src/util/intmap.ml
+++ b/src/util/intmap.ml
@@ -73,7 +73,7 @@ let included_prefix p q =
let pp_mask m fmt p =
begin
- let bits = Array.create 63 false in
+ let bits = Array.make 63 false in
let last = ref 0 in
for i = 0 to 62 do
let u = 1 lsl i in
@@ -89,7 +89,7 @@ let pp_mask m fmt p =
let pp_bits fmt k =
begin
- let bits = Array.create 63 false in
+ let bits = Array.make 63 false in
let last = ref 0 in
for i = 0 to 62 do
if (1 lsl i) land k <> 0 then
diff --git a/src/util/simple_vector.ml b/src/util/simple_vector.ml
index 219c290c0a193745c1bd29805bb9590aae4e9515..c06fae3f22d66bcec3d6e26b530ba1e933b98868 100644
--- a/src/util/simple_vector.ml
+++ b/src/util/simple_vector.ml
@@ -27,8 +27,7 @@ let dumb : 'a. 'a =
let dumb_addr = ref 0 in
Obj.magic dumb_addr
-let create size = { data = Array.create size dumb;
- size = size }
+let create size = { data = Array.make size dumb; size = size }
let size t = t.size
diff --git a/src/variable.mli b/src/variable.mli
index ac794884f513c3eb16e92a1912341a3ebc81f44e..42aa16b39cd89d52c0d0978e1a7d499b8e9bd35b 100644
--- a/src/variable.mli
+++ b/src/variable.mli
@@ -26,7 +26,7 @@ type make_dec = Cl.t -> Explanation.chogen
val cst: Solver.d -> Ty.t -> string -> Cl.t
(** same string, same class *)
-val fresh: Solver.Delayed.t -> Ty.t -> string -> Cl.t
+val fresh: Solver.d -> Ty.t -> string -> Cl.t
(** always fresh *)
val add_dec: dec:make_dec -> Solver.Delayed.t -> Cl.t -> unit