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

[Z3backend] Add support for EInj nodes

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-03-16 12:00:19 +01:00
parent e3f3704be9
commit b00d270df7
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -698,7 +698,15 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr
let accessor = List.nth accessors idx in
let ctx, s = translate_expr ctx s in
(ctx, Expr.mk_app ctx.ctx_z3 accessor [ s ])
| EInj _ -> failwith "[Z3 encoding] EInj unsupported"
| EInj (e, idx, en, _tys) ->
(* This node corresponds to creating a value for the enumeration [en], by
calling the [idx]-th constructor of enum [en], with argument [e] *)
let ctx, z3_enum = find_or_create_enum ctx en in
let ctx, z3_arg = translate_expr ctx e in
let ctrs = Datatype.get_constructors z3_enum in
(* This should always succeed if the expression is well-typed in dcalc *)
let ctr = List.nth ctrs idx in
(ctx, Expr.mk_app ctx.ctx_z3 ctr [ z3_arg ])
| EMatch (arg, arms, enum) ->
let ctx, z3_enum = find_or_create_enum ctx enum in
let ctx, z3_arg = translate_expr ctx arg in