Z3 es un demostrador de teoremas moderno de Microsoft Research. Puede ser usado para verificar la satisfactibilidad de fórmulas lógicas sobre una o más teorías. Es una herramienta de bajo nivel que es usada a menudo como un componente en el contexto de otras herramientas que requieren resolver fórmulas lógicas.
El formato de entrada de Z3 es una extensión del formato definido por el estándar SMT-LIB 2.0. Un script Z3 es una secuencia de comandos. Z3 mantiene una pila de fórmulas y declaraciones proveídas por el usuario.
El conjunto de fórmulas en la pila de Z3 es satisfactible si existe una interpretación (para las constantes y funciones declaradas por el usuario) que hace verdaderas a todas las fórmulas asertadas. Cuando el comando check-sat devuelve sat, el comando get-model puede ser usado para conseguir una interpretación que hace verdaderas a todas las fórmulas en la pila interna de Z3.
Podemos comprobar aserciones de lógica proposicional usando funciones que representan las proposiciones x e y. Por ejemplo, copiá y pegá lo siguiente en la interfaz en línea de Z3 en http://www.rise4fun.com/z3 y apretá el botón reproducir. Eso comprueba si ¬(x ∧ y)≡(¬x ∨ ¬y):
(declare-fun x () Bool)
(declare-fun y () Bool)
(assert ( = (not(and x y)) (or (not x)(not y))))
(check-sat)El comando check-sat determina si las fórmulas actuales en la pila Z3 son satisfactibles o no. Si no son satisfactibles, Z3 devuelve unsat. Z3 puede también devolver unknown cuando no puede determinar si una fórmula es satisfactible o no.
Usando Z3, determiná si las fórmulas siguientes son verdaderas:
Nota 1 Podemos usar lógica proposicional usando constantes y podemos nombrar los teoremas con los cuales queremos trabajar. Por ejemplo:
(declare-const a Bool)
(declare-const b Bool)
(define-fun demorgan () Bool
(= (and a b) (not (or (not a) (not b)))))
(assert (not demorgan))
(check-sat)En el script siguiente, la primera formula asertada dice que la constante a debe ser mayor a 10. La segunda dice que la función f aplicada a a y true debe devolver un valor menor a 100.
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)Agregá la aserción (get-model) al script anterior. Explicá qué entendés de la salida.
El script siguiente nos permite resolver las dos ecuaciones dadas, encontrando valores apropiados para x e y:
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)(get-model). Explicá la salida.Usando Z3, podés encontrar una solución para x e y en las ecuaciones siguientes:
3x + 2y = 36 5x + 4y = 64
Z3 también soporta la división, y los operadores división entera, módulo y resto. Por ejemplo:
(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(assert (= a 10))
(assert (= r1 (div a 4))); integer division
(assert (= r2 (mod a 4))); mod
(assert (= r3 (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)Usando Z3, calculá lo siguiente y guardá el resultado en constantes a1, a2 y a3:
Z3 mantiene una pila global de las declaraciones y aserciones. El comando push crea un ámbito nuevo guardando el tamaño actual de la pila. El comando pop saca cualquier aserción o declaración que se hizo entre él y su push correspondiente. Los comandos check-sat y get-assertions siempre operan sobre el contenido de la pila global.
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(push)
(assert (= (+ x y) 10))
(assert (= (+ x (* 2 y)) 20))
(check-sat)
(pop) ; remove the two assertions
(push)
(assert (= (+ (* 3 x) y) 10))
(assert (= (+ (* 2 x) (* 2 y)) 21))
(check-sat)