Formula simplification at preprocessing

non-regression/main_script.sh

@@ -54,6 +54,7 @@ do
         tput hpa 25
         total=`expr $total + 1`
         echo -n "$total / $big_total"
+	echo "$pr $ae $opt 1>  $main_script_out 2> $main_script_err"
         timeout 2 $pr $ae $opt 1> $main_script_out 2> $main_script_err
         if grep -q -w Valid $main_script_out ; then
 	    score=`expr $score + 1`

src/bin/gui/annoted_ast.ml

@@ -739,15 +739,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"
@@ -759,9 +762,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"
@@ -814,7 +821,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
     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,57 @@ open Commands
 module E = Expr
 module Sy = Symbols
 module SE = E.Set
+module SRE = Simple_reasoner_expr
+
+(** Simplifyer not using the theory *)
+module DummySimp:
+  (Simple_reasoner_expr.S with type expr = Expr.t
+                           and type env = Theory.Main_Default.t
+                           and type expl = Explanation.t) =
+  Expr.SimpExpr
+    (Explanation)
+    (struct
+      type expr = Expr.t
+      type expl = Explanation.t
+      type env = Theory.Main_Default.t
+      let empty = Theory.Main_Default.empty
+      let bool_query _ _ = None
+      let q_query _ _ = None
+    end
+    )
+
+(** Simplifyer using the theory *)
+module ThSimp : Simple_reasoner_expr.S with type expr = Expr.t
+                                        and type env = Theory.Main_Default.t
+                                        and type expl = Explanation.t =
+  Expr.SimpExpr
+    (Explanation)
+    (struct
+      type expr = Expr.t
+      type expl = Explanation.t
+      type env = Theory.Main_Default.t
+      let empty = Theory.Main_Default.empty
+      let bool_query ex env =
+        try
+          match Theory.Main_Default.query ex env with
+          | Some (expl,[]) -> Some (true, expl)
+          | Some _ | None -> None
+        with _ ->
+          Format.eprintf "Query failed on %a@." Expr.print ex; None
+      let q_query _ex _env = None
+    end
+    )
+
+
+let choose_preproc () :
+  (module Simple_reasoner_expr.S with type expr = Expr.t
+                                  and type env = Theory.Main_Default.t
+                                  and type expl = Explanation.t)  =
+  if not (Options.get_simplify_th ())
+  then (module DummySimp)
+  else (module ThSimp)
+
+module SimpExprPreproc () = (val (choose_preproc ()))
 
 [@@ocaml.ppwarning "TODO: Change Symbols.Float to store FP numeral \
                     constants (eg, <24, -149> for single) instead of \
@@ -283,8 +334,15 @@ let rec make_term up_qv quant_basename t =
         ~decl_kind:E.Daxiom (* not correct, but not a problem *)
         ~toplevel:false
   in
-  mk_term t
-
+  let term = mk_term t in
+  match Options.get_simplify () with
+  | Util.SNo -> term
+  | Util.SPreprocess | Util.SAll ->
+    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
@@ -485,7 +543,14 @@ 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 | Util.SAll ->
+      let module S = SimpExprPreproc () in
+      let smp_form = S.simp_expr form 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
@@ -511,7 +576,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;_];_}; _}; _}
@@ -554,12 +619,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