z3_rcf.h

Go to the documentation of this file.

/*++
Copyright (c) 2013 Microsoft Corporation
 
Module Name:
 
    z3_rcf.h
 
Abstract:
 
    Additional APIs for handling elements of the Z3 real closed field that contains:
       - transcendental extensions
       - infinitesimal extensions
       - algebraic extensions
 
Author:
 
    Leonardo de Moura (leonardo) 2012-01-05
 
Notes:
 
--*/
#pragma once
 
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
 
    void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a);
 
    Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val);
 
    Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val);
 
    Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c);
 
    Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c);
 
    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
 
    unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
 
    Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
 
    Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
 
    Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
 
    bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
 
    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html);
 
    Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec);
 
   void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
 
   bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a);
 
   bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a);
 
   bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a);
 
   bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a);
 
   unsigned Z3_API Z3_rcf_extension_index(Z3_context c, Z3_rcf_num a);
 
   Z3_symbol Z3_API Z3_rcf_transcendental_name(Z3_context c, Z3_rcf_num a);
 
   Z3_symbol Z3_API Z3_rcf_infinitesimal_name(Z3_context c, Z3_rcf_num a);
 
   unsigned Z3_API Z3_rcf_num_coefficients(Z3_context c, Z3_rcf_num a);
 
   Z3_rcf_num Z3_API Z3_rcf_coefficient(Z3_context c, Z3_rcf_num a, unsigned i);
 
   int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper);
 
   unsigned Z3_API Z3_rcf_num_sign_conditions(Z3_context c, Z3_rcf_num a);
 
   int Z3_API Z3_rcf_sign_condition_sign(Z3_context c, Z3_rcf_num a, unsigned i);
 
   unsigned Z3_API Z3_rcf_num_sign_condition_coefficients(Z3_context c, Z3_rcf_num a, unsigned i);
 
   Z3_rcf_num Z3_API Z3_rcf_sign_condition_coefficient(Z3_context c, Z3_rcf_num a, unsigned i, unsigned j);
 
#ifdef __cplusplus
}
#endif // __cplusplus