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

Small printing upgrades

Browse source
This commit is contained in:
Guillaume Bury 2016-07-13 18:14:23 +02:00
parent 2ff1279f26
commit 1acecc0815
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
solver/solver_types.ml
View file

@ -263,7 +263,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
(* Complete debug printing *)
let sign a = if a == a.var.pa then "" else "-"
let sign a = if a == a.var.pa then "+" else "-"
let level a =
match a.var.v_level, a.var.reason with
@ -292,14 +292,14 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
(v.lid+1) E.Term.print v.term pp_assign v.assigned
let pp_atom out a =
Format.fprintf out "%s%d%s[atom:%a]"
Format.fprintf out "%s%d%s[atom:%a]@ "
(sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
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} =
Format.fprintf out "@[<hov 2>%s%s{@[<hov 2>%a@]}@ cpremise={@[<hov2>%a@]}@]"
Format.fprintf out "%s%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
end