mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-09 11:37:35 +03:00
Error message pretty-printing and sat solving example [skip ci]
This commit is contained in:
Denis Merigoux
parent
c0a8362fd9
commit
bf444f548f
@ -61,21 +61,26 @@ let unique_name (v : Var.t) : string =
|
||||
lost during the translation (e.g., by translating a date to an integer) **)
|
||||
let print_model (ctx : context) (model : Model.model) : string =
|
||||
let decls = Model.get_decls model in
|
||||
List.fold_left
|
||||
(fun acc d ->
|
||||
match Model.get_const_interp model d with
|
||||
(* TODO: Better handling of this case *)
|
||||
| None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
|
||||
(* Prints "name : value\n" *)
|
||||
| Some e ->
|
||||
if FuncDecl.get_arity d = 0 then
|
||||
(* Constant case *)
|
||||
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
|
||||
let v = StringMap.find symbol_name ctx.ctx_z3vars in
|
||||
(* TODO: Needs a better parsing of the value once we have more than integer types *)
|
||||
Format.asprintf " %s : %s\n%s" (Bindlib.name_of v) (Expr.to_string e) acc
|
||||
else failwith "[Z3 model]: Printing of functions is not yet supported")
|
||||
"" decls
|
||||
Format.asprintf "%a"
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n")
|
||||
(fun fmt d ->
|
||||
match Model.get_const_interp model d with
|
||||
(* TODO: Better handling of this case *)
|
||||
| None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution"
|
||||
(* Prints "name : value\n" *)
|
||||
| Some e ->
|
||||
if FuncDecl.get_arity d = 0 then
|
||||
(* Constant case *)
|
||||
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
|
||||
let v = StringMap.find symbol_name ctx.ctx_z3vars in
|
||||
(* TODO: Needs a better parsing of the value once we have more than integer types *)
|
||||
Format.fprintf fmt "%s %s : %s"
|
||||
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
|
||||
(Expr.to_string e)
|
||||
else failwith "[Z3 model]: Printing of functions is not yet supported"))
|
||||
decls
|
||||
|
||||
(** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)
|
||||
let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort =
|
||||
@ -272,30 +277,43 @@ type vc_encoding_result = Success of context * Expr.expr | Fail of string
|
||||
let print_positive_result (vc : Conditions.verification_condition) : string =
|
||||
match vc.Conditions.vc_kind with
|
||||
| Conditions.NoEmptyError ->
|
||||
Format.asprintf "%s: this variable never returns an empty error"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s"
|
||||
Format.asprintf "%s This variable never returns an empty error"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
| Conditions.NoOverlappingExceptions ->
|
||||
Format.asprintf "%s: no two exceptions to ever overlap for this variable"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s"
|
||||
Format.asprintf "%s No two exceptions to ever overlap for this variable"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
|
||||
let print_negative_result (vc : Conditions.verification_condition) : string =
|
||||
match vc.Conditions.vc_kind with
|
||||
| Conditions.NoEmptyError ->
|
||||
Format.asprintf "%s: this variable might return an empty error\n%s"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
|
||||
| Conditions.NoOverlappingExceptions ->
|
||||
Format.asprintf "%s: at least two exceptions overlap for this variable\n%s"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
|
||||
let print_negative_result (vc : Conditions.verification_condition) (ctx : context)
|
||||
(solver : Solver.solver) : string =
|
||||
let var_and_pos =
|
||||
match vc.Conditions.vc_kind with
|
||||
| Conditions.NoEmptyError ->
|
||||
Format.asprintf "%s This variable might return an empty error:\n%s"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
|
||||
| Conditions.NoOverlappingExceptions ->
|
||||
Format.asprintf "%s At least two exceptions overlap for this variable:\n%s"
|
||||
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
|
||||
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
|
||||
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
|
||||
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
|
||||
in
|
||||
let counterexample =
|
||||
match Solver.get_model solver with
|
||||
| None ->
|
||||
"The solver did not manage to generate a counterexample to explain the faulty behavior."
|
||||
| Some model ->
|
||||
Format.asprintf
|
||||
"The solver generated the following counterexample to explain the faulty behavior:\n%s"
|
||||
(print_model ctx model)
|
||||
in
|
||||
var_and_pos ^ "\n" ^ counterexample
|
||||
|
||||
(** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the expression [vc] **)
|
||||
let encode_and_check_vc (decl_ctx : decl_ctx) (z3_ctx : Z3.context)
|
||||
@ -324,15 +342,9 @@ let encode_and_check_vc (decl_ctx : decl_ctx) (z3_ctx : Z3.context)
|
||||
Solver.add solver [ Boolean.mk_not z3_ctx z3_vc ];
|
||||
|
||||
if Solver.check solver [] = UNSATISFIABLE then Cli.result_print (print_positive_result vc)
|
||||
else (
|
||||
else
|
||||
(* TODO: Print model as error message for Catala debugging purposes *)
|
||||
Cli.error_print (print_negative_result vc);
|
||||
match Solver.get_model solver with
|
||||
| None -> Cli.error_print "Z3 did not manage to generate a counterexample"
|
||||
| Some model ->
|
||||
Cli.error_print
|
||||
(Format.asprintf "Z3 generated the following counterexample:\n%s"
|
||||
(print_model ctx model)))
|
||||
Cli.error_print (print_negative_result vc ctx solver)
|
||||
| Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg)
|
||||
|
||||
(** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs]
|
||||
|
||||
@ -1,12 +1,11 @@
|
||||
[ERROR] A.y: at least two exceptions overlap for this variable
|
||||
[ERROR] [A.y] At least two exceptions overlap for this variable:
|
||||
--> tests/test_proof/bad/no_vars-conflict.catala_en
|
||||
|
|
||||
8 | context y content integer
|
||||
| ^
|
||||
+ Test
|
||||
[ERROR] Z3 generated the following counterexample:
|
||||
x : 0
|
||||
|
||||
[RESULT] A.y: this variable never returns an empty error
|
||||
[RESULT] A.x: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.x: this variable never returns an empty error
|
||||
The solver generated the following counterexample to explain the faulty behavior:
|
||||
--> x : 0
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
|
||||
@ -1,12 +1,11 @@
|
||||
[RESULT] A.y: no two exceptions to ever overlap for this variable
|
||||
[ERROR] A.y: this variable might return an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.y] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/no_vars-empty.catala_en
|
||||
|
|
||||
7 | context y content integer
|
||||
| ^
|
||||
+ Test
|
||||
[ERROR] Z3 generated the following counterexample:
|
||||
x : 1
|
||||
|
||||
[RESULT] A.x: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.x: this variable never returns an empty error
|
||||
The solver generated the following counterexample to explain the faulty behavior:
|
||||
--> x : 1
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
|
||||
35
tests/test_proof/bad/output/sat_solving.catala_en.Proof
Normal file
35
tests/test_proof/bad/output/sat_solving.catala_en.Proof
Normal file
@ -0,0 +1,35 @@
|
||||
[RESULT] [A.x10] No two exceptions to ever overlap for this variable
|
||||
[ERROR] [A.x10] This variable might return an empty error:
|
||||
--> tests/test_proof/bad/sat_solving.catala_en
|
||||
|
|
||||
15 | context x10 content boolean
|
||||
| ^^^
|
||||
+ Test
|
||||
The solver generated the following counterexample to explain the faulty behavior:
|
||||
--> x6 : false
|
||||
--> x8 : false
|
||||
--> x5 : false
|
||||
--> x2 : true
|
||||
--> x1 : true
|
||||
--> x9 : false
|
||||
--> x3 : true
|
||||
--> x7 : true
|
||||
--> x4 : true
|
||||
[RESULT] [A.x9] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x9] This variable never returns an empty error
|
||||
[RESULT] [A.x8] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x8] This variable never returns an empty error
|
||||
[RESULT] [A.x7] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x7] This variable never returns an empty error
|
||||
[RESULT] [A.x6] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x6] This variable never returns an empty error
|
||||
[RESULT] [A.x5] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x5] This variable never returns an empty error
|
||||
[RESULT] [A.x4] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x4] This variable never returns an empty error
|
||||
[RESULT] [A.x3] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x3] This variable never returns an empty error
|
||||
[RESULT] [A.x2] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x2] This variable never returns an empty error
|
||||
[RESULT] [A.x1] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x1] This variable never returns an empty error
|
||||
39
tests/test_proof/bad/sat_solving.catala_en
Normal file
39
tests/test_proof/bad/sat_solving.catala_en
Normal file
@ -0,0 +1,39 @@
|
||||
## Test
|
||||
|
||||
|
||||
```catala
|
||||
declaration scope A:
|
||||
context x1 content boolean
|
||||
context x2 content boolean
|
||||
context x3 content boolean
|
||||
context x4 content boolean
|
||||
context x5 content boolean
|
||||
context x6 content boolean
|
||||
context x7 content boolean
|
||||
context x8 content boolean
|
||||
context x9 content boolean
|
||||
context x10 content boolean
|
||||
|
||||
scope A:
|
||||
definition x1 equals true
|
||||
definition x2 equals false
|
||||
definition x3 equals true
|
||||
definition x4 equals false
|
||||
definition x5 equals true
|
||||
definition x6 equals false
|
||||
definition x7 equals true
|
||||
definition x8 equals false
|
||||
definition x9 equals true
|
||||
definition x10 under condition
|
||||
(x1 or x2 or x3 or x4 or x5)
|
||||
and (not x1 or not x2 or not x3 or not x4 or not x5)
|
||||
and (x1 or not x2)
|
||||
and (x3 or not x4 or x5)
|
||||
and (x5)
|
||||
and (not x1 or x2)
|
||||
and (x6 or not x7 or x8 or not x1)
|
||||
and (x2 or not x4 or x5 or not x6)
|
||||
and (x7 or x8 or x9 or not x2)
|
||||
consequence equals false
|
||||
|
||||
```
|
||||
@ -1,4 +1,4 @@
|
||||
[RESULT] A.z: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.z: this variable never returns an empty error
|
||||
[RESULT] A.x: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.x: this variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
|
||||
@ -1,2 +1,2 @@
|
||||
[RESULT] A.x: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.x: this variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
[RESULT] A.z: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.z: this variable never returns an empty error
|
||||
[RESULT] A.x: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.x: this variable never returns an empty error
|
||||
[RESULT] A.y: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.y: this variable never returns an empty error
|
||||
[RESULT] [A.z] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.z] This variable never returns an empty error
|
||||
[RESULT] [A.x] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.x] This variable never returns an empty error
|
||||
[RESULT] [A.y] No two exceptions to ever overlap for this variable
|
||||
[RESULT] [A.y] This variable never returns an empty error
|
||||
|
||||
Loading…
Reference in New Issue
Block a user