Basile Clément
Basile Clément
Linking #211 as this is one of the sub-tasks in that issue
Some progress report: I have a better understanding of satML and a couple partially working prototypes for doing this, but did not run any large-scale benchmarks with them yet. There...
After discussing with @Gbury we can deal with this in Alt-Ergo proper for now. This would require adding support in the "additional builtins" in d_cnf. Note that: - This is...
What do we need that was not in #841 ?
Nice! I will not have time to look at this PR before the JFLA, however two quick remarks: > At the end of the function unsat, we perform a SAT.cancel_until...
> Please either remove entirely `Sat_solver_util.Make` or separate the definition of `Satml_frontend.Make` in `Satml_frontend.Make_internal` followed by `Satml_frontend.Make(Th) = Sat_solver_util.Make(Make_internal(Th))`; the indentation changes make it virtually impossible to review changes to...
> actually, there is another reason for which I couldn't use a CLI option for all the tests. The get-value feature doesn't work with optimization. I can add (set-option :verify-models...
Yeah I think that's fair — things will probably be easier if we finish #1000 first :(
Note that most of the functions mentioned above are handled by the FPA preludes. Notable exceptions are the BV functions bvand and bvor. - For the arith related stuff, would...
Note that when everything is uninterpreted, we do solve much faster (2s). Reintroducing ony `bvadd` as interpreted causes the issues to pop up again, so this is due to a...