Z3
doc/tmp/z3_rcf.h
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2013 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     z3_rcf.h
00007 
00008 Abstract:
00009 
00010     Additional APIs for handling elements of the Z3 real closed field that contains:
00011        - transcendental extensions
00012        - infinitesimal extensions
00013        - algebraic extensions
00014 
00015 Author:
00016 
00017     Leonardo de Moura (leonardo) 2012-01-05
00018 
00019 Notes:
00020     
00021 --*/
00022 #ifndef _Z3_RCF_H_
00023 #define _Z3_RCF_H_
00024 
00025 #ifdef __cplusplus
00026 extern "C" {
00027 #endif // __cplusplus
00028     
00035 
00040 
00045     void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a);
00046 
00051     Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val);
00052 
00057     Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val);
00058 
00063     Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c);
00064 
00069     Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c);
00070 
00075     Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c);
00076 
00085     unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[]);
00086 
00091     Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00092 
00097     Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00098 
00103     Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00104 
00109     Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00110     
00115     Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a);
00116 
00121     Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a);
00122 
00127     Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k);
00128 
00133     Z3_bool Z3_API Z3_rcf_lt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00134 
00139     Z3_bool Z3_API Z3_rcf_gt(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00140 
00145     Z3_bool Z3_API Z3_rcf_le(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00146 
00151     Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00152 
00157     Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00158 
00163     Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b);
00164 
00169     Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html);
00170 
00175     Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec);
00176 
00182     void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
00183 
00186 
00187 #ifdef __cplusplus
00188 };
00189 #endif // __cplusplus
00190 
00191 #endif
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines