Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Properties
RatNum Class Reference

Rational Numerals More...

+ Inheritance diagram for RatNum:

Public Member Functions

string ToDecimalString (uint precision)
 Returns a string representation in decimal notation.
 
override string ToString ()
 Returns a string representation of the numeral.
 

Properties

IntNum Numerator [get]
 The numerator of a rational numeral.
 
IntNum Denominator [get]
 The denominator of a rational numeral.
 
BigInteger BigIntNumerator [get]
 Converts the numerator of the rational to a BigInteger
 
BigInteger BigIntDenominator [get]
 Converts the denominator of the rational to a BigInteger
 

Additional Inherited Members

- Static Public Member Functions inherited from AST
static bool operator== (AST a, AST b)
 Comparison operator.
 
static bool operator!= (AST a, AST b)
 Comparison operator.
 
- Protected Member Functions inherited from RealExpr
 RealExpr (Context ctx)
 Constructor for RealExpr
 

Detailed Description

Rational Numerals

Definition at line 126 of file Numeral.cs.

Member Function Documentation

string ToDecimalString ( uint  precision)
inline

Returns a string representation in decimal notation.

The result has at most precision decimal places.

Definition at line 180 of file Numeral.cs.

{
return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
}
override string ToString ( )
inline

Returns a string representation of the numeral.

Definition at line 188 of file Numeral.cs.

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

Property Documentation

BigInteger BigIntDenominator
get

Converts the denominator of the rational to a BigInteger

Definition at line 167 of file Numeral.cs.

BigInteger BigIntNumerator
get

Converts the numerator of the rational to a BigInteger

Definition at line 155 of file Numeral.cs.

IntNum Denominator
get

The denominator of a rational numeral.

Definition at line 143 of file Numeral.cs.

IntNum Numerator
get

The numerator of a rational numeral.

Definition at line 132 of file Numeral.cs.