How should I represent user-defined types that are SMT bit-vectors

I'd like to create user-defined types to represent IP addresses. Specifically, a `bv[32]` to represent an IPv4 address and a `bv[128]` to represent an IPv6 address. Since `i32` is interchangeable with `bv[32]` I'm currently just doing:

```
type ipv4address = i32
```

And then I can parse an IPv4 address from a string to a 32-bit integer:

```
fun parseIPv4Address(address: string) : ipv4address option = ...

rel ipv4addresses(string, ipv4address option)
ipv4addresses("11.2.3.4", parseIPv4Address("11.2.3.4")).
```

And when I run with `--dump-all` I do see this relation:

```
ipv4addresses("11.2.3.4", some(184681220))
```

Where `184681220` is the decimal representation of that IPv4 address.

However, this won't work for IPv6 addresses since there is no corresponding native 128-bit type. Additionally, I'd like to extend this to represent CIDR ranges / subnetworks. For example, the CIDR `192.168.0.0/16` represents the range of IP addresses from `192.168.0.0` to `192.168.255.255`. I'd like to represent this as an SMT bit vector where the first 16-bits are fixed (has the values from the first two octets, `192` and `168`) and the last 16-bits are free. This representation makes it very easy to check if a (concrete) IP address is in the range of a CIDR. And I'll be using IP addresses and CIDRs to build out models of firewalls and routing tables.

So my questions are:

1. How can I define a user-type that is just an arbitrary-length SMT bit-vector?
2. Once that's done, I'll need functions that parse IP address (or CIDR) strings to their binary representations. I'll also need functions that can check if a particular IP address is within the CIDR range. Can these just functions written in ML+SMT? Or do I need something else to manipulate these bit-vectors?