Zee3.StdLib.FiniteSet (zee3 v0.5.0)

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

Summary

Types

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 MapSets.

Functions

contains(set, element)

Checks that the set contains an element.

declare(pid \\ Zee3.current_z3_pid!(), name, element_type, args)

Declare a new finite set.

disjoint(set_a, set_b)

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

equal(set_a, set_b)

Checks the sets contain exactly the same elements.

extract_all_from_model(model)

Extracts Z3 finite sets from a model map into Elixir MapSets.

extract_from_model(model, set_name)

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.

extract_from_model!(model, set_name)

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

subset_of(set_a, set_b)

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

superset_of(set_a, set_b)

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

Types

t()

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

Functions

contains(set, element)

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

Checks that the set contains an element.

declare(pid \\ Zee3.current_z3_pid!(), name, element_type, args)

@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(set_a, set_b)

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

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

equal(set_a, set_b)

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

Checks the sets contain exactly the same elements.

extract_all_from_model(model)

@spec extract_all_from_model(map()) :: %{required(binary()) => MapSet.t()}

Extracts Z3 finite sets from a model map into Elixir MapSets.

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

extract_from_model(model, set_name)

@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!(model, set_name)

@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(set_a, set_b)

@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(set_a, set_b)

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

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