Denis Merigoux
158d49fe86
Removed unnecessary extra runtime function
2022-03-28 18:59:53 +02:00
Aymeric Fromherz
2b0206a5a8
Restrict duration z3 encoding to days only
2022-03-28 18:47:13 +02:00
Aymeric Fromherz
2c247128d1
[Z3encoding] Add support for duration literals
2022-03-24 17:22:31 +01:00
Aymeric Fromherz
8d2348d1d9
[Z3 encoding] Add support for Duration type and operators
2022-03-24 17:15:22 +01:00
Denis Merigoux
6722cf9647
Fix bug
2022-03-17 17:52:26 +01:00
Denis Merigoux
a7bdc0a114
Add condition for focusing the proof mode on a single scope
2022-03-17 17:44:24 +01:00
Denis Merigoux
cdac6de9fe
Implement the round money builtin
2022-03-17 12:30:14 +01:00
Aymeric Fromherz
97c0211bdc
[Z3encoding] Support for unit literal
2022-03-16 12:01:21 +01:00
Aymeric Fromherz
b00d270df7
[Z3backend] Add support for EInj nodes
2022-03-16 12:00:19 +01:00
Aymeric Fromherz
e3f3704be9
comment typo
2022-03-16 11:35:13 +01:00
Aymeric Fromherz
148afda523
Counterexamples generation for arrays
2022-03-16 11:28:03 +01:00
Aymeric Fromherz
fb6c18763f
Fix encoding of hypotheses into Z3
2022-03-16 11:20:20 +01:00
Aymeric Fromherz
f6ad6bbd2f
Encode that an array length is always positive
2022-03-15 18:52:02 +01:00
Aymeric Fromherz
fb924c50e5
Encode the length of arrays into Z3
2022-03-15 18:43:11 +01:00
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