Z3
doc/tmp/z3_algebraic.h
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     z3_algebraic.h
00007 
00008 Abstract:
00009 
00010     Additional APIs for handling Z3 algebraic numbers encoded as 
00011     Z3_ASTs
00012 
00013 Author:
00014 
00015     Leonardo de Moura (leonardo) 2012-12-07
00016 
00017 Notes:
00018     
00019 --*/
00020 
00021 #ifndef _Z3_ALGEBRAIC_H_
00022 #define _Z3_ALGEBRAIC_H_
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif // __cplusplus    
00027 
00034 
00039 
00045     Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
00046 
00053     Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
00054 
00061     Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
00062 
00069     Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
00070 
00077     int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
00078 
00087     Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00088 
00097     Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00098 
00107     Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00108     
00118     Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00119     
00128     Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
00129 
00137     Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
00138     
00146     Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00147     
00155     Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00156 
00164     Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00165 
00173     Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00174 
00182     Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00183 
00191     Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);    
00192 
00202     Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);    
00203 
00212     int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);    
00213 
00216 
00217 #ifdef __cplusplus
00218 };
00219 #endif // __cplusplus
00220 
00221 #endif
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines