Commits · main · AVA / Dandelion

Jul 29, 2022
- Use binary again · 45ce1e37
  Heiko Becker authored 2 years ago
  
  45ce1e37
- Revert "Remove buggy regression test" · 9fd9dde9
  Heiko Becker authored 2 years ago
  
  This reverts commit 3f6bcdab.
  9fd9dde9
Jul 28, 2022
- Remove buggy regression test · 3f6bcdab
  Heiko Becker authored 2 years ago
  
  3f6bcdab
Jul 20, 2022
- Remove unused test file · 35fcb8ac
  Heiko Becker authored 2 years ago
  
  35fcb8ac
Jul 19, 2022
- Remove unnnecessary printing · b70d4edd
  Heiko Becker authored 2 years ago
  
  b70d4edd
- Fix bitArithLib divergence · d3c2f8f4
  Heiko Becker authored 2 years ago
  
  d3c2f8f4
Jul 18, 2022
- Remove calls to 'use_karatsuba' · 9c557425
  Heiko Becker authored 2 years ago
  
  9c557425
- Fix binary folder for new HOL4 real structure · f19980fa
  Heiko Becker authored 2 years ago
  
  f19980fa
- Update ci to use latest CakeML master · d251bc71
  Heiko Becker authored 2 years ago
  
  d251bc71
Jul 15, 2022
- Fix bug in bitArithLib · 8a3ccc17
  Heiko Becker authored 2 years ago
  
  8a3ccc17
Jul 14, 2022
- Make CI more stringent to see error messages properly · 04546974
  Heiko Becker authored 2 years ago
  
  04546974
Jul 12, 2022
- Fix Holmakefile · 0010cbdd
  Heiko Becker authored 2 years ago
  
  0010cbdd
- Fix broken Holmakefile · 54f031f1
  Heiko Becker authored 2 years ago
  
  54f031f1
- Update Dandelion to properly use bit arithmetic · a889e8d6
  Heiko Becker authored 2 years ago
  
  a889e8d6
Feb 09, 2022
- Add missing soundness theorem · 253feec3
  Heiko Becker authored 3 years ago
  
  253feec3
Feb 07, 2022
- Add a bit of documentation to files · 68ceda80
  Heiko Becker authored 3 years ago
  
  68ceda80
- Add some explanation of the testcases to the README · 64771381
  Heiko Becker authored 3 years ago
  
  64771381
- Move examples for REAL_INEQ_TAC into a separate directory · 98e0630e
  Heiko Becker authored 3 years ago
  
  98e0630e
- Update testcases · 30f7ea29
  Heiko Becker authored 3 years ago
  
  30f7ea29
- Remove old testcases · db55dc75
  Heiko Becker authored 3 years ago
  
  db55dc75
- Add support for better approximations if propagated error is 0 · 53c6b95c
  Heiko Becker authored 3 years ago
  
  53c6b95c
- Add some instructions to README · a0948c32
  Heiko Becker authored 3 years ago
  
  a0948c32
Feb 06, 2022
- Add a number of new benchmarks for evaluation · e8745526
  Heiko Becker authored 3 years ago
  
  e8745526
Feb 04, 2022
- Update binary extraction · 0aa04d2b
  Heiko Becker authored 3 years ago
  
  0aa04d2b
- Make tool more robust, fix arctan and log approximations · f8916d1f
  Heiko Becker authored 3 years ago
  
  f8916d1f
- Minor updates, add benchmarks used in paper · d1cbb9a6
  Heiko Becker authored 3 years ago
  
  d1cbb9a6
- Update testcases · b87ed695
  Heiko Becker authored 3 years ago
  
  b87ed695
- Add sqrt replacement pass · 988ae017
  Heiko Becker authored 3 years ago
  
  988ae017
Feb 01, 2022
- Update metitarski script · a072da5f
  Heiko Becker authored 3 years ago
  
  a072da5f
- Make realZeroLib emit a good error message · c0f52d25
  Heiko Becker authored 3 years ago
  
  c0f52d25
- Fix error and computation of log · 229d57c7
  Heiko Becker authored 3 years ago
  
  229d57c7
- Add more testcases · f9edb408
  Heiko Becker authored 3 years ago
  
  f9edb408
- Clean up sturmCompute · 9fda01cb
  Heiko Becker authored 3 years ago
  
  9fda01cb
Jan 28, 2022
- Add updated version of eval scripts, simplify some lib files · b7f448af
  Heiko Becker authored 3 years ago
  
  b7f448af
- Rename testcases, do a proper run · c79c977e
  Heiko Becker authored 3 years ago
  
  c79c977e
- Merge branch 'sqrt_approx' into 'main' · 20da5a06
  Heiko Becker authored 3 years ago
  
  proved soundness of polynomial approximation of sqrt. changed the lemma... See merge request !25
  20da5a06
Jan 27, 2022
- ahh frustating. finally removed all occurences of elementary function in the sqrt_err def · dc91244b
  Mohit Tekriwal authored 3 years ago
  
  dc91244b
- just noticed another mention of an elementary function in the sqrt_err def and removed it · 260acf3e
  Mohit Tekriwal authored 3 years ago
  
  260acf3e
- Merge branch 'main' into sqrt_approx · 9cc8d746
  Mohit Tekriwal authored 3 years ago
  
  9cc8d746
- modified the sqrt_error def · 04c534b0
  Mohit Tekriwal authored 3 years ago
  
  04c534b0