From b00d270df7ff92c9ac715ecc4b93b1137b484b72 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Mar 2022 12:00:19 +0100 Subject: [PATCH] [Z3backend] Add support for EInj nodes --- compiler/verification/z3backend.real.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 6ac6dc5b..c1d3b5be 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -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