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

Slightly better formatting for clause printing

Browse source
This commit is contained in:
Guillaume Bury 2016-07-13 17:07:03 +02:00
parent c159a60d9b
commit ef49d5eaaa
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
solver/solver_types.ml
View file

@ -278,25 +278,25 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let pp_premise out = function let pp_premise out = function
| Hyp _ -> Format.fprintf out "hyp" | Hyp _ -> Format.fprintf out "hyp"
| Lemma _ -> Format.fprintf out "th_lemma" | Lemma _ -> Format.fprintf out "th_lemma"
| History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v
let pp_assign out = function let pp_assign out = function
| None -> () | None -> ()
| Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t | Some t -> Format.fprintf out " ->@ %a" E.Term.print t
let pp_lit out v = let pp_lit out v =
Format.fprintf out "%d [lit:%a]%a" Format.fprintf out "%d [lit:%a%a]"
(v.lid+1) E.Term.print v.term pp_assign v.assigned (v.lid+1) E.Term.print v.term pp_assign v.assigned
let pp_atom out a = let pp_atom out a =
Format.fprintf out "%s%d%s[lit:%a]" Format.fprintf out "%s%d%s[atom:%a]"
(sign a) (a.var.vid+1) (value a) E.Formula.print a.lit (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
let pp_atoms_vec out vec = let pp_atoms_vec out vec =
Vec.print ~sep:"; " pp_atom out vec Vec.print ~sep:"@ " pp_atom out vec
let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} = let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
Format.fprintf out "%s%s{ %a} cpremise={{%a}}" Format.fprintf out "@[<hov 2>%s%s{@[<hov 2>%a@]}@ cpremise={@[<hov2>%a@]}@]"
name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
end end