Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation
W Wang, H Søndergaard, PJ Stuckey
Journal of Automated Reasoning | Springer Netherlands | Published : 2019
We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector so..View full abstract
Related Projects (1)
Awarded by Australian Research Council
We acknowledge support from the Australian Research Council through ARC Discovery Grant DP140102194.