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

[Proof Backend] Use Z3's native encoding for ite

Browse Source
This commit is contained in:
Aymeric Fromherz 2023-04-24 12:11:55 +02:00
parent c983099e59
commit c6e478c9dd
1 changed files with 4 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
compiler/verification/z3backend.real.ml
View File

@ -772,18 +772,13 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } ->
(* Encode this as (e_if ==> e_then) /\ (not e_if ==> e_else) *)
(* We rely on Z3's native encoding for ite to encode this node. There might
be some interesting optimization in the future about when to split this
node/bubble up the if_then_else, but this is left as future work *)
let ctx, z3_if = translate_expr ctx e_if in
let ctx, z3_then = translate_expr ctx e_then in
let ctx, z3_else = translate_expr ctx e_else in
( ctx,
Boolean.mk_and ctx.ctx_z3
[
Boolean.mk_implies ctx.ctx_z3 z3_if z3_then;
Boolean.mk_implies ctx.ctx_z3
(Boolean.mk_not ctx.ctx_z3 z3_if)
z3_else;
] )
ctx, Boolean.mk_ite ctx.ctx_z3 z3_if z3_then z3_else
| EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
| _ -> .