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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | Decision proceduresVMCAI at Amphitheater 44 Chair(s): Andreas Podelski University of Freiburg, Germany | ||
16:00 30mTalk | Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games VMCAI Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences File Attached | ||
16:30 30mTalk | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes File Attached | ||
17:00 30mTalk | Matching multiplications in Bit-Vector formulas VMCAI File Attached |