Useful links for Z3

Z3Py.md

Useful Links for Z3 encoding

Tailored for Python

Official

• Tutorial: Jupyter Notebook

• Official guide: Github, Z3 API

• Z3 Course & Slides: Gitlab

Stack Overflow

• Basics: 1

• Print Assertions: 1,2, 3

• Tactics/Nonlinear Artithmetic: 1, 2

  • Non-linear integer arithmetic, 2
  • Tactic
  • Strategies
  • More details on Tactics

• Example with complex numbers: 1

• Square root encoding: 1, 2, 3,4

• Min/max encoding: 1, 2, 3

• If/then/else: 1

• Exponential: 1

Other Links

• Reproducibility in ML:1, 2
• Add bibliography, e.g. Reluplex, Marabu
• SMT & Binarized Networks [Katz][An SMT-Based Approach for Verifying Binarized Neural Networks] (https://arxiv.org/pdf/2011.02948.pdf)
• Chebyshev approximations for NN and Z3py, blog post

SMT comparisons& Tools

• cvc5: A Versatile and Industrial-Strength SMT Solver, Link
• SMT competition 2022, Links: 1, 2