From bebad7da50496164b81f4b4b17c7be887a0e1d51 Mon Sep 17 00:00:00 2001 From: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com> Date: Sun, 15 Mar 2026 10:36:17 -0700 Subject: [PATCH] Add numeral extraction helpers to Java API (#8978) New methods: - Expr.getNumeralDouble(): retrieve any numeral as a double - IntNum.getUint(): extract numeral as unsigned 32-bit value - IntNum.getUint64(): extract numeral as unsigned 64-bit value - RatNum.getSmall(): numerator/denominator as int64 pair - RatNum.getRationalInt64(): numerator/denominator (returns null on overflow) Each is a thin wrapper around the existing Native binding. Added examples to JavaExample.java covering all new methods. --- examples/java/JavaExample.java | 62 +++++++++++++++++++++++++++++++++- src/api/java/Expr.java | 9 +++++ src/api/java/IntNum.java | 27 +++++++++++++++ src/api/java/RatNum.java | 28 +++++++++++++++ 4 files changed, 125 insertions(+), 1 deletion(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 734f410dd..2a02009af 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2277,7 +2277,64 @@ class JavaExample } - @SuppressWarnings("unchecked") + void numeralDoubleExample(Context ctx) throws TestFailedException + { + System.out.println("NumeralDoubleExample"); + Log.append("NumeralDoubleExample"); + + IntNum n42 = ctx.mkInt(42); + if (n42.getNumeralDouble() != 42.0) + throw new TestFailedException(); + + RatNum half = ctx.mkReal(1, 2); + if (Math.abs(half.getNumeralDouble() - 0.5) > 1e-10) + throw new TestFailedException(); + + System.out.println("NumeralDoubleExample passed."); + } + + void unsignedNumeralExample(Context ctx) throws TestFailedException + { + System.out.println("UnsignedNumeralExample"); + Log.append("UnsignedNumeralExample"); + + IntNum n100 = ctx.mkInt(100); + if (n100.getUint() != 100) + throw new TestFailedException(); + + IntNum big = ctx.mkInt(3000000000L); + if (big.getUint64() != 3000000000L) + throw new TestFailedException(); + + System.out.println("UnsignedNumeralExample passed."); + } + + void rationalExtractionExample(Context ctx) throws TestFailedException + { + System.out.println("RationalExtractionExample"); + Log.append("RationalExtractionExample"); + + RatNum r34 = ctx.mkReal(3, 4); + + // getSmall returns [numerator, denominator] + long[] small = r34.getSmall(); + if (small[0] != 3 || small[1] != 4) + throw new TestFailedException(); + + // getRationalInt64 returns [numerator, denominator] or null + long[] ri64 = r34.getRationalInt64(); + if (ri64 == null || ri64[0] != 3 || ri64[1] != 4) + throw new TestFailedException(); + + // integer as rational: 7/1 + RatNum r71 = ctx.mkReal(7, 1); + long[] small71 = r71.getSmall(); + if (small71[0] != 7 || small71[1] != 1) + throw new TestFailedException(); + + System.out.println("RationalExtractionExample passed."); + } + void isGroundExample(Context ctx) throws TestFailedException { System.out.println("IsGroundExample"); @@ -2465,6 +2522,9 @@ class JavaExample p.finiteDomainExample(ctx); p.floatingPointExample1(ctx); // core dumps: p.floatingPointExample2(ctx); + p.numeralDoubleExample(ctx); + p.unsignedNumeralExample(ctx); + p.rationalExtractionExample(ctx); p.isGroundExample(ctx); p.astDepthExample(ctx); p.arrayArityExample(ctx); diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index acfebe5a9..58491eb7a 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -244,6 +244,15 @@ public class Expr extends AST return Native.isNumeralAst(getContext().nCtx(), getNativeObject()); } + /** + * Return the numeral value as a double. + * The expression must be a numeral or an algebraic number. + **/ + public double getNumeralDouble() + { + return Native.getNumeralDouble(getContext().nCtx(), getNativeObject()); + } + /** * Indicates whether the term is well-sorted. * diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index d3a5b456f..3dda55714 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -52,6 +52,33 @@ public class IntNum extends IntExpr return res.value; } + /** + * Retrieve the unsigned 32-bit value. + * The returned Java {@code int} holds the raw bit pattern; + * use {@code Integer.toUnsignedLong(v)} for unsigned interpretation. + **/ + public int getUint() + { + Native.IntPtr res = new Native.IntPtr(); + if (!Native.getNumeralUint(getContext().nCtx(), getNativeObject(), res)) + throw new Z3Exception("Numeral is not a uint"); + return res.value; + } + + /** + * Retrieve the unsigned 64-bit value. + * The returned Java {@code long} holds the raw bit pattern; + * use {@code Long.toUnsignedString(v)} or {@link #getBigInteger()} + * for values exceeding {@code Long.MAX_VALUE}. + **/ + public long getUint64() + { + Native.LongPtr res = new Native.LongPtr(); + if (!Native.getNumeralUint64(getContext().nCtx(), getNativeObject(), res)) + throw new Z3Exception("Numeral is not a uint64"); + return res.value; + } + /** * Retrieve the BigInteger value. **/ diff --git a/src/api/java/RatNum.java b/src/api/java/RatNum.java index 2bf1b28dd..cde3a8bd8 100644 --- a/src/api/java/RatNum.java +++ b/src/api/java/RatNum.java @@ -60,6 +60,34 @@ public class RatNum extends RealExpr return new BigInteger(n.toString()); } + /** + * Retrieve the numerator and denominator as 64-bit integers. + * Throws if the value does not fit in 64-bit integers. + * @return a two-element array [numerator, denominator] + **/ + public long[] getSmall() + { + Native.LongPtr num = new Native.LongPtr(); + Native.LongPtr den = new Native.LongPtr(); + if (!Native.getNumeralSmall(getContext().nCtx(), getNativeObject(), num, den)) + throw new Z3Exception("Numeral does not fit in int64"); + return new long[] { num.value, den.value }; + } + + /** + * Retrieve the numerator and denominator as 64-bit integers. + * Returns null if the value does not fit in 64-bit integers. + * @return a two-element array [numerator, denominator], or null + **/ + public long[] getRationalInt64() + { + Native.LongPtr num = new Native.LongPtr(); + Native.LongPtr den = new Native.LongPtr(); + if (!Native.getNumeralRationalInt64(getContext().nCtx(), getNativeObject(), num, den)) + return null; + return new long[] { num.value, den.value }; + } + /** * Returns a string representation in decimal notation. * Remarks: The result