Z3 is an SMT solver developed by Microsoft Research (https://github.com/Z3Prover/z3/wiki).

Z3 allows you to mix Presburger arithmetic and propositional logic, and check whether
given formulas hold. For example, try executing the two examples below at https://rise4fun.com/Z3.

You may also read sections 1–5 and 9 of https://rise4fun.com/Z3/tutorial,
and even more here: https://github.com/Z3Prover/z3/wiki/Documentation.


;;; Example 1 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Declare the function foo : Int × Int × Int → Bool
; s.t. foo(x, y, z) holds iff
; x, y, z >= 0, y = 1 + x + 5·z and z = 2 - 2·z - y
(define-fun foo ((x Int) (y Int) (z Int)) Bool
  (and
    (>= x 0)
    (>= y 0)
    (>= z 0)
    (= y (+ 1 x (* 5 z)))
    (= z (- 2 (* 2 z) y))
  )
)

; Declare existentially quantified integer variables
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

; Assert that foo has a solution (x, y, z)
(assert (foo x y z))

(check-sat) ; Check whether assertions hold
(get-model) ; Obtain solution


;;; Example 2 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Declare function bar : Bool × Bool × Bool → Bool
; s.t. bar(x, y, z) holds iff
;                (x ⇒	(y ⇒ z)) ⇔ ((x ∧ y) ⇒	z)
(define-fun bar ((x Bool) (y Bool) (z Bool)) Bool
  (=
    (=> x (=> y z))
    (=> (and x y) z)
  )
)

; Assert that bar is a tautology
(assert
  (forall ((x Bool) (y Bool) (z Bool))
    (bar x y z) 
  )
)

(check-sat) ; Check whether assertions hold