> ## Documentation Index
> Fetch the complete documentation index at: https://qwed-ai-mintlify-a1106bd1.mintlify.site/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](/changelog#v5-1-0-—-agent-state-governance-and-fail-closed-hardening) for migration details.
</Warning>

## 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))")
print(result.satisfiable)  # True
print(result.model)        # {"x": 7}
```

***

## QWED-Logic DSL

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

### Operators

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

<Tip>
  Comparison and arithmetic operators accept multiple aliases for convenience. For example, `GTE` and `GE` both mean "greater than or equal to", `NEQ` and `NE` both mean "not equal", and `MUL` and `MULT` both mean multiplication.
</Tip>

### 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

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

***

## Satisfiability checking

### Basic check

```python theme={null}
# Satisfiable - has solution
result = client.verify_logic("(AND (GT x 0) (LT x 100))")
print(result.satisfiable)  # True
print(result.model)        # {"x": 50}

# Unsatisfiable - no solution
result = client.verify_logic("(AND (GT x 10) (LT x 5))")
print(result.satisfiable)  # False (x can't be > 10 AND < 5)
```

### Finding all solutions

```python theme={null}
result = client.find_all_models(
    "(AND (GTE x 1) (LTE x 3))",
    max_models=10
)
# [{"x": 1}, {"x": 2}, {"x": 3}]
```

***

## Business rules

### Age verification

```python theme={null}
rule = """
(IMPLIES 
    (AND (GTE age 18) (EQ has_id True))
    (EQ can_purchase True)
)
"""
result = client.verify_logic(rule)
```

### 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 = client.verify_logic(rule)
```

### Approval workflow

```python theme={null}
rule = """
(IMPLIES 
    (GT amount 10000)
    (AND (EQ requires_approval True) 
         (GTE approvers 2))
)
"""
result = client.verify_logic(rule)
```

***

## Quantifiers

### Universal (FORALL)

```python theme={null}
# All items must have positive quantity
result = client.verify_logic(
    "(FORALL item (GT (quantity item) 0))"
)
```

### Existential (EXISTS)

```python theme={null}
# At least one item must be in stock
result = client.verify_logic(
    "(EXISTS item (GT (stock item) 0))"
)
```

***

## 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"
print(result.status)         # "UNSAT"
```

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

***

## Error handling

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

if not result.satisfiable:
    print("No solution exists")
    print(f"Reason: {result.reason}")
    # "Constraints are contradictory: x > 5 conflicts with x < 0"
```

***

## `LogicVerifier` returns `DiagnosticResult` (v5.4.0)

<Info>
  **Introduced in v5.4.0.** `LogicVerifier` is the second engine — after `FactVerifier` — to conform to the unified [`DiagnosticResult` contract](/advanced/diagnostics). The legacy `LogicResult` dataclass has been removed. The high-level SDK client (`client.verify_logic()`) and the `/verify/logic` API endpoint still return the same SAT/UNSAT/UNKNOWN shape shown above.
</Info>

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](/advanced/diagnostics#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.
</Tip>

### `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](/api/dsl-reference) - Complete operator documentation
* [Verification diagnostics](/advanced/diagnostics) - The 3-layer `DiagnosticResult` model
* [Code engine](./code) - Verify code correctness
* [SQL engine](./sql) - Verify SQL queries