Various resources found while trying to understand z3 better:
- http://rise4fun.com/Z3/tutorial/guide (Z3 tutorial for SMT-2.0)
- https://github.com/ericpony/z3py-tutorial (Z3 tutorial for Python)
- https://ece.uwaterloo.ca/~agurfink/ece653/z3py-advanced (z3, python, quantifiers)
- https://leodemoura.github.io/files/qsmt.pdf
- http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/advanced-examples.htm
- https://stackoverflow.com/questions/13930013/equivalence-checking-with-z3
- https://stackoverflow.com/questions/13199219/z3-quantifier-support
- https://stackoverflow.com/questions/15758601/for-all-quantifier-in-z3
-
https://github.com/mrexodia/z3-haskell (git repository for the
Z3.Monadmodule) -
https://hackage.haskell.org/package/z3-4.1.1/docs/Z3-Monad.html (docs for
Z3.Monad) - https://stackoverflow.com/questions/38538197/difference-between-z3-mk-forall-and-z3-mk-forall-const-in-c-api-for-z3
Z3.Monad mkForall
-- | Create a forall formula.
--
-- The bound variables are de-Bruijn indices created using 'mkBound'.
--
-- Z3 applies the convention that the last element in /xs/ refers to the
-- variable with index 0, the second to last element of /xs/ refers to the
-- variable with index 1, etc.
mkForall :: Context
-> [Pattern] -- ^ Instantiation patterns (see 'mkPattern').
-> [Symbol] -- ^ Bound (quantified) variables /xs/.
-> [Sort] -- ^ Sorts of the bound variables.
-> AST -- ^ Body of the quantifier.
-> IO AST