# IAL-501 (Prof. Dr. Silvio do Lago Pereira)

from util import *

#-----------------------------------------------------------
# Exemplo 1
#-----------------------------------------------------------

def A(x): return chr(ord(x) - ord('a') + ord('A'))

#-----------------------------------------------------------
# Exemplo 6
#-----------------------------------------------------------

def zero(a,b):
    sat(s0=True)
    x = -b/a
    sat()
    return x

#-----------------------------------------------------------
# Exemplo 7
#-----------------------------------------------------------

def z(a,b):
    sat('a != 0', s0=True)
    x = b/a
    sat('a*x + b == 0')
    return x

#-----------------------------------------------------------
# Exercicio 1
#-----------------------------------------------------------

def menor(x,y):
    sat(s0=True)
    if x < y: 
       m = x
       sat()
    else:   
       m = y
       sat()
    sat()
    return m

#-----------------------------------------------------------
# Exemplo 8
#-----------------------------------------------------------

def inc(v,i):
    sat(s0=True)
    v[i] = v[i] + 1
    sat('v[i] == $v[i]+1')

#-----------------------------------------------------------
# Exercicio 2
#-----------------------------------------------------------

def troca(v,i,j):
    sat(s0=True)
    x = v[i];    sat()
    v[i] = v[j]; sat()
    v[j] = x;    sat()

#-----------------------------------------------------------
# Exercicio 3
#-----------------------------------------------------------

def raiz(v):
    sat()
    n = len(v)
    for i in range(n):
        r = 0
        while r*r <= v[i]: 
            r += 1
        v[i] = r - 1
    sat()

#-----------------------------------------------------------
# Exercicio 5
#-----------------------------------------------------------

def enigma(v,i,j):
    sat(s0=True)
    v[i] = v[i] + v[j]; sat()
    v[j] = v[i] - v[j]; sat()
    v[i] = v[i] - v[j]; sat()