mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
[skip ci] Z3 encoding: update last missing examples with TODOs
This commit is contained in:
Aymeric Fromherz
parent
f342c89482
commit
c0a8362fd9
@ -1,104 +1,6 @@
|
||||
[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:
|
||||
[ERROR] The translation to Z3 failed:
|
||||
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:
|
||||
[ERROR] The translation to Z3 failed:
|
||||
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
|
||||
[RESULT] A.y: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.y: this variable never returns an empty error
|
||||
|
||||
@ -1,108 +1,6 @@
|
||||
[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:
|
||||
[ERROR] The translation to Z3 failed:
|
||||
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:
|
||||
[ERROR] The translation to Z3 failed:
|
||||
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
|
||||
[RESULT] A.y: no two exceptions to ever overlap for this variable
|
||||
[RESULT] A.y: this variable never returns an empty error
|
||||
|
||||
Loading…
Reference in New Issue
Block a user