Skip to content

Support get-value statement #1032

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Halbaroth wants to merge 3 commits into
base: next
Choose a base branch
from
Open

Support get-value statement #1032

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7a1e91b
Keep partial models in with a separate key
Halbaroth Jan 17, 2024
bfaf336
remove dune.inc
Halbaroth Aug 16, 2024
34949ec
Disable verify models if we use optimize values
Halbaroth Aug 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,9 @@
* Require dolmen 0.9 #1050
* Test compatibility for OCaml 5.2 #1059

### New features
* support for the SMT-LIB statement `get-value`

## v2.5.2

### Bug fixes
Expand Down
19 changes: 16 additions & 3 deletions src/bin/common/parse_command.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -420,7 +420,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation

let mk_output_opt
interpretation 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
Expand Down Expand Up @@ -901,7 +901,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. \
Expand All @@ -926,13 +926,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 =
Expand Down Expand Up @@ -982,6 +990,7 @@ let parse_output_opt =
),
dump_models,
dump_models_on,
verify_models,
frontend
in

Expand Down Expand Up @@ -1135,6 +1144,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 ignore $ frontend)
in
Expand All @@ -1143,7 +1156,7 @@ let parse_output_opt =
interpretation $
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
))

Expand Down
143 changes: 98 additions & 45 deletions src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,6 @@ let is_solver_ctx_empty = function
{ ctx = []; local = []; global = [] } -> true
| _ -> false

type 'a sat_module = (module Sat_solver_sig.S with type t = 'a)

let empty_solver_ctx = {
ctx = [];
local = [];
Expand Down Expand Up @@ -99,6 +97,24 @@ let cmd_on_modes st modes cmd =
Errors.forbidden_command curr_mode cmd
| _ -> ()

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] *)
Expand All @@ -117,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
Expand Down Expand Up @@ -181,6 +197,12 @@ let process_source ?selector_inst ~print_status src =
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 ->
Expand All @@ -194,6 +216,12 @@ let process_source ?selector_inst ~print_status src =
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
Expand All @@ -209,7 +237,7 @@ let process_source ?selector_inst ~print_status src =
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 =
Expand Down Expand Up @@ -511,6 +539,12 @@ let process_source ?selector_inst ~print_status src =
| 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
Expand Down Expand Up @@ -632,45 +666,44 @@ let process_source ?selector_inst ~print_status src =
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)
[]
(Translate.dty_to_ty term.DStd.Expr.term_ty)
let dl_to_ael dloc_file (compact_loc: DStd.Loc.t) =
DStd.Loc.(lexing_positions (loc dloc_file compact_loc))
in

let handle_get_value loc ~get_value l =
let l =
List.map (Translate.mk_expr ~loc ~toplevel:false ~decl_kind:Daxiom) l
in
match get_value simple_form with
| Some v -> Fmt.to_to_string Expr.print v
| None -> "unknown"
in

let print_terms_assignments =
Fmt.list
~sep:Fmt.cut
(fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v)
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)
[]
match get_value l with
| Some values ->
Printer.print_std
"(@[<v 0>%a@])@,"
Fmt.(iter ~sep:cut My_list.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_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) []
(Translate.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 My_list.iter_pair
((pair ~sep:sp string Sat_solver_util.pp_lbool) |> parens))
(names, values)
in

let handle_stmt :
Expand Down Expand Up @@ -763,11 +796,12 @@ let process_source ?selector_inst ~print_status src =
| {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."
Expand Down Expand Up @@ -811,9 +845,10 @@ let process_source ?selector_inst ~print_status src =
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; \
Expand All @@ -826,6 +861,24 @@ let process_source ?selector_inst ~print_status src =
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

Expand Down
3 changes: 2 additions & 1 deletion src/lib/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,8 @@
Instances IntervalCalculus Intervals_intf Intervals_core 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 Domains Domains_intf Rel_utils Bitlist
Sig Sat_solver_util Sig_rel Theory Uf Use Domains Domains_intf
Rel_utils Bitlist
; structures
Commands Errors Explanation Fpa_rounding
Profiling Satml_types Symbols
Expand Down
23 changes: 12 additions & 11 deletions src/lib/frontend/frontend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,18 +290,19 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
});
Errors.run_error Errors.Failed_check_unsat_core
with
| SAT.Unsat _ -> ()
| (SAT.Sat | SAT.I_dont_know) as e -> raise e
| Sat_solver_sig.Unsat _ -> ()
| (Sat_solver_sig.Sat | Sat_solver_sig.I_dont_know) as e -> raise e

let mk_root_dep name f loc =
if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
else Ex.empty

let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
let internal_decl ?(loc = Loc.dummy) (name : Symbols.typed_name)
(env : env) : unit =
ignore loc;
match env.res with
| `Sat | `Unknown ->
SAT.declare env.sat_env id
SAT.declare env.sat_env name
| `Unsat -> ()

let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
Expand Down Expand Up @@ -415,11 +416,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct

let handle_sat_exn f ?loc x env =
try f ?loc x env with
| SAT.Sat -> env.res <- `Sat
| SAT.Unsat expl ->
| Sat_solver_sig.Sat -> env.res <- `Sat
| Sat_solver_sig.Unsat expl ->
env.res <- `Unsat;
env.expl <- Ex.union expl env.expl
| SAT.I_dont_know ->
| Sat_solver_sig.I_dont_know ->
env.res <- `Unknown

(* Wraps the function f to check if the step limit is reached (in which case,
Expand Down Expand Up @@ -457,7 +458,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
(* If we have reached an unknown state, we can return it right
away. *)
match SAT.get_unknown_reason env.sat_env with
| Some (Step_limit _ | Timeout _) -> raise SAT.I_dont_know
| Some (Step_limit _ | Timeout _) -> raise Sat_solver_sig.I_dont_know
| Some _ ->
(* For now, only the step limit is an unknown step reachable
here. We could raise SAT.I_dont_know as in the previous case,
Expand All @@ -475,13 +476,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
| Optimize fn ->
check_if_over (internal_optimize ~loc:d.st_loc fn) env
with
| SAT.Sat ->
| Sat_solver_sig.Sat ->
(* This case should mainly occur when a query has a non-unsat result,
so we want to print the status in this case. *)
hook_on_status (Sat d) (Steps.get_steps ());
env.res <- `Sat

| SAT.Unsat expl' ->
| Sat_solver_sig.Unsat expl' ->
(* This case should mainly occur when a new assumption results in an unsat
env, in which case we do not want to print status, since the correct
status should be printed at the next query. *)
Expand All @@ -491,7 +492,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
env.res <- `Unsat;
env.expl <- expl

| SAT.I_dont_know ->
| Sat_solver_sig.I_dont_know ->
(* TODO: always print Unknown for why3 ? *)
let ur = SAT.get_unknown_reason env.sat_env in
let status =
Expand Down
Loading