mirror of
https://github.com/Z3Prover/z3
synced 2025-06-19 12:23:38 +00:00
charsort
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
97a035fd6d
commit
79c261736b
2 changed files with 2 additions and 7 deletions
|
@ -156,11 +156,11 @@ namespace Microsoft.Z3
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Retrieves the String sort of the context.
|
/// Retrieves the String sort of the context.
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public SeqSort CharSort
|
public CharSort CharSort
|
||||||
{
|
{
|
||||||
get
|
get
|
||||||
{
|
{
|
||||||
if (m_charSort == null) m_charSort = new CharSort(this, Native.Z3_mk_char_sort(nCtx)); return m_charSort;
|
if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -33,11 +33,6 @@ namespace Microsoft.Z3
|
||||||
{
|
{
|
||||||
Debug.Assert(ctx != null);
|
Debug.Assert(ctx != null);
|
||||||
}
|
}
|
||||||
internal SeqSort(Context ctx)
|
|
||||||
: base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
|
|
||||||
{
|
|
||||||
Debug.Assert(ctx != null);
|
|
||||||
}
|
|
||||||
#endregion
|
#endregion
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue