Commit Graph

2016 Commits

Author SHA1 Message Date
lIlIlIlIIIIlIIIllIIlIllIIllIII
b8d65f9f29
pair programming with alain & lilya 2022-03-16 12:22:32 +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
lIlIlIlIIIIlIIIllIIlIllIIllIII
1f0518a241
fixing typos 2022-03-16 10:42:35 +01:00
Denis Merigoux
c936e7b6ed
Reshuffle code, make it work, correct a few yes/no inversion bugs 2022-03-15 19:47:41 +01:00
Aymeric Fromherz
f6ad6bbd2f Encode that an array length is always positive 2022-03-15 18:52:02 +01:00
Denis Merigoux
3780af59f5
Merge branch 'master' into allocations_logement 2022-03-15 18:44:49 +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
Lilya Slimani
2de4b7620c Oublie de la date de naissance du demandeur 2022-03-15 14:13:11 +01:00
Denis Merigoux
169432c9f2
Pair programming @Lilyaslm 2022-03-14 11:55:32 +01:00
Denis Merigoux
88bf577db6
Merge branch 'master' into allocations_logement 2022-03-14 10:46:57 +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
Lilya Slimani
5712816bdc Premier test !! :) 2022-03-11 16:51:00 +01:00
Lilya Slimani
5e96656eb0 Merge branch 'allocations_logement' of https://github.com/CatalaLang/catala into allocations_logement 2022-03-11 15:14:51 +01:00
Lilya Slimani
f4e85e20d5 Ajout des articles pour la cession de PP + Tentative de programmation d'un exemple. 2022-03-11 11:46:45 +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
Denis Merigoux
a5425ec5ee
Pair programming with @Lilyaslm today! 2022-03-09 15:27:38 +01:00
Lilya Slimani
c945198898 Merge branch 'allocations_logement' of https://github.com/CatalaLang/catala into allocations_logement 2022-03-09 14:18:10 +01:00
Lilya Slimani
3206cd4cfb Ajout des articles à coder pour la prochaine cession de pair programming 2022-03-09 14:17:21 +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
42cd56eaf1
Use grouped exceptions in allocations familiales code 2022-03-09 11:25:16 +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
97ede2cde1
Merge branch 'master' into allocations_logement 2022-03-09 10:47:29 +01:00
Denis Merigoux
2dfb15d888
reformat (sync with master) 2022-03-09 10:43:17 +01:00
Denis Merigoux
cf233ac7de
Change settings 2022-03-09 10:43:00 +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