QWED-Logic DSL Reference

(AND (GT x 5) (LT y 10))

(OPERATOR arg1 arg2 ...)

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

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

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

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

TRUE
FALSE

(INT x)          # x is an integer
(NAT x)          # x is a natural number (≥ 0)
(POS x)          ; x is positive

(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

# User must be 18-65 years old
(AND 
  (GE age 18) 
  (LE age 65)
)

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

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

# Password must be 8-20 chars with at least 1 uppercase
(AND
  (GE (LEN password) 8)
  (LE (LEN password) 20)
  (GT uppercase_count 0)
)

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

# x² - 5x + 6 = 0 has solutions
(EXISTS (x)
  (EQ (PLUS (POW x 2) (TIMES -5 x) 6) 0)
)

result = client.verify_logic("(AND (GT x 5) (LT x 10))")

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

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']}")

# 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

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"
  }'

(AND (GE x min) (LE x max))

(GT (LEN str) 0)

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

(LE (PLUS (IF a 1 0) (IF b 1 0) (IF c 1 0)) 1)

(EQ (PLUS (IF a 1 0) (IF b 1 0) (IF c 1 0)) 1)

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         = "\"" [^\"]* "\""