Z3 |

Here is a list of all struct and union fields with links to the structures/unions they belong to:

### - i -

- Id : AST, FuncDecl, Sort
- id() : expr, func_decl, sort, UserPropagateBase
- IDecRefQueue() : IDecRefQueue< T extends Z3Object >
- implies : expr
- import_model_converter() : Solver
- ImportModelConverter() : Solver
- inconsistent() : Goal
- Inconsistent : Goal
- inconsistent() : goal, Goal
- Index : Expr
- index() : AlgebraicNumRef
- insert() : Fixedpoint, Goal, PropClosures, Solver
- Int : BitVecNum, FiniteDomainNum, FuncDecl.Parameter, IntNum, IntSymbol
- int2bv : expr
- Int64 : BitVecNum, FiniteDomainNum, IntNum
- int_const() : context
- int_sort() : context
- int_symbol() : context
- int_val() : context
- interrupt() : Context, Solver
- Interrupt() : Context
- interrupt() : context, Context
- IntSort : Context
- intToString() : Context
- IntToString() : Context
- is_algebraic() : expr
- is_and() : expr
- is_app() : expr
- is_arith() : expr, sort
- is_array() : expr, sort
- is_bool() : expr, sort, BoolSortRef
- is_bv() : expr, sort
- is_const() : expr, func_decl
- is_datatype() : expr, sort
- is_decided_sat() : goal
- is_decided_unsat() : goal
- is_distinct() : expr
- is_double() : stats
- is_eq() : expr
- is_exists() : expr, QuantifierRef
- is_false() : expr
- is_finite_domain() : expr, sort
- is_forall() : expr, QuantifierRef
- is_fpa() : expr, sort
- is_implies() : expr
- is_int() : expr, sort, ArithRef, ArithSortRef, BoolSortRef, RatNumRef
- is_int_value() : RatNumRef
- is_ite() : expr
- is_lambda() : expr, QuantifierRef
- is_not() : expr
- is_numeral() : expr
- is_numeral_i() : expr
- is_numeral_i64() : expr
- is_numeral_u() : expr
- is_numeral_u64() : expr
- is_or() : expr
- is_quantifier() : expr
- is_re() : expr, sort
- is_real() : expr, sort, ArithRef, ArithSortRef, RatNumRef
- is_relation() : expr, sort
- is_seq() : expr, sort
- is_string() : SeqRef, SeqSortRef
- is_string_value() : expr, SeqRef
- is_true() : expr
- is_uint() : stats
- is_var() : expr
- is_well_sorted() : expr
- is_xor() : expr
- isAdd() : Expr< R extends Sort >
- IsAdd : Expr
- isAlgebraicNumber() : Expr< R extends Sort >
- IsAlgebraicNumber : Expr
- isAnd() : Expr< R extends Sort >
- IsAnd : Expr
- isApp() : AST
- IsApp : AST
- isArithmeticNumeral() : Expr< R extends Sort >
- IsArithmeticNumeral : Expr
- isArray() : Expr< R extends Sort >
- IsArray : Expr
- isArrayMap() : Expr< R extends Sort >
- IsArrayMap : Expr
- isAsArray() : Expr< R extends Sort >
- IsAsArray : Expr
- IsAt : Expr
- IsAtLeast : Expr
- IsAtMost : Expr
- isBool() : Expr< R extends Sort >
- IsBool : Expr
- isBV() : Expr< R extends Sort >
- IsBV : Expr
- isBVAdd() : Expr< R extends Sort >
- IsBVAdd : Expr
- isBVAND() : Expr< R extends Sort >
- IsBVAND : Expr
- isBVBitOne() : Expr< R extends Sort >
- IsBVBitOne : Expr
- isBVBitZero() : Expr< R extends Sort >
- IsBVBitZero : Expr
- isBVCarry() : Expr< R extends Sort >
- IsBVCarry : Expr
- isBVComp() : Expr< R extends Sort >
- IsBVComp : Expr
- isBVConcat() : Expr< R extends Sort >
- IsBVConcat : Expr
- isBVExtract() : Expr< R extends Sort >
- IsBVExtract : Expr
- isBVMul() : Expr< R extends Sort >
- IsBVMul : Expr
- isBVNAND() : Expr< R extends Sort >
- IsBVNAND : Expr
- isBVNOR() : Expr< R extends Sort >
- IsBVNOR : Expr
- isBVNOT() : Expr< R extends Sort >
- IsBVNOT : Expr
- isBVNumeral() : Expr< R extends Sort >
- IsBVNumeral : Expr
- isBVOR() : Expr< R extends Sort >
- IsBVOR : Expr
- isBVReduceAND() : Expr< R extends Sort >
- IsBVReduceAND : Expr
- isBVReduceOR() : Expr< R extends Sort >
- IsBVReduceOR : Expr
- isBVRepeat() : Expr< R extends Sort >
- IsBVRepeat : Expr
- isBVRotateLeft() : Expr< R extends Sort >
- IsBVRotateLeft : Expr
- isBVRotateLeftExtended() : Expr< R extends Sort >
- IsBVRotateLeftExtended : Expr
- isBVRotateRight() : Expr< R extends Sort >
- IsBVRotateRight : Expr
- isBVRotateRightExtended() : Expr< R extends Sort >
- IsBVRotateRightExtended : Expr
- isBVSDiv() : Expr< R extends Sort >
- IsBVSDiv : Expr
- isBVSGE() : Expr< R extends Sort >
- IsBVSGE : Expr
- isBVSGT() : Expr< R extends Sort >
- IsBVSGT : Expr
- isBVShiftLeft() : Expr< R extends Sort >
- IsBVShiftLeft : Expr
- isBVShiftRightArithmetic() : Expr< R extends Sort >
- IsBVShiftRightArithmetic : Expr
- isBVShiftRightLogical() : Expr< R extends Sort >
- IsBVShiftRightLogical : Expr
- isBVSignExtension() : Expr< R extends Sort >
- IsBVSignExtension : Expr
- isBVSLE() : Expr< R extends Sort >
- IsBVSLE : Expr
- isBVSLT() : Expr< R extends Sort >
- IsBVSLT : Expr
- isBVSMod() : Expr< R extends Sort >
- IsBVSMod : Expr
- isBVSRem() : Expr< R extends Sort >
- IsBVSRem : Expr
- isBVSub() : Expr< R extends Sort >
- IsBVSub : Expr
- isBVToInt() : Expr< R extends Sort >
- IsBVToInt : Expr
- isBVUDiv() : Expr< R extends Sort >
- IsBVUDiv : Expr
- isBVUGE() : Expr< R extends Sort >
- IsBVUGE : Expr
- isBVUGT() : Expr< R extends Sort >
- IsBVUGT : Expr
- isBVULE() : Expr< R extends Sort >
- IsBVULE : Expr
- isBVULT() : Expr< R extends Sort >
- IsBVULT : Expr
- isBVUMinus() : Expr< R extends Sort >
- IsBVUMinus : Expr
- isBVURem() : Expr< R extends Sort >
- IsBVURem : Expr
- isBVXNOR() : Expr< R extends Sort >
- IsBVXNOR : Expr
- isBVXOR() : Expr< R extends Sort >
- IsBVXOR : Expr
- isBVXOR3() : Expr< R extends Sort >
- IsBVXOR3 : Expr
- isBVZeroExtension() : Expr< R extends Sort >
- IsBVZeroExtension : Expr
- isConcat() : Expr< R extends Sort >
- IsConcat : Expr
- IsConsDecl : ListSort
- isConst() : Expr< R extends Sort >
- IsConst : Expr
- isConstantArray() : Expr< R extends Sort >
- IsConstantArray : Expr
- IsContains : Expr
- isDecidedSat() : Goal
- IsDecidedSat : Goal
- isDecidedUnsat() : Goal
- IsDecidedUnsat : Goal
- isDefaultArray() : Expr< R extends Sort >
- IsDefaultArray : Expr
- isDistinct() : Expr< R extends Sort >
- IsDistinct : Expr
- isDiv() : Expr< R extends Sort >
- IsDiv : Expr
- isDouble() : Statistics.Entry
- IsDouble : Statistics.Entry
- isEmptyRelation() : Expr< R extends Sort >
- IsEmptyRelation : Expr
- isEq() : Expr< R extends Sort >
- IsEq : Expr
- isExistential() : Quantifier
- IsExistential : Quantifier
- isExpr() : AST
- IsExpr : AST
- IsExtract : Expr
- isFalse() : Expr< R extends Sort >
- IsFalse : Expr
- isFiniteDomain() : Expr< R extends Sort >
- IsFiniteDomain : Expr
- isFiniteDomainLT() : Expr< R extends Sort >
- IsFiniteDomainLT : Expr
- IsFP : Expr
- IsFPAbs : Expr
- IsFPAdd : Expr
- IsFPDiv : Expr
- IsFPEq : Expr
- IsFPFMA : Expr
- IsFPFP : Expr
- IsFPGe : Expr
- IsFPGt : Expr
- IsFPisInf : Expr
- IsFPisNaN : Expr
- IsFPisNegative : Expr
- IsFPisNormal : Expr
- IsFPisPositive : Expr
- IsFPisSubnormal : Expr
- IsFPisZero : Expr
- IsFPLe : Expr
- IsFPLt : Expr
- IsFPMax : Expr
- IsFPMin : Expr
- IsFPMinusInfinity : Expr
- IsFPMinusZero : Expr
- IsFPMul : Expr
- IsFPNaN : Expr
- IsFPNeg : Expr
- IsFPNumeral : Expr
- IsFPPlusInfinity : Expr
- IsFPPlusZero : Expr
- IsFPRem : Expr
- IsFPRM : Expr
- IsFPRMExpr : Expr
- IsFPRMExprRNA : Expr
- IsFPRMExprRNE : Expr
- IsFPRMExprRTN : Expr
- IsFPRMExprRTP : Expr
- IsFPRMExprRTZ : Expr
- IsFPRMNumeral : Expr
- IsFPRMRoundNearestTiesToAway : Expr
- IsFPRMRoundNearestTiesToEven : Expr
- IsFPRMRoundTowardNegative : Expr
- IsFPRMRoundTowardPositive : Expr
- IsFPRMRoundTowardZero : Expr
- IsFPRoundToIntegral : Expr
- IsFPSqrt : Expr
- IsFPSub : Expr
- IsFPToFp : Expr
- IsFPToFpUnsigned : Expr
- IsFPToIEEEBV : Expr
- IsFPToReal : Expr
- IsFPToSBV : Expr
- IsFPToUBV : Expr
- isFuncDecl() : AST
- IsFuncDecl : AST
- isGarbage() : Goal
- IsGarbage : Goal
- isGE() : Expr< R extends Sort >
- IsGE : Expr
- isGT() : Expr< R extends Sort >
- IsGT : Expr
- isIDiv() : Expr< R extends Sort >
- IsIDiv : Expr
- isIff() : Expr< R extends Sort >
- IsIff : Expr
- isImplies() : Expr< R extends Sort >
- IsImplies : Expr
- IsIndex : Expr
- isInf() : FPNum
- IsInf : FPNum
- isInf() : FPNumRef
- isInt() : Expr< R extends Sort >
- IsInt : Expr
- isIntNum() : Expr< R extends Sort >
- IsIntNum : Expr
- isIntSymbol() : Symbol
- IsIntSymbol() : Symbol
- isIntToBV() : Expr< R extends Sort >
- IsIntToBV : Expr
- isIntToReal() : Expr< R extends Sort >
- IsIntToReal : Expr
- isIsEmptyRelation() : Expr< R extends Sort >
- IsIsEmptyRelation : Expr
- isITE() : Expr< R extends Sort >
- IsITE : Expr
- isLabel() : Expr< R extends Sort >
- IsLabel : Expr
- isLabelLit() : Expr< R extends Sort >
- IsLabelLit : Expr
- isLE() : Expr< R extends Sort >
- IsLE : Expr
- IsLength : Expr
- isLT() : Expr< R extends Sort >
- IsLT : Expr
- isModulus() : Expr< R extends Sort >
- IsModulus : Expr
- isMul() : Expr< R extends Sort >
- IsMul : Expr
- isNaN() : FPNum
- IsNaN : FPNum
- isNaN() : FPNumRef
- isNegative() : FPNum
- IsNegative : FPNum
- isNegative() : FPNumRef
- IsNilDecl : ListSort
- isNormal() : FPNum
- IsNormal : FPNum
- isNormal() : FPNumRef
- isNot() : Expr< R extends Sort >
- IsNot : Expr
- isNumeral() : Expr< R extends Sort >
- IsNumeral : Expr
- isOEQ() : Expr< R extends Sort >
- IsOEQ : Expr
- isOpen() : Log
- isOr() : Expr< R extends Sort >
- IsOr : Expr
- isOverApproximation() : Goal
- IsOverApproximation : Goal
- IsPbEq : Expr
- IsPbGe : Expr
- IsPbLe : Expr
- isPositive() : FPNum
- IsPositive : FPNum
- isPositive() : FPNumRef
- isPrecise() : Goal
- IsPrecise : Goal
- IsPrefix : Expr
- isProofAndElimination() : Expr< R extends Sort >
- IsProofAndElimination : Expr
- isProofApplyDef() : Expr< R extends Sort >
- IsProofApplyDef : Expr
- isProofAsserted() : Expr< R extends Sort >
- IsProofAsserted : Expr
- isProofCommutativity() : Expr< R extends Sort >
- IsProofCommutativity : Expr
- isProofDefAxiom() : Expr< R extends Sort >
- IsProofDefAxiom : Expr
- isProofDefIntro() : Expr< R extends Sort >
- IsProofDefIntro : Expr
- isProofDER() : Expr< R extends Sort >
- IsProofDER : Expr
- isProofDistributivity() : Expr< R extends Sort >
- IsProofDistributivity : Expr
- isProofElimUnusedVars() : Expr< R extends Sort >
- IsProofElimUnusedVars : Expr
- isProofGoal() : Expr< R extends Sort >
- IsProofGoal : Expr
- isProofHypothesis() : Expr< R extends Sort >
- IsProofHypothesis : Expr
- isProofIFFFalse() : Expr< R extends Sort >
- IsProofIFFFalse : Expr
- isProofIFFOEQ() : Expr< R extends Sort >
- IsProofIFFOEQ : Expr
- isProofIFFTrue() : Expr< R extends Sort >
- IsProofIFFTrue : Expr
- isProofLemma() : Expr< R extends Sort >
- IsProofLemma : Expr
- isProofModusPonens() : Expr< R extends Sort >
- IsProofModusPonens : Expr
- isProofModusPonensOEQ() : Expr< R extends Sort >
- IsProofModusPonensOEQ : Expr
- isProofMonotonicity() : Expr< R extends Sort >
- IsProofMonotonicity : Expr
- isProofNNFNeg() : Expr< R extends Sort >
- IsProofNNFNeg : Expr
- isProofNNFPos() : Expr< R extends Sort >
- IsProofNNFPos : Expr
- isProofOrElimination() : Expr< R extends Sort >
- IsProofOrElimination : Expr
- isProofPullQuant() : Expr< R extends Sort >
- IsProofPullQuant : Expr
- isProofPushQuant() : Expr< R extends Sort >
- IsProofPushQuant : Expr
- isProofQuantInst() : Expr< R extends Sort >
- IsProofQuantInst : Expr
- isProofQuantIntro() : Expr< R extends Sort >
- IsProofQuantIntro : Expr
- isProofReflexivity() : Expr< R extends Sort >
- IsProofReflexivity : Expr
- isProofRewrite() : Expr< R extends Sort >
- IsProofRewrite : Expr
- isProofRewriteStar() : Expr< R extends Sort >
- IsProofRewriteStar : Expr
- isProofSkolemize() : Expr< R extends Sort >
- IsProofSkolemize : Expr
- isProofSymmetry() : Expr< R extends Sort >
- IsProofSymmetry : Expr
- isProofTheoryLemma() : Expr< R extends Sort >
- IsProofTheoryLemma : Expr
- isProofTransitivity() : Expr< R extends Sort >
- IsProofTransitivity : Expr
- isProofTransitivityStar() : Expr< R extends Sort >
- IsProofTransitivityStar : Expr
- isProofTrue() : Expr< R extends Sort >
- IsProofTrue : Expr
- isProofUnitResolution() : Expr< R extends Sort >
- IsProofUnitResolution : Expr
- isQuantifier() : AST
- IsQuantifier : AST
- isRatNum() : Expr< R extends Sort >
- IsRatNum : Expr
- isReal() : Expr< R extends Sort >
- IsReal : Expr
- isRealIsInt() : Expr< R extends Sort >
- IsRealIsInt : Expr
- isRealToInt() : Expr< R extends Sort >
- IsRealToInt : Expr
- isRelation() : Expr< R extends Sort >
- IsRelation : Expr
- isRelationalJoin() : Expr< R extends Sort >
- IsRelationalJoin : Expr
- isRelationClone() : Expr< R extends Sort >
- IsRelationClone : Expr
- isRelationComplement() : Expr< R extends Sort >
- IsRelationComplement : Expr
- isRelationFilter() : Expr< R extends Sort >
- IsRelationFilter : Expr
- isRelationNegationFilter() : Expr< R extends Sort >
- IsRelationNegationFilter : Expr
- isRelationProject() : Expr< R extends Sort >
- IsRelationProject : Expr
- isRelationRename() : Expr< R extends Sort >
- IsRelationRename : Expr
- isRelationSelect() : Expr< R extends Sort >
- IsRelationSelect : Expr
- isRelationStore() : Expr< R extends Sort >
- IsRelationStore : Expr
- isRelationUnion() : Expr< R extends Sort >
- IsRelationUnion : Expr
- isRelationWiden() : Expr< R extends Sort >
- IsRelationWiden : Expr
- isRemainder() : Expr< R extends Sort >
- IsRemainder : Expr
- IsReplace : Expr
- isRNA() : FPRMNum
- isRNE() : FPRMNum
- isRoundNearestTiesToAway() : FPRMNum
- isRoundNearestTiesToEven() : FPRMNum
- isRoundTowardNegative() : FPRMNum
- isRoundTowardPositive() : FPRMNum
- isRoundTowardZero() : FPRMNum
- isRTN() : FPRMNum
- isRTP() : FPRMNum
- isRTZ() : FPRMNum
- isSelect() : Expr< R extends Sort >
- IsSelect : Expr
- isSetComplement() : Expr< R extends Sort >
- IsSetComplement : Expr
- isSetDifference() : Expr< R extends Sort >
- IsSetDifference : Expr
- isSetIntersect() : Expr< R extends Sort >
- IsSetIntersect : Expr
- isSetSubset() : Expr< R extends Sort >
- IsSetSubset : Expr
- isSetUnion() : Expr< R extends Sort >
- IsSetUnion : Expr
- isSort() : AST
- IsSort : AST
- isStore() : Expr< R extends Sort >
- IsStore : Expr
- isString() : Expr< R extends Sort >
- IsString : Expr
- isStringSymbol() : Symbol
- IsStringSymbol() : Symbol
- isSub() : Expr< R extends Sort >
- IsSub : Expr
- isSubnormal() : FPNum
- IsSubnormal : FPNum
- isSubnormal() : FPNumRef
- IsSuffix : Expr
- isTrue() : Expr< R extends Sort >
- IsTrue : Expr
- isUInt() : Statistics.Entry
- IsUInt : Statistics.Entry
- isUMinus() : Expr< R extends Sort >
- IsUMinus : Expr
- isUnderApproximation() : Goal
- IsUnderApproximation : Goal
- isUniversal() : Quantifier
- IsUniversal : Quantifier
- isVar() : AST
- IsVar : AST
- isWellSorted() : Expr< R extends Sort >
- IsWellSorted : Expr
- isXor() : Expr< R extends Sort >
- IsXor : Expr
- isZero() : FPNum
- IsZero : FPNum
- isZero() : FPNumRef
- ite : expr
- iterator() : ast_vector_tpl< T >::iterator
- itos() : expr