1 /*++ 2 Copyright (c) 2013 Microsoft Corporation 3 4 Module Name: 5 6 z3_rcf.h 7 8 Abstract: 9 10 Additional APIs for handling elements of the Z3 real closed field that contains: 11 - transcendental extensions 12 - infinitesimal extensions 13 - algebraic extensions 14 15 Author: 16 17 Leonardo de Moura (leonardo) 2012-01-05 18 19 Notes: 20 21 --*/ 22 #pragma once 23 24 #ifdef __cplusplus 25 extern "C" { 26 #endif // __cplusplus 27 28 /** \defgroup capi C API */ 29 /*@{*/ 30 31 /** @name Real Closed Fields */ 32 /*@{*/ 33 /** 34 \brief Delete a RCF numeral created using the RCF API. 35 36 def_API('Z3_rcf_del', VOID, (_in(CONTEXT), _in(RCF_NUM))) 37 */ 38 void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a); 39 40 /** 41 \brief Return a RCF rational using the given string. 42 43 def_API('Z3_rcf_mk_rational', RCF_NUM, (_in(CONTEXT), _in(STRING))) 44 */ 45 Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val); 46 47 /** 48 \brief Return a RCF small integer. 49 50 def_API('Z3_rcf_mk_small_int', RCF_NUM, (_in(CONTEXT), _in(INT))) 51 */ 52 Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val); 53 54 /** 55 \brief Return Pi 56 57 def_API('Z3_rcf_mk_pi', RCF_NUM, (_in(CONTEXT),)) 58 */ 59 Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c); 60 61 /** 62 \brief Return e (Euler's constant) 63 64 def_API('Z3_rcf_mk_e', RCF_NUM, (_in(CONTEXT),)) 65 */ 66 Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c); 67 68 /** 69 \brief Return a new infinitesimal that is smaller than all elements in the Z3 field. 70 71 def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),)) 72 */ 73 Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c); 74 75 /** 76 \brief Store in roots the roots of the polynomial \ccode{a[n-1]*x^{n-1} + ... + a[0]}. 77 The output vector \c roots must have size \c n. 78 It returns the number of roots of the polynomial. 79 80 \pre The input polynomial is not the zero polynomial. 81 82 def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM))) 83 */ 84 unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]); 85 86 /** 87 \brief Return the value \ccode{a + b}. 88 89 def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 90 */ 91 Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 92 93 /** 94 \brief Return the value \ccode{a - b}. 95 96 def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 97 */ 98 Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 99 100 /** 101 \brief Return the value \ccode{a * b}. 102 103 def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 104 */ 105 Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 106 107 /** 108 \brief Return the value \ccode{a / b}. 109 110 def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 111 */ 112 Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 113 114 /** 115 \brief Return the value \ccode{-a}. 116 117 def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM))) 118 */ 119 Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a); 120 121 /** 122 \brief Return the value \ccode{1/a}. 123 124 def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM))) 125 */ 126 Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a); 127 128 /** 129 \brief Return the value \ccode{a^k}. 130 131 def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT))) 132 */ 133 Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k); 134 135 /** 136 \brief Return \c true if \ccode{a < b}. 137 138 def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 139 */ 140 bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 141 142 /** 143 \brief Return \c true if \ccode{a > b}. 144 145 def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 146 */ 147 bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 148 149 /** 150 \brief Return \c true if \ccode{a <= b}. 151 152 def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 153 */ 154 bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 155 156 /** 157 \brief Return \c true if \ccode{a >= b}. 158 159 def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 160 */ 161 bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 162 163 /** 164 \brief Return \c true if \ccode{a == b}. 165 166 def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 167 */ 168 bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 169 170 /** 171 \brief Return \c true if \ccode{a != b}. 172 173 def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) 174 */ 175 bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b); 176 177 /** 178 \brief Convert the RCF numeral into a string. 179 180 def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL))) 181 */ 182 Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html); 183 184 /** 185 \brief Convert the RCF numeral into a string in decimal notation. 186 187 def_API('Z3_rcf_num_to_decimal_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(UINT))) 188 */ 189 Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec); 190 191 /** 192 \brief Extract the "numerator" and "denominator" of the given RCF numeral. 193 We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions. 194 195 def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM))) 196 */ 197 void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d); 198 199 /*@}*/ 200 /*@}*/ 201 202 #ifdef __cplusplus 203 } 204 #endif // __cplusplus 205 206