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
open Base
open Stdio
type run_solver = dimacs_in:string -> result_out:string -> unit -> unit Or_error.t
let run ?(exit_codes = [ 0 ]) command =
match Unix.system command with
| WEXITED e when List.mem exit_codes e ~equal:Int.equal -> Ok ()
| WEXITED exit_code ->
Or_error.error_s [%message "SAT solver returned non-zero exit code" (exit_code : int)]
| WSIGNALED _ | WSTOPPED _ ->
Or_error.error_s [%message "SAT solver was signaled or stopped"]
;;
let swallow_stderr = "2>/dev/null"
let minisat ~dimacs_in ~result_out () =
run
~exit_codes:[ 10; 20 ]
(String.concat
~sep:" "
[ Config.minisat; "-verb=0"; dimacs_in; result_out; ">/dev/null"; swallow_stderr ])
;;
let picosat ~dimacs_in ~result_out () =
run
~exit_codes:[ 10; 20 ]
(String.concat
~sep:" "
[ Config.picosat; dimacs_in; ">" ^ result_out; swallow_stderr ])
;;
let z3 ?seed ~parallel () ~dimacs_in ~result_out () =
let seed =
match seed with
| Some seed -> seed
| None -> if Exported_for_specific_uses.am_testing then 192452 else 0
in
run
(String.concat
~sep:" "
[ Config.z3
; "-dimacs"
; (if parallel then "parallel.enable=true" else "")
; "sat.random_seed=" ^ Int.to_string seed
; dimacs_in
; ">" ^ result_out
; swallow_stderr
])
;;
module Filename = Stdlib.Filename
type 'a result = 'a list Sat.t Or_error.t [@@deriving sexp_of]
let solve_with_model
(type a)
?(solver = z3 ~parallel:false ())
?(print_model = false)
(module Model : Cnf.Model with type input = a)
cnf
: a list Sat.t Or_error.t
=
let dimacs_file = Filename.temp_file "cnf" "dimacs" in
let result_file = Filename.temp_file "cnf" "result" in
let dimacs_out = Out_channel.create dimacs_file in
Dimacs.write_problem cnf dimacs_out;
Out_channel.close dimacs_out;
let solver_result = solver ~dimacs_in:dimacs_file ~result_out:result_file () in
match solver_result with
| Ok () ->
let file = In_channel.create result_file in
let dimacs_result = Dimacs.read_result file in
In_channel.close file;
Unix.unlink dimacs_file;
Unix.unlink result_file;
let model = Or_error.map dimacs_result ~f:(Model.get cnf) in
if print_model then Model.print Stdio.stdout model;
model
| Error e ->
Unix.unlink dimacs_file;
Error e
;;
let solve ?solver ?print_model cnf =
solve_with_model ?solver ?print_model (module Cnf.Model_with_vectors) cnf
;;