Aymeric Fromherz
|
63704324c1
|
[Z3 Backend] Better error message when function has type TAny
|
2022-02-19 23:28:04 +01:00 |
|
Aymeric Fromherz
|
31c2adf0f1
|
Z3 Backend: Extend arithmetic operations to money
|
2022-02-19 23:18:23 +01:00 |
|
Aymeric Fromherz
|
25ff8c50fb
|
[Z3 Backend]: Add support for rationals
|
2022-02-19 01:59:34 +01:00 |
|
Aymeric Fromherz
|
dd05e4468b
|
[Z3backend]: Do not crash when trying to print function model
|
2022-02-18 00:34:42 +01:00 |
|
Aymeric Fromherz
|
6dec7bfe04
|
Refactor Z3 print_model: get_const_interp is only usable for non-function expressions
|
2022-02-18 00:28:36 +01:00 |
|
Aymeric Fromherz
|
d776a10e5f
|
format
|
2022-02-17 18:44:40 +01:00 |
|
Aymeric Fromherz
|
378ab4697a
|
Encode TUnit in Z3
|
2022-02-17 18:34:30 +01:00 |
|
Denis Merigoux
|
9fcc79a66f
|
Fix bug for encoding verification conditions from Dcalc, coming from #189
|
2022-02-15 17:58:18 +01:00 |
|
Denis Merigoux
|
e1dc36f1b1
|
Merge branch 'master' into io-qualifiers-112-part-2
|
2022-02-10 22:59:37 +01:00 |
|
Denis Merigoux
|
5004929a51
|
Fix #193 -- authored with @R1kM
Moved no model generation flag
Fixed bug for VC generation in the IfThenElse case
|
2022-02-10 16:49:01 +01:00 |
|
Denis Merigoux
|
d401b3424c
|
Fixed verification conditions generation
|
2022-02-10 10:05:14 +01:00 |
|
Denis Merigoux
|
effc2b24e4
|
Optimizations for defaults in Dcalc
|
2022-01-31 15:27:58 +01:00 |
|
Denis Merigoux
|
5e253ba321
|
Disabling exact counterexamples values from CI testing because of randomness
|
2022-01-26 16:24:09 +01:00 |
|
Denis Merigoux
|
d2977b48ce
|
Documentation pass
|
2022-01-19 10:54:16 +01:00 |
|
Denis Merigoux
|
a4002fefaf
|
Finished functorization
|
2022-01-19 10:17:19 +01:00 |
|
Denis Merigoux
|
bc2742961f
|
More functors, but still not finished
|
2022-01-19 10:12:20 +01:00 |
|
Denis Merigoux
|
2f7059c1ac
|
More functorization
|
2022-01-19 09:47:08 +01:00 |
|
Denis Merigoux
|
4852891e6c
|
Added interfaces
|
2022-01-18 18:59:05 +01:00 |
|
Denis Merigoux
|
b11e3329b3
|
Functorize VC solving IO [skip ci]
|
2022-01-18 18:51:02 +01:00 |
|
Denis Merigoux
|
2e1dc4740a
|
Restore build [skip ci]
|
2022-01-18 17:59:15 +01:00 |
|
Denis Merigoux
|
777f194178
|
.mlis and ocamldoc [skip-ci]
|
2022-01-18 15:13:16 +01:00 |
|
Aymeric Fromherz
|
400a777891
|
Support common case for getYear: Comparison against a literal [skip ci]
|
2022-01-17 15:02:56 +01:00 |
|
Aymeric Fromherz
|
cf63e4f3d3
|
Restore pretty-printing of enum model [skip ci]
|
2022-01-14 21:10:34 +01:00 |
|
Aymeric Fromherz
|
2548b4ad5e
|
Pretty-print structs, temporarily disable pretty-printing of enum model during refactoring [skip ci]
|
2022-01-14 21:02:34 +01:00 |
|
Aymeric Fromherz
|
0b011a5e3a
|
Support TTuple type [skip ci]
|
2022-01-14 20:37:45 +01:00 |
|
Aymeric Fromherz
|
7fa271b9f4
|
Construct Z3 sort corresponding to a struct [skip ci]
|
2022-01-14 20:35:22 +01:00 |
|
Aymeric Fromherz
|
89e41b3a33
|
Encode ETupleAccess node [skip ci]
|
2022-01-14 20:17:27 +01:00 |
|
Aymeric Fromherz
|
850718be17
|
Add support for structs in the Z3 encoding context [skip ci]
|
2022-01-14 20:08:42 +01:00 |
|
Aymeric Fromherz
|
6c749fdbfe
|
Pretty-print enums in Z3 model [skip ci]
|
2022-01-14 19:23:26 +01:00 |
|
Aymeric Fromherz
|
06b845316d
|
Allow match bodies in VCs to refer to the value corresponding to the destructed enum [skip ci]
|
2022-01-14 19:01:54 +01:00 |
|
Aymeric Fromherz
|
3c21182dea
|
Finish encoding arms of EMatch in VCs [skip ci]
|
2022-01-14 18:33:56 +01:00 |
|
Aymeric Fromherz
|
a7abe630e7
|
More progress towards encoding arms of EMatch in VCs [skip ci]
|
2022-01-14 18:24:32 +01:00 |
|
Aymeric Fromherz
|
ffee0d815d
|
Wrap up the find_or_create_enum function [skip ci]
|
2022-01-14 17:42:12 +01:00 |
|
Aymeric Fromherz
|
7c1e808880
|
Translate the type TEnum to Z3
|
2022-01-14 17:42:12 +01:00 |
|
Aymeric Fromherz
|
a1e12a22b1
|
Create or retrieve Z3 enum types [skip ci]
|
2022-01-14 17:42:12 +01:00 |
|
Aymeric Fromherz
|
ae0935f035
|
Z3 encoding: Add a map from enumnames to Z3 sorts to the context [skip ci]
|
2022-01-14 17:42:12 +01:00 |
|
Aymeric Fromherz
|
1932277c80
|
Fix printing of negative money amounts [skip ci]
|
2022-01-14 11:45:47 +01:00 |
|
Aymeric Fromherz
|
951e50637f
|
Actually plug date pretty printing into Z3 encoding [skip ci]
|
2022-01-14 02:08:04 +01:00 |
|
Aymeric Fromherz
|
50ad5e3044
|
Print dates generated by Z3 model [skip ci]
|
2022-01-14 02:04:55 +01:00 |
|
Aymeric Fromherz
|
977e985e4c
|
Encode dates to Z3 [skip ci]
|
2022-01-14 01:54:33 +01:00 |
|
Aymeric Fromherz
|
d89eea0481
|
Encode comparison operators on money [skip ci]
|
2022-01-13 20:11:28 +01:00 |
|
Aymeric Fromherz
|
827f5cb916
|
encode money to Z3 [skip ci]
|
2022-01-13 20:02:14 +01:00 |
|
Aymeric Fromherz
|
50d0ee0909
|
Start printing z3 model results according to their type [skip ci]
|
2022-01-13 19:52:58 +01:00 |
|
Denis Merigoux
|
428ae95c62
|
[skip ci] Added a walkthrough example for ProLaLa + tweaked tests output order of vcs
|
2022-01-13 16:58:43 +01:00 |
|
Denis Merigoux
|
5a6f4485e7
|
Matching subscope variables also [skip ci]
|
2022-01-13 16:00:09 +01:00 |
|
Denis Merigoux
|
a9454a0aac
|
Correctly match ignored part of expressions in VC generation [skip ci]
|
2022-01-13 12:15:37 +01:00 |
|
Denis Merigoux
|
bf444f548f
|
Error message pretty-printing and sat solving example [skip ci]
|
2022-01-13 10:46:23 +01:00 |
|
Aymeric Fromherz
|
f342c89482
|
[skip ci] Z3encoding: proper error message for ill-formed unary operators
|
2022-01-12 19:15:51 +01:00 |
|
Aymeric Fromherz
|
29ed4ff696
|
[skip ci] Z3encoding: refer to Catala source code variable names when printing a model
|
2022-01-12 19:09:20 +01:00 |
|
Aymeric Fromherz
|
297b7ec604
|
[skip ci] Z3encoding: documenting the function style for the context
|
2022-01-12 19:02:56 +01:00 |
|
Aymeric Fromherz
|
83e83507ed
|
[skip ci] Z3encoding: Passing the context around to preserve dynamic updates throughout the VC encoding
|
2022-01-12 18:59:01 +01:00 |
|
Aymeric Fromherz
|
e66730bdd5
|
[skip ci] Start improving model prettyprinting
|
2022-01-12 18:35:36 +01:00 |
|
Aymeric Fromherz
|
a7ad86233e
|
[skip ci] document Z3encoding context type
|
2022-01-12 18:23:50 +01:00 |
|
Aymeric Fromherz
|
862af7a3d8
|
[skip ci] Pretty-print simple Z3 models when a VC is not satisfied
|
2022-01-12 18:15:09 +01:00 |
|
Aymeric Fromherz
|
45dc3faeed
|
[skip ci] minor refactor: prepare to parse Z3 model
|
2022-01-12 17:55:32 +01:00 |
|
Aymeric Fromherz
|
0e59cff1ed
|
[skip ci] print Z3 model when verification is failing
|
2022-01-12 17:51:28 +01:00 |
|
Aymeric Fromherz
|
9995837564
|
[skip ci] Z3encoding: support function calls
|
2022-01-12 17:38:12 +01:00 |
|
Denis Merigoux
|
78b1fe08f4
|
[skip ci] Always name of the variable on the left
|
2022-01-12 16:56:05 +01:00 |
|
Denis Merigoux
|
6d06f9c81c
|
Prettified error messages
|
2022-01-12 16:50:10 +01:00 |
|
Aymeric Fromherz
|
2a8f7f7c07
|
[skip ci] remove all logs before encoding query to z3
|
2022-01-12 16:30:00 +01:00 |
|
Aymeric Fromherz
|
d455e29978
|
[skip ci] Z3encoding: obtain type of bound variables
|
2022-01-12 15:58:19 +01:00 |
|
Denis Merigoux
|
c7b225bad5
|
Add types of free variables in VC [skip ci]
|
2022-01-12 15:52:44 +01:00 |
|
Aymeric Fromherz
|
7f3e59f7b0
|
[skip ci] Z3encoding: more debug information when encoding fails
|
2022-01-12 15:21:13 +01:00 |
|
Aymeric Fromherz
|
8bb8053580
|
[skip ci] Z3 encoding: Better split output between debug and non-debug information
|
2022-01-12 14:43:17 +01:00 |
|
Aymeric Fromherz
|
3c6f9d9174
|
[skip ci] formatting + slight refactor for better error messages during Z3 verification
|
2022-01-12 14:20:52 +01:00 |
|
Aymeric Fromherz
|
b11c76404f
|
[skip ci] Spawn one query per VC and correctly encode VC by negating it
|
2022-01-12 14:08:35 +01:00 |
|
Aymeric Fromherz
|
e10a25876f
|
[skip ci] Print Z3 encoding information as debug information only
|
2022-01-12 13:58:38 +01:00 |
|
Aymeric Fromherz
|
1c8f9c31f5
|
Z3 encoding: Add missing Lte for integers
|
2022-01-12 12:16:54 +01:00 |
|
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
|
5c5bc77c87
|
formatting (sorry, problem with the makefile)
|
2022-01-10 17:53:48 +01:00 |
|
Alain
|
5bc9a36308
|
vc generation for conflict errors
|
2022-01-10 17:30:19 +01:00 |
|
Alain
|
e8dbaaec47
|
add not to z3encoding
|
2022-01-10 17:30:08 +01:00 |
|
Alain
|
0c2dbdddd1
|
correct typo in vc generation for conflict error
add some debug in comments
|
2022-01-10 17:29:53 +01:00 |
|
Alain
|
8a0a4c7603
|
naive verification condition for conflicts
|
2022-01-10 16:25:20 +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
|
50719911f8
|
Added TODOs
|
2022-01-10 13:48:00 +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
|
ad4218285d
|
Working partial evaluation for Dcalc using ugly but correct style
|
2022-01-09 19:16:34 +01:00 |
|
Denis Merigoux
|
743a1b74c9
|
Renamed and grouped modules cleanly
|
2022-01-08 18:37:04 +01:00 |
|