CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Add support for let_in in Z3 backend

Browse Source
This commit is contained in:
Aymeric Fromherz 2023-03-28 12:48:44 +09:00
parent 69be2f6ed8
commit 082caae498
2 changed files with 9 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
compiler/verification/.z3backend.real.ml.swp Normal file
View File

Binary file not shown.

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

@ -742,6 +742,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
| EArray _ -> failwith "[Z3 encoding] EArray unsupported"
| ELit l -> ctx, translate_lit ctx l
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
| EApp { f = head; args = [] } -> failwith "[Z3 encoding] let in"
| EApp { f = head; args } -> (
match Marked.unmark head with
| EOp { op; _ } -> translate_op ctx op args
@ -758,6 +759,14 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
args (ctx, [])
in
ctx, Expr.mk_app ctx.ctx_z3 fd z3_args
| EAbs { binder; _ } ->
let vars, body = Bindlib.unmbind binder in
if Array.length vars != 1 || List.length args != 1 then
failwith "[Z3 encoding] EAbs not supported beyond let_in"
else
let arg = List.hd args in
let expr = Bindlib.msubst binder [| Marked.unmark arg |] in
translate_expr ctx expr
| _ ->
failwith
"[Z3 encoding] EApp node: Catala function calls should only include \