Logic engine

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}

# 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

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

result = client.find_all_models(
    "(AND (GTE x 1) (LTE x 3))",
    max_models=10
)
# [{"x": 1}, {"x": 2}, {"x": 3}]

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

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)

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

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

# At least one item must be in stock
result = client.verify_logic(
    "(EXISTS item (GT (stock item) 0))"
)

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

result = client.verify_logic("x must be greater than 5 and less than 3")
print(result.provider_used)  # "openai_compat"
print(result.status)         # "UNSAT"

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"