Incremental solving

Layers are what make the loop this interface exists for cheaper on its second pass than its first. The rules are in The model; this is how to use them.

For applications

A model starts with one permanent base layer. Push a layer to add decisions and constraints as a group; pop it to retract the whole group.

Python

model = fznso.LayeredModel()
x = model.add_decision(var_int, range(1, 101), name="x")   # base layer
model.add_constraint("int_lin_le", [[1], [x], 50])         # x <= 50

solver.run(model, on_solution=record)

model.push_layer()
model.add_constraint("int_lin_le", [[-1], [x], -20])       # x >= 20
model.set_unchanged(1)                                     # the base layer is untouched
solver.run(model, on_solution=record)                      # solved incrementally

model.pop_layer()                                          # retract that constraint
model.set_unchanged(1)                                     # ...and still is
solver.run(model, on_solution=record)                      # back to the original problem

Rust

let mut model = LayeredModel::default();
let x = model.add_decision(var_int, domain, Some("x".into()), false, true, vec![]);

solver.run(&model, &mut record, ignore_messages(), dont_interrupt());

model.push_layer();
let _ = model.add_constraint("int_lin_le", vec![/* x >= 20 */], None, vec![]);
model.set_unchanged(1);   // the base layer is untouched
solver.run(&model, &mut record, ignore_messages(), dont_interrupt());

model.pop_layer();
model.set_unchanged(1);
solver.run(&model, &mut record, ignore_messages(), dont_interrupt());

C++

fznso::LayeredModel model;
fznso::Decision x = model.add_decision(INT_VAR, fznso::OwnedValue::int_range(1, 100), "x");

solver.run(model, record);

model.push_layer();
model.add_constraint("int_lin_le", {/* x >= 20 */});
model.set_unchanged(1);   // the base layer is untouched
solver.run(model, record);

model.pop_layer();
model.set_unchanged(1);
solver.run(model, record);

Because indices follow layer order, popping never renumbers anything that survives: x is still decision 0.

Choosing the right kind of layer

Push a plain layer for anything you might retract: a hypothesis, a user’s tentative choice, a branch of your own search.

mark_permanent() promises that every layer currently in the model will never be retracted, and none of them can be popped again. That promise buys something real: the solver may fold those constraints irreversibly into its own representation, simplify against them, and discard the original form.

mark_redundant(layer) says a permanent layer has become vacuous — typically because a later layer’s stronger constraint subsumes it. The solver may then drop it, which is not the same as retracting it: a permanent layer can only be made irrelevant, never removed.

What the solver sees

LayeredModel reports the three layer counts correctly for free. Over your own structures you maintain them yourself — and reporting layer_unchanged as 0 every time is always correct, since it just means the solver re-reads everything.

Caution

Reporting a layer as unchanged when it is not is the one way to get a wrong answer. The solver will skip it, and search a problem you did not pose.

For solvers

Reading layer_unchanged is optional. A solver that ignores it and re-posts the whole model on every run is correct, and is the right place to start.

To exploit it:

pseudocode

n = model.layer_unchanged()

if n == 0 or n < layers_i_have_posted:
    reset everything and post from layer 0
else:
    keep my state through layer n-1
    post decisions   decision_layer_end(n-1)   .. decision_len()
    post constraints constraint_layer_end(n-1) .. constraint_len()

You may not assume the layer count only grows. A pop reduces it, and a push after a pop can put different content at the same index — which is why layer_unchanged exists rather than being inferred from the count.