RCFNum Class Reference

Real Closed Field (RCF) numerals. More...

Inheritance diagram for RCFNum:

Public Member Functions
	RCFNum (Context ctx, string value)
	Create an RCF numeral from a rational string.
	RCFNum (Context ctx, int value)
	Create an RCF numeral from a small integer.
RCFNum	Add (RCFNum other)
	Add two RCF numerals.
RCFNum	Sub (RCFNum other)
	Subtract two RCF numerals.
RCFNum	Mul (RCFNum other)
	Multiply two RCF numerals.
RCFNum	Div (RCFNum other)
	Divide two RCF numerals.
RCFNum	Neg ()
	Negate this RCF numeral.
RCFNum	Inv ()
	Compute the multiplicative inverse.
RCFNum	Power (uint k)
	Raise this RCF numeral to a power.
bool	Lt (RCFNum other)
	Check if this RCF numeral is less than another.
bool	Gt (RCFNum other)
	Check if this RCF numeral is greater than another.
bool	Le (RCFNum other)
	Check if this RCF numeral is less than or equal to another.
bool	Ge (RCFNum other)
	Check if this RCF numeral is greater than or equal to another.
bool	Eq (RCFNum other)
	Check if this RCF numeral is equal to another.
bool	Neq (RCFNum other)
	Check if this RCF numeral is not equal to another.
bool	IsRational ()
	Check if this RCF numeral is a rational number.
bool	IsAlgebraic ()
	Check if this RCF numeral is an algebraic number.
bool	IsInfinitesimal ()
	Check if this RCF numeral is an infinitesimal.
bool	IsTranscendental ()
	Check if this RCF numeral is a transcendental number.
string	ToString (bool compact)
	Convert this RCF numeral to a string.
override string	ToString ()
	Convert this RCF numeral to a string (non-compact).
string	ToDecimal (uint precision)
	Convert this RCF numeral to a decimal string.
override bool	Equals (object obj)
	Override Equals for proper equality semantics.
override int	GetHashCode ()
	Override GetHashCode for proper equality semantics.
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

Static Public Member Functions
static RCFNum	MkPi (Context ctx)
	Create an RCF numeral representing pi.
static RCFNum	MkE (Context ctx)
	Create an RCF numeral representing e (Euler's constant).
static RCFNum	MkInfinitesimal (Context ctx)
	Create an RCF numeral representing an infinitesimal.
static RCFNum[]	MkRoots (Context ctx, RCFNum[] coefficients)
	Find roots of a polynomial.
static RCFNum	operator+ (RCFNum a, RCFNum b)
	Operator overload for addition.
static RCFNum	operator- (RCFNum a, RCFNum b)
	Operator overload for subtraction.
static RCFNum	operator* (RCFNum a, RCFNum b)
	Operator overload for multiplication.
static RCFNum	operator/ (RCFNum a, RCFNum b)
	Operator overload for division.
static RCFNum	operator- (RCFNum a)
	Operator overload for negation.
static bool	operator< (RCFNum a, RCFNum b)
	Operator overload for less than.
static bool	operator> (RCFNum a, RCFNum b)
	Operator overload for greater than.
static bool	operator<= (RCFNum a, RCFNum b)
	Operator overload for less than or equal.
static bool	operator>= (RCFNum a, RCFNum b)
	Operator overload for greater than or equal.
static bool	operator== (RCFNum a, RCFNum b)
	Operator overload for equality.
static bool	operator!= (RCFNum a, RCFNum b)
	Operator overload for inequality.

Additional Inherited Members
Properties inherited from Z3Object
Context	Context [get]
	Access Context object.

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 33 of file RCFNum.cs.

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")

Definition at line 40 of file RCFNum.cs.

            : base(ctx, Native.Z3_rcf_mk_rational(ctx.nCtx, value))
        {
            Debug.Assert(ctx != null);
        }

RCFNum() [2/2]

RCFNum ( Context  ctx, int  value  )

inline

Create an RCF numeral from a small integer.

Parameters

ctx	Z3 context
value	Integer value

Definition at line 51 of file RCFNum.cs.

            : base(ctx, Native.Z3_rcf_mk_small_int(ctx.nCtx, value))
        {
            Debug.Assert(ctx != null);
        }

Member Function Documentation

Add()

RCFNum Add ( RCFNum  other )

inline

Add two RCF numerals.

Parameters

other

The RCF numeral to add

Returns

this + other

Definition at line 136 of file RCFNum.cs.

        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_add(Context.nCtx, NativeObject, other.NativeObject));
        }

Referenced by RCFNum.operator+().

Div()

RCFNum Div ( RCFNum  other )

inline

Divide two RCF numerals.

Parameters

other

The RCF numeral to divide by

Returns

this / other

Definition at line 169 of file RCFNum.cs.

        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_div(Context.nCtx, NativeObject, other.NativeObject));
        }

Referenced by RCFNum.operator/().

Eq()

bool 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

Definition at line 292 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_eq(Context.nCtx, NativeObject, other.NativeObject);
        }

Referenced by RCFNum.operator==().

Equals()

override bool Equals ( object  obj )

inline

Override Equals for proper equality semantics.

Definition at line 427 of file RCFNum.cs.

        {
            if (obj is RCFNum other)
            {
                return this == other;
            }
            return false;
        }

Ge()

bool 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

Definition at line 281 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_ge(Context.nCtx, NativeObject, other.NativeObject);
        }

Referenced by RCFNum.operator>=().

GetHashCode()

override int GetHashCode ( )

inline

Override GetHashCode for proper equality semantics.

Definition at line 439 of file RCFNum.cs.

        {
            return NativeObject.GetHashCode();
        }

Gt()

bool 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

Definition at line 259 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_gt(Context.nCtx, NativeObject, other.NativeObject);
        }

Referenced by RCFNum.operator>().

Inv()

RCFNum Inv ( )

inline

Compute the multiplicative inverse.

Returns

1/this

Definition at line 188 of file RCFNum.cs.

        {
            return new RCFNum(Context, Native.Z3_rcf_inv(Context.nCtx, NativeObject));
        }

IsAlgebraic()

bool IsAlgebraic ( )

inline

Check if this RCF numeral is an algebraic number.

Returns

true if this is algebraic

Definition at line 372 of file RCFNum.cs.

        {
            return 0 != Native.Z3_rcf_is_algebraic(Context.nCtx, NativeObject);
        }

IsInfinitesimal()

bool IsInfinitesimal ( )

inline

Check if this RCF numeral is an infinitesimal.

Returns

true if this is infinitesimal

Definition at line 381 of file RCFNum.cs.

        {
            return 0 != Native.Z3_rcf_is_infinitesimal(Context.nCtx, NativeObject);
        }

IsRational()

bool IsRational ( )

inline

Check if this RCF numeral is a rational number.

Returns

true if this is rational

Definition at line 363 of file RCFNum.cs.

        {
            return 0 != Native.Z3_rcf_is_rational(Context.nCtx, NativeObject);
        }

IsTranscendental()

bool IsTranscendental ( )

inline

Check if this RCF numeral is a transcendental number.

Returns

true if this is transcendental

Definition at line 390 of file RCFNum.cs.

        {
            return 0 != Native.Z3_rcf_is_transcendental(Context.nCtx, NativeObject);
        }

Le()

bool 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

Definition at line 270 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_le(Context.nCtx, NativeObject, other.NativeObject);
        }

Referenced by RCFNum.operator<=().

Lt()

bool 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

Definition at line 248 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_lt(Context.nCtx, NativeObject, other.NativeObject);
        }

Referenced by RCFNum.operator<().

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

Definition at line 81 of file RCFNum.cs.

        {
            return new RCFNum(ctx, Native.Z3_rcf_mk_e(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

Definition at line 91 of file RCFNum.cs.

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

MkPi()

static RCFNum MkPi ( Context  ctx )

inlinestatic

Create an RCF numeral representing pi.

Parameters

ctx	Z3 context

Returns

RCF numeral for pi

Definition at line 71 of file RCFNum.cs.

        {
            return new RCFNum(ctx, Native.Z3_rcf_mk_pi(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

Definition at line 104 of file RCFNum.cs.

        {
            if (coefficients == null || coefficients.Length == 0)
            {
                throw new Z3Exception("Polynomial coefficients cannot be empty");
            }
 
            uint n = (uint)coefficients.Length;
            IntPtr[] a = new IntPtr[n];
            IntPtr[] roots = new IntPtr[n];
 
            for (uint i = 0; i < n; i++)
            {
                a[i] = coefficients[i].NativeObject;
            }
 
            uint numRoots = Native.Z3_rcf_mk_roots(ctx.nCtx, n, a, roots);
 
            RCFNum[] result = new RCFNum[numRoots];
            for (uint 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

Definition at line 158 of file RCFNum.cs.

        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_mul(Context.nCtx, NativeObject, other.NativeObject));
        }

Referenced by RCFNum.operator*().

Neg()

RCFNum Neg ( )

inline

Negate this RCF numeral.

Returns

-this

Definition at line 179 of file RCFNum.cs.

        {
            return new RCFNum(Context, Native.Z3_rcf_neg(Context.nCtx, NativeObject));
        }

Referenced by RCFNum.operator-().

Neq()

bool 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

Definition at line 303 of file RCFNum.cs.

        {
            CheckContext(other);
            return 0 != Native.Z3_rcf_neq(Context.nCtx, NativeObject, other.NativeObject);
        }

operator!=()

static bool operator!= ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for inequality.

Definition at line 354 of file RCFNum.cs.

        {
            return !(a == b);
        }

operator*()

static RCFNum operator* ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for multiplication.

Definition at line 222 of file RCFNum.cs.

        {
            return a.Mul(b);
        }

operator+()

static RCFNum operator+ ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for addition.

Definition at line 206 of file RCFNum.cs.

        {
            return a.Add(b);
        }

operator-() [1/2]

static RCFNum operator- ( RCFNum  a )

inlinestatic

Operator overload for negation.

Definition at line 238 of file RCFNum.cs.

        {
            return a.Neg();
        }

operator-() [2/2]

static RCFNum operator- ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for subtraction.

Definition at line 214 of file RCFNum.cs.

        {
            return a.Sub(b);
        }

operator/()

static RCFNum operator/ ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for division.

Definition at line 230 of file RCFNum.cs.

        {
            return a.Div(b);
        }

operator<()

static bool operator< ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for less than.

Definition at line 312 of file RCFNum.cs.

        {
            return a.Lt(b);
        }

operator<=()

static bool operator<= ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for less than or equal.

Definition at line 328 of file RCFNum.cs.

        {
            return a.Le(b);
        }

operator==()

static bool operator== ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for equality.

Definition at line 344 of file RCFNum.cs.

        {
            if (ReferenceEquals(a, b)) return true;
            if (ReferenceEquals(a, null) || ReferenceEquals(b, null)) return false;
            return a.Eq(b);
        }

operator>()

static bool operator> ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for greater than.

Definition at line 320 of file RCFNum.cs.

        {
            return a.Gt(b);
        }

operator>=()

static bool operator>= ( RCFNum  a, RCFNum  b  )

inlinestatic

Operator overload for greater than or equal.

Definition at line 336 of file RCFNum.cs.

        {
            return a.Ge(b);
        }

Power()

RCFNum Power ( uint  k )

inline

Raise this RCF numeral to a power.

Parameters

k	The exponent

Returns

this^k

Definition at line 198 of file RCFNum.cs.

        {
            return new RCFNum(Context, Native.Z3_rcf_power(Context.nCtx, NativeObject, k));
        }

Sub()

RCFNum Sub ( RCFNum  other )

inline

Subtract two RCF numerals.

Parameters

other

The RCF numeral to subtract

Returns

this - other

Definition at line 147 of file RCFNum.cs.

        {
            CheckContext(other);
            return new RCFNum(Context, Native.Z3_rcf_sub(Context.nCtx, NativeObject, other.NativeObject));
        }

Referenced by RCFNum.operator-().

ToDecimal()

string ToDecimal ( uint  precision )

inline

Convert this RCF numeral to a decimal string.

Parameters

precision

Number of decimal places

Returns

Decimal string representation

Definition at line 419 of file RCFNum.cs.

        {
            return Native.Z3_rcf_num_to_decimal_string(Context.nCtx, NativeObject, precision);
        }

ToString() [1/2]

override string ToString ( )

inline

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

Returns

String representation

Definition at line 409 of file RCFNum.cs.

        {
            return ToString(false);
        }

Referenced by RCFNum.ToString().

ToString() [2/2]

string ToString ( bool  compact )

inline

Convert this RCF numeral to a string.

Parameters

compact

If true, use compact representation

Returns

String representation

Definition at line 400 of file RCFNum.cs.

        {
            return Native.Z3_rcf_num_to_string(Context.nCtx, NativeObject, compact ? (byte)1 : (byte)0, 0);
        }