Not simplifying substrations of the form (0 - x)

sources/lib/frontend/simple_reasoner_expr.ml

@@ -160,6 +160,9 @@ sig
   (** Represents no explanation. *)
   val empty : t
 
+  (** Tests if the explanation is empty *)
+  val is_empty : t -> bool
+
   (** Merges two explanations. *)
   val union : t -> t -> t
 end
@@ -292,10 +295,10 @@ struct
     (* Wrapper for op. Checks that it has been called.
        If it has never been called, then there have been no
        simplification. *)
-    let op_has_been_called = ref false in
+    let op_has_been_called = ref 0 in
     let op v1 v2 =
-      op_has_been_called := true ;
-      debug "Calling operator.@.";
+      op_has_been_called := !op_has_been_called + 1 ;
+      debug "Calling operator@.";
       op v1 v2
     in
 
@@ -314,19 +317,19 @@ struct
         (None, Expl.empty, [])
         e_list
     in
-    if not (!op_has_been_called)
-    then
-      begin
-        debug "Operator has not been called.@.";
-        identity e_list
-      end
-    else
-      match vals with
-        None -> identity e_list
-      | Some v ->
-        let cst_expr = value_to_expr ty v in
-        debug "Result of simplifyable operations : %a@." E.pretty cst_expr;
-        {v = List.rev exprs @ [value_to_expr ty v]; diff = true; expl}
+      if !op_has_been_called = 0
+      then
+        begin
+          debug "Operator has not been called.@.";
+          identity e_list
+        end
+      else
+        match vals with
+          None -> identity e_list
+        | Some v ->
+          let cst_expr = value_to_expr ty v in
+          debug "Result of simplifyable operations : %a@." E.pretty cst_expr;
+          {v = List.rev exprs @ [value_to_expr ty v]; diff = true; expl}
 
   let oper (op : value -> value -> bool) (l : expr list) : bool * bool * expl =
     (* all_true is a boolean stating that every call of 'op' returned 'true'.
@@ -435,7 +438,18 @@ struct
           (expr list, expl) simp * bool =
           match op with
           | Symbols.Plus  -> arith ty (++) elist, false
-          | Symbols.Minus -> arith ty (--) elist, false
+          | Symbols.Minus -> (
+            match elist with
+                hd :: _ :: []  -> (
+                (* in the case 0 - sthg, we don't want to do anything. *)
+                  match E.get_comp hd with
+                  | Int s
+                  | Real s when Q.equal (Q.of_string (Hstring.view s)) Q.zero ->
+                    identity elist, false
+                  | _ ->  arith ty ( -- ) elist, false
+                )
+              | _ -> arith ty ( -- ) elist, false
+          )
           | Symbols.Mult  -> arith ty ( ** ) elist, false
           | Symbols.Tite -> (
               match elist with

sources/lib/frontend/simple_reasoner_expr.mli

@@ -57,7 +57,14 @@ end
 module type Expl =
 sig
   type t
+
+  (** Represents no explanation. *)
   val empty : t
+
+  (** Tests if the explanation is empty *)
+  val is_empty : t -> bool
+
+  (** Merges two explanations. *)
   val union : t -> t -> t
 end
 

sources/lib/structures/expr.ml

@@ -2556,6 +2556,7 @@ module SimpExprDummy =
     (struct
       type t = unit
       let empty = ()
+      let is_empty _ = true
       let union _ _ = ()
     end)
     (struct