### Configure tactics with parameters and use aig

Source: https://microsoft.github.io/z3guide/docs/strategies/tactics

Demonstrates using 'using-params' to configure the 'simplify' tactic and includes 'aig' for compressing Boolean formulas. This example also shows how to get the value of an expression.

```z3
(declare-const x (_ BitVec 16))

(declare-const y (_ BitVec 16))



(assert (= (bvadd (bvmul (_ bv32 16) x) y) (_ bv13 16)))

(assert (bvslt (bvand x y) (_ bv10 16)))

(assert (bvsgt y (bvneg (_ bv100 16))))



(check-sat-using (then (using-params simplify :mul2concat true)

                       solve-eqs 

                       bit-blast 

                       aig

                       sat))

(get-model)

(get-value ((bvand x y)))
```

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

### Install Z3 Python Bindings

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Use this command to install the Z3 Python solver library. Ensure you have pip installed.

```bash
pip install z3-solver
```

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

### First installation check with refined functions

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This demonstrates the first check using the refined install_check function with a specific set of dependencies and conflicts. It prints the resulting installation profile or an invalid message.

```python
print ("Check 1")

install_check(DependsOn(a, [b, c, z]),

              DependsOn(b, d),

              DependsOn(c, [Or(d, e), Or(f, g)]),

              Conflict(d, e),

              Conflict(d, g),

              a, z)
```

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

### Second installation check with refined functions

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This demonstrates the second check using the refined install_check function, including an additional package 'g' in the constraints. It again prints the resulting installation profile or an invalid message.

```python
print ("Check 2")

install_check(DependsOn(a, [b, c, z]),

              DependsOn(b, d),

              DependsOn(c, [Or(d, e), Or(f, g)]),

              Conflict(d, e),

              Conflict(d, g),

              a, z, g)
```

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

### Difference Logic Example with Optimization

Source: https://microsoft.github.io/z3guide/docs/optimization/advancedtopics

An example demonstrating the use of difference logic with maximization. It declares integer variables, asserts constraints, and then seeks to maximize a linear combination of these variables.

```smt-lib
(declare-const x Int)

(declare-const y Int)

(assert (>= 10 x))

(assert (>= x (+ y 7)))

(maximize (+ x y))

(check-sat)

(get-objectives)
```

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

### MBQI Example with Quantifiers

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example uses the :smt.mbqi option for quantifier reasoning. It defines functions and sorts, then asserts quantified properties and checks for satisfiability.

```smt
(set-option :smt.mbqi true)

(declare-sort S)

(declare-fun g (S S) S)
(declare-fun f (S S) S)

(declare-const a S)
(declare-const b S)



(assert (forall ((x S) (y S))
                (= (g (f x y) (f x x)) x)))
(assert (forall ((x S) (y S))
                (= (f (g x y) (g x x)) x)))
(assert (forall ((x S) (y S) (z S))
                (= (g (g x y) z) (g (g y z) x))))
(assert (forall ((x S) (y S) (z S))
                (= (f (f x y) z) (f (f y z) x))))
(assert (distinct (g a (f b a)) (f a (g b a))))

(check-sat)

```

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

### Infinite Model Example

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example illustrates a formula that only has infinite models, which can cause Z3 to diverge. It defines functions and asserts properties about them.

```smt
(set-option :smt.mbqi true)

(declare-sort S)

(declare-fun g (S) S)
(declare-fun f (S) S)

(declare-const a S)

(assert (forall ((x S)) (= (g (f x)) x)))
(assert (forall ((x S)) (not (= a (f x)))))

(check-sat)

(get-model)

```

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

### List Available Simplifiers

Source: https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Use the `(help-simplifier)` command to list all available simplifiers and get information about their parameters.

```z3
(help-simplifier)
```

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

### String Constraints Example

Source: https://microsoft.github.io/z3guide/docs/theories/Strings

Demonstrates asserting constraints on string concatenations and non-empty strings to find a solution.

```smtlib
(declare-const a String)

(declare-const b String)

(declare-const c String)

(assert (= (str.++ a b) "abcd"))

(assert (= (str.++ b c) "cdef"))

(assert (not (= b "")))

(check-sat)
```

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

### Apply qfnra-nlsat Tactic

Source: https://microsoft.github.io/z3guide/docs/strategies/summary

This example demonstrates how to declare constants, assert nonlinear arithmetic constraints, and then apply the `qfnra-nlsat` tactic to solve the resulting goal.

```z3
(declare-const x Real)

(declare-const y Real)

(assert (> (* x x) (* y x)))

(assert (> x 0))

(assert (< y 1))

(apply qfnra-nlsat)

```

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

### Encode and solve install problem

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This snippet encodes an example install problem using Z3Py, including dependencies and conflicts, and then solves it. It demonstrates the combined use of DependsOn and Conflict functions.

```python
def DependsOn(pack, deps):

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


def Conflict(p1, p2):

    return Or(Not(p1), Not(p2))

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')


solve(DependsOn(a, [b, c, z]),

      DependsOn(b, [d]),

      DependsOn(c, [Or(d, e), Or(f, g)]),

      Conflict(d, e),

      a, z)
```

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

### Z3 Proof Trimming Configuration

Source: https://microsoft.github.io/z3guide/programming/Proof%20Logs

Configure Z3 to enable proof logging and set the default tactic to SMT. This setup is necessary before trimming proofs.

```z3
(set-option :sat.euf true)  
(set-option :tactic.default_tactic smt)  
(set-option :solver.proof.log log.smt2)  
(declare-const a Bool)  
(declare-const b Bool)  
(declare-const c Bool)  
(declare-const d Bool)  
  
(assert (or a (not b)))  
(assert (or b (not c)))  
(assert (or c (not d)))  
(assert (or d (not a)))  
(assert a)  
(assert (not c))  
(check-sat)  

```

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

### String Equality and Inequality Constraints

Source: https://microsoft.github.io/z3guide/docs/theories/Strings

Example showing string equality and inequality constraints, including checking for non-trivial overlaps and retrieving a model.

```smtlib
(declare-const a String)

(declare-const b String)

(declare-const c String)

(assert (= (str.++ a "ab" b) (str.++ b "ba" c)))

(assert (= c (str.++ a b)))

(assert (not (= (str.++ a "a") (str.++ "a" a))))

(check-sat)

(get-model)
```

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

### Combine Splitting and Solving

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

Chains multiple tactics using 'Then'. This example first repeatedly splits clauses and then applies 'solve-eqs' to simplify the resulting goal.

```python
x, y, z = Reals('x y z')

g = Goal()

g.add(Or(x == 0, x == 1), 
      Or(y == 0, y == 1), 
      Or(z == 0, z == 1),
      x + y + z > 2)


# Split all clauses and solve equations
split_solve = Then(Repeat(OrElse(Tactic('split-clause'),
                                 Tactic('skip'))),
                   Tactic('solve-eqs'))


print (split_solve(g))
```

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

### Sequence Insertion Example

Source: https://microsoft.github.io/z3guide/docs/theories/Sequences

Demonstrates inserting an element into a sequence and checking for resulting properties like length and element changes. This example verifies that inserting 'b' at or after position 8, but before the string length, results in a string of the same length, with either character 8 or 9 unchanged.

```z3
(declare-const s (Seq Int))

(declare-const t (Seq Int))

(declare-const j Int)

(declare-const b Int)



(assert (<= 10 (seq.len s)))

(assert (<= 8 j))

(assert (< j (seq.len s)))

(assert (= t (seq.++ (seq.extract s 0 j) (seq.unit b) (seq.extract s (+ j 1) (- (seq.len s) j 1)))))

(push)

(assert (not (= (seq.unit b) (seq.at t j))))

(check-sat)

(pop)

(push)

(assert (not (= (seq.len s) (seq.len t))))

(check-sat)

(pop)

(push)

(assert (not (= (seq.at s 8) (seq.at t 8))))

(assert (not (= (seq.at s 9) (seq.at t 9))))

(check-sat)

(pop)
```

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

### Sequence Map Example

Source: https://microsoft.github.io/z3guide/docs/theories/Sequences

Applies a mapping function to each element of a sequence and asserts properties about the resulting sequence. This example doubles each integer in sequence 's' to create sequence 't' and checks if 't' has a length greater than 3.

```z3
(declare-const s (Seq Int))

(declare-const t (Seq Int))



(assert (= t (seq.map (lambda ((x Int)) (* x 2)) s)))

(assert (> (seq.len t) 3))

(check-sat)

(get-model)
```

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

### Z3 with Macro Finder Enabled

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example shows how to enable the macro-finder preprocessor option in Z3. This can improve the performance of the model finder by expanding quantifiers representing macros at preprocessing time.

```z3
(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)
```

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

### Non-linear Arithmetic Example

Source: https://microsoft.github.io/z3guide/docs/theories/Arithmetic

Demonstrates Z3's handling of non-linear arithmetic constraints. Z3 may return 'unknown' or loop for some non-linear problems, but can also prove unsatisfiability for others.

```smt-lib
(declare-const a Int)

(assert (< (* a a) 3))

(check-sat)

(get-model)



(echo "Z3 does not always find solutions to non-linear problems")

(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (sin (* b c))) 7))

(check-sat)



(echo "yet it can show unsatisfiability for some nontrivial nonlinear problems...")

(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)



(reset)

(echo "When presented only non-linear polynomial constraints over reals, Z3 uses a specialized complete solver")

(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

(get-model)
```

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

### Compose Tactics with Then

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

Combines two tactics, applying the first to the input goal and the second to each resulting subgoal. This example uses 'simplify' and 'solve-eqs' to process a goal.

```python
x, y = Reals('x y')

g  = Goal()

g.add(x > 0, y > 0, x == y + 2)

print (g)


t1 = Tactic('simplify')
t2 = Tactic('solve-eqs')
t  = Then(t1, t2)

print (t(g))
```

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

### Create Solver using 'smt' Tactic

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

The 'smt' tactic wraps the main Z3 solver. This example demonstrates creating a solver using the 'smt' tactic and adding an integer constraint.

```python
x, y = Ints('x y')
s = Tactic('smt').solver()
s.add(x > y + 1)
print (s.check())
print (s.model())
```

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

### Quantified Bit-Vector Formula Example

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This snippet demonstrates a quantified bit-vector formula (QBVF) with assertions and a query for satisfiability. It defines custom sorts and functions, asserting conditions on variables and functions.

```smt
(set-option :smt.mbqi true)

(define-sort AsciiChar () (_ BitVec 8))



(declare-fun f  (AsciiChar) AsciiChar)

(declare-fun f1 (AsciiChar) AsciiChar)

(declare-const a AsciiChar)



(assert (bvugt a #x00))

(assert (= (f1 (bvadd a #x01)) #x00))

(assert (forall ((x AsciiChar)) (or (= x (bvadd a #x01)) (= (f1 x) (f x)))))



(check-sat)

(get-model)
```

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

### Array Property Fragment Example

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

Demonstrates array updates and assertions about sortedness using SMT-LIB. This is useful for verifying properties of array manipulations.

```smtlib
(set-option :smt.mbqi true)

(set-option :model.compact true)



;; A0, A1, A2, A3, A4 are "arrays" from Integers to Integers.

(declare-fun A0 (Int) Int) (declare-fun A1 (Int) Int)

(declare-fun A2 (Int) Int) (declare-fun A3 (Int) Int)

(declare-fun A4 (Int) Int) 

(declare-const n Int) (declare-const l Int)

(declare-const k Int) (declare-const x Int)

(declare-const y Int) (declare-const w Int)

(declare-const z Int)



;; A1 = A0[k <- w]

(assert (= (A1 k) w))

(assert (forall ((x Int)) (or (= x k) (= (A1 x) (A0 x)))))



;; A2 = A1[l <- x] = A0[k <- w][l <- x]

(assert (= (A2 l) x))

(assert (forall ((x Int)) (or (= x l) (= (A2 x) (A1 x)))))



;; A3 = A0[k <- y]

(assert (= (A3 k) y))

(assert (forall ((x Int)) (or (= x k) (= (A3 x) (A0 x)))))



;; A4 = A3[l <- z] = A0[k <- y][l <- z] 

(assert (= (A3 l) z))

(assert (forall ((x Int)) (or (= x l) (= (A4 x) (A3 x)))))



(assert (and (< w x) (< x y) (< y z)))

(assert (and (< 0 k) (< k l) (< l n)))

(assert (> (- l k) 1))



;; A2 is sorted in the interval [0,n-1]

(assert (forall ((i Int) (j Int))

                (=> (and (<= 0 i) (<= i j) (<= j (- n 1)))

                    (<= (A2 i) (A2 j)))))



(check-sat)

(get-model)



;; A4 is sorted in the interval [0,n-1]

(assert (forall ((i Int) (j Int))

                (=> (and (<= 0 i) (<= i j) (<= j (- n 1)))

                    (<= (A4 i) (A4 j)))))



(check-sat)

```

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

### Knights and Knaves Puzzle: Basic Setup

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

Sets up the domain for the Knights and Knaves logic puzzle, defining inhabitants, their identities (Knight/Knave), and the rules of truth-telling and lying.

```smt-lib
(declare-sort Inhabitant)

(declare-datatype Statement (truth falsity))

(declare-datatype Identity (Knave Knight))

(declare-const John Inhabitant)

(declare-const Bill Inhabitant)

(declare-fun Is (Inhabitant Identity) Statement)

(declare-fun Says (Inhabitant Statement) Bool)

(declare-fun Holds (Statement) Bool)

(assert (Holds truth))

(assert (not (Holds falsity)))

(assert (forall ((x Inhabitant)) (xor (Holds (Is x Knave)) (Holds (Is x Knight)))))

(assert (forall ((x Inhabitant) (y Statement)) (=> (Holds (Is x Knave)) (Says x y) (not (Holds y)))))

(assert (forall ((x Inhabitant) (y Statement)) (=> (Holds (Is x Knight)) (Says x y) (Holds y))))
```

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

### Z3 Formula with Quantifiers

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example demonstrates a Z3 formula with quantifiers, including universal quantifiers (forall) and implications (=>). It defines functions and asserts properties that Z3 attempts to satisfy.

```z3
(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)
```

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

### Using AstVector in Z3 JavaScript

Source: https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples

Demonstrates the use of Z3's AstVector to manage a collection of Z3 arithmetic expressions. This example adds constraints to ensure distinct integer values.

```javascript
const solver = new Z3.Solver();



const vector = new Z3.AstVector<Arith>();

for (let i = 0; i < 5; i++) {

    vector.push(Z3.Int.const(`int__${i}`));

}



const length = vector.length();

for (let i = 0; i < length; i++) {

    solver.add((vector.get(i) as Arith).gt(1));

}

solver.add(Z3.Distinct(...vector));

await solver.check();

solver.model()
```

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

### Combine Tactic with Solver and Model Conversion

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

This example shows how to apply a tactic to a goal, obtain subgoals, select one, and solve it using a solver. It also demonstrates using model converters to transform a subgoal's model into a model for the original goal.

```python
t = Then('simplify', 
         'normalize-bounds', 
         'solve-eqs')

x, y, z = Ints('x y z')
g = Goal()
g.add(x > 10, y == x + 3, z > y)

r = t(g)
# r contains only one subgoal
print (r)

s = Solver()
s.add(r[0])
print (s.check())
# Model for the subgoal
print (s.model())
# Model for the original goal
print (r[0].convert_model(s.model()))
```

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

### Configure Solver with 'With' and 'aig' Tactic

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

This example shows how to configure a solver using the 'With' combinator for specific options like 'mul2concat=True' and includes the 'aig' tactic for compressing Boolean formulas. It then adds constraints and prints the check result and model.

```python
bv_solver = Then(With('simplify', mul2concat=True),
                 'solve-eqs',
                 'bit-blast',
                 'aig',
                 'sat').solver()
x, y = BitVecs('x y', 16)
bv_solver.add(x*32 + y == 13, x & y < 10, y > -100)
print (bv_solver.check())
m = bv_solver.model()
print (m)

print (x*32 + y, "==", m.evaluate(x*32 + y))
print (x & y, "==", m.evaluate(x & y))
```

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

### Define DependsOn function

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This function creates Z3 constraints to capture the semantics of a 'depends on' clause. It ensures that if a package is installed, all its dependencies must also be installed.

```python
def DependsOn(pack, deps):

   return And([ Implies(pack, dep) for dep in deps ])
```

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

### Z3 Function Declaration Example

Source: https://microsoft.github.io/z3guide/docs/theories/Arrays

An example of a function declaration in Z3. This declaration defines the signature for a function `f` that takes an Integer and a Boolean, returning a Real.

```z3
(declare-fun f (Int Bool) Real)
```

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

### Generate DependsOn constraint

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This shows the Z3 constraint generated by DependsOn(a, [b, c, z]). It means if package 'a' is installed, then packages 'b', 'c', and 'z' must also be installed.

```z3py
And(Implies(a, b), Implies(a, c), Implies(a, z))
```

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

### Custom Z3 Simplifier Example

Source: https://microsoft.github.io/z3guide/programming/Example%20Programs/Formula%20Simplification

This example demonstrates the usage of a custom Z3 simplifier. It defines a term and a constraint, then uses the custom simplify function to reduce the term based on the model.

```python
H = Int('H')  
s = Solver()  
t = 4 + 4 * (((H - 1) / 2) / 2)  
s.add(H % 4 == 0)  
s.check()  
m = s.model()  
print(t, "-->", simplify(s, m, t))  
```

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

### Complex Quantified Formula Example

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example showcases a complex formula with nested quantifiers, demonstrating Z3's ability to handle intricate logical structures. It includes assertions and checks for satisfiability.

```smt
(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))))
  )
  )
   )))

```

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

### Basic Datalog Relations, Rules, and Queries

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Fixedpoints

Illustrates declaring relations, rules, and posing queries in the Datalog engine. Use this to understand basic fixed-point computations.

```python
fp = Fixedpoint()


a, b, c = Bools('a b c')


fp.register_relation(a.decl(), b.decl(), c.decl())
fp.rule(a,b)
fp.rule(b,c)
fp.set(engine='datalog')


print ("current set of rules\n", fp)

print (fp.query(a))


fp.fact(c)
print ("updated set of rules\n", fp)

print (fp.query(a))

print (fp.get_answer())
```

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

### Import Formula from String

Source: https://microsoft.github.io/z3guide/programming/Example%20Programs/MBQI

Imports a Z3 formula from a string representation. Ensure Z3 is installed and imported.

```python
from z3 import *

s = Solver()
s.from_string("""
(define-fun s4 () (_ BitVec 1) #b0)
(declare-fun s0 () (_ BitVec 64))
(declare-fun s1 () (_ BitVec 64))
(assert (forall ((s2 (_ BitVec 64))) 
            (let ((s3 ((_ extract 7 7) s2)))
            (let ((s5 (distinct s3 s4)))
            (let ((s6 (bvand s0 s2)))
            (let ((s7 (bvmul s1 s6)))
            (let ((s8 ((_ extract 56 56) s7)))
            (let ((s9 (distinct s4 s8)))
            (let ((s10 (= s5 s9)))
            (let ((s11 ((_ extract 15 15) s2)))
            (let ((s12 (distinct s4 s11)))
            (let ((s13 ((_ extract 57 57) s7)))
            (let ((s14 (distinct s4 s13)))
            (let ((s15 (= s12 s14)))
            (let ((s16 ((_ extract 23 23) s2)))
            (let ((s17 (distinct s4 s16)))
            (let ((s18 ((_ extract 58 58) s7)))
            (let ((s19 (distinct s4 s18)))
            (let ((s20 (= s17 s19)))
            (let ((s21 ((_ extract 31 31) s2)))
            (let ((s22 (distinct s4 s21)))
            (let ((s23 ((_ extract 59 59) s7)))
            (let ((s24 (distinct s4 s23)))
            (let ((s25 (= s22 s24)))
            (let ((s26 ((_ extract 39 39) s2)))
            (let ((s27 (distinct s4 s26)))
            (let ((s28 ((_ extract 60 60) s7)))
            (let ((s29 (distinct s4 s28)))
            (let ((s30 (= s27 s29)))
            (let ((s31 ((_ extract 47 47) s2)))
            (let ((s32 (distinct s4 s31)))
            (let ((s33 ((_ extract 61 61) s7)))
            (let ((s34 (distinct s4 s33)))
            (let ((s35 (= s32 s34)))
            (let ((s36 ((_ extract 55 55) s2)))
            (let ((s37 (distinct s4 s36)))
            (let ((s38 ((_ extract 62 62) s7)))
            (let ((s39 (distinct s4 s38)))
            (let ((s40 (= s37 s39)))
            (let ((s41 ((_ extract 63 63) s2)))
            (let ((s42 (distinct s4 s41)))
            (let ((s43 ((_ extract 63 63) s7)))
            (let ((s44 (distinct s4 s43)))
            (let ((s45 (= s42 s44)))
            (let ((s46 (and s40 s45)))
            (let ((s47 (and s35 s46)))
            (let ((s48 (and s30 s47)))
            (let ((s49 (and s25 s48)))
            (let ((s50 (and s20 s49)))
            (let ((s51 (and s15 s50)))
            (let ((s52 (and s10 s51)))
            s52)))))))))))))))))))))))))))))))))))))))))))))))))))  

")  

```

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

### Create Bit-Vector Solver

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

This snippet demonstrates creating a basic bit-vector solver using 'simplify', 'solve-eqs', 'bit-blast', and 'sat' tactics. It then uses this solver to check satisfiability for given bit-vector constraints.

```python
bv_solver = Then('simplify', 
                 'solve-eqs',
                 'bit-blast',
                 'sat').solver()

x, y = BitVecs('x y', 16)
solve_using(bv_solver, x | y == 13, x > y)
```

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

### Use Comments in Z3Py

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Comments in Z3Py start with `#` and extend to the end of the line, similar to Python. Multi-line comments are not supported.

```python
# This is a comment
x = Real('x') # comment: creating x
print (x**2 + 2*x + 2)  # comment: printing polynomial
```

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

### Get Z3 AST ID

Source: https://microsoft.github.io/z3guide/programming/Example%20Programs/Cores%20and%20Satisfying%20Subsets

Retrieves the unique identifier for a Z3 AST node. This is a utility function used internally by the solvers.

```python
def get_id(x):

    return Z3_get_ast_id(x.ctx.ref(),x.as_ast())
```

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

### Quantifier Instantiation with Pattern (f (g x))

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example demonstrates quantifier instantiation using the pattern (f (g x)). When no ground instance of this pattern exists, Z3 fails to prove unsatisfiability. Model-based quantifier instantiation and saturation engines are disabled.

```smt
(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)

```

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

### Lambdas as Arrays and Function Spaces

Source: https://microsoft.github.io/z3guide/docs/logic/Lambdas

Demonstrates the equivalence of lambdas and arrays in Z3, showing how to convert functions to arrays using `as-array` and vice versa.

```z3
(declare-fun f (Int) Int)

(push)

(assert (not (=  (select (_ as-array f) 0) (f 0))))

(check-sat)

(pop)

(push)

(declare-const a (Array Int Int))

(define-fun-rec f2 ((x Int)) Int (select a x))

(assert (not (= (select a 0) (select (_ as-array f2) 0))))

(check-sat)

(pop)
```

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

### Get Reason Unknown Info in Z3

Source: https://microsoft.github.io/z3guide/docs/strategies/tactics

Use the `get-info` tactic with `:reason-unknown` to retrieve information about why Z3 could not determine a definitive answer.

```z3
(get-info :reason-unknown)
```

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

### MapSolver initialization

Source: https://microsoft.github.io/z3guide/programming/Example%20Programs/Cores%20and%20Satisfying%20Subsets

Initializes the MapSolver with the number of constraints. It sets up an internal Z3 solver and a set of all constraint indices.

```python
class MapSolver:

   def __init__(self, n):

       """Initialization.

             Args:

            n: The number of constraints to map.

       """

       self.solver = Solver()

       self.n = n

       self.all_n = set(range(n))  # used in complement fairly frequently
```

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

### Define Conflict function

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

This function creates Z3 constraints to capture the semantics of a 'conflicts with' clause. It ensures that two specified packages cannot be installed simultaneously.

```python
def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))
```

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

### Combine Polynomial and Boolean Constraints

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Illustrates solving a problem involving both polynomial (x < 5) and boolean (p) constraints. Requires Z3 to be installed.

```python
p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
```

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

### Basic Z3 Solver API Usage

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Demonstrates the fundamental Z3 Solver API, including creating a solver, adding constraints, checking satisfiability, and managing scopes with push/pop. Constraints are asserted using s.add() and checked with s.check().

```python
x = Int('x')
y = Int('y')

s = Solver()
print (s)

s.add(x > 10, y == x + 2)
print (s)

print ("Solving constraints in the solver s ...")
print (s.check())


print ("Create a new scope...")
s.push()
s.add(y < 11)
print (s)

print ("Solving updated set of constraints...")
print (s.check())


print ("Restoring state...")
s.pop()
print (s)
print ("Solving restored set of constraints...")
print (s.check())
```

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

### Division by Zero Handling

Source: https://microsoft.github.io/z3guide/docs/theories/Arithmetic

Illustrates Z3's behavior with division by zero, where the result is under-specified and constraints involving it can still be satisfiable. All functions in Z3 are total.

```smt-lib
(declare-const a Real)

; The following formula is satisfiable since division by zero is not specified.

(assert (= (/ a 0.0) 10.0)) 

(check-sat)

(get-model)



; Although division by zero is not specified, division is still a function.

; Therefore, (/ a 0.0) cannot evaluate to both 10.0 and 2.0.

(assert (= (/ a 0.0) 2.0))

(check-sat)
```

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

### Higher-Order Reasoning with Quantifiers

Source: https://microsoft.github.io/z3guide/docs/logic/Lambdas

Shows a limited example of higher-order reasoning by using a quantified variable of array type, which Z3 instantiates with a lambda expression.

```z3
(declare-const x Int)

(declare-const y Int)

(assert (forall ((q (Array Int Bool))) (= (q x) (q y))))

(assert (not (= x y)))

(check-sat)
```

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

### Unbounded Maximize Objective in Z3

Source: https://microsoft.github.io/z3guide/docs/optimization/arithmeticaloptimization

Z3 indicates that maxima are at infinity for unbounded objective functions. This example demonstrates a scenario where the maximization objective is unbounded.

```smtlib
(declare-const x Int)

(declare-const y Int)

(assert (< x 2))

(assert (> (- y x) 1))

(maximize (+ x y))

(check-sat)
```

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

### List Built-in Tactics with help-tactic

Source: https://microsoft.github.io/z3guide/docs/strategies/probes

Use `(help-tactic)` to list all available built-in tactics in Z3. This is useful for exploring Z3's capabilities.

```z3
(help-tactic)
```

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

### Create a Specialized Solver with Simplifiers

Source: https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Use the `(set-simplifier)` command to create a specialized solver by defining a sequence of pre-processing simplification steps.

```z3
(set-simplifier (then simplify solve-eqs elim-unconstrained propagate-values simplify qe-light simplify qe-light))
```

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

### List available Z3Py probes

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Strategies

Use describe_probes() to get a list of all built-in probes in Z3Py. This is useful for understanding available measures for goal evaluation.

```python
describe_probes()
```

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

### Solve Boolean Constraints with Z3

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Demonstrates solving a set of boolean constraints using Z3's Implies, Not, and Or operators. Ensure Z3 is installed and imported.

```python
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))
```

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

### Create and Use Z3 Rational Numbers

Source: https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction

Demonstrates correct ways to create Z3 rational numbers using `Q(num, den)` or `RealVal()`, and shows how Python's default division differs. It also shows creating rationals from strings and decimals.

```python
print (1/3)
print (RealVal(1)/3)
print (Q(1,3))

x = Real('x')
print (x + 1/3)
print (x + Q(1,3))
print (x + "1/3")
print (x + 0.25)
```

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

### Satisfiable Formula with Nested Quantifiers

Source: https://microsoft.github.io/z3guide/docs/logic/Quantifiers

This example demonstrates a satisfiable formula with nested quantifiers. The option `(set-option :smt.pull-nested-quantifiers true)` can be used to simplify such formulas for Z3.

```smt
(set-option :smt.pull-nested-quantifiers true)

(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 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)

```