Module domain_tightening 

Infer tighter declaration domains from the constraint list, before rewriting.

The first component looks at cardinality equalities |s| = k (and |s| = |t| when |t| is constant) and, when s is a sequence find, intersects that size into its domain. Indexed equalities forAll i : D . |m[i]| = k_i over a matrix of sequences are included so that each cell can later be represented as a fixed-length sequence.

Functions

tighten_domains_from_constraints

Walk the model’s constraints and tighten declaration domains where a fact can be proved.