Bit-Vector Rewriting with Automatic Rule Generation

  • Alexander Nadel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)


Rewriting is essential for efficient bit-vector SMT solving. The rewriting algorithm commonly used by modern SMT solvers iteratively applies a set of ad hoc rewriting rules hard-coded into the solver to simplify the given formula at the preprocessing stage. This paper proposes an automatic approach to rewriting. The solver starts each invocation with an empty set of rewriting rules. The set is extended by applying at run-time an automatic SAT-based algorithm for new rewriting rule generation. The set of rules differs from instance to instance. We implemented our approach in the framework of an algorithm for equivalence and constant propagation, called 0-saturation, which we extended from purely propositional reasoning to bit-vector reasoning. Our approach results in a substantial performance improvement in a state-of-the-art SMT solver over various SMT-LIB families.


Hash Table Unary Minus Propositional Reasoning Function Merge Substantial Performance Improvement 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Babic, D.: Exploiting structure for scalable software verification. Dissertation, The University of British Columbia (2008)Google Scholar
  2. 2.
    Bansal, S.: Peephole Superoptimization. Dissertation, Stanford University (2008)Google Scholar
  3. 3.
    Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: Shen, J.P., Martonosi, M. (eds.) ASPLOS, pp. 394–403. ACM (2006)Google Scholar
  4. 4.
    Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010),
  5. 5.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)Google Scholar
  6. 6.
    Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  8. 8.
    Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C programs using LLVM. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 623–626. Springer, Heidelberg (2013)Google Scholar
  9. 9.
    Franzén, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. Dissertation, University of Trento (2010)Google Scholar
  10. 10.
    Franzén, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 121–128. IEEE (2010)Google Scholar
  11. 11.
    Ganesh, V., Berezin, S., Dill, D.L.: A Decision Procedure for Fixed-Width Bit-Vectors. Technical report, Computer Science Department, Stanford University (April 2005)Google Scholar
  12. 12.
    Harrison, J.: Stålmarck’s algorithm as a HOL derived rule. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 221–234. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  13. 13.
    Katelman, M., Meseguer, J.: vlogsl: A strategy language for simulation-based verification of hardware. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 129–145. Springer, Heidelberg (2010)Google Scholar
  14. 14.
    Marić, F., Janičić, P.: URBiVA: Uniform reduction to bit-vector arithmetic. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 346–352. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Michel, R., Hubaux, A., Ganesh, V., Heymans, P.: An SMT-based approach to automated configuration. In: SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP 2012, p. 107 (2012)Google Scholar
  16. 16.
    Nadel, A.: Detailed experimental results for bit-vector rewriting with automatic rule generation,
  17. 17.
    Nordström, J.: Stålmarck’s method versus resolution: A comparative theoretical study. Master’s thesis, Stockholm University, Stockholm, Sweden (2001)Google Scholar
  18. 18.
    Romano, A., Engler, D.: Expression reduction from programs in a symbolic binary executor. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 301–319. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  19. 19.
    Sheeran, M., Stålmarck, G.: A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  20. 20.
    Trevor, A.H.: A constraint solver and its application to machine code test generation. Dissertation, Dept. of Computing and Information Systems, The University of Melbourne (2012)Google Scholar
  21. 21.
    Wille, R., Große, D., Haedicke, F., Drechsler, R.: SMT-based stimuli generation in the SystemC verification library. In: Borrione, D. (ed.) Advances in Design Methods from Modeling Languages for Embedded Systems and SoC’s. LNEE, vol. 63, pp. 227–244. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Alexander Nadel
    • 1
  1. 1.Intel CorporationHaifaIsrael

Personalised recommendations