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

# QWED-Logic DSL reference

> QWED-Logic S-expression DSL reference for logical constraints. Covers basic syntax, operators (AND, OR, NOT, IMPLIES), verified by the Z3 SMT solver.

Quick reference for the QWED-Logic Domain Specific Language.

## Overview

QWED-Logic is an S-expression based DSL for expressing logical constraints. It's verified by the Z3 SMT solver for mathematical correctness.

```lisp theme={null}
(AND (GT x 5) (LT y 10))
```

> **Why S-expressions?** They're unambiguous, easy to parse, and map directly to Z3 constraints.

***

## Basic syntax

```
(OPERATOR arg1 arg2 ...)
```

All expressions are enclosed in parentheses. The operator comes first, followed by arguments.

***

## Logical operators

| Operator | Meaning | Example |
| - | - | - |
| `AND` | Logical AND | `(AND a b c)` |
| `OR` | Logical OR | `(OR a b)` |
| `NOT` | Logical NOT | `(NOT a)` |
| `IMPLIES` | Implication (a → b) | `(IMPLIES a b)` |
| `IFF` | Biconditional (a ↔ b). Both operands must be Boolean. | `(IFF (GT x 1) (GTE x 2))` |
| `XOR` | Exclusive OR | `(XOR a b)` |

### Examples

```lisp theme={null}
# Both conditions must be true
(AND (GT x 0) (LT x 100))

# At least one must be true
(OR (EQ status 1) (EQ status 2))

# If raining, then umbrella (raining and has_umbrella declared Bool)
(IMPLIES raining has_umbrella)

# x > 1 exactly when x >= 2
(IFF (GT x 1) (GTE x 2))
```

`IFF` is a biconditional, not equality. Its operands must be comparisons, `Bool` variables, or `True`/`False`. `(IFF x y)` on two `Int` variables is a compile error, not `x == y`.

***

## Comparison operators

| Operator | Meaning | Example |
| - | - | - |
| `EQ` | Equal (=) | `(EQ x 5)` |
| `NEQ` | Not equal (≠) | `(NEQ x 0)` |
| `GT` | Greater than | `(GT x 5)` |
| `LT` | Less than | `(LT x 10)` |
| `GTE` | Greater or equal (≥) | `(GTE x 0)` |
| `LTE` | Less or equal (≤) | `(LTE x 100)` |

Only these names are on the operator whitelist. `NE`, `GE`, `LE`, and `MUL` return `BLOCKED` with `Unknown operator`.

### Examples

```lisp theme={null}
# x is between 0 and 100 (exclusive)
(AND (GT x 0) (LT x 100))

# x equals y
(EQ x y)

# Price is at least $10
(GTE price 10)
```

***

## Arithmetic operators

| Operator | Meaning | Example |
| - | - | - |
| `PLUS` | Addition (+) | `(PLUS x y)` |
| `MINUS` | Subtraction (-) | `(MINUS x y)` |
| `MULT` | Multiplication (\*) | `(MULT x y)` |
| `DIV` | Division (/) | `(DIV x y)` |
| `MOD` | Modulo (%) | `(MOD x 2)` |
| `POW` | Power (^) | `(POW x 2)` |

### Examples

```lisp theme={null}
# Check if x + y = 10
(EQ (PLUS x y) 10)

# x squared equals 16
(EQ (POW x 2) 16)

# Even number check
(EQ (MOD x 2) 0)
```

***

## Quantifiers

| Operator | Meaning | Example |
| - | - | - |
| `FORALL` | For all (∀) | `(FORALL x (GTE (MULT x x) 0))` |
| `EXISTS` | There exists (∃) | `(EXISTS x (EQ x 5))` |

A quantifier takes a binder and a body: `(FORALL x body)` or `(EXISTS x body)`.

* The binder is one plain variable name. The parser returns `BLOCKED` for any other binder, including a list such as `(x)` or `(x y)`, a number, an operator name, or `True`/`False`.
* The bound variable takes its declared sort, or `Int` if it isn't declared.
* The binding applies inside the body only. A free variable with the same name outside the quantifier is unaffected.
* The body must be Boolean. `(FORALL x (PLUS x 1))` is a compile error.
* If Z3 returns `unknown` on a hard quantified formula, the result is `UNKNOWN`. It is never reported as verified.

### Examples

```lisp theme={null}
# Every square is non-negative
(FORALL x (GTE (MULT x x) 0))

# Every number greater than 5 is greater than 3
(FORALL n (IMPLIES (GT n 5) (GT n 3)))

# Nest quantifiers to bind more than one variable
(EXISTS x (EXISTS y (AND (EQ (PLUS x y) 10) (GT x 0) (GT y 0))))
```

***

## Special types

### Boolean literals

```lisp theme={null}
True
False
```

### Variable sorts

Variables are `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.

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

result = DSLLogicVerifier().verify_from_dsl(
    "(EQ flag True)", variables=[{"name": "flag", "type": "Bool"}]
)

if result.status == "SAT":
    print(result.model)               # {"flag": "True"}
elif result.status == "UNSAT":
    print(result.rejection_reason)    # the constraints contradict each other
else:
    # ERROR, BLOCKED or UNKNOWN: the solver reached no verdict. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")
```

The compiler checks operand sorts and never coerces a Boolean to `1` or `0`:

* `EQ`/`NEQ` between a Boolean (a literal, `Bool` variable, or comparison) and a non-Boolean value is a compile error.
* `GT`, `LT`, `GTE`, and `LTE` reject Boolean operands, because Booleans have no ordering.
* `PLUS`, `MINUS`, `MULT`, `DIV`, `POW`, and `MOD` reject Boolean operands.
* An undeclared name compared with `True` or `False` is a compile error. Declare it `Bool`.

```lisp theme={null}
# ERROR: flag is undeclared, so it is an Int
(EQ flag True)

# Valid once flag is declared Bool (in variables)
(EQ flag True)

# Valid: compares two Booleans
(EQ (GT x 5) True)

# ERROR: Boolean inside arithmetic
(EQ x (PLUS True 0))
```

A compile error returns `ERROR`, never `SAT` or `VERIFIED`.

***

## Complete examples

### Example 1: age validation

```lisp theme={null}
# User must be 18-65 years old
(AND 
  (GTE age 18) 
  (LTE age 65)
)
```

**Python:**

```python theme={null}
result = client.verify_logic("(AND (GTE age 18) (LTE age 65))")
if result.status == "VERIFIED":            # SAT
    print(result.result["model"])          # e.g. {"age": "18"}
elif result.status == "UNVERIFIABLE":      # UNSAT
    print("No age satisfies the rule")
else:
    # BLOCKED: the query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")
```

### Example 2: budget constraint

```lisp theme={null}
# Total spending must not exceed budget
(LTE 
  (PLUS food transport entertainment) 
  budget
)
```

### Example 3: password rules

```lisp theme={null}
# Password must be 8-20 chars with at least 1 uppercase
# (lengths and counts are integers the caller supplies; the DSL has no string functions)
(AND
  (GTE password_length 8)
  (LTE password_length 20)
  (GT uppercase_count 0)
)
```

### Example 4: scheduling constraint

```lisp theme={null}
# Meetings can't overlap
(OR
  (LTE meeting1_end meeting2_start)
  (LTE meeting2_end meeting1_start)
)
```

### Example 5: quadratic equation

```lisp theme={null}
# x² - 5x + 6 = 0 has solutions
(EXISTS x
  (EQ (PLUS (POW x 2) (MULT -5 x) 6) 0)
)
```

***

## Verification results

| Status | Meaning | Model |
| - | - | - |
| `SAT` | Satisfiable — solution exists | `{x: 6, y: 4}` |
| `UNSAT` | Unsatisfiable — no solution | `null` |
| `UNKNOWN` | Solver timeout or undecidable | `null` |

### Reading results

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

if result.status == "VERIFIED":          # SAT on /verify/logic
    print(result.result["model"])        # {"x": "6"}
elif result.status == "UNVERIFIABLE":    # UNSAT
    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}")
```

The table above is the DSL verdict, which `DSLLogicVerifier.verify_from_dsl()` returns as is. `POST /verify/logic`, and so `client.verify_logic()`, maps it: `SAT` is `VERIFIED` with the model as evidence, `UNSAT` is `UNVERIFIABLE`, and anything else is `BLOCKED`. The route makes no admission decision, so the Python SDK's `is_verified` stays `False`; read `status` and the model.

***

## API usage

### Python

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

client = QWEDClient(api_key="qwed_your_key")

# Simple constraint: check the status before using the result, as below
result = client.verify_logic("(GT x 5)")

# Complex constraint
result = client.verify_logic("""
  (AND 
    (GTE x 0) 
    (LTE x 100)
    (EQ (MOD x 7) 0)
  )
""")

if result.status == "VERIFIED":
    print(f"Solution: x = {result.result['model']['x']}")
elif result.status == "UNVERIFIABLE":
    print("No solution exists")
else:
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")
```

### CLI

```bash theme={null}
# Verify a constraint
qwed verify-logic "(AND (GT x 5) (LT x 10))"

# From file
echo "(EQ (PLUS x y) 10)" > constraint.dsl
qwed verify-logic -f constraint.dsl
```

### HTTP API

`POST /verify/logic` takes a natural-language `query`. The server translates it into this DSL with the LLM provider you configured, then checks the DSL with Z3. It does not take DSL directly.

```bash theme={null}
curl -X POST http://localhost:8000/verify/logic \
  -H "X-API-Key: qwed_your_key" \
  -H "Content-Type: application/json" \
  -d '{"query": "Is there an x greater than 5 and less than 10?"}'
```

***

## Common patterns

### Range check

```lisp theme={null}
(AND (GTE x min) (LTE x max))
```

### Mutual exclusion

```lisp theme={null}
(NOT (AND a b))     # a and b can't both be true
```

### At most one

```lisp theme={null}
(NOT (OR (AND a b) (AND a c) (AND b c)))     # a, b, c declared Bool
```

### Exactly one

```lisp theme={null}
(AND (OR a b c) (NOT (OR (AND a b) (AND a c) (AND b c))))     # a, b, c declared Bool
```

***

## Error handling

| Error | Cause | Fix |
| - | - | - |
| `PARSE_ERROR` | Invalid syntax | Check parentheses matching |
| `UNKNOWN_OPERATOR` | Typo in operator | Use valid operator names |
| `TYPE_ERROR` | Boolean and numeric operands mixed, or a non-Boolean `IFF` operand or quantifier body | Declare Boolean variables as `Bool` in `variables` and keep comparisons and arithmetic numeric |
| `TIMEOUT` | Constraint too complex | Simplify or set longer timeout |

***

## Grammar (EBNF)

```ebnf theme={null}
expression     = atom | compound
compound       = "(" operator expression* ")" | quantified
atom           = variable | number | boolean
operator       = "AND" | "OR" | "NOT" | "IMPLIES" | "IFF" | "XOR"
               | "EQ" | "NEQ" | "GT" | "LT" | "GTE" | "LTE"
               | "PLUS" | "MINUS" | "MULT" | "DIV" | "MOD" | "POW"
               | "VAR"
quantified     = "(" ( "FORALL" | "EXISTS" ) variable expression ")"
variable       = [a-zA-Z_][a-zA-Z0-9_]*
number         = [-]?[0-9]+("."[0-9]+)?
boolean        = "True" | "False"
```

***

## Full specification

See [QWED-Logic DSL Specification](https://docs.qwedai.tech/specs/qwed-spec.md#7-qwed-logic-dsl) for the complete formal grammar.


## Related topics

- [LLM configuration](https://docs.qwedai.tech/getting-started/llm-configuration.md)
- [Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL](https://docs.qwedai.tech/engines/logic.md)
- [Changelog](https://docs.qwedai.tech/changelog.md)
- [QWED protocol specification](https://docs.qwedai.tech/specs/qwed-spec.md)
- [Protocol specifications](https://docs.qwedai.tech/specs/overview.md)


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