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

# Logic engine

> The Logic Engine uses Microsoft's Z3 SMT solver for satisfiability checking, model finding, and proof generation.

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"
```

***

## Performance

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

***

## Next steps

* [DSL reference](/api/dsl-reference) - Complete operator documentation
* [Code engine](./code) - Verify code correctness
* [SQL engine](./sql) - Verify SQL queries