Skip to content

Python API · Submodule

alkahest.smt

SMT/SAT bridge — hand a discrete or mixed subproblem to an external solver.

P2 item 3 — see docs/mdbook/src/smt.md.

Discrete and mixed integer/real/boolean problems are not Alkahest's problem class and should not become one. What a search loop needs is not an in-tree solver but a way to hand the subproblem off — and to bring the answer back in a form the rest of the toolchain can trust. This module is that hand-off:

to_smtlib Re-exported from the Rust emitter (alkahest_core::logic::smtlib). Turns a predicate Expr into a complete SMT-LIB 2 script. The emitter is exhaustive over Formula and PredicateKind by construction — rustc refuses to compile a missing case — so a node added later cannot silently emit wrong SMT-LIB.

supported() The plan-ahead predicate, in the spirit of certifiable(): can this formula be sent at all, is a solver installed, and should it be sent rather than kept in-tree.

solve() Runs the solver in a subprocess and returns an SmtResult.

Two asymmetries drive the whole design and are worth stating up front.

sat and unsat are not equally trustworthy. A sat model is checkable inside Alkahest for free: substitute it back and evaluate the formula exactly. solve() always does this — it is not optional and there is no flag to skip it — and a model that fails raises SmtError E-SMT-004 rather than warning, because a failure there means the bridge or the solver is broken. unsat, by contrast, is not machine-checked here at all: consuming an unsat proof is a large project with unstable formats. So an unsat result gets the status EXTERNALLY_ASSERTED, which is deliberately not in alkahest.research.MACHINE_CHECKED_STATUSES. "z3 said so" is a fact about z3, not a proof, and the claim graph must keep being able to tell the two apart.

Exactness is where a model reader breaks. Rationals lift cleanly; algebraic numbers (z3's root-obj) do not, and the tempting move — round to a float — would record an approximation as an exact witness. That is the precise silent error this subsystem exists to prevent, so root-obj is refused with E-SMT-003 until it can be lifted into the real-algebraic machinery (RootInterval / refine_root) that already exists for it.

class

class smt.SmtResult

What an external solver said, and how much of it was checked here.

Quacks like a DerivedResult (value / steps / verification / certificate) so ResearchSession.record accepts it unchanged — and so the honest status travels with it.

Attributes

status{"sat", "unsat", "unknown"}: The solver's verdict.
modeldict[str, Fraction]: Exact rational witness, on sat. Always the values that were actually verified.
model_exprsdict[str, Expr]: The same values interned into an ExprPool, when one was passed or was active via alkahest.context(pool=...). Empty otherwise — an Expr carries no reference to its pool, so this is not always constructible, and model never depends on it.
enginestr: Which solver answered, and at what version. A result that does not say what produced it is not something a loop can weigh.
logicstr: The SMT-LIB logic that was sent.
smtlibstr: The exact script that was sent. Also exposed as certificate.
verificationdict: DerivedResult-shaped: status is exactly_verified for a checked sat model, EXTERNALLY_ASSERTED for unsat, and unverified for unknown. It also carries logic and sorts — see sorts, and read them before you read status: status tells you the answer was checked, sorts tells you which question was answered.
sortsdict[str, str]: Symbol name → the SMT-LIB sort it was declared with, "Int" or "Real", read back out of the script that was actually sent. This is the difference between an integer feasibility question and its real relaxation, and nothing in status or verification ["status"] distinguishes the two: a model of the relaxation is a genuine model of the formula as emitted, so it verifies exactly and reports sat / exactly_verified either way. A symbol lands in Real whenever it was built without an integer domain — check here rather than assume.
badgestr: The unflattering one-line rendering of verification["status"].
reason_unknownstr or None: The solver's own explanation, on unknown.
elapsed_msfloat: Wall-clock time spent in the solver process.

Properties

status: str

model: dict[str, Fraction]

model_exprs: dict[str, Any]

engine: str

logic: str

smtlib: str

verification: dict[str, Any]

reason_unknown: str | None

elapsed_ms: float

raw_output: str

steps: tuple[dict[str, Any], ...]

value: Any

The formula that was asked about — DerivedResult-compatible.

certificate: str

The SMT-LIB script. An artifact, explicitly not a checked proof.

sorts: dict[str, str]

Symbol name → declared SMT-LIB sort ("Int" / "Real").

Recovered from verification so it survives serialisation into a ResearchSession record, where the smtlib text may not.

badge: str

Honest one-line description of what was actually established.

machine_checked: bool

True only when a checker ran in this process.

unsat is never machine-checked here, however confident the solver was.

class

class smt.SmtSupport

The answer to "can I hand this formula to a solver, and should I?".

Truthy exactly when solve() would run, so it drops into if supported(f): — but it carries the reason, which is what a planning loop actually needs. This mirrors _certificates.Certifiability.

Attributes

supportedbool: The verdict: exportable, quantifier-free, and a solver is installed. bool(self) is the same value.
exportablebool: to_smtlib() would succeed. Independent of solver installation, so an emitter-only workflow can rely on it.
quantifiedbool: The formula contains Forall/Exists. to_smtlib() handles these; solve() refuses them, because it guarantees exact in-process model checking and a quantified model has nothing to check.
solverstr or None: The solver solve() would use, or None if none is installed.
logicstr or None: The SMT-LIB logic the emitter chose, e.g. "QF_NRA".
reasonstr: Stable reason code, and the complete set a caller may branch on: "ok", "outside_fragment", "quantified", "not_exactly_checkable", or "no_solver". "not_exactly_checkable" is the one that is easy to miss: the formula exports fine, but the kernel cannot evaluate it exactly at a rational model (abs is the case you will actually hit), so solve() refuses it rather than return a sat it did not check.
detailstr: One-sentence human explanation.
recommendationstr: "smt" or "prefer_in_tree" — see supported().
scriptstr or None: The emitted script, handed back so a caller that goes on to use it does not pay for the export twice.
errorSmtError or None: The refusal solve() would raise: the export error when exportable is False (reason="outside_fragment"), or the E-SMT-002 refusal when reason is "not_exactly_checkable". None otherwise — including for "quantified" and "no_solver".

Properties

supported: bool

exportable: bool

quantified: bool

solver: str | None

logic: str | None

reason: str

detail: str

recommendation: str

script: str | None

error: SmtError | None

function

smt.to_smtlib(
    formula: Any,
    logic: str='auto',
    *,
    check_sat: bool=True,
    get_model: bool=True
) → str

Export a predicate Expr as an SMT-LIB 2 script.

The SMT counterpart of to_lean(): Alkahest emits a standard artifact and an independently maintained external tool consumes it. The emitter itself lives in Rust (alkahest_core::logic::smtlib) so that match exhaustiveness over Formula / PredicateKind enforces total coverage; this wrapper only maps the error type.

Parameters

formulaExpr: A predicate or quantified expression — built with pool.gt/lt/… and And() / Or() / Not(), or Forall() / Exists().
logicstr: "auto" (default) infers the weakest logic that fits: QF_LIA, QF_NIA, QF_LRA, QF_NRA, QF_LIRA, QF_NIRA, their quantified counterparts, or ALL. Naming a logic too weak for the formula is an error (E-SMT-002), not a silent downgrade.
check_sat, get_modelbool: Append (check-sat) / (get-model) and set :produce-models.

Raises

SmtError: E-SMT-002 when the formula is outside the exportable fragment. Use supported() to ask the same question without raising.

Examples

Python

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> print(ak.to_smtlib(ak.And(pool.gt(x, pool.integer(0)), pool.lt(x, pool.integer(3)))))
... # doctest: +SKIP
; alkahest SMT-LIB 2 export
(set-logic QF_LRA)
...

constant

smt.EXTERNALLY_ASSERTED

EXTERNALLY_ASSERTED = 'externally_asserted'

No docstring.

constant

smt.SOLVERS

SOLVERS = tuple(_SPECS)

No docstring.

constant

smt.STATUS_BADGES

STATUS_BADGES = {'exactly_verified': "the solver's model was substituted back and the kernel evaluated the formula to true exactly", EXTERNALLY_ASSERTED: 'an external solver…

No docstring.