CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 00:41:05 +03:00
Code Issues Projects Releases Wiki Activity
2,888 Commits 41 Branches 8 Tags 60 MiB
5f04e0efaf
Commit Graph

196 Commits

Author SHA1 Message Date
Aymeric Fromherz
4b1ace2739 [Z3Backend] Support GetYear equality comparison 2022-03-15 18:09:56 +01:00
Aymeric Fromherz
d760d883a6 [Z3encoding] Print variable name when encoding is not supported 2022-03-15 18:09:33 +01:00
Louis Gesbert
e7e89873db Make Z3 an optional dependency 
If Catala is compiled without Z3, trying to run it with the backend `Proof` will
yield:
```
[ERROR] This instance of Catala was compiled without Z3 support.
```
and return 124

Note that this doesn't change the `make depends`, opam file or CI to account for it,
it just enables it at the build-system level.

There are also no hooks at this moment to have Catala self-document the options
whith which it was compiled (e.g. in the `--help` screen). But that could be
added in a more general way later, it's probably not really needed yet.
 2022-03-08 18:38:42 +01:00
Denis Merigoux
5bd66142a6
Big reformatting 
ocamlformat 0.19.0 -> 0.20.1
100 -> 80 columns per line
Reestablished @emilerolley's smart fun break
 2022-03-08 15:03:14 +01:00
Louis Gesbert
12ec65601d Use format strings directly in debug/error/log functions 
This avoids many intermediate calls to e.g. `Format.asprintf`; should result in
some cases in "more correct" use of `Format`¹, avoid the computation of unused
debug strings, and make the code more readable.

¹ for `Format` to work as expected, all intermediate calls need to go through
it. Some cases of formatting to an intermediate string then printing through Format
again are still present, but this makes the situation better.
 2022-03-08 13:04:27 +01:00
Aymeric Fromherz
a463ec7db2 Use Cli.max_prec_digits 2022-02-21 14:54:40 +01:00
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