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.

(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

# 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

# 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

# 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

# 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

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.

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.

# 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

# User must be 18-65 years old
(AND 
  (GTE age 18) 
  (LTE age 65)
)

Python:

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

# Total spending must not exceed budget
(LTE 
  (PLUS food transport entertainment) 
  budget
)

​

Example 3: password rules

# 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

# Meetings can't overlap
(OR
  (LTE meeting1_end meeting2_start)
  (LTE meeting2_end meeting1_start)
)

​

Example 5: quadratic equation

# 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

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

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

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

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

(AND (GTE x min) (LTE x max))

​

Mutual exclusion

(NOT (AND a b))     # a and b can't both be true

​

At most one

(NOT (OR (AND a b) (AND a c) (AND b c)))     # a, b, c declared Bool

​

Exactly one

(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)

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 for the complete formal grammar.