mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
updated documentation for finite domain sizes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
01d59d2c91
commit
7bbabcdf6d
|
@ -303,6 +303,9 @@ namespace Microsoft.Z3
|
|||
|
||||
/// <summary>
|
||||
/// Create a new finite domain sort.
|
||||
/// <param name="name">The name used to identify the sort</param>
|
||||
/// <param size="size">The size of the sort</param>
|
||||
/// <returns>The result is a sort</returns>
|
||||
/// </summary>
|
||||
public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
|
||||
{
|
||||
|
@ -315,6 +318,11 @@ namespace Microsoft.Z3
|
|||
|
||||
/// <summary>
|
||||
/// Create a new finite domain sort.
|
||||
/// <param name="name">The name used to identify the sort</param>
|
||||
/// <param size="size">The size of the sort</param>
|
||||
/// <returns>The result is a sort</returns>
|
||||
/// Elements of the sort are created using <seealso cref="MkNumeral"/>,
|
||||
/// and the elements range from 0 to <tt>size-1</tt>.
|
||||
/// </summary>
|
||||
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
|
||||
{
|
||||
|
|
|
@ -1721,6 +1721,8 @@ extern "C" {
|
|||
To create constants that belong to the finite domain,
|
||||
use the APIs for creating numerals and pass a numeric
|
||||
constant together with the sort returned by this call.
|
||||
The numeric constant should be between 0 and the less
|
||||
than the size of the domain.
|
||||
|
||||
\sa Z3_get_finite_domain_sort_size
|
||||
|
||||
|
|
Loading…
Reference in a new issue