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

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

`LogicVerifier` returns `DiagnosticResult` (v5.4.0)

Introduced in v5.4.0. LogicVerifier is the second engine — after FactVerifier — to conform to the unified DiagnosticResult contract. The legacy LogicResult dataclass has been removed. The high-level SDK client (client.verify_logic()) and the /verify/logic API endpoint still return the same SAT/UNSAT/UNKNOWN shape shown above.

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

Overview

Core Engines

Analysis Engines

Specialized Engines

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

Capabilities

Quick start

QWED-Logic DSL

Operators

Examples

Satisfiability checking

Basic check

Finding all solutions

Business rules

Age verification

Discount eligibility

Approval workflow

Quantifiers

Universal (FORALL)

Existential (EXISTS)

Security: operator whitelist

Fail-closed constraint parsing

Provider tracking

Error handling

`LogicVerifier` returns `DiagnosticResult` (v5.4.0)

Reading a result

SAT/UNSAT status matrix

`symbol_table` on every VERIFIED result

New `BLOCKED` constraint IDs

Migrating from `LogicResult`

Performance

Next steps

​Capabilities

​Quick start

​QWED-Logic DSL

​Operators

​Examples

​Satisfiability checking

​Basic check

​Finding all solutions

​Business rules

​Age verification

​Discount eligibility

​Approval workflow

​Quantifiers

​Universal (FORALL)

​Existential (EXISTS)

​Security: operator whitelist

​Fail-closed constraint parsing

​Provider tracking

​Error handling

​LogicVerifier returns DiagnosticResult (v5.4.0)

​Reading a result

​SAT/UNSAT status matrix

​symbol_table on every VERIFIED result

​New BLOCKED constraint IDs

​Migrating from LogicResult

​Performance

​Next steps

Capabilities

Quick start

QWED-Logic DSL

Operators

Examples

Satisfiability checking

Basic check

Finding all solutions

Business rules

Age verification

Discount eligibility

Approval workflow

Quantifiers

Universal (FORALL)

Existential (EXISTS)

Security: operator whitelist

Fail-closed constraint parsing

Provider tracking

Error handling

`LogicVerifier` returns `DiagnosticResult` (v5.4.0)

Reading a result

SAT/UNSAT status matrix

`symbol_table` on every VERIFIED result

New `BLOCKED` constraint IDs

Migrating from `LogicResult`

Performance

Next steps