[Bitv] Add support for the SMT-LIB2's BV primitives #669

hra687261 · 2023-06-20T08:12:17Z

src/lib/frontend/d_cnf.ml

src/lib/reasoners/bitv.ml

bclement-ocp

Alright, I made a first pass with a few comments/questions. There are still things I don't understand, I will do a second pass tomorrow.

src/lib/structures/symbols.mli

src/lib/structures/symbols.ml

src/lib/structures/symbols.mli

src/lib/structures/expr.ml

src/lib/reasoners/bitv.ml

Co-authored-by: Basile Clément <[email protected]>

bclement-ocp · 2023-07-03T08:50:11Z

@hra687261 you mentioned crashes, can you add the crashing test cases here?

hra687261 · 2023-07-04T05:04:42Z

Done the crashing tests are under tests/dolmen/bitv/errors and goals that should be proven but aren't are under tests/dolmen/bitv/todo
(Although there might be more since I haven't ran the benches in a while)

src/lib/structures/expr.ml

This patch adds support for the negation (bvnot) operator in the bitvector solver. There are two components to this support: - First, the union-find data structure used by the solver is replaced with an actual union-find data structure implemented using Tarjan's efficient algorithm, rather than using an implementation with sets and maps. - Second, the new union-find data structure is augmented with a link between a class representative and the representative of its negated class. When merging two classes, their negated classes are merged as well (and, in particular, if a class gets forced to all ones or all zeroes, its negated classes gets forced to the other bit value). If a class is ever merged with its negated class, the problem is unsolvable. The implementation is not necessarily the most efficient (e.g. we iterate over lists to negate them rather than directly creating the negated variables at several points), but it should be fairly simple and requires few changes to the existing solver infrastructure. The performance can be improved later if necessary. This extracted and simplified from part OCamlPro#669 and works towards better support for OCamlPro#625.

… of the bit-vectors they are called on)

This is the first part in a reloaded version of OCamlPro#669. It only includes parsing and typechecking support for the bit-vector primitives: bvnot, bvand, bvor, bv2nat and nat2bv (called int2bv because it also accepts negative inputs) are treated as uninterpreted functions; the other operators defined in the SMT-LIB are defined in terms of these primitives and of the existing `concat` and `extract` operators. The support for the bit-vector functions will be improved in separate PRs focusing on the bv2nat/nat2bv interaction, so that we are at least able to solve simple arithmetic goals. In the future, we might want to consider additional strategies (e.g. bitblasting), but that is out of scope for now. Following the discussion in OCamlPro#669, including the apparent restrictions around the building of "ite" in the theory and the lack of infrastructure for actually doing simplifications there (at least for now), the definition of most functions are moved back to `Expr.ml`. The PR also includes a few helper functions to help write the definition of the bitvector operators more concisely, which should help ensuring that they are correct.

This is a full rewrite of the Canonizer module in the bitvector solver. The new Canonizer (now called Canon) performs the same work as the old one, but does so slightly differently -- in particular, we now build terms lazily, which allows us to ignore parts of the tree for performance. The main motivation is actually not performance, but the ability to integrate bitwise operators (bvnot, bvand, bvor) into the canonizer in a more natural way. This is essentially the same architecture as that of `make_aux` from OCamlPro#669, but lifted to use a simple custom type (`view`) to avoid building new terms during canonization and benefit from match exhaustiveness checks.

This is the first part in a reloaded version of #669. It only includes parsing and typechecking support for the bit-vector primitives: bvnot, bvand, bvor, bv2nat and nat2bv (called int2bv because it also accepts negative inputs) are treated as uninterpreted functions; the other operators defined in the SMT-LIB are defined in terms of these primitives and of the existing `concat` and `extract` operators. The support for the bit-vector functions will be improved in separate PRs focusing on the bv2nat/nat2bv interaction, so that we are at least able to solve simple arithmetic goals. In the future, we might want to consider additional strategies (e.g. bitblasting), but that is out of scope for now. Following the discussion in #669, including the apparent restrictions around the building of "ite" in the theory and the lack of infrastructure for actually doing simplifications there (at least for now), the definition of most functions are moved back to `Expr.ml`. The PR also includes a few helper functions to help write the definition of the bitvector operators more concisely, which should help ensuring that they are correct.

This is a full rewrite of the Canonizer module in the bitvector solver. The new Canonizer (now called Canon) performs the same work as the old one, but does so slightly differently -- in particular, we now build terms lazily, which allows us to ignore parts of the tree for performance. The main motivation is actually not performance, but the ability to integrate bitwise operators (bvnot, bvand, bvor) into the canonizer in a more natural way. This is essentially the same architecture as that of `make_aux` from #669, but lifted to use a simple custom type (`view`) to avoid building new terms during canonization and benefit from match exhaustiveness checks.

Halbaroth · 2023-07-18T12:33:13Z

Is it ready for review?

bclement-ocp · 2023-07-18T12:36:14Z

Sorry, this one should be closed, it has been split off into #733 and #730

hra687261 added 2 commits June 19, 2023 22:41

Full support of BV primitives, 1st version

3a92a55

Move bv smart constructors to expr.ml

05f6349

hra687261 marked this pull request as draft June 20, 2023 08:12

This was referenced Jun 20, 2023

[WIP] attempt to add support for more FPA and BV primitives #554

Closed

Use the dolmen frontend for some tests #670

Closed