Denis Merigoux
3f49824150
Merge branch 'master' into c_backend
2022-04-04 18:02:33 +02:00
Denis Merigoux
31e8f37a43
Sort VCs by alphabetical order
2022-04-04 17:51:41 +02:00
Denis Merigoux
7ca5ef283a
Code builds but bugguy [skip ci]
2022-04-04 08:56:48 +02:00
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
