  We present a CLP(FD)-based constraint solver able to deal with unbounded
domains. It is based on constraint propagation, resorting to enumeration if all
other methods fail. An important aspect is detecting when enumeration was
complete and if this has an impact on the soundness of the result. We present a
technique which guarantees soundness in the following way: if the constraint
solver finds a solution it is guaranteed to be correct; if the constraint
solver fails to find a solution it can either return the result "definitely
false" in case it knows enumeration was exhaustive, or "unknown" in case it was
aborted. The technique can deal with nested universal and existential
quantifiers. It can easily be extended to set comprehensions and other
operators introducing new quantified variables. We show applications in data
validation and proof.
