alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
The purpose of this PR is to make it possible to use Dolmen as a front-end to Alt-Ergo and eventually make it the default front-end instead of the current one....
The purpose of this PR is to add the necessary functions to allow resolution context re-initialization in Alt-Ergo. Since Alt-Ergo internally relies on side effects through references and hash-tables, A...
The preprocessing of a formula sometimes allow Alt-Ergo to discard useless patterns (especially on ite where the condition is trivial). Three options are included in this PR: - `-simplify [y|n]`...
AltErgo 2.4.1 crashes on the following file with the above error message. The error case was generated in Why3. (Zipped for the GH filters..) [01_resolve_unsoundness-C01ResolveUnsoundness_MakeVecOfSize-make_vec_of_sizeqtvc_1.ae.zip](https://github.com/OCamlPro/alt-ergo/files/9185811/01_resolve_unsoundness-C01ResolveUnsoundness_MakeVecOfSize-make_vec_of_sizeqtvc_1.ae.zip)
The error message "alt-ergo: algebraic datatype are not supported" does not come from Alt-Ergo but from Why3 (here: https://gitlab.inria.fr/why3/why3/-/blob/master/src/printer/alt_ergo.ml#L366). But ```omg``` still doesn't pass the type checking in Alt-Ergo: ```...
The purpose of this PR is to add a new plugin based on semi-definite programming (SDP, aka convex optimization). It solves problems involving polynomial inequalities which cannot be solved with...
