Type type of auxilliary information attached to constraints c:

• prov c is the module in which the constraint was created
• span c is the originating location of the rhs of the constraint

INV: CInfo does not determine equality of constraints.

The type of constraints c of shape guard c ? left c ⊆ right c that originated from the source at srcSpan c.

Given an atomic constraint a, isTriviallyUnsat a just if a is of the form G ? k in {}.

Given two atomic constraints a and b, a impliedBy b just if a and b have the same body and the guard of a is implied by the guard of b.

Given an atomic constraint a, tautology a just if a is satisfied in every assignment.

When m is the current module: Given atomic constraints a and b, resolve m a b is:

• Nothing if the resolvant of a and b is a tautology
• Just r otherwise, where r is the resolvant as an atomic constraint

The type of sets of constraints.

We say that a set of constraints cs is reduced just if, for all X, d, Y, k: definiteVV cs X d Y, definiteKV cs X d k and goal cs are non-increasing lists wrt impliedBy.

We say that a set of constraints cs is an antichain just if each of these lists are also non-decreasing.

Most sets of constraints we process are reduced, but we allow non-reduced constraint sets to occur as a consequence of renaming of variables.

Many sets of constraints are also antichains, for example, when filtering a reduced constraint set one can guarantee the new constraint set will be an antichain by using insert and constructing the new constraint set in the reverse order. Constraint sets returned from saturation will always be antichains.

Given a list of atomic constraints cs, fromList cs is largest antichain contained in cs

empty is the empty constraint set

Given a constraint set cs, unsats cs is the constraint set consisting of just those trivially unsatisfiable constraints in cs.

When cs is a constraint set, size cs is its cardinality.

When a is an atomic constraint and cs a constraint set, unsafeInsert a cs is the constraint set obtained by inserting a into cs.

Note: unsafeInsert a cs may not be reduced even if cs is.

When a is an atomic constraint and cs is a constraint antichain insert a cs is:

• Nothing just if a is already implied by some constraint in cs.
• Just ds otherwise, where ds is the constraint antichain obtained by inserting a into cs. Note: ds may be smaller than cs.

When a is an atomic constraint and cs is a constraint set insert a cs is the constraint set obtained by inserting a into cs.

If cs is reduced then so is insert a cs. However, insert a cs may not be an antichain even when cs is.

When g is a guard and cs a set of constraints, guardWith g cs is the set of constraints obtained from cs by appending g to every guard of every constraint.

When iface is a set of interface variables and ci is the current ctx and cs is a constraint set, saturate ci iface cs is the constraint set obtained from cs by saturation and restriction to iface.

Given a set of interface variables exts and a constraint c, eligible exts c just if there are no interface variables in the head of c and only interface variables elsewhere in c.

(This means it is eligible to be used as the left-constraint in a resolution step.)

Given some context ci and constraints cs attempt to build a model of cs. cexs ci cs is the set of trivially unsatisfiable constrants obtained from the candidate model.

When exts is the set of interface variables and ci is the current ctx fix ci exts is the stateful computation that transforms an initial state (ls, rs) where ls are all unit constraints modulo exts and ls is contained in rs, into a final state (ls', rs') in which ls is empty and rs' is the saturation of rs.

When exts is a set of interface variables and ci is the current ctx saturate1 ci exts is the stateful computation that takes an initial state (ls, rs) consisting of a pair of constraint sets with ls being unit clauses modulo exts and ls being contained in rs to a final state (ls', rs') in which:

• ls' is those constraints in rs' that are not in rs and which are unit modulo exts.
• rs' contains all the constraints obtained from rs by resolving on the left with each clauses from ls once.