Concepts
Six things make up the protocol. Everything else is a detail of one of them.
The objects
Section titled “The objects”Library — a dynamically loadable file exporting the thirteen entry points. Found by name, not by path. Declares its capabilities through five lists; those answers are fixed for the life of the library.
Solver — an instance created from a library. Holds options and whatever search state survives between runs. Created, configured, run repeatedly, freed.
Model — the problem. Not a structure you hand over, but a table of callbacks the solver reads through while it searches. Read-only for the duration of a run.
Value — anything that crosses the interface as data. An opaque handle you interrogate for its kind and then read with the matching accessor.
Solution — an assignment to the decision variables, delivered to a callback. Valid only for the duration of that callback.
Layer — a group of decisions and constraints added together, and retracted together. What makes incremental solving possible; see below.
How they relate
Section titled “How they relate”The dashed edge is the one the protocol exists for: the same instance runs again against a changed model, and layers tell it which part of that model it has already seen.
The shape of a session
Section titled “The shape of a session”- Find and open a library by name. The loader searches a fixed list of directories and picks the newest matching version.
- Check the ABI version. Before anything else. See ABI stability.
- Read the capability lists to learn what this solver accepts.
- Create a solver instance.
- Set options — a time limit, a thread count, a random seed.
- Run, passing a model and callbacks.
Solutions arrive at
on_solution; diagnostics aton_message; the search stops when it is complete, or whenshould_stopsays so. - Inspect the status and statistics.
- Change the model and run again. This is the step the protocol exists for.
- Free the instance.
Steps 5 to 8 repeat. Steps 1 to 3 happen once per library.
Incrementality
Section titled “Incrementality”The reason for layers is step 8. A layer groups decisions and constraints so they can be added and retracted together, and because indices follow layer order, nothing that survives a retraction is renumbered. Before each run the model then tells the solver how much of the problem is unchanged, how much is committed for good, and how much has become vacuous — three numbers a solver may exploit or ignore, since re-reading everything is always correct.
The rules are in The model; the workflow in Incremental solving.
Two rules to internalise early
Section titled “Two rules to internalise early”Both cause most first-time bugs, and both are stated in full in Lifetimes & ownership:
nothing you receive is yours — copy anything you want to keep — and accessors have preconditions, so ask a value its kind before reading it and check a length before using an index.