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

Do not pass free_vars to make_context

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-11-16 21:59:48 +01:00
parent 0ccf7da89a
commit 5a5003b22d
5 changed files with 7 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
compiler/verification/io.ml
View File

@ -24,7 +24,7 @@ module type Backend = sig
type backend_context
val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> backend_context
type vc_encoding
@ -46,7 +46,7 @@ module type BackendIO = sig
type backend_context
val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> backend_context
type vc_encoding

6
compiler/verification/io.mli
View File

@ -24,8 +24,7 @@ module type Backend = sig
type backend_context
val make_context :
decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> backend_context
type vc_encoding
@ -47,8 +46,7 @@ module type BackendIO = sig
type backend_context
val make_context :
decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> backend_context
type vc_encoding

3
compiler/verification/solver.ml
View File

@ -30,8 +30,7 @@ let solve_vc
try
let ctx, z3_vc =
Z3backend.Io.translate_expr
(Z3backend.Io.make_context decl_ctx
vc.Conditions.vc_free_vars_typ)
(Z3backend.Io.make_context decl_ctx)
vc.Conditions.vc_guard
in
Z3backend.Io.Success (z3_vc, ctx)

2
compiler/verification/z3backend.dummy.ml
View File

@ -27,7 +27,7 @@ module Io = struct
type backend_context = unit
let make_context _ _ = dummy ()
let make_context _ = dummy ()
type vc_encoding = unit

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

@ -814,9 +814,7 @@ module Backend = struct
let init_backend () =
Cli.debug_print "Running Z3 version %s" Version.to_string
let make_context
(decl_ctx : decl_ctx)
(free_vars_typ : (typed expr, typ) Var.Map.t) : backend_context =
let make_context (decl_ctx : decl_ctx) : backend_context =
let cfg =
(if !Cli.disable_counterexamples then [] else ["model", "true"])
@ ["proof", "false"]