Solver

Solver Module

The solver is the heart of atopile's parameter subsystem: it symbolically simplifies and checks constraint systems built from Parameters, Literals (Sets), and Expressions.

If you are touching solver internals, read these first:

• src/faebryk/core/solver/README.md (concepts, set correlation, append-only graphs, canonicalization)
• src/faebryk/core/solver/symbolic/invariants.py (the actual invariants enforced during expression insertion)

Quick Start

import faebryk.core.node as fabll
import faebryk.library._F as F
from faebryk.core.solver.defaultsolver import DefaultSolver
from faebryk.libs.test.boundexpressions import BoundExpressions

E = BoundExpressions()

class _App(fabll.Node):
    x = F.Parameters.NumericParameter.MakeChild(unit=E.U.dl)

app = _App.bind_typegraph(tg=E.tg).create_instance(g=E.g)
x = app.x.get().can_be_operand.get()
E.is_subset(x, E.lit_op_range(((9, E.U.dl), (11, E.U.dl))), assert_=True)

solver = DefaultSolver()
res = solver.simplify(g=E.g, tg=E.tg, terminal=True).data.mutation_map
lit = res.try_extract_superset(app.x.get().is_parameter_operatable.get(), domain_default=True)
assert lit is not None

Relevant Files

• Solver runtime + orchestration:
  • src/faebryk/core/solver/defaultsolver.py (DefaultSolver, iteration loop, terminal vs non-terminal)
  • src/faebryk/core/solver/solver.py (solver protocol + helper APIs)
• Mutation machinery (this is where “graphs are append-only” is handled):
  • src/faebryk/core/solver/mutator.py (Mutator, Transformations, MutationStage, MutationMap, tracebacks)
• Symbolic layer (canonical forms + invariants):
  • src/faebryk/core/solver/symbolic/invariants.py (insert_expression(...) invariant pipeline)
  • src/faebryk/core/solver/symbolic/canonical.py (canonicalization passes)
  • src/faebryk/core/solver/symbolic/* (structural + expression-wise algorithms)
• Domain objects (what users actually create in graphs):
  • src/faebryk/library/Parameters.py (ParameterOperatables, domains, compact repr)
  • src/faebryk/library/Expressions.py (expression node types, predicates, assertables)
  • src/faebryk/library/Literals.py (Sets; numeric/boolean/enum literals)
• Test helpers:
  • src/faebryk/libs/test/boundexpressions.py (concise graph + expression construction for tests)

Dependants (Call Sites)

• Library components (src/faebryk/library/): define parameters/constraints (e.g. R.resistance)
• Compiler + frontends: translate ato constraints into solver expressions
• Picker backend: uses solver simplification + bounds extraction to prune candidate parts

How to Work With / Develop / Test

Mental Model (the parts that matter for correctness)

1) Literals are Sets (and correlation is subtle)

• A literal like 100kOhm +/- 10% is a Set (a range), not a scalar.
• Singleton sets are self-correlated; all other sets are treated as uncorrelated, even with themselves.
  • This is why X - X is not necessarily {0} when X is a range, but is {0} when X is a singleton.

2) Symbols (Parameters) introduce correlation

• A Parameter behaves like a mathematical symbol (variable), not a Python variable.
• Correlation between symbols is created via asserted constraints, most notably:
  • Is(A, B).assert_() / A.alias_is(B) creates a strong “these are the same” correlation.
  • IsSubset(A, X).assert_() / A.constrain_subset(X) constrains A to be within X.
  • IsSubset(X, A).assert_() / A.constrain_superset(X) constrains A to accept at least X.

3) Expressions are graph objects (not just Python trees)

Expressions are nodes in the Faebryk graph that point at operand nodes. This matters because…

4) The underlying graphs are append-only

The solver cannot “edit” an expression in-place. Instead it:

• builds a new graph containing transformed/copied nodes,
• records a mapping from old nodes → new nodes (MutationMap),
• leaves the old graph untouched.

Development Workflow

1. Reproduce in a minimal graph (prefer tests + BoundExpressions).
2. Run DefaultSolver().simplify(...) and inspect the resulting MutationMap.
3. If you’re changing rewrite logic, make sure you understand and preserve the invariant pipeline in src/faebryk/core/solver/symbolic/invariants.py::insert_expression.
4. Add/adjust algorithms in src/faebryk/core/solver/symbolic/* (most logic lives there, not in mutator.py).

Testing

• Solver tests live in test/core/solver/:
  • test/core/solver/test_solver.py
  • test/core/solver/test_literal_folding.py
  • test/core/solver/test_solver_util.py

Run a tight loop while iterating:

• ato dev test --llm test/core/solver -k invariant -q
• ato dev test --llm test/core/solver/test_solver.py::test_simplify -q

Best Practices

Prefer explicit simplify(...) arguments

DefaultSolver.simplify has a compatibility layer that accepts (tg, g) or (g, tg). In new code, prefer named args:

res = DefaultSolver().simplify(g=g, tg=tg, terminal=True)
mutation_map = res.data.mutation_map

Use the Mutator/insert_expression pipeline, not ad-hoc rewrites

When you “create” or “rewrite” an expression, you are really requesting that the solver insert something into the transient graph while upholding invariants. The canonical place where this happens is:

• src/faebryk/core/solver/symbolic/invariants.py::insert_expression

If you bypass this, you will almost certainly violate an invariant and get:

• duplicate/congruent expressions,
• multiple incompatible bounds on an operand,
• predicates used as operands,
• missed literal folding, or
• contradictions that don’t point back to the real root cause.