Skip to main content

Logic Engine

Verify logical constraints using the Z3 SMT Solver.

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

Capabilities​

FeatureDescription
SatisfiabilityCheck if constraints have a solution
Model FindingFind values that satisfy constraints
Proof GenerationProve tautologies
QuantifiersFORALL, EXISTS support
ArithmeticInteger 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​

CategoryOperatorsExample
LogicAND, OR, NOT(AND a b)
ComparisonGT, LT, EQ, GTE, LTE, NEQ(GT x 5)
ImplicationIMPLIES, IFF(IMPLIES a b)
QuantifiersFORALL, EXISTS(FORALL x (GT x 0))
ArithmeticPLUS, MINUS, MULT, DIV(PLUS x y)

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'

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​

OperationAvg Latency
Simple constraint5ms
Complex (10+ clauses)20ms
Quantified50ms

Next Steps​