simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 12:15:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

style

Browse source
This commit is contained in:
Simon Cruanes 2020-10-12 02:06:16 -04:00
parent 534fc45783
commit 51be2f52e8
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -85,7 +85,7 @@ module Make(A : ARG)
let[@inline] raise_conflict a lits pr = let[@inline] raise_conflict a lits pr =
a.Msat.acts_raise_conflict lits pr a.Msat.acts_raise_conflict lits pr
let[@inline] propagate a lit ~reason pr = let[@inline] propagate a lit ~reason pr =
let reason = Msat.Consequence (fun () -> reason(), pr) in let reason = Msat.Consequence (fun () -> reason(), pr) in
a.Msat.acts_propagate lit reason a.Msat.acts_propagate lit reason
end end
end end
@ -106,7 +106,7 @@ module Make(A : ARG)
type lit = Lit.t type lit = Lit.t
type term_state = Term.state type term_state = Term.state
type th_states = type th_states =
| Ths_nil | Ths_nil
| Ths_cons : { | Ths_cons : {
st: 'a; st: 'a;
@ -236,7 +236,7 @@ module Make(A : ARG)
match h self ~mk_lit ~add_clause t with match h self ~mk_lit ~add_clause t with
| None -> aux_rec t hooks_tl | None -> aux_rec t hooks_tl
| Some u -> | Some u ->
Log.debugf 30 Log.debugf 30
(fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])" (fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])"
Term.pp t Term.pp u); Term.pp t Term.pp u);
aux u aux u