Create a custom ADT for Th_util.answer

An option type is not self-documenting code.

src/lib/reasoners/adt_rel.ml

@@ -664,24 +664,25 @@ let case_split env uf ~for_model =
 let optimizing_objective _env _uf _o = None
 
 let query _env uf (ra, _, ex, _) =
-  if Options.get_disable_adts () then None
+  if Options.get_disable_adts () then Th_util.Unknown
   else
     let domains = Uf.GlobalDomains.find (module Domains) (Uf.domains uf) in
     try
       match ra with
       | Xliteral.Builtin(true, Sy.IsConstr c, [r]) ->
         let rr, _ = Uf.find_r uf r in
         ignore (assume_is_constr ~ex rr c domains);
-        None
+        Unknown
 
       | Xliteral.Builtin(false, Sy.IsConstr c, [r]) ->
         let rr, _ = Uf.find_r uf r in
         ignore (assume_not_is_constr ~ex rr c domains);
-        None
+        Unknown
 
       | _ ->
-        None
+        Unknown
     with
-    | Domain.Inconsistent ex -> Some (ex, Uf.cl_extract uf)
+    | Domain.Inconsistent ex ->
+      Entailed { ex; classes = Uf.cl_extract uf }
 
 (* ################################################################ *)

src/lib/reasoners/arrays_rel.ml

@@ -237,23 +237,23 @@ module type UF = module type of Uf
    (respectively [q]) is already true, we do not add the consequence. *)
 let update_env (module Uf : UF) uf dep env acc gi si p p_ded n n_ded =
   match Uf.are_equal uf ~added_terms:true gi si, Uf.are_distinct uf gi si with
-  | Some (idep, _) , None ->
+  | Entailed { ex = idep; _ }, Unknown ->
     let conseq = LRmap.add n n_ded dep env.conseq in
     {env with conseq = conseq},
     Conseq.add (p_ded, Ex.union dep idep) acc
 
-  | None, Some (idep, _) ->
+  | Unknown, Entailed { ex = idep; _ } ->
     let conseq = LRmap.add p p_ded dep env.conseq in
     {env with conseq = conseq},
     Conseq.add (n_ded, Ex.union dep idep) acc
 
-  | None, None ->
+  | Unknown, Unknown ->
     let sp = LRset.add p env.split in
     let conseq = LRmap.add p p_ded dep env.conseq in
     let conseq = LRmap.add n n_ded dep conseq in
     { env with split = sp; conseq = conseq }, acc
 
-  | Some _,  Some _ ->
+  | Entailed _,  Entailed _ ->
     (* This case cannot occur because we cannot have `gi = si` and
        `gi <> si` at the same time. *)
     assert false
@@ -290,8 +290,8 @@ let get_of_set (module Uf : UF) uf gtype (env, acc) =
            let n_ded = E.mk_eq ~iff:false get get_stab in
            let dep =
              match Uf.are_equal uf ~added_terms:true gtab set with
-             | Some (dep, _) -> dep
-             | None -> assert false
+             | Entailed { ex; _ } -> ex
+             | Unknown -> assert false
            in
            let env =
              {env with new_terms =
@@ -362,8 +362,8 @@ let get_and_set (module Uf : UF) uf gtype (env, acc) =
            let n_ded = E.mk_eq ~iff:false gt_of_st get_stab in
            let dep =
              match Uf.are_equal uf ~added_terms:true gtab stab with
-             | Some (dep, _) -> dep
-             | None -> assert false
+             | Entailed { ex; _ } -> ex
+             | Unknown -> assert false
            in
            let env =
              {env with
@@ -471,7 +471,7 @@ let assume env uf la =
   in
   env, Uf.domains uf, { Sig_rel.assume = l; remove = [] }
 
-let query _ _ _ = None
+let query _ _ _ = Th_util.Unknown
 let add env uf _ _ = env, Uf.domains uf, []
 
 let new_terms env = env.new_terms

src/lib/reasoners/bitv_rel.ml

@@ -2210,7 +2210,7 @@ let assume env uf la =
   Uf.GlobalDomains.add (module Interval_domains) int_domain ds,
   result
 
-let query _ _ _ = None
+let query _ _ _ = Th_util.Unknown
 
 let case_split env uf ~for_model =
   if not for_model && Stdlib.(env.size_splits >= Options.get_max_split ()) then

src/lib/reasoners/ccx.ml

@@ -264,9 +264,10 @@ module Main : S = struct
 
   let explain_equality env ex t1 t2 =
     if E.equal t1 t2 then ex
-    else match Uf.are_equal env.uf t1 t2 ~added_terms:true with
-      | Some (dep, _) -> Ex.union ex dep
-      | None -> raise Exit
+    else
+      match Uf.are_equal env.uf t1 t2 ~added_terms:true with
+      | Entailed { ex = ex'; _ } -> Ex.union ex ex'
+      | Unknown -> raise Exit
 
   let equal_only_by_congruence env (facts: r Sig_rel.facts) t1 t2 =
     if not (E.equal t1 t2) then
@@ -353,11 +354,11 @@ module Main : S = struct
                let ty_y = Expr.type_info y in
                if Ty.equal ty_x ty_y then
                  begin match Uf.are_distinct env.uf t1 t2 with
-                   | Some (ex_r, _) ->
+                   | Entailed { ex = ex_r; _ } ->
                      let a = E.mk_distinct ~iff:false [x; y] in
                      Debug.contra_congruence a ex_r;
                      Q.push (Literal.LTerm a, ex_r, Th_util.Other) facts.diseqs
-                   | None -> assert false
+                   | Unknown -> assert false
                  end
              | _ -> ()
           ) (Uf.class_of env.uf bol)
@@ -739,7 +740,8 @@ module Main : S = struct
     {env with relation = Rel.assume_th_elt env.relation th_elt dep}
 
   let are_equal env t1 t2 ~init_terms =
-    if E.equal t1 t2 then Some (Ex.empty, [])
+    if E.equal t1 t2 then
+      Th_util.Entailed { ex = Ex.empty; classes = [] }
     else
     if init_terms then
       let facts = empty_facts() in
@@ -748,7 +750,8 @@ module Main : S = struct
       try
         let env, _ = assume_literals env [] facts in
         Uf.are_equal env.uf t1 t2 ~added_terms:true
-      with Ex.Inconsistent (ex,cl) -> Some (ex, cl)
+      with Ex.Inconsistent (ex, classes) ->
+        Entailed { ex; classes }
     else
       Uf.are_equal env.uf t1 t2 ~added_terms:false
 

src/lib/reasoners/fun_sat.ml

@@ -678,8 +678,10 @@ module Make (Th : Theory.S) = struct
     with Not_found ->
       assert (E.is_ground a);
       match Th.query a env.tbox with
-      | None -> tmp_cache := ME.add a None !tmp_cache; None
-      | Some (ex,_) as y ->
+      | Unknown ->
+        tmp_cache := ME.add a Th_util.Unknown !tmp_cache;
+        Unknown
+      | Entailed { ex; _ } as y ->
         if Options.get_tableaux_cdcl () then
           cdcl_learn_clause true env ex (ff.E.ff);
         learn_clause env ff ex;
@@ -689,53 +691,60 @@ module Make (Th : Theory.S) = struct
     match E.form_view ff.E.ff with
     | E.Literal a ->
       let ans = query_of tcp_cache tmp_cache ff a env in
-      if ans != None then
-        begin
-          Options.tool_req 2 "TR-Sat-Bcp-Elim-2";
-          if Options.get_profiling() then Profiling.elim false;
-        end;
+      let () =
+        match ans with
+        | Entailed _ ->
+          begin
+            Options.tool_req 2 "TR-Sat-Bcp-Elim-2";
+            if Options.get_profiling() then Profiling.elim false;
+          end
+        | Unknown -> ()
+      in
       ans
     | E.Unit _ | E.Clause _ | E.Lemma _ | E.Skolem _
-    | E.Let _ | E.Iff _ | E.Xor _ -> None
+    | E.Let _ | E.Iff _ | E.Xor _ -> Unknown
 
   let red tcp_cache tmp_cache ff env tcp =
     let nf = E.neg ff.E.ff in
     let nff = {ff with E.ff = nf} in
     try
       let _, ex = ME.find nf !(env.unit_facts_cache) in
-      Some(ex, []), true
+      Th_util.Entailed { ex; classes = [] }, true
     with Not_found ->
     try
       let _, ex, _, _ = ME.find nf env.gamma in
-      let r = Some (ex, Th.cl_extract env.tbox) in
       Options.tool_req 2 "TR-Sat-Bcp-Red-1";
-      r, true
+      Entailed { ex; classes = Th.cl_extract env.tbox }, true
     with Not_found ->
-      if not tcp then None, false
+      if not tcp then Unknown, false
       else match E.form_view nf with
         | E.Literal a ->
           let ans = query_of tcp_cache tmp_cache nff a env in
-          if ans != None then Options.tool_req 2 "TR-Sat-Bcp-Red-2";
+          let () =
+            match ans with
+            | Entailed _ -> Options.tool_req 2 "TR-Sat-Bcp-Red-2"
+            | _ -> ()
+          in
           ans, false
         | E.Unit _ | E.Clause _ | E.Lemma _ | E.Skolem _
-        | E.Let _ | E.Iff _ | E.Xor _ -> None, false
+        | E.Let _ | E.Iff _ | E.Xor _ -> Unknown, false
 
   let red tcp_cache tmp_cache ff env tcp =
     match red tcp_cache tmp_cache ff env tcp with
-    | (Some _, _)  as ans -> ans
-    | None, b ->
+    | Entailed _, _  as ans -> ans
+    | Unknown, b ->
       if not (Options.get_tableaux_cdcl ()) then
-        None, b
+        Th_util.Unknown, b
       else
         match CDCL.is_true !(env.cdcl) (E.neg ff.E.ff) with
         | Some (ex, _lvl) ->
           let ex = Lazy.force ex in
           if Options.(get_debug_sat () && get_verbose ()) then
             Printer.print_dbg "red thanks to satML";
           assert (cdcl_known_decisions ex env);
-          Some(ex, []), true
+          Entailed { ex; classes = [] }, true
         | None ->
-          None, b
+          Unknown, b
 
   let add_dep f dep =
     match E.form_view f with
@@ -790,16 +799,16 @@ module Make (Th : Theory.S) = struct
             let u =
               match th_elim tcp_cache tmp_cache gf1 env,
                     th_elim tcp_cache tmp_cache gf2 env with
-              | None, None -> raise Exit
-              | Some _, _ | _, Some _ when gf1.E.theory_elim -> u
+              | Unknown, Unknown -> raise Exit
+              | Entailed _, _ | _, Entailed _ when gf1.E.theory_elim -> u
 
-              | Some _, Some _ ->
+              | Entailed _, Entailed _ ->
                 u (* eliminate if both are true ? why ? *)
               (*(gf1, Ex.union d d1) :: (gf2, Ex.union d d2) :: u*)
 
-              | Some (d1, _), _ -> (gf1, Ex.union d d1) :: u
+              | Entailed { ex = d1; _ }, _ -> (gf1, Ex.union d d1) :: u
 
-              | _, Some (d2, _) -> (gf2, Ex.union d d2) :: u
+              | _, Entailed { ex = d2; _ } -> (gf2, Ex.union d d2) :: u
             in
             cl, u
           with Exit ->
@@ -809,27 +818,28 @@ module Make (Th : Theory.S) = struct
                 red tcp_cache tmp_cache gf1 env tcp,
                 red tcp_cache tmp_cache gf2 env tcp
               with
-              | (Some (d1, c1), b1) , (Some (d2, c2), b2) ->
+              | (Entailed { ex = d1; classes = c1 }, b1),
+                (Entailed { ex = d2; classes = c2 }, b2) ->
                 if Options.get_profiling() then Profiling.bcp_conflict b1 b2;
                 let expl = Ex.union (Ex.union d d1) d2 in
                 let c = List.rev_append c1 c2 in
                 raise (Ex.Inconsistent (expl, c))
 
-              | (Some(d1, _), b) , (None, _) ->
+              | (Entailed { ex = d1; _ }, b), (Unknown, _) ->
                 if Options.get_profiling() then Profiling.red b;
                 let gf2 =
                   {gf2 with E.nb_reductions = gf2.E.nb_reductions + 1} in
                 let gf2 = update_distances env gf2 f1 in
                 cl, (gf2,Ex.union d d1) :: u
 
-              | (None, _) , (Some(d2, _),b) ->
+              | (Unknown, _) , (Entailed { ex = d2; _ }, b) ->
                 if Options.get_profiling() then Profiling.red b;
                 let gf1 =
                   {gf1 with E.nb_reductions = gf1.E.nb_reductions + 1} in
                 let gf1 = update_distances env gf1 f2 in
                 cl, (gf1,Ex.union d d2) :: u
 
-              | (None, _) , (None, _) -> fd::cl , u
+              | (Unknown, _) , (Unknown, _) -> fd::cl , u
             end
       ) acc delta
 
@@ -1185,9 +1195,9 @@ module Make (Th : Theory.S) = struct
            | E.Literal a ->
              begin
                match query_of tcp_cache tmp_cache {gf with E.ff=f} a env with
-               | Some (ex, _) ->
+               | Entailed { ex; _ } ->
                  Ex.union dep ex, ({gf with E.ff=f}, ex) :: acc
-               | None ->
+               | Unknown ->
                  Printer.print_err
                    "Bad inst! Hyp %a is not true!" E.print f;
                  assert false

src/lib/reasoners/intervalCalculus.ml

@@ -794,9 +794,10 @@ let cannot_be_equal_to_zero env p ip =
   try
     let z = alien_of (P.create [] Q.zero (P.type_info p)) in
     match X.solve (alien_of p) z with
-    | [] -> None (* p is equal to zero *)
+    | [] -> Th_util.Unknown (* p is equal to zero *)
     | _ -> I.doesnt_contain_0 ip
-  with Util.Unsolvable -> Some (Explanation.empty, env.classes)
+  with Util.Unsolvable ->
+    Entailed { ex = Explanation.empty; classes = env.classes }
 
 
 let rec init_monomes_of_poly are_eq env p use_p expl =
@@ -867,22 +868,23 @@ and update_monome are_eq expl use_x env x =
             let env, ib =
               init_alien are_eq expl pb npb use_x env in
             let ib = I.add_explanation ib eb in (* take repr into account*)
-            let ia, ib = match cannot_be_equal_to_zero env pb ib with
-              | Some (ex, _) when Q.equal ca cb
-                               && P.compare pa' pb' = 0 ->
+            let ia, ib =
+              match cannot_be_equal_to_zero env pb ib with
+              | Entailed { ex; _ }
+                when Q.equal ca cb && P.compare pa' pb' = 0 ->
                 let expl = Explanation.union ex expl in
                 I.point da ty expl, I.point db ty expl
-              | Some (ex, _) ->
+              | Entailed { ex; _ } ->
                 begin
                   match are_eq a b with
-                  | Some (ex_eq, _) ->
+                  | Th_util.Entailed { ex = ex_eq; _ } ->
                     let expl = Explanation.union ex expl in
                     let expl = Explanation.union ex_eq expl in
                     I.point Q.one ty expl,
                     I.point Q.one ty expl
-                  | None -> ia, ib
+                  | Unknown -> ia, ib
                 end
-              | None -> ia, ib
+              | Unknown -> ia, ib
             in
             I.div ia ib, env
           | _ -> I.undefined ty, env
@@ -1743,8 +1745,9 @@ let assume ~query env uf la =
 let query env uf a_ex =
   try
     ignore(assume ~query:true env uf [a_ex]);
-    None
-  with Ex.Inconsistent (expl, classes) -> Some (expl, classes)
+    Th_util.Unknown
+  with Ex.Inconsistent (ex, classes) ->
+    Entailed { ex; classes }
 
 let case_split_polynomes env =
   let o = MP.fold
@@ -1824,7 +1827,10 @@ let default_case_split env uf ~for_model =
 
 let add =
   let are_eq t1 t2 =
-    if E.equal t1 t2 then Some (Explanation.empty, []) else None
+    if E.equal t1 t2 then
+      Th_util.Entailed { ex = Explanation.empty; classes = [] }
+    else
+      Unknown
   in
   fun env new_uf r t ->
     Debug.env env;

src/lib/reasoners/intervals.ml

@@ -757,17 +757,16 @@ module Legacy = struct
     | _ -> Fmt.invalid_arg "point: %a (as %a)" Q.pp_print v Ty.print ty
 
   let doesnt_contain_0 u =
-    Option.map (fun ex -> (ex, [])) @@
     match u with
     | Real u -> Real.(
         match intersect u (of_interval @@ Interval.singleton Q.zero) with
-        | NonEmpty _ -> None
-        | Empty ex -> Some ex
+        | NonEmpty _ -> Th_util.Unknown
+        | Empty ex -> Entailed { ex; classes = [] }
       )
     | Int u -> Int.(
         match intersect u (of_interval @@ Interval.singleton Z.zero) with
-        | NonEmpty _ -> None
-        | Empty ex -> Some ex
+        | NonEmpty _ -> Unknown
+        | Empty ex -> Entailed { ex; classes = [] }
       )
 
   let is_strict_smaller u1 u2 =