Update documentation of Th.optimize_obj

src/lib/reasoners/sig_rel.mli

@@ -86,7 +86,20 @@ module type RELATION = sig
   val optimizing_objective :
     t -> Uf.t -> Objective.Function.t -> Th_util.optimized_split option
   (** [optimizing_split env uf o] tries to optimize objective [o].
-      Returns [None] if the theory cannot optimize the objective. *)
+      Returns [None] if no theory knows how to optimize the objective.
+
+      If the function returns [Some o] then the value of the optimized split
+      [o] is never [Unknown] because all the theories that support
+      optimization will always produce an answer even if this answer is not
+      the best value.
+
+      For instance, if the objective is a nonlinear arithmetical
+      expressions of the form:
+        5 * x * x + 2 * y + 3,
+      the arithmetic theory will translate this function into the linear
+      objective function:
+        5 * U + 2 * y + 3 where U = x * x
+      and send it to Ocplib-simplex. *)
 
   val add : t -> Uf.t -> Shostak.Combine.r -> Expr.t ->
     t * Uf.GlobalDomains.t *

src/lib/reasoners/theory.ml

@@ -617,25 +617,8 @@ module Main_Default : S = struct
     in
     match opt_split.value with
     | Unknown ->
-      (* In the current implementation of optimization, the function
-         [CC_X.optimizing_objective] cannot fail to optimize the objective
-         function [obj]. First of all, the parser only accepts
-         optimization clauses on expressions of type [Real] or [Int].
-         For the [Real] or [Int] expressions, we have two cases:
-         - If the objective function is a linear functions of variables, the
-           decision procedure implemented in Ocplib-simplex cannot fail to
-           optimize the split. For instance, if we try to maximize the
-           expression:
-             5 * x + 2 * y + 3 where x and y are real variables,
-           the procedure will success to produce the upper bound of [x] and
-           [y] modulo the other constraints on it.
-         - If the objective function isn't linear, the nonlinear part of the
-           expression is seen as uninterpreted term of the arithmetic theory.
-           Let's imagine we try to maximize the expression:
-             5 * x * x + 2 * y + 3,
-           The objective function given to Ocplib-simplex looks like:
-             5 * U + 2 * y + 3 where U = x * x
-           and the procedure will optimize the problem in terms of U and y. *)
+      (* Cannot happen as [Rel.optimizing_objective] never returns an
+         unknown value. *)
       assert false
 
     | Pinfinity | Minfinity | Limit _ when not for_model ->