Pierre Villemot

New test scripts

1

This PR consists in replacing the old bash scripts used for running the non-regression tests by a mighty Ocaml script. I moved most of the tests from `/non-regression` directory to...

This PR removes most of the global opens in the Alt-Ergo library. They are replaced by local opens, aliases and explicit type annotations.

First of all, thanks for your cool plugin :) I am a lazy guy and I can't remember two shortcuts when I could use only one. I mainly use your...

feat(ADT): model generation

1

This PR implements the model generation for ADT. The model generation is done by the casesplit mechanism in `Adt_rel`. - If `--enable-adts-cs` is present, we do casesplits by choosing a...

This PR is rebased on #1078 and #1086.

ADT reasoning on distinct literals is incomplete

8

The current implementation of the ADT theory is incomplete. By incomplete I mean the reasoning isn't capable to notice inconsistency of some ground problems involving only ADT and boolean symbols....

Logs

2

This PR starts to use logs to print debug messages. I tried to keep it as reasonable as possible, so I didn't change all the printers. - Every named modules...

Support `get-value` statement

13

This PR adds the support for the `get-value` statement for both `SatML` and `FunSAT` solvers. I create a new functor to factorize the code between these solvers. This PR doesn't...

Invalid SAT environment while optimizing

9

The current implementation of `unsat_rec_prem` is wrong in presence of optimization if we try to use the SAT API directly. Consider the input problem: ```smt2 (set-option :produce-models true) (set-logic ALL)...

While implementing the `get-value` support (see #1032), I noticed that the decision level of `SatML` isn't always zero after calling `SAT.unsat`. It means we cannot always assert new facts after...