Returns the value of e in cutsat's current candidate assignment if that value is an
integer. e may be an Int term, or a Nat term whose cast to Int has been
internalized by cutsat. The result is a heuristic, not a guarantee: the assignment may
contain rational or default values (e.g. from eliminated or skipped variables), in which
case it is not a model of the integer constraints; such values are filtered per term.
This is sufficient for model-based theory combination, which only uses the values to
propose case splits. The homomorphism engine is the intended client: all homomorphism
target domains are handled by cutsat, so the result type is Int.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.