Z3 |

Public Member Functions | Protected Member Functions | Properties
Expr Class Reference

Expressions are terms. More...

Inheritance diagram for Expr:

## Public Member Functions
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...
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...

## Protected Member Functions
| Expr (Context ctx, IntPtr obj)
| Constructor for Expr More...

## Properties
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...

## Additional Inherited Members
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...

## Detailed Description

Expressions are terms.

Definition at line 30 of file Expr.cs.

## Constructor & Destructor Documentation

## ◆ Expr()

Expr | ( | Context | ctx,
|  | IntPtr | obj
| ) |  |
| inline protected

Constructor for Expr

Definition at line 1821 of file Expr.cs.

1821: base(ctx, obj) { Debug.Assert(ctx != null); }

## Member Function Documentation

## ◆ Arg()

Expr Arg | ( | uint | i | ) |
| inline

The i'th argument of the expression.

Definition at line 93 of file Expr.cs.

94 {
95 return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
96 }
Microsoft.Z3.Expr.Expr
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1821

## ◆ Simplify()

Expr Simplify | ( | Params | p = `null` | ) |
| inline

Returns a simplified version of the expression.

Parameters

  p | A set of parameters to configure the simplifier

See also
  Context.SimplifyHelp

Definition at line 37 of file Expr.cs.

38 {
39
40 if (p == null)
41 return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject));
42 else
43 return Expr.Create(Context, Native.Z3_simplify_ex(Context.nCtx, NativeObject, p.NativeObject));
44 }

## ◆ Substitute() [1/2]

Expr Substitute | ( | Expr | from,
|  | Expr | to
| ) |  |
| inline

Substitute every occurrence of `from` in the expression with `to`.

See also
  Substitute(Expr[],Expr[])

Definition at line 139 of file Expr.cs.

140 {
141 Debug.Assert(from != null);
142 Debug.Assert(to != null);
143
144 return Substitute(new Expr[] { from }, new Expr[] { to });
145 }
Microsoft.Z3.Expr.Substitute
Expr Substitute(Expr[] from, Expr[] to)
Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
Definition: Expr.cs:121

## ◆ Substitute() [2/2]

Expr Substitute | ( | Expr[] | from,
|  | Expr[] | to
| ) |  |
| inline

Substitute every occurrence of `from[i]` in the expression with `to[i]`, for `i` smaller than `num_exprs`.

The result is the new expression. The arrays `from` and `to` must have size `num_exprs`. For every `i` smaller than `num_exprs`, we must have that sort of `from[i]` must be equal to sort of `to[i]`.

Definition at line 121 of file Expr.cs.

122 {
123 Debug.Assert(from != null);
124 Debug.Assert(to != null);
125 Debug.Assert(from.All(f => f != null));
126 Debug.Assert(to.All(t => t != null));
127
128 Context.CheckContextMatch<Expr>(from);
129 Context.CheckContextMatch<Expr>(to);
130 if (from.Length != to.Length)
131 throw new Z3Exception("Argument sizes do not match");
132 return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
133 }

Referenced by Expr.Substitute().

## ◆ SubstituteVars()

Expr SubstituteVars | ( | Expr[] | to | ) |
| inline

Substitute the free variables in the expression with the expressions in to

For every `i` smaller than `num_exprs`, the variable with de-Bruijn index `i` is replaced with term `to[i]`.

Definition at line 153 of file Expr.cs.

154 {
155 Debug.Assert(to != null);
156 Debug.Assert(to.All(t => t != null));
157
158 Context.CheckContextMatch<Expr>(to);
159 return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
160 }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

Returns a string representation of the expression.

Definition at line 175 of file Expr.cs.

176 {
177 return base.ToString();
178 }

## ◆ Translate()

new Expr Translate | ( | Context | ctx | ) |
| inline

Translates (copies) the term to the Context ctx .

Parameters

  ctx | A context

Returns
  A copy of the term which is associated with ctx

Definition at line 167 of file Expr.cs.

168 {
169 return (Expr)base.Translate(ctx);
170 }

Referenced by Expr.Translate().

## ◆ Update()

void Update | ( | Expr[] | args | ) |
| inline

Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments.

Definition at line 102 of file Expr.cs.

103 {
104 Debug.Assert(args != null);
105 Debug.Assert(args.All(a => a != null));
106
107 Context.CheckContextMatch<Expr>(args);
108 if (IsApp && args.Length != NumArgs)
109 throw new Z3Exception("Number of arguments does not match");
110 NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
111 }
Microsoft.Z3.AST.IsApp
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:154
Microsoft.Z3.Expr.NumArgs
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:70

## Property Documentation

## ◆ Args

Expr [] Args
| get

The arguments of the expression.

Definition at line 77 of file Expr.cs.

78 {
79 get
80 {
81
82 uint n = NumArgs;
83 Expr[] res = new Expr[n];
84 for (uint i = 0; i < n; i++)
85 res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
86 return res;
87 }
88 }

## ◆ AtLeastBound

uint AtLeastBound
| get

Retrieve bound of at-least

Definition at line 338 of file Expr.cs.

338{ get { Debug.Assert(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }
Microsoft.Z3.Expr.IsAtLeast
bool IsAtLeast
Indicates whether the term is at-least
Definition: Expr.cs:333
Microsoft.Z3.Expr.FuncDecl
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Microsoft.Z3.FuncDecl.Parameter.Int
int Int
The int value of the parameter.
Definition: FuncDecl.cs:219
Microsoft.Z3.FuncDecl.Parameters
Parameter[] Parameters
The parameters of the function declaration
Definition: FuncDecl.cs:164

## ◆ AtMostBound

uint AtMostBound
| get

Retrieve bound of at-most

Definition at line 328 of file Expr.cs.

328{ get { Debug.Assert(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }
Microsoft.Z3.Expr.IsAtMost
bool IsAtMost
Indicates whether the term is at-most
Definition: Expr.cs:323

## ◆ BoolValue

Z3_lbool BoolValue
| get

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).

Definition at line 61 of file Expr.cs.

62 {
63 get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
64 }
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ FuncDecl

FuncDecl FuncDecl
| get

The function declaration of the function that is applied in this expression.

Definition at line 49 of file Expr.cs.

50 {
51 get
52 {
53 return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
54 }
55 }

Referenced by Model.ConstInterp().

## ◆ Index

uint Index
| get

The de-Bruijn index of a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
z3::forall
expr forall(expr const &x, expr const &b)
Definition: z3++.h:2189
z3::abs
expr abs(expr const &a)
Definition: z3++.h:1863

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Definition at line 1805 of file Expr.cs.

1806 {
1807 get
1808 {
1809 if (!IsVar)
1810 throw new Z3Exception("Term is not a bound variable.");
1811
1812 return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1813 }
1814 }
Microsoft.Z3.AST.IsVar
bool IsVar
Indicates whether the AST is a BoundVariable
Definition: AST.cs:162

## ◆ IsAdd

bool IsAdd
| get

Indicates whether the term is addition (binary)

Definition at line 402 of file Expr.cs.

402{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
Microsoft.Z3.FuncDecl.DeclKind
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:137
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000

## ◆ IsAlgebraicNumber

bool IsAlgebraicNumber
| get

Indicates whether the term is an algebraic number

Definition at line 242 of file Expr.cs.

243 {
244 get { return 0 != Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
245 }

## ◆ IsAnd

bool IsAnd
| get

Indicates whether the term is an n-ary conjunction

Definition at line 293 of file Expr.cs.

293{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }

## ◆ IsArithmeticNumeral

bool IsArithmeticNumeral
| get

Indicates whether the term is an arithmetic numeral.

Definition at line 377 of file Expr.cs.

377{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }

## ◆ IsArray

bool IsArray
| get

Indicates whether the term is of an array sort.

Definition at line 459 of file Expr.cs.

460 {
461 get
462 {
463 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
464 (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
465 == Z3_sort_kind.Z3_ARRAY_SORT);
466 }
467 }
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150

## ◆ IsArrayMap

bool IsArrayMap
| get

Indicates whether the term is an array map.

It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.

Definition at line 497 of file Expr.cs.

497{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }

## ◆ IsAsArray

bool IsAsArray
| get

Indicates whether the term is an as-array term.

An as-array term is n array value that behaves as the function graph of the function passed as parameter.

Definition at line 504 of file Expr.cs.

504{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }

## ◆ IsAt

bool IsAt
| get

Check whether expression is an at.

Returns
  a Boolean

Definition at line 877 of file Expr.cs.

877{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }

## ◆ IsAtLeast

bool IsAtLeast
| get

Indicates whether the term is at-least

Definition at line 333 of file Expr.cs.

333{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_LEAST; } }

## ◆ IsAtMost

bool IsAtMost
| get

Indicates whether the term is at-most

Definition at line 323 of file Expr.cs.

323{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_MOST; } }

## ◆ IsBool

bool IsBool
| get

Indicates whether the term has Boolean sort.

Definition at line 254 of file Expr.cs.

255 {
256 get
257 {
258 return (IsExpr &&
259 Native.Z3_is_eq_sort(Context.nCtx,
260 Native.Z3_mk_bool_sort(Context.nCtx),
261 Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
262 }
263 }
Microsoft.Z3.AST.IsExpr
bool IsExpr
Indicates whether the AST is an Expr
Definition: AST.cs:136

## ◆ IsBV

bool IsBV
| get

Indicates whether the terms is of bit-vector sort.

Definition at line 538 of file Expr.cs.

539 {
540 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
541 }

## ◆ IsBVAdd

bool IsBVAdd
| get

Indicates whether the term is a bit-vector addition (binary)

Definition at line 566 of file Expr.cs.

566{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }

## ◆ IsBVAND

bool IsBVAND
| get

Indicates whether the term is a bit-wise AND

Definition at line 671 of file Expr.cs.

671{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }

## ◆ IsBVBitOne

bool IsBVBitOne
| get

Indicates whether the term is a one-bit bit-vector with value one

Definition at line 551 of file Expr.cs.

551{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }

## ◆ IsBVBitZero

bool IsBVBitZero
| get

Indicates whether the term is a one-bit bit-vector with value zero

Definition at line 556 of file Expr.cs.

556{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }

## ◆ IsBVCarry

bool IsBVCarry
| get

Indicates whether the term is a bit-vector carry

Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

Definition at line 799 of file Expr.cs.

799{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }

## ◆ IsBVComp

bool IsBVComp
| get

Indicates whether the term is a bit-vector comparison

Definition at line 741 of file Expr.cs.

741{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }

## ◆ IsBVConcat

bool IsBVConcat
| get

Indicates whether the term is a bit-vector concatenation (binary)

Definition at line 706 of file Expr.cs.

706{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }

## ◆ IsBVExtract

bool IsBVExtract
| get

Indicates whether the term is a bit-vector extraction

Definition at line 721 of file Expr.cs.

721{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }

## ◆ IsBVMul

bool IsBVMul
| get

Indicates whether the term is a bit-vector multiplication (binary)

Definition at line 576 of file Expr.cs.

576{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }

## ◆ IsBVNAND

bool IsBVNAND
| get

Indicates whether the term is a bit-wise NAND

Definition at line 691 of file Expr.cs.

691{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }

## ◆ IsBVNOR

bool IsBVNOR
| get

Indicates whether the term is a bit-wise NOR

Definition at line 696 of file Expr.cs.

696{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }

## ◆ IsBVNOT

bool IsBVNOT
| get

Indicates whether the term is a bit-wise NOT

Definition at line 681 of file Expr.cs.

681{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }

## ◆ IsBVNumeral

bool IsBVNumeral
| get

Indicates whether the term is a bit-vector numeral

Definition at line 546 of file Expr.cs.

546{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }

## ◆ IsBVOR

bool IsBVOR
| get

Indicates whether the term is a bit-wise OR

Definition at line 676 of file Expr.cs.

676{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }

## ◆ IsBVReduceAND

bool IsBVReduceAND
| get

Indicates whether the term is a bit-vector reduce AND

Definition at line 736 of file Expr.cs.

736{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }

## ◆ IsBVReduceOR

bool IsBVReduceOR
| get

Indicates whether the term is a bit-vector reduce OR

Definition at line 731 of file Expr.cs.

731{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }

## ◆ IsBVRepeat

bool IsBVRepeat
| get

Indicates whether the term is a bit-vector repetition

Definition at line 726 of file Expr.cs.

726{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }

## ◆ IsBVRotateLeft

bool IsBVRotateLeft
| get

Indicates whether the term is a bit-vector rotate left

Definition at line 761 of file Expr.cs.

761{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }

## ◆ IsBVRotateLeftExtended

bool IsBVRotateLeftExtended
| get

Indicates whether the term is a bit-vector rotate left (extended)

Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Definition at line 772 of file Expr.cs.

772{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }

## ◆ IsBVRotateRight

bool IsBVRotateRight
| get

Indicates whether the term is a bit-vector rotate right

Definition at line 766 of file Expr.cs.

766{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }

## ◆ IsBVRotateRightExtended

bool IsBVRotateRightExtended
| get

Indicates whether the term is a bit-vector rotate right (extended)

Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Definition at line 778 of file Expr.cs.

778{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }

## ◆ IsBVSDiv

bool IsBVSDiv
| get

Indicates whether the term is a bit-vector signed division (binary)

Definition at line 581 of file Expr.cs.

581{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }

## ◆ IsBVSGE

bool IsBVSGE
| get

Indicates whether the term is a signed bit-vector greater-than-or-equal

Definition at line 646 of file Expr.cs.

646{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }

## ◆ IsBVSGT

bool IsBVSGT
| get

Indicates whether the term is a signed bit-vector greater-than

Definition at line 666 of file Expr.cs.

666{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }

## ◆ IsBVShiftLeft

bool IsBVShiftLeft
| get

Indicates whether the term is a bit-vector shift left

Definition at line 746 of file Expr.cs.

746{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }

## ◆ IsBVShiftRightArithmetic

bool IsBVShiftRightArithmetic
| get

Indicates whether the term is a bit-vector arithmetic shift left

Definition at line 756 of file Expr.cs.

756{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }

## ◆ IsBVShiftRightLogical

bool IsBVShiftRightLogical
| get

Indicates whether the term is a bit-vector logical shift right

Definition at line 751 of file Expr.cs.

751{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }

## ◆ IsBVSignExtension

bool IsBVSignExtension
| get

Indicates whether the term is a bit-vector sign extension

Definition at line 711 of file Expr.cs.

711{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }

## ◆ IsBVSLE

bool IsBVSLE
| get

Indicates whether the term is a signed bit-vector less-than-or-equal

Definition at line 636 of file Expr.cs.

636{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }

## ◆ IsBVSLT

bool IsBVSLT
| get

Indicates whether the term is a signed bit-vector less-than

Definition at line 656 of file Expr.cs.

656{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }

## ◆ IsBVSMod

bool IsBVSMod
| get

Indicates whether the term is a bit-vector signed modulus

Definition at line 601 of file Expr.cs.

601{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }

## ◆ IsBVSRem

bool IsBVSRem
| get

Indicates whether the term is a bit-vector signed remainder (binary)

Definition at line 591 of file Expr.cs.

591{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }

## ◆ IsBVSub

bool IsBVSub
| get

Indicates whether the term is a bit-vector subtraction (binary)

Definition at line 571 of file Expr.cs.

571{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }

## ◆ IsBVToInt

bool IsBVToInt
| get

Indicates whether the term is a coercion from bit-vector to integer

This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

Definition at line 792 of file Expr.cs.

792{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }

## ◆ IsBVUDiv

bool IsBVUDiv
| get

Indicates whether the term is a bit-vector unsigned division (binary)

Definition at line 586 of file Expr.cs.

586{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }

## ◆ IsBVUGE

bool IsBVUGE
| get

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

Definition at line 641 of file Expr.cs.

641{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }

## ◆ IsBVUGT

bool IsBVUGT
| get

Indicates whether the term is an unsigned bit-vector greater-than

Definition at line 661 of file Expr.cs.

661{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }

## ◆ IsBVULE

bool IsBVULE
| get

Indicates whether the term is an unsigned bit-vector less-than-or-equal

Definition at line 631 of file Expr.cs.

631{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }

## ◆ IsBVULT

bool IsBVULT
| get

Indicates whether the term is an unsigned bit-vector less-than

Definition at line 651 of file Expr.cs.

651{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }

## ◆ IsBVUMinus

bool IsBVUMinus
| get

Indicates whether the term is a bit-vector unary minus

Definition at line 561 of file Expr.cs.

561{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }

## ◆ IsBVURem

bool IsBVURem
| get

Indicates whether the term is a bit-vector unsigned remainder (binary)

Definition at line 596 of file Expr.cs.

596{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }

## ◆ IsBVXNOR

bool IsBVXNOR
| get

Indicates whether the term is a bit-wise XNOR

Definition at line 701 of file Expr.cs.

701{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }

## ◆ IsBVXOR

bool IsBVXOR
| get

Indicates whether the term is a bit-wise XOR

Definition at line 686 of file Expr.cs.

686{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }

## ◆ IsBVXOR3

bool IsBVXOR3
| get

Indicates whether the term is a bit-vector ternary XOR

The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)

Definition at line 805 of file Expr.cs.

805{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }

## ◆ IsBVZeroExtension

bool IsBVZeroExtension
| get

Indicates whether the term is a bit-vector zero extension

Definition at line 716 of file Expr.cs.

716{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }

## ◆ IsConcat

bool IsConcat
| get

Check whether expression is a concatenation.

Returns
  a Boolean

Definition at line 841 of file Expr.cs.

841{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }

## ◆ IsConst

bool IsConst
| get

Indicates whether the term represents a constant.

Definition at line 212 of file Expr.cs.

213 {
214 get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
215 }
Microsoft.Z3.FuncDecl.DomainSize
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101

## ◆ IsConstantArray

bool IsConstantArray
| get

Indicates whether the term is a constant array.

For example, select(const(v),i) = v holds for every v and i. The function is unary.

Definition at line 485 of file Expr.cs.

485{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }

## ◆ IsContains

bool IsContains
| get

Check whether expression is a contains.

Returns
  a Boolean

Definition at line 859 of file Expr.cs.

859{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }

## ◆ IsDefaultArray

bool IsDefaultArray
| get

Indicates whether the term is a default array.

For example default(const(v)) = v. The function is unary.

Definition at line 491 of file Expr.cs.

491{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }

## ◆ IsDistinct

bool IsDistinct
| get

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).

Definition at line 283 of file Expr.cs.

283{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }

## ◆ IsDiv

bool IsDiv
| get

Indicates whether the term is division (binary)

Definition at line 422 of file Expr.cs.

422{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }

## ◆ IsEmptyRelation

bool IsEmptyRelation
| get

Indicates whether the term is an empty relation

Definition at line 1395 of file Expr.cs.

1395{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }

## ◆ IsEq

bool IsEq
| get

Indicates whether the term is an equality predicate.

Definition at line 278 of file Expr.cs.

278{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }

## ◆ IsExtract

bool IsExtract
| get

Check whether expression is an extract.

Returns
  a Boolean

Definition at line 865 of file Expr.cs.

865{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }

## ◆ IsFalse

bool IsFalse
| get

Indicates whether the term is the constant false.

Definition at line 273 of file Expr.cs.

273{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }

## ◆ IsFiniteDomain

bool IsFiniteDomain
| get

Indicates whether the term is of an array sort.

Definition at line 1494 of file Expr.cs.

1495 {
1496 get
1497 {
1498 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1499 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1500 }
1501 }

## ◆ IsFiniteDomainLT

bool IsFiniteDomainLT
| get

Indicates whether the term is a less than predicate over a finite domain.

Definition at line 1506 of file Expr.cs.

1506{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }

## ◆ IsFP

bool IsFP
| get

Indicates whether the terms is of floating-point sort.

Definition at line 1513 of file Expr.cs.

1514 {
1515 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1516 }

## ◆ IsFPAbs

bool IsFPAbs
| get

Indicates whether the term is a floating-point term absolute value term

Definition at line 1659 of file Expr.cs.

1659{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }

## ◆ IsFPAdd

bool IsFPAdd
| get

Indicates whether the term is a floating-point addition term

Definition at line 1628 of file Expr.cs.

1628{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }

## ◆ IsFPDiv

bool IsFPDiv
| get

Indicates whether the term is a floating-point division term

Definition at line 1649 of file Expr.cs.

1649{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }

## ◆ IsFPEq

bool IsFPEq
| get

Indicates whether the term is a floating-point equality term

Definition at line 1689 of file Expr.cs.

1689{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }

## ◆ IsFPFMA

bool IsFPFMA
| get

Indicates whether the term is a floating-point fused multiply-add term

Definition at line 1674 of file Expr.cs.

1674{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }

## ◆ IsFPFP

bool IsFPFP
| get

Indicates whether the term is a floating-point constructor term

Definition at line 1749 of file Expr.cs.

1749{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }

## ◆ IsFPGe

bool IsFPGe
| get

Indicates whether the term is a floating-point greater-than or equal term

Definition at line 1709 of file Expr.cs.

1709{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }

## ◆ IsFPGt

bool IsFPGt
| get

Indicates whether the term is a floating-point greater-than term

Definition at line 1699 of file Expr.cs.

1699{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }

## ◆ IsFPisInf

bool IsFPisInf
| get

Indicates whether the term is a floating-point isInf predicate term

Definition at line 1719 of file Expr.cs.

1719{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }

## ◆ IsFPisNaN

bool IsFPisNaN
| get

Indicates whether the term is a floating-point isNaN predicate term

Definition at line 1714 of file Expr.cs.

1714{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }

## ◆ IsFPisNegative

bool IsFPisNegative
| get

Indicates whether the term is a floating-point isNegative predicate term

Definition at line 1739 of file Expr.cs.

1739{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }

## ◆ IsFPisNormal

bool IsFPisNormal
| get

Indicates whether the term is a floating-point isNormal term

Definition at line 1729 of file Expr.cs.

1729{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }

## ◆ IsFPisPositive

bool IsFPisPositive
| get

Indicates whether the term is a floating-point isPositive predicate term

Definition at line 1744 of file Expr.cs.

1744{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }

## ◆ IsFPisSubnormal

bool IsFPisSubnormal
| get

Indicates whether the term is a floating-point isSubnormal predicate term

Definition at line 1734 of file Expr.cs.

1734{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }

## ◆ IsFPisZero

bool IsFPisZero
| get

Indicates whether the term is a floating-point isZero predicate term

Definition at line 1724 of file Expr.cs.

1724{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }

## ◆ IsFPLe

bool IsFPLe
| get

Indicates whether the term is a floating-point less-than or equal term

Definition at line 1704 of file Expr.cs.

1704{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }

## ◆ IsFPLt

bool IsFPLt
| get

Indicates whether the term is a floating-point less-than term

Definition at line 1694 of file Expr.cs.

1694{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }

## ◆ IsFPMax

bool IsFPMax
| get

Indicates whether the term is a floating-point maximum term

Definition at line 1669 of file Expr.cs.

1669{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }

## ◆ IsFPMin

bool IsFPMin
| get

Indicates whether the term is a floating-point minimum term

Definition at line 1664 of file Expr.cs.

1664{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }

## ◆ IsFPMinusInfinity

bool IsFPMinusInfinity
| get

Indicates whether the term is a floating-point -oo

Definition at line 1608 of file Expr.cs.

1608{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }

## ◆ IsFPMinusZero

bool IsFPMinusZero
| get

Indicates whether the term is a floating-point -zero

Definition at line 1623 of file Expr.cs.

1623{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }

## ◆ IsFPMul

bool IsFPMul
| get

Indicates whether the term is a floating-point multiplication term

Definition at line 1644 of file Expr.cs.

1644{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }

## ◆ IsFPNaN

bool IsFPNaN
| get

Indicates whether the term is a floating-point NaN

Definition at line 1613 of file Expr.cs.

1613{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }

## ◆ IsFPNeg

bool IsFPNeg
| get

Indicates whether the term is a floating-point negation term

Definition at line 1639 of file Expr.cs.

1639{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }

## ◆ IsFPNumeral

bool IsFPNumeral
| get

Indicates whether the term is a floating-point numeral

Definition at line 1529 of file Expr.cs.

1529{ get { return IsFP && IsNumeral; } }
Microsoft.Z3.Expr.IsFP
bool IsFP
Indicates whether the terms is of floating-point sort.
Definition: Expr.cs:1514
Microsoft.Z3.Expr.IsNumeral
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:184

## ◆ IsFPPlusInfinity

bool IsFPPlusInfinity
| get

Indicates whether the term is a floating-point +oo

Definition at line 1603 of file Expr.cs.

1603{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }

## ◆ IsFPPlusZero

bool IsFPPlusZero
| get

Indicates whether the term is a floating-point +zero

Definition at line 1618 of file Expr.cs.

1618{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }

## ◆ IsFPRem

bool IsFPRem
| get

Indicates whether the term is a floating-point remainder term

Definition at line 1654 of file Expr.cs.

1654{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }

## ◆ IsFPRM

bool IsFPRM
| get

Indicates whether the terms is of floating-point rounding mode sort.

Definition at line 1521 of file Expr.cs.

1522 {
1523 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1524 }

## ◆ IsFPRMExpr

bool IsFPRMExpr
| get

Indicates whether the term is a floating-point rounding mode numeral

Definition at line 1589 of file Expr.cs.

1589 {
1590 get {
1591 return IsApp &&
1592 (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
1593 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
1594 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
1595 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
1596 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
1597 }
1598 }

## ◆ IsFPRMExprRNA

bool IsFPRMExprRNA
| get

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Definition at line 1569 of file Expr.cs.

1569{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }

## ◆ IsFPRMExprRNE

bool IsFPRMExprRNE
| get

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Definition at line 1564 of file Expr.cs.

1564{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }

## ◆ IsFPRMExprRTN

bool IsFPRMExprRTN
| get

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Definition at line 1574 of file Expr.cs.

1574{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }

## ◆ IsFPRMExprRTP

bool IsFPRMExprRTP
| get

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Definition at line 1579 of file Expr.cs.

1579{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }

## ◆ IsFPRMExprRTZ

bool IsFPRMExprRTZ
| get

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Definition at line 1584 of file Expr.cs.

1584{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }

## ◆ IsFPRMNumeral

bool IsFPRMNumeral
| get

Indicates whether the term is a floating-point rounding mode numeral

Definition at line 1534 of file Expr.cs.

1534{ get { return IsFPRM && IsNumeral; } }
Microsoft.Z3.Expr.IsFPRM
bool IsFPRM
Indicates whether the terms is of floating-point rounding mode sort.
Definition: Expr.cs:1522

## ◆ IsFPRMRoundNearestTiesToAway

bool IsFPRMRoundNearestTiesToAway
| get

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Definition at line 1544 of file Expr.cs.

1544{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }

## ◆ IsFPRMRoundNearestTiesToEven

bool IsFPRMRoundNearestTiesToEven
| get

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Definition at line 1539 of file Expr.cs.

1539{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }

## ◆ IsFPRMRoundTowardNegative

bool IsFPRMRoundTowardNegative
| get

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Definition at line 1549 of file Expr.cs.

1549{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }

## ◆ IsFPRMRoundTowardPositive

bool IsFPRMRoundTowardPositive
| get

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Definition at line 1554 of file Expr.cs.

1554{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }

## ◆ IsFPRMRoundTowardZero

bool IsFPRMRoundTowardZero
| get

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Definition at line 1559 of file Expr.cs.

1559{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }

## ◆ IsFPRoundToIntegral

bool IsFPRoundToIntegral
| get

Indicates whether the term is a floating-point roundToIntegral term

Definition at line 1684 of file Expr.cs.

1684{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }

## ◆ IsFPSqrt

bool IsFPSqrt
| get

Indicates whether the term is a floating-point square root term

Definition at line 1679 of file Expr.cs.

1679{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }

## ◆ IsFPSub

bool IsFPSub
| get

Indicates whether the term is a floating-point subtraction term

Definition at line 1634 of file Expr.cs.

1634{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }

## ◆ IsFPToFp

bool IsFPToFp
| get

Indicates whether the term is a floating-point conversion term

Definition at line 1754 of file Expr.cs.

1754{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }

## ◆ IsFPToFpUnsigned

bool IsFPToFpUnsigned
| get

Indicates whether the term is a floating-point conversion from unsigned bit-vector term

Definition at line 1759 of file Expr.cs.

1759{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }

## ◆ IsFPToIEEEBV

bool IsFPToIEEEBV
| get

Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term

Definition at line 1780 of file Expr.cs.

1780{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }

## ◆ IsFPToReal

bool IsFPToReal
| get

Indicates whether the term is a floating-point conversion to real term

Definition at line 1774 of file Expr.cs.

1774{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }

## ◆ IsFPToSBV

bool IsFPToSBV
| get

Indicates whether the term is a floating-point conversion to signed bit-vector term

Definition at line 1769 of file Expr.cs.

1769{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }

## ◆ IsFPToUBV

bool IsFPToUBV
| get

Indicates whether the term is a floating-point conversion to unsigned bit-vector term

Definition at line 1764 of file Expr.cs.

1764{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }

## ◆ IsGE

bool IsGE
| get

Indicates whether the term is a greater-than-or-equal

Definition at line 387 of file Expr.cs.

387{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }

## ◆ IsGT

bool IsGT
| get

Indicates whether the term is a greater-than

Definition at line 397 of file Expr.cs.

397{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }

## ◆ IsIDiv

bool IsIDiv
| get

Indicates whether the term is integer division (binary)

Definition at line 427 of file Expr.cs.

427{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }

## ◆ IsIff

bool IsIff
| get

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)

Definition at line 303 of file Expr.cs.

303{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }

## ◆ IsImplies

bool IsImplies
| get

Indicates whether the term is an implication

Definition at line 318 of file Expr.cs.

318{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }

## ◆ IsIndex

bool IsIndex
| get

Check whether expression is a sequence index.

Returns
  a Boolean

Definition at line 889 of file Expr.cs.

889{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }

## ◆ IsInt

bool IsInt
| get

Indicates whether the term is of integer sort.

Definition at line 361 of file Expr.cs.

362 {
363 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
364 }

## ◆ IsIntNum

bool IsIntNum
| get

Indicates whether the term is an integer numeral.

Definition at line 222 of file Expr.cs.

223 {
224 get { return IsNumeral && IsInt; }
225 }
Microsoft.Z3.Expr.IsInt
bool IsInt
Indicates whether the term is of integer sort.
Definition: Expr.cs:362

## ◆ IsIntToBV

bool IsIntToBV
| get

Indicates whether the term is a coercion from integer to bit-vector

This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

Definition at line 785 of file Expr.cs.

785{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }

## ◆ IsIntToReal

bool IsIntToReal
| get

Indicates whether the term is a coercion of integer to real (unary)

Definition at line 442 of file Expr.cs.

442{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }

## ◆ IsIsEmptyRelation

bool IsIsEmptyRelation
| get

Indicates whether the term is a test for the emptiness of a relation

Definition at line 1400 of file Expr.cs.

1400{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }

## ◆ IsITE

bool IsITE
| get

Indicates whether the term is a ternary if-then-else term

Definition at line 288 of file Expr.cs.

288{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }

## ◆ IsLabel

bool IsLabel
| get

Indicates whether the term is a label (used by the Boogie Verification condition generator).

The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.

Definition at line 814 of file Expr.cs.

814{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }

## ◆ IsLabelLit

bool IsLabelLit
| get

Indicates whether the term is a label literal (used by the Boogie Verification condition generator).

A label literal has a set of string parameters. It takes no arguments.

Definition at line 820 of file Expr.cs.

820{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }

## ◆ IsLE

bool IsLE
| get

Indicates whether the term is a less-than-or-equal

Definition at line 382 of file Expr.cs.

382{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }

## ◆ IsLength

bool IsLength
| get

Check whether expression is a sequence length.

Returns
  a Boolean

Definition at line 883 of file Expr.cs.

883{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }

## ◆ IsLT

bool IsLT
| get

Indicates whether the term is a less-than

Definition at line 392 of file Expr.cs.

392{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }

## ◆ IsModulus

bool IsModulus
| get

Indicates whether the term is modulus (binary)

Definition at line 437 of file Expr.cs.

437{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }

## ◆ IsMul

bool IsMul
| get

Indicates whether the term is multiplication (binary)

Definition at line 417 of file Expr.cs.

417{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }

## ◆ IsNot

bool IsNot
| get

Indicates whether the term is a negation

Definition at line 313 of file Expr.cs.

313{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }

## ◆ IsNumeral

bool IsNumeral
| get

Indicates whether the term is a numeral

Definition at line 183 of file Expr.cs.

184 {
185 get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
186 }

## ◆ IsOEQ

bool IsOEQ
| get

Indicates whether the term is a binary equivalence modulo namings.

This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

Definition at line 900 of file Expr.cs.

900{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }

## ◆ IsOr

bool IsOr
| get

Indicates whether the term is an n-ary disjunction

Definition at line 298 of file Expr.cs.

298{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }

## ◆ IsPbEq

bool IsPbEq
| get

Indicates whether the term is pbeq

Definition at line 343 of file Expr.cs.

343{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_EQ; } }

## ◆ IsPbGe

bool IsPbGe
| get

Indicates whether the term is pbge

Definition at line 353 of file Expr.cs.

353{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_GE; } }

## ◆ IsPbLe

bool IsPbLe
| get

Indicates whether the term is pble

Definition at line 348 of file Expr.cs.

348{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_LE; } }

## ◆ IsPrefix

bool IsPrefix
| get

Check whether expression is a prefix.

Returns
  a Boolean

Definition at line 847 of file Expr.cs.

847{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }

## ◆ IsProofAndElimination

bool IsProofAndElimination
| get

Indicates whether the term is a proof by elimination of AND

Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and l_1 ... l_n)

Definition at line 1031 of file Expr.cs.

1031{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }

## ◆ IsProofApplyDef

bool IsProofApplyDef
| get

Indicates whether the term is a proof for application of a definition

[apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Definition at line 1260 of file Expr.cs.

1260{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }

## ◆ IsProofAsserted

bool IsProofAsserted
| get

Indicates whether the term is a proof for a fact asserted by the user.

Definition at line 910 of file Expr.cs.

910{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }

## ◆ IsProofCommutativity

bool IsProofCommutativity
| get

Indicates whether the term is a proof by commutativity

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Definition at line 1191 of file Expr.cs.

1191{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }

## ◆ IsProofDefAxiom

bool IsProofDefAxiom
| get

Indicates whether the term is a proof for Tseitin-like axioms

Proof object used to justify Tseitin's like axioms:

(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)

This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

Definition at line 1227 of file Expr.cs.

1227{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }

## ◆ IsProofDefIntro

bool IsProofDefIntro
| get

Indicates whether the term is a proof for introduction of a name

Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type:

or:

when e only occurs positively.

When e is of the form (ite cond th el):

Otherwise: [def-intro]: (= n e)

Definition at line 1250 of file Expr.cs.

1250{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }

## ◆ IsProofDER

bool IsProofDER
| get

Indicates whether the term is a proof for destructive equality resolution

A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Definition at line 1121 of file Expr.cs.

1121{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }

## ◆ IsProofDistributivity

bool IsProofDistributivity
| get

Indicates whether the term is a distributivity proof object.

Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.

This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

Definition at line 1021 of file Expr.cs.

1021{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }

## ◆ IsProofElimUnusedVars

bool IsProofElimUnusedVars
| get

Indicates whether the term is a proof for elimination of unused variables.

A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))

It is used to justify the elimination of unused variables. This proof object has no antecedents.

Definition at line 1107 of file Expr.cs.

1107{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }

## ◆ IsProofGoal

bool IsProofGoal
| get

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.

Definition at line 915 of file Expr.cs.

915{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }

## ◆ IsProofHypothesis

bool IsProofHypothesis
| get

Indicates whether the term is a hypothesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1135 of file Expr.cs.

1135{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }

## ◆ IsProofIFFFalse

bool IsProofIFFFalse
| get

Indicates whether the term is a proof by iff-false

T1: (not p) [iff-false T1]: (iff p false)

Definition at line 1178 of file Expr.cs.

1178{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }

## ◆ IsProofIFFOEQ

bool IsProofIFFOEQ
| get

Indicates whether the term is a proof iff-oeq

T1: (iff p q) [iff~ T1]: (~ p q)

Definition at line 1269 of file Expr.cs.

1269{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }

## ◆ IsProofIFFTrue

bool IsProofIFFTrue
| get

Indicates whether the term is a proof by iff-true

T1: p [iff-true T1]: (iff p true)

Definition at line 1169 of file Expr.cs.

1169{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }

## ◆ IsProofLemma

bool IsProofLemma
| get

Indicates whether the term is a proof by lemma

T1: false

This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.

Definition at line 1148 of file Expr.cs.

1148{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }

## ◆ IsProofModusPonens

bool IsProofModusPonens
| get

Indicates whether the term is proof via modus ponens

Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q)

The second antecedents may also be a proof for (iff p q).

Definition at line 926 of file Expr.cs.

926{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }

## ◆ IsProofModusPonensOEQ

bool IsProofModusPonensOEQ
| get

Indicates whether the term is a proof by modus ponens for equi-satisfiability.

Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q)

Definition at line 1346 of file Expr.cs.

1346{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }

## ◆ IsProofMonotonicity

bool IsProofMonotonicity
| get

Indicates whether the term is a monotonicity proof object.

T1: (R t_1 s_1) ... Tn: (R t_n s_n)

Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are suppressed to save space.

Definition at line 993 of file Expr.cs.

993{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }

## ◆ IsProofNNFNeg

bool IsProofNNFNeg
| get

Indicates whether the term is a proof for a negative NNF step

Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n

and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n

and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'

(and (or r_1 r_2) (or r_1' r_2')))

Definition at line 1322 of file Expr.cs.

1322{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }

## ◆ IsProofNNFPos

bool IsProofNNFPos
| get

Indicates whether the term is a proof for a positive NNF step

Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'

(and (or r_1 r_2') (or r_1' r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new

(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.

Definition at line 1297 of file Expr.cs.

1297{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }

## ◆ IsProofOrElimination

bool IsProofOrElimination
| get

Indicates whether the term is a proof by elimination of not-or

Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)

Definition at line 1041 of file Expr.cs.

1041{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }

## ◆ IsProofPullQuant

bool IsProofPullQuant
| get

Indicates whether the term is a proof for pulling quantifiers out.

A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Definition at line 1081 of file Expr.cs.

1081{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }

## ◆ IsProofPushQuant

bool IsProofPushQuant
| get

Indicates whether the term is a proof for pushing quantifiers in.

A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents

Definition at line 1095 of file Expr.cs.

1095{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }

## ◆ IsProofQuantInst

bool IsProofQuantInst
| get

Indicates whether the term is a proof for quantifier instantiation

A proof of (or (not (forall (x) (P x))) (P a))

Definition at line 1129 of file Expr.cs.

1129{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }

## ◆ IsProofQuantIntro

bool IsProofQuantIntro
| get

Indicates whether the term is a quant-intro proof

Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: (~ p q)

Definition at line 1003 of file Expr.cs.

1003{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }

## ◆ IsProofReflexivity

bool IsProofReflexivity
| get

Indicates whether the term is a proof for (R t t), where R is a reflexive relation.

This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.

Definition at line 935 of file Expr.cs.

935{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }

## ◆ IsProofRewrite

bool IsProofRewrite
| get

Indicates whether the term is a proof by rewriting

A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.

Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

Definition at line 1060 of file Expr.cs.

1060{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }

## ◆ IsProofRewriteStar

bool IsProofRewriteStar
| get

Indicates whether the term is a proof by rewriting

A proof for rewriting an expression t into an expression s. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is used in a few cases:

- When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
- When converting bit-vectors to Booleans (BIT2BOOL=true)

Definition at line 1073 of file Expr.cs.

1073{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }

## ◆ IsProofSkolemize

bool IsProofSkolemize
| get

Indicates whether the term is a proof for a Skolemization step

Proof for:

This proof object has no antecedents.

Definition at line 1335 of file Expr.cs.

1335{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }

## ◆ IsProofSymmetry

bool IsProofSymmetry
| get

Indicates whether the term is proof by symmetricity of a relation

Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the antecedent of this proof object.

Definition at line 946 of file Expr.cs.

946{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }

## ◆ IsProofTheoryLemma

bool IsProofTheoryLemma
| get

Indicates whether the term is a proof for theory lemma

Generic proof for theory lemmas.

The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are:

- farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
- triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
- gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.

Definition at line 1365 of file Expr.cs.

1365{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }

## ◆ IsProofTransitivity

bool IsProofTransitivity
| get

Indicates whether the term is a proof by transitivity of a relation

Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u)

Definition at line 958 of file Expr.cs.

958{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }

## ◆ IsProofTransitivityStar

bool IsProofTransitivityStar
| get

Indicates whether the term is a proof by condensed transitivity of a relation

Condensed transitivity proof. It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

Definition at line 979 of file Expr.cs.

979{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }

## ◆ IsProofTrue

bool IsProofTrue
| get

Indicates whether the term is a Proof for the expression 'true'.

Definition at line 905 of file Expr.cs.

905{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }

## ◆ IsProofUnitResolution

bool IsProofUnitResolution
| get

Indicates whether the term is a proof by unit resolution

T1: (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')

Definition at line 1160 of file Expr.cs.

1160{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }

## ◆ IsRatNum

bool IsRatNum
| get

Indicates whether the term is a real numeral.

Definition at line 232 of file Expr.cs.

233 {
234 get { return IsNumeral && IsReal; }
235 }
Microsoft.Z3.Expr.IsReal
bool IsReal
Indicates whether the term is of sort real.
Definition: Expr.cs:370

## ◆ IsReal

bool IsReal
| get

Indicates whether the term is of sort real.

Definition at line 369 of file Expr.cs.

370 {
371 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
372 }

## ◆ IsRealIsInt

bool IsRealIsInt
| get

Indicates whether the term is a check that tests whether a real is integral (unary)

Definition at line 452 of file Expr.cs.

452{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }

## ◆ IsRealToInt

bool IsRealToInt
| get

Indicates whether the term is a coercion of real to integer (unary)

Definition at line 447 of file Expr.cs.

447{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }

## ◆ IsRelation

bool IsRelation
| get

Indicates whether the term is of relation sort.

Definition at line 1372 of file Expr.cs.

1373 {
1374 get
1375 {
1376 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1377 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
1378 == (uint)Z3_sort_kind.Z3_RELATION_SORT);
1379 }
1380 }

## ◆ IsRelationalJoin

bool IsRelationalJoin
| get

Indicates whether the term is a relational join

Definition at line 1405 of file Expr.cs.

1405{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }

## ◆ IsRelationClone

bool IsRelationClone
| get

Indicates whether the term is a relational clone (copy)

Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind

See also
  IsRelationUnion

to perform destructive updates to the first argument.

Definition at line 1487 of file Expr.cs.

1487{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }

## ◆ IsRelationComplement

bool IsRelationComplement
| get

Indicates whether the term is the complement of a relation

Definition at line 1465 of file Expr.cs.

1465{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }

## ◆ IsRelationFilter

bool IsRelationFilter
| get

Indicates whether the term is a relation filter

Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Definition at line 1435 of file Expr.cs.

1435{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }

## ◆ IsRelationNegationFilter

bool IsRelationNegationFilter
| get

Indicates whether the term is an intersection of a relation with the negation of another.

Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

Definition at line 1451 of file Expr.cs.

1451{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }

## ◆ IsRelationProject

bool IsRelationProject
| get

Indicates whether the term is a projection of columns (provided as numbers in the parameters).

The function takes one argument.

Definition at line 1423 of file Expr.cs.

1423{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }

## ◆ IsRelationRename

bool IsRelationRename
| get

Indicates whether the term is the renaming of a column in a relation

The function takes one argument. The parameters contain the renaming as a cycle.

Definition at line 1460 of file Expr.cs.

1460{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }

## ◆ IsRelationSelect

bool IsRelationSelect
| get

Indicates whether the term is a relational select

Check if a record is an element of the relation. The function takes `n+1` arguments, where the first argument is a relation, and the remaining `n` arguments correspond to a record.

Definition at line 1475 of file Expr.cs.

1475{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }

## ◆ IsRelationStore

bool IsRelationStore
| get

Indicates whether the term is an relation store

Insert a record into a relation. The function takes `n+1` arguments, where the first argument is the relation and the remaining `n` elements correspond to the `n` columns of the relation.

Definition at line 1390 of file Expr.cs.

1390{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }

## ◆ IsRelationUnion

bool IsRelationUnion
| get

Indicates whether the term is the union or convex hull of two relations.

The function takes two arguments.

Definition at line 1411 of file Expr.cs.

1411{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }

## ◆ IsRelationWiden

bool IsRelationWiden
| get

Indicates whether the term is the widening of two relations

The function takes two arguments.

Definition at line 1417 of file Expr.cs.

1417{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }

## ◆ IsRemainder

bool IsRemainder
| get

Indicates whether the term is remainder (binary)

Definition at line 432 of file Expr.cs.

432{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }

## ◆ IsReplace

bool IsReplace
| get

Check whether expression is a replace.

Returns
  a Boolean

Definition at line 871 of file Expr.cs.

871{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }

## ◆ IsSelect

bool IsSelect
| get

Indicates whether the term is an array select.

Definition at line 479 of file Expr.cs.

479{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }

## ◆ IsSetComplement

bool IsSetComplement
| get

Indicates whether the term is set complement

Definition at line 526 of file Expr.cs.

526{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }

## ◆ IsSetDifference

bool IsSetDifference
| get

Indicates whether the term is set difference

Definition at line 521 of file Expr.cs.

521{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }

## ◆ IsSetIntersect

bool IsSetIntersect
| get

Indicates whether the term is set intersection

Definition at line 516 of file Expr.cs.

516{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }

## ◆ IsSetSubset

bool IsSetSubset
| get

Indicates whether the term is set subset

Definition at line 531 of file Expr.cs.

531{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }

## ◆ IsSetUnion

bool IsSetUnion
| get

Indicates whether the term is set union

Definition at line 511 of file Expr.cs.

511{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }

## ◆ IsStore

bool IsStore
| get

Indicates whether the term is an array store.

It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.

Definition at line 474 of file Expr.cs.

474{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }

## ◆ IsString

bool IsString
| get

Check whether expression is a string constant.

Returns
  a Boolean

Definition at line 829 of file Expr.cs.

829{ get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject) != 0; } }

## ◆ IsSub

bool IsSub
| get

Indicates whether the term is subtraction (binary)

Definition at line 407 of file Expr.cs.

407{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }

## ◆ IsSuffix

bool IsSuffix
| get

Check whether expression is a suffix.

Returns
  a Boolean

Definition at line 853 of file Expr.cs.

853{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }

## ◆ IsTrue

bool IsTrue
| get

Indicates whether the term is the constant true.

Definition at line 268 of file Expr.cs.

268{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }

## ◆ IsUMinus

bool IsUMinus
| get

Indicates whether the term is a unary minus

Definition at line 412 of file Expr.cs.

412{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }

## ◆ IsWellSorted

bool IsWellSorted
| get

Indicates whether the term is well-sorted.

Returns
  True if the term is well-sorted, false otherwise.

Definition at line 192 of file Expr.cs.

193 {
194 get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
195 }

## ◆ IsXor

bool IsXor
| get

Indicates whether the term is an exclusive or

Definition at line 308 of file Expr.cs.

308{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }

## ◆ NumArgs

uint NumArgs
| get

The number of arguments of the expression.

Definition at line 69 of file Expr.cs.

70 {
71 get { return Native.Z3_get_app_num_args(Context.nCtx, NativeObject); }
72 }

Referenced by Expr.Update().

## ◆ Sort

Sort Sort
| get

The Sort of the term.

Definition at line 200 of file Expr.cs.

201 {
202 get
203 {
204 return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
205 }
206 }
Microsoft.Z3.Expr.Sort
Sort Sort
The Sort of the term.
Definition: Expr.cs:201

## ◆ String

string String
| get

Retrieve string corresponding to string constant.

the expression should be a string constant, (IsString should be true).

Definition at line 835 of file Expr.cs.

835{ get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }