# `Zee3.StdLib.FiniteSet`

Implementation of a custom finite set objecte on top of existing theories.

# `t`

```elixir
@type t() :: %Zee3.StdLib.FiniteSet{
  cardinality: Zee3.Smt2.t(),
  max_size: integer(),
  name: binary(),
  slots: [Zee3.Smt2.t()]
}
```

A type for a `FiniteSet`, for use inside a `Zee3.program`.
This should not be used inside normal Elixir code.
This module contains functionality to extract these sets
from the Zee3 model into elixir `MapSet`s.

# `contains`

```elixir
@spec contains(t(), Zee3.Smt2.smt2_like()) :: Zee3.Smt2.t()
```

Checks that the set contains an element.

# `declare`

```elixir
@spec declare(pid(), binary(), Sort.t(), [{:max_size, integer()}]) :: t()
```

Declare a new finite set.

This will return a `#Zee3.StdLib.FiniteSet<...>`, which can
be used as an argument to the functions in this module.
This struct contains a `:cardinality` field (`set.cardinality`)
which can be used as a constant inside the Zee3 program.
This can be used to assert facts about the cardinality, which
is just a normal integer constant inside Zee3.

Note that this function *does not* declare a normal Z3 constant
which is a set. That is not possible, because Z3 doesn't support
a theory of finite sets. Instead, this function declares a number
of constants and constraints between them in such a way that the
normal axioms of set theory will work.

# `disjoint`

```elixir
@spec disjoint(t(), t()) :: Zee3.Smt2.t()
```

Checks that the sets are disjoint (i.e. they share no elements in common)

# `equal`

```elixir
@spec equal(t(), t()) :: Zee3.Smt2.t()
```

Checks the sets contain exactly the same elements.

# `extract_all_from_model`

```elixir
@spec extract_all_from_model(map()) :: %{required(binary()) =&gt; MapSet.t()}
```

Extracts Z3 finite sets from a model map into Elixir `MapSet`s.

Expects slot keys in the format `__set_slot_000000__set_name`,
which is the format generated by the set declaration functions.

# `extract_from_model`

```elixir
@spec extract_from_model(map(), binary()) :: {:ok, MapSet.t()} | :error
```

Extracts a single Z3 finite set from a model map into an Elixir `MapSet`.
Returns either `{:ok, MapSet.new([...])}` or `:error` if the set does
not exist.

Expects slot keys in the format `__set_slot_000000__set_name`,
which is the format generated by the set declaration functions.

# `extract_from_model!`

```elixir
@spec extract_from_model!(map(), binary()) :: MapSet.t()
```

Extracts a single Z3 finite set from a model map into an Elixir `MapSet`.
Raises on error.

Expects slot keys in the format `__set_slot_000000__set_name`,
which is the format generated by the set declaration functions.

# `subset_of`

```elixir
@spec subset_of(t(), t()) :: Zee3.Smt2.t()
```

Checks that the set on the LHS is a subset of the set on the RHS

# `superset_of`

```elixir
@spec superset_of(t(), t()) :: Zee3.Smt2.t()
```

Checks that the set on the LHS is a superset of the set on the RHS

---

*Consult [api-reference.md](api-reference.md) for complete listing*