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

Fix for tseitin cnf conversion

Browse source
This commit is contained in:
Guillaume Bury 2014-11-10 19:47:42 +01:00
parent e74dddc4b0
commit 625c0ad309
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
sat/tseitin.ml
View file

@ -52,8 +52,15 @@ module Make (F : Formula_intf.S) = struct
let f_true = make_atom atomic_true
let f_false = make_atom atomic_false
let rec flatten comb acc = function
| [] -> acc
| (Comb (c, l)) :: r when c = comb ->
flatten comb (List.rev_append l acc) r
| a :: r ->
flatten comb (a :: acc) r
let make_not f = make Not [f]
let make_and l = make And l
let make_and l = make And (flatten And [] l)
let make_imply f1 f2 = make Imp [f1; f2]
let make_equiv f1 f2 = make And [ make_imply f1 f2; make_imply f2 f1]
let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ];
@ -62,7 +69,7 @@ module Make (F : Formula_intf.S) = struct
let make_or = function
| [] -> raise Empty_Or
| [a] -> a
| l -> Comb (Or, l)
| l -> Comb (Or, flatten Or [] l)
(* simplify formula *)
let rec sform = function