WIP: Simplify preprocess

src/bin/common/parse_command.ml

@@ -171,7 +171,8 @@ let mk_dbg_opt_spl2 debug_explanations debug_fm debug_fpa debug_gc
   `Ok()
 
 let mk_dbg_opt_spl3 debug_split debug_sum debug_triggers debug_types
-    debug_typing debug_uf debug_unsat_core debug_use debug_warnings rule
+    debug_typing debug_uf debug_unsat_core debug_use debug_warnings
+    debug_simplify rule
   =
   let rule = value_of_rule rule in
   set_debug_split debug_split;
@@ -183,6 +184,7 @@ let mk_dbg_opt_spl3 debug_split debug_sum debug_triggers debug_types
   set_debug_unsat_core debug_unsat_core;
   set_debug_use debug_use;
   set_debug_warnings debug_warnings;
+  set_debug_simplify debug_simplify;
   set_rule rule;
   `Ok()
 
@@ -436,7 +438,7 @@ let halt_opt version_info where =
   with Failure f -> `Error (false, f)
      | Error (b, m) -> `Error (b, m)
 
-let mk_opts file () () () () () () halt_opt (gc) () () () () () () () ()
+let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () ()
   =
 
   if halt_opt then `Ok false
@@ -466,6 +468,12 @@ let mk_fmt_opt std_fmt err_fmt
   set_err_fmt (value_of_fmt err_fmt);
   `Ok()
 
+let mk_simplify simp_opt use_th =
+  set_simplify
+    (if simp_opt then SPreprocess else SNo);
+  set_simplify_th use_th;
+  `Ok ()
+
 (* Custom sections *)
 
 let s_debug = "DEBUG OPTIONS"
@@ -482,6 +490,7 @@ let s_sat = "SAT OPTIONS"
 let s_term = "TERM OPTIONS"
 let s_theory = "THEORY OPTIONS"
 let s_fmt = "FORMATTER OPTIONS"
+let s_simp = "SIMPLIFIER"
 
 (* Parsers *)
 
@@ -629,6 +638,10 @@ let parse_dbg_opt_spl3 =
     let doc = "Set the debugging flag of warnings." in
     Arg.(value & flag & info ["dwarnings"] ~docs ~doc) in
 
+  let debug_simplify =
+    let doc = "Set the debugging flag of the simplifier." in
+    Arg.(value & flag & info ["dsimplify"] ~docs ~doc) in
+
   let rule =
     let doc =
       "$(docv) = parsing|typing|sat|cc|arith, output rule used on stderr." in
@@ -646,6 +659,7 @@ let parse_dbg_opt_spl3 =
              debug_unsat_core $
              debug_use $
              debug_warnings $
+             debug_simplify $
              rule
             ))
 
@@ -1242,6 +1256,19 @@ let parse_fmt_opt =
              std_formatter $ err_formatter
             ))
 
+let simplifier =
+  let docs = s_simp in
+
+  let simplify =
+    let doc = "Activates the formula preprocessing" in
+    Arg.(value & flag & info ["simplify"] ~docs ~doc)
+  in
+  let simplify_th =
+    let doc = "Activates the use of theories during formula preprocessing" in
+    Arg.(value & flag & info ["simplify-th"] ~docs ~doc)
+  in
+  Term.(ret (const mk_simplify $ simplify $ simplify_th))
+
 let main =
 
   let file =
@@ -1278,6 +1305,7 @@ let main =
       `S s_halt;
       `S s_fmt;
       `S s_debug;
+      `S s_simp;
       `P "These options are used to output debug info for the concerned \
           part of the solver.\
           They are $(b,not) used to check internal consistency.";
@@ -1309,7 +1337,7 @@ let main =
                parse_execution_opt $ parse_halt_opt $ parse_internal_opt $
                parse_limit_opt $ parse_output_opt $ parse_profiling_opt $
                parse_quantifiers_opt $ parse_sat_opt $ parse_term_opt $
-               parse_theory_opt $ parse_fmt_opt
+               parse_theory_opt $ parse_fmt_opt $ simplifier
               ))
   in
   let info =

src/bin/gui/annoted_ast.ml

@@ -717,15 +717,18 @@ and print_tt_desc fmt = function
   | TTnamed (lbl, t) -> fprintf fmt "%s:%a" (Hstring.view lbl) print_tterm t
   | TTinInterval(e, lb, ub) ->
     fprintf fmt "%a in %a, %a"
-      print_term e
+      (print_term ~annot:no_print) e
       Symbols.print_bound lb
       Symbols.print_bound ub
 
-  | TTmapsTo(x,e) -> fprintf fmt "%a |-> %a" Var.print x print_term e
+  | TTmapsTo(x,e) ->
+    fprintf fmt "%a |-> %a" Var.print x (print_term ~annot:no_print) e
 
   | TTite(f,t1, t2) ->
     fprintf fmt "(if %a then %a else %a)"
-      print_tform f print_term t1 print_term t2
+      print_tform f
+      (print_term ~annot:no_print) t1
+      (print_term ~annot:no_print) t2
 
   | TTproject (_, _, _) | TTmatch (_, _) ->
     Gui_config.not_supported "Algebraic datatypes"
@@ -737,9 +740,13 @@ and print_term_binders fmt l =
   match l with
   | [] -> assert false
   | (sy, t) :: l ->
-    fprintf fmt "%a = %a" Symbols.print_clean sy print_term t;
+    fprintf fmt "%a = %a" Symbols.print_clean sy (print_term ~annot:no_print) t;
     List.iter (fun (sy, t) ->
-        fprintf fmt ",\n%a = %a" Symbols.print_clean sy print_term t) l
+        fprintf
+          fmt
+          ",\n%a = %a"
+          Symbols.print_clean sy
+          (print_term ~annot:no_print) t) l
 
 and print_tatom fmt a = match a.Typed.c with
   | TAtrue -> fprintf fmt "true"
@@ -792,7 +799,7 @@ and print_tform2 fmt f = match f.Typed.c with
 and print_mixed_binders =
   let aux fmt e =
     match e with
-    | TletTerm t -> fprintf fmt "%a" print_term t
+    | TletTerm t -> fprintf fmt "%a" (print_term ~annot:no_print) t
     | TletForm f -> fprintf fmt "%a" print_tform2 f
   in fun fmt binders ->
     match binders with

src/lib/dune

@@ -29,6 +29,7 @@
   ; modules that make up the lib
   (modules
     ; frontend
+    Simple_reasoner_expr Simplifiers
     Cnf Input Frontend Parsed_interface Typechecker
     ; reasoners
     Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel

src/lib/frontend/cnf.ml

@@ -34,6 +34,17 @@ open Commands
 module E = Expr
 module Sy = Symbols
 module SE = E.Set
+module SRE = Simple_reasoner_expr
+module Smp = Simplifiers
+
+let choose_preproc () :
+  (module Simple_reasoner_expr.S) =
+  if not (Options.get_simplify_th ()) then
+    (module Smp.DummySimp)
+  else
+    (module Smp.IntervalsSimp)
+
+module SimpExprPreproc () = (val (choose_preproc ()))
 
 [@@ocaml.ppwarning "TODO: Change Symbols.Float to store FP numeral \
                     constants (eg, <24, -149> for single) instead of \
@@ -282,9 +293,16 @@ let rec make_term up_qv quant_basename t =
         up_qv quant_basename e Loc.dummy
         ~decl_kind:E.Daxiom (* not correct, but not a problem *)
         ~toplevel:false
-  in
-  mk_term t
-
+  in (*mk_term t*)
+  let term = mk_term t in
+  match Options.get_simplify () with
+  | Util.SNo -> term
+  | Util.SPreprocess ->
+    let module S = SimpExprPreproc () in
+    let smp_term = S.simp_expr  term in
+    if SRE.has_changed smp_term
+    then SRE.get_expr smp_term
+    else term
 
 and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) =
   let content, guard = match e with
@@ -496,14 +514,31 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
 (* wrapper of function make_form *)
 let make_form name f loc ~decl_kind =
   let ff =
-    make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true
+    let form = make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true in
+    match Options.get_simplify () with
+      Util.SNo -> form
+    | Util.SPreprocess ->
+      let module S = SimpExprPreproc () in
+      (*Format.printf "Simplifying@.";*)
+      let smp_form = S.simp_expr form in
+      (* let () =
+        (* Emptying the caches modified by the simplifier.
+           St : This is necessary for having consistent results. *)
+        Shostak.Combine.empty_cache ();
+        S.empty_caches (); ()
+      in *)
+      if SRE.has_changed smp_form
+      then SRE.get_expr smp_form
+      else form
   in
   assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty));
   let ff = E.purify_form ff in
-  if Ty.Svty.is_empty (E.free_type_vars ff) then ff
-  else
+  if Ty.Svty.is_empty (E.free_type_vars ff) then begin
+    ff
+  end else begin
     let id = E.id ff in
     E.mk_forall name loc Symbols.Map.empty [] ff id ~toplevel:true ~decl_kind
+  end
 
 let mk_assume acc f name loc =
   let ff = make_form name f loc ~decl_kind:E.Daxiom in
@@ -522,7 +557,7 @@ let mk_assume acc f name loc =
 *)
 let defining_term f =
   if get_verbose () then
-    Format.eprintf "defining term of %a@." Typed.print_formula f;
+    Format.eprintf "defining term of %a@." (Typed.print_formula ?annot:None) f;
   match f.c with
   | TFforall {qf_form={c=TFop(OPiff,[{c=TFatom {c=TApred(d,_);_};_};_]); _}; _}
   | TFforall {qf_form={c=TFatom {c=TAeq[d;_];_}; _}; _}
@@ -565,12 +600,16 @@ let mk_theory acc l th_name extends _loc =
          | TAxiom (loc, name, ax_kd, f) -> loc, name, f, ax_kd
          | _ -> assert false
        in
-       let ax_form = make_form ax_name f loc ~decl_kind:E.Dtheory in
+       let ax_form =
+         make_form ax_name f loc ~decl_kind:E.Dtheory
+       in
        let th_elt = {Expr.th_name; axiom_kind; extends; ax_form; ax_name} in
        {st_decl=ThAssume th_elt ; st_loc=loc} :: acc
-    )acc l
+    )
+    acc
+    l
 
-let make acc d =
+let make acc (d : (int Typed.tdecl, 'a) Typed.annoted) =
   match d.c with
   | TPush (loc,n) -> {st_decl=Push n; st_loc=loc} :: acc
   | TPop (loc,n) -> {st_decl=Pop n; st_loc=loc} :: acc