Logic Engine

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

The Logic Engine uses Z3, Microsoft’s industry-leading Satisfiability Modulo Theories (SMT) solver, to verify logical constraints with mathematical precision.

---

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

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)

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.

Examples

# 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

# 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

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

rule = """
(IMPLIES 
    (AND (GTE age 18) (EQ has_id True))
    (EQ can_purchase True)
)
"""
result = client.verify_logic(rule)

Discount Eligibility

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

rule = """
(IMPLIES 
    (GT amount 10000)
    (AND (EQ requires_approval True) 
         (GTE approvers 2))
)
"""
result = client.verify_logic(rule)

---

Quantifiers

Universal (FORALL)

# All items must have positive quantity
result = client.verify_logic(
    "(FORALL item (GT (quantity item) 0))"
)

Existential (EXISTS)

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

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

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

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 - Complete operator documentation
• Code Engine - Verify code correctness
• SQL Engine - Verify SQL queries