### Z3 SMT Example: Using :macro-finder for Quantifier Expansion

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Illustrates the use of Z3's preprocessor option `:macro-finder` to expand quantifiers that represent macros. This can improve the performance of the model finder. The example defines several sorts and functions related to roles, permissions, and actions in a system.

```smt2
(set-option :smt.mbqi true)
(set-option :smt.macro-finder true)

(declare-sort Action)
(declare-sort Role)
(declare-sort Permission)
(declare-sort Id)

(declare-fun Client () Role)  
(declare-fun FinAdmin () Role)
(declare-fun FinClerk () Role)
(declare-fun Manager () Role)
(declare-fun POAdmin () Role)
(declare-fun POClerk () Role)
(declare-fun action2int (Action) Int)
(declare-fun id1 () Id)
(declare-fun id2 () Id)
(declare-fun id2int (Id) Int)
(declare-fun id3 () Id)
(declare-fun id4 () Id)
(declare-fun id5 () Id)
(declare-fun id6 () Id)
(declare-fun id7 () Id)
(declare-fun p1 () Permission)
(declare-fun p2 () Permission)
(declare-fun p3 () Permission)
(declare-fun p4 () Permission)
(declare-fun p5 () Permission)
(declare-fun p6 () Permission)
(declare-fun permission2int (Permission) Int)
(declare-fun role2int (Role) Int)
(declare-fun role_level (Role) Int)
(declare-fun t1_receive () Action)
(declare-fun t2_invoke () Action)
(declare-fun t3_split () Action)
(declare-fun t4_join () Action)
(declare-fun t5_invoke () Action)
(declare-fun t6_invoke () Action)
(declare-fun t7_invokeO () Action)
(declare-fun t8_invokeI () Action)
(declare-fun t9_invoke () Action)
(declare-fun in_creator_ctrPay_0 () Int)
(declare-fun in_creator_ctrPay_1 () Int)
(declare-fun in_customer_crtPO_0 () Int)
(declare-fun in_customer_crtPO_1 () Int)
(declare-fun out_approverPOPayment_apprPay_0 () Int)
(declare-fun out_approverPOPayment_apprPay_1 () Int)
(declare-fun out_approverPO_apprPO_0 () Int)
(declare-fun out_approverPO_apprPO_1 () Int)
(declare-fun out_creator_ctrPay_0 () Int)
(declare-fun out_creator_ctrPay_1 () Int)
(declare-fun out_signerGRN_ctrsignGRN_0 () Int)
(declare-fun out_signerGRN_ctrsignGRN_1 () Int)
(declare-fun out_signerGRN_signGRN_0 () Int)
(declare-fun out_signerGRN_signGRN_1 () Int)
(declare-fun p10_final_0 () Int)
(declare-fun p10_final_1 () Int)
(declare-fun p11_final_0 () Int)
(declare-fun p11_final_1 () Int)
(declare-fun p1_final_0 () Int)
(declare-fun p1_final_1 () Int)
(declare-fun p2_final_0 () Int)
(declare-fun p2_final_1 () Int)
(declare-fun p3_running_0 () Int)
(declare-fun p3_running_1 () Int)
(declare-fun p4_final_0 () Int)
(declare-fun p4_final_1 () Int)
(declare-fun p5_final_0 () Int)
(declare-fun p5_final_1 () Int)
(declare-fun p6_initial_0 () Int)
(declare-fun p6_initial_1 () Int)
(declare-fun p7_final_0 () Int)
(declare-fun p7_final_1 () Int)
(declare-fun p8_initial_0 () Int)
(declare-fun p8_initial_1 () Int)
(declare-fun p9_initial_0 () Int)
(declare-fun p9_initial_1 () Int)


;PREDICATES

(declare-fun has_permission (Id Action) Bool)
(declare-fun permission (Permission Action) Bool)
(declare-fun role (Role) Bool)
(declare-fun role_le (Role Role) Bool)
(declare-fun role_permission_assign (Role Permission) Bool)
(declare-fun user (Id) Bool)
(declare-fun user_role_assign (Id Role) Bool)
(declare-fun can_exec_0 (Id Action) Bool)
(declare-fun can_exec_1 (Id Action) Bool)
(declare-fun executed_0 (Id Action) Bool) 
(declare-fun executed_1 (Id Action) Bool)
(declare-fun initial_pm_0 () Bool)
(declare-fun initial_wf_0 () Bool)
(declare-fun t1_receive_0_1 (Id) Bool)
(declare-fun t2_invoke_0_1 (Id) Bool)
(declare-fun t3_split_0_1 (Id) Bool)
(declare-fun t4_join_0_1 (Id) Bool)
(declare-fun t5_invoke_0_1 (Id) Bool)
(declare-fun t6_invoke_0_1 (Id) Bool)
(declare-fun t7_invokeO_0_1 (Id) Bool)
```

--------------------------------

### Z3 SMT Example: Model Finding for Unfragmented Formulas

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Demonstrates Z3's ability to find models for formulas not explicitly defined in fragments. It includes declarations for integers, functions, and assertions, followed by checks for satisfiability and model retrieval. The example also shows how to add further assertions and re-check satisfiability.

```smt2
(set-option :smt.mbqi true)
(declare-fun n () Int)
(declare-fun a_1 () Int)
(declare-fun f (Int) Int)
(declare-fun g_1 (Int) Int)
(assert (> n 0))
(assert (forall ((i Int))
        (=> (and (<= 0 i) (<= i n))
            (and (= (f 0) 0)
                 (= (f 2) 2)
                 (<= 0 (f i))
                 (<= (f i) 2)
                 (=> (= (f i) 2) (= i n))
                 (=> (= (f i) 0)
                     (or (= (f (+ i 1)) 1) (= (f (+ i 1)) 2)))
                 (=> (= (f i) 1)
                     (or (= (f (+ i 1)) 1) (= (f (+ i 1)) 2)))
                 (= (g_1 0) 0)
                 (=> (= (f i) 0) (= (g_1 (+ i 1)) 0))
                 (=> (= (f i) 1) (= (g_1 (+ i 1)) (+ (g_1 i) 1)))
                 (=> (= (f i) 2)
                     (= (g_1 (+ i 1)) (g_1 i)))
                 (=> (= (f i) 1) (< (g_1 i) a_1))
                 (=> (= (f i) 2) 
                     (and (>= (g_1 i) a_1) (> (g_1 i) 2)))))))
(check-sat)
(get-model)

(echo "Property does not hold for n > 1")
(assert (> n 1))
(check-sat)
```

--------------------------------

### Z3 SMT-LIB Example: Reset and Nonlinear Real Arithmetic

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB snippet first resets the context and then defines real variables and asserts a nonlinear equation. It checks for satisfiability and retrieves a model, showcasing Z3's specialized solver for nonlinear real arithmetic.

```smtlib
(reset)
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT-LIB Example: Nonlinear Integer Arithmetic

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB snippet demonstrates asserting a nonlinear constraint involving integer multiplication and checking for satisfiability. It showcases Z3's ability to handle some nonlinear integer problems, though it notes the general undecidability of this domain.

```smtlib
(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT-LIB Example with E-Matching

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB example demonstrates E-matching, where terms are considered equal modulo congruence and pattern matching occurs modulo ground equalities. It shows how `(f a)` and `(f (g b))` are considered equal due to asserted equalities, allowing the pattern `(f (g x))` to match and deduce `(= (f (g b)) b)`.

```smt-lib
(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((f (g x))))))
(assert (= a (g b)))
(assert (= b c))
(assert (not (= (f a) c)))
(check-sat)
```

--------------------------------

### Z3 SMT-LIB Example: Nonlinear Real Arithmetic - Unsatisfiability

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB snippet defines real variables and asserts a system of nonlinear equations. It then checks for satisfiability, demonstrating Z3's ability to prove unsatisfiability for nontrivial nonlinear real problems.

```smtlib
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)
```

--------------------------------

### Z3 SMT-LIB Example with Restrictive Pattern

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB example demonstrates the use of a restrictive pattern `(f (g x))` for quantifier instantiation. It shows how disabling auto-config and model-based quantifier instantiation (MBQI) affects the prover's ability to find a contradiction.

```smt-lib
(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((f (g x))))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)
```

--------------------------------

### Z3 SMT-LIB Example with Permissive Pattern

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB example uses a more permissive pattern `(g x)` for quantifier instantiation. Compared to the restrictive pattern, this allows Z3 to prove the formula unsatisfiable, highlighting the impact of pattern choice on completeness and performance.

```smt-lib
(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((g x)))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)
```

--------------------------------

### Quantified Bit-Vector Formulas (QBVF) in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Illustrates the use of Quantified Bit-Vector Formulas (QBVF) in Z3, which involves many-sorted first-order logic with bit-vector sorts. It supports uninterpreted functions and predicates.

```smtlib
(set-option :smt.mbqi true)
(define-sort Char () (_ BitVec 8))

(declare-fun f  (Char) Char)
(declare-fun f1 (Char) Char)
(declare-const a Char)

(assert (bvugt a #x00))
(assert (= (f1 (bvadd a #x01)) #x00))
(assert (forall ((x Char)) (or (= x (bvadd a #x01)) (= (f1 x) (f x)))))

(check-sat)
(get-model)
```

--------------------------------

### Conditional Macros with Z3 Quantifiers

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Shows how Z3 automatically detects quantifiers defining 'macros' by cases. This example defines a function 'f' based on conditions involving predicates 'p' and 'p2'.

```smtlib
(set-option :smt.mbqi true)
(declare-fun f (Int) Int)
(declare-fun p (Int) Bool)
(declare-fun p2 (Int) Bool)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int)) 
                (=> (not (p x)) (= (f x) (+ x 1)))))
(assert (forall ((x Int)) 
                (=> (and (p x) (not (p2 x))) (= (f x) x))))
(assert (forall ((x Int)) 
                (=> (p2 x) (= (f x) (- x 1)))))
(assert (p b))
(assert (p c))
(assert (p2 a))
(assert (> (f a) b))
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT-LIB: Model-Based Quantifier Instantiation (MBQI)

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Illustrates the use of Model-Based Quantifier Instantiation (MBQI) in Z3. It enables Z3 to find models and evaluate expressions within those models, useful for decision procedures and exploring formulas.

```smt-lib
(set-option :smt.mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

(assert (< (f a b) a))
(assert (> a 0))
(check-sat)
(get-model)

(echo "evaluating (f (+ a 10) 20)...")
(eval (f (+ a 10) 20))
```

--------------------------------

### Z3 Model Definition Examples

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Provides examples of how Z3 defines interpretations for constants and functions within a model. It shows the syntax for defining a constant's value and a function's behavior using conditional logic (ite).

```z3
(define-fun a () Int [val])
(define-fun f ((x!1 Int) (x!2 Bool)) Int
   (ite (and (= x!1 11) (= x!2 false)) 21 0)
)
```

--------------------------------

### Z3 SMT-LIB Example: Nonlinear Real Arithmetic - Satisfiability

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB snippet defines real variables and asserts a nonlinear equation involving cubic and linear terms. It then checks for satisfiability, illustrating Z3's capacity to find solutions for certain nonlinear real arithmetic problems.

```smtlib
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT: Injectivity using Partial Inverse and Patterns

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Shows an alternative method to assert function injectivity by defining a partial inverse and using a simpler pattern. This method aims for a linear number of instantiations.

```smt
(declare-sort A)
(declare-sort B)
(declare-fun f (A) B)
(declare-fun f-inv (B) A)
(assert (forall ((x A))
                (! (= (f-inv (f x)) x)
                   :pattern ((f x))
                   )))
(declare-const a1 A)
(declare-const a2 A)
(declare-const b B)
(assert (not (= a1 a2)))
(assert (= (f a1) b))
(assert (= (f a2) b))
(check-sat)
```

--------------------------------

### Integer Division, Modulo, and Remainder in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Demonstrates the usage of integer division (div), modulo (mod), and remainder (rem) operators in Z3. It shows how these operators work with positive and negative divisors and includes assertions for checking the results. The code also includes an example of real number division.

```SMT-LIB
(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT: Injectivity using Multi-patterns

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Demonstrates how to assert the injectivity of a function 'f' using multi-patterns in Z3 SMT. This approach helps in cases where a single pattern cannot capture all bound variables and interpreted symbols.

```smt
(declare-sort A)
(declare-sort B)
(declare-fun f (A) B)
(assert (forall ((x A) (y A))
                (! (= (f x) (f y)) (= x y))
                   :pattern ((f x) (f y))
                   ))
(declare-const a1 A)
(declare-const a2 A)
(declare-const b B)
(assert (not (= a1 a2)))
(assert (= (f a1) b))
(assert (= (f a2) b))
(check-sat)
```

--------------------------------

### Z3 Basic Declarations and Echo Command

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Demonstrates basic Z3 commands for echoing a message and declaring a constant of type Int and a function that takes an Int and a Bool, returning an Int. These are foundational for building logical formulas.

```z3
(echo "starting Z3...")
(declare-const a Int)
(declare-fun f (Int Bool) Int)
```

--------------------------------

### Bitvector Literals and Display Options in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Illustrates how to define bitvector literals in Z3 using binary, decimal, and hexadecimal notations. It also shows how to control the display format of bitvector literals using 'set-option'.

```z3
(display #b0100)
(display (\_ bv20 8))
(display (\_ bv20 7))
(display #x0a) 
(set-option :pp.bv-literals false)
(display #b0100)
(display (\_ bv20 8))
(display (\_ bv20 7))
(display #x0a)
```

--------------------------------

### Z3 Query: Unsatisfiable and Satisfiable Examples

Source: https://context7.com/z3prover/doc/llms.txt

Demonstrates how Z3 handles unsatisfiable queries with ForAll constraints and satisfiable queries. It shows the basic solve command and expected output for both cases.

```z3
solve([y == x + 1, ForAll([y], Implies(y <= 0, x < y))])
# Output: no solution

solve([y == x + 1, ForAll([y], Implies(y <= 0, x > y))])
# Output: [x = 0, y = 1]
```

--------------------------------

### Solving Quantified Formulas with QSAT Tactic

Source: https://github.com/z3prover/doc/blob/master/examples/programmingz3-tutorial-v2.ipynb

Demonstrates using the 'qsat' tactic to solve quantified formulas. It defines a recursive game-like structure using Z3's datatypes and then checks its satisfiability.

```python
from z3 import *

s = Tactic('qsat').solver()
Nat = Datatype('Nat')
Nat.declare('Z')
Nat.declare('S', ('pred', Nat))
Nat = Nat.create()
Z = Nat.Z
S = Nat.S
def move(x, y):
    return Or(x == S(y), x == S(S(y)))
def win(x, n):
    if n == 0:
        return False
    y = FreshConst(Nat)
    return Exists(y, And(move(x, y), Not(win(y, n - 1))))

s.add(win(S(S(S(S(Z)))), 3))
print(s.check())
```

--------------------------------

### Z3 SMT-LIB Example with Matching Loop Potential

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

This Z3 SMT-LIB example illustrates a scenario where a pattern `(subtype x y)` can lead to a matching loop. The instantiation of the axiom `(=> (subtype x y) (subtype (array-of x) (array-of y)))` can recursively create new terms that match the pattern, causing an undesirable infinite loop.

```smt-lib
(assert (forall (x Type) (y Type) 
  (! (=> (subtype x y) (subtype (array-of x) (array-of y)))
     :pattern ((subtype x y))
  )))
```

--------------------------------

### Z3 Logical Formula Example

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

This snippet demonstrates a complex logical formula in Z3's SMT-LIB format, involving quantifiers, logical operators (and, or), and function applications. It's used to express relationships and constraints within a system.

```z3
;; assumption 52
(assert
(forall ((?U Id)) (iff (t1_receive_0_1 ?U)
   (and (and (can_exec_0 ?U t1_receive) (and (<= 1 in_customer_crtPO_0) (<= 1 p9_initial_0)))
  (and (and (= p1_final_1 p1_final_0) (and (= p2_final_1 p2_final_0) (and (= p3_running_1 p3_running_0) (and (= p4_final_1 p4_final_0) (and (= p5_final_1 p5_final_0) (and (= p6_initial_1 p6_initial_0) (and (= p7_final_1 p7_final_0) (and (= p8_initial_1 p8_initial_0) (and (= p9_initial_1 (+ (~ 1) p9_initial_0)) (and (= p10_final_1 (+ 1 p10_final_0)) (and (= p11_final_1 p11_final_0) (and (= in_customer_crtPO_1 (+ (~ 1) in_customer_crtPO_0)) (and (= in_creator_ctrPay_1 in_creator_ctrPay_0) (and (= out_creator_ctrPay_1 out_creator_ctrPay_0) (and (= out_approverPOPayment_apprPay_1 out_approverPOPayment_apprPay_0) (and (= out_approverPO_apprPO_1 out_approverPO_apprPO_0) (and (= out_signerGRN_signGRN_1 out_signerGRN_signGRN_0) (and (= out_signerGRN_ctrsignGRN_1 out_signerGRN_ctrsignGRN_0) true))))))))))))))))))
  (forall ((?V Id) (?W Action)) (iff (executed_1 ?V ?W) (or (and (= ?V ?U) (= ?W t1_receive)) (executed_0 ?V ?W))))
  )
  )
   )))

;;assumption 53
(assert 
 (not (and initial_wf_0 (and initial_pm_0 (t1_receive_0_1 id6))))
 )

(set-info :status sat)
(check-sat)
(get-model)
```

--------------------------------

### Z3 SMT: Effectively Propositional Fragment Example

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Illustrates the effectively propositional fragment of first-order logic by axiomatizing a subtype partial order relation with the tree property. It uses Z3's ability to create auxiliary functions during model construction.

```smt
; click on edit to see the example
; Note: The actual SMT code for this example is not provided in the text, only a description.
```

--------------------------------

### Cubing for Problem Decomposition in Z3

Source: https://github.com/z3prover/doc/blob/master/examples/SMTWorkshop.ipynb

Demonstrates the 'cubing' technique in Z3, which breaks down problems into independent sub-problems. This example uses SolverFor('QF_FD') and sets a lookahead cube depth to control the decomposition process. The output shows the resulting independent sub-problems.

```python
s = SolverFor("QF_FD")
s.from_file("core.cnf")
s.set("lookahead.cube.depth", 3)
for c in s.cube():
    print(c)
```

--------------------------------

### Z3Py: Quantifier Instantiation with Patterns

Source: https://github.com/z3prover/doc/blob/master/riselive/python_courses/advanced.htm

Illustrates quantifier instantiation using patterns in Z3Py. It shows how different patterns affect Z3's ability to prove unsatisfiability and discusses the concept of matching loops.

```python
from z3 import *

# Example demonstrating pattern matching for quantifier instantiation
x, y = Ints('x y')

# Scenario 1: Less permissive pattern, Z3 fails to prove unsatisfiability
s1 = Solver()
s1.set(auto_config=False, smt_timeout=1000, model_={ 'quantifier_instantiation': 'skip' })
# Assuming 'f' and 'g' are defined functions or predicates
# s1.add(ForAll([x], Implies(f(g(x)), False), patterns=[f(g(x))]))
# print(s1.check())

# Scenario 2: More permissive pattern, Z3 proves unsatisfiability
s2 = Solver()
s2.set(auto_config=False, smt_timeout=1000, model_={ 'quantifier_instantiation': 'skip' })
# s2.add(ForAll([x], Implies(f(g(x)), False), patterns=[g(x)]))
# print(s2.check())

# Example of a matching loop scenario
s3 = Solver()
# Assuming 'subtype' is a predicate and 'array_of' is a function
# s3.add(ForAll([x, y], Implies(subtype(x, y), subtype(array_of(x), array_of(y))), patterns=[subtype(x, y)]))
# print(s3.check())
```

--------------------------------

### Define Custom Sorts in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Define new sort symbols as abbreviations for sort expressions using 'define-sort'. This command supports parameterized sorts, where parameter names are specified and used in the sort expression. Examples include defining 'Set', 'IList', 'List-Set', and 'I'.

```z3
(define-sort Set (T) (Array T Bool))
(define-sort IList () (List Int))
(define-sort List-Set (T) (Array (List T) Bool))
(define-sort I () Int)

(declare-const s1 (Set I))
(declare-const s2 (List-Set Int))
(declare-const a I)
(declare-const l IList)

(assert (= (select s1 a) true))
(assert (= (select s2 l) false))
(check-sat)
(get-model)
```

--------------------------------

### Basic Bitvector Arithmetic Operations in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Provides examples of basic arithmetic operations on bitvectors in Z3, including addition (bvadd), subtraction (bvsub), unary minus (bvneg), multiplication (bvmul), remainder (bvurem, bvsrem), modulo (bvsmod), and shifts (bvshl, bvlshr, bvashr).

```z3
(simplify (bvadd #x07 #x03)) ; addition
(simplify (bvsub #x07 #x03)) ; subtraction
(simplify (bvneg #x07)) ; unary minus
(simplify (bvmul #x07 #x03)) ; multiplication
(simplify (bvurem #x07 #x03)) ; unsigned remainder
(simplify (bvsrem #x07 #x03)) ; signed remainder
(simplify (bvsmod #x07 #x03)) ; signed modulo
(simplify (bvshl #x07 #x03)) ; shift left
(simplify (bvlshr #xf0 #x03)) ; unsigned (logical) shift right
(simplify (bvashr #xf0 #x03)) ; signed (arithmetical) shift right
```

--------------------------------

### Quantifier Elimination with Z3 Tactics

Source: https://github.com/z3prover/doc/blob/master/examples/programmingz3-tutorial-v2.ipynb

Illustrates the use of Z3 tactics for quantifier elimination. It defines a goal with quantifiers and then applies 'qe-light' and 'simplify' tactics to eliminate them.

```python
from z3 import *

x, y = Reals('x y')
g  = Goal()
g.add(2 < x, Exists(y, And(y > 0, x == y + 2)))
print(g)

t1 = Tactic('qe-light')
t2 = Tactic('simplify')
 t  = Then(t1, t2)
print(t(g))
```

--------------------------------

### Z3 Prover: Model Output Example

Source: https://github.com/z3prover/doc/blob/master/examples/TutorialISPRAS2019.ipynb

This snippet shows a typical output from the Z3 model function, detailing variable assignments and function interpretations. It's useful for understanding how Z3 represents solutions.

```text
sat
[p1 = Ptr!val!2,
 n = 1,
 p0 = Ptr!val!1,
 a = 1,
 newH = [Ptr!val!0 -> 0,
         Ptr!val!2 -> 1,
         else -> deref(Var(0))],
 deref = [else -> 0],
 ref = [else -> If(1 <= Var(0), Ptr!val!0, Ptr!val!2)],
 member = [else ->
           If(is(nil, Var(1)),
              False,
              If(head(Var(1)) == Var(0),
                 True,
                 member(Var(0), tail(Var(1)))))],
 connected = [else ->
              If(fst(next(d,
                          e,
                          Var(0),
                          Var(2),
                          next(b,
                               c,
                               Var(0),
                               Var(2),
                               next(a,
                                    b,
                                    Var(0),
                                    Var(2),
                                    pair(nil, Var(2)))))) ==
                 nil,
                 False,
                 If(member(Var(1),
                           fst(next(d,
                                    e,
                                    Var(0),
                                    Var(2),
                                    next(b,
                                        c,
                                        Var(0),
                                        Var(2),
                                        next(a,
                                        b,
                                        Var(0),
                                        Var(2),
                                        pair(nil, Var(2))))))),
                    True,
                    connected(fst(next(d,
                                       e,
                                       Var(0),
                                       Var(2),
                                       next(b,
                                        c,
                                        Var(0),
                                        Var(2),
                                        next(a,
                                        b,
                                        Var(0),
                                        Var(2),
                                        pair(nil, Var(2)))))),
                              Var(1),
                              snd(next(d,
                                       e,
                                       Var(0),
                                       Var(2),
                                       next(b,
                                        c,
                                        Var(0),
                                        Var(2),
                                        next(a,
                                        b,
                                        Var(0),
                                        Var(2),
                                        pair(nil, Var(2)))))))))],
 next = [else ->
         If(And(member(Var(0), Var(2)),
                Not(member(Var(1), Var(3)))),
            pair(cons(Var(1), fst(Var(4))),
                 cons(Var(1), snd(Var(4)))),
            Var(4))]]
```

--------------------------------

### Quantifiers and Patterns in Z3 (SMT-LIB)

Source: https://context7.com/z3prover/doc/llms.txt

Explains Z3's handling of quantified formulas using pattern-based instantiation. Shows modeling of subtype relations and guiding instantiation with patterns.

```smt2
; Modeling subtype relations with quantifiers
(declare-sort Type)
(declare-fun subtype (Type Type) Bool)

; Reflexivity
(assert (forall ((x Type)) (subtype x x)))

; Transitivity
(assert (forall ((x Type) (y Type) (z Type))
          (=> (and (subtype x y) (subtype y z))
              (subtype x z))))

; Antisymmetry
(assert (forall ((x Type) (y Type))
          (=> (and (subtype x y) (subtype y x))
              (= x y))))

(check-sat)
; Output: sat

; Patterns guide instantiation
(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const c Int)

; Pattern ((g x)) causes instantiation when g terms appear
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((g x)))))
(assert (= (g a) c))
(assert (not (= (f c) a)))
(check-sat)
; Output: unsat (pattern enables the proof)
```

--------------------------------

### Illustrate Uninterpreted Functions and Constants with Abstract Sorts in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

This example illustrates the use of uninterpreted functions and constants with abstract sorts in Z3. It declares an abstract sort 'A', constants 'x' and 'y' of sort 'A', and an uninterpreted function 'f' that maps 'A' to 'A'. Assertions are made to define relationships between these elements, and then satisfiability is checked.

```smtlib
(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)
```

--------------------------------

### Solving with Custom Datatypes (Trees)

Source: https://github.com/z3prover/doc/blob/master/examples/programmingz3-tutorial-v2.ipynb

Shows how to define and use custom datatypes in Z3, specifically a binary tree. It demonstrates solving for a non-empty tree and proving properties about it.

```python
from z3 import *
Tree = Datatype('Tree')
Tree.declare('Empty')
Tree.declare('Node', ('left', Tree), ('data', Z), ('right', Tree))
Tree = Tree.create()
t = Const('t', Tree)
solve(t != Tree.Empty)
```

```python
from z3 import *
Tree = Datatype('Tree')
Tree.declare('Empty')
Tree.declare('Node', ('left', Tree), ('data', Z), ('right', Tree))
Tree = Tree.create()
t = Const('t', Tree)
prove(t != Tree.Node(t, 0, t))
```

--------------------------------

### Model Object-Oriented Type System with Quantifiers in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Shows how to model an object-oriented type system with single inheritance using Z3. It defines a 'Type' sort and a 'subtype' predicate, asserting properties of a partial order and respecting single inheritance. The example also includes assertions for monotonicity of 'array-of' and establishes a 'root-type'.

```z3
(declare-sort Type)
(declare-fun subtype (Type Type) Bool)
(declare-fun array-of (Type) Type)
(assert (forall ((x Type)) (subtype x x)))
(assert (forall ((x Type) (y Type) (z Type))
          (=> (and (subtype x y) (subtype y z)) 
              (subtype x z)))) 
(assert (forall ((x Type) (y Type))
          (=> (and (subtype x y) (subtype y x)) 
              (= x y))))
(assert (forall ((x Type) (y Type) (z Type))
          (=> (and (subtype x y) (subtype x z)) 
              (or (subtype y z) (subtype z y)))))
(assert (forall ((x Type) (y Type))
          (=> (subtype x y) 
              (subtype (array-of x) (array-of y)))))
(declare-const root-type Type)
(assert (forall ((x Type)) (subtype x root-type)))
(check-sat)
```

--------------------------------

### Bitvector Literals and Display Options in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Shows how to define bitvector literals in Z3 using binary, decimal, and hexadecimal notations. It demonstrates how Z3 displays these literals by default and how to change the display format using the ':pp.bv-literals' option.

```SMT-LIB
(display #b0100)
(display (_ bv20 8))
(display (_ bv20 7))
(display #x0a)
(set-option :pp.bv-literals false)
(display #b0100)
(display (_ bv20 8))
(display (_ bv20 7))
(display #x0a)
```

--------------------------------

### Z3 Limitation: Cannot Prove Inductive Facts

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Illustrates Z3's limitation in proving inductive facts for recursive datatypes. The example defines a 'Nat' datatype and a function 'p' which is intended to be true for all natural numbers. Z3 enters a matching loop when trying to instantiate the universally quantified implication, highlighting that it does not inherently support proofs by induction.

```z3
(set-option :timeout 2000)
(declare-datatypes () ((Nat zero (succ (pred Nat)))))
(declare-fun p (Nat) Bool)
(assert (p zero))
(assert (forall ((x Nat)) (implies (p (pred x)) (p x))))
(assert (not (forall ((x Nat)) (p x))))
(check-sat)
(get-info :all-statistics)
```

--------------------------------

### Array Select and Store Operations in Z3

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/guide.htm

Demonstrates the basic array theory in Z3, focusing on the select and store operations. It shows how to assert properties related to array reads and writes, and checks for satisfiability under different conditions, including when indices are not equal.

```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(assert (not (= x y)))
(check-sat)
```

--------------------------------

### MaxSAT Example 1: Basic Usage in Python

Source: https://github.com/z3prover/doc/blob/master/examples/SMTWorkshop.ipynb

Demonstrates a basic MaxSAT problem setup and solution using the `maxsat` function. It defines a set of formulas `Fs` and solves for the minimum number of clauses to satisfy.

```python
a, b, c, d, e = Bools('a b c d e')
Fs = {a, Implies(a, b), Implies(b, c), Not(c)}
s = Solver()
maxsat(s, Fs)
```

--------------------------------

### Optimization with Z3 Python

Source: https://github.com/z3prover/doc/blob/master/examples/programmingz3-tutorial-v2.ipynb

Shows how to use Z3's optimization module to find a satisfying assignment that minimizes or maximizes certain soft constraints. This example adds soft constraints and checks for satisfiability.

```python
from z3 import *

s = Optimize()
a, b, c, d = Bools('a b c d')
s.add(Or(a,b), Or(Not(a), Not(b)), Or(Not(c), Not(d), Not(a)))
s.add_soft(a)
s.add_soft(b)
s.add_soft(c)
s.add_soft(d)
print(s.check())
print(s.model())
```

--------------------------------

### Define Role-Permission Assignments in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Asserts the relationship between roles and permissions using a bi-implication. This defines which permissions are assigned to specific roles.

```smtlib
;assumption 30
(assert
(forall ((?U Role) (?V Permission)) (iff (role_permission_assign ?U ?V) (or (and (= ?U POClerk) (= ?V p3)) (or (and (= ?U FinClerk) (= ?V p4)) (or (and (= ?U POAdmin) (or (= ?V p1) (= ?V p3))) (or (and (= ?U FinAdmin) (or (= ?V p5) (= ?V p4))) (or (and (= ?U Client) (or (= ?V p6) (= ?V p2))) (and (= ?U Manager) (or (= ?V p1) (or (= ?V p3) (or (= ?V p4) (= ?V p5)))))))))))))
```

--------------------------------

### Z3 Prover: Pareto Front Optimization with SMT-LIB

Source: https://github.com/z3prover/doc/blob/master/riselive/courses/optimization.html

Demonstrates how to configure Z3 Prover to find Pareto fronts by setting the 'opt.priority' option to 'pareto'. This involves defining variables, constraints, and objectives, then using Z3 to find optimal solutions considering all objectives simultaneously. The output shows the results of multiple calls to 'check-sat' and 'get-objectives'.

```smt-lib
(declare-const x Int)
(declare-const y Int)
(assert (>= 5 x))
(assert (>= x 0))
(assert (>= 4 y))
(assert (>= y 0))
(minimize x)
(maximize (+ x y))
(minimize y)
(set-option :opt.priority pareto)
(check-sat)
(get-objectives)
(check-sat)
(get-objectives)
(check-sat)
(get-objectives)
(check-sat)
(get-objectives)
```

--------------------------------

### Z3 Configuration Options in SMT-LIB

Source: https://context7.com/z3prover/doc/llms.txt

Shows how to set various configuration options in Z3 using SMT-LIB format. These options control Z3's behavior, including proof generation, model construction, and solving strategies.

```smt2
(set-option :print-success true)          ; print 'success' for commands
(set-option :produce-unsat-cores true)    ; enable unsat core extraction
(set-option :produce-models true)         ; enable model generation
(set-option :produce-proofs true)         ; enable proof generation

(declare-const x Int)
(assert (> x 0))
(check-sat)

; Reset clears all assertions and allows reconfiguration
(reset)
(set-option :smt.mbqi true)  ; enable model-based quantifier instantiation
```

--------------------------------

### Define Permission-Action Relationships in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Asserts the relationship between permissions and actions using a bi-implication. This defines which permissions are required for specific actions.

```smtlib
;assumption 28
(assert
(forall ((?U Permission) (?V Action)) (iff (permission ?U ?V) (or (and (= ?U p1) (= ?V t2_invoke)) (or (and (= ?U p2) (= ?V t5_invoke)) (or (and (= ?U p3) (= ?V t6_invoke)) (or (and (= ?U p4) (or (= ?V t7_invokeO) (= ?V t8_invokeI))) (or (and (= ?U p5) (= ?V t9_invoke)) (and (= ?U p6) (= ?V t1_receive))))))))))
```

--------------------------------

### Declare Z3 Functions

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Declares functions with specified argument types and return types. These are fundamental for defining the domain of discourse in Z3.

```smtlib
(declare-fun t8_invokeI_0_1 (Id) Bool)
(declare-fun t9_invoke_0_1 (Id) Bool)
```

--------------------------------

### SAT Solver with Finite Domain Backend

Source: https://github.com/z3prover/doc/blob/master/examples/programmingz3-tutorial-v2.ipynb

Sets up a Z3 solver specifically for Quantifier-Free Finite Domain (QF_FD) formulas, forcing it to use a SAT backend. It also configures restart parameters and includes a recursive `cube_and_conquer` function.

```python
from z3 import *

Fs = []                    # Formula
s = SolverFor("QF_FD")     # Forces to use SAT backend, only applies to finite domain formulas
s.add(Fs)
s.set("sat.restart.max", 100)
def cube_and_conquer(s):
    for cube in s.cube():
       if len(cube) == 0:
          return unknown
       if is_true(cube[0]):
          return sat     
       is_sat = s.check(cube)
       if is_sat == unknown:
          s1 = s.translate(s.ctx)
          s1.add(cube)
          is_sat = cube_and_conquer(s1)
       if is_sat != unsat:
          return is_sat
    return unsat
```

--------------------------------

### Define Package Dependency Constraint in Z3 Python

Source: https://github.com/z3prover/doc/blob/master/riselive/python_courses/guide.htm

Defines a Python function `DependsOn` that creates Z3 constraints to capture package dependency semantics. If package 'a' depends on packages 'b', 'c', and 'z', installing 'a' requires installing 'b', 'c', and 'z'.

```python
from Z3 import *

def DependsOn(pack, deps):
   return And([ Implies(pack, dep) for dep in deps ])

# Example usage:
# a = Bool('a')
# b = Bool('b')
# c = Bool('c')
# z = Bool('z')
# constraint = DependsOn(a, [b, c, z])
# print constraint
```

--------------------------------

### Z3 Optimization (MaxSAT) in SMT-LIB

Source: https://context7.com/z3prover/doc/llms.txt

Provides an example of how to set up an optimization problem in Z3 using SMT-LIB format. This example focuses on MaxSAT, aiming to maximize the number of satisfied soft constraints.

```smt2
; MaxSAT: maximize satisfied soft constraints
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (or a b))
(assert (or (not a) (not b)))
(assert (or (not c) (not a)))

; Soft constraints - maximize how many are true
; Z3's optimize solver handles this
```

--------------------------------

### Define User-Role Assignments in Z3

Source: https://github.com/z3prover/doc/blob/master/src/guide.html

Asserts the relationship between users (IDs) and roles using a bi-implication. This defines which roles are assigned to specific user IDs.

```smtlib
;assumption 29
(assert
(forall ((?U Id) (?V Role)) (iff (user_role_assign ?U ?V) (or (and (= ?U id7) (= ?V Manager)) (or (and (= ?U id1) (= ?V Manager)) (or (and (= ?U id2) (= ?V FinAdmin)) (or (and (= ?U id3) (= ?V FinClerk)) (or (and (= ?U id4) (= ?V POAdmin)) (or (and (= ?U id5) (= ?V POClerk)) (and (= ?U id6) (= ?V Client)))))))))))
```