mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-19 16:28:12 +03:00
Test base for verification conditions encoding
This commit is contained in:
Denis Merigoux
parent
d705334d9e
commit
83bdd0b632
@ -124,6 +124,7 @@ let filename_to_expected_output_descr (output_dir : string) (filename : string)
|
||||
| ".tex" -> Some Cli.Latex
|
||||
| ".html" -> Some Cli.Html
|
||||
| ".py" -> Some Cli.Python
|
||||
| ".proof" -> Some Cli.Proof
|
||||
| _ -> None
|
||||
in
|
||||
match backend with
|
||||
|
||||
@ -162,7 +162,7 @@ type vc_encoding_result = Success of Expr.expr | Fail of string
|
||||
them **)
|
||||
let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) :
|
||||
unit =
|
||||
Printf.printf "Running Z3 version %s\n" Version.to_string;
|
||||
Cli.debug_print (Format.asprintf "Running Z3 version %s" Version.to_string);
|
||||
|
||||
let cfg = [ ("model", "true"); ("proof", "false") ] in
|
||||
let z3_ctx = mk_context cfg in
|
||||
@ -205,7 +205,7 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati
|
||||
Solver.add solver
|
||||
(List.filter_map (fun (_, vc) -> match vc with Success e -> Some e | _ -> None) z3_vcs);
|
||||
|
||||
if Solver.check solver [] = SATISFIABLE then Cli.result_print "Success: Empty unreachable\n"
|
||||
if Solver.check solver [] = SATISFIABLE then Cli.result_print "Success: Empty unreachable"
|
||||
else
|
||||
(* TODO: Print model as error message for Catala debugging purposes *)
|
||||
Cli.error_print "Failure: Empty reachable\n"
|
||||
Cli.error_print "Failure: Empty reachable"
|
||||
|
||||
20
tests/test_proof/good/enums.catala_en
Normal file
20
tests/test_proof/good/enums.catala_en
Normal file
@ -0,0 +1,20 @@
|
||||
## Test
|
||||
|
||||
```catala
|
||||
declaration enumeration T:
|
||||
-- C content boolean
|
||||
-- D content integer
|
||||
|
||||
declaration enumeration S:
|
||||
-- A content integer
|
||||
-- B content T
|
||||
|
||||
declaration scope A:
|
||||
context x content integer
|
||||
context y content S
|
||||
|
||||
scope A:
|
||||
definition y equals B content (D content 1)
|
||||
definition x under condition match y with pattern -- A of a: true -- B of b: false consequence equals 0
|
||||
definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1
|
||||
```
|
||||
14
tests/test_proof/good/functions.catala_en
Normal file
14
tests/test_proof/good/functions.catala_en
Normal file
@ -0,0 +1,14 @@
|
||||
## Test
|
||||
|
||||
```catala
|
||||
declaration scope A:
|
||||
context x content integer depends on boolean
|
||||
context z content integer
|
||||
|
||||
scope A:
|
||||
definition x of y under condition y consequence equals 0
|
||||
definition x of y under condition not y consequence equals 1
|
||||
definition z under condition x of true = 0 consequence equals 0
|
||||
definition z under condition x of true < 0 consequence equals -1
|
||||
definition z under condition x of true > 0 consequence equals 1
|
||||
```
|
||||
10
tests/test_proof/good/no_vars.catala_en
Normal file
10
tests/test_proof/good/no_vars.catala_en
Normal file
@ -0,0 +1,10 @@
|
||||
## Test
|
||||
|
||||
```catala
|
||||
declaration scope A:
|
||||
context x content integer
|
||||
|
||||
scope A:
|
||||
definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54))
|
||||
consequence equals 0
|
||||
```
|
||||
104
tests/test_proof/good/output/enums.catala_en.Proof
Normal file
104
tests/test_proof/good/output/enums.catala_en.Proof
Normal file
@ -0,0 +1,104 @@
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/enums.catala_en
|
||||
|
|
||||
13 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true &&
|
||||
~
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if
|
||||
match y_12 with
|
||||
A: λ (a_44: integer) → true
|
||||
| B: λ (b_45: T) → false then true else false &&
|
||||
true && true && true && true else false && true && true &&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if
|
||||
match y_12 with
|
||||
A: λ (a_46: integer) → false
|
||||
| B: λ (b_47: T) → true then true else false &&
|
||||
true && true && true && true else false && true && true
|
||||
&& true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/enums.catala_en
|
||||
|
|
||||
13 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if
|
||||
match y_12 with
|
||||
A: λ (a_48: integer) → true
|
||||
| B: λ (b_49: T) → false then true else false &&
|
||||
true && true && true && true else false && true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if
|
||||
match y_12 with
|
||||
A: λ (a_50: integer) → false
|
||||
| B: λ (b_51: T) → true then true else false &&
|
||||
true && true && true && true else false && true && true else
|
||||
false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/enums.catala_en
|
||||
|
|
||||
14 | context y content S
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (and true (and (and true true) (not false)))
|
||||
(and true (and (and true true) (not false)))
|
||||
(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/enums.catala_en
|
||||
|
|
||||
14 | context y content S
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if true then true else false && true && true else false &&
|
||||
true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (=> false false) (=> (not false) false) (and true true))))
|
||||
(let ((a!2 (or a!1 (and (=> true true) (=> (not true) false) (and true true)))))
|
||||
(let ((a!3 (or (and (=> true (or a!1 a!1))
|
||||
(=> (not true) false)
|
||||
(and true true))
|
||||
(and (=> true a!2) (=> (not true) false) (and true true)))))
|
||||
(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false)))
|
||||
(and a!4 true)))))
|
||||
[RESULT] Success: Empty unreachable
|
||||
1
tests/test_proof/good/output/functions.catala_en.Proof
Normal file
1
tests/test_proof/good/output/functions.catala_en.Proof
Normal file
@ -0,0 +1 @@
|
||||
TODO
|
||||
55
tests/test_proof/good/output/no_vars.catala_en.Proof
Normal file
55
tests/test_proof/good/output/no_vars.catala_en.Proof
Normal file
@ -0,0 +1,55 @@
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/no_vars.catala_en
|
||||
|
|
||||
5 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true &&
|
||||
true && true && true && true && true && true && true && true && true &&
|
||||
true && true && true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(and (and true true)
|
||||
true
|
||||
(and true true (and true true) true)
|
||||
(and true true)
|
||||
(and true true)
|
||||
(and true true (and true true) true)
|
||||
true
|
||||
true
|
||||
(not false)
|
||||
(and true (and (and true true) (not false)))
|
||||
(and (and true true) (not false))
|
||||
(and true (and (and true true) (not false)))
|
||||
(and true (and (and true true) (not false)))
|
||||
(and (and true true) (not false))
|
||||
true
|
||||
(not false)
|
||||
true)
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/no_vars.catala_en
|
||||
|
|
||||
5 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if 6 * 7 = 42 && false || true && 1458 / 27 = 54 then true else false
|
||||
&&
|
||||
true && true && true && true && true && true && true &&
|
||||
true && true && true && true && true && true && true && true &&
|
||||
true else false && true && true else false && true || false &&
|
||||
true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] Success: Empty unreachable
|
||||
205
tests/test_proof/good/output/simple_vars.catala_en.Proof
Normal file
205
tests/test_proof/good/output/simple_vars.catala_en.Proof
Normal file
@ -0,0 +1,205 @@
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/simple_vars.catala_en
|
||||
|
|
||||
7 | context z content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true &&
|
||||
~
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 = 0 then true else false &&
|
||||
true && true && true && true else false && true && true
|
||||
&&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 < 0 then true && true else false &&
|
||||
true && true && true && true else false && true && true
|
||||
||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 = 0 then true else false &&
|
||||
true && true && true && true else false && true && true
|
||||
&&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 > 0 then true else false &&
|
||||
true && true && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 < 0 then true && true else false &&
|
||||
true && true && true && true else false &&
|
||||
true && true &&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 > 0 then true else false &&
|
||||
true && true && true && true else false &&
|
||||
true && true && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/simple_vars.catala_en
|
||||
|
|
||||
7 | context z content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 = 0 then true else false && true && true && true && true else
|
||||
false && true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 < 0 then true && true else false &&
|
||||
true && true && true && true else false && true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if x_5 > 0 then true else false && true && true && true && true
|
||||
else false && true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/simple_vars.catala_en
|
||||
|
|
||||
5 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false &&
|
||||
true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true &&
|
||||
~
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if y_4 then true else false && true && true else false &&
|
||||
true && true &&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if ~ y_4 then true else false && true && true && true else
|
||||
false && true && true && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (and true (and (and true true) (not false)))
|
||||
(and true (and (and true true) (not false)))))
|
||||
(a!2 (and (=> false false) (=> (not false) false) (and true true)))
|
||||
(a!4 (and (=> (not y_4) true)
|
||||
(=> (not (not y_4)) false)
|
||||
(and (and true true) true))))
|
||||
(let ((a!3 (or a!2 (and (=> y_4 true) (=> (not y_4) false) (and true true)))))
|
||||
(let ((a!5 (not (and (=> true a!3)
|
||||
(=> (not true) false)
|
||||
(and true true)
|
||||
(=> true (or a!2 a!4))
|
||||
(=> (not true) false)
|
||||
(and true true)))))
|
||||
(and (and true true)
|
||||
a!1
|
||||
(and (and true true) (not false))
|
||||
true
|
||||
(and (and true true) true)
|
||||
(not false)
|
||||
(and true (and (and true true) (not false)))
|
||||
(and (and true true) (not false))
|
||||
a!1
|
||||
(and true true)
|
||||
a!5
|
||||
true
|
||||
(not false)
|
||||
true))))
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/simple_vars.catala_en
|
||||
|
|
||||
5 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if y_4 then true else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if ~ y_4 then true else false && true && true && true else false &&
|
||||
true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (=> false false) (=> (not false) false) (and true true)))
|
||||
(a!3 (and (=> (not y_4) true)
|
||||
(=> (not (not y_4)) false)
|
||||
(and true true)
|
||||
true)))
|
||||
(let ((a!2 (or a!1 (and (=> y_4 true) (=> (not y_4) false) (and true true)))))
|
||||
(let ((a!4 (or (and (=> true (or a!1 a!1))
|
||||
(=> (not true) false)
|
||||
(and true true))
|
||||
(and (=> true a!2) (=> (not true) false) (and true true))
|
||||
(and (=> true (or a!1 a!3))
|
||||
(=> (not true) false)
|
||||
(and true true)))))
|
||||
(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
|
||||
|
|
||||
6 | context y content boolean
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (and true (and (and true true) (not false)))
|
||||
(and true (and (and true true) (not false)))
|
||||
(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
|
||||
|
|
||||
6 | context y content boolean
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if true then true else false && true && true else false &&
|
||||
true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (=> false false) (=> (not false) false) (and true true))))
|
||||
(let ((a!2 (or a!1 (and (=> true true) (=> (not true) false) (and true true)))))
|
||||
(let ((a!3 (or (and (=> true (or a!1 a!1))
|
||||
(=> (not true) false)
|
||||
(and true true))
|
||||
(and (=> true a!2) (=> (not true) false) (and true true)))))
|
||||
(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false)))
|
||||
(and a!4 true)))))
|
||||
[RESULT] Success: Empty unreachable
|
||||
108
tests/test_proof/good/output/structs.catala_en.Proof
Normal file
108
tests/test_proof/good/output/structs.catala_en.Proof
Normal file
@ -0,0 +1,108 @@
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/structs.catala_en
|
||||
|
|
||||
13 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true &&
|
||||
true && true && true && true && true && true && true && true && ~ false
|
||||
&& true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true &&
|
||||
~
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if y_4."a" = 0 && y_4."b"."c" then true else false &&
|
||||
true && true && true && true && true && true else false &&
|
||||
true && true &&
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false &&
|
||||
true && true && true && true && true && true && true &&
|
||||
true else false && true && true && true && ~ false &&
|
||||
true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/structs.catala_en
|
||||
|
|
||||
13 | context x content integer
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if y_4."a" = 0 && y_4."b"."c" then true else false &&
|
||||
true && true && true && true && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false &&
|
||||
true && true && true && true && true && true && true && true else
|
||||
false && true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
TODO
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/structs.catala_en
|
||||
|
|
||||
14 | context y content S
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for no two exceptions to ever overlap:
|
||||
true && true &&
|
||||
true && true && true && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && ~ false &&
|
||||
true && true && true && ~ false && true && true && true && ~ false &&
|
||||
true && true && ~ false && true && ~ false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(and (and true true)
|
||||
(and true true)
|
||||
true
|
||||
(and (and true true) (not false))
|
||||
(and true (and (and true true) (not false)))
|
||||
(and (and true true) (not false))
|
||||
(and true (and (and true true) (not false)))
|
||||
(and true (and (and true true) (not false)))
|
||||
(and (and true true) (not false))
|
||||
true
|
||||
(not false)
|
||||
true)
|
||||
[RESULT] For this variable:
|
||||
--> test_proof/good/structs.catala_en
|
||||
|
|
||||
14 | context y content S
|
||||
| ^
|
||||
+ Test
|
||||
This verification condition was generated for the variable definition never to return an empty error:
|
||||
if true then
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if false then false else false && true && true else false &&
|
||||
true && true ||
|
||||
if true then
|
||||
if false then false else false && true && true ||
|
||||
if true then true && true && true else false && true && true else
|
||||
false && true && true else false && true || false && true
|
||||
[RESULT] The translation to Z3 is the following:
|
||||
(let ((a!1 (and (=> false false) (=> (not false) false) (and true true)))
|
||||
(a!2 (and (=> true (and (and true true) true))
|
||||
(=> (not true) false)
|
||||
(and true true))))
|
||||
(let ((a!3 (or (and (=> true (or a!1 a!1))
|
||||
(=> (not true) false)
|
||||
(and true true))
|
||||
(and (=> true (or a!1 a!2))
|
||||
(=> (not true) false)
|
||||
(and true true)))))
|
||||
(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false)))
|
||||
(and a!4 true))))
|
||||
[RESULT] Success: Empty unreachable
|
||||
16
tests/test_proof/good/simple_vars.catala_en
Normal file
16
tests/test_proof/good/simple_vars.catala_en
Normal file
@ -0,0 +1,16 @@
|
||||
## Test
|
||||
|
||||
```catala
|
||||
declaration scope A:
|
||||
context x content integer
|
||||
context y content boolean
|
||||
context z content integer
|
||||
|
||||
scope A:
|
||||
definition y equals true
|
||||
definition x under condition y consequence equals 0
|
||||
definition x under condition not y consequence equals 1
|
||||
definition z under condition x = 0 consequence equals 0
|
||||
definition z under condition x < 0 consequence equals -1
|
||||
definition z under condition x > 0 consequence equals 1
|
||||
```
|
||||
20
tests/test_proof/good/structs.catala_en
Normal file
20
tests/test_proof/good/structs.catala_en
Normal file
@ -0,0 +1,20 @@
|
||||
## Test
|
||||
|
||||
```catala
|
||||
declaration structure T:
|
||||
data c content boolean
|
||||
data d content integer
|
||||
|
||||
declaration structure S:
|
||||
data a content integer
|
||||
data b content T
|
||||
|
||||
declaration scope A:
|
||||
context x content integer
|
||||
context y content S
|
||||
|
||||
scope A:
|
||||
definition y equals S { -- a : 0 -- b : T { -- c : false -- d: 0}}
|
||||
definition x under condition (y.a = 0) and y.b.c consequence equals 0
|
||||
definition x under condition not (y.a = 0) or not y.b.c consequence equals 1
|
||||
```
|
||||
Loading…
Reference in New Issue
Block a user