Simplifying formulas in literals

OCamlPro · Jul 28, 2022 · 8445b2e · 8445b2e
1 parent 27ecc5f
commit 8445b2e
Show file tree

Hide file tree

Showing 4 changed files with 445 additions and 255 deletions.
diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml
@@ -519,16 +519,19 @@ let make_form name f loc ~decl_kind =
       Util.SNo -> form
     | Util.SPreprocess | Util.SAll ->
       let module S = SimpExprPreproc () in
+      (*Format.printf "Simplifying@.";*)
       let smp_form = S.simp_expr form in
-      let () =
+      (* let () =
         (* Emptying the caches modified by the simplifier.
            St : This is necessary for having consistent results. *)
         Shostak.Combine.empty_cache ();
-        S.empty_caches () in
+         S.empty_caches (); () in *)
       if SRE.has_changed smp_form then
+        (*let () = Format.printf "Simplification over: success@." in*)
         let exp = SRE.get_expr smp_form in
         exp
       else begin
+        (*let () = Format.printf "Simplification over: fail@." in*)
         form
       end
   in