Keep partial models in with a separate key

We keep the last consistent SAT environment with the Dolmen key
`partial_model` in `Solving_loop`. This solution isn't sufficient to
implement correctly `get-value`. Indeed, we need to ensure `get-model`
statements located after some `get-value` statements will still print
the same model. To obtain this behaviour, now we keep the last model
and the last unknown reason after a `check-sat` in a separate key.

Support `get-value` in Solving_loop

Add support for the SMT-LIB statement `get-value` in `Solving_loop`.
With the current implementation of the solver, it's not easy to keep
a consistent environment of the SAT solver without reassuming all the
formulas as we do in `Solving_loop`.

Instead, we save the last consistent environment obtained after a `check-sat`
statement in the Dolmen state and we have to keep the last model and unknown
reason with different keys. Indeed, after using `get-value`, the
`get-model` statement has to output the same model.

Create a new type name in `Symbols`

Refactoring `get-value` support

This commit adds a better support of `get-value` and `get-assignment`.
These features are implemented using a new wrapper functor on the top of
the SAT solvers of Alt-Ergo.

- Values for bool expressions are computed by the SAT solver;
- Before launching the solver to compute some model terms, we check if
  there aren't already available in the boolean or first-order models;
- Thanks to the wrapper functor, the feature works well with the legacy
  solver FunSAT;

We also test our generated models by non-regression tests using the
`get-value`.

Add option `--verify-models`

This option will be useful to check our models with the new
`get-value` command. Adding `--verify-models` turns on the model
generation (as we did with the `--produce-models` option). If our
best-effort model checker doesn't find a contradiction, we don't print
anything.

fix documentation

Add the location for get-value

À la C

Use first-class module instead of functor

Add Expr.Core.of_bool

Reinit GetValue cpt

spelling

Documentation of the module Graph

Derive comparison function of name_space

Restore the documentation of `name`

Remove the joke :(

Remove the joke :(

New exception for wrong model

We raise a new exception `Wrong_model` in `get_value` in order to
clarify the API.

Rebase artefacts

Removing get-value statements to check models

Add a new SMT option for the CLI option `--verify-models`

Use `Stdcompat.Either` for OCaml 4.08

Reset decisions only for get-value statements

We need to reset the decision level of SatML after calling the `unsat`
function as the decision level of this solver isn't necessary zero. This
hotfix is only necessary for SatML.

Add a new function `reset_decisions` in the SAT API.

Saved the boolean model before resetting decisions

The call `SAT.reset_decisions` may erase part of the boolean models in
`get_value`. For sake of efficiency, we save the boolean model before
resetting decisions.

Add tests

Add a link to issue 1063

Address partially review

Author: Halbaroth

CHANGES.md

@@ -10,6 +10,9 @@
   External plugins must now be registered through the dune-site plugin
   mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo.
 
+### New features
+* support for the SMT-LIB statement `get-value`
+
 ## v2.5.2
 
 ### Bug fixes

src/bin/common/parse_command.ml

@@ -367,7 +367,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
 
 let mk_output_opt
     interpretation use_underscore objectives_in_interpretation unsat_core
-    output_format model_type () () () ()
+    output_format model_type () () () () ()
   =
   set_infer_output_format (Option.is_none output_format);
   let output_format = match output_format with
@@ -863,7 +863,7 @@ let parse_output_opt =
 
   (* Use the --interpretation and --produce-models (which is equivalent to
      --interpretation last) to determine the interpretation value. *)
-  let interpretation, dump_models, dump_models_on, frontend =
+  let interpretation, dump_models, dump_models_on, verify_models, frontend =
     let interpretation =
       let doc = Format.sprintf
           "Best effort support for counter-example generation. \
@@ -888,13 +888,21 @@ let parse_output_opt =
       Arg.(value & opt interpretation INone &
            info ["interpretation"] ~docv ~docs:s_models ~doc)
     in
+
     let produce_models =
       let doc =
         "Enable model generation (equivalent to --interpretation last)."
       in
       Arg.(value & flag & info ["produce-models"] ~doc ~docs:s_models)
     in
 
+    let verify_models =
+      let doc =
+        "Verify generated models."
+      in
+      Arg.(value & flag & info ["verify-models"] ~doc ~docs:s_models)
+    in
+
 
     let frontend =
       let doc =
@@ -947,6 +955,7 @@ let parse_output_opt =
     ),
     dump_models,
     dump_models_on,
+    verify_models,
     frontend
   in
 
@@ -1113,6 +1122,10 @@ let parse_output_opt =
     Term.(const Output.set_dump_models $ dump_models_on)
   in
 
+  let set_verify_models =
+    Term.(const set_verify_models $ verify_models)
+  in
+
   let set_frontend =
     Term.(const set_frontend $ frontend)
   in
@@ -1121,7 +1134,7 @@ let parse_output_opt =
              interpretation $ use_underscore $
              objectives_in_interpretation $ unsat_core $
              output_format $ model_type $
-             set_dump_models $ set_dump_models_on $
+             set_dump_models $ set_dump_models_on $ set_verify_models $
              set_sat_options $ set_frontend
             ))
 

src/bin/common/solving_loop.ml

@@ -42,15 +42,11 @@ let is_solver_ctx_empty = function
     { ctx = []; local = []; global = [] } -> true
   | _ -> false
 
-type 'a sat_module = (module Sat_solver_sig.S with type t = 'a)
-
-type any_sat_module = (module Sat_solver_sig.S)
-
 (* Internal state while iterating over input statements *)
 type 'a state = {
   env : 'a;
   solver_ctx: solver_ctx;
-  sat_solver : any_sat_module;
+  sat_solver : Sat_solver_util.any_sat_module;
 }
 
 let empty_solver_ctx = {
@@ -101,6 +97,24 @@ let cmd_on_modes st modes cmd =
       Errors.forbidden_command curr_mode cmd
   end
 
+let verify_model ~get_value () =
+  match get_value [Expr.vrai] with
+  | Some [e] when Expr.equal e Expr.vrai -> ()
+
+  | Some [_]
+  | exception Sat_solver_util.Wrong_model _
+  | exception Sat_solver_util.No_model ->
+    recoverable_error "The model is wrong"
+
+  | None ->
+    (* The model generation is not enabled. *)
+    ()
+
+  | Some _ ->
+    (* The length of the output list is the same as the length of the
+       input list. *)
+    assert false
+
 (* Dolmen util *)
 
 (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *)
@@ -119,7 +133,7 @@ let add_if_named
     acc
 
 (* We currently use the full state of the solver as model. *)
-type model = Model : 'a sat_module * 'a -> model
+type model = Model : 'a Sat_solver_util.sat_module * 'a -> model
 
 type solve_res =
   | Sat of model
@@ -181,6 +195,12 @@ let main () =
             Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
               FE.print_model partial_model
           end;
+          if Options.get_verify_models () then begin
+            let get_value =
+              Sat_solver_util.get_value (module SAT) partial_model
+            in
+            verify_model ~get_value ()
+          end;
           Sat mdl
         end
       | `Unknown ->
@@ -194,6 +214,12 @@ let main () =
             Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
               FE.print_model partial_model
           end;
+          if Options.get_verify_models () then begin
+            let get_value =
+              Sat_solver_util.get_value (module SAT) partial_model
+            in
+            verify_model ~get_value ()
+          end;
           Unknown (Some mdl)
         end
       | `Unsat -> Unsat
@@ -342,7 +368,7 @@ let main () =
   in
 
   let partial_model_key: model option State.key =
-    State.create_key ~pipe:"" "sat_state"
+    State.create_key ~pipe:"" "partial_model"
   in
 
   let named_terms: DStd.Expr.term Util.MS.t State.key =
@@ -685,6 +711,12 @@ let main () =
         | None -> print_wrn_opt ~name st_loc "integer" value; st
         | Some i -> set_steps_bound i st
       end
+    | ":verify-models", Symbol { name = Simple "true"; _ } ->
+      Options.set_verify_models true;
+      st
+    | ":verify-models", Symbol { name = Simple "false"; _ } ->
+      Options.set_verify_models false;
+      st
     | _ ->
       unsupported_opt name; st
   in
@@ -800,45 +832,45 @@ let main () =
       unsupported_opt name
   in
 
-  (* Fetches the term value in the current model. *)
-  let evaluate_term get_value name term =
-    (* There are two ways to evaluate a term:
-       - if its name is registered in the environment, get its value;
-       - if not, check if the formula is in the environment.
-    *)
-    let simple_form =
-      Expr.mk_term
-        (Sy.name name)
-        []
-        (D_cnf.dty_to_ty term.DStd.Expr.term_ty)
-    in
-    match get_value simple_form with
-    | Some v -> Fmt.to_to_string Expr.print v
-    | None -> "unknown"
+  let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) =
+    DStd.Loc.(lexing_positions (loc dloc_file compact_loc))
   in
 
-  let print_terms_assignments =
-    Fmt.list
-      ~sep:Fmt.cut
-      (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v)
+  let handle_get_value loc ~get_value l =
+    let l =
+      List.map (D_cnf.mk_expr ~loc ~toplevel:false
+                  ~decl_kind:Daxiom) l
+    in
+    match get_value l with
+    | Some values ->
+      Printer.print_std
+        "(@[<v 0>%a@])@,"
+        Fmt.(iter ~sep:cut Lists.iter_pair
+               ((pair ~sep:sp Expr.pp_smtlib Expr.pp_smtlib) |> parens))
+        (l, values)
+    | None ->
+      recoverable_error "No model produced, cannot execute get-value."
+    | exception Sat_solver_util.Wrong_model _ ->
+      recoverable_error "The model is wrong, cannot execute get-value."
+    | exception Sat_solver_util.No_model ->
+      recoverable_error "No model produced but it should, cannot execute get-value."
   in
 
-  let handle_get_assignment ~get_value st =
-    let assignments =
-      Util.MS.fold
-        (fun name term acc ->
-           if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then
-             (name, evaluate_term get_value name term) :: acc
-           else
-             acc
-        )
-        (State.get named_terms st)
-        []
+  let handle_get_assignment ~get_assignment st =
+    let names, l =
+      Util.MS.fold (fun name term (names, acc) ->
+          assert (DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool);
+          name :: names,
+          Expr.mk_term (Sy.name name) []
+            (D_cnf.dty_to_ty term.DStd.Expr.term_ty) :: acc
+        ) (State.get named_terms st) ([], [])
     in
+    let values = get_assignment l in
     Printer.print_std
       "(@[<v 0>%a@])@,"
-      print_terms_assignments
-      assignments
+      Fmt.(iter ~sep:cut Lists.iter_pair
+             ((pair ~sep:sp string Sat_solver_util.pp_lbool) |> parens))
+      (names, values)
   in
 
   let handle_stmt :
@@ -931,11 +963,12 @@ let main () =
       | {contents = `Get_model; _ } ->
         cmd_on_modes st [Sat] "get-model";
         if Options.get_interpretation () then
-          let () = match State.get partial_model_key st with
-            | Some (Model ((module SAT), env)) ->
+          let () =
+            match State.get partial_model_key st with
+            | Some Model ((module SAT), partial_model) ->
               let module FE = Frontend.Make (SAT) in
               Fmt.pf (Options.Output.get_fmt_regular ()) "%a@."
-                FE.print_model env
+                FE.print_model partial_model
             | None ->
               (* TODO: add the location of the statement. *)
               recoverable_error "No model produced."
@@ -979,9 +1012,10 @@ let main () =
           match State.get partial_model_key st with
           | Some Model ((module SAT), partial_model) ->
             if DO.ProduceAssignment.get st then
-              handle_get_assignment
-                ~get_value:(SAT.get_value partial_model)
-                st
+              let get_assignment =
+                Sat_solver_util.get_assignment (module SAT) partial_model
+              in
+              handle_get_assignment ~get_assignment st
             else
               recoverable_error
                 "Produce assignments disabled; \
@@ -994,6 +1028,24 @@ let main () =
             st
         end
 
+      | {contents = `Get_value l; loc; _} ->
+        begin
+          cmd_on_modes st [Sat] "get-value";
+          match State.get partial_model_key st with
+          | Some Model ((module SAT), partial_model) ->
+            let file = (State.get State.logic_file st).loc in
+            let loc = dl_to_ael file loc in
+            let get_value =
+              Sat_solver_util.get_value (module SAT) partial_model
+            in
+            handle_get_value loc ~get_value l;
+            st
+          | None ->
+            (* TODO: add the location of the statement. *)
+            recoverable_error "No model produced, cannot execute get-value.";
+            st
+        end
+
       | {contents = `Other (custom, args); loc; _} ->
         handle_custom_statement loc custom args st
 

src/lib/dune

@@ -52,7 +52,8 @@
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils Bitlist
+    Sat_solver Sat_solver_sig Sig Sat_solver_util Sig_rel Theory Uf Use
+    Rel_utils Bitlist
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols

src/lib/frontend/d_cnf.ml

@@ -32,7 +32,6 @@ module SE = E.Set
 
 module C = Commands
 module Sy = Symbols
-module SM = Sy.Map
 
 module DE = DStd.Expr
 module DT = DE.Ty
@@ -627,13 +626,13 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     in the cache as well as the symbol associated to the term. *)
 let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
   let name = get_basename path in
-  let sy =
+  let name =
     begin match DStd.Tag.get tags DE.Tags.ac with
-      | Some () -> Sy.name ~kind:Sy.Ac name
-      | _ -> Sy.name name
+      | Some () -> Sy.Name.mk ~kind:Sy.Ac name
+      | _ -> Sy.Name.mk name
     end
   in
-  Cache.store_sy tcst sy;
+  Cache.store_sy tcst (Sy.Name name);
   (* Adding polymorphic types to the cache. *)
   Cache.store_ty_vars id_ty;
   let arg_tys, ret_ty =
@@ -642,7 +641,7 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
       List.map dty_to_ty arg_tys, dty_to_ty ret_ty
     | _ -> [], dty_to_ty id_ty
   in
-  (Hstring.make name, arg_tys, ret_ty)
+  (name, arg_tys, ret_ty)
 
 (** Handles the definitions of a list of mutually recursive types.
     - If one of the types is an ADT, the ADTs that have only one case are

src/lib/frontend/d_cnf.mli

@@ -48,6 +48,14 @@ val make_form :
   decl_kind:Expr.decl_kind ->
   Expr.t
 
+val mk_expr :
+  ?loc:Loc.t ->
+  ?name_base:string ->
+  ?toplevel:bool ->
+  decl_kind:Expr.decl_kind ->
+  Dolmen.Std.Expr.term ->
+  Expr.t
+
 val make :
   D_loop.DStd.Loc.file ->
   Commands.sat_tdecl list ->