Zee3.
Copy Markdown
Documentation for Zee3.MARCO algorithm, which implements
the MARCO argoritm
for Zee3-based constraints.
Summary
Functions
Returns all minimum unsatisfiable cores (MSSs) for a set of constraints. Returns a list.
Returns all minimum unsatisfiable cores (MUSs) for a set of constraints. Returns a list.
Returns all maximum satisfying sets (MSSs)
and minimum unsatisfiable cores (MUSs) for a set of
constraints. Returns a list of tuples of
the form {:mss, set} or {:mus, set}.
Enumerate the MSSs for this set of constraints. Returns a Stream.
Enumerate the MUSs for this set of constraints. Returns a Stream.
Enumerate the all the maximum satisfying sets (MSSs)
and minimum unsatisfiable cores (MUSs) for a set of
constraints. Returns a Stream that yields tuples of
the form {:mss, set} or {:mus, set}.
Functions
Returns all minimum unsatisfiable cores (MSSs) for a set of constraints. Returns a list.
This function eagerly evaluates all MSSs, which can take
a rather long time.
If you need control over how long to wait until you quit
generating more sets or if you want to stream sets as they
are generated, use the enumerate_mus/2 function.
The results are sorted by set (generally, smaller sets come first) so that the result of this function is deterministic.
Returns all minimum unsatisfiable cores (MUSs) for a set of constraints. Returns a list.
This function eagerly evaluates all MUSs, which can take
a rather long time.
If you need control over how long to wait until you quit
generating more sets or if you want to stream sets as they
are generated, use the enumerate_mus/2 function.
The results are sorted by set (generally, smaller sets come first) so that the result of this function is deterministic.
Returns all maximum satisfying sets (MSSs)
and minimum unsatisfiable cores (MUSs) for a set of
constraints. Returns a list of tuples of
the form {:mss, set} or {:mus, set}.
This function eagerly evaluates all sets, which can take
a rather long time.
If you need control over how long to wait until you quit
generating more sets or if you want to stream sets as they
are generated, use the enumerate_sets/2 function.
The results are sorted by set (generally, smaller sets come first) so that the result of this function is deterministic.
@spec enumerate_mss(map(), (pid() -> :ok)) :: Enumerable.t(MapSet.t())
Enumerate the MSSs for this set of constraints. Returns a Stream.
Warning
The order of the returned MSSs is non-deterministic
@spec enumerate_mus(map(), (pid() -> :ok)) :: Enumerable.t(MapSet.t())
Enumerate the MUSs for this set of constraints. Returns a Stream.
Warning
The order of the returned MUSs is non-deterministic
@spec enumerate_sets(map(), (pid() -> :ok)) :: Enumerable.t({:mss | :mus, MapSet.t()})
Enumerate the all the maximum satisfying sets (MSSs)
and minimum unsatisfiable cores (MUSs) for a set of
constraints. Returns a Stream that yields tuples of
the form {:mss, set} or {:mus, set}.
Warning
The order of the returned sets is non-deterministic