- May 04, 2023
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
- Includes both direct and indirect dependencies of variables. - Avoids using Base.SetLattice.project. - Properly catches Not_found error when a variable is not in relation in the state. Also fixes [get_var_bases] function on missing variables. This function is called by [relate] according to the [Relations] map, which is an over-approximation of the relations really inferred in the state — it can contains variables that do not belong to the state, so [get_var_bases] should not crash in that case.
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
(Outside of the Variable module, which still differentiates variables and lvalues for now.) Infers intervals about lvalues and not only variables. Registers in deps variables and lvalues for which an interval is inferred.
-
-
-
-
-
-
-
-
-
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
-
David Bühler authored
The order between variables in an octagon state now depends on the id of hashconsed lvalues, which is not deterministic — unless option -deterministic is set.
-
-
- remove variables present only left or only right during joins
-
-
-
-
-
-
-
-
-
-
-
-