Skip to content
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

Jump to bottom

Proof platform: Better error message when Z3 encoding not supported, and extend GetYear support #227

Merged
merged 2 commits into from
Mar 15, 2022
Merged

Proof platform: Better error message when Z3 encoding not supported, and extend GetYear support #227

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d760d88
[Z3encoding] Print variable name when encoding is not supported
R1kM Mar 15, 2022
4b1ace2
[Z3Backend] Support GetYear equality comparison
R1kM Mar 15, 2022
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
4 changes: 3 additions & 1 deletion compiler/lcalc/ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,9 @@ let make_matchopt_with_abs_arms
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox arg in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some [@ocamlformat "disable"] in
let+ arg = arg
and+ e_none = e_none
and+ e_some = e_some [@ocamlformat "disable"] in

mark @@ EMatch (arg, [ e_none; e_some ], option_enum)

Expand Down
7 changes: 6 additions & 1 deletion compiler/verification/io.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,5 +179,10 @@ module MakeBackendIO (B : Backend) = struct
Cli.error_print "%s" (print_negative_result vc backend_ctx model)
| Unknown ->
failwith "The solver failed at proving or disproving the VC")
| Fail msg -> Cli.error_print "The translation to Z3 failed:@\n%s" msg
| Fail msg ->
Cli.error_print "%s The translation to Z3 failed:\n%s"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
msg
end
18 changes: 18 additions & 0 deletions compiler/verification/z3backend.real.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -475,6 +475,24 @@ let rec translate_op
thus be directly translated as >= in the Z3 encoding using the
number of days *)
(ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2)
| Eq, [ (EApp ((EOp (Unop GetYear), _), [ e1 ]), _); (ELit (LInt n), _) ]
->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let min_date =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
(date_to_int (date_of_year n))
in
let max_date =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
(date_to_int (date_of_year (n + 1)))
in
( ctx,
Boolean.mk_and ctx.ctx_z3
[
Arithmetic.mk_ge ctx.ctx_z3 e1 min_date;
Arithmetic.mk_lt ctx.ctx_z3 e1 max_date;
] )
| _ -> (
let ctx, e1, e2 =
match args with
Expand Down