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...
 
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 IsInterpolant [get]
 Indicates whether the term is marked for interpolation. 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 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 eliminiation 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 IsProofPullQuantStar [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 hypthesis 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 IsProofNNFStar [get]
 Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. More...
 
bool IsProofCNFStar [get]
 Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. 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 divison 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 erqual 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-Burijn 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 29 of file Expr.cs.

Constructor & Destructor Documentation

◆ Expr()

Expr ( Context  ctx,
IntPtr  obj 
)
inlineprotected

Constructor for Expr

Definition at line 1763 of file Expr.cs.

1763 : base(ctx, obj) { Contract.Requires(ctx != null); }

Member Function Documentation

◆ Simplify()

Expr Simplify ( Params  p = null)
inline

Returns a simplified version of the expression.

Parameters
pA set of parameters to configure the simplifier
See also
Context.SimplifyHelp

Definition at line 36 of file Expr.cs.

37  {
38  Contract.Ensures(Contract.Result<Expr>() != null);
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  }
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ Substitute() [1/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 115 of file Expr.cs.

116  {
117  Contract.Requires(from != null);
118  Contract.Requires(to != null);
119  Contract.Requires(Contract.ForAll(from, f => f != null));
120  Contract.Requires(Contract.ForAll(to, t => t != null));
121  Contract.Ensures(Contract.Result<Expr>() != null);
122 
123  Context.CheckContextMatch<Expr>(from);
124  Context.CheckContextMatch<Expr>(to);
125  if (from.Length != to.Length)
126  throw new Z3Exception("Argument sizes do not match");
127  return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
128  }
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ Substitute() [2/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 134 of file Expr.cs.

135  {
136  Contract.Requires(from != null);
137  Contract.Requires(to != null);
138  Contract.Ensures(Contract.Result<Expr>() != null);
139 
140  return Substitute(new Expr[] { from }, new Expr[] { to });
141  }
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:115
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ 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 149 of file Expr.cs.

150  {
151  Contract.Requires(to != null);
152  Contract.Requires(Contract.ForAll(to, t => t != null));
153  Contract.Ensures(Contract.Result<Expr>() != null);
154 
155  Context.CheckContextMatch<Expr>(to);
156  return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
157  }
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ ToString()

override string ToString ( )
inline

Returns a string representation of the expression.

Definition at line 178 of file Expr.cs.

179  {
180  return base.ToString();
181  }

◆ Translate()

new Expr Translate ( Context  ctx)
inline

Translates (copies) the term to the Context ctx .

Parameters
ctxA context
Returns
A copy of the term which is associated with ctx

Definition at line 164 of file Expr.cs.

165  {
166  Contract.Requires(ctx != null);
167  Contract.Ensures(Contract.Result<Expr>() != null);
168 
169  if (ReferenceEquals(Context, ctx))
170  return this;
171  else
172  return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
173  }
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ 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 96 of file Expr.cs.

97  {
98  Contract.Requires(args != null);
99  Contract.Requires(Contract.ForAll(args, a => a != null));
100 
101  Context.CheckContextMatch<Expr>(args);
102  if (IsApp && args.Length != NumArgs)
103  throw new Z3Exception("Number of arguments does not match");
104  NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
105  }
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:71
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

Property Documentation

◆ Args

Expr [] Args
get

The arguments of the expression.

Definition at line 79 of file Expr.cs.

79  {
80  get
81  {
82  Contract.Ensures(Contract.Result<Expr[]>() != null);
83 
84  uint n = NumArgs;
85  Expr[] res = new Expr[n];
86  for (uint i = 0; i < n; i++)
87  res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
88  return res;
89  }
90  }
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:71
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1763

◆ BoolValue

Z3_lbool BoolValue
get

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

Definition at line 63 of file Expr.cs.

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

◆ FuncDecl

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

Definition at line 50 of file Expr.cs.

Referenced by Model.ConstInterp().

50  {
51  get
52  {
53  Contract.Ensures(Contract.Result<FuncDecl>() != null);
54  return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
55  }
56  }
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50

◆ Index

uint Index
get

The de-Burijn 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))

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 1746 of file Expr.cs.

1746  {
1747  get
1748  {
1749  if (!IsVar)
1750  throw new Z3Exception("Term is not a bound variable.");
1751 
1752  Contract.EndContractBlock();
1753 
1754  return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1755  }
1756  }
bool IsVar
Indicates whether the AST is a BoundVariable
Definition: AST.cs:164

◆ IsAdd

bool IsAdd
get

Indicates whether the term is addition (binary)

Definition at line 379 of file Expr.cs.

379 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsAlgebraicNumber

bool IsAlgebraicNumber
get

Indicates whether the term is an algebraic number

Definition at line 247 of file Expr.cs.

247  {
248  get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
249  }

◆ IsAnd

bool IsAnd
get

Indicates whether the term is an n-ary conjunction

Definition at line 297 of file Expr.cs.

297 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsArithmeticNumeral

bool IsArithmeticNumeral
get

Indicates whether the term is an arithmetic numeral.

Definition at line 354 of file Expr.cs.

354 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsArray

bool IsArray
get

Indicates whether the term is of an array sort.

Definition at line 437 of file Expr.cs.

437  {
438  get
439  {
440  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
441  (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
442  == Z3_sort_kind.Z3_ARRAY_SORT);
443  }
444  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ 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 474 of file Expr.cs.

474 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 481 of file Expr.cs.

481 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBool

bool IsBool
get

Indicates whether the term has Boolean sort.

Definition at line 259 of file Expr.cs.

259  {
260  get
261  {
262  return (IsExpr &&
263  Native.Z3_is_eq_sort(Context.nCtx,
264  Native.Z3_mk_bool_sort(Context.nCtx),
265  Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
266  }
267  }
bool IsExpr
Indicates whether the AST is an Expr
Definition: AST.cs:138

◆ IsBV

bool IsBV
get

Indicates whether the terms is of bit-vector sort.

Definition at line 516 of file Expr.cs.

516  {
517  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
518  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsBVAdd

bool IsBVAdd
get

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

Definition at line 543 of file Expr.cs.

543 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVAND

bool IsBVAND
get

Indicates whether the term is a bit-wise AND

Definition at line 648 of file Expr.cs.

648 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVBitOne

bool IsBVBitOne
get

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

Definition at line 528 of file Expr.cs.

528 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVBitZero

bool IsBVBitZero
get

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

Definition at line 533 of file Expr.cs.

533 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 776 of file Expr.cs.

776 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVComp

bool IsBVComp
get

Indicates whether the term is a bit-vector comparison

Definition at line 718 of file Expr.cs.

718 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVConcat

bool IsBVConcat
get

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

Definition at line 683 of file Expr.cs.

683 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVExtract

bool IsBVExtract
get

Indicates whether the term is a bit-vector extraction

Definition at line 698 of file Expr.cs.

698 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVMul

bool IsBVMul
get

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

Definition at line 553 of file Expr.cs.

553 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVNAND

bool IsBVNAND
get

Indicates whether the term is a bit-wise NAND

Definition at line 668 of file Expr.cs.

668 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVNOR

bool IsBVNOR
get

Indicates whether the term is a bit-wise NOR

Definition at line 673 of file Expr.cs.

673 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVNOT

bool IsBVNOT
get

Indicates whether the term is a bit-wise NOT

Definition at line 658 of file Expr.cs.

658 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVNumeral

bool IsBVNumeral
get

Indicates whether the term is a bit-vector numeral

Definition at line 523 of file Expr.cs.

523 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVOR

bool IsBVOR
get

Indicates whether the term is a bit-wise OR

Definition at line 653 of file Expr.cs.

653 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVReduceAND

bool IsBVReduceAND
get

Indicates whether the term is a bit-vector reduce AND

Definition at line 713 of file Expr.cs.

713 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVReduceOR

bool IsBVReduceOR
get

Indicates whether the term is a bit-vector reduce OR

Definition at line 708 of file Expr.cs.

708 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVRepeat

bool IsBVRepeat
get

Indicates whether the term is a bit-vector repetition

Definition at line 703 of file Expr.cs.

703 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVRotateLeft

bool IsBVRotateLeft
get

Indicates whether the term is a bit-vector rotate left

Definition at line 738 of file Expr.cs.

738 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 749 of file Expr.cs.

749 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVRotateRight

bool IsBVRotateRight
get

Indicates whether the term is a bit-vector rotate right

Definition at line 743 of file Expr.cs.

743 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 755 of file Expr.cs.

755 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSDiv

bool IsBVSDiv
get

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

Definition at line 558 of file Expr.cs.

558 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSGE

bool IsBVSGE
get

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

Definition at line 623 of file Expr.cs.

623 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSGT

bool IsBVSGT
get

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

Definition at line 643 of file Expr.cs.

643 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVShiftLeft

bool IsBVShiftLeft
get

Indicates whether the term is a bit-vector shift left

Definition at line 723 of file Expr.cs.

723 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVShiftRightArithmetic

bool IsBVShiftRightArithmetic
get

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

Definition at line 733 of file Expr.cs.

733 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVShiftRightLogical

bool IsBVShiftRightLogical
get

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

Definition at line 728 of file Expr.cs.

728 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSignExtension

bool IsBVSignExtension
get

Indicates whether the term is a bit-vector sign extension

Definition at line 688 of file Expr.cs.

688 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSLE

bool IsBVSLE
get

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

Definition at line 613 of file Expr.cs.

613 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSLT

bool IsBVSLT
get

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

Definition at line 633 of file Expr.cs.

633 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSMod

bool IsBVSMod
get

Indicates whether the term is a bit-vector signed modulus

Definition at line 578 of file Expr.cs.

578 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSRem

bool IsBVSRem
get

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

Definition at line 568 of file Expr.cs.

568 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVSub

bool IsBVSub
get

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

Definition at line 548 of file Expr.cs.

548 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 769 of file Expr.cs.

769 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVUDiv

bool IsBVUDiv
get

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

Definition at line 563 of file Expr.cs.

563 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVUGE

bool IsBVUGE
get

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

Definition at line 618 of file Expr.cs.

618 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVUGT

bool IsBVUGT
get

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

Definition at line 638 of file Expr.cs.

638 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVULE

bool IsBVULE
get

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

Definition at line 608 of file Expr.cs.

608 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVULT

bool IsBVULT
get

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

Definition at line 628 of file Expr.cs.

628 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVUMinus

bool IsBVUMinus
get

Indicates whether the term is a bit-vector unary minus

Definition at line 538 of file Expr.cs.

538 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVURem

bool IsBVURem
get

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

Definition at line 573 of file Expr.cs.

573 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVXNOR

bool IsBVXNOR
get

Indicates whether the term is a bit-wise XNOR

Definition at line 678 of file Expr.cs.

678 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVXOR

bool IsBVXOR
get

Indicates whether the term is a bit-wise XOR

Definition at line 663 of file Expr.cs.

663 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 782 of file Expr.cs.

782 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsBVZeroExtension

bool IsBVZeroExtension
get

Indicates whether the term is a bit-vector zero extension

Definition at line 693 of file Expr.cs.

693 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsConst

bool IsConst
get

Indicates whether the term represents a constant.

Definition at line 217 of file Expr.cs.

217  {
218  get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
219  }
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:100
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:71
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50

◆ 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 462 of file Expr.cs.

462 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 468 of file Expr.cs.

468 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsDistinct

bool IsDistinct
get

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

Definition at line 287 of file Expr.cs.

287 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsDiv

bool IsDiv
get

Indicates whether the term is division (binary)

Definition at line 399 of file Expr.cs.

399 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsEmptyRelation

bool IsEmptyRelation
get

Indicates whether the term is an empty relation

Definition at line 1335 of file Expr.cs.

1335 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsEq

bool IsEq
get

Indicates whether the term is an equality predicate.

Definition at line 282 of file Expr.cs.

282 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFalse

bool IsFalse
get

Indicates whether the term is the constant false.

Definition at line 277 of file Expr.cs.

277 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFiniteDomain

bool IsFiniteDomain
get

Indicates whether the term is of an array sort.

Definition at line 1435 of file Expr.cs.

1435  {
1436  get
1437  {
1438  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1439  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1440  }
1441  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsFiniteDomainLT

bool IsFiniteDomainLT
get

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

Definition at line 1446 of file Expr.cs.

1446 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFP

bool IsFP
get

Indicates whether the terms is of floating-point sort.

Definition at line 1454 of file Expr.cs.

1454  {
1455  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1456  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsFPAbs

bool IsFPAbs
get

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

Definition at line 1599 of file Expr.cs.

1599 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPAdd

bool IsFPAdd
get

Indicates whether the term is a floating-point addition term

Definition at line 1568 of file Expr.cs.

1568 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPDiv

bool IsFPDiv
get

Indicates whether the term is a floating-point divison term

Definition at line 1589 of file Expr.cs.

1589 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPEq

bool IsFPEq
get

Indicates whether the term is a floating-point equality term

Definition at line 1629 of file Expr.cs.

1629 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPFMA

bool IsFPFMA
get

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

Definition at line 1614 of file Expr.cs.

1614 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPFP

bool IsFPFP
get

Indicates whether the term is a floating-point constructor term

Definition at line 1689 of file Expr.cs.

1689 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPGe

bool IsFPGe
get

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

Definition at line 1649 of file Expr.cs.

1649 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPGt

bool IsFPGt
get

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

Definition at line 1639 of file Expr.cs.

1639 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisInf

bool IsFPisInf
get

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

Definition at line 1659 of file Expr.cs.

1659 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisNaN

bool IsFPisNaN
get

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

Definition at line 1654 of file Expr.cs.

1654 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisNegative

bool IsFPisNegative
get

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

Definition at line 1679 of file Expr.cs.

1679 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisNormal

bool IsFPisNormal
get

Indicates whether the term is a floating-point isNormal term

Definition at line 1669 of file Expr.cs.

1669 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisPositive

bool IsFPisPositive
get

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

Definition at line 1684 of file Expr.cs.

1684 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisSubnormal

bool IsFPisSubnormal
get

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

Definition at line 1674 of file Expr.cs.

1674 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPisZero

bool IsFPisZero
get

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

Definition at line 1664 of file Expr.cs.

1664 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPLe

bool IsFPLe
get

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

Definition at line 1644 of file Expr.cs.

1644 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPLt

bool IsFPLt
get

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

Definition at line 1634 of file Expr.cs.

1634 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPMax

bool IsFPMax
get

Indicates whether the term is a floating-point maximum term

Definition at line 1609 of file Expr.cs.

1609 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPMin

bool IsFPMin
get

Indicates whether the term is a floating-point minimum term

Definition at line 1604 of file Expr.cs.

1604 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPMinusInfinity

bool IsFPMinusInfinity
get

Indicates whether the term is a floating-point -oo

Definition at line 1548 of file Expr.cs.

1548 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPMinusZero

bool IsFPMinusZero
get

Indicates whether the term is a floating-point -zero

Definition at line 1563 of file Expr.cs.

1563 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPMul

bool IsFPMul
get

Indicates whether the term is a floating-point multiplication term

Definition at line 1584 of file Expr.cs.

1584 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPNaN

bool IsFPNaN
get

Indicates whether the term is a floating-point NaN

Definition at line 1553 of file Expr.cs.

1553 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPNeg

bool IsFPNeg
get

Indicates whether the term is a floating-point negation term

Definition at line 1579 of file Expr.cs.

1579 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPNumeral

bool IsFPNumeral
get

Indicates whether the term is a floating-point numeral

Definition at line 1469 of file Expr.cs.

1469 { get { return IsFP && IsNumeral; } }
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:187
bool IsFP
Indicates whether the terms is of floating-point sort.
Definition: Expr.cs:1454

◆ IsFPPlusInfinity

bool IsFPPlusInfinity
get

Indicates whether the term is a floating-point +oo

Definition at line 1543 of file Expr.cs.

1543 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPPlusZero

bool IsFPPlusZero
get

Indicates whether the term is a floating-point +zero

Definition at line 1558 of file Expr.cs.

1558 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRem

bool IsFPRem
get

Indicates whether the term is a floating-point remainder term

Definition at line 1594 of file Expr.cs.

1594 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRM

bool IsFPRM
get

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

Definition at line 1462 of file Expr.cs.

1462  {
1463  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1464  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsFPRMExpr

bool IsFPRMExpr
get

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

Definition at line 1529 of file Expr.cs.

1529  {
1530  get {
1531  return IsApp &&
1532  (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
1533  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
1534  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
1535  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
1536  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
1537  }
1538  }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMExprRNA

bool IsFPRMExprRNA
get

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

Definition at line 1509 of file Expr.cs.

1509 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMExprRNE

bool IsFPRMExprRNE
get

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

Definition at line 1504 of file Expr.cs.

1504 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMExprRTN

bool IsFPRMExprRTN
get

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

Definition at line 1514 of file Expr.cs.

1514 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMExprRTP

bool IsFPRMExprRTP
get

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

Definition at line 1519 of file Expr.cs.

1519 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMExprRTZ

bool IsFPRMExprRTZ
get

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

Definition at line 1524 of file Expr.cs.

1524 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMNumeral

bool IsFPRMNumeral
get

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

Definition at line 1474 of file Expr.cs.

1474 { get { return IsFPRM && IsNumeral; } }
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:187
bool IsFPRM
Indicates whether the terms is of floating-point rounding mode sort.
Definition: Expr.cs:1462

◆ IsFPRMRoundNearestTiesToAway

bool IsFPRMRoundNearestTiesToAway
get

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

Definition at line 1484 of file Expr.cs.

1484 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMRoundNearestTiesToEven

bool IsFPRMRoundNearestTiesToEven
get

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

Definition at line 1479 of file Expr.cs.

1479 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMRoundTowardNegative

bool IsFPRMRoundTowardNegative
get

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

Definition at line 1489 of file Expr.cs.

1489 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMRoundTowardPositive

bool IsFPRMRoundTowardPositive
get

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

Definition at line 1494 of file Expr.cs.

1494 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRMRoundTowardZero

bool IsFPRMRoundTowardZero
get

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

Definition at line 1499 of file Expr.cs.

1499 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPRoundToIntegral

bool IsFPRoundToIntegral
get

Indicates whether the term is a floating-point roundToIntegral term

Definition at line 1624 of file Expr.cs.

1624 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPSqrt

bool IsFPSqrt
get

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

Definition at line 1619 of file Expr.cs.

1619 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPSub

bool IsFPSub
get

Indicates whether the term is a floating-point subtraction term

Definition at line 1574 of file Expr.cs.

1574 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToFp

bool IsFPToFp
get

Indicates whether the term is a floating-point conversion term

Definition at line 1694 of file Expr.cs.

1694 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToFpUnsigned

bool IsFPToFpUnsigned
get

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

Definition at line 1699 of file Expr.cs.

1699 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToIEEEBV

bool IsFPToIEEEBV
get

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

Definition at line 1720 of file Expr.cs.

1720 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToReal

bool IsFPToReal
get

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

Definition at line 1714 of file Expr.cs.

1714 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToSBV

bool IsFPToSBV
get

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

Definition at line 1709 of file Expr.cs.

1709 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsFPToUBV

bool IsFPToUBV
get

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

Definition at line 1704 of file Expr.cs.

1704 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsGE

bool IsGE
get

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

Definition at line 364 of file Expr.cs.

364 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsGT

bool IsGT
get

Indicates whether the term is a greater-than

Definition at line 374 of file Expr.cs.

374 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsIDiv

bool IsIDiv
get

Indicates whether the term is integer division (binary)

Definition at line 404 of file Expr.cs.

404 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsIff

bool IsIff
get

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

Definition at line 307 of file Expr.cs.

307 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsImplies

bool IsImplies
get

Indicates whether the term is an implication

Definition at line 322 of file Expr.cs.

322 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsInt

bool IsInt
get

Indicates whether the term is of integer sort.

Definition at line 339 of file Expr.cs.

339  {
340  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
341  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsInterpolant

bool IsInterpolant
get

Indicates whether the term is marked for interpolation.

Definition at line 331 of file Expr.cs.

331 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsIntNum

bool IsIntNum
get

Indicates whether the term is an integer numeral.

Definition at line 227 of file Expr.cs.

227  {
228  get { return IsNumeral && IsInt; }
229  }
bool IsInt
Indicates whether the term is of integer sort.
Definition: Expr.cs:339
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:187

◆ 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 762 of file Expr.cs.

762 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsIntToReal

bool IsIntToReal
get

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

Definition at line 419 of file Expr.cs.

419 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsIsEmptyRelation

bool IsIsEmptyRelation
get

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

Definition at line 1340 of file Expr.cs.

1340 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsITE

bool IsITE
get

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

Definition at line 292 of file Expr.cs.

292 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 791 of file Expr.cs.

791 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 797 of file Expr.cs.

797 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsLE

bool IsLE
get

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

Definition at line 359 of file Expr.cs.

359 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsLT

bool IsLT
get

Indicates whether the term is a less-than

Definition at line 369 of file Expr.cs.

369 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsModulus

bool IsModulus
get

Indicates whether the term is modulus (binary)

Definition at line 414 of file Expr.cs.

414 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsMul

bool IsMul
get

Indicates whether the term is multiplication (binary)

Definition at line 394 of file Expr.cs.

394 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsNot

bool IsNot
get

Indicates whether the term is a negation

Definition at line 317 of file Expr.cs.

317 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsNumeral

bool IsNumeral
get

Indicates whether the term is a numeral

Definition at line 187 of file Expr.cs.

187  {
188  get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
189  }

◆ 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 806 of file Expr.cs.

806 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsOr

bool IsOr
get

Indicates whether the term is an n-ary disjunction

Definition at line 302 of file Expr.cs.

302 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 937 of file Expr.cs.

937 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1178 of file Expr.cs.

1178 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofAsserted

bool IsProofAsserted
get

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

Definition at line 816 of file Expr.cs.

816 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofCNFStar

bool IsProofCNFStar
get

Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.

A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1262 of file Expr.cs.

1262 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1109 of file Expr.cs.

1109 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1145 of file Expr.cs.

1145 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1168 of file Expr.cs.

1168 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1039 of file Expr.cs.

1039 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 927 of file Expr.cs.

927 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1025 of file Expr.cs.

1025 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofGoal

bool IsProofGoal
get

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

Definition at line 821 of file Expr.cs.

821 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofHypothesis

bool IsProofHypothesis
get

Indicates whether the term is a hypthesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1053 of file Expr.cs.

1053 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1096 of file Expr.cs.

1096 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofIFFOEQ

bool IsProofIFFOEQ
get

Indicates whether the term is a proof iff-oeq

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

Definition at line 1187 of file Expr.cs.

1187 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1087 of file Expr.cs.

1087 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1066 of file Expr.cs.

1066 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 832 of file Expr.cs.

832 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1286 of file Expr.cs.

1286 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 supressed to save space.

Definition at line 899 of file Expr.cs.

899 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1240 of file Expr.cs.

1240 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1215 of file Expr.cs.

1215 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofNNFStar

bool IsProofNNFStar
get

Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.

A proof for (~ P Q) where Q is in negation normal form.

This proof object is only used if the parameter PROOF_MODE is 1.

This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1252 of file Expr.cs.

1252 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofOrElimination

bool IsProofOrElimination
get

Indicates whether the term is a proof by eliminiation 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 947 of file Expr.cs.

947 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 990 of file Expr.cs.

990 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofPullQuantStar

bool IsProofPullQuantStar
get

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

A proof for (iff P Q) where Q is in prenex normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents

Definition at line 1000 of file Expr.cs.

1000 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1013 of file Expr.cs.

1013 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1047 of file Expr.cs.

1047 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 909 of file Expr.cs.

909 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 841 of file Expr.cs.

841 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 966 of file Expr.cs.

966 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are:

  • When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
  • When converting bit-vectors to Booleans (BIT2BOOL=true)
  • When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)

Definition at line 982 of file Expr.cs.

982 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1275 of file Expr.cs.

1275 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 852 of file Expr.cs.

852 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1305 of file Expr.cs.

1305 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 864 of file Expr.cs.

864 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofTransitivityStar

bool IsProofTransitivityStar
get

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

Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. 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 885 of file Expr.cs.

885 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsProofTrue

bool IsProofTrue
get

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

Definition at line 811 of file Expr.cs.

811 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1078 of file Expr.cs.

1078 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRatNum

bool IsRatNum
get

Indicates whether the term is a real numeral.

Definition at line 237 of file Expr.cs.

237  {
238  get { return IsNumeral && IsReal; }
239  }
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:187
bool IsReal
Indicates whether the term is of sort real.
Definition: Expr.cs:347

◆ IsReal

bool IsReal
get

Indicates whether the term is of sort real.

Definition at line 347 of file Expr.cs.

347  {
348  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
349  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsRealIsInt

bool IsRealIsInt
get

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

Definition at line 429 of file Expr.cs.

429 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRealToInt

bool IsRealToInt
get

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

Definition at line 424 of file Expr.cs.

424 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRelation

bool IsRelation
get

Indicates whether the term is of relation sort.

Definition at line 1313 of file Expr.cs.

1313  {
1314  get
1315  {
1316  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1317  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
1318  == (uint)Z3_sort_kind.Z3_RELATION_SORT);
1319  }
1320  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

◆ IsRelationalJoin

bool IsRelationalJoin
get

Indicates whether the term is a relational join

Definition at line 1345 of file Expr.cs.

1345 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1427 of file Expr.cs.

1427 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRelationComplement

bool IsRelationComplement
get

Indicates whether the term is the complement of a relation

Definition at line 1405 of file Expr.cs.

1405 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Definition at line 1375 of file Expr.cs.

1375 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1391 of file Expr.cs.

1391 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1363 of file Expr.cs.

1363 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1400 of file Expr.cs.

1400 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1415 of file Expr.cs.

1415 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1330 of file Expr.cs.

1330 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 1351 of file Expr.cs.

1351 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRelationWiden

bool IsRelationWiden
get

Indicates whether the term is the widening of two relations

The function takes two arguments.

Definition at line 1357 of file Expr.cs.

1357 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsRemainder

bool IsRemainder
get

Indicates whether the term is remainder (binary)

Definition at line 409 of file Expr.cs.

409 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSelect

bool IsSelect
get

Indicates whether the term is an array select.

Definition at line 456 of file Expr.cs.

456 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSetComplement

bool IsSetComplement
get

Indicates whether the term is set complement

Definition at line 503 of file Expr.cs.

503 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSetDifference

bool IsSetDifference
get

Indicates whether the term is set difference

Definition at line 498 of file Expr.cs.

498 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSetIntersect

bool IsSetIntersect
get

Indicates whether the term is set intersection

Definition at line 493 of file Expr.cs.

493 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSetSubset

bool IsSetSubset
get

Indicates whether the term is set subset

Definition at line 508 of file Expr.cs.

508 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSetUnion

bool IsSetUnion
get

Indicates whether the term is set union

Definition at line 488 of file Expr.cs.

488 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ 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 451 of file Expr.cs.

451 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsSub

bool IsSub
get

Indicates whether the term is subtraction (binary)

Definition at line 384 of file Expr.cs.

384 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsTrue

bool IsTrue
get

Indicates whether the term is the constant true.

Definition at line 272 of file Expr.cs.

272 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsUMinus

bool IsUMinus
get

Indicates whether the term is a unary minus

Definition at line 389 of file Expr.cs.

389 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ IsWellSorted

bool IsWellSorted
get

Indicates whether the term is well-sorted.

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

Definition at line 196 of file Expr.cs.

196  {
197  get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
198  }

◆ IsXor

bool IsXor
get

Indicates whether the term is an exclusive or

Definition at line 312 of file Expr.cs.

312 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:156
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955

◆ NumArgs

uint NumArgs
get

The number of arguments of the expression.

Definition at line 71 of file Expr.cs.

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

◆ Sort

Sort Sort
get

The Sort of the term.

Definition at line 204 of file Expr.cs.

204  {
205  get
206  {
207  Contract.Ensures(Contract.Result<Sort>() != null);
208  return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
209  }
210  }
Sort Sort
The Sort of the term.
Definition: Expr.cs:204