Logic engine — Z3 SAT/SMT verification with QWED-Logic DSL

The QWED Logic Engine uses Microsoft’s Z3 SMT solver for satisfiability checking, model finding, and proof generation from S-expression DSL constraints.

The Logic Engine uses Z3, a Satisfiability Modulo Theories (SMT) solver from Microsoft Research, to verify logical constraints.

---

The legacy VerificationEngine.verify_logic_rule() method has been removed as of v5.1.0. It now raises NotImplementedError. Use LogicVerifier from qwed_new.core.logic_verifier or the SDK’s client.verify_logic() method instead. See the changelog for migration details.

​

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))")
if result.status == "VERIFIED":            # satisfiable
    print(result.result["model"])          # {"x": "7"}
elif result.status == "UNVERIFIABLE":      # unsatisfiable
    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}")

---

​

QWED-Logic DSL

QWED uses a secure S-expression DSL for logic expressions.

​

Operators

Category	Operators	Example
Logic	AND, OR, NOT, XOR	(AND a b)
Comparison	EQ, NEQ, GT, LT, GTE, LTE	(GT x 5)
Implication	IMPLIES, IFF	(IMPLIES a b)
Quantifiers	FORALL, EXISTS	(FORALL x (GT x 0))
Arithmetic	PLUS, MINUS, MULT, DIV, MOD, POW	(PLUS x y)
Declaration	VAR	(VAR flag Bool)

The parser accepts only the operator names in this table. Aliases such as NE, GE, LE, and MUL are not on the whitelist, so the engine returns BLOCKED with Unknown operator. Use NEQ, GTE, LTE, and MULT.

​

Type rules

Every variable has a sort: 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.

The compiler rejects mixed Boolean and numeric operands instead of coercing True to 1. A rejected program returns ERROR, never SAT or VERIFIED.

Rule	Valid	Rejected (ERROR)
EQ/NEQ compare two Booleans or two numbers	(EQ (GT x 5) True)	(EQ x True) with x an Int
An undeclared name compared with True/False must be declared Bool	(EQ flag True) with flag declared Bool	(EQ flag True) with flag undeclared
GT/LT/GTE/LTE take numeric operands only	(GTE x 2)	(GT flag 0) with flag a Bool
PLUS/MINUS/MULT/DIV/POW/MOD take numeric operands only	(EQ (PLUS x 1) 2)	(EQ x (PLUS True 0))
IFF takes Boolean operands: comparisons, Bool variables, or True/False	(IFF (GT x 1) (GTE x 2))	(IFF x y) with x, y as Int
A FORALL/EXISTS body must be Boolean	(FORALL x (GTE (MULT x x) 0))	(FORALL x (PLUS x 1))

QWED does not infer the sort of an undeclared name from a Boolean literal, because that would hide a translation that forgot the declaration.

​

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 (adult declared Bool)

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

---

​

Satisfiability checking

​

Basic check

def check(result):
    if result.status == "VERIFIED":        # satisfiable: a model exists
        return result.result["model"]
    if result.status == "UNVERIFIABLE":    # unsatisfiable: no model
        return None
    # BLOCKED: the query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")

print(check(client.verify_logic("(AND (GT x 0) (LT x 100))")))  # {"x": "50"}
print(check(client.verify_logic("(AND (GT x 10) (LT x 5))")))   # None: x can't be > 10 AND < 5

​

Finding all solutions

The SDK client’s verify_logic() returns a single verdict with one model. For all-solutions enumeration, iterate with a low-level solver (e.g. z3) or use the LogicVerifier low-level API and extend constraints yourself:

from z3 import Int, Solver

x = Int("x")
solver = Solver()
solver.add(x >= 1, x <= 3)
while solver.check() == sat:
    m = solver.model()
    print(m[x])
    solver.add(x != m[x])
# 1
# 2
# 3

---

​

Business rules

These rules compare flags such as has_id with True, so each flag must be declared Bool, or the compiler returns ERROR (see Type rules). The examples here and under Quantifiers run the DSL directly with DSLLogicVerifier, which takes the declarations in variables. verdict() returns SAT or UNSAT and fails closed on anything else:

from qwed_new.core.dsl_logic_verifier import DSLLogicVerifier

verifier = DSLLogicVerifier()


def verdict(result):
    if result.status in ("SAT", "UNSAT"):
        return result.status
    # ERROR, BLOCKED or UNKNOWN: the solver reached no verdict. Fail closed.
    raise RuntimeError(f"Logic verification failed ({result.status}): {result.error}")

​

Age verification

rule = """
(IMPLIES 
    (AND (GTE age 18) (EQ has_id True))
    (EQ can_purchase True)
)
"""
result = verifier.verify_from_dsl(rule, variables=[
    {"name": "has_id", "type": "Bool"},
    {"name": "can_purchase", "type": "Bool"},
])
print(verdict(result))  # "SAT"

​

Discount eligibility

rule = """
(AND
    (IMPLIES (GT total 100) (EQ discount 10))
    (IMPLIES (AND (EQ member True) (GT total 50)) (EQ discount 15))
)
"""
result = verifier.verify_from_dsl(rule, variables=[{"name": "member", "type": "Bool"}])
print(verdict(result))  # "SAT"

​

Approval workflow

rule = """
(IMPLIES 
    (GT amount 10000)
    (AND (EQ requires_approval True) 
         (GTE approvers 2))
)
"""
result = verifier.verify_from_dsl(rule, variables=[{"name": "requires_approval", "type": "Bool"}])
print(verdict(result))  # "SAT"

---

​

Quantifiers

FORALL and EXISTS take exactly two arguments: a binder and a body.

(FORALL x body)
(EXISTS x body)

• Binder. The first argument is a single plain variable name. The parser returns BLOCKED for any other binder, such as a number, an operator name, True/False, a list like (x), or an expression.
• Sort. The bound variable takes its declared sort. If it isn’t declared, it is an Int.
• Scope. The binding applies inside the body only. A free variable with the same name outside the quantifier is a separate variable.
• Body. The body must be Boolean, such as a comparison or a logical expression. A numeric body returns ERROR.
• Solver limits. Quantified formulas can be hard for Z3. If Z3 returns unknown, for example on a timeout, verify_from_dsl() returns UNKNOWN and POST /verify/logic returns BLOCKED. Neither is verified.

To quantify over a collection, quantify over a numeric variable and state the property with arithmetic and comparisons. The DSL has no uninterpreted functions, so a form like (quantity item) returns BLOCKED with Unknown operator.

​

Universal (FORALL)

# Every number greater than 5 is also greater than 3
result = verifier.verify_from_dsl("(FORALL n (IMPLIES (GT n 5) (GT n 3)))")
print(verdict(result))  # "SAT"

# Not every integer is positive
result = verifier.verify_from_dsl("(FORALL x (GT x 0))")
print(verdict(result))  # "UNSAT"

​

Existential (EXISTS)

# Some integer lies strictly between 0 and 10
result = verifier.verify_from_dsl("(EXISTS x (AND (GT x 0) (LT x 10)))")
print(verdict(result))  # "SAT"

# No integer lies strictly between 0 and 1 (x is an Int by default)
result = verifier.verify_from_dsl("(EXISTS x (AND (GT x 0) (LT x 1)))")
print(verdict(result))  # "UNSAT"

​

Bound and free variables

# The quantified x and the free x are different variables
result = verifier.verify_from_dsl("(AND (FORALL x (GTE (MULT x x) 0)) (EQ x 3))")
print(verdict(result), result.model)  # SAT {'x': '3'}

---

​

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", also set when the request fails
if result.status == "BLOCKED":
    raise RuntimeError(f"Logic verification failed: {result.error}")
print(result.status)         # "UNVERIFIABLE" (unsatisfiable)

This field also appears in error responses, which helps you debug provider-related issues without inspecting server logs.

​

Python-style constraints

QWED also converts Python-style constraints from a structured logic task into DSL. It maps each operator to its whitelisted DSL name:

Constraint	DSL operator
==, !=	EQ, NEQ
>, <, >=, <=	GT, LT, GTE, LTE
+, -, *, /, %, **	PLUS, MINUS, MULT, DIV, MOD, POW

Constraints such as x >= 5 or x * 2 <= 10 compile and return SAT or UNSAT. Earlier releases emitted GE, LE, NE, and MUL, so these constraints came back BLOCKED.

You can join conditions with infix and/or/not in any case, or with the call forms And(...) and Or(...):

"x > 1 and x < 3"        # (AND (GT x 1) (LT x 3))
"(x > 1) AND (x < 3)"    # infix, parenthesized operands
"And(x > 1, x < 3)"      # call form

Unknown operators, unsupported Python syntax, and solver errors still fail closed.

​

Categorical string constants fail closed

The natural-language bridge rejects string literals such as tier == 'gold'. The solver has no string type, so QWED can’t soundly model categorical string constants. A constraint that contains one returns UNVERIFIABLE (or an error) instead of a verdict. Floating-point literals are rejected the same way.

Encode categories as explicit integers instead:

# Fails closed: string constants are rejected
result = client.verify_logic("tier == 'gold' and tier == 'silver'")

# Encode categories as integers (gold = 1, silver = 2)
result = client.verify_logic("(AND (EQ tier 1) (EQ tier 2))")
if result.status == "UNVERIFIABLE":        # unsatisfiable: a tier can't be both
    print("The claims contradict each other")
elif result.status == "BLOCKED":
    # The query could not be translated or solved. Fail closed.
    raise RuntimeError(f"Logic verification failed: {result.error}")

Before v7.3.0, the bridge turned each string into a free integer variable, so contradictory categorical claims could come back satisfiable. See GHSA-g25v-44j8-gg7x.

---

​

Error handling

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

if result.status == "UNVERIFIABLE":
    print("No solution exists")
    print(result.result.get("agent_message"))   # "Logic constraints are unsatisfiable"
elif result.status == "BLOCKED":
    # The query could not be translated or solved; error says why. Fail closed.
    raise RuntimeError(f"Logic verification failed: {result.error}")

---

​

LogicVerifier returns DiagnosticResult (v6.0.0)

Introduced in v6.0.0. LogicVerifier is the second engine — after FactVerifier — to conform to the unified DiagnosticResult contract. The legacy LogicResult dataclass has been removed from the verifier’s return surface. The /verify/logic endpoint, and so client.verify_logic(), maps the DSL verdict instead: SAT is VERIFIED with the model as evidence, UNSAT is UNVERIFIABLE, and anything else (UNKNOWN, ERROR, BLOCKED) is BLOCKED. DSLLogicVerifier.verify_from_dsl() returns the raw SAT, UNSAT, UNKNOWN, ERROR or BLOCKED.

If you call the low-level LogicVerifier class directly, every one of its nine public methods now returns a DiagnosticResult:

• verify_logic
• verify_with_quantifiers
• verify_bitvector
• verify_array
• prove_theorem
• check_implication
• check_equivalence
• verify_optimization
• check_vacuity

​

Reading a result

from qwed_new.core.logic_verifier import LogicVerifier

verifier = LogicVerifier()
result = verifier.verify_logic(
    variables={"x": "Int", "y": "Int"},
    constraints=["x > 0", "y > 0", "x + y == 10"],
)

result.is_verified                                  # True
result.status.value                                 # "VERIFIED"
result.developer_fields["deterministic_verdict"]    # "SAT"
result.developer_fields["model"]                    # {"x": "5", "y": "5"}
result.developer_fields["symbol_table"]             # [{"name": "x", "type": "Int"}, {"name": "y", "type": "Int"}]
result.proof_ref                                    # "sha256:..." (present only when VERIFIED)
result.agent_message                                # "Logic constraints are satisfiable — model found"

The three diagnostic layers — agent_message, developer_fields, and proof_ref — are populated on every result. proof_ref is computed from the Z3 solver’s assertion stack and is present only when status == "VERIFIED".

​

SAT/UNSAT status matrix

Z3’s sat/unsat outcome has different meanings depending on the method. The engine disambiguates by mapping each per-method outcome to a DiagnosticResult status and recording the raw Z3 verdict under developer_fields.deterministic_verdict.

Method	Z3 sat	Z3 unsat	Z3 unknown
verify_logic	VERIFIED (model found)	UNVERIFIABLE (no model)	UNVERIFIABLE
verify_with_quantifiers	VERIFIED	UNVERIFIABLE	UNVERIFIABLE
verify_bitvector	VERIFIED	UNVERIFIABLE	UNVERIFIABLE
verify_array	VERIFIED	UNVERIFIABLE	UNVERIFIABLE
prove_theorem	BLOCKED (counterexample)	VERIFIED (theorem proved by contradiction)	UNVERIFIABLE
check_implication	BLOCKED	VERIFIED	UNVERIFIABLE
check_equivalence	BLOCKED (counterexample)	VERIFIED (equivalent)	UNVERIFIABLE
verify_optimization	VERIFIED (optimal model)	UNVERIFIABLE	UNVERIFIABLE
check_vacuity	VERIFIED (non-vacuous)	UNVERIFIABLE (vacuously true)	UNVERIFIABLE

Always branch on result.is_verified (or result.proof_ref is not None) for control flow. Read developer_fields["deterministic_verdict"] for diagnostic context — never for authorization.

​

symbol_table on every VERIFIED result

developer_fields.symbol_table is a sorted list of every declared variable and its type. It is included on every VERIFIED result so audit logs record exactly what was proven:

result.developer_fields["symbol_table"]
# [
#   {"name": "age",  "type": "Int"},
#   {"name": "seat", "type": "BitVec[8]"},
# ]

​

New BLOCKED constraint IDs

Two fail-closed behaviors ship with the migration:

constraint_id	Trigger
logic_verifier.explicit_declarations_required	The variables dict is empty. The previous _infer_variables heuristic has been removed — the engine now refuses to guess types from constraint syntax.
dsl_compiler.type_validation	A variable is declared with a malformed type such as "BitVec" (missing width), "BitVec[]", or "BitVec[abc]". The engine no longer silently defaults to 32-bit; you must declare a valid BitVec[N] with N ≥ 1.

Other constraint_ids used by the engine: logic_verifier.invalid_constraint, logic_verifier.unknown_quantifier, and logic_verifier.execution_error.

​

Migrating from LogicResult

Status field

# Before — LogicResult with a solver-level status string
result = verifier.verify_logic(variables, constraints)
if result.status == "SAT":
    solution = result.model
elif result.status == "UNSAT":
    ...

# After — DiagnosticResult with method-scoped semantics
result = verifier.verify_logic(variables, constraints)
if result.is_verified:
    solution = result.developer_fields["model"]
elif result.developer_fields.get("deterministic_verdict") == "UNSAT":
    ...

Proving a theorem

# Before — SAT meant "theorem is valid"
result = verifier.prove_theorem(variables, premises, conclusion)
if result.status == "SAT":
    ...   # theorem valid
elif result.status == "UNSAT":
    counterexample = result.model

# After — VERIFIED means "theorem proved", BLOCKED means "counterexample found"
result = verifier.prove_theorem(variables, premises, conclusion)
if result.is_verified:
    ...   # theorem proved by contradiction
elif result.status.value == "BLOCKED":
    counterexample = result.developer_fields["model"]

Variable declarations are now mandatory

# Before — the engine tried to infer types from constraint syntax
result = verifier.verify_logic({}, ["x > 5", "P and Q"])
# Types guessed: x -> Int, P/Q -> Bool

# After — empty variables dict fails closed
result = verifier.verify_logic({}, ["x > 5", "P and Q"])
result.status.value                              # "BLOCKED"
result.developer_fields["constraint_id"]         # "logic_verifier.explicit_declarations_required"

Malformed BitVec declarations fail closed

# Before — silently defaulted to 32-bit
result = verifier.verify_bitvector({"x": "BitVec"}, ["x == 0"])

# After — BLOCKED with a type-validation constraint ID
result = verifier.verify_logic({"x": "BitVec"}, ["x == 0"])
result.status.value                              # "BLOCKED"
result.developer_fields["constraint_id"]         # "dsl_compiler.type_validation"

---

​

Performance

Operation	Avg Latency
Simple constraint	5ms
Complex (10+ clauses)	20ms
Quantified	50ms

---

​

Next steps

• DSL reference - Complete operator documentation
• Verification diagnostics - The 3-layer DiagnosticResult model
• Code engine - Verify code correctness
• SQL engine - Verify SQL queries