Pierre Villemot

Optimization and `push` and `pop`

2

The current implementation of `SatML` doesn't apply properly `push` and `pop` in presence of objectives. Indeed, the following input (thanks @bclement-ocp): ```smt (set-option :produce-models true) (set-logic ALL) (declare-const x Int)...

Printing unknown reason

2

We should support the SMT-LIB syntax `(get-info :reason-unknown)` to be able to print the reason why Alt-Ergo answers `timeout`. See https://github.com/OCamlPro/alt-ergo/pull/829#discussion_r1332945479 The PR #837 partially solves this issue.

--dump-models-on implies --dump-models

2

If we want to dump models somewhere, we definitively want models! I also refactor a bit the code and fix spelling.

The distinct expression clashes with the SMT-LIB specification

2

The current implementation of the `distinct` expression in the module `Expr` clashes with the SMT-LIB specification. In Alt-Ergo, the expression `mk_distinct [x_1; ...; x_n]` means: ``` x_1 x2 and x2...

Supporting the float theory of the SMT-LIB

1

The current implementation of Alt-Ergo doesn't support the float theory https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml but a theory about round functions from the `real` to subset of `real` corresponding to finite floats with fixed...

Wrong model for arrays

5

The current model produced by Alt-Ergo for the input `555.smt2` is wrong: ``` (set-logic ALL) (set-option :produce-models true) (declare-const x Int) (declare-const y Int) (declare-const a1 (Array Int Int)) (declare-const...

We publish 4 `opam` packages for the project now. It makes sense to publish plugins in separate packages as they can used different licenses. It'll be simpler to publish the...