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 5061 of file z3++.h.

Constructor & Destructor Documentation

rcf_num() [1/4]

rcf_num ( context &  c, Z3_rcf_num  n  )

inline

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

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

rcf_num() [2/4]

rcf_num ( context &  c, int  val  )

inline

Definition at line 5074 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 5078 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 5082 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 5098 of file z3++.h.

                   {
            Z3_rcf_del(m_ctx, m_num);
        }

Member Function Documentation

ctx()

Z3_context ctx ( ) const

inline

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

{ return m_ctx; }

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), AstMap::__contains__(), AstRef::__copy__(), Goal::__copy__(), AstVector::__copy__(), FuncInterp::__copy__(), ModelRef::__copy__(), AstRef::__deepcopy__(), Datatype::__deepcopy__(), ParamsRef::__deepcopy__(), ParamDescrsRef::__deepcopy__(), Goal::__deepcopy__(), AstVector::__deepcopy__(), AstMap::__deepcopy__(), FuncEntry::__deepcopy__(), FuncInterp::__deepcopy__(), ModelRef::__deepcopy__(), Statistics::__deepcopy__(), Context::__del__(), AstRef::__del__(), ScopedConstructor::__del__(), ScopedConstructorList::__del__(), ParamsRef::__del__(), ParamDescrsRef::__del__(), Goal::__del__(), AstVector::__del__(), AstMap::__del__(), FuncEntry::__del__(), FuncInterp::__del__(), ModelRef::__del__(), Statistics::__del__(), Solver::__del__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), AstVector::__getitem__(), ModelRef::__getitem__(), Statistics::__getitem__(), AstMap::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), AstVector::__len__(), AstMap::__len__(), ModelRef::__len__(), Statistics::__len__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), BoolRef::__mul__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), ParamsRef::__repr__(), ParamDescrsRef::__repr__(), AstMap::__repr__(), Statistics::__repr__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), AstVector::__setitem__(), AstMap::__setitem__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), ExprRef::arg(), FuncEntry::arg_value(), FuncInterp::arity(), Goal::as_expr(), Solver::assert_and_track(), Goal::assert_exprs(), Solver::assert_exprs(), QuantifierRef::body(), FiniteSetSortRef::cast(), Solver::check(), Goal::convert_model(), AstRef::ctx_ref(), ExprRef::decl(), ModelRef::decls(), ArrayRef::default(), RatNumRef::denominator(), Goal::depth(), Goal::dimacs(), FuncDeclRef::domain(), ArraySortRef::domain_n(), FuncInterp::else_value(), FuncInterp::entry(), AstMap::erase(), ModelRef::eval(), Goal::get(), ParamDescrsRef::get_documentation(), ModelRef::get_interp(), Statistics::get_key_value(), ParamDescrsRef::get_kind(), ParamDescrsRef::get_name(), ModelRef::get_sort(), ModelRef::get_universe(), Goal::inconsistent(), AstMap::keys(), Statistics::keys(), Solver::model(), SortRef::name(), QuantifierRef::no_pattern(), FuncEntry::num_args(), FuncInterp::num_entries(), Solver::num_scopes(), ModelRef::num_sorts(), FuncDeclRef::params(), QuantifierRef::pattern(), AlgebraicNumRef::poly(), Solver::pop(), Goal::prec(), ModelRef::project(), ModelRef::project_with_witness(), Solver::push(), AstVector::push(), QuantifierRef::qid(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Context::ref(), AstMap::reset(), Solver::reset(), AstVector::resize(), Solver::set(), ParamsRef::set(), Goal::sexpr(), AstVector::sexpr(), ModelRef::sexpr(), ParamDescrsRef::size(), Goal::size(), QuantifierRef::skolem_id(), AstVector::translate(), AstRef::translate(), Goal::translate(), ModelRef::translate(), ExprRef::update(), DatatypeRef::update_field(), ParamsRef::validate(), FuncEntry::value(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

inv()

rcf_num inv ( ) const

inline

Return the multiplicative inverse (1/this).

Definition at line 5160 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 5201 of file z3++.h.

                                  {
            return Z3_rcf_is_algebraic(m_ctx, m_num);
        }

is_infinitesimal()

bool is_infinitesimal ( ) const

inline

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

                                      {
            return Z3_rcf_is_infinitesimal(m_ctx, m_num);
        }

is_rational()

bool is_rational ( ) const

inline

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

                                 {
            return Z3_rcf_is_rational(m_ctx, m_num);
        }

is_transcendental()

bool is_transcendental ( ) const

inline

Definition at line 5209 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 5102 of file z3++.h.

{ return 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_neq(m_ctx, m_num, other.m_num);
        }

operator*()

rcf_num operator* ( rcf_num const &  other ) const

inline

Definition at line 5132 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 5120 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 5144 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 5126 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 5138 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 5166 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 5176 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 5088 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 5186 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 5171 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 5181 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 5152 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 5115 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 5108 of file z3++.h.

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

Friends And Related Symbol Documentation

operator<<

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

friend

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

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