Models: export the map of term |-> get-value(term) computed in UF

OCamlPro · Oct 4, 2023 · c203ad1 · c203ad1
1 parent 741f26c
commit c203ad1
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 10 deletions.
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
@@ -384,10 +384,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         (Some time) (Some steps)
 
 
-
-
-
-
   let init_with_replay_used acc f =
     assert (Sys.file_exists f);
     let cin = open_in f in

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
@@ -56,7 +56,8 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t
+  objectives: (Expr.t * objective_value) Util.MI.t;
+  terms_values : (Shostak.Combine.r * string) Expr.Map.t
 }
 
 module Pp_smtlib_term = struct
@@ -437,9 +438,6 @@ module SmtlibCounterExample = struct
       ) fprofs;
     !records
 
-  let output_arrays_counterexample fmt _arrays =
-    fprintf fmt "@ ; Arrays not yet supported@ "
-
   let output_objectives fmt objectives =
     (* TODO: we can decide to print objectives to stderr if
        Options.get_objectives_in_interpretation() is enabled *)

diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli
@@ -41,7 +41,10 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t
+  objectives: (Expr.t * objective_value) Util.MI.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. *)
 }
 
 val output_concrete_model : t Fmt.t

diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
@@ -1182,7 +1182,8 @@ let extract_concrete_model ~prop_model ~optimized_splits env =
         in
         let objectives = compute_objectives ~optimized_splits env mrepr in
         { Models.propositional = prop_model;
-          functions; constants; arrays; objectives }
+          functions; constants; arrays; objectives;
+          terms_values = mrepr }
       ))
   else
     None