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

Port verification code to the AST changes

Browse Source
This commit is contained in:
Louis Gesbert 2022-07-06 10:08:27 +02:00
parent 5f882e35a2
commit 18e86621d5
9 changed files with 75 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/dcalc/ast.ml
View File

@ -439,6 +439,8 @@ module Var = struct
let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)
let compare (V x) (V y) = Bindlib.compare_vars x y
let eq (V x) (V y) = Bindlib.eq_vars x y
end
module VarSet = Set.Make (Var)

1
compiler/dcalc/ast.mli
View File

@ -418,6 +418,7 @@ module Var : sig
val t: 'm expr Bindlib.var -> t
val get: t -> 'm expr Bindlib.var
val compare : t -> t -> int
val eq : t -> t -> bool
end
module VarMap : Map.S with type key = Var.t

64
compiler/verification/conditions.ml
View File

@ -21,7 +21,7 @@ open Ast
(** {1 Helpers and type definitions}*)
type vc_return = expr Marked.pos * typ Marked.pos VarMap.t
type 'm vc_return = 'm marked_expr * typ Marked.pos VarMap.t
(** The return type of VC generators is the VC expression plus the types of any
locally free variable inside that expression. *)
@ -32,30 +32,30 @@ type ctx = {
scope_variables_typs : typ Marked.pos VarMap.t;
}
let conjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let conjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return =
let acc, list =
match args with
| hd :: tl -> hd, tl
| [] -> ((ELit (LBool true), pos), VarMap.empty), []
| [] -> ((ELit (LBool true), mark), VarMap.empty), []
in
List.fold_left
(fun (acc, acc_ty) (arg, arg_ty) ->
( (EApp ((EOp (Binop And), pos), [arg; acc]), pos),
( (EApp ((EOp (Binop And), mark), [arg; acc]), mark),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
let negation ((arg, arg_ty) : vc_return) (pos : Pos.t) : vc_return =
(EApp ((EOp (Unop Not), pos), [arg]), pos), arg_ty
let negation ((arg, arg_ty) : 'm vc_return) (mark : 'm mark) : 'm vc_return =
(EApp ((EOp (Unop Not), mark), [arg]), mark), arg_ty
let disjunction (args : vc_return list) (pos : Pos.t) : vc_return =
let disjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return =
let acc, list =
match args with
| hd :: tl -> hd, tl
| [] -> ((ELit (LBool false), pos), VarMap.empty), []
| [] -> ((ELit (LBool false), mark), VarMap.empty), []
in
List.fold_left
(fun ((acc, acc_ty) : vc_return) (arg, arg_ty) ->
( (EApp ((EOp (Binop Or), pos), [arg; acc]), pos),
(fun ((acc, acc_ty) : 'm vc_return) (arg, arg_ty) ->
( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark),
VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty ))
acc list
@ -71,8 +71,8 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
variables, or [fun () -> e1] for subscope variables. But what we really want
to analyze is only [e1], so we match this outermost structure explicitely
and have a clean verification condition generator that only runs on [e1] *)
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) :
expr Marked.pos =
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : 'm marked_expr) :
'm marked_expr =
match Marked.unmark e with
| ErrorOnEmpty
( EDefault
@ -80,7 +80,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) :
(ELit (LBool true), _),
cons ),
_ )
when List.exists (fun x' -> Bindlib.eq_vars x x') ctx.input_vars ->
when List.exists (fun x' -> Var.eq (Var.t x) x') ctx.input_vars ->
(* scope variables*)
cons
| EAbs (binder, [(TLit TUnit, _)]) ->
@ -90,7 +90,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) :
| ErrorOnEmpty d ->
d (* input subscope variables and non-input scope variable *)
| _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (pos e)
"Internal error: this expression does not have the structure expected by \
the VC generator:\n\
%a"
@ -103,8 +103,8 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) :
[b] such that if [b] is true, then [e] will never return an empty error. It
also returns a map of all the types of locally free variables inside the
expression. *)
let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) :
vc_return =
let rec generate_vc_must_not_return_empty (ctx : ctx) (e : 'm marked_expr) :
'm vc_return =
let out =
match Marked.unmark e with
| ETuple (args, _) | EArray args ->
@ -130,7 +130,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) :
in
( vc_body_expr,
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
(fun acc (var, ty) -> VarMap.add (Var.t var) ty acc)
vc_body_ty
(List.map2 (fun x y -> x, y) (Array.to_list vars) typs) )
| EApp (f, args) ->
@ -197,8 +197,8 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) :
[b] such that if [b] is true, then [e] will never return a conflict error.
It also returns a map of all the types of locally free variables inside the
expression. *)
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) :
vc_return =
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : 'm marked_expr) :
'm vc_return =
let out =
(* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this
function relies on. *)
@ -223,7 +223,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) :
in
( vc_body_expr,
List.fold_left
(fun acc (var, ty) -> VarMap.add var ty acc)
(fun acc (var, ty) -> VarMap.add (Var.t var) ty acc)
vc_body_ty
(List.map2 (fun x y -> x, y) (Array.to_list vars) typs) )
| EApp (f, args) ->
@ -279,8 +279,8 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) :
type verification_condition_kind = NoEmptyError | NoOverlappingExceptions
type verification_condition = {
vc_guard : expr Marked.pos;
type 'm verification_condition = {
vc_guard : 'm marked_expr;
(* should have type bool *)
vc_kind : verification_condition_kind;
vc_scope : ScopeName.t;
@ -290,7 +290,7 @@ type verification_condition = {
let rec generate_verification_conditions_scope_body_expr
(ctx : ctx)
(scope_body_expr : expr scope_body_expr) : ctx * verification_condition list
(scope_body_expr : ('m expr, 'm) scope_body_expr) : ctx * 'm verification_condition list
=
match scope_body_expr with
| Result _ -> ctx, []
@ -301,7 +301,7 @@ let rec generate_verification_conditions_scope_body_expr
let new_ctx, vc_list =
match scope_let.scope_let_kind with
| DestructuringInputStruct ->
{ ctx with input_vars = scope_let_var :: ctx.input_vars }, []
{ ctx with input_vars = Var.t scope_let_var :: ctx.input_vars }, []
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never evaluate to
emptyError nor conflictError. But for subscope variable definitions,
@ -328,7 +328,7 @@ let rec generate_verification_conditions_scope_body_expr
(fun _ _ -> failwith "should not happen")
ctx.scope_variables_typs vc_confl_typs;
vc_scope = ctx.current_scope_name;
vc_variable = scope_let_var, scope_let.scope_let_pos;
vc_variable = Var.t scope_let_var, scope_let.scope_let_pos;
};
]
in
@ -351,7 +351,7 @@ let rec generate_verification_conditions_scope_body_expr
(fun _ _ -> failwith "should not happen")
ctx.scope_variables_typs vc_empty_typs;
vc_scope = ctx.current_scope_name;
vc_variable = scope_let_var, scope_let.scope_let_pos;
vc_variable = Var.t scope_let_var, scope_let.scope_let_pos;
}
:: vc_list
| _ -> vc_list
@ -364,7 +364,7 @@ let rec generate_verification_conditions_scope_body_expr
{
new_ctx with
scope_variables_typs =
VarMap.add scope_let_var scope_let.scope_let_typ
VarMap.add (Var.t scope_let_var) scope_let.scope_let_typ
new_ctx.scope_variables_typs;
}
scope_let_next
@ -373,8 +373,8 @@ let rec generate_verification_conditions_scope_body_expr
let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx)
(scopes : expr scopes)
(s : ScopeName.t option) : verification_condition list =
(scopes : ('m expr, 'm) scopes)
(s : ScopeName.t option) : 'm verification_condition list =
match scopes with
| Nil -> []
| ScopeDef scope_def ->
@ -413,8 +413,8 @@ let rec generate_verification_conditions_scopes
generate_verification_conditions_scopes decl_ctx next s @ vcs
let generate_verification_conditions
(p : program)
(s : Dcalc.Ast.ScopeName.t option) : verification_condition list =
(p : 'm program)
(s : Dcalc.Ast.ScopeName.t option) : 'm verification_condition list =
let vcs = generate_verification_conditions_scopes p.decl_ctx p.scopes s in
(* We sort this list by scope name and then variable name to ensure consistent
output for testing*)
@ -423,7 +423,7 @@ let generate_verification_conditions
let to_str vc =
Format.asprintf "%s.%s"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Marked.unmark vc.vc_variable))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))
in
String.compare (to_str vc1) (to_str vc2))
vcs

6
compiler/verification/conditions.mli
View File

@ -25,8 +25,8 @@ type verification_condition_kind =
(** This verification condition checks whether a definition never returns
a conflict error *)
type verification_condition = {
vc_guard : Dcalc.Ast.typed_expr;
type 'm verification_condition = {
vc_guard : 'm Dcalc.Ast.marked_expr;
(** This expression should have type [bool]*)
vc_kind : verification_condition_kind;
vc_scope : Dcalc.Ast.ScopeName.t;
@ -40,7 +40,7 @@ type verification_condition = {
val generate_verification_conditions :
'm Dcalc.Ast.program ->
Dcalc.Ast.ScopeName.t option ->
verification_condition list
'm verification_condition list
(** [generate_verification_conditions p None] will generate the verification
conditions for all the variables of all the scopes of the program [p], while
[generate_verification_conditions p (Some s)] will focus only on the

28
compiler/verification/io.ml
View File

@ -38,7 +38,7 @@ module type Backend = sig
val translate_expr :
backend_context ->
Dcalc.Ast.expr Utils.Marked.pos ->
'm Dcalc.Ast.marked_expr ->
backend_context * vc_encoding
end
@ -53,7 +53,7 @@ module type BackendIO = sig
val translate_expr :
backend_context ->
Dcalc.Ast.expr Utils.Marked.pos ->
'm Dcalc.Ast.marked_expr ->
backend_context * vc_encoding
type model
@ -62,17 +62,17 @@ module type BackendIO = sig
| Success of vc_encoding * backend_context
| Fail of string
val print_positive_result : Conditions.verification_condition -> string
val print_positive_result : 'm Conditions.verification_condition -> string
val print_negative_result :
Conditions.verification_condition ->
'm Conditions.verification_condition ->
backend_context ->
model option ->
string
val encode_and_check_vc :
Dcalc.Ast.decl_ctx ->
Conditions.verification_condition * vc_encoding_result ->
'm Conditions.verification_condition * vc_encoding_result ->
unit
end
@ -93,21 +93,21 @@ module MakeBackendIO (B : Backend) = struct
| Success of B.vc_encoding * B.backend_context
| Fail of string
let print_positive_result (vc : Conditions.verification_condition) : string =
let print_positive_result (vc : 'm Conditions.verification_condition) : string =
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Marked.unmark vc.vc_variable)))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s No two exceptions to ever overlap for this variable"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Marked.unmark vc.vc_variable)))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
let print_negative_result
(vc : Conditions.verification_condition)
(vc : 'm Conditions.verification_condition)
(ctx : B.backend_context)
(model : B.model option) : string =
let var_and_pos =
@ -116,14 +116,14 @@ module MakeBackendIO (B : Backend) = struct
Format.asprintf "%s This variable might return an empty error:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Marked.unmark vc.vc_variable)))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
(Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable))
| Conditions.NoOverlappingExceptions ->
Format.asprintf
"%s At least two exceptions overlap for this variable:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Marked.unmark vc.vc_variable)))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
(Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable))
in
let counterexample : string option =
@ -155,11 +155,11 @@ module MakeBackendIO (B : Backend) = struct
expression [vc] **)
let encode_and_check_vc
(decl_ctx : decl_ctx)
(vc : Conditions.verification_condition * vc_encoding_result) : unit =
(vc : 'm Conditions.verification_condition * vc_encoding_result) : unit =
let vc, z3_vc = vc in
Cli.debug_print "For this variable:\n%s\n"
(Pos.retrieve_loc_text (Marked.get_mark vc.Conditions.vc_guard));
(Pos.retrieve_loc_text (pos vc.Conditions.vc_guard));
Cli.debug_format "This verification condition was generated for %a:@\n%a"
(Cli.format_with_style [ANSITerminal.yellow])
(match vc.vc_kind with
@ -182,6 +182,6 @@ module MakeBackendIO (B : Backend) = struct
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 (Marked.unmark vc.vc_variable)))
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
msg
end

10
compiler/verification/io.mli
View File

@ -39,7 +39,7 @@ module type Backend = sig
val is_model_empty : model -> bool
val translate_expr :
backend_context -> Dcalc.Ast.typed_expr -> backend_context * vc_encoding
backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding
end
module type BackendIO = sig
@ -55,7 +55,7 @@ module type BackendIO = sig
type vc_encoding
val translate_expr :
backend_context -> Dcalc.Ast.typed_expr -> backend_context * vc_encoding
backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding
type model
@ -63,17 +63,17 @@ module type BackendIO = sig
| Success of vc_encoding * backend_context
| Fail of string
val print_positive_result : Conditions.verification_condition -> string
val print_positive_result : 'm Conditions.verification_condition -> string
val print_negative_result :
Conditions.verification_condition ->
'm Conditions.verification_condition ->
backend_context ->
model option ->
string
val encode_and_check_vc :
Dcalc.Ast.decl_ctx ->
Conditions.verification_condition * vc_encoding_result ->
'm Conditions.verification_condition * vc_encoding_result ->
unit
end

2
compiler/verification/solver.ml
View File

@ -21,7 +21,7 @@ open Dcalc.Ast
discharged by Z3, and attempts to solve them **)
let solve_vc
(decl_ctx : decl_ctx)
(vcs : Conditions.verification_condition list) : unit =
(vcs : 'm Conditions.verification_condition list) : unit =
(* Right now we only use the Z3 backend but the functorial interface should
make it easy to mix and match different proof backends. *)
Z3backend.Io.init_backend ();

2
compiler/verification/solver.mli
View File

@ -17,4 +17,4 @@
(** Solves verification conditions using various proof backends *)
val solve_vc :
Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit
Dcalc.Ast.decl_ctx -> 'm Conditions.verification_condition list -> unit

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

@ -99,7 +99,7 @@ let base_day = CalendarLib.Date.make 1900 1 1
(** [unique_name] returns the full, unique name corresponding to variable [v],
as given by Bindlib **)
let unique_name (v : Var.t) : string =
let unique_name (v : 'm var) : string =
Format.asprintf "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
(** [date_to_int] translates [date] to an integer corresponding to the number of
@ -223,7 +223,7 @@ let print_model (ctx : context) (model : Model.model) : string =
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of (Var.get v)))
(print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
else
(* Declaration d is a function *)
@ -238,7 +238,7 @@ let print_model (ctx : context) (model : Model.model) : string =
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.with_style [ANSITerminal.blue] "%s" "-->")
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v))
(Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of (Var.get v)))
(* TODO: Model of a Z3 function should be pretty-printed *)
(Model.FuncInterp.to_string f)))
decls
@ -396,7 +396,7 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) :
| TArrow (t1, t2) ->
let ctx, z3_t1 = translate_typ ctx (Marked.unmark t1) in
let ctx, z3_t2 = translate_typ ctx (Marked.unmark t2) in
let name = unique_name v in
let name = unique_name (Var.get v) in
let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in
let ctx = add_funcdecl v fd ctx in
let ctx = add_z3var name v ctx in
@ -415,7 +415,7 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) :
let rec translate_op
(ctx : context)
(op : operator)
(args : expr Marked.pos list) : context * Expr.expr =
(args : 'm marked_expr list) : context * Expr.expr =
match op with
| Ternop _top ->
let _e1, _e2, _e3 =
@ -426,7 +426,7 @@ let rec translate_op
(Format.asprintf
"[Z3 encoding] Ill-formed ternary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
(EApp ((EOp op, Untyped {pos=Pos.no_pos}), (List.map untype_expr args)), Untyped {pos=Pos.no_pos}))
in
failwith "[Z3 encoding] ternary operator application not supported"
@ -514,7 +514,7 @@ let rec translate_op
(Format.asprintf
"[Z3 encoding] Ill-formed binary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
(EApp ((EOp op, Untyped{pos=Pos.no_pos}), List.map untype_expr args), Untyped{pos=Pos.no_pos}))
in
match bop with
@ -561,7 +561,7 @@ let rec translate_op
(Format.asprintf
"[Z3 encoding] Ill-formed unary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
(EApp ((EOp op, Untyped{pos=Pos.no_pos}), List.map untype_expr args), Untyped{pos=Pos.no_pos}))
in
match uop with
@ -593,12 +593,12 @@ let rec translate_op
(** [translate_expr] translate the expression [vc] to its corresponding Z3
expression **)
and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr
and translate_expr (ctx : context) (vc : 'm marked_expr) : context * Expr.expr
=
let translate_match_arm
(head : Expr.expr)
(ctx : context)
(e : expr Marked.pos * FuncDecl.func_decl list) : context * Expr.expr =
(e : 'm marked_expr * FuncDecl.func_decl list) : context * Expr.expr =
let e, accessors = e in
match Marked.unmark e with
| EAbs (e, _) ->
@ -611,7 +611,7 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr
let proj = Expr.mk_app ctx.ctx_z3 accessor [head] in
(* The fresh variable should be substituted by a projection into the enum
in the body, we add this to the context *)
let ctx = add_z3matchsubst fresh_v proj ctx in
let ctx = add_z3matchsubst (Var.t fresh_v) proj ctx in
let body = Bindlib.msubst e [| fresh_e |] in
translate_expr ctx body
@ -621,12 +621,12 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr
match Marked.unmark vc with
| EVar v -> (
match VarMap.find_opt v ctx.ctx_z3matchsubsts with
match VarMap.find_opt (Var.t v) ctx.ctx_z3matchsubsts with
| None ->
(* We are in the standard case, where this is a true Catala variable *)
let t = VarMap.find v ctx.ctx_var in
let t = VarMap.find (Var.t v) ctx.ctx_var in
let name = unique_name v in
let ctx = add_z3var name v ctx in
let ctx = add_z3var name (Var.t v) ctx in
let ctx, ty = translate_typ ctx (Marked.unmark t) in
let z3_var = Expr.mk_const_s ctx.ctx_z3 name ty in
let ctx =
@ -698,7 +698,7 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr
match Marked.unmark head with
| EOp op -> translate_op ctx op args
| EVar v ->
let ctx, fd = find_or_create_funcdecl ctx v in
let ctx, fd = find_or_create_funcdecl ctx (Var.t v) in
(* Fold_right to preserve the order of the arguments: The head argument is
appended at the head *)
let ctx, z3_args =
@ -768,7 +768,7 @@ module Backend = struct
let is_model_empty (m : model) : bool = List.length (Z3.Model.get_decls m) = 0
let translate_expr (ctx : backend_context) (e : Dcalc.Ast.expr Marked.pos) =
let translate_expr (ctx : backend_context) (e : 'm marked_expr) =
translate_expr ctx e
let init_backend () =