Write transformation of program into logical formula.

1 files changed, 6 insertions, 0 deletions

diff --git a/main.ml b/main.ml
index 61755e3..08bfe91 100644
--- a/main.ml
+++ b/main.ml
@@ -63,6 +63,12 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
+      let prog_f = Formula.eliminate_not (Transform.f_of_prog prog "test") in
+      Formula_printer.print_expr Format.std_formatter prog_f;
+      Format.printf "@.";
+      let prog_f_cl = Formula.conslist_of_f prog_f in
+      Formula_printer.print_conslist Format.std_formatter prog_f_cl;
+
       if !vtest then do_test_interpret prog true
       else if !test then do_test_interpret prog false;