Z3
Public Member Functions | Friends
rcf_num Class Reference
C++ API

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

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. More...
 
std::string to_decimal (unsigned precision=10) const
 Return decimal string representation with given precision. More...
 
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. More...
 
rcf_num inv () const
 Return the multiplicative inverse (1/this). More...
 
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:

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

Constructor & Destructor Documentation

rcf_num ( context &  c,
Z3_rcf_num  n 
)
inline

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

Referenced by rcf_num::inv(), rcf_num::operator*(), rcf_num::operator+(), rcf_num::operator-(), rcf_num::operator/(), and rcf_num::power().

4840 : m_ctx(c), m_num(n) {}
rcf_num ( context &  c,
int  val 
)
inline

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

4842  : m_ctx(c) {
4843  m_num = Z3_rcf_mk_small_int(c, val);
4844  }
Z3_rcf_mk_small_int
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val)
Return a RCF small integer.
rcf_num ( context &  c,
char const *  val 
)
inline

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

4846  : m_ctx(c) {
4847  m_num = Z3_rcf_mk_rational(c, val);
4848  }
Z3_rcf_mk_rational
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val)
Return a RCF rational using the given string.
rcf_num ( rcf_num const &  other)
inline

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

4850  : m_ctx(other.m_ctx) {
4851  // Create a copy by converting to string and back
4852  std::string str = Z3_rcf_num_to_string(m_ctx, other.m_num, false, false);
4853  m_num = Z3_rcf_mk_rational(m_ctx, str.c_str());
4854  }
Z3_rcf_num_to_string
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html)
Convert the RCF numeral into a string.
Z3_rcf_mk_rational
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val)
Return a RCF rational using the given string.
~rcf_num ( )
inline

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

4866  {
4867  Z3_rcf_del(m_ctx, m_num);
4868  }
Z3_rcf_del
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.

Member Function Documentation

Z3_context ctx ( ) const
inline

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

4871 { return m_ctx; }
rcf_num inv ( ) const
inline

Return the multiplicative inverse (1/this).

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

4928  {
4929  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4930  Z3_rcf_inv(m_ctx, m_num));
4931  }
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
Z3_rcf_inv
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a)
Return the value 1/a.
bool is_algebraic ( ) const
inline

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

4969  {
4970  return Z3_rcf_is_algebraic(m_ctx, m_num);
4971  }
Z3_rcf_is_algebraic
bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a)
Return true if a represents an algebraic number.
bool is_infinitesimal ( ) const
inline

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

4973  {
4974  return Z3_rcf_is_infinitesimal(m_ctx, m_num);
4975  }
Z3_rcf_is_infinitesimal
bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a)
Return true if a represents an infinitesimal.
bool is_rational ( ) const
inline

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

4965  {
4966  return Z3_rcf_is_rational(m_ctx, m_num);
4967  }
Z3_rcf_is_rational
bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a)
Return true if a represents a rational number.
bool is_transcendental ( ) const
inline

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

4977  {
4978  return Z3_rcf_is_transcendental(m_ctx, m_num);
4979  }
Z3_rcf_is_transcendental
bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a)
Return true if a represents a transcendental number.
operator Z3_rcf_num ( ) const
inline

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

4870 { return m_num; }
bool operator!= ( rcf_num const &  other) const
inline

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

4959  {
4960  check_context(other);
4961  return Z3_rcf_neq(m_ctx, m_num, other.m_num);
4962  }
Z3_rcf_neq
bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a != b.
rcf_num operator* ( rcf_num const &  other) const
inline

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

4900  {
4901  check_context(other);
4902  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4903  Z3_rcf_mul(m_ctx, m_num, other.m_num));
4904  }
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
Z3_rcf_mul
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a * b.
rcf_num operator+ ( rcf_num const &  other) const
inline

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

4888  {
4889  check_context(other);
4890  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4891  Z3_rcf_add(m_ctx, m_num, other.m_num));
4892  }
Z3_rcf_add
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a + b.
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
rcf_num operator- ( rcf_num const &  other) const
inline

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

4894  {
4895  check_context(other);
4896  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4897  Z3_rcf_sub(m_ctx, m_num, other.m_num));
4898  }
Z3_rcf_sub
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a - b.
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
rcf_num operator- ( ) const
inline

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

4912  {
4913  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4914  Z3_rcf_neg(m_ctx, m_num));
4915  }
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
Z3_rcf_neg
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a)
Return the value -a.
rcf_num operator/ ( rcf_num const &  other) const
inline

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

4906  {
4907  check_context(other);
4908  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4909  Z3_rcf_div(m_ctx, m_num, other.m_num));
4910  }
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
Z3_rcf_div
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a / b.
bool operator< ( rcf_num const &  other) const
inline

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

4934  {
4935  check_context(other);
4936  return Z3_rcf_lt(m_ctx, m_num, other.m_num);
4937  }
Z3_rcf_lt
bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a < b.
bool operator<= ( rcf_num const &  other) const
inline

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

4944  {
4945  check_context(other);
4946  return Z3_rcf_le(m_ctx, m_num, other.m_num);
4947  }
Z3_rcf_le
bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a <= b.
rcf_num& operator= ( rcf_num const &  other)
inline

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

4856  {
4857  if (this != &other) {
4858  Z3_rcf_del(m_ctx, m_num);
4859  m_ctx = other.m_ctx;
4860  std::string str = Z3_rcf_num_to_string(m_ctx, other.m_num, false, false);
4861  m_num = Z3_rcf_mk_rational(m_ctx, str.c_str());
4862  }
4863  return *this;
4864  }
Z3_rcf_del
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.
Z3_rcf_num_to_string
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html)
Convert the RCF numeral into a string.
Z3_rcf_mk_rational
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val)
Return a RCF rational using the given string.
bool operator== ( rcf_num const &  other) const
inline

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

4954  {
4955  check_context(other);
4956  return Z3_rcf_eq(m_ctx, m_num, other.m_num);
4957  }
Z3_rcf_eq
bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a == b.
bool operator> ( rcf_num const &  other) const
inline

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

4939  {
4940  check_context(other);
4941  return Z3_rcf_gt(m_ctx, m_num, other.m_num);
4942  }
Z3_rcf_gt
bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a > b.
bool operator>= ( rcf_num const &  other) const
inline

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

4949  {
4950  check_context(other);
4951  return Z3_rcf_ge(m_ctx, m_num, other.m_num);
4952  }
Z3_rcf_ge
bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a >= b.
rcf_num power ( unsigned  k) const
inline

Return the power of this number raised to k.

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

4920  {
4921  return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
4922  Z3_rcf_power(m_ctx, m_num, k));
4923  }
z3::rcf_num::rcf_num
rcf_num(context &c, Z3_rcf_num n)
Definition: z3++.h:4840
Z3_rcf_power
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k)
Return the value a^k.
std::string to_decimal ( unsigned  precision = 10) const
inline

Return decimal string representation with given precision.

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

4883  {
4884  return std::string(Z3_rcf_num_to_decimal_string(m_ctx, m_num, precision));
4885  }
Z3_rcf_num_to_decimal_string
Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec)
Convert the RCF numeral into a string in decimal notation.
std::string to_string ( bool  compact = false) const
inline

Return string representation of the RCF numeral.

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

4876  {
4877  return std::string(Z3_rcf_num_to_string(m_ctx, m_num, compact, false));
4878  }
Z3_rcf_num_to_string
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html)
Convert the RCF numeral into a string.

Friends And Related Function Documentation

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

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

4981  {
4982  return out << n.to_string();
4983  }
Generated on Sun Apr 26 2026 02:49:43 for Z3 by   doxygen 1.8.10