Inheritance diagram for RCFNum:

Public Member Functions
	RCFNum (Context ctx, String value)

	RCFNum (Context ctx, int value)

RCFNum	add (RCFNum other)

RCFNum	sub (RCFNum other)

RCFNum	mul (RCFNum other)

RCFNum	div (RCFNum other)

RCFNum	neg ()

RCFNum	inv ()

RCFNum	power (int k)

boolean	lt (RCFNum other)

boolean	gt (RCFNum other)

boolean	le (RCFNum other)

boolean	ge (RCFNum other)

boolean	eq (RCFNum other)

boolean	neq (RCFNum other)

boolean	isRational ()

boolean	isAlgebraic ()

boolean	isInfinitesimal ()

boolean	isTranscendental ()

String	toString (boolean compact)

String	toString ()

String	toDecimal (int precision)

Static Public Member Functions
static RCFNum	mkPi (Context ctx)

static RCFNum	mkE (Context ctx)

static RCFNum	mkInfinitesimal (Context ctx)

static RCFNum[]	mkRoots (Context ctx, RCFNum[] coefficients)

Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)

static int	arrayLength (Z3Object[] a)

Detailed Description

Real Closed Field (RCF) numerals.

RCF numerals can represent:

Rational numbers
Algebraic numbers (roots of polynomials)
Transcendental extensions (e.g., pi, e)
Infinitesimal extensions

Definition at line 31 of file RCFNum.java.

Constructor & Destructor Documentation

◆ RCFNum() [1/2]

RCFNum	(	Context	ctx,
		String	value
	)

inline

Create an RCF numeral from a rational string.

Parameters

ctx	Z3 context
value	String representation of a rational number (e.g., "3/2", "0.5", "42")

Exceptions

Z3Exception on error

Definition at line 39 of file RCFNum.java.

                                             {
        super(ctx, Native.rcfMkRational(ctx.nCtx(), value));
    }

◆ RCFNum() [2/2]

RCFNum	(	Context	ctx,
		int	value
	)

inline

Create an RCF numeral from a small integer.

Parameters

ctx	Z3 context
value	Integer value

Exceptions

Z3Exception on error

Definition at line 49 of file RCFNum.java.

                                          {
        super(ctx, Native.rcfMkSmallInt(ctx.nCtx(), value));
    }

Member Function Documentation

◆ add()

RCFNum add ( RCFNum other )

inline

Add two RCF numerals.

Parameters

other The RCF numeral to add

Returns: this + other

Exceptions

Z3Exception on error

Definition at line 129 of file RCFNum.java.

                                    {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfAdd(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }

Referenced by Solver.__iadd__().

◆ div()

RCFNum div ( RCFNum other )

inline

Divide two RCF numerals.

Parameters

other The RCF numeral to divide by

Returns: this / other

Exceptions

Z3Exception on error

Definition at line 168 of file RCFNum.java.

                                    {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfDiv(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }

◆ eq()

boolean eq ( RCFNum other )

inline

Check if this RCF numeral is equal to another.

Parameters

other The RCF numeral to compare with

Returns: true if this == other

Exceptions

Z3Exception on error

Definition at line 260 of file RCFNum.java.

                                    {
        checkContext(other);
        return Native.rcfEq(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }

Referenced by AstRef.__eq__(), and SortRef.cast().

◆ ge()

boolean ge ( RCFNum other )

inline

Check if this RCF numeral is greater than or equal to another.

Parameters

other The RCF numeral to compare with

Returns: true if this >= other

Exceptions

Z3Exception on error

Definition at line 248 of file RCFNum.java.

                                    {
        checkContext(other);
        return Native.rcfGe(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }

◆ gt()

boolean gt ( RCFNum other )

inline

Check if this RCF numeral is greater than another.

Parameters

other The RCF numeral to compare with

Returns: true if this > other

Exceptions

Z3Exception on error

Definition at line 224 of file RCFNum.java.

                                    {
        checkContext(other);
        return Native.rcfGt(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }

◆ inv()

RCFNum inv ( )

inline

Compute the multiplicative inverse.

Returns: 1/this

Exceptions

Z3Exception on error

Definition at line 190 of file RCFNum.java.

                        {
        return new RCFNum(getContext(), Native.rcfInv(getContext().nCtx(), 
                                                       getNativeObject()));
    }

◆ isAlgebraic()

boolean isAlgebraic ( )

inline

Check if this RCF numeral is an algebraic number.

Returns: true if this is algebraic

Exceptions

Z3Exception on error

Definition at line 292 of file RCFNum.java.

                                 {
        return Native.rcfIsAlgebraic(getContext().nCtx(), getNativeObject());
    }

◆ isInfinitesimal()

boolean isInfinitesimal ( )

inline

Check if this RCF numeral is an infinitesimal.

Returns: true if this is infinitesimal

Exceptions

Z3Exception on error

Definition at line 301 of file RCFNum.java.

                                     {
        return Native.rcfIsInfinitesimal(getContext().nCtx(), getNativeObject());
    }

◆ isRational()

boolean isRational ( )

inline

Check if this RCF numeral is a rational number.

Returns: true if this is rational

Exceptions

Z3Exception on error

Definition at line 283 of file RCFNum.java.

                                {
        return Native.rcfIsRational(getContext().nCtx(), getNativeObject());
    }

◆ isTranscendental()

boolean isTranscendental ( )

inline

Check if this RCF numeral is a transcendental number.

Returns: true if this is transcendental

Exceptions

Z3Exception on error

Definition at line 310 of file RCFNum.java.

                                      {
        return Native.rcfIsTranscendental(getContext().nCtx(), getNativeObject());
    }

◆ le()

boolean le ( RCFNum other )

inline

Check if this RCF numeral is less than or equal to another.

Parameters

other The RCF numeral to compare with

Returns: true if this <= other

Exceptions

Z3Exception on error

Definition at line 236 of file RCFNum.java.

                                    {
        checkContext(other);
        return Native.rcfLe(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }

◆ lt()

boolean lt ( RCFNum other )

inline

Check if this RCF numeral is less than another.

Parameters

other The RCF numeral to compare with

Returns: true if this < other

Exceptions

Z3Exception on error

Definition at line 212 of file RCFNum.java.

                                    {
        checkContext(other);
        return Native.rcfLt(getContext().nCtx(), getNativeObject(), 
                           other.getNativeObject());
    }

◆ mkE()

static RCFNum mkE ( Context ctx )

inlinestatic

Create an RCF numeral representing e (Euler's constant).

Parameters

ctx	Z3 context

Returns: RCF numeral for e

Exceptions

Z3Exception on error

Definition at line 76 of file RCFNum.java.

                                          {
        return new RCFNum(ctx, Native.rcfMkE(ctx.nCtx()));
    }

◆ mkInfinitesimal()

static RCFNum mkInfinitesimal ( Context ctx )

inlinestatic

Create an RCF numeral representing an infinitesimal.

Parameters

ctx	Z3 context

Returns: RCF numeral for an infinitesimal

Exceptions

Z3Exception on error

Definition at line 86 of file RCFNum.java.

                                                      {
        return new RCFNum(ctx, Native.rcfMkInfinitesimal(ctx.nCtx()));
    }

◆ mkPi()

static RCFNum mkPi ( Context ctx )

inlinestatic

Create an RCF numeral representing pi.

Parameters

ctx	Z3 context

Returns: RCF numeral for pi

Exceptions

Z3Exception on error

Definition at line 66 of file RCFNum.java.

                                           {
        return new RCFNum(ctx, Native.rcfMkPi(ctx.nCtx()));
    }

◆ mkRoots()

static RCFNum[] mkRoots	(	Context	ctx,
		RCFNum[]	coefficients
	)

inlinestatic

Find roots of a polynomial.

The polynomial is a[n-1]*x^(n-1) + ... + a[1]*x + a[0].

Parameters

ctx	Z3 context
coefficients	Polynomial coefficients (constant term first)

Returns: Array of RCF numerals representing the roots

Exceptions

Z3Exception on error

Definition at line 100 of file RCFNum.java.

                                                                       {
        if (coefficients == null || coefficients.length == 0) {
            throw new Z3Exception("Polynomial coefficients cannot be empty");
        }
        
        int n = coefficients.length;
        long[] a = new long[n];
        long[] roots = new long[n];
        
        for (int i = 0; i < n; i++) {
            a[i] = coefficients[i].getNativeObject();
        }
        
        int numRoots = Native.rcfMkRoots(ctx.nCtx(), n, a, roots);
        
        RCFNum[] result = new RCFNum[numRoots];
        for (int i = 0; i < numRoots; i++) {
            result[i] = new RCFNum(ctx, roots[i]);
        }
        
        return result;
    }

◆ mul()

RCFNum mul ( RCFNum other )

inline

Multiply two RCF numerals.

Parameters

other The RCF numeral to multiply

Returns: this * other

Exceptions

Z3Exception on error

Definition at line 155 of file RCFNum.java.

                                    {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfMul(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }

◆ neg()

RCFNum neg ( )

inline

Negate this RCF numeral.

Returns: -this

Exceptions

Z3Exception on error

Definition at line 180 of file RCFNum.java.

                        {
        return new RCFNum(getContext(), Native.rcfNeg(getContext().nCtx(), 
                                                       getNativeObject()));
    }

◆ neq()

boolean neq ( RCFNum other )

inline

Check if this RCF numeral is not equal to another.

Parameters

other The RCF numeral to compare with

Returns: true if this != other

Exceptions

Z3Exception on error

Definition at line 272 of file RCFNum.java.

                                     {
        checkContext(other);
        return Native.rcfNeq(getContext().nCtx(), getNativeObject(), 
                            other.getNativeObject());
    }

◆ power()

RCFNum power ( int k )

inline

Raise this RCF numeral to a power.

Parameters

k	The exponent

Returns: this^k

Exceptions

Z3Exception on error

Definition at line 201 of file RCFNum.java.

                               {
        return new RCFNum(getContext(), Native.rcfPower(getContext().nCtx(), 
                                                         getNativeObject(), k));
    }

◆ sub()

RCFNum sub ( RCFNum other )

inline

Subtract two RCF numerals.

Parameters

other The RCF numeral to subtract

Returns: this - other

Exceptions

Z3Exception on error

Definition at line 142 of file RCFNum.java.

                                    {
        checkContext(other);
        return new RCFNum(getContext(), Native.rcfSub(getContext().nCtx(), 
                                                       getNativeObject(), 
                                                       other.getNativeObject()));
    }

◆ toDecimal()

String toDecimal ( int precision )

inline

Convert this RCF numeral to a decimal string.

Parameters

precision Number of decimal places

Returns: Decimal string representation

Exceptions

Z3Exception on error

Definition at line 341 of file RCFNum.java.

                                           {
        return Native.rcfNumToDecimalString(getContext().nCtx(), 
                                            getNativeObject(), precision);
    }

◆ toString() [1/2]

String toString ( )

inline

Convert this RCF numeral to a string (non-compact).

Returns: String representation

Exceptions

Z3Exception on error

Definition at line 331 of file RCFNum.java.

                             {
        return toString(false);
    }

Referenced by RCFNum.toString().

◆ toString() [2/2]

String toString ( boolean compact )

inline

Convert this RCF numeral to a string.

Parameters

compact If true, use compact representation

Returns: String representation

Exceptions

Z3Exception on error

Definition at line 320 of file RCFNum.java.

                                            {
        return Native.rcfNumToString(getContext().nCtx(), getNativeObject(), 
                                     compact, false);
    }

Public Member Functions

Static Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ RCFNum() [1/2]

◆ RCFNum() [2/2]

Member Function Documentation

◆ add()

◆ div()

◆ eq()

◆ ge()

◆ gt()

◆ inv()

◆ isAlgebraic()

◆ isInfinitesimal()

◆ isRational()

◆ isTranscendental()

◆ le()

◆ lt()

◆ mkE()

◆ mkInfinitesimal()

◆ mkPi()

◆ mkRoots()

◆ mul()

◆ neg()

◆ neq()

◆ power()

◆ sub()

◆ toDecimal()

◆ toString() [1/2]

◆ toString() [2/2]