Denis Merigoux
c47ce263b5
Merge pull request #228 from CatalaLang/afromher_z3
...
[Z3encoding] Basic support for arrays
2022-03-16 12:17:31 +01:00
Denis Merigoux
041d47bf06
Merge pull request #229 from CatalaLang/fix_just_logging
...
Fix logging operator location for default justifications
2022-03-16 12:05:02 +01:00
Denis Merigoux
bba5e3afea
Only print logging in Scopelang if debug
2022-03-16 12:00:36 +01:00
Denis Merigoux
c59451751b
Fix logging operator location for default justifications
2022-03-16 11:44:34 +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
bb57abf750
Negative tests for array length encoding
2022-03-16 11:23:36 +01:00
Aymeric Fromherz
123541dc34
Add positive test for array length
2022-03-16 11:21:54 +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
Denis Merigoux
f3cf8ae3e4
Merge pull request #227 from CatalaLang/afromher_z3
...
Proof platform: Better error message when Z3 encoding not supported, and extend GetYear support
2022-03-15 18:14:50 +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
Denis Merigoux
ecdd3dfaef
Merge pull request #225 from CatalaLang/fix-nix/alcotest+patch
...
Fix nix/alcotest+patch
2022-03-11 18:26:32 +01:00
lIlIlIlIIIIlIIIllIIlIllIIllIII
3f54574a5a
alcotest import
2022-03-10 12:00:38 +01:00
lIlIlIlIIIIlIIIllIIlIllIIllIII
bf73109ecc
no-web-patch fix
2022-03-10 12:00:25 +01:00
Denis Merigoux
6227097de4
Merge pull request #223 from AltGr/optional-z3
...
Make Z3 an optional dependency
2022-03-09 17:22:06 +01:00
Denis Merigoux
a797ee1b25
Removes the JS build from the website assets (no longer used on the website)
2022-03-09 17:08:32 +01:00
Denis Merigoux
20996a10be
Cleaning
2022-03-09 17:06:25 +01:00
Denis Merigoux
c1cf956308
Warning about Z3 and the proof platform
2022-03-09 17:03:47 +01:00
Denis Merigoux
897a282b70
Default is witout Z3
2022-03-09 17:00:53 +01:00
Louis Gesbert
933869d269
Move 'dependencies' from the 'all' target
...
and adapt the CI to skip z3 installation.
Is it more usual for `all` targets to build everything but not include
dependencies handling ?
2022-03-09 13:23:11 +01:00
Louis Gesbert
9456ace6b1
Make z3 an optional dependency, add 'make dependencies-noz3'
...
Also the CI will no longer compile/use z3
2022-03-09 12:53:17 +01:00
Denis Merigoux
41cf1ec0e6
Merge pull request #222 from CatalaLang/refactor-catala_backend_option-functions
...
Refactor: group common functions related to backend_option in the Cli module
2022-03-09 11:12:01 +01:00
Denis Merigoux
296760f09c
Merge pull request #224 from CatalaLang/afromher_dcalc
...
DCalc optimization pass: Remove if_then_else when both branches are identical
2022-03-09 10:29:51 +01:00
Denis Merigoux
e0a8bb1f6b
Merge pull request #221 from AltGr/options-record
...
Command-line: use a record for the options
2022-03-09 10:28:59 +01:00
Aymeric Fromherz
9eec6a474c
format
2022-03-08 20:43:55 +01:00
Aymeric Fromherz
9cbfc13288
Merge branch 'master' into afromher_dcalc
2022-03-08 20:41:35 +01:00
Aymeric Fromherz
3fb14264c2
Implement equal_ops in dcalc
2022-03-08 20:39:45 +01:00
Aymeric Fromherz
ac42bf65a7
Refactor to extract common equal_exprs_list and equal_typs_list
2022-03-08 20:31:22 +01:00
Aymeric Fromherz
5b345b4782
format
2022-03-08 20:23:45 +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
Aymeric Fromherz
2fa2f36c1d
Optimize if_then_else when both branches are identical
2022-03-08 17:38:14 +01:00
Louis Gesbert
b4b6d5d648
Fix compilation catala_web_interpreter
...
oops I overlooked that one
2022-03-08 17:35:57 +01:00
Aymeric Fromherz
89d69c2316
Implement equality function on dcalc expressions
2022-03-08 17:35:08 +01:00
Denis Merigoux
e5e0164fee
Remove unused dev dependencies in opam file
...
As suggested by https://github.com/ocaml/opam-repository/pull/20861#issuecomment-1061807613
2022-03-08 17:25:25 +01:00
Louis Gesbert
0e874752c1
Merge remote-tracking branch 'origin/master'
2022-03-08 16:20:41 +01:00
Emile Rolley
709d4e5ae5
fix(lcalc): disable ocamlformat for let+ expressions
2022-03-08 16:13:47 +01:00
Louis Gesbert
729fb7e551
reformat (sync with master)
2022-03-08 16:12:25 +01:00
Denis Merigoux
5c5eae1d19
Change settings
2022-03-08 16:11:53 +01:00
Louis Gesbert
071ec35234
Command-line: use a record for the options
...
Should make it much easier and less error-prone to add new options. There is
still a bit of boiler-plate, but at least it's contained in the Cli.options
function and doesn't transpire in the interfaces.
2022-03-08 16:11:39 +01:00
Emile Rolley
7c1f4cc02d
refactor: group common functions related to backend_option in the Cli module
2022-03-08 15:52:26 +01:00
Denis Merigoux
efdf653ec7
Merge pull request #220 from CatalaLang/reformat
...
Reformatting of the OCaml code
2022-03-08 15:40:02 +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
Denis Merigoux
65a5a42c16
Change settings
2022-03-08 15:01:18 +01:00
Denis Merigoux
5a186f8cfd
Merge pull request #218 from AltGr/format-strings
...
Use format strings directly in debug/error/log functions
2022-03-08 15:00:56 +01:00
Denis Merigoux
c07bab1377
FIXME -> TODO
2022-03-08 14:55:48 +01:00
Denis Merigoux
95bf732940
Update assets
2022-03-08 14:54:17 +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
