Commits · 257115620a5856d5cdaa53d8e8317c5fdbd93a42 · pub / colibrics

Jan 21, 2023
- [Array] better use of the DiffGraph · 25711562
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  25711562
- [NSeq] fix types of builtins · 3adeaaf6
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  3adeaaf6
- [Interp] Fix heuristic for wto · 64d1b194
  François Bobot authored 2 years ago
  
  64d1b194
- [Array] iterate on all the values of arrays · a4c0ea34
  François Bobot authored 2 years ago
  
  unsatisfactory use of limit, not fear iteration
  a4c0ea34
- [Array] DiffGraph and foreign_dom inetroperation · 13a4798f
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  In addition, added interface files and headers
  13a4798f
- [Array] Attempt at solving sat problems · 564e2bf7
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  564e2bf7
- [Array] Split the array theories: · 8f18c61b
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  - Generalized, Efficient Array Decision Procedures - Sharing is Caring
  8f18c61b
- [Array] Added the diff graph · d10b5e22
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  d10b5e22
- [NSeq] Added the nseq_content builtin · e00fa71b
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  e00fa71b
- Readd registering decision not linked to ground terms · 41004c69
  François Bobot authored 2 years ago
  
  41004c69
- Fix some warnings and remove some deadcode · 41fd439f
  François Bobot authored 2 years ago
  
  41fd439f
- [NSeq] updated builtins · fc62d090
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  fc62d090
- [Array] added the blast rule · 3f3dd785
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  3f3dd785
- Update Dolmen state creation · 7f570046
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  7f570046
- [Array] Added Array_dom and used it for map rules · 05621433
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  05621433
- [Array] Changes to the map rules · dfd1c276
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  dfd1c276
- [Seq] Added builtins · 77e92cc7
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  77e92cc7
- [Array] Added "colibri2_" as a prefix to the names of the builtins · acc73081
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  acc73081
- [Array] Fixed res-ext soundness error · bae2c9cd
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  bae2c9cd
- [Array] Attempt to fix and improve res-ext · 8ad8c3dd
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  8ad8c3dd
- Fix build · 0fcf8ee2
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  0fcf8ee2
- [equality] Add an hook for new disequalities · 94a4f835
  François Bobot authored 2 years ago
  
  94a4f835
- Added map inference rules · ea2f7d9c
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  ea2f7d9c
- Correct check of application argument type · c01ec56f
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  c01ec56f
- Use of polymorphic arrays instead of int arrays · 4875b823
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  4875b823
- [Array] fix a couple of bugs · 7e95ff14
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  7e95ff14
- [Array] Added headers to dom files · 14b1aab0
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  14b1aab0
- [Array] Partial support for the array combinator extension · e660bbdd
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  e660bbdd
- [Array] added restricted ext, aup rules · 11d17b69
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  11d17b69
- [Array] Added builtin op · e2ebc1fb
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  e2ebc1fb
- [Array] Moved the idx rule into the converter func · 625ff34b
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  625ff34b
- [Array] Remove useless eq from pattern · aee6d176
  François Bobot authored 2 years ago
  
  aee6d176
- [Array] fixed some bugs, added tests · 68afd58d
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  and the selectstore and distinct2neq rules
  68afd58d
- [Array] Added the array theory's basic rules · a4b6d26c
  Hichem R. A. authored 2 years ago and François Bobot committed 2 years ago
  
  a4b6d26c
- [Array] Start the theory · 0c66cfe6
  François Bobot authored 2 years ago
  
  0c66cfe6
Dec 01, 2022
- Add missing Why3__Builtin · c316da4a
  François Bobot authored 2 years ago
  
  c316da4a
- [Common] Add definition domain for unary strictly increasing · fd45399b
  François Bobot authored 2 years ago
  
  fd45399b
- Add tests for ceil, floor · 31d0fdad
  François Bobot authored 2 years ago
  
  31d0fdad
- [LRA] add propagators for ceil, truncate, floor · e997ecfe
  François Bobot authored 2 years ago
  
  e997ecfe
- Prove non-strictly increasing · fa41d606
  François Bobot authored 2 years ago
  
  fa41d606