Aymeric Fromherz
|
e2963bd7f3
|
Add a duration_to_nb_days function to runtime
|
2022-03-24 17:22:16 +01:00 |
|
Aymeric Fromherz
|
8d2348d1d9
|
[Z3 encoding] Add support for Duration type and operators
|
2022-03-24 17:15:22 +01:00 |
|
Denis Merigoux
|
f2307b88d3
|
Merge pull request #234 from CatalaLang/select_scope_proof
Select a single scope for the proof mode
|
2022-03-17 17:55:36 +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
|
7872e8dac3
|
Typo in lexer
|
2022-03-17 13:23:07 +01:00 |
|
Denis Merigoux
|
52680bdca7
|
Merge pull request #233 from CatalaLang/rounding_builtin
Adding a money rounding builtin to Catala
|
2022-03-17 13:15:01 +01:00 |
|
Denis Merigoux
|
a3e9dfa534
|
Fix wrong round definitions in runtime
|
2022-03-17 13:09:57 +01:00 |
|
Denis Merigoux
|
80dea233d7
|
Merge pull request #232 from isovector/patch-1
Fix typos in English tutorial
|
2022-03-17 12:37:16 +01:00 |
|
Denis Merigoux
|
f312c6bc6a
|
Documentation in syntax cheat sheet
|
2022-03-17 12:35:03 +01:00 |
|
Denis Merigoux
|
cdac6de9fe
|
Implement the round money builtin
|
2022-03-17 12:30:14 +01:00 |
|
Sandy Maguire
|
8bc3a87376
|
Fix typos in English tutorial
|
2022-03-16 18:07:19 -07:00 |
|
Denis Merigoux
|
5663c616fd
|
Merge pull request #230 from CatalaLang/afromher_z3_2
[Z3encoding] Extend support for enumerations
|
2022-03-16 12:22:51 +01:00 |
|
Denis Merigoux
|
9b35cfcf7d
|
Merge branch 'master' into afromher_z3_2
|
2022-03-16 12:18:01 +01:00 |
|
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 |
|
Aymeric Fromherz
|
cb36b9d72f
|
[Z3backend] Bad unit tests for EInj node
|
2022-03-16 12:04:31 +01:00 |
|
Aymeric Fromherz
|
d758170cde
|
[Z3backend] Good unit tests for EInj node
|
2022-03-16 12:03:24 +01:00 |
|
Aymeric Fromherz
|
97c0211bdc
|
[Z3encoding] Support for unit literal
|
2022-03-16 12:01:21 +01:00 |
|
Denis Merigoux
|
bba5e3afea
|
Only print logging in Scopelang if debug
|
2022-03-16 12:00:36 +01:00 |
|
Aymeric Fromherz
|
b00d270df7
|
[Z3backend] Add support for EInj nodes
|
2022-03-16 12:00:19 +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 |
|