alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
The target of this PR: the first part before getting rid of the Commands module. As the legacy frontend still relies on it, this PR only cuts all the dependencies...
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
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...
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...
This patch adds interval and bitlist propagators for the bvshl (left shift) and bvlshr (logical right shift) in the intervals and bitlist domains for bit-vectors. The interval propagator for left...
These are interval propagators only and respect the SMT-LIB semantics for division by 0. This requires custom operators in the `Intervals` module that update the bounds appropriately, sincethe existing `div`...
This patch adds constraints to represent bit-vector addition and multiplication, with propagators in the interval domain and a simple propagator for multiplication that only considers the factors-of-two multiples in the...
In CC(X), the leaves are always terms that were present in the original problem: we do not introduce new uninterpreted terms. In AC(X), this is no longer true: we might...
This is a backport of https://github.com/OCamlPro/alt-ergo/pull/1045 to the 2.4.x branch so that we can provide static builds for the release 2.4.3 as requested by our partners in the Decysif project.
I think #1049 fixed the issue, but we should double-check. See https://github.com/ocaml/opam-repository/pull/25294