# AAProver

AAProver is a bit-precise theorem prover for typical operations present in programming languages. It takes a single bit vector expression and reduces it to a CNF by replacing all operations with circuits and then applying Tseitin tautologies. Finally, the CNF is solved using MiniSAT. If a solution is found the satisfying assignment may be queried.

Though this library was not a main objective for the original thesis, it is shortly described there as well (more extensive than here).

The code is available for download.

AAProver is then able to prove that there is a single solution, with the satisfying assignment being (x == 7) && (y == -8).

This is just a very basic example, please look at AACalysto to see what is possible with this library.

(*) AAProver supports arbitrary bit-width (even mixed in the same expression), 4 bits were chosen to keep the example simple.

Though this library was not a main objective for the original thesis, it is shortly described there as well (more extensive than here).

The code is available for download.

## Example

For the following (simple) example assume that x and y are both 4 bit wide signed integers (*):(y == x + 1) && (y < x)

AAProver is then able to prove that there is a single solution, with the satisfying assignment being (x == 7) && (y == -8).

This is just a very basic example, please look at AACalysto to see what is possible with this library.

(*) AAProver supports arbitrary bit-width (even mixed in the same expression), 4 bits were chosen to keep the example simple.