Descubrí que el demostrador CVC viene con una característica que permite traducir a formato SMT-lib. Este es un formato que usan todos los demostradores SMT en una competencia que se hace una vez por año.
O sea, que ahora puedo escribir en SMT-lib gratis, sin esfuerzo porque el output a CVC ya lo tenía hecho.
Un tema es que varios demostradores, al leer archivos en este formato SMT-lib, sólo le dan bola a la primer propiedad que aparece ahí. Por eso ahora lo que hago es:
O sea, que ahora puedo escribir en SMT-lib gratis, sin esfuerzo porque el output a CVC ya lo tenía hecho.
Un tema es que varios demostradores, al leer archivos en este formato SMT-lib, sólo le dan bola a la primer propiedad que aparece ahí. Por eso ahora lo que hago es:
- Ir acumulando las cosas que sé que son verdad (precondición y los asserts que surgen del flujo del programa).
- Cuando encuentro un query lo parto en tantos átomos como elementos de la conjunción que denota.
- Para cada átomo genero un archivo con todos los asserts acumulados como axiomas y pregunto si es teorema.
- Si es teorema lo agrego al conjunto de axiomas. Sino, no.
- Sigo hasta agotar todos los átomos de cada uno de los queries.
No hay comentarios.:
Publicar un comentario