cuantificador en Z3

Question

Básicamente, quiero preguntar a Z3 dame un entero arbitrario cuyo valor es mayor que 10. Así que escribir las siguientes declaraciones:

(declare-const x (Int)) 
(assert (forall ((i Int)) (> i 10))) 
(check-sat) 
(get-value(x)) 

¿Cómo puedo aplicar este cuantificador a mi modelo? Sé que puedes escribir (assert (> x 10)) para lograr esto. Pero quiero decir que quiero un cuantificador en mi modelo, así que cada vez que declaro una constante entera cuyo valor está garantizado es más de 10. Así que no tengo que insertar declaración (assert (> x 10)) para cada constante entera que yo declarado.

Answer 1

Cuando usa (assert (forall ((i Int)) (> i 10))), i es una variable limitada y la fórmula cuantificada es equivalente a un valor de verdad, que es false en este caso.

creo que se quiere definir una macro utilizando cuantificadores:

(declare-fun greaterThan10 (Int) Bool) 
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10)))) 

y se puede utilizar para evitar la repetición de código:

(declare-const x (Int)) 
(declare-const y (Int)) 
(assert (greaterThan10 x)) 
(assert (greaterThan10 y)) 
(check-sat) 

Es esencialmente la forma de definir las macros usando funciones no interpretados cuando trabajas con Z3 API. Tenga en cuenta que debe establecer (set-option :macro-finder true) para que Z3 reemplace los cuantificadores universales con los cuerpos de esas funciones.

Sin embargo, si está trabajando con la interfaz textual, la macro define-fun en SMT-LIB v2 es una manera más fácil de hacer lo que quiere:

(define-fun greaterThan10 ((i Int)) Bool 
    (> i 10))