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

Now using unicode characters

Browse source
This commit is contained in:
Guillaume Bury 2014-11-06 21:24:11 +01:00
parent fd4a618c2a
commit 19ebfeb866
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sat/res.ml
View file

@ -48,12 +48,12 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
(* Printing functions *) (* Printing functions *)
let print_atom fmt a = let print_atom fmt a =
Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "¬ ") St.(a.var.vid + 1)
let rec print_cl fmt = function let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]" | [] -> Format.fprintf fmt "[]"
| [a] -> print_atom fmt a | [a] -> print_atom fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" print_atom a print_cl r
(* Compute resolution of 2 clauses *) (* Compute resolution of 2 clauses *)
let resolve l = let resolve l =