rcf_num Class Reference

Wrapper for Z3 Real Closed Field (RCF) numerals. More...

#include <z3++.h>

Public Member Functions
	rcf_num (context &c, Z3_rcf_num n)
	rcf_num (context &c, int val)
	rcf_num (context &c, char const *val)
	rcf_num (rcf_num const &other)
rcf_num &	operator= (rcf_num const &other)
	~rcf_num ()
	operator Z3_rcf_num () const
Z3_context	ctx () const
std::string	to_string (bool compact=false) const
	Return string representation of the RCF numeral.
std::string	to_decimal (unsigned precision=10) const
	Return decimal string representation with given precision.
rcf_num	operator+ (rcf_num const &other) const
rcf_num	operator- (rcf_num const &other) const
rcf_num	operator* (rcf_num const &other) const
rcf_num	operator/ (rcf_num const &other) const
rcf_num	operator- () const
rcf_num	power (unsigned k) const
	Return the power of this number raised to k.
rcf_num	inv () const
	Return the multiplicative inverse (1/this).
bool	operator< (rcf_num const &other) const
bool	operator> (rcf_num const &other) const
bool	operator<= (rcf_num const &other) const
bool	operator>= (rcf_num const &other) const
bool	operator== (rcf_num const &other) const
bool	operator!= (rcf_num const &other) const
bool	is_rational () const
bool	is_algebraic () const
bool	is_infinitesimal () const
bool	is_transcendental () const

Friends
std::ostream &	operator<< (std::ostream &out, rcf_num const &n)

Detailed Description

Wrapper for Z3 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 5076 of file z3++.h.

Constructor & Destructor Documentation

rcf_num() [1/4]

rcf_num ( context & c, Z3_rcf_num n )

inline

Definition at line 5087 of file z3++.h.

: m_ctx(c), m_num(n) {}

Referenced by inv(), operator!=(), operator*(), operator+(), operator-(), operator-(), operator/(), operator<(), operator<<, operator<=(), operator=(), operator==(), operator>(), operator>=(), power(), z3::rcf_e(), z3::rcf_infinitesimal(), rcf_num(), z3::rcf_pi(), and z3::rcf_roots().

rcf_num() [2/4]

rcf_num ( context & c, int val )

inline

Definition at line 5089 of file z3++.h.

                                    : m_ctx(c) {
            m_num = Z3_rcf_mk_small_int(c, val);
        }

rcf_num() [3/4]

rcf_num ( context & c, char const * val )

inline

Definition at line 5093 of file z3++.h.

                                            : m_ctx(c) {
            m_num = Z3_rcf_mk_rational(c, val);
        }

rcf_num() [4/4]

rcf_num ( rcf_num const & other )

inline

Definition at line 5097 of file z3++.h.

                                     : m_ctx(other.m_ctx) {
            // Create a copy by converting to string and back
            std::string str = Z3_rcf_num_to_string(m_ctx, other.m_num, false, false);
            m_num = Z3_rcf_mk_rational(m_ctx, str.c_str());
        }

~rcf_num()

~rcf_num ( )

inline

Definition at line 5113 of file z3++.h.

                   {
            Z3_rcf_del(m_ctx, m_num);
        }

Member Function Documentation

ctx()

Z3_context ctx ( ) const

inline

Definition at line 5118 of file z3++.h.

{ return m_ctx; }

inv()

rcf_num inv ( ) const

inline

Return the multiplicative inverse (1/this).

Definition at line 5175 of file z3++.h.

                            {
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_inv(m_ctx, m_num));
        }

is_algebraic()

bool is_algebraic ( ) const

inline

Definition at line 5216 of file z3++.h.

                                  {
            return Z3_rcf_is_algebraic(m_ctx, m_num);
        }

is_infinitesimal()

bool is_infinitesimal ( ) const

inline

Definition at line 5220 of file z3++.h.

                                      {
            return Z3_rcf_is_infinitesimal(m_ctx, m_num);
        }

is_rational()

bool is_rational ( ) const

inline

Definition at line 5212 of file z3++.h.

                                 {
            return Z3_rcf_is_rational(m_ctx, m_num);
        }

is_transcendental()

bool is_transcendental ( ) const

inline

Definition at line 5224 of file z3++.h.

                                       {
            return Z3_rcf_is_transcendental(m_ctx, m_num);
        }

operator Z3_rcf_num()

operator Z3_rcf_num ( ) const

inline

Definition at line 5117 of file z3++.h.

{ return m_num; }

operator!=()

bool operator!= ( rcf_num const & other ) const

inline

Definition at line 5206 of file z3++.h.

                                                  {
            check_context(other);
            return Z3_rcf_neq(m_ctx, m_num, other.m_num);
        }

operator*()

rcf_num operator* ( rcf_num const & other ) const

inline

Definition at line 5147 of file z3++.h.

                                                      {
            check_context(other);
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_mul(m_ctx, m_num, other.m_num));
        }

operator+()

rcf_num operator+ ( rcf_num const & other ) const

inline

Definition at line 5135 of file z3++.h.

                                                      {
            check_context(other);
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_add(m_ctx, m_num, other.m_num));
        }

operator-() [1/2]

rcf_num operator- ( ) const

inline

Definition at line 5159 of file z3++.h.

                                  {
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_neg(m_ctx, m_num));
        }

operator-() [2/2]

rcf_num operator- ( rcf_num const & other ) const

inline

Definition at line 5141 of file z3++.h.

                                                      {
            check_context(other);
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_sub(m_ctx, m_num, other.m_num));
        }

operator/()

rcf_num operator/ ( rcf_num const & other ) const

inline

Definition at line 5153 of file z3++.h.

                                                      {
            check_context(other);
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_div(m_ctx, m_num, other.m_num));
        }

operator<()

bool operator< ( rcf_num const & other ) const

inline

Definition at line 5181 of file z3++.h.

                                                   {
            check_context(other);
            return Z3_rcf_lt(m_ctx, m_num, other.m_num);
        }

operator<=()

bool operator<= ( rcf_num const & other ) const

inline

Definition at line 5191 of file z3++.h.

                                                  {
            check_context(other);
            return Z3_rcf_le(m_ctx, m_num, other.m_num);
        }

operator=()

rcf_num & operator= ( rcf_num const & other )

inline

Definition at line 5103 of file z3++.h.

                                               {
            if (this != &other) {
                Z3_rcf_del(m_ctx, m_num);
                m_ctx = other.m_ctx;
                std::string str = Z3_rcf_num_to_string(m_ctx, other.m_num, false, false);
                m_num = Z3_rcf_mk_rational(m_ctx, str.c_str());
            }
            return *this;
        }

operator==()

bool operator== ( rcf_num const & other ) const

inline

Definition at line 5201 of file z3++.h.

                                                  {
            check_context(other);
            return Z3_rcf_eq(m_ctx, m_num, other.m_num);
        }

operator>()

bool operator> ( rcf_num const & other ) const

inline

Definition at line 5186 of file z3++.h.

                                                   {
            check_context(other);
            return Z3_rcf_gt(m_ctx, m_num, other.m_num);
        }

operator>=()

bool operator>= ( rcf_num const & other ) const

inline

Definition at line 5196 of file z3++.h.

                                                  {
            check_context(other);
            return Z3_rcf_ge(m_ctx, m_num, other.m_num);
        }

power()

rcf_num power ( unsigned k ) const

inline

Return the power of this number raised to k.

Definition at line 5167 of file z3++.h.

                                        {
            return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)), 
                          Z3_rcf_power(m_ctx, m_num, k));
        }

to_decimal()

std::string to_decimal ( unsigned precision = 10 ) const

inline

Return decimal string representation with given precision.

Definition at line 5130 of file z3++.h.

                                                          {
            return std::string(Z3_rcf_num_to_decimal_string(m_ctx, m_num, precision));
        }

to_string()

std::string to_string ( bool compact = false ) const

inline

Return string representation of the RCF numeral.

Definition at line 5123 of file z3++.h.

                                                      {
            return std::string(Z3_rcf_num_to_string(m_ctx, m_num, compact, false));
        }

Referenced by operator<<.

Friends And Related Symbol Documentation

operator<<

std::ostream & operator<< ( std::ostream & out, rcf_num const & n )

friend

Definition at line 5228 of file z3++.h.

                                                                         {
            return out << n.to_string();
        }