molfoundry.FlowModelSMT#

class molfoundry.FlowModelSMT(dg)#

Bases: object

An SMT (z3) integer-flow model over a derivation graph.

A drop-in analogue of FlowModel that uses z3 instead of Gurobi. On construction it creates one integer firing-count variable per hyperedge (reaction) and records the per-vertex stoichiometry. The caller then declares inflow / outflow on individual vertices, optionally sets a custom objective (the default minimizes the total number of reactions), and solves.

The mass-balance constraints – produced - consumed + inflow - outflow = 0 for every vertex – are added automatically the first time the model is solved, so inflow / outflow must be declared before solving.

The underlying z3.Solver (holding the constraints) is exposed via model, and the z3 module via z3, so extra constraints can be built directly (fm.model.add(...)); the objective is set through set_objective(). n-best enumeration finds the optimum with a z3.Optimize, blocks it, and re-optimizes for the next best.

Example:

from molfoundry import FlowModelSMT

fm = FlowModelSMT(dg)
fm.add_in_flow(dg.findVertex(a), 6, 6)
fm.add_in_flow(dg.findVertex(water), 1, 1)
for v in dg.vertices:
        fm.add_out_flow(v, 0, None)
sink = dg.findVertex(product)
fm.add_out_flow(sink, 1, None)
# Minimize reactions while maximizing the sink outflow.
fm.set_objective(
        fm.z3.Sum([fm.reaction_var(e) for e in dg.edges])
        - 1000 * fm.out_flow_var(sink)
)
for solution in fm.enumerate_solutions(100):
        ...
Parameters:

dg (DG)

property model#

The underlying z3.Solver holding the constraints, for arbitrary customization (add constraints with fm.model.add(...)). The objective is managed separately via set_objective().

reaction_var(edge)#

The integer firing-count variable for edge.

Parameters:

edge (HyperEdge)

Return type:

Any

in_flow_var(vertex)#

The inflow variable for vertex, or None if none was added.

Parameters:

vertex (Vertex)

Return type:

Any | None

out_flow_var(vertex)#

The outflow variable for vertex, or None if none was added.

Parameters:

vertex (Vertex)

Return type:

Any | None

add_in_flow(vertex, lo=0, hi=None)#

Declare an inflow (source) on vertex bounded to [lo, hi].

hi=None leaves the inflow unbounded above. Returns the created variable (also reachable later via in_flow_var()).

Parameters:
Return type:

Any

add_out_flow(vertex, lo=0, hi=None)#

Declare an outflow (sink) on vertex bounded to [lo, hi].

hi=None leaves the outflow unbounded above. Returns the created variable (also reachable later via out_flow_var()).

Parameters:
Return type:

Any

set_objective(expr, sense=ObjectiveSense.MINIMIZE)#

Set the objective; sense is ObjectiveSense.MINIMIZE (the default) or ObjectiveSense.MAXIMIZE.

Parameters:
Return type:

None

optimum(time_limit=None)#

Solve for a single optimal flow, or None if the model is infeasible.

Parameters:

time_limit (float | None)

Return type:

FlowSolution | None

enumerate_solutions(max_num_solutions, time_limit=None)#

Enumerate up to max_num_solutions best flows, best objective first.

Finds the optimum with a z3.Optimize, then blocks each solution and re-optimizes for the next best, so solutions are yielded in nondecreasing (for ObjectiveSense.MINIMIZE) / nonincreasing (for ObjectiveSense.MAXIMIZE) objective order. time_limit (seconds) bounds each individual solve.

Yields:

FlowSolution objects, best objective first.

Parameters:

  • max_num_solutions (int)

  • time_limit (float | None)

Return type:

Iterator[FlowSolution]

dispose()#

Release solver resources (a no-op for z3; provided for API parity).

Return type:

None