SMT

Requires the smt extra (pip install "longeron[smt]").

Requirement consistency and design-space bounds on Z3 (spike).

Complements longeron.analysis.trades (discrete architecture selection, CP-SAT): Z3 works over unbounded reals, so it answers questions CP-SAT’s scaled integers cannot – is a requirement set consistent at all, WHICH requirements conflict (unsat cores), and what are exact feasibility bounds of a continuous attribute (z3.Optimize handles strict inequalities by reporting suprema).

Mapping: scalar attributes of an instantiated part tree -> Z3 Real / Int / Bool consts named by dotted path; attribute value expressions -> equality assertions (omit paths listed in free); assert constraint bodies and requirement assume/require bodies -> labeled assertions; calc invocations are inlined by substitution. Attributes whose values do not depend – transitively – on any free path are CONSTANT under the query and are pinned to their interpreter-exact values instead of being encoded symbolically: the requirement algebra stays symbolic only where the freed variables can actually reach, and physics upstream of them (sqrt/pow/max chains Z3 has no business solving) never hits the solver at all. Sequences, strings, state machines, and -> collection operators are out of scope (recorded in gaps).

Requires the smt extra: pip install "longeron[smt]".

class longeron.analysis.smt.SmtResult(status, witness=<factory>, core=<factory>)

Bases: object

longeron.analysis.smt.SmtStatus

a Z3 check outcome, verbatim

alias of Literal[‘sat’, ‘unsat’, ‘unknown’]

class longeron.analysis.smt.SmtSystem(variables=<factory>, assertions=<factory>, gaps=<factory>)

Bases: object

Z3 variables + labeled assertions for one part tree.

check(exclude=())

SAT + witness, or UNSAT + a labeled conflict core.

Return type:

SmtResult

maximize(path, exclude=())

Supremum of a variable over the feasible region (exact, as text).

Strict inequalities yield open bounds: Z3 reports the supremum with an infinitesimal (e.g. 2865/1090 + -1*epsilon).

Return type:

tuple[str, SmtResult]

longeron.analysis.smt.to_smt(model, part, requirements=(), free=())

Encode a part definition’s tree (and requirements) for Z3.

free names the attribute paths left unconstrained (the query’s variables). Attribute values that cannot be reached by any free path are pinned to their interpreter-exact numbers; the rest are encoded symbolically.

Return type:

SmtSystem