Give up if we try to optimize a strict inequality

src/lib/reasoners/intervalCalculus.ml

@@ -1383,9 +1383,6 @@ let fm (module Oracle : S with type p = P.t) uf are_eq rclass_of env eqs =
 let is_num r =
   let ty = X.type_info r in ty == Ty.Tint || ty == Ty.Treal
 
-let is_num_term r =
-  let ty = E.type_info r in ty == Ty.Tint || ty == Ty.Treal
-
 let add_disequality are_eq env eqs p expl =
   let ty = P.type_info p in
   match P.to_list p with
@@ -2062,11 +2059,16 @@ let optimizing_split env uf opt_split =
       E.print e
       (if to_max then "maximum" else "minimum")
       Q.print optim;
+
     let r2 = alien_of (P.create [] optim  ty) in
-    let t2 = mk_const_term optim ty in
     Debug.case_split r1 r2;
-    let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
-    let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
+    let t2 = mk_const_term optim ty in
+    let o =
+      Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2}
+    in
+    let s =
+      LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one)
+    in
     Some { opt_split with value = Value s }
 
   | None ->
@@ -2089,8 +2091,7 @@ let optimizing_split env uf opt_split =
         in
         Some { opt_split with value }
 
-      | Sim.Core.Max(mx,_sol) ->
-        let {Sim.Core.max_v; _} = Lazy.force mx in
+      | Sim.Core.Max (lazy Sim.Core.{ max_v; is_le = true }, _sol) ->
         let max_p = Q.add max_v.bvalue.v c in
         let optim = if to_max then max_p else Q.mult Q.m_one max_p in
         Printer.print_dbg "%a has a %s: %a@."
@@ -2108,6 +2109,10 @@ let optimizing_split env uf opt_split =
           LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one)
         in
         Some { opt_split with value = Value s; }
+
+      | Sim.Core.Max (lazy Sim.Core.{ is_le = false; _ }, _) ->
+        (* There is no upper bound as we try to optimize a strict bound. *)
+        None
     end
 
 (*** part dedicated to FPA reasoning ************************************)

src/lib/reasoners/satml_frontend.ml

@@ -1063,7 +1063,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
              | Value _ ->
                assert false
              | Unknown ->
-               assert false
+               seen_infinity := true; acc
         ) obj []
     in
     begin match acc with

src/lib/reasoners/theory.ml

@@ -428,42 +428,58 @@ module Main_Default : S = struct
              | Th_util.Unknown -> acc (* not optimized yet *)
              | Value _ -> Util.MI.add ord {v with value = Unknown} acc
              | Pinfinity | Minfinity -> assert false (* may happen? *)
-        )objectives objectives
+        ) objectives objectives
 
   let look_for_sat ?(bad_last=None) ch env l ~for_model =
-    let rec aux ch bad_last dl env li =
+    let rec aux ~optimize ch bad_last dl env li =
       Options.exec_thread_yield ();
       match li, bad_last with
       | [], _ ->
         begin
           Options.tool_req 3 "TR-CCX-CS-Case-Split";
-          match next_optimization ~for_model env with
-          | Some opt_split ->
-            begin
-              let opt_split =
+          if optimize then
+            match next_optimization ~for_model env with
+            | Some opt_split ->
+              begin
                 match CC_X.optimizing_split env.gamma_finite opt_split with
-                | Some x -> x
+                | Some x ->
+                  let to_opt =
+                    register_optimized_split env.objectives x
+                  in
+                  let env = {env with objectives = to_opt} in
+                  begin
+                    match x.value with
+                    | Value v ->
+                      let splits = add_explanations_to_splits [v] in
+                      aux ~optimize ch None dl env splits
+                    | Pinfinity | Minfinity ->
+                      if for_model then
+                        aux ~optimize:false ch None dl env []
+                      else
+                        { env with choices = List.rev dl }, ch
+                    | Unknown -> assert false
+                  end
                 | None ->
-                  (* At least one theory should be able to optimize the
-                     split. *)
-                  assert false
-              in
-              let to_opt = register_optimized_split env.objectives opt_split in
-              let env = {env with objectives = to_opt} in
-              begin
-                match opt_split.value with
-                | Value v ->
-                  let splits = add_explanations_to_splits [v] in
-                  aux ch None dl env splits
-                | Pinfinity | Minfinity ->
                   if for_model then
-                    aux ch None dl env []
+                    aux ~optimize:false ch None dl env []
                   else
                     { env with choices = List.rev dl }, ch
-                | Unknown -> assert false
               end
-            end
-          | None ->
+            | None ->
+              begin
+                let l, base_env =
+                  CC_X.case_split env.gamma_finite ~for_model
+                in
+                let env = {env with gamma_finite = base_env} in
+                match l with
+                | [] ->
+                  { env with choices = List.rev dl }, ch
+
+                | _ ->
+                  let l = add_explanations_to_splits l in
+                  aux ~optimize ch None dl env l
+              end
+          else
             begin
               let l, base_env =
                 CC_X.case_split env.gamma_finite ~for_model
@@ -475,15 +491,15 @@ module Main_Default : S = struct
 
               | _ ->
                 let l = add_explanations_to_splits l in
-                aux ch None dl env l
+                aux ~optimize ch None dl env l
             end
         end
       | ((c, lit_orig, CNeg, ex_c) as a)::l, _ ->
         let facts = CC_X.empty_facts () in
         CC_X.add_fact facts (LSem c,ex_c,lit_orig);
         let base_env, ch = CC_X.assume_literals env.gamma_finite ch facts in
         let env = { env with gamma_finite = base_env} in
-        aux ch bad_last (a::dl) env l
+        aux ~optimize ch bad_last (a::dl) env l
 
       (* This optimisation is not correct with the current explanation *)
       (* | [(c, lit_orig, CPos exp, ex_c)], Yes (dep,_) -> *)
@@ -500,7 +516,7 @@ module Main_Default : S = struct
           let base_env, ch =  CC_X.assume_literals env.gamma_finite ch facts in
           let env = { env with gamma_finite = base_env} in
           Options.tool_req 3 "TR-CCX-CS-Normal-Run";
-          aux ch bad_last (a::dl) env l
+          aux ~optimize ch bad_last (a::dl) env l
         with Ex.Inconsistent (dep, classes) ->
         match Ex.remove_fresh exp dep with
         | None ->
@@ -524,9 +540,9 @@ module Main_Default : S = struct
           let env =
             { env with objectives =
                          partial_objectives_reset env.objectives is_opt } in
-          aux ch None dl env [neg_c, lit_orig, CNeg, dep]
+          aux ~optimize ch None dl env [neg_c, lit_orig, CNeg, dep]
     in
-    aux ch bad_last (List.rev env.choices) env l
+    aux ~optimize:true ch bad_last (List.rev env.choices) env l
 
   (* remove old choices involving fresh variables that are no longer in UF *)
   let filter_valid_choice uf (ra,_,_,_) =

tests/models/arith/arith7.optimize.expected

@@ -0,0 +1,10 @@
+
+unknown
+(
+  (define-fun x () Real 0)
+)
+
+unknown
+(
+  (define-fun x () Real (- (/ 3 2)))
+)

tests/models/arith/arith7.optimize.smt2

@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Real)
+(push 1)
+(assert (< x 0.5))
+(maximize x)
+(check-sat)
+(get-model)
+(pop 1)
+(push 1)
+(assert (< x (- 0.0 0.5)))
+(maximize x)
+(check-sat)
+(get-model)
+(pop 1)