mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

add char sort to .net

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-13 19:43:12 +02:00
parent 1b648437b7
commit 97a035fd6d
3 changed files with 59 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/api/dotnet/Context.cs
View file

@ -89,7 +89,6 @@ namespace Microsoft.Z3
/// </remarks>
public IntSymbol MkSymbol(int i)
{
return new IntSymbol(this, i);
}
@ -98,7 +97,6 @@ namespace Microsoft.Z3
/// </summary>
public StringSymbol MkSymbol(string name)
{
return new StringSymbol(this, name);
}
@ -107,7 +105,6 @@ namespace Microsoft.Z3
/// </summary>
internal Symbol[] MkSymbols(string[] names)
{
if (names == null) return null;
Symbol[] result = new Symbol[names.Length];
for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
@ -120,6 +117,7 @@ namespace Microsoft.Z3
private IntSort m_intSort = null;
private RealSort m_realSort = null;
private SeqSort m_stringSort = null;
private CharSort m_charSort = null;
/// <summary>
/// Retrieves the Boolean sort of the context.
@ -155,6 +153,18 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Retrieves the String sort of the context.
/// </summary>
public SeqSort CharSort
{
get
{
if (m_charSort == null) m_charSort = new CharSort(this, Native.Z3_mk_char_sort(nCtx)); return m_charSort;
}
}
/// <summary>
/// Retrieves the String sort of the context.
/// </summary>
@ -2385,6 +2395,16 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
}
/// <summary>
/// Convert a bit-vector expression, represented as an unsigned number, to a string.
/// </summary>
public SeqExpr UbvToString(Expr e)
{
Debug.Assert(e != null);
Debug.Assert(e is ArithExpr);
return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
}
/// <summary>
/// Convert an integer expression to a string.
/// </summary>