Saltar al contenido

Regla de descuento: (estudiante OR mayor) AND NOT caducado AND (socio OR cupon)

Una regla de descuento, (student OR senior) AND NOT expired AND (member OR coupon): una tabla de 32 filas con nueve que cumplen, una FND de cuatro términos, 7 compuertas NOR frente a 31 NAND, y sin mapa de Karnaugh, porque cinco entradas superan el límite.

El glosario fija las entradas: student significa carné de estudiante, senior significa 65 años o más, expired significa que el carné o el cupón ha caducado, member significa ser socio, coupon significa que se presenta un cupón. La regla son tres requisitos unidos con AND: alguna condición, nada caducado, alguna prueba de derecho. La lectura del motor enumera exactamente esos tres. Con cinco entradas la tabla tiene 32 filas, y la salida es verdadera en nueve, Σm(9, 10, 11, 17, 18, 19, 25, 26, 27).

Las comprobaciones: no es tautología, contraejemplo las cinco entradas en FALSO; satisfacible, testigo student = FALSO, senior = VERDADERO, expired = FALSO, member = FALSO, coupon = VERDADERO. El simplificador no encontró ninguna ley que acorte la regla de cinco operadores, y el conversor a FNC la devuelve sin cambios como tres cláusulas. El conversor a FND aplica dos distributividades y obtiene cuatro términos de tres literales, uno por combinación de condición y derecho. Compuertas: 7 NOR frente a 31 NAND. El mapa de Karnaugh no está disponible: el mapa cubre hasta cuatro variables y esta regla tiene cinco.

Las reglas de elegibilidad con esta forma, varios grupos OR bajo un AND, son el caso común en la lógica de precios y prestaciones, y la FND es la lista de perfiles concretos de cliente que cumplen, que es también la lista de casos de prueba positivos. Lo que hay que vigilar es expired: es un único bloqueo que se aplica tanto a la condición como al derecho, y la redacción del glosario, «el carné o el cupón», deja abierto a qué documento se refiere. Una regla con un solo indicador expired para dos documentos es una decisión de modelado que conviene hacer explícita.

student: el cliente tiene carné de estudiante; senior: el cliente tiene 65 años o más; expired: el carné o el cupón ha caducado; member: el cliente es socio; coupon: el cliente presenta un cupón;

discount := (student OR senior) AND NOT expired AND (member OR coupon) · salida

Comprobaciones exactas

¿Siempre verdadera (tautología)? No Contraejemplo: student = F, senior = F, expired = F, member = F, coupon = F · Exhaustively checked and solver cross-checked · 1 filas
¿Siempre falsa (contradicción)? No Contraejemplo: student = F, senior = V, expired = F, member = F, coupon = V · Exhaustively checked and solver cross-checked · 10 filas
¿Puede ser verdadera? Sí Asignación de ejemplo: student = F, senior = V, expired = F, member = F, coupon = V · Exhaustively checked and solver cross-checked · 10 filas

Tabla de verdad (32 filas)

Regla de descuento: (estudiante OR mayor) AND NOT caducado AND (socio OR cupon)
#studentseniorexpiredmembercoupondiscount
0FALSOFALSOFALSOFALSOFALSOFALSO
1FALSOFALSOFALSOFALSOVERDADEROFALSO
2FALSOFALSOFALSOVERDADEROFALSOFALSO
3FALSOFALSOFALSOVERDADEROVERDADEROFALSO
4FALSOFALSOVERDADEROFALSOFALSOFALSO
5FALSOFALSOVERDADEROFALSOVERDADEROFALSO
6FALSOFALSOVERDADEROVERDADEROFALSOFALSO
7FALSOFALSOVERDADEROVERDADEROVERDADEROFALSO
8FALSOVERDADEROFALSOFALSOFALSOFALSO
9FALSOVERDADEROFALSOFALSOVERDADEROVERDADERO
10FALSOVERDADEROFALSOVERDADEROFALSOVERDADERO
11FALSOVERDADEROFALSOVERDADEROVERDADEROVERDADERO
12FALSOVERDADEROVERDADEROFALSOFALSOFALSO
13FALSOVERDADEROVERDADEROFALSOVERDADEROFALSO
14FALSOVERDADEROVERDADEROVERDADEROFALSOFALSO
15FALSOVERDADEROVERDADEROVERDADEROVERDADEROFALSO
16VERDADEROFALSOFALSOFALSOFALSOFALSO
17VERDADEROFALSOFALSOFALSOVERDADEROVERDADERO
18VERDADEROFALSOFALSOVERDADEROFALSOVERDADERO
19VERDADEROFALSOFALSOVERDADEROVERDADEROVERDADERO
20VERDADEROFALSOVERDADEROFALSOFALSOFALSO
21VERDADEROFALSOVERDADEROFALSOVERDADEROFALSO
22VERDADEROFALSOVERDADEROVERDADEROFALSOFALSO
23VERDADEROFALSOVERDADEROVERDADEROVERDADEROFALSO
24VERDADEROVERDADEROFALSOFALSOFALSOFALSO
25VERDADEROVERDADEROFALSOFALSOVERDADEROVERDADERO
26VERDADEROVERDADEROFALSOVERDADEROFALSOVERDADERO
27VERDADEROVERDADEROFALSOVERDADEROVERDADEROVERDADERO
28VERDADEROVERDADEROVERDADEROFALSOFALSOFALSO
29VERDADEROVERDADEROVERDADEROFALSOVERDADEROFALSO
30VERDADEROVERDADEROVERDADEROVERDADEROFALSOFALSO
31VERDADEROVERDADEROVERDADEROVERDADEROVERDADEROFALSO

Lectura en lenguaje claro

Principiantediscount es verdadero exactamente cuando se cumplen todas las condiciones siguientes:
1. al menos uno entre student y senior es verdadero (pueden serlo ambos)
2. expired es falso
3. al menos uno entre member y coupon es verdadero (pueden serlo ambos)
En todos los demás casos, discount es falso.
Sobre los operadores:
- AND (Y) solo es verdadero cuando todas sus partes son verdaderas.
- OR (O) es inclusivo: es verdadero en cuanto al menos una parte es verdadera, también cuando lo son varias.
- NOT (NO) invierte un valor: lo verdadero pasa a ser falso y lo falso, verdadero.
Intermediodiscount es verdadero exactamente cuando se cumplen todas las condiciones siguientes:
1. al menos uno entre student y senior es verdadero (pueden serlo ambos)
2. expired es falso
3. al menos uno entre member y coupon es verdadero (pueden serlo ambos)
En todos los demás casos, discount es falso.
Avanzadodiscount es verdadero exactamente cuando se cumplen todas las condiciones siguientes [conjunción ∧]:
1. al menos uno entre student y senior es verdadero (pueden serlo ambos) [disyunción inclusiva ∨]
2. expired es falso [negación ¬]
3. al menos uno entre member y coupon es verdadero (pueden serlo ambos) [disyunción inclusiva ∨]
En todos los demás casos, discount es falso.
Notación formal: (student ∨ senior) ∧ ¬expired ∧ (member ∨ coupon)

Diagrama lógico

Discount eligibility rule: (student OR senior) AND NOT expired AND (member OR coupon) Discount eligibility rule: (student OR senior) AND NOT expired AND (member OR coupon) student senior expired member coupon discount AND OR NOT OR
Discount eligibility rule: (student OR senior) AND NOT expired AND (member OR coupon) Discount eligibility rule: (student OR senior) AND NOT expired AND (member OR coupon) student senior expired member coupon discount AND OR NOT OR

Simplificación paso a paso

El motor no encontró ninguna ley que acorte esta expresión; ya es tan corta como sus leyes de reescritura permiten.

(student OR senior) AND NOT expired AND (member OR coupon)

Mapa de Karnaugh

Un mapa de Karnaugh muestra como máximo 4 variables; esta expresión tiene más. Usa la herramienta para fijar algunas entradas y ver un corte etiquetado. discount depends on 5 inputs that are not shown to be irrelevant; a Karnaugh map shows at most 4. Fix coupon to view an explicitly labelled slice.

Mintérminos y maxtérminos

discount(student, senior, expired, member, coupon) = Σm(9, 10, 11, 17, 18, 19, 25, 26, 27)discount(student, senior, expired, member, coupon) = ΠM(0, 1, 2, 3, 4, 5, 6, 7, 8, 12, 13, 14, 15, 16, 20, 21, 22, 23, 24, 28, 29, 30, 31)

Orden de variables: student, senior, expired, member, coupon · 32 filas

Formas normales

Forma normal conjuntiva (FNC)

(student OR senior) AND NOT expired AND (member OR coupon)

3 cláusulas, 5 literales · complete

Forma normal disyuntiva (FND)

(student AND NOT expired AND member) OR (student AND NOT expired AND coupon) OR (senior AND NOT expired AND member) OR (senior AND NOT expired AND coupon)

4 términos, 12 literales · complete · Distributividad ×2

Solo NAND, solo NOR

Forma solo con NAND

NAND(NAND(NAND(NAND(NAND(NAND(student, student), NAND(senior, senior)), NAND(expired, expired)), NAND(NAND(NAND(student, student), NAND(senior, senior)), NAND(expired, expired))), NAND(NAND(member, member), NAND(coupon, coupon))), NAND(NAND(NAND(NAND(NAND(student, student), NAND(senior, senior)), NAND(expired, expired)), NAND(NAND(NAND(student, student), NAND(senior, senior)), NAND(expired, expired))), NAND(NAND(member, member), NAND(coupon, coupon))))

31 compuertas · equivalencia verificada en todas las filas

Forma solo con NOR

NOR(NOR(NOR(NOR(student, senior), expired), NOR(NOR(student, senior), expired)), NOR(member, coupon))

7 compuertas · equivalencia verificada en todas las filas

La misma regla como código

Python
# -*- coding: utf-8 -*-
# Generated by Tangibool (tangibool.python/1). Do not edit by hand; regenerate from the source revision.
# Model: not stated
# Source revision: reference
# Interpretation status: not stated
"""Tangibool evaluator (decision model).

Generated deterministically from the validated Boolean model; it evaluates exactly that
model. It does not establish that the model is a complete, legal, or safe statement of a
real-world rule, and evaluating examples does not verify the rule.

Source revision: reference
Interpretation status: not stated
Exporter: 1.0.0 (format tangibool.python/1; engine 1.0.0; semantics tangibool-semantics/1)
Logic digest: a7ccaac3652524d0b2342e0bc0961ef98c69958628e3ef40fb5cadf1fd7ebdd8
Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78

Inputs (dict keys, declared order) and generated parameter names:
    'student' -> input_student
    'senior' -> input_senior
    'expired' -> input_expired
    'member' -> input_member
    'coupon' -> input_coupon

Outputs (declared order) and their functions:
    'discount' -> output_discount(inputs)

Assumptions (the declared scope, checked by in_scope(inputs)):
    none; every complete assignment is in scope.

Input contract:
    Every required input must be exactly True or False (type(value) is bool). Missing
    inputs, None, strings, integers (including 0 and 1), and keys that are not declared
    inputs raise InputError before anything is evaluated, including inputs that a
    short-circuiting operator would never read. Results are always bool.

Scope:
    Decision functions raise OutOfScopeError when the inputs violate an assumption; an
    out-of-scope assignment is never turned into a False result. Pass check_scope=False
    to evaluate without the scope check, and use in_scope(inputs) to test it separately.

Usage:

    import tangibool_model as model

    model.evaluate({'student': False, 'senior': False, 'expired': False, 'member': False, 'coupon': False})
    # -> {'discount': False}
    model.output_discount({'student': False, 'senior': False, 'expired': False, 'member': False, 'coupon': False})
    # -> False
    model.evaluate({'student': 1, 'senior': False, 'expired': False, 'member': False, 'coupon': False})
    # raises InputError: 1 is an int, not a bool
"""

import collections.abc as _abc
from typing import Dict, Mapping, Tuple

__all__ = [
    "MODEL_INFO",
    "IDENTIFIER_MAP",
    "INPUT_NAMES",
    "OUTPUT_NAMES",
    "ASSUMPTIONS",
    "InputError",
    "OutOfScopeError",
    "minterm_index",
    "in_scope",
    "evaluate",
    "output_discount",
]

MODEL_INFO = {
    "format": "tangibool.python/1",
    "mode": "decision",
    "model": None,
    "revision": "reference",
    "interpretation": None,
    "exporter": "1.0.0",
    "engine_version": "1.0.0",
    "semantics_version": "tangibool-semantics/1",
    "logic_digest": "a7ccaac3652524d0b2342e0bc0961ef98c69958628e3ef40fb5cadf1fd7ebdd8",
    "assumptions_digest": "d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78",
    "primary_output": "discount",
    "unused_inputs": (),
    "subcircuits": (),
}

# Stable ID -> generated identifier (reversible mapping; names are exact, escaped strings).
IDENTIFIER_MAP = {
    "v_97a451a60f14": {"kind": "input", "name": "student", "identifier": "input_student"},
    "v_9373a966ab63": {"kind": "input", "name": "senior", "identifier": "input_senior"},
    "v_7a1672e8b8cb": {"kind": "input", "name": "expired", "identifier": "input_expired"},
    "v_dbfd54032935": {"kind": "input", "name": "member", "identifier": "input_member"},
    "v_67d46adf341f": {"kind": "input", "name": "coupon", "identifier": "input_coupon"},
    "f_8a13877dfb35": {"kind": "output", "name": "discount", "identifier": "output_discount"},
}

INPUT_NAMES = ("student", "senior", "expired", "member", "coupon")
OUTPUT_NAMES = ("discount",)
ASSUMPTIONS = ()

_DECLARED_INPUTS = frozenset(INPUT_NAMES)
_SCOPE_INPUTS = ()
_ASSUMPTION_FORMULAS = {entry["name"]: entry["formula"] for entry in ASSUMPTIONS}


class InputError(ValueError):
    """Raised when inputs are missing, undeclared, or not exactly True/False.

    Every required input must satisfy type(value) is bool. Missing inputs, None, strings,
    integers (including 0 and 1), and keys that are not declared inputs are rejected before
    anything is evaluated. A missing input is never treated as False. The individual problems
    are listed in the problems attribute.
    """

    def __init__(self, problems):
        self.problems = tuple(problems)
        super().__init__("Invalid inputs: " + "; ".join(self.problems))


class OutOfScopeError(ValueError):
    """Raised when the inputs violate the model's assumptions (its declared scope).

    Outside its assumptions the rule has no decision: this error is never a False result.
    The names of the violated assumptions are in the violated attribute.
    """

    def __init__(self, violated):
        self.violated = tuple(violated)
        details = ", ".join(name + " (" + _ASSUMPTION_FORMULAS.get(name, "?") + ")" for name in self.violated)
        super().__init__(
            "Out of scope: the inputs violate "
            + ("assumption " if len(self.violated) == 1 else "assumptions ")
            + details
            + ". The rule has no decision outside its assumptions; this is not a False result."
        )


def _short_repr(value: object) -> str:
    text = repr(value)
    return text if len(text) <= 60 else text[:57] + "..."


def _checked_inputs(inputs: Mapping[str, bool], required: Tuple[str, ...], check_scope: bool) -> Dict[str, bool]:
    """Validate inputs strictly before anything is evaluated and return a plain copy."""
    if type(check_scope) is not bool:
        raise TypeError("check_scope must be True or False")
    if not isinstance(inputs, _abc.Mapping):
        raise InputError(["inputs must be a mapping from input names to True/False, got " + type(inputs).__name__])
    problems = []
    for key in inputs:
        if type(key) is not str or key not in _DECLARED_INPUTS:
            declared = ", ".join(repr(name) for name in INPUT_NAMES) or "none"
            problems.append("undeclared input " + _short_repr(key) + " (declared inputs: " + declared + ")")
    needed = tuple(required) + (_SCOPE_INPUTS if check_scope else ())
    for name in needed:
        if name not in inputs:
            problems.append("missing required input " + repr(name))
    for key, value in inputs.items():
        if type(key) is str and key in _DECLARED_INPUTS and type(value) is not bool:
            problems.append(
                "input " + repr(key) + " must be True or False (type bool), got "
                + type(value).__name__ + " " + _short_repr(value)
            )
    if problems:
        raise InputError(list(dict.fromkeys(problems)))
    return dict(inputs.items())


def _require_bool_args(function: str, pairs: Tuple[Tuple[str, object], ...]) -> None:
    problems = [
        "argument " + repr(name) + " of " + function + " must be True or False (type bool), got "
        + type(value).__name__ + " " + _short_repr(value)
        for name, value in pairs
        if type(value) is not bool
    ]
    if problems:
        raise InputError(problems)


def minterm_index(*values: bool) -> int:
    """Row index of an assignment over a declared variable order.

    The first value is the most significant bit, so all-False is row 0. Used for indexed
    minterm (sum) and maxterm (product) forms.
    """
    index = 0
    for value in values:
        if type(value) is not bool:
            raise InputError(["minterm_index() takes True/False values, got " + type(value).__name__ + " " + _short_repr(value)])
        index = index * 2 + (1 if value else 0)
    return index


def _scope_values(values: Dict[str, bool]) -> Tuple[Tuple[str, bool], ...]:
    """Value of every enabled, confirmed assumption for validated inputs, in declared order."""
    return ()


def _require_in_scope(values: Dict[str, bool]) -> None:
    violated = tuple(name for name, holds in _scope_values(values) if not holds)
    if violated:
        raise OutOfScopeError(violated)


def in_scope(inputs: Mapping[str, bool]) -> bool:
    """True when the inputs satisfy every assumption (the model's declared scope).

    Requires the inputs the assumptions read; raises InputError for invalid inputs.
    """
    values = _checked_inputs(inputs, (), True)
    return all(holds for _, holds in _scope_values(values))


# ---- Formula bodies (inputs are validated by the public functions below) ----


def _compute_output_discount(input_student: bool, input_senior: bool, input_expired: bool, input_member: bool, input_coupon: bool) -> bool:
    """Decision output 'discount': (student OR senior) AND NOT expired AND (member OR coupon)"""
    return (input_student or input_senior) and (not input_expired) and (input_member or input_coupon)


# ---- Public API ----


def output_discount(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'discount' (stable ID f_8a13877dfb35).

    'discount' := (student OR senior) AND NOT expired AND (member OR coupon)

    Required inputs: 'student', 'senior', 'expired', 'member', 'coupon'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("student", "senior", "expired", "member", "coupon"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_discount_value = _compute_output_discount(values["student"], values["senior"], values["expired"], values["member"], values["coupon"])
    return output_discount_value


def evaluate(inputs: Mapping[str, bool], *, check_scope: bool = True) -> Dict[str, bool]:
    """Evaluate every output (declared order); each output is computed once.

    Required inputs: 'student', 'senior', 'expired', 'member', 'coupon'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("student", "senior", "expired", "member", "coupon"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_discount_value = _compute_output_discount(values["student"], values["senior"], values["expired"], values["member"], values["coupon"])
    return {
        "discount": output_discount_value,
    }
PostgreSQL
-- Tangibool PostgreSQL export (tangibool.postgresql/1)
-- Target: PostgreSQL 16 or later with typed boolean inputs; tested with PostgreSQL 18.3 (PGlite 0.5.8).
-- Not a claim of compatibility with other SQL dialects.
-- Model: not stated
-- Source revision: reference
-- Interpretation status: not stated
-- Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
-- Logic digest: a7ccaac3652524d0b2342e0bc0961ef98c69958628e3ef40fb5cadf1fd7ebdd8
-- Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
-- Mode: decision
--
-- Read-only: this file contains only WITH / VALUES / SELECT statements. No DDL, DML,
-- procedures, credentials, network access, or database changes. The expressions are pure
-- Boolean expressions, so their result does not depend on SQL evaluation order.
--
-- NON-NULL INPUT PRECONDITION: NULL is not a truth value of this rule. Every fragment below
-- is defined only when every input column it reads is a non-NULL boolean. The guard template
-- (section 2) marks any NULL input as 'invalid_input' and any row that violates the
-- assumptions as 'out_of_scope', and fills output columns only for 'ok' rows; a NULL in an
-- output column of another row is an envelope marker, not a third truth value. Never wrap
-- the fragments in COALESCE(..., FALSE) or otherwise choose a meaning for unknown inputs.
-- This evaluates the supplied model; it does not show that the model is a complete, legal,
-- or safe statement of a real-world rule.
--
-- Input columns (stable ID: name -> column):
--   v_97a451a60f14: student -> "in_student"
--   v_9373a966ab63: senior -> "in_senior"
--   v_7a1672e8b8cb: expired -> "in_expired"
--   v_dbfd54032935: member -> "in_member"
--   v_67d46adf341f: coupon -> "in_coupon"
-- Output columns:
--   f_8a13877dfb35: discount -> "out_discount"
-- Assumptions (scope K; exported separately and never folded into an output):
--   none; every complete input row is in scope.

-- ----------------------------------------------------------------------------------------------
-- 1. Expression fragments (parenthesised; non-NULL boolean inputs required)
-- ----------------------------------------------------------------------------------------------
--
-- [out_discount] output discount (stable ID f_8a13877dfb35)
--   discount := (student OR senior) AND NOT expired AND (member OR coupon)
--   PRECONDITION: "in_student", "in_senior", "in_expired", "in_member", "in_coupon" are non-NULL booleans.
--   (("in_student" OR "in_senior") AND (NOT "in_expired") AND ("in_member" OR "in_coupon"))
--

-- ----------------------------------------------------------------------------------------------
-- 2. Guard template (read-only SELECT over an inputs list)
-- ----------------------------------------------------------------------------------------------
-- Replace the example rows between the markers with your own rows, or replace the inputs
-- CTE with a SELECT that provides the boolean columns listed in the header. status is
-- 'invalid_input' when any input is NULL, 'out_of_scope' when the assumptions are false, and
-- 'ok' otherwise; output columns are filled only for 'ok' rows (NULL elsewhere is an
-- envelope marker). Assumption columns are shown for rows with complete inputs.
WITH inputs ("row_id", "in_student", "in_senior", "in_expired", "in_member", "in_coupon") AS (
  -- tangibool:example-rows:begin
  VALUES
    (1, FALSE, FALSE, FALSE, FALSE, FALSE),
    (2, TRUE, TRUE, TRUE, TRUE, TRUE),
    (3, NULL::boolean, FALSE, FALSE, FALSE, FALSE)
  -- tangibool:example-rows:end
),
checked AS (
  SELECT
    inputs.*,
    CASE
      WHEN "in_student" IS NULL OR "in_senior" IS NULL OR "in_expired" IS NULL OR "in_member" IS NULL OR "in_coupon" IS NULL THEN 'invalid_input'
      ELSE 'ok'
    END AS "status"
  FROM inputs
)
SELECT
  "row_id",
  "in_student",
  "in_senior",
  "in_expired",
  "in_member",
  "in_coupon",
  "status",
  CASE WHEN "status" = 'ok' THEN (("in_student" OR "in_senior") AND (NOT "in_expired") AND ("in_member" OR "in_coupon")) END AS "out_discount"
FROM checked
ORDER BY "row_id";
SMT-LIB
; 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: a7ccaac3652524d0b2342e0bc0961ef98c69958628e3ef40fb5cadf1fd7ebdd8
; 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_97a451a60f14: student -> in_student
;   v_9373a966ab63: senior -> in_senior
;   v_7a1672e8b8cb: expired -> in_expired
;   v_dbfd54032935: member -> in_member
;   v_67d46adf341f: coupon -> in_coupon
;   f_8a13877dfb35: discount -> out_discount

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

; ---- Inputs (declared order)
(declare-const in_student Bool) ; student
(declare-const in_senior Bool) ; senior
(declare-const in_expired Bool) ; expired
(declare-const in_member Bool) ; member
(declare-const in_coupon Bool) ; coupon

; ---- Outputs (dependencies first)
; output discount (stable ID f_8a13877dfb35): (student OR senior) AND NOT expired AND (member OR coupon)
(define-fun out_discount () Bool (and (or in_student in_senior) (not in_expired) (or in_member in_coupon)))

; ---- 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.
LaTeX
discount = \left(\mathit{student} + \mathit{senior}\right) \cdot \overline{\mathit{expired}} \cdot \left(\mathit{member} + \mathit{coupon}\right)

El error habitual

Esperar un mapa de Karnaugh para una regla de cinco variables. El mapa del motor cubre hasta cuatro variables e informa de que aquí el mapa no está disponible en vez de dibujar algo incompleto. La tabla de 32 filas, la FND de cuatro términos y las comprobaciones exactas llevan el análisis completo; nada de la regla queda sin comprobar.

Preguntas

¿Por qué los números de mintérmino están tan repartidos?

Con student como bit más significativo y coupon como el menos, cada fila que cumple necesita expired en FALSO, que fija el bit central, y al menos un bit en cada par. Las nueve filas vienen en tres grupos de tres, 9 a 11, 17 a 19 y 25 a 27, uno por combinación de condición.

Relacionado

Operadores y compuertas

Herramientas

Véase también

Ejemplos resueltos

Generado a partir del motor de Tangibool, semántica tangibool-semantics/1, motor 1.0.0, compilación . 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.