# Z3 is an SMT solver. A tool that can be used to check if a logic formula is satisfiable, 
# i.e. the variables in the formula can be assigned in a way such that the formula becomes true.
# In this course you will interact with Z3 using its Python API.

import z3

# get the solver
solver = z3.Solver()

# *** Basic functionality ***

# Create boolean variables "a" and "b"
a = z3.Bool('a')
b = z3.Bool('b')
# Build a formula f1 consisting of the conjunction of a and b
f1 = z3.And(a, b)

# Check if the formula f1 is satisfiable.
res = solver.check(f1) # return satisfiable/unsatisfiable/undefined
if res == z3.sat:
  # There is a variable assingment for which f1 is true.
  print("The formula is satisfiable.") 
  print(solver.model()) # Get a variable assignment for which f1 is true.
else if res == z3.unsat:
  # The formula f1 is false for all possible variable assignments.
  print("The formula is unsatisfiable.")
else:
  # This should not happen during the exercise. All formulas you have to create should be either sat or unsat.
  print("The solver could not determine the status of the formula.")

# Check a formula with disjunction and negation.
print(solver.check(z3.Or(a, z3.Not(a))))

# ** Side Note **
# Instead of calling check with a paramter you can also add a formula to the solver.
solver.add(f1)
# Checks satisfiablility of the conjunction of all added formulas.
solver.check()
# Reset the solver and removes all added formulas.
solver.reset()


# *** Formulas with integers variables ***
# Define integer variables "x", "y" and "z"
x = z3.Int('x')
y = z3.Int('y')
z = z3.Int('z')
# arithmetic operations and implication
f2 = z3.Implies((x - y > 0), y > x)
print(solver.check(f2))

# *** Using Z3 to prove a formula is valid i.e. true for all variable assignments. ***
# A formula is valid iff its negation is unsatisfiable.
print(solver.check(z3.Not(f2)) == z3.unsat)


# *** Explicitly creating literals ***
# In most cases Z3 implicitly converts Python literals (true,false,1,2,3,...) to Z3 formulas.
# However, when creating formulas in a program it is recomended to do this explicitly unsing z3.BoolVal and z3.IntVal.
print(solver.check(z3.IntVal(1) != z3.IntVal(2)))
print(solver.check(z3.BoolVal(True) == z3.And(z3.Bool('a'), z3.Not(z3.Bool('a')))))

# *** Arrays ***
# Defines an array variable "a1" with integer indices and interger values.
a1 = z3.Array('a', z3.IntSort(), z3.IntSort())
# Insert the value 1 at index 0. This returns a new array.
a2 = z3.Store(a1, 0, 1)
# Select accesses the value stored in an array at a given index.
print(solver.check(z3.Select(a2, 0) == 1))
a3 = z3.Store(a2, 1, 1)
# Quantified formulas can be created using z3.ForAll and z3.Exists.
# The first argument is a list of variables that should be bound by the quantifier and
# the second argument is a formula that can contain these (and other) variables.
i = z3.Int('i')
print(solver.check(z3.ForAll([i], z3.Implies(z3.And(i >= 0, i < 2), z3.Select(a3, i) == 1))))
print(solver.check(z3.Exists([i], z3.And(i >= 0, i < 2, z3.Select(a3, i) == 2))))