Keep only the simplification (0 - x) -> (- x)

OCamlPro · Nov 29, 2023 · b4998bc · b4998bc
1 parent 29720fd
commit b4998bc
Showing 1 changed file with 0 additions and 43 deletions.
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
@@ -454,31 +454,12 @@ let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint
 (** pretty printing *)
 
 module SmtPrinter = struct
-  (** Helper functions used by the postprocessing phase in the printers. *)
-  let zero ty =
-    match ty with
-    | Ty.Tint -> Sy.Int Z.zero
-    | Ty.Treal -> Sy.Real Q.zero
-    | _ -> assert false
-
   let is_zero sy =
     match sy with
     | Sy.Int i when Z.(equal i zero) -> true
     | Sy.Real q when Q.(equal q zero) -> true
     | _ -> false
 
-  let is_one sy =
-    match sy with
-    | Sy.Int i when Z.(equal i one) -> true
-    | Sy.Real q when Q.(equal q one) -> true
-    | _ -> false
-
-  let is_mone sy =
-    match sy with
-    | Sy.Int i when Z.(equal i (neg one)) -> true
-    | Sy.Real q when Q.(equal q (neg one)) -> true
-    | _ -> false
-
   let pp_binder ppf (var, (ty, _)) =
     let var =
       match var with
@@ -586,33 +567,9 @@ module SmtPrinter = struct
 
     | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op
 
-    | Sy.Op Plus, [e1; e2] when is_zero e1.f -> pp ppf e2
-
-    | Sy.Op Plus, [e1; e2] when is_zero e2.f -> pp ppf e1
-
     | Sy.Op Minus, [e1; e2] when is_zero e1.f ->
       Fmt.pf ppf "@[<hv 2>(-@ %a@])" pp e2
 
-    | Sy.Op Minus, [e1; e2] when is_zero e2.f -> pp ppf e1
-
-    | Sy.Op Mult, [e1; e2] when is_one e1.f -> pp ppf e2
-
-    | Sy.Op Mult, [e1; e2] when is_one e2.f -> pp ppf e1
-
-    | Sy.Op Mult, [e1; e2] when is_mone e2.f ->
-      let ty = e1.ty in
-      pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e2] ty)
-
-    | Sy.Op Mult, [e1; e2] when is_mone e1.f ->
-      let ty = e2.ty in
-      pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty)
-
-    | Sy.Op Div, [e1; e2] when is_one e2.f -> pp ppf e1
-
-    | Sy.Op Div, [e1; e2] when is_mone e2.f ->
-      let ty = e1.ty in
-      pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty)
-
     | Sy.Op op, _ :: _ ->
       Fmt.pf ppf "@[<hv 2>(%a@ %a@])"
         Symbols.pp_smtlib_operator op