Adding basic get_value (breaks a .ae test)

OCamlPro · Nov 2, 2023 · 935b1fa · 935b1fa
1 parent 9b461ef
commit 935b1fa
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 2 deletions.
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
@@ -1847,7 +1847,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
-  let get_value _env _t = None
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
 
   let reinit_ctx () =
     (* all_models_sat_env := None; *)

diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
@@ -1249,7 +1249,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
-  let get_value _env _t = None
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
 
   let reinit_ctx () =
     Steps.reinit_steps ();