mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Added is_numeral_negative to .NET and Java APIs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-27 15:07:10 +01:00
parent e4f7ff9881
commit 95d7b33ebb
2 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/dotnet/FPNum.cs
View file

@ -166,6 +166,11 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
/// <summary>
/// Indicates whether the numeral is negative.
/// </summary>
public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
#region Internal #region Internal
internal FPNum(Context ctx, IntPtr obj) internal FPNum(Context ctx, IntPtr obj)
: base(ctx, obj) : base(ctx, obj)

11
src/api/java/FPNum.java
View file

@ -167,6 +167,17 @@ public class FPNum extends FPExpr
return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject()); return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
} }
/**
* Indicates whether the numeral is negative.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isNegative()
{
return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
}
public FPNum(Context ctx, long obj) public FPNum(Context ctx, long obj)
{ {
super(ctx, obj); super(ctx, obj);