Source file Mc2_smtlib.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
(** {1 Process Statements} *)
open Mc2_core
module PA = Smtlib_utils.V_2_6.Ast
module Typecheck = Typecheck
module E = CCResult
type 'a or_error = ('a, string) CCResult.t
module Make(ARG : sig
val solver : Solver.t
end)
= struct
let solver = ARG.solver
let parse = Smtlib_utils.V_2_6.parse_file
let parse_stdin () = Smtlib_utils.V_2_6.parse_chan ~filename:"<stdin>" stdin
module TC = Typecheck.Make(ARG)
module Dot = Mc2_backend.Dot.Make(Mc2_backend.Dot.Default)
(** {2 Processing Statements} *)
let typecheck stmts =
try
let l = CCList.flat_map TC.conv_statement stmts in
Ok l
with e -> E.of_exn_trace e
let hyps = ref []
let check_model 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 t -> Solver.Sat_state.eval_opt state t = 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
Solver.Sat_state.check_model state &&
List.for_all check_clause !hyps
let solve
?gc ?restarts ?dot_proof
?(pp_model=false) ?(check=false) ?time ?memory ?progress ?switch
~assumptions s : unit =
let t1 = Sys.time() in
let res =
Solver.solve ?gc ?restarts ?time ?memory ?progress ?switch
s ~assumptions in
let t2 = Sys.time () in
begin match res with
| Solver.Sat state ->
if pp_model then (
let pp_t out = function
| A_bool (t,b) -> Fmt.fprintf out "(@[%a@ %B@])" Term.pp t b
| A_semantic (t,v) -> Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Value.pp v
in
Format.printf "(@[<hv1>model@ %a@])@."
(Util.pp_list pp_t) (Solver.Sat_state.model state)
);
if check then (
if not (check_model state) then (
Error.error "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
let process_stmt
?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
?time ?memory ?progress ?switch
(stmt:Statement.t) : unit or_error =
Log.debugf 5
(fun k->k "(@[<2>process statement@ %a@])" Statement.pp stmt);
begin match stmt with
| Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return ()
| Stmt_set_logic s ->
Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
E.return ()
| Stmt_set_option l ->
Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l);
E.return ()
| Stmt_set_info _ -> E.return ()
| Stmt_exit ->
Log.debug 1 "exit";
raise Exit
| Stmt_check_sat ->
solve ?gc ?restarts ?dot_proof ?check ?pp_model ?time
?memory ?progress ?switch
solver ~assumptions:[];
E.return()
| Stmt_ty_decl _ -> E.return ()
| Stmt_decl _ -> E.return ()
| Stmt_assert_clauses clauses ->
if pp_cnf then (
Format.printf "(@[<hv1>assert@ %a@])@."
(Util.pp_list Clause.pp_atoms) clauses;
);
hyps := clauses @ !hyps;
Solver.assume solver clauses;
E.return()
| Stmt_define _ ->
E.return ()
end
end