Z3 |

z3_rcf.h
Go to the documentation of this file.
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
30
37 void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a);
38
43 Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val);
44
49 Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val);
50
55 Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c);
56
61 Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c);
62
67 Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
68
77 unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
78
83 Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
84
89 Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
90
95 Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
96
101 Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
102
107 Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
108
113 Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
114
119 Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
120
125 bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
126
131 bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
132
137 bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
138
143 bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
144
149 bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
150
155 bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
156
161 Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html);
162
167 Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec);
168
174 void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
175
178
179#ifdef __cplusplus
180}
181#endif // __cplusplus
182
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
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.
Z3_rcf_mk_roots
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[])
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must ...
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.
Z3_rcf_get_numerator_denominator
void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num *n, Z3_rcf_num *d)
Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d,...
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_eq
bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a == b.
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.
Z3_rcf_inv
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a)
Return the value 1/a.
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.
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_le
bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a <= b.
Z3_rcf_mk_infinitesimal
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c)
Return a new infinitesimal that is smaller than all elements in the Z3 field.
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.
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.
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.
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.
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_neq
bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a != b.
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_mk_pi
Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c)
Return Pi.
Z3_rcf_neg
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a)
Return the value -a.
Z3_rcf_mk_e
Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c)
Return e (Euler's constant)
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.