mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
fix warnings
This commit is contained in:
parent
7722319b0a
commit
5e12b26fc0
2 changed files with 4 additions and 4 deletions
|
|
@ -42,12 +42,12 @@ module Make(St : Solver_types.S)(Dummy: sig end) = struct
|
||||||
Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec
|
Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec
|
||||||
|
|
||||||
let export_icnf_aux r name map_filter fmt vec =
|
let export_icnf_aux r name map_filter fmt vec =
|
||||||
let aux fmt v =
|
let aux fmt _ =
|
||||||
for i = !r to (Vec.size vec) - 1 do
|
for i = !r to (Vec.size vec) - 1 do
|
||||||
let x = Vec.get vec i in
|
let x = Vec.get vec i in
|
||||||
match map_filter x with
|
match map_filter x with
|
||||||
| None -> ()
|
| None -> ()
|
||||||
| Some y -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i)
|
| Some _ -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i)
|
||||||
done;
|
done;
|
||||||
r := Vec.size vec
|
r := Vec.size vec
|
||||||
in
|
in
|
||||||
|
|
@ -108,7 +108,7 @@ module Make(St : Solver_types.S)(Dummy: sig end) = struct
|
||||||
let lemmas = history in
|
let lemmas = history in
|
||||||
(* Local assertions *)
|
(* Local assertions *)
|
||||||
let l = List.map (function
|
let l = List.map (function
|
||||||
| {St.cpremise = St.Local; atoms = [| a |] } -> a
|
| {St.cpremise = St.Local; atoms = [| a |];_ } -> a
|
||||||
| _ -> assert false) (Vec.to_list local) in
|
| _ -> assert false) (Vec.to_list local) in
|
||||||
let local = St.make_clause "local (tmp)" l St.Local in
|
let local = St.make_clause "local (tmp)" l St.Local in
|
||||||
(* Number of atoms and clauses *)
|
(* Number of atoms and clauses *)
|
||||||
|
|
|
||||||
|
|
@ -115,7 +115,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
|
||||||
let rule, color, l = A.assumption_info S.(n.conclusion) in
|
let rule, color, l = A.assumption_info S.(n.conclusion) in
|
||||||
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
|
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
|
||||||
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
|
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
|
||||||
| S.Lemma lemma ->
|
| S.Lemma _ ->
|
||||||
let rule, color, l = A.lemma_info S.(n.conclusion) in
|
let rule, color, l = A.lemma_info S.(n.conclusion) in
|
||||||
let color = match color with None -> "YELLOW" | Some c -> c in
|
let color = match color with None -> "YELLOW" | Some c -> c in
|
||||||
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
|
print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue