Documentation

Assumes simplified, linear, defined.

The name of a variable in the SMT translation.

The name of a boolean variable, representing `fin x`.

Given a model, compute an improving substitution, implied by the model. The entries in the substitution look like this:

• x = A variable x must equal constant A
• x = y variable x must equal variable y
• x = A * y + B (coming soon) variable x is a linear function of y, A and B are natural numbers.

We are mostly interested in improving unification variables. However, it is also useful to improve skolem variables, as this could turn non-linear constraints into linear ones. For example, if we have a constraint x * y = z, and we can figure out that x must be 5, then we end up with a linear constraint 5 * y = z.

Get the value for the given name. * Assumes that we are in a SAT state (i.e., there is a model) * Assumes that the name is in the model

Get the values for the given names.