CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 16:16:44 +03:00
Code Issues Projects Releases Wiki Activity

Formatting + correct expected tests output

Browse Source
This commit is contained in:
Denis Merigoux 2022-01-11 18:33:45 +01:00
parent b7e11e79b9
commit 260959b088
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
3 changed files with 20 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
compiler/verification/z3encoding.ml
View File

@ -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")

4
tests/test_proof/good/output/no_vars.catala_en.Proof
View File

@ -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
| ^

12
tests/test_proof/good/output/simple_vars.catala_en.Proof
View File

@ -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
| ^