Fully disable heavy assertions (#1089)

* Fully disable heavy assertions

In some part of the codebase, we use heavy assertions as follow:
```
assert (not @@ Options.get_enable_assertions () || heavy_assertion)
```
This trick has two advantages:
- As the logical `or` in OCaml has short-circuit evaluation, if the option
  `enable_assertions` is not `true`, we don't evaluate the heavy
  assertion.
- If we use the compiler option `no-asserts`, we don't even test the
  option `Options.get_enable_assertions`.

This PR adds a new function in `Options` to reproduce this good design
everywhere in the codebase.

Notice that I put the function `heavy_assert` in `Options` but it would
be better to put it in `Util`. Alas, we got a cycle dependency :/

* Use suspensions instead of lazy values

* Use Options.heavy_assert in `Enum_rel`

src/lib/reasoners/arith.ml

@@ -710,8 +710,8 @@ module Shostak
     let sbs = List.filter (fun (p,_) -> SX.mem p lvs || is_non_lin p) sbs in
       (*
         This assert is not TRUE because of AC and distributivity of '*'
-        assert (not (get_enable_assertions ()) ||
-        X.equal (apply_subst a sbs) (apply_subst b sbs));
+        Options.heavy_assert
+          (fun () -> X.equal (apply_subst a sbs) (apply_subst b sbs));
       *)
     List.iter
       (fun (p, _) ->

src/lib/reasoners/enum_rel.ml

@@ -156,7 +156,7 @@ module Domains = struct
     let od = get r t in
     (* For sake of completeness, the domain [d] has to be a subset of the old
        domain of [r]. *)
-    assert (not (Options.get_enable_assertions ()) || Domain.subset d od);
+    Options.heavy_assert (fun () -> Domain.subset d od);
     if Domain.equal od d then
       t
     else

src/lib/reasoners/fun_sat.ml

@@ -487,7 +487,7 @@ module Make (Th : Theory.S) = struct
     end
 
   let cdcl_same_decisions env =
-    if Options.(get_tableaux_cdcl () && get_enable_assertions ()) then begin
+    if Options.get_tableaux_cdcl () then begin
       let cdcl_decs = CDCL.get_decisions !(env.cdcl) in
       let ok = ref true in
       let decs =
@@ -1048,7 +1048,7 @@ module Make (Th : Theory.S) = struct
     if list == [] then
       begin
         print_decisions_in_the_sats "exit assume rec" env;
-        assert (cdcl_same_decisions env);
+        Options.heavy_assert (fun () -> cdcl_same_decisions env);
         env
       end
     else
@@ -1435,7 +1435,7 @@ module Make (Th : Theory.S) = struct
       if Options.get_profiling() then
         Profiling.decision new_level a.E.origin_name;
       (*fprintf fmt "@.BEFORE DECIDING %a@." E.print f;*)
-      assert (cdcl_same_decisions env);
+      Options.heavy_assert (fun () -> cdcl_same_decisions env);
       let env_a =
         {env with
          delta=l;
@@ -1478,11 +1478,11 @@ module Make (Th : Theory.S) = struct
             (*No backtrack, reset cache*)
             ignore (update_instances_cache (Some []));
         end;
-        assert (cdcl_same_decisions env);
+        Options.heavy_assert (fun () -> cdcl_same_decisions env);
         if Options.get_tableaux_cdcl () then
           cdcl_learn_clause false env dep' (E.neg f);
         print_decisions_in_the_sats "make_one_decision:backtrack" env;
-        assert (cdcl_same_decisions env);
+        Options.heavy_assert (fun () -> cdcl_same_decisions env);
         if not (Options.get_tableaux_cdcl ()) then
           unsat_rec (assume env [b, Ex.union d dep']) (not_a,dep') false
         else
@@ -1501,7 +1501,7 @@ module Make (Th : Theory.S) = struct
         Options.tool_req 2 "TR-Sat-Backjumping";
         dep
     with Propagate (ff, ex) ->
-      assert (cdcl_same_decisions env);
+      Options.heavy_assert (fun () -> cdcl_same_decisions env);
       back_tracking (assume env [ff, ex])
 
   let max_term_depth_in_sat env =

src/lib/reasoners/intervalCalculus.ml

@@ -1351,8 +1351,7 @@ let fm (module Oracle : S with type p = P.t) uf are_eq rclass_of env eqs =
   Options.tool_req 4 "TR-Arith-Fm";
   let ineqs =
     MPL.fold (fun _ v acc ->
-        if Options.get_enable_assertions() then
-          assert (is_normalized_poly uf v.ple0);
+        Options.heavy_assert (fun () -> is_normalized_poly uf v.ple0);
         (better_bound_from_intervals env v) :: acc
       ) env.inequations []
   in

src/lib/reasoners/matching.ml

@@ -494,8 +494,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
     let open Matching_types in
     let pats = pat_info.trigger in
     let pats_list = pats.E.content in
-    assert (not (Options.get_enable_assertions ()) ||
-            Lists.is_sorted pat_weight pats_list);
+    Options.heavy_assert (fun () -> Lists.is_sorted pat_weight pats_list);
     Debug.matching pats;
     if List.length pats_list > Options.get_max_multi_triggers_size () then
       pat_info, []

src/lib/reasoners/satml.ml

@@ -712,14 +712,14 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   let debug_enqueue_level a lvl reason =
     match reason with
-    | None -> ()
+    | None -> true
     | Some (c : Atom.clause) ->
       let maxi = ref min_int in
       Vec.iter (fun (atom : Atom.atom) ->
           if not (Atom.eq_atom a atom) then
             maxi := max !maxi atom.var.level
         ) c.atoms;
-      assert (!maxi = lvl)
+      !maxi = lvl
 
   let max_level_in_clause (c : Atom.clause) =
     let max_lvl = ref 0 in
@@ -750,7 +750,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     if is_semantic a then
       env.nchoices <- env.nchoices + 1;
     a.var.index <- Vec.size env.trail;
-    if Options.get_enable_assertions() then  debug_enqueue_level a lvl reason
+    Options.heavy_assert (fun () -> debug_enqueue_level a lvl reason)
 
   let progress_estimate env =
     let prg = ref 0. in
@@ -1002,9 +1002,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     (*let a = SFF.cardinal env.relevants in*)
     env.lazy_cnf <-
       Queue.fold (relevancy_propagation env) env.lazy_cnf env.tatoms_queue;
-    if Options.get_enable_assertions() then (*debug *)
-      Matoms.iter (fun a _ -> assert (not a.is_true)) env.lazy_cnf
-
+    Options.heavy_assert (fun () ->
+        Matoms.for_all (fun a _ -> not a.is_true) env.lazy_cnf
+      )
 
   let _expensive_theory_propagate () = None
   (* try *)

src/lib/reasoners/shostak.ml

@@ -145,13 +145,14 @@ struct
           "abstract selectors of %a" CX.print a
 
     let assert_have_mem_types tya tyb =
-      assert (
-        not (Options.get_enable_assertions()) ||
-        if not (Ty.compare tya tyb = 0) then (
-          print_err "@[<v 0>@ Tya = %a  and @ Tyb = %a@]"
-            Ty.print tya Ty.print tyb;
-          false)
-        else true)
+      Options.heavy_assert (fun () ->
+          if not (Ty.compare tya tyb = 0) then begin
+            print_err "@[<v 0>@ Tya = %a  and @ Tyb = %a@]"
+              Ty.print tya Ty.print tyb;
+            false
+          end
+          else true
+        )
 
   end
   (*BISECT-IGNORE-END*)
@@ -526,8 +527,8 @@ struct
     Debug.print_sbt "Triangular and cleaned" sbs;
     (*
       This assert is not TRUE because of AC and distributivity of '*'
-      assert (not (Options.get_enable_assertions()) ||
-      equal (apply_subst a sbs) (apply_subst b sbs));
+      Options.heavy_assert
+        (fun () -> equal (apply_subst a sbs) (apply_subst b sbs));
     *)
     sbs
 

src/lib/reasoners/uf.ml

@@ -285,34 +285,32 @@ module Debug = struct
         ~module_name:"Uf" ~function_name:"are_distinct"
         "are_distinct %a %a" E.print t1 E.print t2
 
-
   let check_inv_repr_normalized =
     let trace orig =
       print_err
         "[uf.%s] invariant broken when calling check_inv_repr_normalized"
         orig
     in
     fun orig repr ->
-      MapX.iter
+      MapX.for_all
         (fun _ (rr, _) ->
-           List.iter
-             (fun x ->
-                try
-                  if not (X.equal x (fst (MapX.find x repr))) then
-                    let () = trace orig in
-                    assert false
-                with Not_found ->
-                  (* all leaves that are in normal form should be in repr ?
-                     not AC leaves, which can be created dynamically,
-                     not for other, that can be introduced by make and solve*)
-                  ()
-             )(X.leaves rr)
-        )repr
+           try
+             let _ : X.r =
+               List.find
+                 (fun x -> not (X.equal x (fst (MapX.find x repr))))
+                 (X.leaves rr)
+             in
+             let () = trace orig in
+             false
+           with Not_found ->
+             (* all leaves that are in normal form should be in repr ?
+                not AC leaves, which can be created dynamically,
+                not for other, that can be introduced by make and solve*)
+             true
+        ) repr
 
   let check_invariants orig env =
-    if Options.get_enable_assertions() then begin
-      check_inv_repr_normalized orig env.repr;
-    end
+    Options.heavy_assert (fun () -> check_inv_repr_normalized orig env.repr)
 end
 (*BISECT-IGNORE-END*)
 

src/lib/structures/expr.ml

@@ -1289,12 +1289,11 @@ let rec apply_subst_aux (s_t, s_ty) t =
         in
         (* TODO: implement case where variables capture happens *)
         assert (no_capture_issue s_t binders);
-        assert (
-          (* invariant: s_t does not contain other free vars than
-             those of t, and binders cannot be free vars of t *)
-          not (Options.get_enable_assertions ()) ||
-          Var.Map.for_all (fun sy _ -> not (Var.Map.mem sy s_t)) binders
-        );
+        (* invariant: s_t does not contain other free vars than
+           those of t, and binders cannot be free vars of t *)
+        Options.heavy_assert (fun () ->
+            Var.Map.for_all (fun sy _ -> not (Var.Map.mem sy s_t)) binders
+          );
         let main = apply_subst_aux s main in
         let trs = List.map (apply_subst_trigger s) trs in
         let binders =

src/lib/util/options.ml

@@ -658,3 +658,6 @@ let pp_comment fmt msg =
   match get_output_format () with
   | Smtlib2 -> Format.fprintf fmt "; %s" msg;
   | Native | Why3 | Unknown _ -> Format.fprintf fmt "%s" msg
+
+let[@inline always] heavy_assert p =
+  assert (not @@ get_enable_assertions () || p ())

src/lib/util/options.mli

@@ -1162,3 +1162,9 @@ end
 
 (** Print message as comment in the corresponding output format *)
 val pp_comment: Format.formatter -> string -> unit
+
+val heavy_assert : (unit -> bool) -> unit
+(** [heavy_assert p] checks if the suspended boolean [p] evaluates to [true].
+    No-op if the [Options.get_enable_assertions ()] is [false].
+
+    @raises Assert_failure if [p] evaluates to [false]. *)