SMT solvers for the theory of fixed-width bit-vectors are widely used. Bit-vector formulas often involve word-level arithmetic operations. Empirical evidence shows that bit-vector formulas with multiplication are often hard for SMT solvers to reason about. Therefore, it is important that an SMT solver uses all the structure available in the problem, including the word-level reasoning. Sometimes multiplication operators are decomposed and implemented in alternative ways, and the solver fails to identify the word-level multiplication operation. In this paper, we present a pre-processing heuristic that identifies the decomposed multipliers, and adds special assertions to the input formula that encodes equivalence of the decomposed multiplication and the word-level multiplication. The pre-processed formulas are then solved using an available solver. We have implemented our pre-processing algorithms in the rewriting engine of Z3 and applied these on a suite of benchmarks. Our experiments with three state-of-the-art SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.
|slides (VMCAI_rahul updated.pdf)||306KiB|
Sun 15 Jan
|16:00 - 16:30|
Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of SciencesFile Attached
|16:30 - 17:00|
Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-AlpesFile Attached
|17:00 - 17:30|