> ## Documentation Index
> Fetch the complete documentation index at: https://docs.qwedai.tech/llms.txt
> Use this file to discover all available pages before exploring further.

# Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL

> The QWED Logic Engine uses Microsoft's Z3 SMT solver for satisfiability checking, model finding, and proof generation from S-expression DSL constraints.

The Logic Engine uses [Z3](https://github.com/Z3Prover/z3), a Satisfiability Modulo Theories (SMT) solver from Microsoft Research, to verify logical constraints.

***

> [!WARNING]
>
> The legacy `VerificationEngine.verify_logic_rule()` method has been removed as of v5.1.0. It now raises `NotImplementedError`. Use `LogicVerifier` from `qwed_new.core.logic_verifier` or the SDK's `client.verify_logic()` method instead. See the [changelog](https://docs.qwedai.tech/changelog-archive#v5-1-0-—-agent-state-governance-and-fail-closed-hardening) for migration details.

## Capabilities

| Feature | Description |
| - | - |
| **Satisfiability** | Check if constraints have a solution |
| **Model Finding** | Find values that satisfy constraints |
| **Proof Generation** | Prove tautologies |
| **Quantifiers** | FORALL, EXISTS support |
| **Arithmetic** | Integer and real arithmetic |

***

## Quick start

```python theme={null}
from qwed_sdk import QWEDClient

client = QWEDClient()

# Check if constraints are satisfiable
result = client.verify_logic("(AND (GT x 5) (LT x 10))")
if result.status == "VERIFIED":            # satisfiable
    print(result.result["model"])          # {"x": "7"}
elif result.status == "UNVERIFIABLE":      # unsatisfiable
    print("No solution exists")
else:
    # BLOCKED: the query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")
```

***

## QWED-Logic DSL

QWED uses a secure S-expression DSL for logic expressions.

### Operators

| Category | Operators | Example |
| - | - | - |
| **Logic** | AND, OR, NOT, XOR | `(AND a b)` |
| **Comparison** | EQ, NEQ, GT, LT, GTE, LTE | `(GT x 5)` |
| **Implication** | IMPLIES, IFF | `(IMPLIES a b)` |
| **Quantifiers** | FORALL, EXISTS | `(FORALL x (GT x 0))` |
| **Arithmetic** | PLUS, MINUS, MULT, DIV, MOD, POW | `(PLUS x y)` |
| **Declaration** | VAR | `(VAR flag Bool)` |

> [!WARNING]
>
> The parser accepts only the operator names in this table. Aliases such as `NE`, `GE`, `LE`, and `MUL` are not on the whitelist, so the engine returns `BLOCKED` with `Unknown operator`. Use `NEQ`, `GTE`, `LTE`, and `MULT`.

### Type rules

Every variable has a sort: `Int`, `Real`, or `Bool`. An undeclared variable is an `Int`. Declare other sorts in the `variables` argument of `DSLLogicVerifier.verify_from_dsl()`, for example `variables=[{"name": "flag", "type": "Bool"}]`. On `POST /verify/logic` the query is natural language, and the translator declares the variables it emits. A `(VAR flag Bool)` form inside a larger expression does not compile, even though the compiler's error message suggests it.

The compiler rejects mixed Boolean and numeric operands instead of coercing `True` to `1`. A rejected program returns `ERROR`, never `SAT` or `VERIFIED`.

| Rule | Valid | Rejected (`ERROR`) |
| - | - | - |
| `EQ`/`NEQ` compare two Booleans or two numbers | `(EQ (GT x 5) True)` | `(EQ x True)` with `x` an `Int` |
| An undeclared name compared with `True`/`False` must be declared `Bool` | `(EQ flag True)` with `flag` declared `Bool` | `(EQ flag True)` with `flag` undeclared |
| `GT`/`LT`/`GTE`/`LTE` take numeric operands only | `(GTE x 2)` | `(GT flag 0)` with `flag` a `Bool` |
| `PLUS`/`MINUS`/`MULT`/`DIV`/`POW`/`MOD` take numeric operands only | `(EQ (PLUS x 1) 2)` | `(EQ x (PLUS True 0))` |
| `IFF` takes Boolean operands: comparisons, `Bool` variables, or `True`/`False` | `(IFF (GT x 1) (GTE x 2))` | `(IFF x y)` with `x`, `y` as `Int` |
| A `FORALL`/`EXISTS` body must be Boolean | `(FORALL x (GTE (MULT x x) 0))` | `(FORALL x (PLUS x 1))` |

QWED does not infer the sort of an undeclared name from a Boolean literal, because that would hide a translation that forgot the declaration.

### Examples

```python theme={null}
# Simple constraint
"(GT x 5)"                      # x > 5

# Compound constraint  
"(AND (GT x 5) (LT y 10))"      # x > 5 AND y < 10

# Implication
"(IMPLIES (GT age 18) adult)"   # age > 18 implies adult (adult declared Bool)

# Nested logic
"(AND (OR a b) (NOT c))"        # (a OR b) AND NOT c (a, b, c declared Bool)
```

***

## Satisfiability checking

### Basic check

```python theme={null}
def check(result):
    if result.status == "VERIFIED":        # satisfiable: a model exists
        return result.result["model"]
    if result.status == "UNVERIFIABLE":    # unsatisfiable: no model
        return None
    # BLOCKED: the query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")

print(check(client.verify_logic("(AND (GT x 0) (LT x 100))")))  # {"x": "50"}
print(check(client.verify_logic("(AND (GT x 10) (LT x 5))")))   # None: x can't be > 10 AND < 5
```

### Finding all solutions

The SDK client's `verify_logic()` returns a single verdict with one model. For all-solutions enumeration, iterate with a low-level solver (e.g. `z3`) or use the `LogicVerifier` low-level API and extend constraints yourself:

```python theme={null}
from z3 import Int, Solver

x = Int("x")
solver = Solver()
solver.add(x >= 1, x <= 3)
while solver.check() == sat:
    m = solver.model()
    print(m[x])
    solver.add(x != m[x])
# 1
# 2
# 3
```

***

## Business rules

These rules compare flags such as `has_id` with `True`, so each flag must be declared `Bool`, or the compiler returns `ERROR` (see [Type rules](#type-rules)). The examples here and under [Quantifiers](#quantifiers) run the DSL directly with `DSLLogicVerifier`, which takes the declarations in `variables`. `verdict()` returns `SAT` or `UNSAT` and fails closed on anything else:

```python theme={null}
from qwed_new.core.dsl_logic_verifier import DSLLogicVerifier

verifier = DSLLogicVerifier()


def verdict(result):
    if result.status in ("SAT", "UNSAT"):
        return result.status
    # ERROR, BLOCKED or UNKNOWN: the solver reached no verdict. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")
```

### Age verification

```python theme={null}
rule = """
(IMPLIES 
    (AND (GTE age 18) (EQ has_id True))
    (EQ can_purchase True)
)
"""
result = verifier.verify_from_dsl(rule, variables=[
    {"name": "has_id", "type": "Bool"},
    {"name": "can_purchase", "type": "Bool"},
])
print(verdict(result))  # "SAT"
```

### Discount eligibility

```python theme={null}
rule = """
(AND
    (IMPLIES (GT total 100) (EQ discount 10))
    (IMPLIES (AND (EQ member True) (GT total 50)) (EQ discount 15))
)
"""
result = verifier.verify_from_dsl(rule, variables=[{"name": "member", "type": "Bool"}])
print(verdict(result))  # "SAT"
```

### Approval workflow

```python theme={null}
rule = """
(IMPLIES 
    (GT amount 10000)
    (AND (EQ requires_approval True) 
         (GTE approvers 2))
)
"""
result = verifier.verify_from_dsl(rule, variables=[{"name": "requires_approval", "type": "Bool"}])
print(verdict(result))  # "SAT"
```

***

## Quantifiers

`FORALL` and `EXISTS` take exactly two arguments: a binder and a body.

```lisp theme={null}
(FORALL x body)
(EXISTS x body)
```

* **Binder.** The first argument is a single plain variable name. The parser returns `BLOCKED` for any other binder, such as a number, an operator name, `True`/`False`, a list like `(x)`, or an expression.
* **Sort.** The bound variable takes its declared sort. If it isn't declared, it is an `Int`.
* **Scope.** The binding applies inside the body only. A free variable with the same name outside the quantifier is a separate variable.
* **Body.** The body must be Boolean, such as a comparison or a logical expression. A numeric body returns `ERROR`.
* **Solver limits.** Quantified formulas can be hard for Z3. If Z3 returns `unknown`, for example on a timeout, `verify_from_dsl()` returns `UNKNOWN` and `POST /verify/logic` returns `BLOCKED`. Neither is verified.

To quantify over a collection, quantify over a numeric variable and state the property with arithmetic and comparisons. The DSL has no uninterpreted functions, so a form like `(quantity item)` returns `BLOCKED` with `Unknown operator`.

### Universal (FORALL)

```python theme={null}
# Every number greater than 5 is also greater than 3
result = verifier.verify_from_dsl("(FORALL n (IMPLIES (GT n 5) (GT n 3)))")
print(verdict(result))  # "SAT"

# Not every integer is positive
result = verifier.verify_from_dsl("(FORALL x (GT x 0))")
print(verdict(result))  # "UNSAT"
```

### Existential (EXISTS)

```python theme={null}
# Some integer lies strictly between 0 and 10
result = verifier.verify_from_dsl("(EXISTS x (AND (GT x 0) (LT x 10)))")
print(verdict(result))  # "SAT"

# No integer lies strictly between 0 and 1 (x is an Int by default)
result = verifier.verify_from_dsl("(EXISTS x (AND (GT x 0) (LT x 1)))")
print(verdict(result))  # "UNSAT"
```

### Bound and free variables

```python theme={null}
# The quantified x and the free x are different variables
result = verifier.verify_from_dsl("(AND (FORALL x (GTE (MULT x x) 0)) (EQ x 3))")
print(verdict(result), result.model)  # SAT {'x': '3'}
```

***

## Security: operator whitelist

The DSL uses a **strict whitelist** — only approved operators are allowed:

```python theme={null}
# ALLOWED
"(AND (GT x 5) (LT y 10))"  ✓

# BLOCKED - unknown operator
"(IMPORT os)"               ✗
# Error: SECURITY BLOCK: Unknown operator 'IMPORT'

# BLOCKED - eval attempt
"(EVAL 'print(1)')"         ✗
# Error: SECURITY BLOCK: Unknown operator 'EVAL'
```

### Fail-closed constraint parsing

The logic engine uses `SafeEvaluator` for all constraint parsing. If `SafeEvaluator` is unavailable, the engine raises a `RuntimeError` instead of falling back to raw evaluation. This fail-closed design ensures that untrusted input is never passed to Python's `eval()`.

***

## Provider tracking

When you verify a natural-language logic query, QWED translates it to DSL using the configured LLM provider. The response includes a `provider_used` field so you can see which provider handled the translation — even when the request falls back to a different provider or ends in an error.

```python theme={null}
result = client.verify_logic("x must be greater than 5 and less than 3")
print(result.provider_used)  # "openai_compat", also set when the request fails
if result.status == "BLOCKED":
    raise RuntimeError(f"Logic verification failed: {result.error}")
print(result.status)         # "UNVERIFIABLE" (unsatisfiable)
```

This field also appears in error responses, which helps you debug provider-related issues without inspecting server logs.

### Python-style constraints

QWED also converts Python-style constraints from a structured logic task into DSL. It maps each operator to its whitelisted DSL name:

| Constraint | DSL operator |
| - | - |
| `==`, `!=` | `EQ`, `NEQ` |
| `>`, `<`, `>=`, `<=` | `GT`, `LT`, `GTE`, `LTE` |
| `+`, `-`, `*`, `/`, `%`, `**` | `PLUS`, `MINUS`, `MULT`, `DIV`, `MOD`, `POW` |

Constraints such as `x >= 5` or `x * 2 <= 10` compile and return `SAT` or `UNSAT`. Earlier releases emitted `GE`, `LE`, `NE`, and `MUL`, so these constraints came back `BLOCKED`.

You can join conditions with infix `and`/`or`/`not` in any case, or with the call forms `And(...)` and `Or(...)`:

```python theme={null}
"x > 1 and x < 3"        # (AND (GT x 1) (LT x 3))
"(x > 1) AND (x < 3)"    # infix, parenthesized operands
"And(x > 1, x < 3)"      # call form
```

Unknown operators, unsupported Python syntax, and solver errors still fail closed.

### Categorical string constants fail closed

The natural-language bridge rejects string literals such as `tier == 'gold'`. The solver has no string type, so QWED can't soundly model categorical string constants. A constraint that contains one returns `UNVERIFIABLE` (or an error) instead of a verdict. Floating-point literals are rejected the same way.

Encode categories as explicit integers instead:

```python theme={null}
# Fails closed: string constants are rejected
result = client.verify_logic("tier == 'gold' and tier == 'silver'")

# Encode categories as integers (gold = 1, silver = 2)
result = client.verify_logic("(AND (EQ tier 1) (EQ tier 2))")
if result.status == "UNVERIFIABLE":        # unsatisfiable: a tier can't be both
    print("The claims contradict each other")
elif result.status == "BLOCKED":
    # The query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed: {result.error}")
```

> [!NOTE]
>
> Before v7.3.0, the bridge turned each string into a free integer variable, so contradictory categorical claims could come back satisfiable. See [GHSA-g25v-44j8-gg7x](https://github.com/QWED-AI/qwed-verification/security/advisories/GHSA-g25v-44j8-gg7x).

***

## Error handling

```python theme={null}
result = client.verify_logic("(AND (GT x 5) (LT x 0))")

if result.status == "UNVERIFIABLE":
    print("No solution exists")
    print(result.result.get("agent_message"))   # "Logic constraints are unsatisfiable"
elif result.status == "BLOCKED":
    # The query could not be translated or solved; error says why. Fail closed.
    raise RuntimeError(f"Logic verification failed: {result.error}")
```

***

## `LogicVerifier` returns `DiagnosticResult` (v6.0.0)

> [!NOTE]
>
> **Introduced in v6.0.0.** `LogicVerifier` is the second engine — after `FactVerifier` — to conform to the unified [`DiagnosticResult` contract](https://docs.qwedai.tech/advanced/diagnostics). The legacy `LogicResult` dataclass has been removed from the verifier's return surface. The `/verify/logic` endpoint, and so `client.verify_logic()`, maps the DSL verdict instead: `SAT` is `VERIFIED` with the model as evidence, `UNSAT` is `UNVERIFIABLE`, and anything else (`UNKNOWN`, `ERROR`, `BLOCKED`) is `BLOCKED`. `DSLLogicVerifier.verify_from_dsl()` returns the raw `SAT`, `UNSAT`, `UNKNOWN`, `ERROR` or `BLOCKED`.

If you call the low-level `LogicVerifier` class directly, every one of its nine public methods now returns a `DiagnosticResult`:

* `verify_logic`
* `verify_with_quantifiers`
* `verify_bitvector`
* `verify_array`
* `prove_theorem`
* `check_implication`
* `check_equivalence`
* `verify_optimization`
* `check_vacuity`

### Reading a result

```python theme={null}
from qwed_new.core.logic_verifier import LogicVerifier

verifier = LogicVerifier()
result = verifier.verify_logic(
    variables={"x": "Int", "y": "Int"},
    constraints=["x > 0", "y > 0", "x + y == 10"],
)

result.is_verified                                  # True
result.status.value                                 # "VERIFIED"
result.developer_fields["deterministic_verdict"]    # "SAT"
result.developer_fields["model"]                    # {"x": "5", "y": "5"}
result.developer_fields["symbol_table"]             # [{"name": "x", "type": "Int"}, {"name": "y", "type": "Int"}]
result.proof_ref                                    # "sha256:..." (present only when VERIFIED)
result.agent_message                                # "Logic constraints are satisfiable — model found"
```

The three [diagnostic layers](https://docs.qwedai.tech/advanced/diagnostics.md#the-3-layer-model) — `agent_message`, `developer_fields`, and `proof_ref` — are populated on every result. `proof_ref` is computed from the Z3 solver's assertion stack and is present **only** when `status == "VERIFIED"`.

### SAT/UNSAT status matrix

Z3's `sat`/`unsat` outcome has different meanings depending on the method. The engine disambiguates by mapping each per-method outcome to a `DiagnosticResult` status and recording the raw Z3 verdict under `developer_fields.deterministic_verdict`.

| Method | Z3 `sat` | Z3 `unsat` | Z3 `unknown` |
| - | - | - | - |
| `verify_logic` | `VERIFIED` (model found) | `UNVERIFIABLE` (no model) | `UNVERIFIABLE` |
| `verify_with_quantifiers` | `VERIFIED` | `UNVERIFIABLE` | `UNVERIFIABLE` |
| `verify_bitvector` | `VERIFIED` | `UNVERIFIABLE` | `UNVERIFIABLE` |
| `verify_array` | `VERIFIED` | `UNVERIFIABLE` | `UNVERIFIABLE` |
| `prove_theorem` | `BLOCKED` (counterexample) | `VERIFIED` (theorem proved by contradiction) | `UNVERIFIABLE` |
| `check_implication` | `BLOCKED` | `VERIFIED` | `UNVERIFIABLE` |
| `check_equivalence` | `BLOCKED` (counterexample) | `VERIFIED` (equivalent) | `UNVERIFIABLE` |
| `verify_optimization` | `VERIFIED` (optimal model) | `UNVERIFIABLE` | `UNVERIFIABLE` |
| `check_vacuity` | `VERIFIED` (non-vacuous) | `UNVERIFIABLE` (vacuously true) | `UNVERIFIABLE` |

> [!TIP]
>
> Always branch on `result.is_verified` (or `result.proof_ref is not None`) for control flow. Read `developer_fields["deterministic_verdict"]` for diagnostic context — never for authorization.

### `symbol_table` on every VERIFIED result

`developer_fields.symbol_table` is a sorted list of every declared variable and its type. It is included on every `VERIFIED` result so audit logs record exactly what was proven:

```python theme={null}
result.developer_fields["symbol_table"]
# [
#   {"name": "age",  "type": "Int"},
#   {"name": "seat", "type": "BitVec[8]"},
# ]
```

### New `BLOCKED` constraint IDs

Two fail-closed behaviors ship with the migration:

| `constraint_id` | Trigger |
| - | - |
| `logic_verifier.explicit_declarations_required` | The `variables` dict is empty. The previous `_infer_variables` heuristic has been removed — the engine now refuses to guess types from constraint syntax. |
| `dsl_compiler.type_validation` | A variable is declared with a malformed type such as `"BitVec"` (missing width), `"BitVec[]"`, or `"BitVec[abc]"`. The engine no longer silently defaults to 32-bit; you must declare a valid `BitVec[N]` with `N ≥ 1`. |

Other `constraint_id`s used by the engine: `logic_verifier.invalid_constraint`, `logic_verifier.unknown_quantifier`, and `logic_verifier.execution_error`.

### Migrating from `LogicResult`

**Status field**

```python theme={null}
# Before — LogicResult with a solver-level status string
result = verifier.verify_logic(variables, constraints)
if result.status == "SAT":
    solution = result.model
elif result.status == "UNSAT":
    ...
```

```python theme={null}
# After — DiagnosticResult with method-scoped semantics
result = verifier.verify_logic(variables, constraints)
if result.is_verified:
    solution = result.developer_fields["model"]
elif result.developer_fields.get("deterministic_verdict") == "UNSAT":
    ...
```

**Proving a theorem**

```python theme={null}
# Before — SAT meant "theorem is valid"
result = verifier.prove_theorem(variables, premises, conclusion)
if result.status == "SAT":
    ...   # theorem valid
elif result.status == "UNSAT":
    counterexample = result.model
```

```python theme={null}
# After — VERIFIED means "theorem proved", BLOCKED means "counterexample found"
result = verifier.prove_theorem(variables, premises, conclusion)
if result.is_verified:
    ...   # theorem proved by contradiction
elif result.status.value == "BLOCKED":
    counterexample = result.developer_fields["model"]
```

**Variable declarations are now mandatory**

```python theme={null}
# Before — the engine tried to infer types from constraint syntax
result = verifier.verify_logic({}, ["x > 5", "P and Q"])
# Types guessed: x -> Int, P/Q -> Bool

# After — empty variables dict fails closed
result = verifier.verify_logic({}, ["x > 5", "P and Q"])
result.status.value                              # "BLOCKED"
result.developer_fields["constraint_id"]         # "logic_verifier.explicit_declarations_required"
```

**Malformed `BitVec` declarations fail closed**

```python theme={null}
# Before — silently defaulted to 32-bit
result = verifier.verify_bitvector({"x": "BitVec"}, ["x == 0"])

# After — BLOCKED with a type-validation constraint ID
result = verifier.verify_logic({"x": "BitVec"}, ["x == 0"])
result.status.value                              # "BLOCKED"
result.developer_fields["constraint_id"]         # "dsl_compiler.type_validation"
```

***

## Performance

| Operation | Avg Latency |
| - | - |
| Simple constraint | 5ms |
| Complex (10+ clauses) | 20ms |
| Quantified | 50ms |

***

## Next steps

* [DSL reference](https://docs.qwedai.tech/api/dsl-reference.md) - Complete operator documentation
* [Verification diagnostics](https://docs.qwedai.tech/advanced/diagnostics.md) - The 3-layer `DiagnosticResult` model
* [Code engine](https://docs.qwedai.tech/engines/code.md) - Verify code correctness
* [SQL engine](https://docs.qwedai.tech/engines/sql.md) - Verify SQL queries


## Related topics

- [QWED-Logic DSL reference](https://docs.qwedai.tech/api/dsl-reference.md)
- [QWED: deterministic verification for LLMs and AI agents](https://docs.qwedai.tech/intro.md)
- [QWED design decisions](https://docs.qwedai.tech/advanced/design.md)
- [QWED Protocol: deterministic verification for LLMs](https://docs.qwedai.tech/whitepaper.md)
- [QWED Infra guards for infrastructure verification](https://docs.qwedai.tech/infra/guards.md)


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.