Z3 Forall con matriz

Question

Z3 proporciona desconocido para el problema simple:

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

Descubrí que se convierte en sat si se niega forall, pero esto parece una cosa particularmente simple que no se puede resolver.

Esto está causando problemas porque la clase de problemas que quiero resolver son más como,

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

Donde negar el forall solo no es el mismo problema, entonces eso no se puede hacer aquí. ¿Hay alguna forma de plantear este tipo de problema a Z3 para obtener un resultado no satisfactorio?

Answer 1

Los problemas con los cuantificadores siempre son problemáticos con los solucionadores SMT, especialmente si involucran matrices y cuantificadores alternos como en su ejemplo. Esencialmente tienes exits u. forall y. P(u, y). Z3, o cualquier otro solucionador SMT, tendrá dificultades para lidiar con este tipo de problemas.

Cuando tiene una afirmación cuantificada como la que tiene forallen el nivel superior o anidada exists, la lógica se vuelve semidecidible. Z3 utiliza MBQI (instanciación de cuantificadores basados ​​en modelos) para resolver heurísticamente tales problemas, pero la mayoría de las veces no lo hace. El problema no es simplemente que z3 no sea capaz: no existe un procedimiento de decisión para tales problemas, y z3 hace todo lo posible.

Puede intentar dar patrones cuantificadores para tales problemas para ayudar a z3, pero no veo una manera fácil de aplicar eso en su problema. (Los patrones cuantificadores se aplican cuando tiene funciones no interpretadas y axiomas cuantificados. Consultehttps://rise4fun.com/z3/tutorialcontent/guide#h28). Entonces, no creo que funcione para ti. Incluso si lo hiciera, los patrones son muy delicados de programar y no son sólidos con respecto a los cambios en su especificación que de otra manera podrían parecer inocuos.

Si está tratando con tales cuantificadores, los solucionadores SMT probablemente no sean una buena opción. Busque probadores de teoremas semiautomatizados como Lean, Isabelle, Coq, etc., que están diseñados para tratar con cuantificadores de una manera mucho más disciplinada. Por supuesto, pierde la automatización completa, pero la mayoría de estas herramientas pueden usar un solucionador SMT para descargar subobjetivos que son lo suficientemente "fáciles". De esa manera, usted todavía hace el "trabajo pesado" manualmente, pero z3 maneja automáticamente la mayoría de los subobjetivos. (Especialmente en el caso de Lean, vea aquí:https://leanprover.github.io/)

Answer 2

Hay un paréntesis de cierre (derecha) adicional, que debe eliminarse. Además, agregue assert antes de la declaración forall.

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

Ejecute el código anterior y debería obtener unsat como respuesta.

Para el segundo programa, la respuesta de alias puede serle útil.