package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file sat_solver.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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Bridge to [MSat] prover} *)

open Logtk

module SI = Msat.Solver_intf

let section = Util.Section.make ~parent:Const.section "msat"
let prof_call_msat = ZProf.make "msat.call"
let stat_num_clauses = Util.mk_stat "msat.num_clauses"
let stat_num_calls = Util.mk_stat "msat.num_calls"

type proof_step = Sat_solver_intf.proof_step
type proof = Sat_solver_intf.proof

type result = Sat_solver_intf.result =
  | Sat
  | Unsat of proof

exception WrongState of string

let wrong_state_ msg = raise (WrongState msg)
let errorf msg = Util.errorf ~where:"sat_solver" msg

let sat_dump_file_ = ref ""
let sat_log_file = ref ""
let sat_compact_ = ref true
let sat_pp_model_ = ref false

module type S = Sat_solver_intf.S

(* Instantiate solver *)
module Solver = Msat.Make_pure_sat(struct
    module Formula = struct
      include BBox.Lit
      let norm (l:t) : t * _ =
        let l', b = norm l in
        l', if b then SI.Negated else SI.Same_sign
    end
    type proof = Sat_solver_intf.proof_step
  end)

module Make() 
  (*   : Sat_solver_intf.S *)
= struct
  module Lit = BBox.Lit
  let solver = ref (Solver.create ~size:`Big ())

  type clause = Lit.t list

  (* queue of clauses waiting for being pushed into the solver *)
  let queue_ = Queue.create()

  (* flag to indicate whether it's time to re-check the model *)
  let must_check = ref false

  (* channel on which to print boolean clauses *)
  let dump_to : out_channel option ref = ref None

  (* print list of clauses on [dump_to], if it's defined *)
  let dump_l l = match !dump_to with
    | None -> ()
    | Some out ->
      let pp_lit out l = output_string out (string_of_int (Lit.to_int l)) in
      let pp_c out c =
        List.iter (fun l -> output_char out ' '; pp_lit out l) c;
        output_string out " 0\n";
      in
      List.iter (pp_c out) l;
      flush out

  module ClauseTbl = CCHashtbl.Make(struct
      type t = Lit.t list
      let equal = CCList.equal Lit.equal
      let hash = (Hash.list Lit.hash)
    end)

  let clause_tbl_ : unit ClauseTbl.t = ClauseTbl.create 32
  let lit_tbl_ : unit Lit.Tbl.t = Lit.Tbl.create 32

  (* add clause, if not added already *)
  let add_clause_ ~proof c =
    let open Msat in
    if not (ClauseTbl.mem clause_tbl_ c) then (
      Util.incr_stat stat_num_clauses;
      (* add new clause -> check again *)
      must_check := true;
      ClauseTbl.add clause_tbl_ c ();
      List.iter (fun lit -> Lit.Tbl.replace lit_tbl_ (Lit.abs lit) ()) c;
      Queue.push ([c], proof) queue_
    )

  let add_clause ~proof (c:clause) =
    let c = CCList.sort_uniq ~cmp:Lit.compare c in (* no duplicates *)
    dump_l [c];
    add_clause_ ~proof c

  let add_clauses ~proof l =
    dump_l l;
    List.iter (add_clause_ ~proof) l

  let add_clause_seq ~proof (seq:clause Iter.t) =
    add_clauses ~proof (Iter.to_rev_list seq)

  let result_ = ref Sat

  let res_is_unsat_ () = match !result_ with Sat -> false | Unsat _ -> true

  (* invariant:
     when result_ = Sat, only eval/eval_level are defined
     when result_ = Unsat, only unsat_core_ is defined
  *)

  let eval_fail_ _ = assert (res_is_unsat_ ()); wrong_state_ "eval"

  let eval_ = ref eval_fail_
  let eval_level_ = ref eval_fail_
  let proof_ : proof option ref = ref None
  let proved_lits_ : Lit.Set.t lazy_t ref = ref (lazy Lit.Set.empty)

  let pp_ = ref Lit.pp

  let pp_clause out c =
    Format.fprintf out "[@[<hv>%a@]]" (Util.pp_list ~sep:" ⊔ " !pp_) c

  let pp_form_simpl out l = Util.pp_list ~sep:"" pp_clause out l

  let pp_form fmt f : unit =
    Format.fprintf fmt "[@[<hv>%a@]]" pp_form_simpl f

  let last_result () = !result_
  let valuation l = !eval_ l
  let valuation_level l = !eval_level_ l
  let all_proved () = Lazy.force !proved_lits_

  let get_proof () = match !proof_ with
    | None -> assert false
    | Some p -> p

  let get_proof_opt () = !proof_

  let () =
    if !sat_log_file <> "" then (
      let oc = open_out !sat_log_file in
      let fmt = Format.formatter_of_out_channel oc in
      Msat.Log.set_debug_out fmt;
      Msat.Log.set_debug 9999;
      at_exit (fun () -> Format.pp_print_flush fmt (); close_out_noerr oc);
    )

  exception UndecidedLit = Solver.UndecidedLit

  type sat_clause = Lit.t list

  let bool_clause_of_sat (c:Solver.Clause.t) : sat_clause =
    Solver.Clause.atoms_l c |> List.map Solver.Atom.formula

  (* (clause * proof * proof) -> 'a *)
  module ResTbl = CCHashtbl.Make(struct
      type t = sat_clause * Proof.t list
      let equal (c,l1)(c',l2) =
        CCList.equal Lit.equal c c' &&
        CCList.equal Proof.S.equal l1 l2
      let hash (c,l) =
        CCHash.combine2
          (CCHash.int @@ List.length c)
          (CCHash.list Proof.S.hash l)
    end)

  let tbl_res = ResTbl.create 16

  let proof_of_leaf c step : proof =
    let c = bool_clause_of_sat c in
    Proof.S.mk step (Bool_clause.mk_proof_res c)

  (* convert a SAT proof into a tree of ProofStep *)
  let conv_proof_atomic_ p : proof =
    let rec aux p =
      let module P = Solver.Proof in
      match P.expand p with
      | {P. step = P.Lemma _; _ } -> errorf "SAT proof involves a lemma"
      | {P. step = P.Assumption; _ } -> errorf "SAT proof involves an assumption"
      | {P. step = P.Duplicate (c',_); _} -> aux c'
      | {P. conclusion=c; step = P.Hyper_res {P.hr_init; hr_steps} } ->
        let c = bool_clause_of_sat c in
        (* atomic resolution step *)
        let q1 = aux hr_init in
        let q2 = List.map (fun (_,p) -> aux p) hr_steps in
        begin match ResTbl.get tbl_res (c, q1::q2) with
          | Some s -> s
          | None ->
            let parents = Proof.Parent.from q1 :: List.map Proof.Parent.from q2 in
            let step =
              Proof.Step.inference parents
                ~rule:(Proof.Rule.mk "sat_resolution") in
            let s = Proof.S.mk step (Bool_clause.mk_proof_res c) in
            ResTbl.add tbl_res (c,q1::q2) s;
            s
        end
      | {P. conclusion=c; step = P.Hypothesis step; _ } ->
        proof_of_leaf c step
    in
    Solver.Proof.check p;
    aux p

  let conv_proof_compact_ p : proof =
    let module P = Solver.Proof in
    let leaves =
      P.fold
        (fun acc pnode -> match pnode with
           | {P. step = P.Lemma _; _ } -> errorf "SAT proof involves a lemma"
           | {P. step = P.Assumption; _ } -> errorf "SAT proof involves an assumption"
           | {P. step = (P.Hyper_res _ | P.Duplicate _); _ } ->
             acc (* ignore, intermediate node *)
           | {P. conclusion=c; step = P.Hypothesis step; _ } ->
             Proof.Parent.from (proof_of_leaf c step) :: acc)
        [] p
    in
    let {P.conclusion=c;_} = P.expand p in
    let c = bool_clause_of_sat c in
    let step =
      Proof.Step.inference leaves
        ~rule:(Proof.Rule.mk "sat_resolution*")  in
    Proof.S.mk step (Bool_clause.mk_proof_res c)

  let conv_proof_ p =
    if !sat_compact_
    then conv_proof_compact_ p
    else conv_proof_atomic_ p

  let get_proof_of_lit lit =
    let module P = Solver.Proof in
    let b, l = valuation_level lit in
    if not b || l <> 0 then invalid_arg "get_proof_of_lit";
    let a = Solver.make_atom !solver lit in
    match P.prove_atom a with
    | Some p -> conv_proof_ p
    | None -> assert false

  let proved_at_0 lit =
    let a = Solver.make_atom !solver lit in
    if Solver.true_at_level0 !solver a then Some true
    else if Solver.true_at_level0 !solver (Solver.Atom.neg a) then Some false
    else None

  let get_proved_lits (): Lit.Set.t =
    Lit.Tbl.to_iter lit_tbl_
    |> Iter.filter_map
      (fun (lit,_) -> match proved_at_0 lit with
         | Some true -> Some lit
         | Some false -> Some (Lit.neg lit)
         | None -> None)
    |> Lit.Set.of_iter

  let pp_model_ (): unit = match last_result() with
    | Sat ->
      let m =
        Lit.Tbl.keys lit_tbl_
        |> Iter.map (fun l -> l, valuation l)
        |> Iter.to_rev_list
      in
      let pp_pair out (l,b) = Format.fprintf out "(@[%B %a@])" b BBox.pp l in
      Format.printf "(@[<hv2>bool_model@ %a@])@." (Util.pp_list ~sep:" " pp_pair) m
    | Unsat _ -> ()

  (* call [S.solve()] in any case, and enforce invariant about eval/unsat_core *)
  let check_unconditional_ () =
    (* reset functions, so they will fail if called in the wrong state *)
    proof_ := None;
    eval_ := eval_fail_;
    eval_level_ := eval_fail_;
    Util.incr_stat stat_num_calls;
    (* add pending clauses *)
    while not (Queue.is_empty queue_) do
      let c, proof = Queue.pop queue_ in
      Util.debugf ~section 4 "@[<hv2>assume@ @[%a@]@ proof: %a@]"
        (fun k->k pp_form c Proof.Step.pp proof);
      Solver.assume !solver c proof
    done;
    (* solve *)
    Util.debug ~section 4 "solve...";
    let res = Solver.solve !solver in
    Util.debug ~section 4 "solve done.";
    begin match res with
      | Solver.Sat s ->
        eval_ := s.SI.eval;
        eval_level_ := s.SI.eval_level;
        proved_lits_ := lazy (get_proved_lits ());
        result_ := Sat;
      | Solver.Unsat us ->
        let p = us.SI.get_proof ()  |> conv_proof_ in
        result_ := Unsat p;
        proof_ := Some p;
    end;
    !result_

  let check_ full =
    if full || !must_check
    then (
      assert (full || not (Queue.is_empty queue_));
      Util.debug ~section 5 "check_real";
      must_check := false;
      check_unconditional_ ()
    )
    else !result_

  (* initialize eval/eval_level to enforce invariant *)
  let () =
    let res = check_unconditional_ () in
    assert (res = Sat)

  let check ~full () = ZProf.with_prof prof_call_msat check_ full

  let set_printer pp = pp_ := pp

  let setup () =
    if !sat_dump_file_ <> "" then (
      Util.debugf ~section 1 "dump SAT clauses to `%s`" (fun k->k !sat_dump_file_);
      try
        let oc = open_out !sat_dump_file_ in
        dump_to := Some oc;
        at_exit (fun () -> close_out_noerr oc);
      with e ->
        Util.warnf "@[<2>could not open `%s`:@ %s@]"
          !sat_dump_file_ (Printexc.to_string e);
    );
    if !sat_pp_model_ then at_exit pp_model_;
    ()
  
  let clear ?(size=`Big) () =
    Queue.clear queue_;
    must_check := true;
    ClauseTbl.clear clause_tbl_;
    Lit.Tbl.clear lit_tbl_;
    solver := Solver.create ~size ()
end

let set_compact b = sat_compact_ := b

let () =
  Params.add_opts
    [ "--sat-dump", Arg.Set_string sat_dump_file_, " output SAT problem(s) into <file>"
    ; "--sat-log", Arg.Set_string sat_log_file, " output SAT logs into <file>"
    ; "--compact-sat", Arg.Set sat_compact_, " compact SAT proofs"
    ; "--no-compact-sat", Arg.Clear sat_compact_, " do not compact SAT proofs"
    ; "--pp-sat-model", Arg.Set sat_pp_model_, " print SAT model on exit"
    ]