Denis Merigoux
|
260959b088
|
Formatting + correct expected tests output
|
2022-01-11 18:33:45 +01:00 |
|
Aymeric Fromherz
|
20cc0795f9
|
Arithmetic binary operators
|
2022-01-11 17:54:02 +01:00 |
|
Aymeric Fromherz
|
f642bfe4be
|
Z3 encoding: More binary operators, pass more tests
|
2022-01-11 17:49:02 +01:00 |
|
Denis Merigoux
|
83bdd0b632
|
Test base for verification conditions encoding
|
2022-01-11 16:13:34 +01:00 |
|
Denis Merigoux
|
d705334d9e
|
Merge branch 'master' into proof_platform
|
2022-01-11 15:43:33 +01:00 |
|
Alain
|
e8dbaaec47
|
add not to z3encoding
|
2022-01-10 17:30:08 +01:00 |
|
Aymeric Fromherz
|
4b47f7fd9a
|
More binary operators encoding, some boolean examples now passing
|
2022-01-10 14:53:58 +01:00 |
|
Aymeric Fromherz
|
b9b593a361
|
Encode some basic types to Z3
|
2022-01-10 14:51:36 +01:00 |
|
Aymeric Fromherz
|
0455029951
|
Z3: Start encoding Catala types as Z3 sorts
|
2022-01-10 14:50:50 +01:00 |
|
Aymeric Fromherz
|
bc4608755a
|
Z3: Encode EVar node
|
2022-01-10 14:46:41 +01:00 |
|
Aymeric Fromherz
|
2d036f9925
|
Add ctx_var to z3encoding context
|
2022-01-10 14:37:17 +01:00 |
|
Aymeric Fromherz
|
a9ebfaed38
|
Pass program to z3encoder
|
2022-01-10 14:36:15 +01:00 |
|
Denis Merigoux
|
04cc274d3e
|
Print term for error message
|
2022-01-10 11:52:48 +01:00 |
|
Denis Merigoux
|
4082e5056e
|
More prettier things
|
2022-01-10 10:59:30 +01:00 |
|
Denis Merigoux
|
3a864b6160
|
Aesthetic improvements
|
2022-01-10 10:28:14 +01:00 |
|
Denis Merigoux
|
743a1b74c9
|
Renamed and grouped modules cleanly
|
2022-01-08 18:37:04 +01:00 |
|