From 260959b0883bd5f21649971b15d6c42a668070c3 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Tue, 11 Jan 2022 18:33:45 +0100 Subject: [PATCH] Formatting + correct expected tests output --- compiler/verification/z3encoding.ml | 18 ++++++++++++------ .../good/output/no_vars.catala_en.Proof | 4 ++-- .../good/output/simple_vars.catala_en.Proof | 12 ++++++------ 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/compiler/verification/z3encoding.ml b/compiler/verification/z3encoding.ml index 6adbbc55..f3eb3bf3 100644 --- a/compiler/verification/z3encoding.ml +++ b/compiler/verification/z3encoding.ml @@ -84,14 +84,18 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis | Or -> Boolean.mk_or ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ] | Xor -> Boolean.mk_xor ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) | Add KInt -> Arithmetic.mk_add ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ] - | Add _ -> failwith "[Z3 encoding] application of non-integer binary operator Add not supported" + | Add _ -> + failwith "[Z3 encoding] application of non-integer binary operator Add not supported" | Sub KInt -> Arithmetic.mk_sub ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ] - | Sub _ -> failwith "[Z3 encoding] application of non-integer binary operator Sub not supported" + | Sub _ -> + failwith "[Z3 encoding] application of non-integer binary operator Sub not supported" | Mult KInt -> Arithmetic.mk_mul ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ] - | Mult _ -> failwith "[Z3 encoding] application of non-integer binary operator Mult not supported" + | Mult _ -> + failwith "[Z3 encoding] application of non-integer binary operator Mult not supported" | Div KInt -> Arithmetic.mk_div ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) - | Div _ -> failwith "[Z3 encoding] application of non-integer binary operator Div not supported" - | Lt KInt -> Arithmetic.mk_lt ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) + | Div _ -> + failwith "[Z3 encoding] application of non-integer binary operator Div not supported" + | Lt KInt -> Arithmetic.mk_lt ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) | Lt _ -> failwith "[Z3 encoding] application of non-integer binary operator Lt not supported" | Lte _ -> failwith "[Z3 encoding] application of binary operator Lte not supported" | Gt KInt -> Arithmetic.mk_gt ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) @@ -100,7 +104,9 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis | Gte _ -> failwith "[Z3 encoding] application of non-integer binary operator Gte not supported" | Eq -> Boolean.mk_eq ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2) - | Neq -> Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2)) + | Neq -> + Boolean.mk_not ctx.ctx_z3 + (Boolean.mk_eq ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2)) | Map -> failwith "[Z3 encoding] application of binary operator Map not supported" | Concat -> failwith "[Z3 encoding] application of binary operator Concat not supported" | Filter -> failwith "[Z3 encoding] application of binary operator Filter not supported") diff --git a/tests/test_proof/good/output/no_vars.catala_en.Proof b/tests/test_proof/good/output/no_vars.catala_en.Proof index 5bfb4963..b34d7cca 100644 --- a/tests/test_proof/good/output/no_vars.catala_en.Proof +++ b/tests/test_proof/good/output/no_vars.catala_en.Proof @@ -1,5 +1,5 @@ [RESULT] For this variable: - --> test_proof/good/no_vars.catala_en + --> tests/test_proof/good/no_vars.catala_en | 5 | context x content integer | ^ @@ -31,7 +31,7 @@ true && true && (not false) true) [RESULT] For this variable: - --> test_proof/good/no_vars.catala_en + --> tests/test_proof/good/no_vars.catala_en | 5 | context x content integer | ^ diff --git a/tests/test_proof/good/output/simple_vars.catala_en.Proof b/tests/test_proof/good/output/simple_vars.catala_en.Proof index 00aff48f..9ab9d906 100644 --- a/tests/test_proof/good/output/simple_vars.catala_en.Proof +++ b/tests/test_proof/good/output/simple_vars.catala_en.Proof @@ -1,5 +1,5 @@ [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 7 | context z content integer | ^ @@ -78,7 +78,7 @@ true && true && (not false) true))) [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 7 | context z content integer | ^ @@ -127,7 +127,7 @@ if true then (let ((a!6 (or (and (=> true a!5) (=> (not true) false) true) false))) (and a!6 true)))) [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 5 | context x content integer | ^ @@ -178,7 +178,7 @@ true && true && (not false) true)))) [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 5 | context x content integer | ^ @@ -214,7 +214,7 @@ if true then (let ((a!5 (or (and (=> true a!4) (=> (not true) false) true) false))) (and a!5 true))))) [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 6 | context y content boolean | ^ @@ -231,7 +231,7 @@ true && true && (and (and true true) (not false))))) (and (and true true) a!1 a!1 true (not false) true)) [RESULT] For this variable: - --> test_proof/good/simple_vars.catala_en + --> tests/test_proof/good/simple_vars.catala_en | 6 | context y content boolean | ^