smt

Generated by sema doc from the compiler’s authoritative native-signature registry.

smt (native adapter)

Governed bounded QF_LIA/QF_LRA decision adapter — bring it in with import smt; calls require proc.run, checked counterexamples disprove, and external unsat remains unverified.

formal

smt.solve(claim, logic) -> SmtResult

Request a bounded external SMT decision. Exact counterexamples are independently replayed; unsat remains digest-bound unverified solver evidence and never becomes Proved.

• domain: one UTF-8 equation-language claim up to 64 KiB in the bounded quantifier-free linear fragment and the exact literal theory QF_LIA or QF_LRA; at most 20,000 AST nodes, depth 256, 64 variables, 1 MiB script/output, 5 s solver soft timeout, and 31 s host deadline; the configured Z3 executable is resource-gated before version probing
• shape: finite set / three-valued logic
• returns: SmtResult
• effects: proc.run
• example: smt.solve("\"x\" < \"y\" implies \"x\" + 1 <= \"y\"", "QF_LIA")

smt.check(claim, logic) -> SmtResult

Produce and integrity-check replayable solver evidence. A checked counterexample disproves the claim; external unsat is explicitly unverified until an independent proof object exists.

• domain: the same bounded QF_LIA/QF_LRA claim, solver, resource, size, variable, and timeout contract as smt.solve
• shape: finite set / three-valued logic
• returns: SmtResult
• effects: proc.run
• example: smt.check("\"x\" < \"y\" implies \"x\" + 1 <= \"y\"", "QF_LRA")

smt.prove(claim, logic) -> SmtResult

Produce an immutable sema.smt-proof/v1 object only after solver-independent exhaustive native replay. Proved results bind the canonical negated obligation, theory, kernel, atom set, assignment count, single-assertion unsat core, and proof reference.

• domain: one UTF-8 equation-language QF_LIA/QF_LRA claim up to 64 KiB; exact linear normalization followed by exhaustive replay of at most 4,096 formula nodes and all valuations of at most 12 independent normalized atoms; returns typed Unknown outside this deliberately bounded proof calculus and never invokes an external solver
• shape: finite set / three-valued logic
• returns: SmtResult
• example: smt.prove("\"x\" < 0 or \"x\" >= 0", "QF_LRA")

smt.verify(claim, proof) -> SmtResult

Replay a checked SMT proof against the caller-supplied claim and return a fresh immutable authenticated SmtResult. This API never trusts Z3 output, nominal type names, or a proof_ref without re-running the bounded native proof calculus.

• domain: one UTF-8 equation-language claim up to 64 KiB plus an exact sema.smt-proof/v1 SmtProofObject; the proof-carried QF_LIA/QF_LRA theory, every identity field, canonical obligation, atom valuation, and native unsat core are re-derived; malformed objects fail typed and rejected proofs remain unaccepted
• shape: scalar
• returns: SmtResult
• example: smt.verify("\"x\" = \"x\"", smt.prove("\"x\" = \"x\"", "QF_LIA").proof_object)