Synthesis of Arithmetic-Logical Expressions Using an SMT Solver

S. V. Kozlov, M. D. Cherepanov

Abstract


The paper investigates a method for automatic synthesis of arithmetic-logical programs based on the Z3 SMT solver. The Syntax-Guided Synthesis (SyGuS) approach is considered in relation to loop-free programs represented as acyclic computation graphs. The problem of synthesis is formalized through a system of logical constraints in the theory of bit-vectors, which includes the operational semantics of nodes, structural constraints on data flow, and symmetry-breaking conditions for commutative operations. A practical implementation of the synthesizer in C# using the Microsoft.Z3 library is described; it encodes the structure and semantics of the program as an optimization problem with cost function minimization. The experimental section demonstrates the synthesis of various target functions with two to four input variables: runtime ranges from 2.9 to 227 seconds depending on the expression’s complexity. It is shown that the synthesizer can automatically detect non-obvious algebraic equivalences and generate cost-optimal implementations. Issues of scalability and the exponential growth of complexity with an increasing number of computational nodes are discussed. The results confirm the applicability of SMT-based technologies to the super optimization of small program fragments with formal correctness guarantees

Full Text:

PDF (Russian)

References


Massalin H. Superoptimizer: a look at the smallest program // ACM SIGARCH Computer Architecture News. IEEE Computer Society Press. – 1987. – Vol. 15. – #. 5. – Pp. 122–126. DOI: 10.1145/36206.36194.

Souper: A synthesizing superoptimizer / Sasnauskas R., Chen Y., Collingbourne P. [et al.] // arXiv preprint arXiv: 1711.04422. – 2017. – Pp. 1-14. – DOI: 10.48550/arXiv.1711.04422.

Scaling up superoptimization / Phothilimthana P. M., Thakur A., Bodik R. [et al.] // ACM SIGARCH Computer Architecture News. ACM. – 2016. – Vol. 51. – #. 4. – Pp. 297–310. – DOI: 10.1145/2954679.2872387.

Syntax-guided synthesis / Alur R., Bodik R., Juniwalet G. [et al.] // Formal Methods in Computer-Aided Design. IEEE. – 2013. – Pp. 1-8. – DOI: 10.1109/FMCAD.2013.6679385.

Synthesis of loop-free programs / Gulwani S., Jha S., Tiwari A. [et al.] // PLDI. 2011. Vol. 11. P. 62–73. – DOI: 10.1145/1993498.1993506.

Beyer D., Dangl M., Wendler P. A unifying view on SMT-based software verification // Journal of Automated Reasoning. – 2018. – Vol. 60. – # 3. – Pp. 299-335. – DOI: 10.1007/s10817-017-9432-6.

Component based synthesis applied to bitvector programs: Technical Report MSR-TR-2010-12 / Gulwani S., Jha S., Tiwari A. [et al.] / Microsoft Research. – 2011. – 14 p.

De Moura L., Bjørner N. Z3: An efficient SMT solver // Tools and Algorithms for the Construction and Analysis of Systems (TACAS). – Berlin; Heidelberg: Springer, 2008. – Vol. 4963. – Pp. 337-340. – DOI: 10.1007/978-3-540-78800-3_24.

Gulwani S. Dimensions in program synthesis // Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming. – 2010. – Pp. 13–24. – DOI: 10.1145/1836089.1836091.

Monniaux D. A survey of satisfiability modulo theories // Computer Engineering & Science. 2016. – Vol. 9890. – Pp. 401-425. – DOI: 10.1007/978-3-319-45641-6_26.

Andrianov I. A., Grigor'eva A. N. Modernizacija indeksa dlja poiska po reguljarnym vyrazhenijam // Sistemy upravlenija i informacionnye tehnologii. – 2020. – # 2 (80). – S. 60-64.

Kozlov S. V. Interpretacija invariantov teorii grafov v kontekste primenenija sootvetstvija Galua pri sozdanii i soprovozhdenii informacionnyh sistem // International Journal of Open Information Technologies. – 2016. – T. 4. # 7. – S. 38-44.

What’s decidable about syntax-guided synthesis? / Caulfield T., Alur R., Fisman D. [et al.] // arXiv preprint arXiv:1510.08393. – 2015. – Pp. 1-15. – DOI: 10.48550/arXiv.1510.08393.

Functional synthesis for linear arithmetic and sets / Kuncak V., Mayer M., Piskac R. [et al.] // International Journal on Software Tools for Technology Transfer. Springer. – 2013. – Vol. 15 # 5-6. – Pp. 455-474. – DOI: 10.1007/s10009-011-0217-7.

Solving quantified bit-vectors using invertibility conditions / Niemetz A., Preiner S., Krebbers R. [et al.] // International Conference on Computer Aided Verification. Springer. 2018. – Pp. 236-255. – DOI: 10.1007/978-3-319-96142-2_16.

Sovetov P. N. Sintez linejnyh programm dlja stekovoj mashiny // Vysokoproizvoditel'nye vychislitel'nye sistemy i tehnologii. – 2019. – T. 3, # 1. – S. 17-22.

Solar-Lezama A. Program synthesis by sketching // Ph.D. Dissertation. – Berkeley. University of California. – 2008. – 176 p.

Synthesising programs with non-trivial constants / Abate A., Barbosa H., Barrett C. [et al.] // Journal of automated reasoning. – 2023. – Vol. 67. – #2. – P. 19. – DOI: 10.1007/s10817-023-09664-4.

Reynolds A. Challenges for fast synthesis procedures in SMT // ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements. – 2017. – Vol. 51. – Pp. 69-75. – DOI: 10.29007/xrhz.

Abraham E., Kremer G. SMT solving for arithmetic theories: Theory and tool support // International Conference on Symbolic and Numeric Algorithms for Scientific Computing. IEEE. – 2017. – Pp. 1-8. – DOI: 10.1109/SYNASC.2017.00009.

Reynolds A., King T., Kuncak V. Solving quantified linear arithmetic by counterexample-guided instantiation // Formal Methods in System Design. – 2017. – Vol. 51. – Pp. 1-33. DOI: 10.1007/s10703-017-0290-y.

Spielmann A., Kuncak V. Synthesis for unbounded bit-vector arithmetic // International Joint Conference on Automated Reasoning. – 2012. – Pp. 499-513. – DOI: 10.1007/978-3-642-31365-3_39.

Barbosa H. An introduction to SMT solving with quantifiers // Universidade Federal de Minas Gerais. – 2024. – 111 p.

Kozlov S. V., Svetlakov A. V. Primenenie reguljarnyh vyrazhenij dlja obrabotki tekstovyh dannyh // International Journal of Open Information Technologies. – 2022. – T. 10, # 9. – S. 82-89.

Kozlov S. V., Svetlakov A. V. O LL(1)-grammatikah, algoritmah na nih i metodah ih analiza v programmirovanii // International Journal of Open Information Technologies. – 2022. – T. 10, # 3. – S. 30-38.

Boosting SMT solver performance on mixed-bitwise-arithmetic expressions / Xu D., Liu B., Feng W. [et al.] // Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. – 2021. – Pp. 651–664. – DOI:10.1145/3453483.3454068.

Schindler T. SMT solving, interpolation, and quantifiers // Ph.D. Dissertation. – University of Freiburg. – 2022. – 229 p. – DOI: 10.6094/UNIFR/229572.

Antipina A. V. Zadacha avtomaticheskoj generacii peephole-optimizacij: obzor podhodov, reshenie problemy optimal'nogo rasshirenija arhitektury nabora managed instrukcij // Sovremennye informacionnye tehnologii i IT-obrazovanie. – 2021. – T. 17, # 3. S. 613-624. – DOI 10.25559/SITITO.17.202103.613-624.

Grashhenkov N. R., Kozlov S. V. Sozdanie vos'mibitnogo summatora v videoigre "Minecraft" / N. R. Grashhenkov, // Novye informacionnye tehnologii i sistemy (NITiS-2023): sbornik nauchnyh statej po materialam XX Mezhdunarodnoj nauchno-tehnicheskoj konferencii, posvjashhennoj 80-letnemu jubileju Penzenskogo gosudarstvennogo universiteta, Penza, 16–17 nojabrja 2023 goda. – Penza: Penzenskij gosudarstvennyj universitet, 2023. – S. 174-178.

Balunovic M., Bielik P., Vechev M. Learning to solve SMT formulas // Proceedings of the 32nd International Conference on Neural Information Processing Systems. – 2018. – Pp. 10338-10349.


Refbacks

  • There are currently no refbacks.


Abava  Кибербезопасность Monetec 2026 СНЭ

ISSN: 2307-8162