1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 z3_algebraic.h 7 8 Abstract: 9 10 Additional APIs for handling Z3 algebraic numbers encoded as 11 Z3_ASTs 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2012-12-07 16 17 Notes: 18 19 --*/ 20 21 #ifndef Z3_ALGEBRAIC_H_ 22 #define Z3_ALGEBRAIC_H_ 23 24 #ifdef __cplusplus 25 extern "C" { 26 #endif // __cplusplus 27 28 /** \defgroup capi C API */ 29 /*@{*/ 30 31 /** @name Algebraic Numbers */ 32 /*@{*/ 33 /** 34 \brief Return \c true if \c a can be used as value in the Z3 real algebraic 35 number package. 36 37 def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST))) 38 */ 39 bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a); 40 41 /** 42 \brief Return \c true if \c a is positive, and \c false otherwise. 43 44 \pre Z3_algebraic_is_value(c, a) 45 46 def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST))) 47 */ 48 bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a); 49 50 /** 51 \brief Return \c true if \c a is negative, and \c false otherwise. 52 53 \pre Z3_algebraic_is_value(c, a) 54 55 def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST))) 56 */ 57 bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a); 58 59 /** 60 \brief Return \c true if \c a is zero, and \c false otherwise. 61 62 \pre Z3_algebraic_is_value(c, a) 63 64 def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST))) 65 */ 66 bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a); 67 68 /** 69 \brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative. 70 71 \pre Z3_algebraic_is_value(c, a) 72 73 def_API('Z3_algebraic_sign', INT, (_in(CONTEXT), _in(AST))) 74 */ 75 int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a); 76 77 /** 78 \brief Return the value a + b. 79 80 \pre Z3_algebraic_is_value(c, a) 81 \pre Z3_algebraic_is_value(c, b) 82 \post Z3_algebraic_is_value(c, result) 83 84 def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST))) 85 */ 86 Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b); 87 88 /** 89 \brief Return the value a - b. 90 91 \pre Z3_algebraic_is_value(c, a) 92 \pre Z3_algebraic_is_value(c, b) 93 \post Z3_algebraic_is_value(c, result) 94 95 def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST))) 96 */ 97 Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b); 98 99 /** 100 \brief Return the value a * b. 101 102 \pre Z3_algebraic_is_value(c, a) 103 \pre Z3_algebraic_is_value(c, b) 104 \post Z3_algebraic_is_value(c, result) 105 106 def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST))) 107 */ 108 Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b); 109 110 /** 111 \brief Return the value a / b. 112 113 \pre Z3_algebraic_is_value(c, a) 114 \pre Z3_algebraic_is_value(c, b) 115 \pre !Z3_algebraic_is_zero(c, b) 116 \post Z3_algebraic_is_value(c, result) 117 118 def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST))) 119 */ 120 Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b); 121 122 /** 123 \brief Return the a^(1/k) 124 125 \pre Z3_algebraic_is_value(c, a) 126 \pre k is even => !Z3_algebraic_is_neg(c, a) 127 \post Z3_algebraic_is_value(c, result) 128 129 def_API('Z3_algebraic_root', AST, (_in(CONTEXT), _in(AST), _in(UINT))) 130 */ 131 Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k); 132 133 /** 134 \brief Return the a^k 135 136 \pre Z3_algebraic_is_value(c, a) 137 \post Z3_algebraic_is_value(c, result) 138 139 def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT))) 140 */ 141 Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k); 142 143 /** 144 \brief Return \c true if a < b, and \c false otherwise. 145 146 \pre Z3_algebraic_is_value(c, a) 147 \pre Z3_algebraic_is_value(c, b) 148 149 def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 150 */ 151 bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b); 152 153 /** 154 \brief Return \c true if a > b, and \c false otherwise. 155 156 \pre Z3_algebraic_is_value(c, a) 157 \pre Z3_algebraic_is_value(c, b) 158 159 def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 160 */ 161 bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b); 162 163 /** 164 \brief Return \c true if a <= b, and \c false otherwise. 165 166 \pre Z3_algebraic_is_value(c, a) 167 \pre Z3_algebraic_is_value(c, b) 168 169 def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 170 */ 171 bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b); 172 173 /** 174 \brief Return \c true if a >= b, and \c false otherwise. 175 176 \pre Z3_algebraic_is_value(c, a) 177 \pre Z3_algebraic_is_value(c, b) 178 179 def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 180 */ 181 bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b); 182 183 /** 184 \brief Return \c true if a == b, and \c false otherwise. 185 186 \pre Z3_algebraic_is_value(c, a) 187 \pre Z3_algebraic_is_value(c, b) 188 189 def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 190 */ 191 bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b); 192 193 /** 194 \brief Return \c true if a != b, and \c false otherwise. 195 196 \pre Z3_algebraic_is_value(c, a) 197 \pre Z3_algebraic_is_value(c, b) 198 199 def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST))) 200 */ 201 bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b); 202 203 /** 204 \brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the 205 roots of the univariate polynomial p(a[0], ..., a[n-1], x_n). 206 207 \pre p is a Z3 expression that contains only arithmetic terms and free variables. 208 \pre forall i in [0, n) Z3_algebraic_is_value(c, a[i]) 209 \post forall r in result Z3_algebraic_is_value(c, result) 210 211 def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) 212 */ 213 Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]); 214 215 /** 216 \brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the 217 sign of p(a[0], ..., a[n-1]). 218 219 \pre p is a Z3 expression that contains only arithmetic terms and free variables. 220 \pre forall i in [0, n) Z3_algebraic_is_value(c, a[i]) 221 222 def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) 223 */ 224 int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]); 225 226 /*@}*/ 227 /*@}*/ 228 229 #ifdef __cplusplus 230 } 231 #endif // __cplusplus 232 233 #endif 234