es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

Advertencia de tabla grande para (declarar-relación)

20 Jul, 2023 Programación


$ z3 sat.smt2
ADVERTENCIA: se está creando una tabla grande de tamaño 16777216 para la relación match1

El archivo sat.smt sin procesar:

; (set-option :fixedpoint.engine datalog)
; sorts
(define-sort s () (_ BitVec 24))
(define-sort t () (_ BitVec 8))
; Relaciones
(declare-rel f (t s s))
(declare-rel match1 (t s))
(declare-rel better (t s))
(declare-rel best (t s))
(declare-rel a (t))
(declare-rel b ())
(declare-rel c ())
(declare-var x s)
(declare-var xmin s)
(declare-var xmax s)
(declare-var p t)
(declare-var q t)

; Reglas
(rule (=> (and (f p xmin xmax) (bvsle xmin x) (bvsle x xmax)) 
      (match1 p x)))
(rule (=> (and (match1 q x) (bvslt q p))
      (better p x)))
(rule (=> (and (not (better p x)) (match1 p x))
     (best p x)))
; Hechos (EDB)
(rule (f #x10 #x100000 #x200000))
(rule (f #x20 #x150000 #x200000))
(rule (f #x20 #x300000 #x500000))

; Consultas
(rule (=> (best #x10 #x170000) c))

; Salida 'ADVERTENCIA: se está creando una tabla grande de tamaño 16777216 para la relación better' y falla
(query c)

Cómo resolver el problema y por qué? La versión de z3 es Z3 versión 4.8.13 – 64 bit. Y cómo agregar todas las declaraciones y consultas para que el ejemplo pueda ejecutarse.

Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    El mensaje de advertencia indica que Z3 está creando una tabla grande de tamaño 16777216 para la relación ‘match1’. Esta advertencia no es un error crítico y generalmente puede ser ignorada. Sin embargo, el programa no logra generar la salida esperada, que es ‘c’. Este fallo probablemente se debe a una asignación de memoria ineficiente para la relación ‘better’.

    Una forma de resolver este problema es aumentar el límite de memoria para Z3, lo cual se puede hacer agregando la siguiente línea al inicio del archivo:

    (set-option :rlimit 8000)

    Esto establece la cantidad máxima de memoria utilizada por Z3 en 8GB. Alternativamente, el programa se puede reescribir para evitar la asignación de memoria ineficiente para la relación ‘better’. Una forma de hacer esto es agregar una relación adicional llamada ‘better_pair’ para almacenar pares de valores (p,x) que satisfacen la relación ‘better’:

    (declare-rel better_pair (t s s))
(rule (better_pair p x y) (and (match1 y x) (bvslt y p)))
(rule (=> (and (match1 p x) (not (exists (y) (better_pair p x y))))) (best p x))
(query c)

    Esta nueva versión elimina la necesidad de tablas grandes en la relación ‘better’ y debería funcionar sin errores.

    Para ejecutar el programa completo, agrega todas las declaraciones, reglas, hechos (EDB), consultas y la opción de límite de memoria a un solo archivo (por ejemplo, ‘program.smt2’). Luego, ejecuta el programa utilizando el comando ‘z3 program.smt2’.

Comments are closed.