SporeLanguage referenceAbout the solverHow it solves
Configurator demo
engine.c

What happens when you pick a value

The public surface is small: load a knowledge base, write a few committed values, call solve_config(), read the rest. This page is about that one call — the restrict/infer walk it runs on every change, and the two kinds of state, committed and derived, that walk works with.


Memory

One array. Two kinds of state.

There is no malloc. Working state lives in a single int heap[], carved by a bump allocator that only resets when a new KB is loaded. Characteristics, domains, chosen sets, condition lists — all the same shape: a count, then values. That is why the same file compiles for a PC and for a chip with 2 KB of RAM. The interesting split is not how the bytes are packed. It is what is allowed to survive a solve.

Committed

The chosen value, plus a mark that says whether it is still a default or an explicit pick. This is the only memory that lasts across solve_config() calls. The writers are the host (set_cstic, set_cstic_observed, unset_cstic) and the procedures in the KB. One exception, below: a domain that has narrowed to a single remaining value is promoted into a committed default.

Derived

The live domain, the RANGE interval, invisible / required / no-input, conflict, incomplete. A pure function of whatever is currently committed. Thrown away and rebuilt every solve. A restriction and a property restriction are the same kind of thing under this split — a different output shape (a set vs. a bool), not a different mechanism.


A pick

Choosing a value does not shrink its own domain

set_cstic is an admission gate. The value has to still be in the current domain (or inside the current RANGE interval). If it is not, the engine rejects the write and flags a conflict — it does not store an illegal pick and mark the configuration bad around it.

If the write is accepted, a SINGLE stores the value and clears default-provenance. It does not remove the other options from the domain. Picking HOME out of {HOME, AWAY} must leave AWAY selectable; only a restriction is allowed to take it off the table. A RANGE commit is different: it pins the interval to that single point, like a setpoint. A MULTI adds the value to a set and, if a default had already placed it there, upgrades it to an explicit pick.

A sensor path (set_cstic_observed) skips the gate and does not pin anything. The next reading is allowed to move. The world is not a product option.


solve_config()

Throw the derived state away. Rebuild it.

If the last pick was already rejected, the call returns immediately — otherwise that rejection would be lost. Then the engine forgets every still-revocable default, restores every domain to the authored baseline, and re-applies class defaults. Explicit picks stay. From there it is a short loop, capped at eight passes, until nothing changes.

1

Reopen, then intersect

Every pass starts from the declared domains again. Restrictions only ever intersect — they never add a value back — so running them on last pass’s already-narrowed domain would ratchet the configuration into a hole it could not leave. Each restriction whose condition currently holds shrinks its target. Several restrictions on the same target just all fire; that is how OR falls out without a special case.

2

Retract a default that no longer fits

If a still-defaulted value now sits outside its own domain, it is cleared. An explicit pick in the same situation is left alone: that is a real conflict. Retracting here, before the emptiness check, gives the same pass a chance to infer the new singleton instead of reporting CONFIG_BAD and stopping.

3

Procedures write committed state

$SET, $SET_DEFAULT, $DEL_DEFAULT, and the expression forms of SET run next, gated on their own conditions. A $SET is the same sticky write as a user pick. A $SET_DEFAULT only lands where nothing is committed yet (on a MULTI, per value, as a union). Arithmetic in a SET expression is a tiny RPN stack over currently committed scalars — not a second solver.

4

Then ask if anything is empty

Procedures run before the emptiness check so a restriction that narrows a slot and a $SET that forces the remaining value can settle in the same pass. If a domain is empty, or a committed value no longer sits in its domain, the configuration is bad. A MULTI with an empty domain and nothing chosen is fine — a checklist with nothing applicable is a legal state. A MULTI whose chosen values are no longer in the domain is not.

5

A singleton becomes a default

A SINGLE domain with one remaining uncommitted value, or a RANGE interval narrowed to a single point, is promoted into a committed default. That is the one place derived state is allowed to write committed memory — and it is marked revocable, so a later restriction can still take it back.

When the loop quiets down, properties are judged against that final state: invisible, required, no-input, then preconditions (visible if any one row holds). Completeness is last. Incomplete is not a conflict. A required, visible slot with no value is unfinished work, not an illegal combination.


Soundness

A condition only fires on a fact, never on a guess

Every branch of a condition asks something that is already unavoidable: a value is committed, a domain has narrowed to exactly this, a RANGE interval is entirely below a threshold. It never asks “what if the user later picks X.” That is why the engine never shrinks a domain on a hypothetical, and why a silent RANGE sensor is not treated as its authored interval.

The cost is the usual one for a propagation-only CSP: some infeasibilities only show up after a search that actually guesses. On the board, that is accepted. On a PC, search_complete() can sit on top of the same set_cstic / solve_config and try the remaining SINGLE values, snapshotting the whole heap at each choice point so a dead end restores exactly. It can prove unsatisfiable. It is not compiled into the AVR build.


Why this shape

Full recompute is the feature

Incremental solvers cache derived facts and patch them. That is faster, and it is a class of bugs: a cached domain that no longer matches the commits. Spore pays the full restrict/infer walk on every change so that class cannot exist. For the size of KB that fits in 800 bytes of heap, the walk is the cheap part. The expensive part, on a microcontroller, is having a second copy of the truth.

The host’s job after a solve is to read, not to remember. Show the live domain. Hide what is invisible. Drive an actuator from what is chosen. On the next tick, write the new sensor value, solve again, throw the last derived picture away.