About Cogent
Cogent is a decision procedure for bitvector logic. Features:
- All ANSI-C operators are supported.
- Core extraction: Which predicates are important for the formula being
UNSAT?
- Optional output of CNF in DIMACS format.
- Optional output of encoded Boolean formula before conversion into CNF.
The ETH technical report describing Cogent is available here.
Download
Further Reading
You might be interested in the following papers on this topic: