Objective values are polymorphic

The values of objectives now uses a polymorphic type as we will need
them to store the final objective model.

src/lib/dune

@@ -58,7 +58,7 @@
     Emap Gc_debug Hconsing Hstring Iheap Lists Loc
     MyUnix Numbers
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories Compat Fqueue
+    Theories Compat
   )
 
  (js_of_ocaml

src/lib/frontend/models.ml

@@ -56,7 +56,7 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: Objective.Model.t;
+  objectives: Expr.t Objective.Model.t;
   terms_values : (Shostak.Combine.r * string) Expr.Map.t
 }
 

src/lib/frontend/models.mli

@@ -41,7 +41,7 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: Objective.Model.t;
+  objectives: Expr.t Objective.Model.t;
   terms_values : (Shostak.Combine.r * string) Expr.Map.t
   (** A map from terms to their values in the model (as a
       representative of type X.r and as a string. *)

src/lib/reasoners/ccx.ml

@@ -88,7 +88,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_objectives:Objective.Model.t ->
+    optimized_objectives:Expr.t Objective.Model.t ->
     t ->
     Models.t Lazy.t option
 

src/lib/reasoners/ccx.mli

@@ -79,7 +79,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_objectives:Objective.Model.t ->
+    optimized_objectives:Expr.t Objective.Model.t ->
     t ->
     Models.t Lazy.t option
 

src/lib/reasoners/satml_frontend.ml

@@ -1097,7 +1097,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     let acc =
       try
         Objective.Model.fold (fun { e; to_max; _ } value acc ->
-            match (value : Objective.Value.t) with
+            match (value : Expr.t Objective.Value.t) with
             | Pinfinity | Minfinity ->
               raise (Give_up acc)
             | Value v ->

src/lib/reasoners/th_util.ml

@@ -48,6 +48,6 @@ type lit_origin =
 type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin
 
 type optimized_split = {
-  value : Objective.Value.t;
+  value : Expr.t Objective.Value.t;
   case_split : case_split;
 }

src/lib/reasoners/th_util.mli

@@ -81,7 +81,7 @@ type lit_origin =
 type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin
 
 type optimized_split = {
-  value : Objective.Value.t;
+  value : Expr.t Objective.Value.t;
   case_split : case_split;
   (** The underlying case-split. Notice that this case-split doesn't always
       propagate to CC(X) an equality of the form [r = v] where [v] should be

src/lib/reasoners/theory.ml

@@ -75,7 +75,7 @@ module type S = sig
 
   val get_assumed : t -> E.Set.t
   val reinit_cpt : unit -> unit
-  val get_objectives : t -> Objective.Model.t
+  val get_objectives : t -> Expr.t Objective.Model.t
 end
 
 module Main_Default : S = struct
@@ -351,9 +351,9 @@ module Main_Default : S = struct
     gamma : CC_X.t;
     gamma_finite : CC_X.t;
     choices : choice list;
-    objectives : Objective.Function.t Fqueue.t;
+    objectives : Objective.Function.t list;
     objective_n : int;
-    objectives_values : Objective.Model.t;
+    objectives_values : Expr.t Objective.Model.t;
   }
 
   let add_explanations_to_split (c, is_cs, size) =
@@ -367,36 +367,6 @@ module Main_Default : S = struct
 
   exception Found of Th_util.optimized_split
 
-  (* TODO: this function could be optimized if "objectives" structure
-     is coded differently *)
-  (* let next_optimization ~for_model env =
-     try
-      Util.MI.iter (fun _ x ->
-          match x.Th_util.value with
-          | Value _ ->
-            (* This split is already optimized. *)
-            ()
-          | Pinfinity | Minfinity | Limit _ ->
-            (* We should block case-split at infinite values.
-                  Otherwise, we may have soundness issues. We
-                  may think an objective is unbounded, but some late
-                  constraints may make it bounded.
-
-                  An alternative is to only allow further splits when we
-                  know that no extra assumptions will be propagated to
-                  the env. Hence the test 'if for_model' *)
-            if for_model then ()
-            else
-              raise (Found { x with Th_util.value = Unknown })
-
-          | Unknown ->
-            raise (Found { x with Th_util.value = Unknown })
-
-        ) env.objectives;
-      None
-     with
-     | Found x -> Some x *)
-
   (* TODO: We cannot retrieve the order of an objecive with the current
      structure used for objective model. *)
   let partial_objectives_reset env _order =
@@ -436,9 +406,9 @@ module Main_Default : S = struct
         let new_choices =
           List.map add_explanations_to_split new_splits
         in
-        aux env sem_facts acc_choices new_choices
+        aux env sem_facts acc_choices [] new_choices
 
-    and optimizing_objective env sem_facts acc_choices obj =
+    and optimizing_objective env sem_facts acc_choices acc_objs obj =
       let opt_split =
         Option.get (CC_X.optimizing_objective env.gamma_finite obj)
       in
@@ -451,14 +421,14 @@ module Main_Default : S = struct
         (* We stop optimizing the split [opt_split] in this case, but
            we continue to produce a model if the flag [for_model] is up. *)
         if for_model then
-          aux env sem_facts acc_choices []
+          aux env sem_facts acc_choices acc_objs []
         else
           { env with choices = List.rev acc_choices }, sem_facts
 
       | Value _ ->
         begin
           let new_choice = add_explanations_to_split opt_split.case_split in
-          propagate_choices env sem_facts acc_choices [new_choice]
+          propagate_choices env sem_facts acc_choices acc_objs [new_choice]
         end
 
     (* Propagates the choice made by case-splitting to the environment
@@ -468,10 +438,10 @@ module Main_Default : S = struct
        @raise [Inconsistent] if we detect an inconsistent with the choice
               on the top of [new_choices] but this choice doesn't
               participate to the inconsistency. *)
-    and propagate_choices env sem_facts acc_choices new_choices =
+    and propagate_choices env sem_facts acc_choices acc_objs new_choices =
       Options.exec_thread_yield ();
       match new_choices with
-      | [] -> aux env sem_facts acc_choices new_choices
+      | [] -> aux env sem_facts acc_choices acc_objs new_choices
 
       | ((c, lit_orig, CNeg, ex_c, _order) as a) :: new_choices ->
         let facts = CC_X.empty_facts () in
@@ -480,7 +450,7 @@ module Main_Default : S = struct
           CC_X.assume_literals env.gamma_finite sem_facts facts
         in
         let env = { env with gamma_finite = base_env } in
-        propagate_choices env sem_facts (a :: acc_choices) new_choices
+        propagate_choices env sem_facts (a :: acc_choices) acc_objs new_choices
 
       | ((c, lit_orig, CPos exp, ex_c_exp, order) as a) :: new_choices ->
         try
@@ -492,7 +462,7 @@ module Main_Default : S = struct
           in
           let env = { env with gamma_finite = base_env } in
           Options.tool_req 3 "TR-CCX-CS-Normal-Run";
-          propagate_choices env sem_facts (a :: acc_choices) new_choices
+          propagate_choices env sem_facts (a :: acc_choices) acc_objs new_choices
 
         with Ex.Inconsistent (dep, classes) ->
         (* As we generate fresh explanation for each choice in
@@ -524,29 +494,23 @@ module Main_Default : S = struct
               "bottom (case-split):%a"
               Expr.print_tagged_classes classes;
           let env = partial_objectives_reset env order in
-          propagate_choices env sem_facts acc_choices
+          propagate_choices env sem_facts acc_choices acc_objs
             [neg_c, lit_orig, CNeg, dep, order]
 
-    and aux env sem_facts acc_choices new_choices =
+    and aux env sem_facts acc_choices acc_objs new_choices =
       Options.tool_req 3 "TR-CCX-CS-Case-Split";
       match new_choices with
       | [] ->
-        let obj, objectives = Fqueue.dequeue env.objectives in
-        begin match obj with
-          | Some obj ->
-            let env = { env with objectives } in
-            optimizing_objective env sem_facts acc_choices obj
-          | None ->
+        begin match acc_objs with
+          | obj :: acc_objs ->
+            optimizing_objective env sem_facts acc_choices acc_objs obj
+          | [] ->
             generate_choices env sem_facts acc_choices
         end
       | _ ->
-        propagate_choices env sem_facts acc_choices new_choices
-    in
-    let o = env.objectives in
-    let env, choices =
-      aux env sem_facts (List.rev env.choices) new_choices
+        propagate_choices env sem_facts acc_choices acc_objs new_choices
     in
-    { env with objectives = o }, choices
+    aux env sem_facts (List.rev env.choices) (List.rev env.objectives) new_choices
 
   (* remove old choices involving fresh variables that are no longer in UF *)
   let filter_valid_choice uf (ra, _, _, _, _) =
@@ -646,8 +610,8 @@ module Main_Default : S = struct
             let uf =  CC_X.get_union_find t.gamma in
             let filt_choices = filter_choices uf t.choices in
             (* let filt_choices =
-               if Util.MI.is_empty t.objectives ||
-                 has_no_limit t.objectives
+               if Lists.is_empty t.objectives ||
+                  has_no_limit t.objectives
                  (* otherwise, we may be unsound because infty optims
                     are not propagated *)
                  then filt_choices
@@ -929,7 +893,7 @@ module Main_Default : S = struct
         assumed = [];
         cs_pending_facts = [];
         terms = Expr.Set.empty;
-        objectives = Fqueue.empty;
+        objectives = [];
         objective_n = 0;
         objectives_values = Objective.Model.empty;
       }
@@ -984,7 +948,7 @@ module Main_Default : S = struct
 
   let optimize env ~to_max fun_ =
     let obj = Objective.Function.mk ~to_max ~order:env.objective_n fun_ in
-    let objectives = Fqueue.enqueue obj env.objectives in
+    let objectives = obj :: env.objectives in
     let env = reset_case_split_env env in
     { env with objectives; objective_n = env.objective_n + 1 }
 

src/lib/reasoners/theory.mli

@@ -66,7 +66,7 @@ module type S = sig
   val reinit_cpt : unit -> unit
   (** Reinitializes the internal counter. *)
 
-  val get_objectives : t -> Objective.Model.t
+  val get_objectives : t -> Expr.t Objective.Model.t
 end
 
 module Main_Default : S

src/lib/reasoners/uf.ml

@@ -1107,7 +1107,7 @@ let terms env = ME.fold MED.add env.make MED.empty
 let compute_concrete_model ?(optimized_objectives=Objective.Model.empty) env =
   let bounded, pinfty, minfty =
     Objective.Model.fold (fun { e; _ } value (bounded, pinfty, minfty) ->
-        match (value : Objective.Value.t) with
+        match (value : Expr.t Objective.Value.t) with
         | Value e | Limit (_, e) ->
           (* TODO: we should use a different branch for the limit cases. *)
           let r, _ = Shostak.Combine.make e in

src/lib/reasoners/uf.mli

@@ -74,7 +74,7 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
 (** Compute a counterexample using the Uf environment *)
 val extract_concrete_model :
   prop_model:Expr.Set.t ->
-  optimized_objectives:Objective.Model.t ->
+  optimized_objectives:Expr.t Objective.Model.t ->
   t ->
   Models.t Lazy.t option
 

src/lib/structures/objective.ml

@@ -47,23 +47,23 @@ module Value = struct
     | Above
     | Below
 
-  type t =
+  type 'a t =
     | Minfinity
     | Pinfinity
-    | Value of Expr.t
-    | Limit of limit_kind * Expr.t
+    | Value of 'a
+    | Limit of limit_kind * 'a
 
-  let pp _ppf _val = assert false
+  let pp _pp_elt _ppf _val = assert false
 end
 
 module Model = struct
   module M =  Map.Make (Function)
 
-  type t = Value.t M.t
+  type 'a t = 'a Value.t M.t
 
   let empty = M.empty
   let is_empty = M.is_empty
   let fold = M.fold
   let add = M.add
-  let pp _ppf _mdl = assert false
+  let pp _pp_elt _ppf _mdl = assert false
 end

src/lib/structures/objective.mli

@@ -46,25 +46,25 @@ module Value : sig
     | Below
     (** Type used to discriminate between limits from above or below. *)
 
-  type t =
+  type 'a t =
     | Minfinity
     | Pinfinity
-    | Value of Expr.t
-    | Limit of limit_kind * Expr.t
+    | Value of 'a
+    | Limit of limit_kind * 'a
     (** This case occurs when we try to optimize a strict bound. For instance,
         we have a constraint of the form [x < 2], there is no maximum for [x] but
         [2] is an upper bound. So [2] is a limit from below of the possible model
         values. *)
 
-  val pp : t Fmt.t
+  val pp : 'a Fmt.t -> 'a t Fmt.t
 end
 
 module Model : sig
-  type t
+  type 'a t
 
-  val empty : t
-  val is_empty : t -> bool
-  val fold : (Function.t -> Value.t -> 'a -> 'a) -> t -> 'a -> 'a
-  val add : Function.t -> Value.t -> t -> t
-  val pp : t Fmt.t
+  val empty : 'a t
+  val is_empty : 'a t -> bool
+  val fold : (Function.t -> 'a Value.t -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val add : Function.t -> 'a Value.t -> 'a t -> 'a t
+  val pp : 'a Fmt.t -> 'a t Fmt.t
 end