Lógica booleana en SMT-LIB: declare-const, assert y check-sat con Z3

SMT-LIB es el lenguaje de entrada de solucionadores como Z3: declaras constantes booleanas, afirmas fórmulas en notación prefija y preguntas check-sat. El listado de abajo es la exportación a SMT-LIB de la regla de entrada generada por el motor, que formula cada comprobación como una pregunta que un solucionador puede responder.

Lógica	SMT-LIB	Nota
`NOT A`	`(not a)`
`A AND B`	`(and a b)`	n-ario: `(and a b c)`
`A OR B`	`(or a b)`	n-ario
`A XOR B`	`(xor a b)`	n-ario; una cadena es paridad
`A -> B`	`(=> a b)`	asocia a la derecha en cadena
`A <-> B`	`(= a b)`	`=` sobre Bool es el bicondicional
`TRUE`, `FALSE`	`true`, `false`	en minúscula

Una entrada booleana es (declare-const member Bool); los operadores son prefijos y n-arios, (and a b c), (or a b), (not a), (xor a b), la implicación (=> a b) y el bicondicional (= a b), ya que = entre dos booleanos es la igualdad de valores de verdad. (assert φ) añade una restricción, (check-sat) responde sat, unsat o unknown, y (get-model) después de sat imprime una asignación que la satisface, que es un testigo en el vocabulario de esta referencia.

Las preguntas se hacen por negación. Para mostrar que una fórmula es una tautología, afirma su negación y espera unsat: ninguna asignación hace verdadera la negación. Para mostrar que dos fórmulas son equivalentes, afirma (not (= f g)) y espera unsat; una respuesta sat viene con un modelo, que es la fila en la que difieren. La exportación hace exactamente esto, un bloque push/pop por pregunta, de modo que las afirmaciones nunca se acumulan entre preguntas, y dice qué significa cada respuesta.

La cabecera nombra el perfil, el subconjunto booleano de SMT-LIB 2.6 con la lógica QF_UF, y la versión de Z3 con la que se probó la exportación. También dice qué es un unsat: comprobado por el solucionador, no una demostración verificada de forma independiente, y unknown no resuelve nada. Es la misma regla de honestidad que el resto del motor, cuyas propias comprobaciones son exhaustivas hasta un límite y contrastadas con el solucionador cuando ambas aplican; el glosario explica la comprobación exhaustiva y el solucionador SAT.

La regla de entrada, exportada por el motor

allow_entry := (member OR invited) AND NOT banned

; Tangibool SMT-LIB export (tangibool.smtlib/1)
; Profile: SMT-LIB 2.6 Boolean subset (QF_UF): Bool constants, define-fun, let, push/pop, assert, check-sat, echo.
; Tested with Z3 5.1.0 (z3-solver 5.2.0, WebAssembly build).
; Model: not stated
; Source revision: reference
; Interpretation status: not stated
; Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
; Logic digest: f0daa82174670c788f59eb058d07f7601cd0ace4ed94d61a747cc26c41fd4e0d
; Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
; Mode: decision
;
; Reading results: each query block states what sat and unsat mean for its question. A sat
; answer comes with a witness or counterexample (ask for it with (get-model) after sat only);
; unsat settles that scoped query and is solver-checked, not an independently checked proof
; certificate; unknown settles nothing. Blocks are scoped with push/pop, so assertions never
; accumulate across questions. This checks the supplied model, not whether it is a complete,
; legal, or safe statement of a real-world rule.
;
; Symbols (stable ID: name -> symbol):
;   v_79df34978043: member -> in_member
;   v_8afde06f51e3: invited -> in_invited
;   v_60b2536f5dc8: banned -> in_banned
;   f_ae8686d89791: allow_entry -> out_allow_entry

(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-logic QF_UF)

; ---- Inputs (declared order)
(declare-const in_member Bool) ; member
(declare-const in_invited Bool) ; invited
(declare-const in_banned Bool) ; banned

; ---- Outputs (dependencies first)
; output allow_entry (stable ID f_ae8686d89791): (member OR invited) AND NOT banned
(define-fun out_allow_entry () Bool (and (or in_member in_invited) (not in_banned)))

; ---- Assumptions (the scope K; never folded into an output)
; K: conjunction of the enabled, confirmed assumptions (true when there are none)
(define-fun K () Bool true)

; ---- Definitions only: nothing is asserted and no check is run.
; Add (assert ...) and (check-sat) inside (push 1) ... (pop 1) to ask a question.

El error habitual

Afirmar la propia fórmula y leer sat como «la regla es válida». sat solo dice que alguna asignación la hace verdadera. La validez es el unsat de la negación, y los bloques de la exportación están escritos en ese sentido para que la respuesta no pueda malinterpretarse.

Preguntas

¿Qué significa unknown?

Que el solucionador se rindió dentro de sus límites. No es un aprobado ni un suspenso; la exportación lo dice en su cabecera, y el motor informa de la misma situación como «No determinado».

¿Con qué solucionador se probó?

La cabecera del archivo generado nombra la versión y la compilación de Z3 con las que se ejecutó. Otros solucionadores SMT-LIB 2.6 deberían aceptar el subconjunto booleano, pero el archivo no lo afirma.

Relacionado

Véase también

Lenguajes

Generado a partir del motor de Tangibool, semántica tangibool-semantics/1, motor 1.0.0, compilación 2026-11-07. Cada tabla, mapa, simplificación y veredicto de estas páginas lo calculó el motor de Tangibool al compilar el sitio, y cada afirmación la volvió a comprobar el mismo verificador exacto que usa la app. Los límites se indican donde aplican. © 2026 Foreranger LTD.