CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

[Z3backend]: Do not crash when trying to print function model

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-02-18 00:34:42 +01:00
parent 6dec7bfe04
commit dd05e4468b
1 changed files with 15 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
compiler/verification/z3backend.ml
View File

@ -178,7 +178,7 @@ let print_model (ctx : context) (model : Model.model) : string =
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
(fun fmt d ->
if FuncDecl.get_arity d = 0 then begin
if FuncDecl.get_arity d = 0 then
(* Constant case *)
match Model.get_const_interp model d with
(* TODO: Better handling of this case *)
@ -187,13 +187,24 @@ let print_model (ctx : context) (model : Model.model) : string =
| Some e ->
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Cli.error_print "testbis\n";
Format.fprintf fmt "%s %s : %s"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
end
else failwith "[Z3 model]: Printing of functions is not yet supported"))
else
(* Declaration d is a function *)
match Model.get_func_interp model d with
(* TODO: Better handling of this case *)
| None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
(* Print "name : value\n" *)
| Some f ->
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(* TODO: Model of a Z3 function should be pretty-printed *)
(Model.FuncInterp.to_string f)))
decls
(** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)