Implement #51368: php_filter_float does not allow custom thousand separators

Implement #51368: php_filter_float does not allow custom thousand separators

A set of hard-coded thousand separator characters (presently, `',.`) is
somewhat limited (users may prefer other separators, such as spaces or
underscores), as well as somewhat too liberal (arbitrary combinations
of different thousand separators are presently possible).  Therefore we
introduce a `thousand` option analogous to `decimal`, which allows to
define the desired thousand separators as non-empty string, defaulting
to `',.`.  While we easily could support empty strings here as well,
that would not make much sense, since this behavior can more easily be
accomplished by not setting the `FILTER_FLAG_ALLOW_THOUSAND` flag in
the first place.