Pierre Villemot
Pierre Villemot
I will stall this PR. There are too much things to fix about the incremental mode. I prefer working on ADT now and fix the incremental mode later.
As I explained during the last dev meeting, we cannot check models of problems involving custom builtin functions like `ae.round` because there is no mechanism in Dolmen's binary to register...
I started a review of the code? Should I discard it?
> Everything except for changes to the `Intervals.ml` module is still valid and can be reviewed. There are subtleties in the interval module (I am starting to believe that there...
The current workflow is as follow: There is a branch `gh-pages` and a GitHub action in `documentation.yml` that build and push the documentation from `next` to the branch `gh-pages` as...
The performance issue is as follow: The branch v2.5.x is slightly slower on problems of the `ae-format` dataset when we enable the theory `fpa`. More precisely for the `unsat` output:...
~~It's a bug in my PR for benchpress. I'll fix it right now :)~~ It's a bit misleading but the current `total_time` outputs by benchpress is the total time for...
Ok, I reword what I mean in this issue. The main problem is the fact some preprocessing computations are performed in the `Expr` AST before feeding the SAT solver with...
**EDIT:** this comment is outdated. I completely rewrote this algorithm. The algorithm I used to ensure the termination of the model generation isn't sufficient. Last Friday, I found very simple...