> ## 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) | `(IFF a b)` |
| `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 "active") (EQ status "pending"))

# If raining, then umbrella
(IMPLIES raining has_umbrella)
```

***

## Comparison operators

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

### 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
(GE price 10)
```

***

## Arithmetic operators

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

### 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) (GT x 0))` |
| `EXISTS` | There exists (∃) | `(EXISTS (x) (EQ x 5))` |

### Examples

```lisp theme={null}
# All elements are positive
(FORALL (x) (GT x 0))

# There exists a solution
(EXISTS (x y) (AND (EQ (PLUS x y) 10) (GT x 0) (GT y 0)))
```

***

## Special types

### Boolean literals

```lisp theme={null}
TRUE
FALSE
```

### Integer constraints

```lisp theme={null}
(INT x)          # x is an integer
(NAT x)          # x is a natural number (≥ 0)
(POS x)          ; x is positive
```

### Array/list operations

```lisp theme={null}
(LEN arr)              # Length of array
(GET arr i)            # Get element at index i
(SET arr i val)        # Set element at index i
(SUM arr)              # Sum of all elements
```

***

## Complete examples

### Example 1: age validation

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

**Python:**

```python theme={null}
result = client.verify_logic("(AND (GE age 18) (LE age 65))")
# SAT with model: {age: 30}
```

### Example 2: budget constraint

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

### Example 3: password rules

```lisp theme={null}
# Password must be 8-20 chars with at least 1 uppercase
(AND
  (GE (LEN password) 8)
  (LE (LEN password) 20)
  (GT uppercase_count 0)
)
```

### Example 4: scheduling constraint

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

### Example 5: quadratic equation

```lisp theme={null}
# x² - 5x + 6 = 0 has solutions
(EXISTS (x)
  (EQ (PLUS (POW x 2) (TIMES -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))")

print(result.status)   # "SAT"
print(result.model)    # {"x": 6}
print(result.verified) # True
```

***

## API usage

### Python

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

client = QWEDClient(api_key="qwed_your_key")

# Simple constraint
result = client.verify_logic("(GT x 5)")

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

if result.status == "SAT":
    print(f"Solution: x = {result.model['x']}")
```

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

```bash theme={null}
curl -X POST https://api.qwedai.com/v1/verify/logic \
  -H "Authorization: Bearer qwed_your_key" \
  -H "Content-Type: application/json" \
  -d '{
    "expression": "(AND (GT x 5) (LT y 10))",
    "format": "dsl"
  }'
```

***

## Common patterns

### Range check

```lisp theme={null}
(AND (GE x min) (LE x max))
```

### Non-empty string

```lisp theme={null}
(GT (LEN str) 0)
```

### Mutual exclusion

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

### At most one

```lisp theme={null}
(LE (PLUS (IF a 1 0) (IF b 1 0) (IF c 1 0)) 1)
```

### Exactly one

```lisp theme={null}
(EQ (PLUS (IF a 1 0) (IF b 1 0) (IF c 1 0)) 1)
```

***

## Error handling

| Error | Cause | Fix |
| - | - | - |
| `PARSE_ERROR` | Invalid syntax | Check parentheses matching |
| `UNKNOWN_OPERATOR` | Typo in operator | Use valid operator names |
| `TYPE_ERROR` | Incompatible types | Check operand types |
| `TIMEOUT` | Constraint too complex | Simplify or set longer timeout |

***

## Grammar (EBNF)

```ebnf theme={null}
expression     = atom | compound
compound       = "(" operator expression* ")"
atom           = variable | number | boolean | string
operator       = "AND" | "OR" | "NOT" | "IMPLIES" | "IFF" | "XOR"
               | "EQ" | "NE" | "GT" | "LT" | "GE" | "LE"
               | "PLUS" | "MINUS" | "TIMES" | "DIV" | "MOD" | "POW"
               | "FORALL" | "EXISTS" | "LEN" | "GET" | "SET"
variable       = [a-zA-Z_][a-zA-Z0-9_]*
number         = [-]?[0-9]+("."[0-9]+)?
boolean        = "TRUE" | "FALSE"
string         = "\"" [^\"]* "\""
```

***

## Full specification

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


## Related topics

- [LLM configuration](/getting-started/llm-configuration.md)
- [Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL](/engines/logic.md)
- [QWED protocol specification](/specs/qwed-spec.md)
- [Protocol specifications](/specs/overview.md)
- [Python SDK](/sdks/python.md)


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