Pierre Villemot
Pierre Villemot
Consider the input file ``` (set-logic ALL) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (assert (distinct a b)) (check-sat) (get-model) ``` Calling AE with the...
The current `Expr` module does not expose smart constructors for FP theory as the `Z3.FloatingPoint` does. I noticed this lack while writing the interface for AE in the project https://github.com/wasp-platform/encoding....
After testing the behavior of cvc5 and z3 and the SMTLIB specification, I noticed that we have to produce a status message (`sat`, `unsat`, `unknown`) before producing a model with...
As you know, Alt-Ergo will use Dolmen parser as a new frontend. The Dolmen integration has been merged on `next`, see #491. In the next release 2.5.0, Dolmen will be...
I found a bug in Dune. On `next`, type ``` make clean ./configure dune build ``` I got a very long error message (about 2.4 Mb!!!): ``` Error: execve(../install/default/bin/alt-ergo): No...
This PR aims to document as much as possible the current AST of Alt-Ergo. Some cleaning works has been done while this marvelous travel :) - Remove an id used...
This PR is an attempt to replace the current comparisons functions in the module `Symbol` and the comparison of triggers in `Expr` by generated ones with [ppx_compare](https://github.com/janestreet/ppx_compare). The current code...
This issue is a notice to keep track of regular problems occurring in AE during the E-matching. At some point between 2.4.1 and 2.4.2, Mohamed introduced an optimization consisting to...
I am using Benchpress to track regressions in Alt-Ergo but sometimes I got regressions that I cannot reproduce manually. My guess is that the way Benchpress computes running times is...