Source file Mc2_dimacs.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(** {1 Main for dimacs} *)
open Mc2_core
module Dot = Mc2_backend.Dot.Make(Mc2_backend.Dot.Default)
module Plugin_sat = Plugin_sat
type 'a or_error = ('a, string) CCResult.t
include Plugin_sat
let parse reg file : atom list list or_error =
try
let mk_atom = Service.Registry.find_exn reg Plugin_sat.k_atom in
CCIO.with_in file
(fun ic ->
let lexbuf = Lexing.from_channel ic in
Parser.file Lexer.token lexbuf)
|> CCList.map (CCList.map mk_atom)
|> CCResult.return
with e ->
CCResult.of_exn_trace e
let solve s =
try Solver.solve s |> CCResult.return
with e -> CCResult.of_exn_trace e
let check_model cs state : bool =
Log.debug 4 "checking model";
let check_clause c =
Log.debugf 15
(fun k -> k "(@[check.clause@ %a@])" Clause.debug_atoms c);
let ok =
List.exists
(fun a ->
Log.debugf 15
(fun k -> k "(@[check.atom@ %a@])" Term.debug (Atom.term a));
let b = Solver.Sat_state.eval_opt state a in
begin match Atom.eval a, b with
| _, None
| Eval_unknown, _ -> ()
| Eval_into (b', _), Some v_a -> assert (v_a = Value.as_bool_exn b')
end;
b = Some true)
c
in
if not ok then (
Log.debugf 0
(fun k->k "(@[check.fail:@ clause %a@ not satisfied in model@])" Clause.debug_atoms c);
);
ok
in
List.for_all check_clause cs
let process ?gc ?restarts ?dot_proof
?(pp_model=false) ?(check=false) ?time ?memory ?progress ?switch
s pb =
try
let t1 = Sys.time() in
Solver.assume s pb;
let res =
Solver.solve
?switch ?gc ?restarts ?time ?memory ?progress
s ~assumptions:[] in
let t2 = Sys.time () in
begin match res with
| Solver.Sat st ->
if pp_model then (
let pp_t out t =
Fmt.fprintf out "(@[%a %B@])" Term.pp t (Term.Bool.is_true t)
in
Format.printf "(@[<hv1>model@ %a@])@."
(Util.pp_iter pp_t) (Solver.Sat_state.iter_trail st)
);
if check then (
if not (check_model pb st) then (
Error.errorf "invalid model"
)
);
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat state ->
if check then (
let p = Solver.Unsat_state.get_proof state in
Proof.check p;
begin match dot_proof with
| None -> ()
| Some file ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.print fmt p;
Format.pp_print_flush fmt (); flush oc)
end
);
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
end;
CCResult.return()
with e ->
CCResult.of_exn_trace e