boolean formulae in What4. This datastructure automatically implements
associative-commutative-idempotent rewriting as well as recognizing
resolution opportunities (i.e. A /\ ~A = False).
gather products.
In addition, use similar machenery to represent bitwise disjunction.
This gives additional boolean lattice reductions, including absorption
and idempotency.
and generalize equality and if/then/else to work over all base types.
Bitvectors now are paricipants in two different semiring instances:
the usual arithmetic one and a bitwise one based on XOR and AND.
This allows automatic term gathering, XOR-canceling and other
similar simplifications to occur automatically.
bitvector operations in `what4`.
Solvers don't generally have primitives for these, but it is nonethess useful,
I think, to provide them as operations. A collection of useful rewrites
could probably be added (e.g., interesting interaction with concat).
This update fixes a variety of issues with solver interaction involving
the named assertion and unsat core updates. CVC4, Z3 and Yices now will
properly issue queries and return resuts.
In addition, a variety of refactorings were made to the interaction code
that should make things more uniform going forward. As part of these
refactorings, it is now possible to pass an "auxiliary output" file handle
when interacting with solvers. If provided, solver commands and responses
will be echoed into this file for debugging purposes.
instead of just a single predicate. The semantics of the query is
just the conjunction of the given predicates. However, for the purposes
of computing unsatisfiable cores, the list of given predicates
will be the atomic units that will either appear (or not) in the
generated unsat cores, for those solvers which support computing
unsat cores.
in the expression builder. That way, it can be fully elminated when
it encounters a `bvNonzero` or `bvTestBit` operation, etc.
This should remove some of the noisy patterns that otherwise arise,
especially from the LLVM translation, which uses length 1 bitvectors
as a stand-in for boolean values.
This commit mainly does two things:
* Add more robust support for the integer theory, including `div`, `mod`, `abs` and `divisible`.
* Audit the semantics of the `integerToBV` operations, and fix lingering bugs.
In the past, there were two different integer->BV operations, because we used a clamping semantics,
and it made sense to have a signed versus unsigned distinction. Now, however, we are using
a modulo `2^n` semantics, and there is only one operation. However, some places in the code were
still using the clamped semantics. These placses have now been cleaned up, and everywhere should
be using the modular arithmetic view.
In addition, I've reduced the need to use the expensive BV->Integer and Integer->BV coersions somewhat
by noticing when we round trip through those coercions more often and translating the result into
statements of modular arithmetic instead.
Along the way, I improved the abstract domain definitions for division and modulus.
