Z3 C API Ohmygentool D translation

z3.d

import core.stdc.stdarg;
import core.stdc.locale;
import core.stdc.ctype;
import core.stdc.time;
import core.stdc.stdio;
import core.stdc.wchar_;
import core.stdc.float_;
import core.stdc.errno;
import core.stdc.string;
import core.stdc.stddef;
import core.stdc.stdlib;
import core.stdc.math;
import core.stdc.limits;
import core.stdc.stdint;

import core.stdc.config;
import std.bitmanip : bitfields;
import std.conv : emplace;

bool isModuleAvailable(alias T)() {
    mixin("import " ~ T ~ ";");
    static if (__traits(compiles, (mixin(T)).stringof))
        return true;
    else
        return false;
}
    
static if (__traits(compiles, isModuleAvailable!"nsgen" )) 
    static import nsgen;

struct CppClassSizeAttr
{
    alias size this;
    size_t size;
}
CppClassSizeAttr cppclasssize(size_t a) { return CppClassSizeAttr(a); }

struct CppSizeAttr
{
    alias size this;
    size_t size;
}
CppSizeAttr cppsize(size_t a) { return CppSizeAttr(a); }

struct CppMethodAttr{}
CppMethodAttr cppmethod() { return CppMethodAttr(); }

struct PyExtract{}
auto pyExtract(string name = null) { return PyExtract(); }

mixin template RvalueRef()
{
    alias T = typeof(this);
    static assert (is(T == struct));

    @nogc @safe
    ref const(T) byRef() const pure nothrow return
    {
        return this;
    }
}


extern(C)
bool Z3_algebraic_is_value(Z3_context c, Z3_ast a);

extern(C)
bool Z3_algebraic_is_pos(Z3_context c, Z3_ast a);

extern(C)
bool Z3_algebraic_is_neg(Z3_context c, Z3_ast a);

extern(C)
bool Z3_algebraic_is_zero(Z3_context c, Z3_ast a);

extern(C)
int Z3_algebraic_sign(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
Z3_ast Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
Z3_ast Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
Z3_ast Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
Z3_ast Z3_algebraic_root(Z3_context c, Z3_ast a, uint k);

extern(C)
Z3_ast Z3_algebraic_power(Z3_context c, Z3_ast a, uint k);

extern(C)
bool Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
bool Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
bool Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
bool Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
bool Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
bool Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);

extern(C)
Z3_ast_vector Z3_algebraic_roots(Z3_context c, Z3_ast p, uint n, Z3_ast* a);

extern(C)
int Z3_algebraic_eval(Z3_context c, Z3_ast p, uint n, Z3_ast* a);

extern(C)
Z3_ast_vector Z3_algebraic_get_poly(Z3_context c, Z3_ast a);

extern(C)
uint Z3_algebraic_get_i(Z3_context c, Z3_ast a);

enum Z3_sort_opt = `Z3_sort`;
enum Z3_ast_opt = `Z3_ast`;
enum Z3_func_interp_opt = `Z3_func_interp`;
enum Z3_TRUE = `true`;
enum Z3_FALSE = `false`;
alias Z3_bool = bool;

alias Z3_string = const(char)*;

alias Z3_char_ptr = const(char)*;

alias Z3_string_ptr = const(char)**;

alias Z3_lbool = int;
enum : Z3_lbool
{
    Z3_L_FALSE = -1, 
    Z3_L_UNDEF = 0, 
    Z3_L_TRUE = 1, 
}

alias Z3_symbol_kind = int;
enum : Z3_symbol_kind
{
    Z3_INT_SYMBOL = 0, 
    Z3_STRING_SYMBOL = 1, 
}

alias Z3_parameter_kind = int;
enum : Z3_parameter_kind
{
    Z3_PARAMETER_INT = 0, 
    Z3_PARAMETER_DOUBLE = 1, 
    Z3_PARAMETER_RATIONAL = 2, 
    Z3_PARAMETER_SYMBOL = 3, 
    Z3_PARAMETER_SORT = 4, 
    Z3_PARAMETER_AST = 5, 
    Z3_PARAMETER_FUNC_DECL = 6, 
}

alias Z3_sort_kind = int;
enum : Z3_sort_kind
{
    Z3_UNINTERPRETED_SORT = 0, 
    Z3_BOOL_SORT = 1, 
    Z3_INT_SORT = 2, 
    Z3_REAL_SORT = 3, 
    Z3_BV_SORT = 4, 
    Z3_ARRAY_SORT = 5, 
    Z3_DATATYPE_SORT = 6, 
    Z3_RELATION_SORT = 7, 
    Z3_FINITE_DOMAIN_SORT = 8, 
    Z3_FLOATING_POINT_SORT = 9, 
    Z3_ROUNDING_MODE_SORT = 10, 
    Z3_SEQ_SORT = 11, 
    Z3_RE_SORT = 12, 
    Z3_UNKNOWN_SORT = 1000, 
}

alias Z3_ast_kind = int;
enum : Z3_ast_kind
{
    Z3_NUMERAL_AST = 0, 
    Z3_APP_AST = 1, 
    Z3_VAR_AST = 2, 
    Z3_QUANTIFIER_AST = 3, 
    Z3_SORT_AST = 4, 
    Z3_FUNC_DECL_AST = 5, 
    Z3_UNKNOWN_AST = 1000, 
}

alias Z3_decl_kind = int;
enum : Z3_decl_kind
{
    Z3_OP_TRUE = 256, 
    Z3_OP_FALSE = 257, 
    Z3_OP_EQ = 258, 
    Z3_OP_DISTINCT = 259, 
    Z3_OP_ITE = 260, 
    Z3_OP_AND = 261, 
    Z3_OP_OR = 262, 
    Z3_OP_IFF = 263, 
    Z3_OP_XOR = 264, 
    Z3_OP_NOT = 265, 
    Z3_OP_IMPLIES = 266, 
    Z3_OP_OEQ = 267, 
    Z3_OP_ANUM = 512, 
    Z3_OP_AGNUM = 513, 
    Z3_OP_LE = 514, 
    Z3_OP_GE = 515, 
    Z3_OP_LT = 516, 
    Z3_OP_GT = 517, 
    Z3_OP_ADD = 518, 
    Z3_OP_SUB = 519, 
    Z3_OP_UMINUS = 520, 
    Z3_OP_MUL = 521, 
    Z3_OP_DIV = 522, 
    Z3_OP_IDIV = 523, 
    Z3_OP_REM = 524, 
    Z3_OP_MOD = 525, 
    Z3_OP_TO_REAL = 526, 
    Z3_OP_TO_INT = 527, 
    Z3_OP_IS_INT = 528, 
    Z3_OP_POWER = 529, 
    Z3_OP_STORE = 768, 
    Z3_OP_SELECT = 769, 
    Z3_OP_CONST_ARRAY = 770, 
    Z3_OP_ARRAY_MAP = 771, 
    Z3_OP_ARRAY_DEFAULT = 772, 
    Z3_OP_SET_UNION = 773, 
    Z3_OP_SET_INTERSECT = 774, 
    Z3_OP_SET_DIFFERENCE = 775, 
    Z3_OP_SET_COMPLEMENT = 776, 
    Z3_OP_SET_SUBSET = 777, 
    Z3_OP_AS_ARRAY = 778, 
    Z3_OP_ARRAY_EXT = 779, 
    Z3_OP_SET_HAS_SIZE = 780, 
    Z3_OP_SET_CARD = 781, 
    Z3_OP_BNUM = 1024, 
    Z3_OP_BIT1 = 1025, 
    Z3_OP_BIT0 = 1026, 
    Z3_OP_BNEG = 1027, 
    Z3_OP_BADD = 1028, 
    Z3_OP_BSUB = 1029, 
    Z3_OP_BMUL = 1030, 
    Z3_OP_BSDIV = 1031, 
    Z3_OP_BUDIV = 1032, 
    Z3_OP_BSREM = 1033, 
    Z3_OP_BUREM = 1034, 
    Z3_OP_BSMOD = 1035, 
    Z3_OP_BSDIV0 = 1036, 
    Z3_OP_BUDIV0 = 1037, 
    Z3_OP_BSREM0 = 1038, 
    Z3_OP_BUREM0 = 1039, 
    Z3_OP_BSMOD0 = 1040, 
    Z3_OP_ULEQ = 1041, 
    Z3_OP_SLEQ = 1042, 
    Z3_OP_UGEQ = 1043, 
    Z3_OP_SGEQ = 1044, 
    Z3_OP_ULT = 1045, 
    Z3_OP_SLT = 1046, 
    Z3_OP_UGT = 1047, 
    Z3_OP_SGT = 1048, 
    Z3_OP_BAND = 1049, 
    Z3_OP_BOR = 1050, 
    Z3_OP_BNOT = 1051, 
    Z3_OP_BXOR = 1052, 
    Z3_OP_BNAND = 1053, 
    Z3_OP_BNOR = 1054, 
    Z3_OP_BXNOR = 1055, 
    Z3_OP_CONCAT = 1056, 
    Z3_OP_SIGN_EXT = 1057, 
    Z3_OP_ZERO_EXT = 1058, 
    Z3_OP_EXTRACT = 1059, 
    Z3_OP_REPEAT = 1060, 
    Z3_OP_BREDOR = 1061, 
    Z3_OP_BREDAND = 1062, 
    Z3_OP_BCOMP = 1063, 
    Z3_OP_BSHL = 1064, 
    Z3_OP_BLSHR = 1065, 
    Z3_OP_BASHR = 1066, 
    Z3_OP_ROTATE_LEFT = 1067, 
    Z3_OP_ROTATE_RIGHT = 1068, 
    Z3_OP_EXT_ROTATE_LEFT = 1069, 
    Z3_OP_EXT_ROTATE_RIGHT = 1070, 
    Z3_OP_BIT2BOOL = 1071, 
    Z3_OP_INT2BV = 1072, 
    Z3_OP_BV2INT = 1073, 
    Z3_OP_CARRY = 1074, 
    Z3_OP_XOR3 = 1075, 
    Z3_OP_BSMUL_NO_OVFL = 1076, 
    Z3_OP_BUMUL_NO_OVFL = 1077, 
    Z3_OP_BSMUL_NO_UDFL = 1078, 
    Z3_OP_BSDIV_I = 1079, 
    Z3_OP_BUDIV_I = 1080, 
    Z3_OP_BSREM_I = 1081, 
    Z3_OP_BUREM_I = 1082, 
    Z3_OP_BSMOD_I = 1083, 
    Z3_OP_PR_UNDEF = 1280, 
    Z3_OP_PR_TRUE = 1281, 
    Z3_OP_PR_ASSERTED = 1282, 
    Z3_OP_PR_GOAL = 1283, 
    Z3_OP_PR_MODUS_PONENS = 1284, 
    Z3_OP_PR_REFLEXIVITY = 1285, 
    Z3_OP_PR_SYMMETRY = 1286, 
    Z3_OP_PR_TRANSITIVITY = 1287, 
    Z3_OP_PR_TRANSITIVITY_STAR = 1288, 
    Z3_OP_PR_MONOTONICITY = 1289, 
    Z3_OP_PR_QUANT_INTRO = 1290, 
    Z3_OP_PR_BIND = 1291, 
    Z3_OP_PR_DISTRIBUTIVITY = 1292, 
    Z3_OP_PR_AND_ELIM = 1293, 
    Z3_OP_PR_NOT_OR_ELIM = 1294, 
    Z3_OP_PR_REWRITE = 1295, 
    Z3_OP_PR_REWRITE_STAR = 1296, 
    Z3_OP_PR_PULL_QUANT = 1297, 
    Z3_OP_PR_PUSH_QUANT = 1298, 
    Z3_OP_PR_ELIM_UNUSED_VARS = 1299, 
    Z3_OP_PR_DER = 1300, 
    Z3_OP_PR_QUANT_INST = 1301, 
    Z3_OP_PR_HYPOTHESIS = 1302, 
    Z3_OP_PR_LEMMA = 1303, 
    Z3_OP_PR_UNIT_RESOLUTION = 1304, 
    Z3_OP_PR_IFF_TRUE = 1305, 
    Z3_OP_PR_IFF_FALSE = 1306, 
    Z3_OP_PR_COMMUTATIVITY = 1307, 
    Z3_OP_PR_DEF_AXIOM = 1308, 
    Z3_OP_PR_ASSUMPTION_ADD = 1309, 
    Z3_OP_PR_LEMMA_ADD = 1310, 
    Z3_OP_PR_REDUNDANT_DEL = 1311, 
    Z3_OP_PR_CLAUSE_TRAIL = 1312, 
    Z3_OP_PR_DEF_INTRO = 1313, 
    Z3_OP_PR_APPLY_DEF = 1314, 
    Z3_OP_PR_IFF_OEQ = 1315, 
    Z3_OP_PR_NNF_POS = 1316, 
    Z3_OP_PR_NNF_NEG = 1317, 
    Z3_OP_PR_SKOLEMIZE = 1318, 
    Z3_OP_PR_MODUS_PONENS_OEQ = 1319, 
    Z3_OP_PR_TH_LEMMA = 1320, 
    Z3_OP_PR_HYPER_RESOLVE = 1321, 
    Z3_OP_RA_STORE = 1536, 
    Z3_OP_RA_EMPTY = 1537, 
    Z3_OP_RA_IS_EMPTY = 1538, 
    Z3_OP_RA_JOIN = 1539, 
    Z3_OP_RA_UNION = 1540, 
    Z3_OP_RA_WIDEN = 1541, 
    Z3_OP_RA_PROJECT = 1542, 
    Z3_OP_RA_FILTER = 1543, 
    Z3_OP_RA_NEGATION_FILTER = 1544, 
    Z3_OP_RA_RENAME = 1545, 
    Z3_OP_RA_COMPLEMENT = 1546, 
    Z3_OP_RA_SELECT = 1547, 
    Z3_OP_RA_CLONE = 1548, 
    Z3_OP_FD_CONSTANT = 1549, 
    Z3_OP_FD_LT = 1550, 
    Z3_OP_SEQ_UNIT = 1551, 
    Z3_OP_SEQ_EMPTY = 1552, 
    Z3_OP_SEQ_CONCAT = 1553, 
    Z3_OP_SEQ_PREFIX = 1554, 
    Z3_OP_SEQ_SUFFIX = 1555, 
    Z3_OP_SEQ_CONTAINS = 1556, 
    Z3_OP_SEQ_EXTRACT = 1557, 
    Z3_OP_SEQ_REPLACE = 1558, 
    Z3_OP_SEQ_AT = 1559, 
    Z3_OP_SEQ_NTH = 1560, 
    Z3_OP_SEQ_LENGTH = 1561, 
    Z3_OP_SEQ_INDEX = 1562, 
    Z3_OP_SEQ_LAST_INDEX = 1563, 
    Z3_OP_SEQ_TO_RE = 1564, 
    Z3_OP_SEQ_IN_RE = 1565, 
    Z3_OP_STR_TO_INT = 1566, 
    Z3_OP_INT_TO_STR = 1567, 
    Z3_OP_STRING_LT = 1568, 
    Z3_OP_STRING_LE = 1569, 
    Z3_OP_RE_PLUS = 1570, 
    Z3_OP_RE_STAR = 1571, 
    Z3_OP_RE_OPTION = 1572, 
    Z3_OP_RE_CONCAT = 1573, 
    Z3_OP_RE_UNION = 1574, 
    Z3_OP_RE_RANGE = 1575, 
    Z3_OP_RE_LOOP = 1576, 
    Z3_OP_RE_INTERSECT = 1577, 
    Z3_OP_RE_EMPTY_SET = 1578, 
    Z3_OP_RE_FULL_SET = 1579, 
    Z3_OP_RE_COMPLEMENT = 1580, 
    Z3_OP_LABEL = 1792, 
    Z3_OP_LABEL_LIT = 1793, 
    Z3_OP_DT_CONSTRUCTOR = 2048, 
    Z3_OP_DT_RECOGNISER = 2049, 
    Z3_OP_DT_IS = 2050, 
    Z3_OP_DT_ACCESSOR = 2051, 
    Z3_OP_DT_UPDATE_FIELD = 2052, 
    Z3_OP_PB_AT_MOST = 2304, 
    Z3_OP_PB_AT_LEAST = 2305, 
    Z3_OP_PB_LE = 2306, 
    Z3_OP_PB_GE = 2307, 
    Z3_OP_PB_EQ = 2308, 
    Z3_OP_SPECIAL_RELATION_LO = 40960, 
    Z3_OP_SPECIAL_RELATION_PO = 40961, 
    Z3_OP_SPECIAL_RELATION_PLO = 40962, 
    Z3_OP_SPECIAL_RELATION_TO = 40963, 
    Z3_OP_SPECIAL_RELATION_TC = 40964, 
    Z3_OP_SPECIAL_RELATION_TRC = 40965, 
    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056, 
    Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 45057, 
    Z3_OP_FPA_RM_TOWARD_POSITIVE = 45058, 
    Z3_OP_FPA_RM_TOWARD_NEGATIVE = 45059, 
    Z3_OP_FPA_RM_TOWARD_ZERO = 45060, 
    Z3_OP_FPA_NUM = 45061, 
    Z3_OP_FPA_PLUS_INF = 45062, 
    Z3_OP_FPA_MINUS_INF = 45063, 
    Z3_OP_FPA_NAN = 45064, 
    Z3_OP_FPA_PLUS_ZERO = 45065, 
    Z3_OP_FPA_MINUS_ZERO = 45066, 
    Z3_OP_FPA_ADD = 45067, 
    Z3_OP_FPA_SUB = 45068, 
    Z3_OP_FPA_NEG = 45069, 
    Z3_OP_FPA_MUL = 45070, 
    Z3_OP_FPA_DIV = 45071, 
    Z3_OP_FPA_REM = 45072, 
    Z3_OP_FPA_ABS = 45073, 
    Z3_OP_FPA_MIN = 45074, 
    Z3_OP_FPA_MAX = 45075, 
    Z3_OP_FPA_FMA = 45076, 
    Z3_OP_FPA_SQRT = 45077, 
    Z3_OP_FPA_ROUND_TO_INTEGRAL = 45078, 
    Z3_OP_FPA_EQ = 45079, 
    Z3_OP_FPA_LT = 45080, 
    Z3_OP_FPA_GT = 45081, 
    Z3_OP_FPA_LE = 45082, 
    Z3_OP_FPA_GE = 45083, 
    Z3_OP_FPA_IS_NAN = 45084, 
    Z3_OP_FPA_IS_INF = 45085, 
    Z3_OP_FPA_IS_ZERO = 45086, 
    Z3_OP_FPA_IS_NORMAL = 45087, 
    Z3_OP_FPA_IS_SUBNORMAL = 45088, 
    Z3_OP_FPA_IS_NEGATIVE = 45089, 
    Z3_OP_FPA_IS_POSITIVE = 45090, 
    Z3_OP_FPA_FP = 45091, 
    Z3_OP_FPA_TO_FP = 45092, 
    Z3_OP_FPA_TO_FP_UNSIGNED = 45093, 
    Z3_OP_FPA_TO_UBV = 45094, 
    Z3_OP_FPA_TO_SBV = 45095, 
    Z3_OP_FPA_TO_REAL = 45096, 
    Z3_OP_FPA_TO_IEEE_BV = 45097, 
    Z3_OP_FPA_BVWRAP = 45098, 
    Z3_OP_FPA_BV2RM = 45099, 
    Z3_OP_INTERNAL = 45100, 
    Z3_OP_UNINTERPRETED = 45101, 
}

alias Z3_param_kind = int;
enum : Z3_param_kind
{
    Z3_PK_UINT = 0, 
    Z3_PK_BOOL = 1, 
    Z3_PK_DOUBLE = 2, 
    Z3_PK_SYMBOL = 3, 
    Z3_PK_STRING = 4, 
    Z3_PK_OTHER = 5, 
    Z3_PK_INVALID = 6, 
}

alias Z3_ast_print_mode = int;
enum : Z3_ast_print_mode
{
    Z3_PRINT_SMTLIB_FULL = 0, 
    Z3_PRINT_LOW_LEVEL = 1, 
    Z3_PRINT_SMTLIB2_COMPLIANT = 2, 
}

alias Z3_error_code = int;
enum : Z3_error_code
{
    Z3_OK = 0, 
    Z3_SORT_ERROR = 1, 
    Z3_IOB = 2, 
    Z3_INVALID_ARG = 3, 
    Z3_PARSER_ERROR = 4, 
    Z3_NO_PARSER = 5, 
    Z3_INVALID_PATTERN = 6, 
    Z3_MEMOUT_FAIL = 7, 
    Z3_FILE_ACCESS_ERROR = 8, 
    Z3_INTERNAL_FATAL = 9, 
    Z3_INVALID_USAGE = 10, 
    Z3_DEC_REF_ERROR = 11, 
    Z3_EXCEPTION = 12, 
}

alias Z3_error_handler = extern(C++) void function(Z3_context, Z3_error_code);

alias Z3_push_eh = extern(C++) void function(void*);

alias Z3_pop_eh = extern(C++) void function(void*, uint);

alias Z3_fresh_eh = extern(C++) void* function(void*, Z3_context);

alias Z3_fixed_eh = extern(C++) void function(void*, Z3_solver_callback, uint, Z3_ast);

alias Z3_eq_eh = extern(C++) void function(void*, Z3_solver_callback, uint, uint);

alias Z3_final_eh = extern(C++) void function(void*, Z3_solver_callback);

alias Z3_goal_prec = int;
enum : Z3_goal_prec
{
    Z3_GOAL_PRECISE = 0, 
    Z3_GOAL_UNDER = 1, 
    Z3_GOAL_OVER = 2, 
    Z3_GOAL_UNDER_OVER = 3, 
}

extern(C)
void Z3_global_param_set(const(char)* param_id, const(char)* param_value);

extern(C)
void Z3_global_param_reset_all();

extern(C)
Z3_bool Z3_global_param_get(const(char)* param_id, const(char)** param_value);

extern(C)
Z3_config Z3_mk_config();

extern(C)
void Z3_del_config(Z3_config c);

extern(C)
void Z3_set_param_value(Z3_config c, const(char)* param_id, const(char)* param_value);

extern(C)
Z3_context Z3_mk_context(Z3_config c);

extern(C)
Z3_context Z3_mk_context_rc(Z3_config c);

extern(C)
void Z3_del_context(Z3_context c);

extern(C)
void Z3_inc_ref(Z3_context c, Z3_ast a);

extern(C)
void Z3_dec_ref(Z3_context c, Z3_ast a);

extern(C)
void Z3_update_param_value(Z3_context c, const(char)* param_id, const(char)* param_value);

extern(C)
void Z3_interrupt(Z3_context c);

extern(C)
Z3_params Z3_mk_params(Z3_context c);

extern(C)
void Z3_params_inc_ref(Z3_context c, Z3_params p);

extern(C)
void Z3_params_dec_ref(Z3_context c, Z3_params p);

extern(C)
void Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v);

extern(C)
void Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, uint v);

extern(C)
void Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v);

extern(C)
void Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v);

extern(C)
const(char)* Z3_params_to_string(Z3_context c, Z3_params p);

extern(C)
void Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d);

extern(C)
void Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p);

extern(C)
void Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p);

extern(C)
Z3_param_kind Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n);

extern(C)
uint Z3_param_descrs_size(Z3_context c, Z3_param_descrs p);

extern(C)
Z3_symbol Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, uint i);

extern(C)
const(char)* Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);

extern(C)
const(char)* Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p);

extern(C)
Z3_symbol Z3_mk_int_symbol(Z3_context c, int i);

extern(C)
Z3_symbol Z3_mk_string_symbol(Z3_context c, const(char)* s);

extern(C)
Z3_sort Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s);

extern(C)
Z3_sort Z3_mk_bool_sort(Z3_context c);

extern(C)
Z3_sort Z3_mk_int_sort(Z3_context c);

extern(C)
Z3_sort Z3_mk_real_sort(Z3_context c);

extern(C)
Z3_sort Z3_mk_bv_sort(Z3_context c, uint sz);

extern(C)
Z3_sort Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size);

extern(C)
Z3_sort Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);

extern(C)
Z3_sort Z3_mk_array_sort_n(Z3_context c, uint n, const(Z3_sort)* domain, Z3_sort range);

extern(C)
Z3_sort Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, uint num_fields, const(Z3_symbol)* field_names, const(Z3_sort)* field_sorts, Z3_func_decl* mk_tuple_decl, Z3_func_decl* proj_decl);

extern(C)
Z3_sort Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, uint n, const(Z3_symbol)* enum_names, Z3_func_decl* enum_consts, Z3_func_decl* enum_testers);

extern(C)
Z3_sort Z3_mk_list_sort(Z3_context c, Z3_symbol name, Z3_sort elem_sort, Z3_func_decl* nil_decl, Z3_func_decl* is_nil_decl, Z3_func_decl* cons_decl, Z3_func_decl* is_cons_decl, Z3_func_decl* head_decl, Z3_func_decl* tail_decl);

extern(C)
Z3_constructor Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, uint num_fields, const(Z3_symbol)* field_names, const(Z3_sort)* sorts, uint* sort_refs);

extern(C)
void Z3_del_constructor(Z3_context c, Z3_constructor constr);

extern(C)
Z3_sort Z3_mk_datatype(Z3_context c, Z3_symbol name, uint num_constructors, Z3_constructor* constructors);

extern(C)
Z3_constructor_list Z3_mk_constructor_list(Z3_context c, uint num_constructors, const(Z3_constructor)* constructors);

extern(C)
void Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);

extern(C)
void Z3_mk_datatypes(Z3_context c, uint num_sorts, const(Z3_symbol)* sort_names, Z3_sort* sorts, Z3_constructor_list* constructor_lists);

extern(C)
void Z3_query_constructor(Z3_context c, Z3_constructor constr, uint num_fields, Z3_func_decl* constructor, Z3_func_decl* tester, Z3_func_decl* accessors);

extern(C)
Z3_func_decl Z3_mk_func_decl(Z3_context c, Z3_symbol s, uint domain_size, const(Z3_sort)* domain, Z3_sort range);

extern(C)
Z3_ast Z3_mk_app(Z3_context c, Z3_func_decl d, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty);

extern(C)
Z3_func_decl Z3_mk_fresh_func_decl(Z3_context c, const(char)* prefix, uint domain_size, const(Z3_sort)* domain, Z3_sort range);

extern(C)
Z3_ast Z3_mk_fresh_const(Z3_context c, const(char)* prefix, Z3_sort ty);

extern(C)
Z3_func_decl Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, uint domain_size, const(Z3_sort)* domain, Z3_sort range);

extern(C)
void Z3_add_rec_def(Z3_context c, Z3_func_decl f, uint n, Z3_ast* args, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_true(Z3_context c);

extern(C)
Z3_ast Z3_mk_false(Z3_context c);

extern(C)
Z3_ast Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r);

extern(C)
Z3_ast Z3_mk_distinct(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_not(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3);

extern(C)
Z3_ast Z3_mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_and(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_or(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_add(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_mul(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_sub(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_unary_minus(Z3_context c, Z3_ast arg);

extern(C)
Z3_ast Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_int2real(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_real2int(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_is_int(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvnot(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvredand(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvredor(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvneg(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_extract(Z3_context c, uint high, uint low, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_sign_ext(Z3_context c, uint i, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_zero_ext(Z3_context c, uint i, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_repeat(Z3_context c, uint i, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_rotate_left(Z3_context c, uint i, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_rotate_right(Z3_context c, uint i, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_int2bv(Z3_context c, uint n, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed);

extern(C)
Z3_ast Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);

extern(C)
Z3_ast Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);

extern(C)
Z3_ast Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1);

extern(C)
Z3_ast Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed);

extern(C)
Z3_ast Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);

extern(C)
Z3_ast Z3_mk_select_n(Z3_context c, Z3_ast a, uint n, const(Z3_ast)* idxs);

extern(C)
Z3_ast Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);

extern(C)
Z3_ast Z3_mk_store_n(Z3_context c, Z3_ast a, uint n, const(Z3_ast)* idxs, Z3_ast v);

extern(C)
Z3_ast Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v);

extern(C)
Z3_ast Z3_mk_map(Z3_context c, Z3_func_decl f, uint n, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_array_default(Z3_context c, Z3_ast array);

extern(C)
Z3_ast Z3_mk_as_array(Z3_context c, Z3_func_decl f);

extern(C)
Z3_ast Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);

extern(C)
Z3_sort Z3_mk_set_sort(Z3_context c, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_empty_set(Z3_context c, Z3_sort domain);

extern(C)
Z3_ast Z3_mk_full_set(Z3_context c, Z3_sort domain);

extern(C)
Z3_ast Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem);

extern(C)
Z3_ast Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem);

extern(C)
Z3_ast Z3_mk_set_union(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_set_intersect(Z3_context c, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_set_complement(Z3_context c, Z3_ast arg);

extern(C)
Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set);

extern(C)
Z3_ast Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);

extern(C)
Z3_ast Z3_mk_numeral(Z3_context c, const(char)* numeral, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_real(Z3_context c, int num, int den);

extern(C)
Z3_ast Z3_mk_int(Z3_context c, int v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_unsigned_int(Z3_context c, uint v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_bv_numeral(Z3_context c, uint sz, const(bool)* bits);

extern(C)
Z3_sort Z3_mk_seq_sort(Z3_context c, Z3_sort s);

extern(C)
bool Z3_is_seq_sort(Z3_context c, Z3_sort s);

extern(C)
Z3_sort Z3_get_seq_sort_basis(Z3_context c, Z3_sort s);

extern(C)
Z3_sort Z3_mk_re_sort(Z3_context c, Z3_sort seq);

extern(C)
bool Z3_is_re_sort(Z3_context c, Z3_sort s);

extern(C)
Z3_sort Z3_get_re_sort_basis(Z3_context c, Z3_sort s);

extern(C)
Z3_sort Z3_mk_string_sort(Z3_context c);

extern(C)
bool Z3_is_string_sort(Z3_context c, Z3_sort s);

extern(C)
Z3_ast Z3_mk_string(Z3_context c, const(char)* s);

extern(C)
Z3_ast Z3_mk_lstring(Z3_context c, uint len, const(char)* s);

extern(C)
bool Z3_is_string(Z3_context c, Z3_ast s);

extern(C)
const(char)* Z3_get_string(Z3_context c, Z3_ast s);

extern(C)
const(char)* Z3_get_lstring(Z3_context c, Z3_ast s, uint* length);

extern(C)
Z3_ast Z3_mk_seq_empty(Z3_context c, Z3_sort seq);

extern(C)
Z3_ast Z3_mk_seq_unit(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_mk_seq_concat(Z3_context c, uint n, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);

extern(C)
Z3_ast Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);

extern(C)
Z3_ast Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);

extern(C)
Z3_ast Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s);

extern(C)
Z3_ast Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s);

extern(C)
Z3_ast Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);

extern(C)
Z3_ast Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);

extern(C)
Z3_ast Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);

extern(C)
Z3_ast Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index);

extern(C)
Z3_ast Z3_mk_seq_length(Z3_context c, Z3_ast s);

extern(C)
Z3_ast Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);

extern(C)
Z3_ast Z3_mk_seq_last_index(Z3_context c, Z3_ast , Z3_ast substr);

extern(C)
Z3_ast Z3_mk_str_to_int(Z3_context c, Z3_ast s);

extern(C)
Z3_ast Z3_mk_int_to_str(Z3_context c, Z3_ast s);

extern(C)
Z3_ast Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);

extern(C)
Z3_ast Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);

extern(C)
Z3_ast Z3_mk_re_plus(Z3_context c, Z3_ast re);

extern(C)
Z3_ast Z3_mk_re_star(Z3_context c, Z3_ast re);

extern(C)
Z3_ast Z3_mk_re_option(Z3_context c, Z3_ast re);

extern(C)
Z3_ast Z3_mk_re_union(Z3_context c, uint n, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_re_concat(Z3_context c, uint n, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);

extern(C)
Z3_ast Z3_mk_re_loop(Z3_context c, Z3_ast r, uint lo, uint hi);

extern(C)
Z3_ast Z3_mk_re_intersect(Z3_context c, uint n, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_mk_re_complement(Z3_context c, Z3_ast re);

extern(C)
Z3_ast Z3_mk_re_empty(Z3_context c, Z3_sort re);

extern(C)
Z3_ast Z3_mk_re_full(Z3_context c, Z3_sort re);

extern(C)
Z3_func_decl Z3_mk_linear_order(Z3_context c, Z3_sort a, uint id);

extern(C)
Z3_func_decl Z3_mk_partial_order(Z3_context c, Z3_sort a, uint id);

extern(C)
Z3_func_decl Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, uint id);

extern(C)
Z3_func_decl Z3_mk_tree_order(Z3_context c, Z3_sort a, uint id);

extern(C)
Z3_func_decl Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);

extern(C)
Z3_pattern Z3_mk_pattern(Z3_context c, uint num_patterns, const(Z3_ast)* terms);

extern(C)
Z3_ast Z3_mk_bound(Z3_context c, uint index, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_forall(Z3_context c, uint weight, uint num_patterns, const(Z3_pattern)* patterns, uint num_decls, const(Z3_sort)* sorts, const(Z3_symbol)* decl_names, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_exists(Z3_context c, uint weight, uint num_patterns, const(Z3_pattern)* patterns, uint num_decls, const(Z3_sort)* sorts, const(Z3_symbol)* decl_names, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_quantifier(Z3_context c, bool is_forall, uint weight, uint num_patterns, const(Z3_pattern)* patterns, uint num_decls, const(Z3_sort)* sorts, const(Z3_symbol)* decl_names, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_quantifier_ex(Z3_context c, bool is_forall, uint weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, uint num_patterns, const(Z3_pattern)* patterns, uint num_no_patterns, const(Z3_ast)* no_patterns, uint num_decls, const(Z3_sort)* sorts, const(Z3_symbol)* decl_names, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_forall_const(Z3_context c, uint weight, uint num_bound, const(Z3_app)* bound, uint num_patterns, const(Z3_pattern)* patterns, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_exists_const(Z3_context c, uint weight, uint num_bound, const(Z3_app)* bound, uint num_patterns, const(Z3_pattern)* patterns, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_quantifier_const(Z3_context c, bool is_forall, uint weight, uint num_bound, const(Z3_app)* bound, uint num_patterns, const(Z3_pattern)* patterns, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_quantifier_const_ex(Z3_context c, bool is_forall, uint weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, uint num_bound, const(Z3_app)* bound, uint num_patterns, const(Z3_pattern)* patterns, uint num_no_patterns, const(Z3_ast)* no_patterns, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_lambda(Z3_context c, uint num_decls, const(Z3_sort)* sorts, const(Z3_symbol)* decl_names, Z3_ast body_);

extern(C)
Z3_ast Z3_mk_lambda_const(Z3_context c, uint num_bound, const(Z3_app)* bound, Z3_ast body_);

extern(C)
Z3_symbol_kind Z3_get_symbol_kind(Z3_context c, Z3_symbol s);

extern(C)
int Z3_get_symbol_int(Z3_context c, Z3_symbol s);

extern(C)
const(char)* Z3_get_symbol_string(Z3_context c, Z3_symbol s);

extern(C)
Z3_symbol Z3_get_sort_name(Z3_context c, Z3_sort d);

extern(C)
uint Z3_get_sort_id(Z3_context c, Z3_sort s);

extern(C)
Z3_ast Z3_sort_to_ast(Z3_context c, Z3_sort s);

extern(C)
bool Z3_is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2);

extern(C)
Z3_sort_kind Z3_get_sort_kind(Z3_context c, Z3_sort t);

extern(C)
uint Z3_get_bv_sort_size(Z3_context c, Z3_sort t);

extern(C)
Z3_bool Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);

extern(C)
Z3_sort Z3_get_array_sort_domain(Z3_context c, Z3_sort t);

extern(C)
Z3_sort Z3_get_array_sort_range(Z3_context c, Z3_sort t);

extern(C)
Z3_func_decl Z3_get_tuple_sort_mk_decl(Z3_context c, Z3_sort t);

extern(C)
uint Z3_get_tuple_sort_num_fields(Z3_context c, Z3_sort t);

extern(C)
Z3_func_decl Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, uint i);

extern(C)
uint Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t);

extern(C)
Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, uint idx);

extern(C)
Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, uint idx);

extern(C)
Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, uint idx_c, uint idx_a);

extern(C)
Z3_ast Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value);

extern(C)
uint Z3_get_relation_arity(Z3_context c, Z3_sort s);

extern(C)
Z3_sort Z3_get_relation_column(Z3_context c, Z3_sort s, uint col);

extern(C)
Z3_ast Z3_mk_atmost(Z3_context c, uint num_args, const(Z3_ast)* args, uint k);

extern(C)
Z3_ast Z3_mk_atleast(Z3_context c, uint num_args, const(Z3_ast)* args, uint k);

extern(C)
Z3_ast Z3_mk_pble(Z3_context c, uint num_args, const(Z3_ast)* args, const(int)* coeffs, int k);

extern(C)
Z3_ast Z3_mk_pbge(Z3_context c, uint num_args, const(Z3_ast)* args, const(int)* coeffs, int k);

extern(C)
Z3_ast Z3_mk_pbeq(Z3_context c, uint num_args, const(Z3_ast)* args, const(int)* coeffs, int k);

extern(C)
Z3_ast Z3_func_decl_to_ast(Z3_context c, Z3_func_decl f);

extern(C)
bool Z3_is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2);

extern(C)
uint Z3_get_func_decl_id(Z3_context c, Z3_func_decl f);

extern(C)
Z3_symbol Z3_get_decl_name(Z3_context c, Z3_func_decl d);

extern(C)
Z3_decl_kind Z3_get_decl_kind(Z3_context c, Z3_func_decl d);

extern(C)
uint Z3_get_domain_size(Z3_context c, Z3_func_decl d);

extern(C)
uint Z3_get_arity(Z3_context c, Z3_func_decl d);

extern(C)
Z3_sort Z3_get_domain(Z3_context c, Z3_func_decl d, uint i);

extern(C)
Z3_sort Z3_get_range(Z3_context c, Z3_func_decl d);

extern(C)
uint Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d);

extern(C)
Z3_parameter_kind Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
int Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
double Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
Z3_symbol Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
Z3_sort Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
Z3_ast Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
Z3_func_decl Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
const(char)* Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, uint idx);

extern(C)
Z3_ast Z3_app_to_ast(Z3_context c, Z3_app a);

extern(C)
Z3_func_decl Z3_get_app_decl(Z3_context c, Z3_app a);

extern(C)
uint Z3_get_app_num_args(Z3_context c, Z3_app a);

extern(C)
Z3_ast Z3_get_app_arg(Z3_context c, Z3_app a, uint i);

extern(C)
bool Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
uint Z3_get_ast_id(Z3_context c, Z3_ast t);

extern(C)
uint Z3_get_ast_hash(Z3_context c, Z3_ast a);

extern(C)
Z3_sort Z3_get_sort(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_well_sorted(Z3_context c, Z3_ast t);

extern(C)
Z3_lbool Z3_get_bool_value(Z3_context c, Z3_ast a);

extern(C)
Z3_ast_kind Z3_get_ast_kind(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_app(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_numeral_ast(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_algebraic_number(Z3_context c, Z3_ast a);

extern(C)
Z3_app Z3_to_app(Z3_context c, Z3_ast a);

extern(C)
Z3_func_decl Z3_to_func_decl(Z3_context c, Z3_ast a);

extern(C)
const(char)* Z3_get_numeral_string(Z3_context c, Z3_ast a);

extern(C)
const(char)* Z3_get_numeral_binary_string(Z3_context c, Z3_ast a);

extern(C)
const(char)* Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, uint precision);

extern(C)
double Z3_get_numeral_double(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_get_numerator(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_get_denominator(Z3_context c, Z3_ast a);

extern(C)
bool Z3_get_numeral_small(Z3_context c, Z3_ast a, int64_t* num, int64_t* den);

extern(C)
bool Z3_get_numeral_int(Z3_context c, Z3_ast v, int* i);

extern(C)
bool Z3_get_numeral_uint(Z3_context c, Z3_ast v, uint* u);

extern(C)
bool Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t* u);

extern(C)
bool Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t* i);

extern(C)
bool Z3_get_numeral_rational_int64(Z3_context c, Z3_ast v, int64_t* num, int64_t* den);

extern(C)
Z3_ast Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, uint precision);

extern(C)
Z3_ast Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, uint precision);

extern(C)
Z3_ast Z3_pattern_to_ast(Z3_context c, Z3_pattern p);

extern(C)
uint Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p);

extern(C)
Z3_ast Z3_get_pattern(Z3_context c, Z3_pattern p, uint idx);

extern(C)
uint Z3_get_index_value(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_quantifier_forall(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_quantifier_exists(Z3_context c, Z3_ast a);

extern(C)
bool Z3_is_lambda(Z3_context c, Z3_ast a);

extern(C)
uint Z3_get_quantifier_weight(Z3_context c, Z3_ast a);

extern(C)
uint Z3_get_quantifier_num_patterns(Z3_context c, Z3_ast a);

extern(C)
Z3_pattern Z3_get_quantifier_pattern_ast(Z3_context c, Z3_ast a, uint i);

extern(C)
uint Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, uint i);

extern(C)
uint Z3_get_quantifier_num_bound(Z3_context c, Z3_ast a);

extern(C)
Z3_symbol Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, uint i);

extern(C)
Z3_sort Z3_get_quantifier_bound_sort(Z3_context c, Z3_ast a, uint i);

extern(C)
Z3_ast Z3_get_quantifier_body(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_simplify(Z3_context c, Z3_ast a);

extern(C)
Z3_ast Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p);

extern(C)
const(char)* Z3_simplify_get_help(Z3_context c);

extern(C)
Z3_param_descrs Z3_simplify_get_param_descrs(Z3_context c);

extern(C)
Z3_ast Z3_update_term(Z3_context c, Z3_ast a, uint num_args, const(Z3_ast)* args);

extern(C)
Z3_ast Z3_substitute(Z3_context c, Z3_ast a, uint num_exprs, const(Z3_ast)* from, const(Z3_ast)* to);

extern(C)
Z3_ast Z3_substitute_vars(Z3_context c, Z3_ast a, uint num_exprs, const(Z3_ast)* to);

extern(C)
Z3_ast Z3_translate(Z3_context source, Z3_ast a, Z3_context target);

extern(C)
Z3_model Z3_mk_model(Z3_context c);

extern(C)
void Z3_model_inc_ref(Z3_context c, Z3_model m);

extern(C)
void Z3_model_dec_ref(Z3_context c, Z3_model m);

extern(C)
Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast* v);

extern(C)
Z3_ast Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);

extern(C)
bool Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a);

extern(C)
Z3_func_interp Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);

extern(C)
uint Z3_model_get_num_consts(Z3_context c, Z3_model m);

extern(C)
Z3_func_decl Z3_model_get_const_decl(Z3_context c, Z3_model m, uint i);

extern(C)
uint Z3_model_get_num_funcs(Z3_context c, Z3_model m);

extern(C)
Z3_func_decl Z3_model_get_func_decl(Z3_context c, Z3_model m, uint i);

extern(C)
uint Z3_model_get_num_sorts(Z3_context c, Z3_model m);

extern(C)
Z3_sort Z3_model_get_sort(Z3_context c, Z3_model m, uint i);

extern(C)
Z3_ast_vector Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);

extern(C)
Z3_model Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);

extern(C)
bool Z3_is_as_array(Z3_context c, Z3_ast a);

extern(C)
Z3_func_decl Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);

extern(C)
Z3_func_interp Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value);

extern(C)
void Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);

extern(C)
void Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f);

extern(C)
void Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f);

extern(C)
uint Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);

extern(C)
Z3_func_entry Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, uint i);

extern(C)
Z3_ast Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);

extern(C)
void Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);

extern(C)
uint Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);

extern(C)
void Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);

extern(C)
void Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);

extern(C)
void Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e);

extern(C)
Z3_ast Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);

extern(C)
uint Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);

extern(C)
Z3_ast Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, uint i);

extern(C)
bool Z3_open_log(const(char)* filename);

extern(C)
void Z3_append_log(const(char)* string_);

extern(C)
void Z3_close_log();

extern(C)
void Z3_toggle_warning_messages(bool enabled);

extern(C)
void Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode);

extern(C)
const(char)* Z3_ast_to_string(Z3_context c, Z3_ast a);

extern(C)
const(char)* Z3_pattern_to_string(Z3_context c, Z3_pattern p);

extern(C)
const(char)* Z3_sort_to_string(Z3_context c, Z3_sort s);

extern(C)
const(char)* Z3_func_decl_to_string(Z3_context c, Z3_func_decl d);

extern(C)
const(char)* Z3_model_to_string(Z3_context c, Z3_model m);

extern(C)
const(char)* Z3_benchmark_to_smtlib_string(Z3_context c, const(char)* name, const(char)* logic, const(char)* status, const(char)* attributes, uint num_assumptions, const(Z3_ast)* assumptions, Z3_ast formula);

extern(C)
Z3_ast_vector Z3_parse_smtlib2_string(Z3_context c, const(char)* str, uint num_sorts, const(Z3_symbol)* sort_names, const(Z3_sort)* sorts, uint num_decls, const(Z3_symbol)* decl_names, const(Z3_func_decl)* decls);

extern(C)
Z3_ast_vector Z3_parse_smtlib2_file(Z3_context c, const(char)* file_name, uint num_sorts, const(Z3_symbol)* sort_names, const(Z3_sort)* sorts, uint num_decls, const(Z3_symbol)* decl_names, const(Z3_func_decl)* decls);

extern(C)
const(char)* Z3_eval_smtlib2_string(Z3_context , const(char)* str);

extern(C)
Z3_error_code Z3_get_error_code(Z3_context c);

extern(C)
void Z3_set_error_handler(Z3_context c, Z3_error_handler h);

extern(C)
void Z3_set_error(Z3_context c, Z3_error_code e);

extern(C)
const(char)* Z3_get_error_msg(Z3_context c, Z3_error_code err);

extern(C)
void Z3_get_version(uint* major, uint* minor, uint* build_number, uint* revision_number);

extern(C)
const(char)* Z3_get_full_version();

extern(C)
void Z3_enable_trace(const(char)* tag);

extern(C)
void Z3_disable_trace(const(char)* tag);

extern(C)
void Z3_reset_memory();

extern(C)
void Z3_finalize_memory();

extern(C)
Z3_goal Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs);

extern(C)
void Z3_goal_inc_ref(Z3_context c, Z3_goal g);

extern(C)
void Z3_goal_dec_ref(Z3_context c, Z3_goal g);

extern(C)
Z3_goal_prec Z3_goal_precision(Z3_context c, Z3_goal g);

extern(C)
void Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);

extern(C)
bool Z3_goal_inconsistent(Z3_context c, Z3_goal g);

extern(C)
uint Z3_goal_depth(Z3_context c, Z3_goal g);

extern(C)
void Z3_goal_reset(Z3_context c, Z3_goal g);

extern(C)
uint Z3_goal_size(Z3_context c, Z3_goal g);

extern(C)
Z3_ast Z3_goal_formula(Z3_context c, Z3_goal g, uint idx);

extern(C)
uint Z3_goal_num_exprs(Z3_context c, Z3_goal g);

extern(C)
bool Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);

extern(C)
bool Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g);

extern(C)
Z3_goal Z3_goal_translate(Z3_context source, Z3_goal g, Z3_context target);

extern(C)
Z3_model Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m);

extern(C)
const(char)* Z3_goal_to_string(Z3_context c, Z3_goal g);

extern(C)
const(char)* Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names);

extern(C)
Z3_tactic Z3_mk_tactic(Z3_context c, const(char)* name);

extern(C)
void Z3_tactic_inc_ref(Z3_context c, Z3_tactic t);

extern(C)
void Z3_tactic_dec_ref(Z3_context c, Z3_tactic g);

extern(C)
Z3_probe Z3_mk_probe(Z3_context c, const(char)* name);

extern(C)
void Z3_probe_inc_ref(Z3_context c, Z3_probe p);

extern(C)
void Z3_probe_dec_ref(Z3_context c, Z3_probe p);

extern(C)
Z3_tactic Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);

extern(C)
Z3_tactic Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2);

extern(C)
Z3_tactic Z3_tactic_par_or(Z3_context c, uint num, const(Z3_tactic)* ts);

extern(C)
Z3_tactic Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2);

extern(C)
Z3_tactic Z3_tactic_try_for(Z3_context c, Z3_tactic t, uint ms);

extern(C)
Z3_tactic Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t);

extern(C)
Z3_tactic Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2);

extern(C)
Z3_tactic Z3_tactic_repeat(Z3_context c, Z3_tactic t, uint max);

extern(C)
Z3_tactic Z3_tactic_skip(Z3_context c);

extern(C)
Z3_tactic Z3_tactic_fail(Z3_context c);

extern(C)
Z3_tactic Z3_tactic_fail_if(Z3_context c, Z3_probe p);

extern(C)
Z3_tactic Z3_tactic_fail_if_not_decided(Z3_context c);

extern(C)
Z3_tactic Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p);

extern(C)
Z3_probe Z3_probe_const(Z3_context x, double val);

extern(C)
Z3_probe Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2);

extern(C)
Z3_probe Z3_probe_not(Z3_context x, Z3_probe p);

extern(C)
uint Z3_get_num_tactics(Z3_context c);

extern(C)
const(char)* Z3_get_tactic_name(Z3_context c, uint i);

extern(C)
uint Z3_get_num_probes(Z3_context c);

extern(C)
const(char)* Z3_get_probe_name(Z3_context c, uint i);

extern(C)
const(char)* Z3_tactic_get_help(Z3_context c, Z3_tactic t);

extern(C)
Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t);

extern(C)
const(char)* Z3_tactic_get_descr(Z3_context c, const(char)* name);

extern(C)
const(char)* Z3_probe_get_descr(Z3_context c, const(char)* name);

extern(C)
double Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g);

extern(C)
Z3_apply_result Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);

extern(C)
Z3_apply_result Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);

extern(C)
void Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r);

extern(C)
void Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r);

extern(C)
const(char)* Z3_apply_result_to_string(Z3_context c, Z3_apply_result r);

extern(C)
uint Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);

extern(C)
Z3_goal Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, uint i);

extern(C)
Z3_solver Z3_mk_solver(Z3_context c);

extern(C)
Z3_solver Z3_mk_simple_solver(Z3_context c);

extern(C)
Z3_solver Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);

extern(C)
Z3_solver Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);

extern(C)
Z3_solver Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);

extern(C)
void Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst);

extern(C)
const(char)* Z3_solver_get_help(Z3_context c, Z3_solver s);

extern(C)
Z3_param_descrs Z3_solver_get_param_descrs(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p);

extern(C)
void Z3_solver_inc_ref(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_dec_ref(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_interrupt(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_push(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_pop(Z3_context c, Z3_solver s, uint n);

extern(C)
void Z3_solver_reset(Z3_context c, Z3_solver s);

extern(C)
uint Z3_solver_get_num_scopes(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a);

extern(C)
void Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);

extern(C)
void Z3_solver_from_file(Z3_context c, Z3_solver s, const(char)* file_name);

extern(C)
void Z3_solver_from_string(Z3_context c, Z3_solver s, const(char)* file_name);

extern(C)
Z3_ast_vector Z3_solver_get_assertions(Z3_context c, Z3_solver s);

extern(C)
Z3_ast_vector Z3_solver_get_units(Z3_context c, Z3_solver s);

extern(C)
Z3_ast_vector Z3_solver_get_trail(Z3_context c, Z3_solver s);

extern(C)
Z3_ast_vector Z3_solver_get_non_units(Z3_context c, Z3_solver s);

extern(C)
void Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, uint sz, uint* levels);

extern(C)
void Z3_solver_propagate_init(Z3_context c, Z3_solver s, void* user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh);

extern(C)
void Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh);

extern(C)
void Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh);

extern(C)
void Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);

extern(C)
void Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);

extern(C)
uint Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e);

extern(C)
void Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback , uint num_fixed, const(uint)* fixed_ids, uint num_eqs, const(uint)* eq_lhs, const(uint)* eq_rhs, Z3_ast conseq);

extern(C)
Z3_lbool Z3_solver_check(Z3_context c, Z3_solver s);

extern(C)
Z3_lbool Z3_solver_check_assumptions(Z3_context c, Z3_solver s, uint num_assumptions, const(Z3_ast)* assumptions);

extern(C)
Z3_lbool Z3_get_implied_equalities(Z3_context c, Z3_solver s, uint num_terms, const(Z3_ast)* terms, uint* class_ids);

extern(C)
Z3_lbool Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences);

extern(C)
Z3_ast_vector Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, uint backtrack_level);

extern(C)
Z3_model Z3_solver_get_model(Z3_context c, Z3_solver s);

extern(C)
Z3_ast Z3_solver_get_proof(Z3_context c, Z3_solver s);

extern(C)
Z3_ast_vector Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);

extern(C)
const(char)* Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s);

extern(C)
Z3_stats Z3_solver_get_statistics(Z3_context c, Z3_solver s);

extern(C)
const(char)* Z3_solver_to_string(Z3_context c, Z3_solver s);

extern(C)
const(char)* Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names);

extern(C)
const(char)* Z3_stats_to_string(Z3_context c, Z3_stats s);

extern(C)
void Z3_stats_inc_ref(Z3_context c, Z3_stats s);

extern(C)
void Z3_stats_dec_ref(Z3_context c, Z3_stats s);

extern(C)
uint Z3_stats_size(Z3_context c, Z3_stats s);

extern(C)
const(char)* Z3_stats_get_key(Z3_context c, Z3_stats s, uint idx);

extern(C)
bool Z3_stats_is_uint(Z3_context c, Z3_stats s, uint idx);

extern(C)
bool Z3_stats_is_double(Z3_context c, Z3_stats s, uint idx);

extern(C)
uint Z3_stats_get_uint_value(Z3_context c, Z3_stats s, uint idx);

extern(C)
double Z3_stats_get_double_value(Z3_context c, Z3_stats s, uint idx);

extern(C)
uint64_t Z3_get_estimated_alloc_size();

extern(C)
Z3_ast_vector Z3_mk_ast_vector(Z3_context c);

extern(C)
void Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v);

extern(C)
void Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v);

extern(C)
uint Z3_ast_vector_size(Z3_context c, Z3_ast_vector v);

extern(C)
Z3_ast Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, uint i);

extern(C)
void Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, uint i, Z3_ast a);

extern(C)
void Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, uint n);

extern(C)
void Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a);

extern(C)
Z3_ast_vector Z3_ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t);

extern(C)
const(char)* Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v);

extern(C)
Z3_ast_map Z3_mk_ast_map(Z3_context c);

extern(C)
void Z3_ast_map_inc_ref(Z3_context c, Z3_ast_map m);

extern(C)
void Z3_ast_map_dec_ref(Z3_context c, Z3_ast_map m);

extern(C)
bool Z3_ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k);

extern(C)
Z3_ast Z3_ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k);

extern(C)
void Z3_ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v);

extern(C)
void Z3_ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k);

extern(C)
void Z3_ast_map_reset(Z3_context c, Z3_ast_map m);

extern(C)
uint Z3_ast_map_size(Z3_context c, Z3_ast_map m);

extern(C)
Z3_ast_vector Z3_ast_map_keys(Z3_context c, Z3_ast_map m);

extern(C)
const(char)* Z3_ast_map_to_string(Z3_context c, Z3_ast_map m);

extern(C)
Z3_fixedpoint Z3_mk_fixedpoint(Z3_context c);

extern(C)
void Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d);

extern(C)
void Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d);

extern(C)
void Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name);

extern(C)
void Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, uint num_args, uint* args);

extern(C)
void Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom);

extern(C)
Z3_bool Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query);

extern(C)
Z3_bool Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, uint num_relations, const(Z3_func_decl)* relations);

extern(C)
Z3_ast Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d);

extern(C)
const(char)* Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d);

extern(C)
void Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name);

extern(C)
uint Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);

extern(C)
Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred);

extern(C)
void Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property);

extern(C)
Z3_stats Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d);

extern(C)
void Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f);

extern(C)
void Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, uint num_relations, const(Z3_symbol)* relation_kinds);

extern(C)
Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f);

extern(C)
Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f);

extern(C)
void Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p);

extern(C)
const(char)* Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f);

extern(C)
Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f);

extern(C)
const(char)* Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, uint num_queries, Z3_ast* queries);

extern(C)
Z3_ast_vector Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, const(char)* s);

extern(C)
Z3_ast_vector Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, const(char)* s);

alias Z3_fixedpoint_reduce_assign_callback_fptr = extern(C) void function(void*, Z3_func_decl, uint, const(Z3_ast)*, uint, const(Z3_ast)*);

alias Z3_fixedpoint_reduce_app_callback_fptr = extern(C) void function(void*, Z3_func_decl, uint, const(Z3_ast)*, Z3_ast*);

extern(C)
void Z3_fixedpoint_init(Z3_context c, Z3_fixedpoint d, void* state);

extern(C)
void Z3_fixedpoint_set_reduce_assign_callback(Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb);

extern(C)
void Z3_fixedpoint_set_reduce_app_callback(Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb);

alias Z3_fixedpoint_new_lemma_eh = extern(C) void function(void*, Z3_ast, uint);

alias Z3_fixedpoint_predecessor_eh = extern(C) void function(void*);

alias Z3_fixedpoint_unfold_eh = extern(C) void function(void*);

extern(C)
void Z3_fixedpoint_add_callback(Z3_context ctx, Z3_fixedpoint f, void* state, void function(void*, Z3_ast, uint) new_lemma_eh, void function(void*) predecessor_eh, void function(void*) unfold_eh);

extern(C)
void Z3_fixedpoint_add_constraint(Z3_context c, Z3_fixedpoint d, Z3_ast e, uint lvl);

extern(C)
Z3_sort Z3_mk_fpa_rounding_mode_sort(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_rne(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_rna(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_round_toward_positive(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_rtp(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_round_toward_negative(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_rtn(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_round_toward_zero(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_rtz(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort(Z3_context c, uint ebits, uint sbits);

extern(C)
Z3_sort Z3_mk_fpa_sort_half(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_16(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_single(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_32(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_double(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_64(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_quadruple(Z3_context c);

extern(C)
Z3_sort Z3_mk_fpa_sort_128(Z3_context c);

extern(C)
Z3_ast Z3_mk_fpa_nan(Z3_context c, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);

extern(C)
Z3_ast Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);

extern(C)
Z3_ast Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);

extern(C)
Z3_ast Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_fpa_numeral_int(Z3_context c, int v, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_fpa_numeral_int_uint(Z3_context c, bool sgn, int exp, uint sig, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty);

extern(C)
Z3_ast Z3_mk_fpa_abs(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_neg(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);

extern(C)
Z3_ast Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);

extern(C)
Z3_ast Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);

extern(C)
Z3_ast Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, uint sz);

extern(C)
Z3_ast Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, uint sz);

extern(C)
Z3_ast Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);

extern(C)
uint Z3_fpa_get_ebits(Z3_context c, Z3_sort s);

extern(C)
uint Z3_fpa_get_sbits(Z3_context c, Z3_sort s);

extern(C)
bool Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int* sgn);

extern(C)
const(char)* Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t);

extern(C)
bool Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t* n);

extern(C)
const(char)* Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased);

extern(C)
bool Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t* n, bool biased);

extern(C)
Z3_ast Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased);

extern(C)
Z3_ast Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t);

extern(C)
Z3_ast Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);

alias Z3_model_eh = extern(C++) void function(void*);

extern(C)
Z3_optimize Z3_mk_optimize(Z3_context c);

extern(C)
void Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);

extern(C)
void Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);

extern(C)
void Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);

extern(C)
void Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t);

extern(C)
uint Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, const(char)* weight, Z3_symbol id);

extern(C)
uint Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);

extern(C)
uint Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);

extern(C)
void Z3_optimize_push(Z3_context c, Z3_optimize d);

extern(C)
void Z3_optimize_pop(Z3_context c, Z3_optimize d);

extern(C)
Z3_bool Z3_optimize_check(Z3_context c, Z3_optimize o, uint num_assumptions, const(Z3_ast)* assumptions);

extern(C)
const(char)* Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);

extern(C)
Z3_model Z3_optimize_get_model(Z3_context c, Z3_optimize o);

extern(C)
Z3_ast_vector Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);

extern(C)
void Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);

extern(C)
Z3_param_descrs Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);

extern(C)
Z3_ast Z3_optimize_get_lower(Z3_context c, Z3_optimize o, uint idx);

extern(C)
Z3_ast Z3_optimize_get_upper(Z3_context c, Z3_optimize o, uint idx);

extern(C)
Z3_ast_vector Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, uint idx);

extern(C)
Z3_ast_vector Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, uint idx);

extern(C)
const(char)* Z3_optimize_to_string(Z3_context c, Z3_optimize o);

extern(C)
void Z3_optimize_from_string(Z3_context c, Z3_optimize o, const(char)* s);

extern(C)
void Z3_optimize_from_file(Z3_context c, Z3_optimize o, const(char)* s);

extern(C)
const(char)* Z3_optimize_get_help(Z3_context c, Z3_optimize t);

extern(C)
Z3_stats Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);

extern(C)
Z3_ast_vector Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);

extern(C)
Z3_ast_vector Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);

extern(C)
void Z3_optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, void* ctx, Z3_model_eh model_eh);

extern(C)
Z3_ast_vector Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x);

extern(C)
bool Z3_get_numeral_rational(int c, int a, ref rational r);

extern(C)
void Z3_rcf_del(Z3_context c, Z3_rcf_num a);

extern(C)
Z3_rcf_num Z3_rcf_mk_rational(Z3_context c, const(char)* val);

extern(C)
Z3_rcf_num Z3_rcf_mk_small_int(Z3_context c, int val);

extern(C)
Z3_rcf_num Z3_rcf_mk_pi(Z3_context c);

extern(C)
Z3_rcf_num Z3_rcf_mk_e(Z3_context c);

extern(C)
Z3_rcf_num Z3_rcf_mk_infinitesimal(Z3_context c);

extern(C)
uint Z3_rcf_mk_roots(Z3_context c, uint n, const(Z3_rcf_num)* a, Z3_rcf_num* roots);

extern(C)
Z3_rcf_num Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
Z3_rcf_num Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
Z3_rcf_num Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
Z3_rcf_num Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
Z3_rcf_num Z3_rcf_neg(Z3_context c, Z3_rcf_num a);

extern(C)
Z3_rcf_num Z3_rcf_inv(Z3_context c, Z3_rcf_num a);

extern(C)
Z3_rcf_num Z3_rcf_power(Z3_context c, Z3_rcf_num a, uint k);

extern(C)
bool Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
bool Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
bool Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
bool Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
bool Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
bool Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);

extern(C)
const(char)* Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html);

extern(C)
const(char)* Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, uint prec);

extern(C)
void Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num* n, Z3_rcf_num* d);

extern(C)
Z3_lbool Z3_fixedpoint_query_from_lvl(Z3_context c, Z3_fixedpoint d, Z3_ast query, uint lvl);

extern(C)
Z3_ast Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d);

extern(C)
Z3_ast_vector Z3_fixedpoint_get_rules_along_trace(Z3_context c, Z3_fixedpoint d);

extern(C)
Z3_symbol Z3_fixedpoint_get_rule_names_along_trace(Z3_context c, Z3_fixedpoint d);

extern(C)
void Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property);

extern(C)
Z3_ast Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred);

extern(C)
Z3_ast Z3_qe_model_project(Z3_context c, Z3_model m, uint num_bounds, const(Z3_app)* bound, Z3_ast body_);

extern(C)
Z3_ast Z3_qe_model_project_skolem(Z3_context c, Z3_model m, uint num_bounds, const(Z3_app)* bound, Z3_ast body_, Z3_ast_map map);

extern(C)
Z3_ast Z3_model_extrapolate(Z3_context c, Z3_model m, Z3_ast fml);

extern(C)
Z3_ast Z3_qe_lite(Z3_context c, Z3_ast_vector vars, Z3_ast body_);

alias z3_replayer_cmd = extern(C++) void function(ref z3_replayer);

alias z3_replayer_exception = default_exception;

extern(C++, class)
@cppclasssize(8) align(8)
struct z3_replayer
{


    @cppsize(8) private imp* m_imp;
    public this(ref istream in_);

    public ~this();

    public void parse();

    public uint get_line() const ;

    public int get_int(uint pos) const ;

    public uint get_uint(uint pos) const ;

    public int64_t get_int64(uint pos) const ;

    public uint64_t get_uint64(uint pos) const ;

    public float get_float(uint pos) const ;

    public double get_double(uint pos) const ;

    public bool get_bool(uint pos) const ;

    public const(char)* get_str(uint pos) const ;

    public Z3_symbol get_symbol(uint pos) const ;

    public void* get_obj(uint pos) const ;

    public uint* get_uint_array(uint pos) const ;

    public int* get_int_array(uint pos) const ;

    public bool* get_bool_array(uint pos) const ;

    public Z3_symbol* get_symbol_array(uint pos) const ;

    public void** get_obj_array(uint pos) const ;

    public int* get_int_addr(uint pos);

    public int64_t* get_int64_addr(uint pos);

    public uint* get_uint_addr(uint pos);

    public uint64_t* get_uint64_addr(uint pos);

    public const(char)** get_str_addr(uint pos);

    public void** get_obj_addr(uint pos);

    public void store_result(void* obj);

    public void register_cmd(uint id, void function(ref z3_replayer) cmd, const(char)* name);

}
struct Z3_sort;
struct Z3_literals;
struct Z3_symbol;
struct Z3_params;
struct Z3_ast;
struct Z3_config;
struct Z3_context;
struct Z3_func_decl;
struct Z3_app;
struct Z3_pattern;
struct Z3_model;
struct Z3_constructor;
struct Z3_constructor_list;
struct Z3_param_descrs;
struct Z3_goal;
struct Z3_tactic;
struct Z3_probe;
struct Z3_stats;
struct Z3_optimize;
struct Z3_solver;
struct Z3_func_entry;
struct Z3_solver_callback;
struct Z3_ast_vector;
struct Z3_ast_map;
struct Z3_apply_result;
struct Z3_func_interp;
struct Z3_fixedpoint;
struct Z3_rcf_num;
struct imp;