mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
fix more warnings
This commit is contained in:
parent
e7e8873295
commit
73b39fe075
4 changed files with 1 additions and 14 deletions
|
|
@ -146,8 +146,6 @@ module Make (A: CC_ARG)
|
||||||
let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits
|
let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits
|
||||||
end
|
end
|
||||||
|
|
||||||
module N_tbl = CCHashtbl.Make(N)
|
|
||||||
|
|
||||||
(* non-recursive, inlinable function for [find] *)
|
(* non-recursive, inlinable function for [find] *)
|
||||||
let[@inline] find_ (n:node) : repr =
|
let[@inline] find_ (n:node) : repr =
|
||||||
let n2 = n.n_root in
|
let n2 = n.n_root in
|
||||||
|
|
|
||||||
|
|
@ -128,7 +128,6 @@ module Make() : S = struct
|
||||||
val pp : t Fmt.printer
|
val pp : t Fmt.printer
|
||||||
val of_list : store -> atom list -> t
|
val of_list : store -> atom list -> t
|
||||||
val of_iter : store -> atom Iter.t -> t
|
val of_iter : store -> atom Iter.t -> t
|
||||||
module Set : CCSet.S with type elt = t
|
|
||||||
module Tbl : CCHashtbl.S with type key = t
|
module Tbl : CCHashtbl.S with type key = t
|
||||||
end = struct
|
end = struct
|
||||||
type t = {
|
type t = {
|
||||||
|
|
@ -171,7 +170,6 @@ module Make() : S = struct
|
||||||
let[@inline] equal a b = a.id = b.id
|
let[@inline] equal a b = a.id = b.id
|
||||||
let[@inline] compare a b = compare a.id b.id
|
let[@inline] compare a b = compare a.id b.id
|
||||||
end
|
end
|
||||||
module Set = CCSet.Make(As_key)
|
|
||||||
module Tbl = CCHashtbl.Make(As_key)
|
module Tbl = CCHashtbl.Make(As_key)
|
||||||
end
|
end
|
||||||
type clause = Clause.t
|
type clause = Clause.t
|
||||||
|
|
|
||||||
|
|
@ -28,10 +28,8 @@ module Make(Plugin : PLUGIN)
|
||||||
(* a boolean variable (positive int) *)
|
(* a boolean variable (positive int) *)
|
||||||
module Var0 : sig
|
module Var0 : sig
|
||||||
include Int_id.S
|
include Int_id.S
|
||||||
module Set : Set.S with type elt = t
|
|
||||||
end = struct
|
end = struct
|
||||||
include Int_id.Make()
|
include Int_id.Make()
|
||||||
module Set = Util.Int_set
|
|
||||||
end
|
end
|
||||||
type var = Var0.t
|
type var = Var0.t
|
||||||
|
|
||||||
|
|
@ -46,7 +44,6 @@ module Make(Plugin : PLUGIN)
|
||||||
val abs : t -> t
|
val abs : t -> t
|
||||||
val pa : var -> t
|
val pa : var -> t
|
||||||
val na : var -> t
|
val na : var -> t
|
||||||
module Set : CCSet.S with type elt = t
|
|
||||||
end = struct
|
end = struct
|
||||||
include Int_id.Make()
|
include Int_id.Make()
|
||||||
let[@inline] neg i = (i lxor 1)
|
let[@inline] neg i = (i lxor 1)
|
||||||
|
|
@ -57,7 +54,6 @@ module Make(Plugin : PLUGIN)
|
||||||
let[@inline] abs a = a land (lnot 1)
|
let[@inline] abs a = a land (lnot 1)
|
||||||
let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
|
let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
|
||||||
let[@inline] na v = (((v:var:>int) lsl 1) lor 1)
|
let[@inline] na v = (((v:var:>int) lsl 1) lor 1)
|
||||||
module Set = Util.Int_set
|
|
||||||
end
|
end
|
||||||
type atom = Atom0.t
|
type atom = Atom0.t
|
||||||
|
|
||||||
|
|
@ -213,7 +209,7 @@ module Make(Plugin : PLUGIN)
|
||||||
let[@inline] pp_sign a = if sign a then "+" else "-"
|
let[@inline] pp_sign a = if sign a then "+" else "-"
|
||||||
|
|
||||||
(* print level+reason of assignment *)
|
(* print level+reason of assignment *)
|
||||||
let debug_reason self out = function
|
let debug_reason _self out = function
|
||||||
| n, _ when n < 0 -> Format.fprintf out "%%"
|
| n, _ when n < 0 -> Format.fprintf out "%%"
|
||||||
| n, None -> Format.fprintf out "%d" n
|
| n, None -> Format.fprintf out "%d" n
|
||||||
| n, Some Decision -> Format.fprintf out "@@%d" n
|
| n, Some Decision -> Format.fprintf out "@@%d" n
|
||||||
|
|
@ -1890,7 +1886,6 @@ module Make(Plugin : PLUGIN)
|
||||||
let module M = struct
|
let module M = struct
|
||||||
type nonrec lit = lit
|
type nonrec lit = lit
|
||||||
type clause = Clause.t
|
type clause = Clause.t
|
||||||
type proof = Proof.t
|
|
||||||
let unsat_conflict = unsat_conflict
|
let unsat_conflict = unsat_conflict
|
||||||
let unsat_assumptions = unsat_assumptions
|
let unsat_assumptions = unsat_assumptions
|
||||||
end in
|
end in
|
||||||
|
|
|
||||||
|
|
@ -34,9 +34,6 @@ module type DATA_TY = sig
|
||||||
val view : t -> (cstor, t) data_ty_view
|
val view : t -> (cstor, t) data_ty_view
|
||||||
|
|
||||||
val cstor_args : cstor -> t Iter.t
|
val cstor_args : cstor -> t Iter.t
|
||||||
|
|
||||||
(** A table indexed by types. *)
|
|
||||||
module Tbl : Hashtbl.S with type key = t
|
|
||||||
end
|
end
|
||||||
|
|
||||||
(** {2 Cardinality of types} *)
|
(** {2 Cardinality of types} *)
|
||||||
|
|
@ -200,7 +197,6 @@ module Make(A : ARG) : S with module A = A = struct
|
||||||
module T = A.S.T.Term
|
module T = A.S.T.Term
|
||||||
module N = SI.CC.N
|
module N = SI.CC.N
|
||||||
module Ty = A.S.T.Ty
|
module Ty = A.S.T.Ty
|
||||||
module Fun = A.S.T.Fun
|
|
||||||
module Expl = SI.CC.Expl
|
module Expl = SI.CC.Expl
|
||||||
|
|
||||||
module Card = Compute_card(A)
|
module Card = Compute_card(A)
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue