Estuve laburando en integrar un demostrador genérico. Para no complicarse con librerias lo hago a travez de un llamado al programa y me engancho escribiendo en su input, leyendo su output desde java, lo cual permite integracion con cualquier demostrador para el cual contemos con:
Por último estuve jugando con los dos demostradores (yices y cvc) para ver que tanto se bancan arrays y cuatificadores. En mi experiencia cada vez que digo algo cuantificado universalmente la respuesta es unknown. Realmente estoy empezando a dudar seriamente de que algo con arrays pueda llegar siquiera a hacerse (siempre y cuando nos quedemos en el mundo de los demostradores automáticos). En caso de que esto sea tan malo como parece, creo que vamos a necesitar un "plan b"... porque introducir arrays sería equivalente a demostrar todos los programas EXCEPTO aquellos que tienen arrays... algo bastante ridículo.
- un ejecutable
- un convertidor de mis predicados a predicados en el lenguaje del demostrador
- un intérprete para la salida del demostrador que mapee a VALID, INVALID, UNKNOWN
Por último estuve jugando con los dos demostradores (yices y cvc) para ver que tanto se bancan arrays y cuatificadores. En mi experiencia cada vez que digo algo cuantificado universalmente la respuesta es unknown. Realmente estoy empezando a dudar seriamente de que algo con arrays pueda llegar siquiera a hacerse (siempre y cuando nos quedemos en el mundo de los demostradores automáticos). En caso de que esto sea tan malo como parece, creo que vamos a necesitar un "plan b"... porque introducir arrays sería equivalente a demostrar todos los programas EXCEPTO aquellos que tienen arrays... algo bastante ridículo.
No hay comentarios.:
Publicar un comentario