z3

6El calor

1Respuesta

Salida de contraejemplo de Z3

Cuando se especifica una fórmula en Z3 unsat y (get-proof) hay un resultado que no encuentro ninguna información acerca de lo que es. ¿Dónde puedo encontrar documentación sobre eso? Me parece bastante

z3 2012-02-02

---

5El calor

1Respuesta

¿Puede Z3 funcionar en modo incremental?

Estoy usando Z3 en fórmulas QFBV. Me preguntaba si Z3 puede trabajar de forma incremental en tales fórmulas, como los solucionadores de SAT pueden en cláusulas booleanas. Básicamente, necesito una for

z3 2012-02-02

---

5El calor

2Respuesta

¿Está buscando ejemplos prácticos de cajas de uso SMT Z3 (como DbC) y alternativas de código abierto a Z3?

Me he interesado y estoy buscando ejemplos prácticos del uso de SMT Z3 (como DbC) con código y alternativas de código abierto para esta herramienta. Así que, de hecho, estoy interesado en las herramie

.net constraint-programming sat-solvers z3 2011-01-06

---

5El calor

1Respuesta

Cuál es la razón detrás del mensaje de advertencia en Z3: "no se pudo encontrar un patrón para el cuantificador (identificación del cuantificador: k! 18)"

Encontré un problema como se muestra en el siguiente programa simple SMT-LIB. El código SMT-LIB: (declare-fun isDigit (Int) Bool) (assert (forall ((x Int)) (=> (isDigit x) (and (>= x 0) (

z3 2012-02-08

---

5El calor

1Respuesta

cuantificador en Z3

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))) (

z3 2012-02-16

---

5El calor

1Respuesta

¿Z3_ast referencias de conteo de conteo fuera de Z3?

En Z3 hay 2 modos: conteo automático de referencias y manual. Entiendo cómo funciona el recuento manual de ref. Gracias al ejemplo. Pero, ¿cómo sabe Z3 cuándo eliminar el nodo AST en el caso de recuen

z3 2011-09-21

---

6El calor

2Respuesta

un tipo de datos contiene un conjunto en Z3

cómo puedo hacer un tipo de datos que contiene un conjunto de otros objetos. Básicamente, estoy haciendo el siguiente código: (define-sort Set(T) (Array Int T)) (declare-datatypes() ((A f1 (cons (val

z3 2012-02-18

---

5El calor

1Respuesta

¿Z3 admite Craig Interpolation

Can Z3 genera interpolantes Craig (al menos para lógica proposicional?). No lo he encontrado en la documentación de Z3.

z3 2011-08-10

---

6El calor

2Respuesta

Uso de reescritura de términos en procedimientos de decisión para aritmética de bit-vector

Estoy trabajando en un proyecto cuyo enfoque es el uso de reescritura de términos para resolver/simplificar problemas aritméticos de bits y vectores de tamaño fijo, lo cual es útil para hacer paso pre

z3 bitvector smt rewriting 2011-11-25

---

7El calor

2Respuesta

Equivalente a definir-diversión en Z3 API

Utilizando Z3 con el formato de texto, puedo usar define-fun para definir funciones para su reutilización más adelante. Por ejemplo: (define-fun mydiv ((x Real) (y Real)) Real (if (not (= y 0.0))

api z3 2011-10-12

---