Hichem R. A.

[WIP] - Adding Dolmen as a front-end

1

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....

Added contex reinitialisation functions

1

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...

Stack overflow in "src/lib/util/zarithNumbers.ml", line 65, when the CDCL solver is used

5

[co_2096_l.ae.txt](https://github.com/OCamlPro/alt-ergo/files/7032249/co_2096_l.ae.txt) Running Alt-Ergo on the attached file with: ``` alt-ergo --sat-solver CDCL co_2096_l.ae ``` causes a stack overflow in the call to Zarith's gcd function. The problem is probably in...

Unsoundness bug (cu_651)

1

[c_651_l_bis.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6992216/c_651_l_bis.smt2.txt) [c_651_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6992217/c_651_l_bis.ae.txt) Alt-Ergo responds with "Valid" on the ".ae" file with the four solvers. And "I don't know" on the ".smt2" file when the CDCL solver is used, and "Valid"...

[c_735_l_bis.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6998557/c_735_l_bis.smt2.txt) [c_735_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6998558/c_735_l_bis.ae.txt) Responses: |   | .smt2 | .ae | |-----------|-----------|-----------| | AE(T) | Valid | Valid | | AE(T-C) | Valid | Valid | | AE(C-T) | Valid |...

[c_685_l.smt2.txt](https://github.com/OCamlPro/alt-ergo/files/6992923/c_685_l.smt2.txt) [c_685_l.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6992924/c_685_l.ae.txt) The .ae and .smt2 files are supposed to be equivalent. Alt-Ergo responds with "Valid" (on both the ".ae" and the ".smt2" files) when the Tableaux or the Tableaux-CDCL...

[c_1130_l_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6982313/c_1130_l_bis.ae.txt) Running the command: ``` ./alt-ergo --sat-solver CDCL c_1130_l_bis.ae ``` Causes the following error: ``` Fatal error: exception File "src/lib/reasoners/satml_frontend.ml", line 1019, characters 13-19: Assertion failed ``` And when the...

Assertion failure in "src/lib/reasoners/intervalCalculus.ml", line 1175, when using the CDCL solver

5

[c_262_0_ae_bis.ae.txt](https://github.com/OCamlPro/alt-ergo/files/6955011/c_262_0_ae_bis.ae.txt) Running Alt-Ergo (built from the "next" branch) on the attached file with the command: ``` ./alt-ergo --sat-solver CDCL c_262_0_ae_bis.ae ``` Causes the following error: ``` Fatal error: exception File...

Fix #504 and #509

1

Changing the installation section for plugins and preludes from `share` to `lib` (to fix issues #504 and #509). If some users use the plugins and look for them in `/usr/share`...