20 using System.Diagnostics.Contracts;
31 [ContractVerification(
true)]
43 Contract.Ensures(Contract.Result<
RatNum>() != null);
57 Contract.Ensures(Contract.Result<
RatNum>() != null);
68 Contract.Ensures(Contract.Result<
string>() != null);
77 Contract.Requires(ctx != null);
RatNum ToUpper(uint precision)
Return a upper bound for a given real algebraic number. The interval isolating the number is smaller ...
string ToDecimal(uint precision)
Returns a string representation in decimal notation.
RatNum ToLower(uint precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
static Z3_ast Z3_get_algebraic_number_upper(Z3_context a0, Z3_ast a1, uint a2)
static Z3_ast Z3_get_algebraic_number_lower(Z3_context a0, Z3_ast a1, uint a2)
static string Z3_get_numeral_decimal_string(Z3_context a0, Z3_ast a1, uint a2)
The main interaction with Z3 happens via the Context.
Arithmetic expressions (int/real)