Sequence expressions More...
Properties | |
Expr | this[Expr index] [get] |
Access the nth element of a sequence More... | |
Properties inherited from Expr | |
FuncDecl | FuncDecl [get] |
The function declaration of the function that is applied in this expression. More... | |
Z3_lbool | BoolValue [get] |
Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF). More... | |
uint | NumArgs [get] |
The number of arguments of the expression. More... | |
Expr[] | Args [get] |
The arguments of the expression. More... | |
bool | IsNumeral [get] |
Indicates whether the term is a numeral More... | |
bool | IsWellSorted [get] |
Indicates whether the term is well-sorted. More... | |
Sort | Sort [get] |
The Sort of the term. More... | |
bool | IsConst [get] |
Indicates whether the term represents a constant. More... | |
bool | IsIntNum [get] |
Indicates whether the term is an integer numeral. More... | |
bool | IsRatNum [get] |
Indicates whether the term is a real numeral. More... | |
bool | IsAlgebraicNumber [get] |
Indicates whether the term is an algebraic number More... | |
bool | IsBool [get] |
Indicates whether the term has Boolean sort. More... | |
bool | IsTrue [get] |
Indicates whether the term is the constant true. More... | |
bool | IsFalse [get] |
Indicates whether the term is the constant false. More... | |
bool | IsEq [get] |
Indicates whether the term is an equality predicate. More... | |
bool | IsDistinct [get] |
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). More... | |
bool | IsITE [get] |
Indicates whether the term is a ternary if-then-else term More... | |
bool | IsAnd [get] |
Indicates whether the term is an n-ary conjunction More... | |
bool | IsOr [get] |
Indicates whether the term is an n-ary disjunction More... | |
bool | IsIff [get] |
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) More... | |
bool | IsXor [get] |
Indicates whether the term is an exclusive or More... | |
bool | IsNot [get] |
Indicates whether the term is a negation More... | |
bool | IsImplies [get] |
Indicates whether the term is an implication More... | |
bool | IsAtMost [get] |
Indicates whether the term is at-most More... | |
uint | AtMostBound [get] |
Retrieve bound of at-most More... | |
bool | IsAtLeast [get] |
Indicates whether the term is at-least More... | |
uint | AtLeastBound [get] |
Retrieve bound of at-least More... | |
bool | IsPbEq [get] |
Indicates whether the term is pbeq More... | |
bool | IsPbLe [get] |
Indicates whether the term is pble More... | |
bool | IsPbGe [get] |
Indicates whether the term is pbge More... | |
bool | IsInt [get] |
Indicates whether the term is of integer sort. More... | |
bool | IsReal [get] |
Indicates whether the term is of sort real. More... | |
bool | IsArithmeticNumeral [get] |
Indicates whether the term is an arithmetic numeral. More... | |
bool | IsLE [get] |
Indicates whether the term is a less-than-or-equal More... | |
bool | IsGE [get] |
Indicates whether the term is a greater-than-or-equal More... | |
bool | IsLT [get] |
Indicates whether the term is a less-than More... | |
bool | IsGT [get] |
Indicates whether the term is a greater-than More... | |
bool | IsAdd [get] |
Indicates whether the term is addition (binary) More... | |
bool | IsSub [get] |
Indicates whether the term is subtraction (binary) More... | |
bool | IsUMinus [get] |
Indicates whether the term is a unary minus More... | |
bool | IsMul [get] |
Indicates whether the term is multiplication (binary) More... | |
bool | IsDiv [get] |
Indicates whether the term is division (binary) More... | |
bool | IsIDiv [get] |
Indicates whether the term is integer division (binary) More... | |
bool | IsRemainder [get] |
Indicates whether the term is remainder (binary) More... | |
bool | IsModulus [get] |
Indicates whether the term is modulus (binary) More... | |
bool | IsIntToReal [get] |
Indicates whether the term is a coercion of integer to real (unary) More... | |
bool | IsRealToInt [get] |
Indicates whether the term is a coercion of real to integer (unary) More... | |
bool | IsRealIsInt [get] |
Indicates whether the term is a check that tests whether a real is integral (unary) More... | |
bool | IsArray [get] |
Indicates whether the term is of an array sort. More... | |
bool | IsStore [get] |
Indicates whether the term is an array store. More... | |
bool | IsSelect [get] |
Indicates whether the term is an array select. More... | |
bool | IsConstantArray [get] |
Indicates whether the term is a constant array. More... | |
bool | IsDefaultArray [get] |
Indicates whether the term is a default array. More... | |
bool | IsArrayMap [get] |
Indicates whether the term is an array map. More... | |
bool | IsAsArray [get] |
Indicates whether the term is an as-array term. More... | |
bool | IsSetUnion [get] |
Indicates whether the term is set union More... | |
bool | IsSetIntersect [get] |
Indicates whether the term is set intersection More... | |
bool | IsSetDifference [get] |
Indicates whether the term is set difference More... | |
bool | IsSetComplement [get] |
Indicates whether the term is set complement More... | |
bool | IsSetSubset [get] |
Indicates whether the term is set subset More... | |
bool | IsBV [get] |
Indicates whether the terms is of bit-vector sort. More... | |
bool | IsBVNumeral [get] |
Indicates whether the term is a bit-vector numeral More... | |
bool | IsBVBitOne [get] |
Indicates whether the term is a one-bit bit-vector with value one More... | |
bool | IsBVBitZero [get] |
Indicates whether the term is a one-bit bit-vector with value zero More... | |
bool | IsBVUMinus [get] |
Indicates whether the term is a bit-vector unary minus More... | |
bool | IsBVAdd [get] |
Indicates whether the term is a bit-vector addition (binary) More... | |
bool | IsBVSub [get] |
Indicates whether the term is a bit-vector subtraction (binary) More... | |
bool | IsBVMul [get] |
Indicates whether the term is a bit-vector multiplication (binary) More... | |
bool | IsBVSDiv [get] |
Indicates whether the term is a bit-vector signed division (binary) More... | |
bool | IsBVUDiv [get] |
Indicates whether the term is a bit-vector unsigned division (binary) More... | |
bool | IsBVSRem [get] |
Indicates whether the term is a bit-vector signed remainder (binary) More... | |
bool | IsBVURem [get] |
Indicates whether the term is a bit-vector unsigned remainder (binary) More... | |
bool | IsBVSMod [get] |
Indicates whether the term is a bit-vector signed modulus More... | |
bool | IsBVULE [get] |
Indicates whether the term is an unsigned bit-vector less-than-or-equal More... | |
bool | IsBVSLE [get] |
Indicates whether the term is a signed bit-vector less-than-or-equal More... | |
bool | IsBVUGE [get] |
Indicates whether the term is an unsigned bit-vector greater-than-or-equal More... | |
bool | IsBVSGE [get] |
Indicates whether the term is a signed bit-vector greater-than-or-equal More... | |
bool | IsBVULT [get] |
Indicates whether the term is an unsigned bit-vector less-than More... | |
bool | IsBVSLT [get] |
Indicates whether the term is a signed bit-vector less-than More... | |
bool | IsBVUGT [get] |
Indicates whether the term is an unsigned bit-vector greater-than More... | |
bool | IsBVSGT [get] |
Indicates whether the term is a signed bit-vector greater-than More... | |
bool | IsBVAND [get] |
Indicates whether the term is a bit-wise AND More... | |
bool | IsBVOR [get] |
Indicates whether the term is a bit-wise OR More... | |
bool | IsBVNOT [get] |
Indicates whether the term is a bit-wise NOT More... | |
bool | IsBVXOR [get] |
Indicates whether the term is a bit-wise XOR More... | |
bool | IsBVNAND [get] |
Indicates whether the term is a bit-wise NAND More... | |
bool | IsBVNOR [get] |
Indicates whether the term is a bit-wise NOR More... | |
bool | IsBVXNOR [get] |
Indicates whether the term is a bit-wise XNOR More... | |
bool | IsBVConcat [get] |
Indicates whether the term is a bit-vector concatenation (binary) More... | |
bool | IsBVSignExtension [get] |
Indicates whether the term is a bit-vector sign extension More... | |
bool | IsBVZeroExtension [get] |
Indicates whether the term is a bit-vector zero extension More... | |
bool | IsBVExtract [get] |
Indicates whether the term is a bit-vector extraction More... | |
bool | IsBVRepeat [get] |
Indicates whether the term is a bit-vector repetition More... | |
bool | IsBVReduceOR [get] |
Indicates whether the term is a bit-vector reduce OR More... | |
bool | IsBVReduceAND [get] |
Indicates whether the term is a bit-vector reduce AND More... | |
bool | IsBVComp [get] |
Indicates whether the term is a bit-vector comparison More... | |
bool | IsBVShiftLeft [get] |
Indicates whether the term is a bit-vector shift left More... | |
bool | IsBVShiftRightLogical [get] |
Indicates whether the term is a bit-vector logical shift right More... | |
bool | IsBVShiftRightArithmetic [get] |
Indicates whether the term is a bit-vector arithmetic shift left More... | |
bool | IsBVRotateLeft [get] |
Indicates whether the term is a bit-vector rotate left More... | |
bool | IsBVRotateRight [get] |
Indicates whether the term is a bit-vector rotate right More... | |
bool | IsBVRotateLeftExtended [get] |
Indicates whether the term is a bit-vector rotate left (extended) More... | |
bool | IsBVRotateRightExtended [get] |
Indicates whether the term is a bit-vector rotate right (extended) More... | |
bool | IsIntToBV [get] |
Indicates whether the term is a coercion from integer to bit-vector More... | |
bool | IsBVToInt [get] |
Indicates whether the term is a coercion from bit-vector to integer More... | |
bool | IsBVCarry [get] |
Indicates whether the term is a bit-vector carry More... | |
bool | IsBVXOR3 [get] |
Indicates whether the term is a bit-vector ternary XOR More... | |
bool | IsLabel [get] |
Indicates whether the term is a label (used by the Boogie Verification condition generator). More... | |
bool | IsLabelLit [get] |
Indicates whether the term is a label literal (used by the Boogie Verification condition generator). More... | |
bool | IsString [get] |
Check whether expression is a string constant. More... | |
string | String [get] |
Retrieve string corresponding to string constant. More... | |
bool | IsConcat [get] |
Check whether expression is a concatenation. More... | |
bool | IsPrefix [get] |
Check whether expression is a prefix. More... | |
bool | IsSuffix [get] |
Check whether expression is a suffix. More... | |
bool | IsContains [get] |
Check whether expression is a contains. More... | |
bool | IsExtract [get] |
Check whether expression is an extract. More... | |
bool | IsReplace [get] |
Check whether expression is a replace. More... | |
bool | IsAt [get] |
Check whether expression is an at. More... | |
bool | IsLength [get] |
Check whether expression is a sequence length. More... | |
bool | IsIndex [get] |
Check whether expression is a sequence index. More... | |
bool | IsOEQ [get] |
Indicates whether the term is a binary equivalence modulo namings. More... | |
bool | IsProofTrue [get] |
Indicates whether the term is a Proof for the expression 'true'. More... | |
bool | IsProofAsserted [get] |
Indicates whether the term is a proof for a fact asserted by the user. More... | |
bool | IsProofGoal [get] |
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. More... | |
bool | IsProofModusPonens [get] |
Indicates whether the term is proof via modus ponens More... | |
bool | IsProofReflexivity [get] |
Indicates whether the term is a proof for (R t t), where R is a reflexive relation. More... | |
bool | IsProofSymmetry [get] |
Indicates whether the term is proof by symmetricity of a relation More... | |
bool | IsProofTransitivity [get] |
Indicates whether the term is a proof by transitivity of a relation More... | |
bool | IsProofTransitivityStar [get] |
Indicates whether the term is a proof by condensed transitivity of a relation More... | |
bool | IsProofMonotonicity [get] |
Indicates whether the term is a monotonicity proof object. More... | |
bool | IsProofQuantIntro [get] |
Indicates whether the term is a quant-intro proof More... | |
bool | IsProofDistributivity [get] |
Indicates whether the term is a distributivity proof object. More... | |
bool | IsProofAndElimination [get] |
Indicates whether the term is a proof by elimination of AND More... | |
bool | IsProofOrElimination [get] |
Indicates whether the term is a proof by elimination of not-or More... | |
bool | IsProofRewrite [get] |
Indicates whether the term is a proof by rewriting More... | |
bool | IsProofRewriteStar [get] |
Indicates whether the term is a proof by rewriting More... | |
bool | IsProofPullQuant [get] |
Indicates whether the term is a proof for pulling quantifiers out. More... | |
bool | IsProofPushQuant [get] |
Indicates whether the term is a proof for pushing quantifiers in. More... | |
bool | IsProofElimUnusedVars [get] |
Indicates whether the term is a proof for elimination of unused variables. More... | |
bool | IsProofDER [get] |
Indicates whether the term is a proof for destructive equality resolution More... | |
bool | IsProofQuantInst [get] |
Indicates whether the term is a proof for quantifier instantiation More... | |
bool | IsProofHypothesis [get] |
Indicates whether the term is a hypothesis marker. More... | |
bool | IsProofLemma [get] |
Indicates whether the term is a proof by lemma More... | |
bool | IsProofUnitResolution [get] |
Indicates whether the term is a proof by unit resolution More... | |
bool | IsProofIFFTrue [get] |
Indicates whether the term is a proof by iff-true More... | |
bool | IsProofIFFFalse [get] |
Indicates whether the term is a proof by iff-false More... | |
bool | IsProofCommutativity [get] |
Indicates whether the term is a proof by commutativity More... | |
bool | IsProofDefAxiom [get] |
Indicates whether the term is a proof for Tseitin-like axioms More... | |
bool | IsProofDefIntro [get] |
Indicates whether the term is a proof for introduction of a name More... | |
bool | IsProofApplyDef [get] |
Indicates whether the term is a proof for application of a definition More... | |
bool | IsProofIFFOEQ [get] |
Indicates whether the term is a proof iff-oeq More... | |
bool | IsProofNNFPos [get] |
Indicates whether the term is a proof for a positive NNF step More... | |
bool | IsProofNNFNeg [get] |
Indicates whether the term is a proof for a negative NNF step More... | |
bool | IsProofSkolemize [get] |
Indicates whether the term is a proof for a Skolemization step More... | |
bool | IsProofModusPonensOEQ [get] |
Indicates whether the term is a proof by modus ponens for equi-satisfiability. More... | |
bool | IsProofTheoryLemma [get] |
Indicates whether the term is a proof for theory lemma More... | |
bool | IsRelation [get] |
Indicates whether the term is of relation sort. More... | |
bool | IsRelationStore [get] |
Indicates whether the term is an relation store More... | |
bool | IsEmptyRelation [get] |
Indicates whether the term is an empty relation More... | |
bool | IsIsEmptyRelation [get] |
Indicates whether the term is a test for the emptiness of a relation More... | |
bool | IsRelationalJoin [get] |
Indicates whether the term is a relational join More... | |
bool | IsRelationUnion [get] |
Indicates whether the term is the union or convex hull of two relations. More... | |
bool | IsRelationWiden [get] |
Indicates whether the term is the widening of two relations More... | |
bool | IsRelationProject [get] |
Indicates whether the term is a projection of columns (provided as numbers in the parameters). More... | |
bool | IsRelationFilter [get] |
Indicates whether the term is a relation filter More... | |
bool | IsRelationNegationFilter [get] |
Indicates whether the term is an intersection of a relation with the negation of another. More... | |
bool | IsRelationRename [get] |
Indicates whether the term is the renaming of a column in a relation More... | |
bool | IsRelationComplement [get] |
Indicates whether the term is the complement of a relation More... | |
bool | IsRelationSelect [get] |
Indicates whether the term is a relational select More... | |
bool | IsRelationClone [get] |
Indicates whether the term is a relational clone (copy) More... | |
bool | IsFiniteDomain [get] |
Indicates whether the term is of an array sort. More... | |
bool | IsFiniteDomainLT [get] |
Indicates whether the term is a less than predicate over a finite domain. More... | |
bool | IsFP [get] |
Indicates whether the terms is of floating-point sort. More... | |
bool | IsFPRM [get] |
Indicates whether the terms is of floating-point rounding mode sort. More... | |
bool | IsFPNumeral [get] |
Indicates whether the term is a floating-point numeral More... | |
bool | IsFPRMNumeral [get] |
Indicates whether the term is a floating-point rounding mode numeral More... | |
bool | IsFPRMRoundNearestTiesToEven [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |
bool | IsFPRMRoundNearestTiesToAway [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |
bool | IsFPRMRoundTowardNegative [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |
bool | IsFPRMRoundTowardPositive [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |
bool | IsFPRMRoundTowardZero [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |
bool | IsFPRMExprRNE [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |
bool | IsFPRMExprRNA [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |
bool | IsFPRMExprRTN [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |
bool | IsFPRMExprRTP [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |
bool | IsFPRMExprRTZ [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |
bool | IsFPRMExpr [get] |
Indicates whether the term is a floating-point rounding mode numeral More... | |
bool | IsFPPlusInfinity [get] |
Indicates whether the term is a floating-point +oo More... | |
bool | IsFPMinusInfinity [get] |
Indicates whether the term is a floating-point -oo More... | |
bool | IsFPNaN [get] |
Indicates whether the term is a floating-point NaN More... | |
bool | IsFPPlusZero [get] |
bool | IsFPMinusZero [get] |
Indicates whether the term is a floating-point -zero More... | |
bool | IsFPAdd [get] |
Indicates whether the term is a floating-point addition term More... | |
bool | IsFPSub [get] |
Indicates whether the term is a floating-point subtraction term More... | |
bool | IsFPNeg [get] |
Indicates whether the term is a floating-point negation term More... | |
bool | IsFPMul [get] |
Indicates whether the term is a floating-point multiplication term More... | |
bool | IsFPDiv [get] |
Indicates whether the term is a floating-point division term More... | |
bool | IsFPRem [get] |
Indicates whether the term is a floating-point remainder term More... | |
bool | IsFPAbs [get] |
Indicates whether the term is a floating-point term absolute value term More... | |
bool | IsFPMin [get] |
Indicates whether the term is a floating-point minimum term More... | |
bool | IsFPMax [get] |
Indicates whether the term is a floating-point maximum term More... | |
bool | IsFPFMA [get] |
Indicates whether the term is a floating-point fused multiply-add term More... | |
bool | IsFPSqrt [get] |
Indicates whether the term is a floating-point square root term More... | |
bool | IsFPRoundToIntegral [get] |
Indicates whether the term is a floating-point roundToIntegral term More... | |
bool | IsFPEq [get] |
Indicates whether the term is a floating-point equality term More... | |
bool | IsFPLt [get] |
Indicates whether the term is a floating-point less-than term More... | |
bool | IsFPGt [get] |
Indicates whether the term is a floating-point greater-than term More... | |
bool | IsFPLe [get] |
Indicates whether the term is a floating-point less-than or equal term More... | |
bool | IsFPGe [get] |
Indicates whether the term is a floating-point greater-than or equal term More... | |
bool | IsFPisNaN [get] |
Indicates whether the term is a floating-point isNaN predicate term More... | |
bool | IsFPisInf [get] |
Indicates whether the term is a floating-point isInf predicate term More... | |
bool | IsFPisZero [get] |
Indicates whether the term is a floating-point isZero predicate term More... | |
bool | IsFPisNormal [get] |
Indicates whether the term is a floating-point isNormal term More... | |
bool | IsFPisSubnormal [get] |
Indicates whether the term is a floating-point isSubnormal predicate term More... | |
bool | IsFPisNegative [get] |
Indicates whether the term is a floating-point isNegative predicate term More... | |
bool | IsFPisPositive [get] |
Indicates whether the term is a floating-point isPositive predicate term More... | |
bool | IsFPFP [get] |
Indicates whether the term is a floating-point constructor term More... | |
bool | IsFPToFp [get] |
Indicates whether the term is a floating-point conversion term More... | |
bool | IsFPToFpUnsigned [get] |
Indicates whether the term is a floating-point conversion from unsigned bit-vector term More... | |
bool | IsFPToUBV [get] |
Indicates whether the term is a floating-point conversion to unsigned bit-vector term More... | |
bool | IsFPToSBV [get] |
Indicates whether the term is a floating-point conversion to signed bit-vector term More... | |
bool | IsFPToReal [get] |
Indicates whether the term is a floating-point conversion to real term More... | |
bool | IsFPToIEEEBV [get] |
Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term More... | |
uint | Index [get] |
The de-Bruijn index of a bound variable. More... | |
Properties inherited from AST | |
uint | Id [get] |
A unique identifier for the AST (unique among all ASTs). More... | |
Z3_ast_kind | ASTKind [get] |
The kind of the AST. More... | |
bool | IsExpr [get] |
Indicates whether the AST is an Expr More... | |
bool | IsApp [get] |
Indicates whether the AST is an application More... | |
bool | IsVar [get] |
Indicates whether the AST is a BoundVariable More... | |
bool | IsQuantifier [get] |
Indicates whether the AST is a Quantifier More... | |
bool | IsSort [get] |
Indicates whether the AST is a Sort More... | |
bool | IsFuncDecl [get] |
Indicates whether the AST is a FunctionDeclaration More... | |
Properties inherited from Z3Object | |
Context | Context [get] |
Access Context object More... | |
Additional Inherited Members | |
Public Member Functions inherited from Expr | |
Expr | Simplify (Params p=null) |
Returns a simplified version of the expression. More... | |
Expr | Arg (uint i) |
The i'th argument of the expression. More... | |
void | Update (Expr[] args) |
Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments. More... | |
Expr | Substitute (Expr[] from, Expr[] to) |
Substitute every occurrence of from[i] in the expression with to[i] , for i smaller than num_exprs . More... | |
Expr | Substitute (Expr from, Expr to) |
Substitute every occurrence of from in the expression with to . More... | |
Expr | SubstituteVars (Expr[] to) |
Substitute the free variables in the expression with the expressions in to More... | |
new Expr | Translate (Context ctx) |
Translates (copies) the term to the Context ctx . More... | |
Expr | Dup () |
Create a duplicate of expression. This feature is to allow extending the life-time of expressions that were passed down as arguments by the user propagator callbacks. By default the life-time of arguments to callbacks is within the callback only. More... | |
override string | ToString () |
Returns a string representation of the expression. More... | |
Public Member Functions inherited from AST | |
override bool | Equals (object o) |
Object comparison. More... | |
virtual int | CompareTo (object other) |
Object Comparison. More... | |
override int | GetHashCode () |
The AST's hash code. More... | |
AST | Translate (Context ctx) |
Translates (copies) the AST to the Context ctx . More... | |
override string | ToString () |
A string representation of the AST. More... | |
string | SExpr () |
A string representation of the AST in s-expression notation. More... | |
Public Member Functions inherited from Z3Object | |
void | Dispose () |
Disposes of the underlying native Z3 object. More... | |
Static Public Member Functions inherited from AST | |
static bool | operator== (AST a, AST b) |
Comparison operator. More... | |
static bool | operator!= (AST a, AST b) |
Comparison operator. More... | |
Protected Member Functions inherited from Expr | |
Expr (Context ctx, IntPtr obj) | |
Constructor for Expr More... | |
Sequence expressions
Definition at line 31 of file SeqExpr.cs.
Access the nth element of a sequence
Definition at line 43 of file SeqExpr.cs.