mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

safe instruction cache

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-18 17:52:14 -07:00
parent bed73a3f43
commit d4babf7181
1 changed files with 410 additions and 392 deletions
Download patch file Download diff file Expand all files Collapse all files

802
src/api/api_ast.cpp
View file

@ -1088,407 +1088,425 @@ extern "C" {
Z3_CATCH_RETURN("");
}
// Helper functions to reduce instruction cache pressure in Z3_get_decl_kind.
// Each theory gets its own function to avoid loading the entire switch table.
static Z3_decl_kind get_decl_kind_basic(decl_kind k) {
switch(k) {
case OP_TRUE: return Z3_OP_TRUE;
case OP_FALSE: return Z3_OP_FALSE;
case OP_EQ: return Z3_OP_EQ;
case OP_DISTINCT: return Z3_OP_DISTINCT;
case OP_ITE: return Z3_OP_ITE;
case OP_AND: return Z3_OP_AND;
case OP_OR: return Z3_OP_OR;
case OP_XOR: return Z3_OP_XOR;
case OP_NOT: return Z3_OP_NOT;
case OP_IMPLIES: return Z3_OP_IMPLIES;
case OP_OEQ: return Z3_OP_OEQ;
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;
case PR_ASSERTED: return Z3_OP_PR_ASSERTED;
case PR_GOAL: return Z3_OP_PR_GOAL;
case PR_MODUS_PONENS: return Z3_OP_PR_MODUS_PONENS;
case PR_REFLEXIVITY: return Z3_OP_PR_REFLEXIVITY;
case PR_SYMMETRY: return Z3_OP_PR_SYMMETRY;
case PR_TRANSITIVITY: return Z3_OP_PR_TRANSITIVITY;
case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR;
case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY;
case PR_QUANT_INTRO: return Z3_OP_PR_QUANT_INTRO;
case PR_BIND: return Z3_OP_PR_BIND;
case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY;
case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM;
case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM;
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
case PR_QUANT_INST: return Z3_OP_PR_QUANT_INST;
case PR_HYPOTHESIS: return Z3_OP_PR_HYPOTHESIS;
case PR_LEMMA: return Z3_OP_PR_LEMMA;
case PR_UNIT_RESOLUTION: return Z3_OP_PR_UNIT_RESOLUTION;
case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE;
case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM;
case PR_ASSUMPTION_ADD: return Z3_OP_PR_ASSUMPTION_ADD;
case PR_LEMMA_ADD: return Z3_OP_PR_LEMMA_ADD;
case PR_REDUNDANT_DEL: return Z3_OP_PR_REDUNDANT_DEL;
case PR_CLAUSE_TRAIL: return Z3_OP_PR_CLAUSE_TRAIL;
case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_arith(decl_kind k) {
switch(k) {
case OP_NUM: return Z3_OP_ANUM;
case OP_IRRATIONAL_ALGEBRAIC_NUM: return Z3_OP_AGNUM;
case OP_LE: return Z3_OP_LE;
case OP_GE: return Z3_OP_GE;
case OP_LT: return Z3_OP_LT;
case OP_GT: return Z3_OP_GT;
case OP_ADD: return Z3_OP_ADD;
case OP_SUB: return Z3_OP_SUB;
case OP_UMINUS: return Z3_OP_UMINUS;
case OP_MUL: return Z3_OP_MUL;
case OP_DIV: return Z3_OP_DIV;
case OP_IDIV: return Z3_OP_IDIV;
case OP_REM: return Z3_OP_REM;
case OP_MOD: return Z3_OP_MOD;
case OP_POWER: return Z3_OP_POWER;
case OP_ABS: return Z3_OP_ABS;
case OP_TO_REAL: return Z3_OP_TO_REAL;
case OP_TO_INT: return Z3_OP_TO_INT;
case OP_IS_INT: return Z3_OP_IS_INT;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_array(decl_kind k) {
switch(k) {
case OP_STORE: return Z3_OP_STORE;
case OP_SELECT: return Z3_OP_SELECT;
case OP_CONST_ARRAY: return Z3_OP_CONST_ARRAY;
case OP_ARRAY_DEFAULT: return Z3_OP_ARRAY_DEFAULT;
case OP_ARRAY_MAP: return Z3_OP_ARRAY_MAP;
case OP_SET_UNION: return Z3_OP_SET_UNION;
case OP_SET_INTERSECT: return Z3_OP_SET_INTERSECT;
case OP_SET_DIFFERENCE: return Z3_OP_SET_DIFFERENCE;
case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT;
case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_special_relations(decl_kind k) {
switch(k) {
case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO;
case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO;
case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC;
default: UNREACHABLE(); return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_bv(decl_kind k) {
switch(k) {
case OP_BV_NUM: return Z3_OP_BNUM;
case OP_BIT1: return Z3_OP_BIT1;
case OP_BIT0: return Z3_OP_BIT0;
case OP_BNEG: return Z3_OP_BNEG;
case OP_BADD: return Z3_OP_BADD;
case OP_BSUB: return Z3_OP_BSUB;
case OP_BMUL: return Z3_OP_BMUL;
case OP_BSDIV: return Z3_OP_BSDIV;
case OP_BUDIV: return Z3_OP_BUDIV;
case OP_BSREM: return Z3_OP_BSREM;
case OP_BUREM: return Z3_OP_BUREM;
case OP_BSMOD: return Z3_OP_BSMOD;
case OP_BSDIV0: return Z3_OP_BSDIV0;
case OP_BUDIV0: return Z3_OP_BUDIV0;
case OP_BSREM0: return Z3_OP_BSREM0;
case OP_BUREM0: return Z3_OP_BUREM0;
case OP_BSMOD0: return Z3_OP_BSMOD0;
case OP_ULEQ: return Z3_OP_ULEQ;
case OP_SLEQ: return Z3_OP_SLEQ;
case OP_UGEQ: return Z3_OP_UGEQ;
case OP_SGEQ: return Z3_OP_SGEQ;
case OP_ULT: return Z3_OP_ULT;
case OP_SLT: return Z3_OP_SLT;
case OP_UGT: return Z3_OP_UGT;
case OP_SGT: return Z3_OP_SGT;
case OP_BAND: return Z3_OP_BAND;
case OP_BOR: return Z3_OP_BOR;
case OP_BNOT: return Z3_OP_BNOT;
case OP_BXOR: return Z3_OP_BXOR;
case OP_BNAND: return Z3_OP_BNAND;
case OP_BNOR: return Z3_OP_BNOR;
case OP_BXNOR: return Z3_OP_BXNOR;
case OP_CONCAT: return Z3_OP_CONCAT;
case OP_SIGN_EXT: return Z3_OP_SIGN_EXT;
case OP_ZERO_EXT: return Z3_OP_ZERO_EXT;
case OP_EXTRACT: return Z3_OP_EXTRACT;
case OP_REPEAT: return Z3_OP_REPEAT;
case OP_BREDOR: return Z3_OP_BREDOR;
case OP_BREDAND: return Z3_OP_BREDAND;
case OP_BCOMP: return Z3_OP_BCOMP;
case OP_BSHL: return Z3_OP_BSHL;
case OP_BLSHR: return Z3_OP_BLSHR;
case OP_BASHR: return Z3_OP_BASHR;
case OP_ROTATE_LEFT: return Z3_OP_ROTATE_LEFT;
case OP_ROTATE_RIGHT: return Z3_OP_ROTATE_RIGHT;
case OP_EXT_ROTATE_LEFT: return Z3_OP_EXT_ROTATE_LEFT;
case OP_EXT_ROTATE_RIGHT: return Z3_OP_EXT_ROTATE_RIGHT;
case OP_INT2BV: return Z3_OP_INT2BV;
case OP_UBV2INT: return Z3_OP_BV2INT;
case OP_SBV2INT: return Z3_OP_SBV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;
case OP_BUREM_I: return Z3_OP_BUREM_I;
case OP_BSMOD_I: return Z3_OP_BSMOD_I;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_dt(decl_kind k) {
switch(k) {
case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR;
case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER;
case OP_DT_IS: return Z3_OP_DT_IS;
case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR;
case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_datalog(decl_kind k) {
switch(k) {
case datalog::OP_RA_STORE: return Z3_OP_RA_STORE;
case datalog::OP_RA_EMPTY: return Z3_OP_RA_EMPTY;
case datalog::OP_RA_IS_EMPTY: return Z3_OP_RA_IS_EMPTY;
case datalog::OP_RA_JOIN: return Z3_OP_RA_JOIN;
case datalog::OP_RA_UNION: return Z3_OP_RA_UNION;
case datalog::OP_RA_WIDEN: return Z3_OP_RA_WIDEN;
case datalog::OP_RA_PROJECT: return Z3_OP_RA_PROJECT;
case datalog::OP_RA_FILTER: return Z3_OP_RA_FILTER;
case datalog::OP_RA_NEGATION_FILTER: return Z3_OP_RA_NEGATION_FILTER;
case datalog::OP_RA_RENAME: return Z3_OP_RA_RENAME;
case datalog::OP_RA_COMPLEMENT: return Z3_OP_RA_COMPLEMENT;
case datalog::OP_RA_SELECT: return Z3_OP_RA_SELECT;
case datalog::OP_RA_CLONE: return Z3_OP_RA_CLONE;
case datalog::OP_DL_CONSTANT: return Z3_OP_FD_CONSTANT;
case datalog::OP_DL_LT: return Z3_OP_FD_LT;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_seq(decl_kind k) {
switch (k) {
case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
case OP_SEQ_REPLACE_RE: return Z3_OP_SEQ_REPLACE_RE;
case OP_SEQ_REPLACE_RE_ALL: return Z3_OP_SEQ_REPLACE_RE_ALL;
case OP_SEQ_REPLACE_ALL: return Z3_OP_SEQ_REPLACE_ALL;
case OP_SEQ_AT: return Z3_OP_SEQ_AT;
case OP_SEQ_NTH: return Z3_OP_SEQ_NTH;
case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
case OP_SEQ_MAP: return Z3_OP_SEQ_MAP;
case OP_SEQ_MAPI: return Z3_OP_SEQ_MAPI;
case OP_SEQ_FOLDL: return Z3_OP_SEQ_FOLDL;
case OP_SEQ_FOLDLI: return Z3_OP_SEQ_FOLDLI;
case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
case _OP_REGEXP_FULL_CHAR: return Z3_OP_RE_FULL_SET;
case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
case OP_STRING_TO_CODE: return Z3_OP_STR_TO_CODE;
case OP_STRING_FROM_CODE: return Z3_OP_STR_FROM_CODE;
case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR;
case OP_STRING_LT: return Z3_OP_STRING_LT;
case OP_STRING_LE: return Z3_OP_STRING_LE;
case OP_RE_PLUS: return Z3_OP_RE_PLUS;
case OP_RE_STAR: return Z3_OP_RE_STAR;
case OP_RE_OPTION: return Z3_OP_RE_OPTION;
case OP_RE_RANGE: return Z3_OP_RE_RANGE;
case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
case OP_RE_UNION: return Z3_OP_RE_UNION;
case OP_RE_DIFF: return Z3_OP_RE_DIFF;
case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
case OP_RE_LOOP: return Z3_OP_RE_LOOP;
case OP_RE_POWER: return Z3_OP_RE_POWER;
case OP_RE_COMPLEMENT: return Z3_OP_RE_COMPLEMENT;
case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET;
case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_CHAR_SET;
case OP_RE_OF_PRED: return Z3_OP_RE_OF_PRED;
case OP_RE_REVERSE: return Z3_OP_RE_REVERSE;
case OP_RE_DERIVATIVE: return Z3_OP_RE_DERIVATIVE;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_char(decl_kind k) {
switch (k) {
case OP_CHAR_CONST: return Z3_OP_CHAR_CONST;
case OP_CHAR_LE: return Z3_OP_CHAR_LE;
case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT;
case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV;
case OP_CHAR_FROM_BV: return Z3_OP_CHAR_FROM_BV;
case OP_CHAR_IS_DIGIT: return Z3_OP_CHAR_IS_DIGIT;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_fpa(decl_kind k) {
switch (k) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;
case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY;
case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE;
case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE;
case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO;
case OP_FPA_NUM: return Z3_OP_FPA_NUM;
case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF;
case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF;
case OP_FPA_NAN: return Z3_OP_FPA_NAN;
case OP_FPA_MINUS_ZERO: return Z3_OP_FPA_MINUS_ZERO;
case OP_FPA_PLUS_ZERO: return Z3_OP_FPA_PLUS_ZERO;
case OP_FPA_ADD: return Z3_OP_FPA_ADD;
case OP_FPA_SUB: return Z3_OP_FPA_SUB;
case OP_FPA_NEG: return Z3_OP_FPA_NEG;
case OP_FPA_MUL: return Z3_OP_FPA_MUL;
case OP_FPA_DIV: return Z3_OP_FPA_DIV;
case OP_FPA_REM: return Z3_OP_FPA_REM;
case OP_FPA_ABS: return Z3_OP_FPA_ABS;
case OP_FPA_MIN: return Z3_OP_FPA_MIN;
case OP_FPA_MAX: return Z3_OP_FPA_MAX;
case OP_FPA_FMA: return Z3_OP_FPA_FMA;
case OP_FPA_SQRT: return Z3_OP_FPA_SQRT;
case OP_FPA_EQ: return Z3_OP_FPA_EQ;
case OP_FPA_ROUND_TO_INTEGRAL: return Z3_OP_FPA_ROUND_TO_INTEGRAL;
case OP_FPA_LT: return Z3_OP_FPA_LT;
case OP_FPA_GT: return Z3_OP_FPA_GT;
case OP_FPA_LE: return Z3_OP_FPA_LE;
case OP_FPA_GE: return Z3_OP_FPA_GE;
case OP_FPA_IS_NAN: return Z3_OP_FPA_IS_NAN;
case OP_FPA_IS_INF: return Z3_OP_FPA_IS_INF;
case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO;
case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL;
case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL;
case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE;
case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE;
case OP_FPA_FP: return Z3_OP_FPA_FP;
case OP_FPA_TO_FP: return Z3_OP_FPA_TO_FP;
case OP_FPA_TO_FP_UNSIGNED: return Z3_OP_FPA_TO_FP_UNSIGNED;
case OP_FPA_TO_UBV: return Z3_OP_FPA_TO_UBV;
case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV;
case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL;
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_BVWRAP: return Z3_OP_FPA_BVWRAP;
case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_label(decl_kind k) {
switch(k) {
case OP_LABEL: return Z3_OP_LABEL;
case OP_LABEL_LIT: return Z3_OP_LABEL_LIT;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_pb(decl_kind k) {
switch(k) {
case OP_PB_LE: return Z3_OP_PB_LE;
case OP_PB_GE: return Z3_OP_PB_GE;
case OP_PB_EQ: return Z3_OP_PB_EQ;
case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
case OP_AT_LEAST_K: return Z3_OP_PB_AT_LEAST;
default: return Z3_OP_INTERNAL;
}
}
static Z3_decl_kind get_decl_kind_finite_set(decl_kind k) {
switch(k) {
case OP_FINITE_SET_EMPTY: return Z3_OP_FINITE_SET_EMPTY;
case OP_FINITE_SET_SINGLETON: return Z3_OP_FINITE_SET_SINGLETON;
case OP_FINITE_SET_UNION: return Z3_OP_FINITE_SET_UNION;
case OP_FINITE_SET_INTERSECT: return Z3_OP_FINITE_SET_INTERSECT;
case OP_FINITE_SET_DIFFERENCE: return Z3_OP_FINITE_SET_DIFFERENCE;
case OP_FINITE_SET_IN: return Z3_OP_FINITE_SET_IN;
case OP_FINITE_SET_SIZE: return Z3_OP_FINITE_SET_SIZE;
case OP_FINITE_SET_SUBSET: return Z3_OP_FINITE_SET_SUBSET;
case OP_FINITE_SET_MAP: return Z3_OP_FINITE_SET_MAP;
case OP_FINITE_SET_FILTER: return Z3_OP_FINITE_SET_FILTER;
case OP_FINITE_SET_RANGE: return Z3_OP_FINITE_SET_RANGE;
case OP_FINITE_SET_EXT: return Z3_OP_FINITE_SET_EXT;
case OP_FINITE_SET_MAP_INVERSE: return Z3_OP_FINITE_SET_MAP_INVERSE;
default: return Z3_OP_INTERNAL;
}
}
Z3_decl_kind Z3_API Z3_get_decl_kind(Z3_context c, Z3_func_decl d) {
Z3_TRY;
LOG_Z3_get_decl_kind(c, d);
RESET_ERROR_CODE();
func_decl* _d = to_func_decl(d);
if (d == nullptr || null_family_id == _d->get_family_id()) {
if (d == nullptr || null_family_id == _d->get_family_id())
return Z3_OP_UNINTERPRETED;
}
if (mk_c(c)->get_basic_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_TRUE: return Z3_OP_TRUE;
case OP_FALSE: return Z3_OP_FALSE;
case OP_EQ: return Z3_OP_EQ;
case OP_DISTINCT: return Z3_OP_DISTINCT;
case OP_ITE: return Z3_OP_ITE;
case OP_AND: return Z3_OP_AND;
case OP_OR: return Z3_OP_OR;
case OP_XOR: return Z3_OP_XOR;
case OP_NOT: return Z3_OP_NOT;
case OP_IMPLIES: return Z3_OP_IMPLIES;
case OP_OEQ: return Z3_OP_OEQ;
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;
case PR_ASSERTED: return Z3_OP_PR_ASSERTED;
case PR_GOAL: return Z3_OP_PR_GOAL;
case PR_MODUS_PONENS: return Z3_OP_PR_MODUS_PONENS;
case PR_REFLEXIVITY: return Z3_OP_PR_REFLEXIVITY;
case PR_SYMMETRY: return Z3_OP_PR_SYMMETRY;
case PR_TRANSITIVITY: return Z3_OP_PR_TRANSITIVITY;
case PR_TRANSITIVITY_STAR: return Z3_OP_PR_TRANSITIVITY_STAR;
case PR_MONOTONICITY: return Z3_OP_PR_MONOTONICITY;
case PR_QUANT_INTRO: return Z3_OP_PR_QUANT_INTRO;
case PR_BIND: return Z3_OP_PR_BIND;
case PR_DISTRIBUTIVITY: return Z3_OP_PR_DISTRIBUTIVITY;
case PR_AND_ELIM: return Z3_OP_PR_AND_ELIM;
case PR_NOT_OR_ELIM: return Z3_OP_PR_NOT_OR_ELIM;
case PR_REWRITE: return Z3_OP_PR_REWRITE;
case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
case PR_DER: return Z3_OP_PR_DER;
case PR_QUANT_INST: return Z3_OP_PR_QUANT_INST;
case PR_HYPOTHESIS: return Z3_OP_PR_HYPOTHESIS;
case PR_LEMMA: return Z3_OP_PR_LEMMA;
case PR_UNIT_RESOLUTION: return Z3_OP_PR_UNIT_RESOLUTION;
case PR_IFF_TRUE: return Z3_OP_PR_IFF_TRUE;
case PR_IFF_FALSE: return Z3_OP_PR_IFF_FALSE;
case PR_COMMUTATIVITY: return Z3_OP_PR_COMMUTATIVITY;
case PR_DEF_AXIOM: return Z3_OP_PR_DEF_AXIOM;
case PR_ASSUMPTION_ADD: return Z3_OP_PR_ASSUMPTION_ADD;
case PR_LEMMA_ADD: return Z3_OP_PR_LEMMA_ADD;
case PR_REDUNDANT_DEL: return Z3_OP_PR_REDUNDANT_DEL;
case PR_CLAUSE_TRAIL: return Z3_OP_PR_CLAUSE_TRAIL;
case PR_DEF_INTRO: return Z3_OP_PR_DEF_INTRO;
case PR_APPLY_DEF: return Z3_OP_PR_APPLY_DEF;
case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE;
case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_arith_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_NUM: return Z3_OP_ANUM;
case OP_IRRATIONAL_ALGEBRAIC_NUM: return Z3_OP_AGNUM;
case OP_LE: return Z3_OP_LE;
case OP_GE: return Z3_OP_GE;
case OP_LT: return Z3_OP_LT;
case OP_GT: return Z3_OP_GT;
case OP_ADD: return Z3_OP_ADD;
case OP_SUB: return Z3_OP_SUB;
case OP_UMINUS: return Z3_OP_UMINUS;
case OP_MUL: return Z3_OP_MUL;
case OP_DIV: return Z3_OP_DIV;
case OP_IDIV: return Z3_OP_IDIV;
case OP_REM: return Z3_OP_REM;
case OP_MOD: return Z3_OP_MOD;
case OP_POWER: return Z3_OP_POWER;
case OP_ABS: return Z3_OP_ABS;
case OP_TO_REAL: return Z3_OP_TO_REAL;
case OP_TO_INT: return Z3_OP_TO_INT;
case OP_IS_INT: return Z3_OP_IS_INT;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_array_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_STORE: return Z3_OP_STORE;
case OP_SELECT: return Z3_OP_SELECT;
case OP_CONST_ARRAY: return Z3_OP_CONST_ARRAY;
case OP_ARRAY_DEFAULT: return Z3_OP_ARRAY_DEFAULT;
case OP_ARRAY_MAP: return Z3_OP_ARRAY_MAP;
case OP_SET_UNION: return Z3_OP_SET_UNION;
case OP_SET_INTERSECT: return Z3_OP_SET_INTERSECT;
case OP_SET_DIFFERENCE: return Z3_OP_SET_DIFFERENCE;
case OP_SET_COMPLEMENT: return Z3_OP_SET_COMPLEMENT;
case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
default:
return Z3_OP_INTERNAL;
}
}
family_id fid = _d->get_family_id();
decl_kind k = _d->get_decl_kind();
if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO;
case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO;
case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC;
default: UNREACHABLE();
}
}
if (mk_c(c)->get_bv_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_BV_NUM: return Z3_OP_BNUM;
case OP_BIT1: return Z3_OP_BIT1;
case OP_BIT0: return Z3_OP_BIT0;
case OP_BNEG: return Z3_OP_BNEG;
case OP_BADD: return Z3_OP_BADD;
case OP_BSUB: return Z3_OP_BSUB;
case OP_BMUL: return Z3_OP_BMUL;
case OP_BSDIV: return Z3_OP_BSDIV;
case OP_BUDIV: return Z3_OP_BUDIV;
case OP_BSREM: return Z3_OP_BSREM;
case OP_BUREM: return Z3_OP_BUREM;
case OP_BSMOD: return Z3_OP_BSMOD;
case OP_BSDIV0: return Z3_OP_BSDIV0;
case OP_BUDIV0: return Z3_OP_BUDIV0;
case OP_BSREM0: return Z3_OP_BSREM0;
case OP_BUREM0: return Z3_OP_BUREM0;
case OP_BSMOD0: return Z3_OP_BSMOD0;
case OP_ULEQ: return Z3_OP_ULEQ;
case OP_SLEQ: return Z3_OP_SLEQ;
case OP_UGEQ: return Z3_OP_UGEQ;
case OP_SGEQ: return Z3_OP_SGEQ;
case OP_ULT: return Z3_OP_ULT;
case OP_SLT: return Z3_OP_SLT;
case OP_UGT: return Z3_OP_UGT;
case OP_SGT: return Z3_OP_SGT;
case OP_BAND: return Z3_OP_BAND;
case OP_BOR: return Z3_OP_BOR;
case OP_BNOT: return Z3_OP_BNOT;
case OP_BXOR: return Z3_OP_BXOR;
case OP_BNAND: return Z3_OP_BNAND;
case OP_BNOR: return Z3_OP_BNOR;
case OP_BXNOR: return Z3_OP_BXNOR;
case OP_CONCAT: return Z3_OP_CONCAT;
case OP_SIGN_EXT: return Z3_OP_SIGN_EXT;
case OP_ZERO_EXT: return Z3_OP_ZERO_EXT;
case OP_EXTRACT: return Z3_OP_EXTRACT;
case OP_REPEAT: return Z3_OP_REPEAT;
case OP_BREDOR: return Z3_OP_BREDOR;
case OP_BREDAND: return Z3_OP_BREDAND;
case OP_BCOMP: return Z3_OP_BCOMP;
case OP_BSHL: return Z3_OP_BSHL;
case OP_BLSHR: return Z3_OP_BLSHR;
case OP_BASHR: return Z3_OP_BASHR;
case OP_ROTATE_LEFT: return Z3_OP_ROTATE_LEFT;
case OP_ROTATE_RIGHT: return Z3_OP_ROTATE_RIGHT;
case OP_EXT_ROTATE_LEFT: return Z3_OP_EXT_ROTATE_LEFT;
case OP_EXT_ROTATE_RIGHT: return Z3_OP_EXT_ROTATE_RIGHT;
case OP_INT2BV: return Z3_OP_INT2BV;
case OP_UBV2INT: return Z3_OP_BV2INT;
case OP_SBV2INT: return Z3_OP_SBV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;
case OP_BUREM_I: return Z3_OP_BUREM_I;
case OP_BSMOD_I: return Z3_OP_BSMOD_I;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_dt_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR;
case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER;
case OP_DT_IS: return Z3_OP_DT_IS;
case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR;
case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_datalog_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case datalog::OP_RA_STORE: return Z3_OP_RA_STORE;
case datalog::OP_RA_EMPTY: return Z3_OP_RA_EMPTY;
case datalog::OP_RA_IS_EMPTY: return Z3_OP_RA_IS_EMPTY;
case datalog::OP_RA_JOIN: return Z3_OP_RA_JOIN;
case datalog::OP_RA_UNION: return Z3_OP_RA_UNION;
case datalog::OP_RA_WIDEN: return Z3_OP_RA_WIDEN;
case datalog::OP_RA_PROJECT: return Z3_OP_RA_PROJECT;
case datalog::OP_RA_FILTER: return Z3_OP_RA_FILTER;
case datalog::OP_RA_NEGATION_FILTER: return Z3_OP_RA_NEGATION_FILTER;
case datalog::OP_RA_RENAME: return Z3_OP_RA_RENAME;
case datalog::OP_RA_COMPLEMENT: return Z3_OP_RA_COMPLEMENT;
case datalog::OP_RA_SELECT: return Z3_OP_RA_SELECT;
case datalog::OP_RA_CLONE: return Z3_OP_RA_CLONE;
case datalog::OP_DL_CONSTANT: return Z3_OP_FD_CONSTANT;
case datalog::OP_DL_LT: return Z3_OP_FD_LT;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
case OP_SEQ_REPLACE_RE: return Z3_OP_SEQ_REPLACE_RE;
case OP_SEQ_REPLACE_RE_ALL: return Z3_OP_SEQ_REPLACE_RE_ALL;
case OP_SEQ_REPLACE_ALL: return Z3_OP_SEQ_REPLACE_ALL;
case OP_SEQ_AT: return Z3_OP_SEQ_AT;
case OP_SEQ_NTH: return Z3_OP_SEQ_NTH;
case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
case OP_SEQ_MAP: return Z3_OP_SEQ_MAP;
case OP_SEQ_MAPI: return Z3_OP_SEQ_MAPI;
case OP_SEQ_FOLDL: return Z3_OP_SEQ_FOLDL;
case OP_SEQ_FOLDLI: return Z3_OP_SEQ_FOLDLI;
case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
case _OP_REGEXP_FULL_CHAR: return Z3_OP_RE_FULL_SET;
case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
case OP_STRING_TO_CODE: return Z3_OP_STR_TO_CODE;
case OP_STRING_FROM_CODE: return Z3_OP_STR_FROM_CODE;
case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR;
case OP_STRING_LT: return Z3_OP_STRING_LT;
case OP_STRING_LE: return Z3_OP_STRING_LE;
case OP_RE_PLUS: return Z3_OP_RE_PLUS;
case OP_RE_STAR: return Z3_OP_RE_STAR;
case OP_RE_OPTION: return Z3_OP_RE_OPTION;
case OP_RE_RANGE: return Z3_OP_RE_RANGE;
case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
case OP_RE_UNION: return Z3_OP_RE_UNION;
case OP_RE_DIFF: return Z3_OP_RE_DIFF;
case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
case OP_RE_LOOP: return Z3_OP_RE_LOOP;
case OP_RE_POWER: return Z3_OP_RE_POWER;
case OP_RE_COMPLEMENT: return Z3_OP_RE_COMPLEMENT;
case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET;
case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_CHAR_SET;
case OP_RE_OF_PRED: return Z3_OP_RE_OF_PRED;
case OP_RE_REVERSE: return Z3_OP_RE_REVERSE;
case OP_RE_DERIVATIVE: return Z3_OP_RE_DERIVATIVE;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_char_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_CHAR_CONST: return Z3_OP_CHAR_CONST;
case OP_CHAR_LE: return Z3_OP_CHAR_LE;
case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT;
case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV;
case OP_CHAR_FROM_BV: return Z3_OP_CHAR_FROM_BV;
case OP_CHAR_IS_DIGIT: return Z3_OP_CHAR_IS_DIGIT;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;
case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY;
case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE;
case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE;
case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO;
case OP_FPA_NUM: return Z3_OP_FPA_NUM;
case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF;
case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF;
case OP_FPA_NAN: return Z3_OP_FPA_NAN;
case OP_FPA_MINUS_ZERO: return Z3_OP_FPA_MINUS_ZERO;
case OP_FPA_PLUS_ZERO: return Z3_OP_FPA_PLUS_ZERO;
case OP_FPA_ADD: return Z3_OP_FPA_ADD;
case OP_FPA_SUB: return Z3_OP_FPA_SUB;
case OP_FPA_NEG: return Z3_OP_FPA_NEG;
case OP_FPA_MUL: return Z3_OP_FPA_MUL;
case OP_FPA_DIV: return Z3_OP_FPA_DIV;
case OP_FPA_REM: return Z3_OP_FPA_REM;
case OP_FPA_ABS: return Z3_OP_FPA_ABS;
case OP_FPA_MIN: return Z3_OP_FPA_MIN;
case OP_FPA_MAX: return Z3_OP_FPA_MAX;
case OP_FPA_FMA: return Z3_OP_FPA_FMA;
case OP_FPA_SQRT: return Z3_OP_FPA_SQRT;
case OP_FPA_EQ: return Z3_OP_FPA_EQ;
case OP_FPA_ROUND_TO_INTEGRAL: return Z3_OP_FPA_ROUND_TO_INTEGRAL;
case OP_FPA_LT: return Z3_OP_FPA_LT;
case OP_FPA_GT: return Z3_OP_FPA_GT;
case OP_FPA_LE: return Z3_OP_FPA_LE;
case OP_FPA_GE: return Z3_OP_FPA_GE;
case OP_FPA_IS_NAN: return Z3_OP_FPA_IS_NAN;
case OP_FPA_IS_INF: return Z3_OP_FPA_IS_INF;
case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO;
case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL;
case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL;
case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE;
case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE;
case OP_FPA_FP: return Z3_OP_FPA_FP;
case OP_FPA_TO_FP: return Z3_OP_FPA_TO_FP;
case OP_FPA_TO_FP_UNSIGNED: return Z3_OP_FPA_TO_FP_UNSIGNED;
case OP_FPA_TO_UBV: return Z3_OP_FPA_TO_UBV;
case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV;
case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL;
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_BVWRAP: return Z3_OP_FPA_BVWRAP;
case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM;
return Z3_OP_UNINTERPRETED;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->m().get_label_family_id() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_LABEL: return Z3_OP_LABEL;
case OP_LABEL_LIT: return Z3_OP_LABEL_LIT;
default:
return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->get_pb_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_PB_LE: return Z3_OP_PB_LE;
case OP_PB_GE: return Z3_OP_PB_GE;
case OP_PB_EQ: return Z3_OP_PB_EQ;
case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
case OP_AT_LEAST_K: return Z3_OP_PB_AT_LEAST;
default: return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->fsutil().get_family_id() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_FINITE_SET_EMPTY: return Z3_OP_FINITE_SET_EMPTY;
case OP_FINITE_SET_SINGLETON: return Z3_OP_FINITE_SET_SINGLETON;
case OP_FINITE_SET_UNION: return Z3_OP_FINITE_SET_UNION;
case OP_FINITE_SET_INTERSECT: return Z3_OP_FINITE_SET_INTERSECT;
case OP_FINITE_SET_DIFFERENCE: return Z3_OP_FINITE_SET_DIFFERENCE;
case OP_FINITE_SET_IN: return Z3_OP_FINITE_SET_IN;
case OP_FINITE_SET_SIZE: return Z3_OP_FINITE_SET_SIZE;
case OP_FINITE_SET_SUBSET: return Z3_OP_FINITE_SET_SUBSET;
case OP_FINITE_SET_MAP: return Z3_OP_FINITE_SET_MAP;
case OP_FINITE_SET_FILTER: return Z3_OP_FINITE_SET_FILTER;
case OP_FINITE_SET_RANGE: return Z3_OP_FINITE_SET_RANGE;
case OP_FINITE_SET_EXT: return Z3_OP_FINITE_SET_EXT;
case OP_FINITE_SET_MAP_INVERSE: return Z3_OP_FINITE_SET_MAP_INVERSE;
default: return Z3_OP_INTERNAL;
}
}
if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
if (mk_c(c)->get_basic_fid() == fid)
return get_decl_kind_basic(k);
if (mk_c(c)->get_arith_fid() == fid)
return get_decl_kind_arith(k);
if (mk_c(c)->get_bv_fid() == fid)
return get_decl_kind_bv(k);
if (mk_c(c)->get_array_fid() == fid)
return get_decl_kind_array(k);
if (mk_c(c)->get_dt_fid() == fid)
return get_decl_kind_dt(k);
if (mk_c(c)->get_seq_fid() == fid)
return get_decl_kind_seq(k);
if (mk_c(c)->get_fpa_fid() == fid)
return get_decl_kind_fpa(k);
if (mk_c(c)->get_datalog_fid() == fid)
return get_decl_kind_datalog(k);
if (mk_c(c)->get_pb_fid() == fid)
return get_decl_kind_pb(k);
if (mk_c(c)->get_special_relations_fid() == fid)
return get_decl_kind_special_relations(k);
if (mk_c(c)->get_char_fid() == fid)
return get_decl_kind_char(k);
if (mk_c(c)->m().get_label_family_id() == fid)
return get_decl_kind_label(k);
if (mk_c(c)->fsutil().get_family_id() == fid)
return get_decl_kind_finite_set(k);
if (mk_c(c)->recfun().get_family_id() == fid)
return Z3_OP_RECURSIVE;
return Z3_OP_UNINTERPRETED;