mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
enable binary string access to unsigned numerals over API #4568
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4a8533e41f
commit
4b346ef693
|
@ -100,13 +100,21 @@ namespace Microsoft.Z3
|
|||
#endif
|
||||
|
||||
/// <summary>
|
||||
/// Returns a string representation of the numeral.
|
||||
/// Returns a decimal string representation of the numeral.
|
||||
/// </summary>
|
||||
public override string ToString()
|
||||
{
|
||||
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Returns a binary string representation of the numeral.
|
||||
/// </summary>
|
||||
public string ToBinaryString()
|
||||
{
|
||||
return Native.Z3_get_numeral_binary_string(Context.nCtx, NativeObject);
|
||||
}
|
||||
|
||||
#region Internal
|
||||
internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
|
||||
#endregion
|
||||
|
|
|
@ -61,7 +61,7 @@ public class BitVecNum extends BitVecExpr
|
|||
}
|
||||
|
||||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
* Returns a decimal string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
|
@ -69,6 +69,15 @@ public class BitVecNum extends BitVecExpr
|
|||
return Native.getNumeralString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns a binary string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toBinaryString()
|
||||
{
|
||||
return Native.getNumeralBinaryString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
BitVecNum(Context ctx, long obj)
|
||||
{
|
||||
super(ctx, obj);
|
||||
|
|
|
@ -3711,6 +3711,10 @@ class BitVecNumRef(BitVecRef):
|
|||
def as_string(self):
|
||||
return Z3_get_numeral_string(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def as_binary_string(self):
|
||||
return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
|
||||
|
||||
|
||||
def is_bv(a):
|
||||
"""Return `True` if `a` is a Z3 bit-vector expression.
|
||||
|
||||
|
|
Loading…
Reference in a new issue