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.
Expr	Arg (uint i)
	The i'th argument of the expression.
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.
Expr	Substitute (Expr[] from, Expr[] to)
	Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
Expr	Substitute (Expr from, Expr to)
	Substitute every occurrence of from in the expression with to.
Expr	SubstituteVars (Expr[] to)
	Substitute the free variables in the expression with the expressions in to
Expr	SubstituteFuns (FuncDecl[] from, Expr[] to)
	Substitute functions in from with the expressions in to .
new Expr	Translate (Context ctx)
	Translates (copies) the term to the Context ctx .
Expr	Dup ()
	Create a duplicate of expression. This feature is to allow extending the life-time of expressions that were passed down as arguments by the user propagator callbacks. By default the life-time of arguments to callbacks is within the callback only.
override string	ToString ()
	Returns a string representation of the expression.
Public Member Functions inherited from AST
override bool	Equals (object o)
	Object comparison.
virtual int	CompareTo (object other)
	Object Comparison.
override int	GetHashCode ()
	The AST's hash code.
AST	Translate (Context ctx)
	Translates (copies) the AST to the Context ctx .
override string	ToString ()
	A string representation of the AST.
string	SExpr ()
	A string representation of the AST in s-expression notation.
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

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

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

Additional Inherited Members
Static Public Member Functions inherited from AST
static bool	operator== (AST a, AST b)
	Comparison operator.
static bool	operator!= (AST a, AST b)
	Comparison operator.

Detailed Description

Expressions are terms.

Definition at line 30 of file Expr.cs.

Constructor & Destructor Documentation

Expr()

Expr ( Context  ctx, IntPtr  obj  )

inlineprotected

Constructor for Expr.

Definition at line 1853 of file Expr.cs.

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

Member Function Documentation

Arg()

Expr Arg ( uint  i )

inline

The i'th argument of the expression.

Definition at line 93 of file Expr.cs.

        {
            return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
        }

Dup()

Expr Dup ( )

inline

Create a duplicate of expression. This feature is to allow extending the life-time of expressions that were passed down as arguments by the user propagator callbacks. By default the life-time of arguments to callbacks is within the callback only.

Definition at line 200 of file Expr.cs.

                          {
             return Expr.Create(Context, NativeObject);
        }

Simplify()

Expr Simplify ( Params  p = null )

inline

Returns a simplified version of the expression.

Parameters

p	A set of parameters to configure the simplifier

See also

Context.SimplifyHelp

Definition at line 37 of file Expr.cs.

        {
 
            if (p == null)
                return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject));
            else
                return Expr.Create(Context, Native.Z3_simplify_ex(Context.nCtx, NativeObject, p.NativeObject));
        }

Substitute() [1/2]

Expr Substitute ( Expr  from, Expr  to  )

inline

Substitute every occurrence of from in the expression with to.

See also

Substitute(Expr[],Expr[])

Definition at line 139 of file Expr.cs.

        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
 
            return Substitute(new Expr[] { from }, new Expr[] { to });
        }

Substitute() [2/2]

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

inline

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

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

Definition at line 121 of file Expr.cs.

        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
            Debug.Assert(from.All(f => f != null));
            Debug.Assert(to.All(t => t != null));
 
            Context.CheckContextMatch<Expr>(from);
            Context.CheckContextMatch<Expr>(to);
            if (from.Length != to.Length)
                throw new Z3Exception("Argument sizes do not match");
            return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
        }

Referenced by Expr.Substitute().

SubstituteFuns()

Expr SubstituteFuns ( FuncDecl[]  from, Expr[]  to  )

inline

Substitute functions in from with the expressions in to .

The expressions in to can have free variables. The free variable in to[i] at de-Bruijn index 0 refers to the first argument of from[i], the free variable at index 1 corresponds to the second argument, and so on. The arrays from and to must have the same size.

Definition at line 170 of file Expr.cs.

        {
            Debug.Assert(from != null);
            Debug.Assert(to != null);
            Debug.Assert(from.All(f => f != null));
            Debug.Assert(to.All(t => t != null));
 
            Context.CheckContextMatch<FuncDecl>(from);
            Context.CheckContextMatch<Expr>(to);
            if (from.Length != to.Length)
                throw new Z3Exception("Arrays 'from' and 'to' must have the same length");
            return Expr.Create(Context, Native.Z3_substitute_funs(Context.nCtx, NativeObject, (uint)from.Length, FuncDecl.ArrayToNative(from), Expr.ArrayToNative(to)));
        }

SubstituteVars()

Expr SubstituteVars ( Expr[]  to )

inline

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

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

Definition at line 153 of file Expr.cs.

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

ToString()

override string ToString ( )

inline

Returns a string representation of the expression.

Definition at line 207 of file Expr.cs.

        {
            return base.ToString();
        }

Translate()

new Expr Translate ( Context  ctx )

inline

Translates (copies) the term to the Context ctx .

Parameters

ctx

A context

Returns

A copy of the term which is associated with ctx

Definition at line 189 of file Expr.cs.

        {
            return (Expr)base.Translate(ctx);
        }

Referenced by Expr.Translate().

Update()

void Update ( Expr[]  args )

inline

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

Definition at line 102 of file Expr.cs.

        {
            Debug.Assert(args != null);
            Debug.Assert(args.All(a => a != null));
 
            Context.CheckContextMatch<Expr>(args);
            if (IsApp && args.Length != NumArgs)
                throw new Z3Exception("Number of arguments does not match");
            NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
        }

Property Documentation

Args

Expr [] Args

get

The arguments of the expression.

Definition at line 77 of file Expr.cs.

        {
            get
            {
 
                uint n = NumArgs;
                Expr[] res = new Expr[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
                return res;
            }
        }

AtLeastBound

uint AtLeastBound

get

Retrieve bound of at-least.

Definition at line 370 of file Expr.cs.

{ get { Debug.Assert(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }

AtMostBound

uint AtMostBound

get

Retrieve bound of at-most.

Definition at line 360 of file Expr.cs.

{ get { Debug.Assert(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }

BoolValue

Z3_lbool BoolValue

get

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

Definition at line 61 of file Expr.cs.

        {
            get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
        }

FuncDecl

FuncDecl FuncDecl

get

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

Definition at line 49 of file Expr.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
            }
        }

Referenced by Model.ConstInterp().

Index

uint Index

get

The de-Bruijn index of a bound variable.

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

abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
abs1(x, x, n) = b_n
abs1(y, x, n) = y
abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))

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

        {
            get
            {
                if (!IsVar)
                    throw new Z3Exception("Term is not a bound variable.");
 
                return Native.Z3_get_index_value(Context.nCtx, NativeObject);
            }
        }

IsAdd

bool IsAdd

get

Indicates whether the term is addition (binary)

Definition at line 434 of file Expr.cs.

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

IsAlgebraicNumber

bool IsAlgebraicNumber

get

Indicates whether the term is an algebraic number.

Definition at line 274 of file Expr.cs.

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

IsAnd

bool IsAnd

get

Indicates whether the term is an n-ary conjunction.

Definition at line 325 of file Expr.cs.

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

IsArithmeticNumeral

bool IsArithmeticNumeral

get

Indicates whether the term is an arithmetic numeral.

Definition at line 409 of file Expr.cs.

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

IsArray

bool IsArray

get

Indicates whether the term is of an array sort.

Definition at line 491 of file Expr.cs.

        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
                        (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                        == Z3_sort_kind.Z3_ARRAY_SORT);
            }
        }

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

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

IsAsArray

bool IsAsArray

get

Indicates whether the term is an as-array term.

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

Definition at line 536 of file Expr.cs.

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

IsAt

bool IsAt

get

Check whether expression is an at.

Returns

a Boolean

Definition at line 909 of file Expr.cs.

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

IsAtLeast

bool IsAtLeast

get

Indicates whether the term is at-least.

Definition at line 365 of file Expr.cs.

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

IsAtMost

bool IsAtMost

get

Indicates whether the term is at-most.

Definition at line 355 of file Expr.cs.

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

IsBool

bool IsBool

get

Indicates whether the term has Boolean sort.

Definition at line 286 of file Expr.cs.

        {
            get
            {
                return (IsExpr &&
                        Native.Z3_is_eq_sort(Context.nCtx,
                                              Native.Z3_mk_bool_sort(Context.nCtx),
                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
            }
        }

IsBV

bool IsBV

get

Indicates whether the terms is of bit-vector sort.

Definition at line 570 of file Expr.cs.

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

IsBVAdd

bool IsBVAdd

get

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

Definition at line 598 of file Expr.cs.

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

IsBVAND

bool IsBVAND

get

Indicates whether the term is a bit-wise AND.

Definition at line 703 of file Expr.cs.

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

IsBVBitOne

bool IsBVBitOne

get

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

Definition at line 583 of file Expr.cs.

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

IsBVBitZero

bool IsBVBitZero

get

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

Definition at line 588 of file Expr.cs.

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

IsBVCarry

bool IsBVCarry

get

Indicates whether the term is a bit-vector carry.

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

Definition at line 831 of file Expr.cs.

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

IsBVComp

bool IsBVComp

get

Indicates whether the term is a bit-vector comparison.

Definition at line 773 of file Expr.cs.

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

IsBVConcat

bool IsBVConcat

get

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

Definition at line 738 of file Expr.cs.

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

IsBVExtract

bool IsBVExtract

get

Indicates whether the term is a bit-vector extraction.

Definition at line 753 of file Expr.cs.

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

IsBVMul

bool IsBVMul

get

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

Definition at line 608 of file Expr.cs.

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

IsBVNAND

bool IsBVNAND

get

Indicates whether the term is a bit-wise NAND.

Definition at line 723 of file Expr.cs.

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

IsBVNOR

bool IsBVNOR

get

Indicates whether the term is a bit-wise NOR.

Definition at line 728 of file Expr.cs.

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

IsBVNOT

bool IsBVNOT

get

Indicates whether the term is a bit-wise NOT.

Definition at line 713 of file Expr.cs.

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

IsBVNumeral

bool IsBVNumeral

get

Indicates whether the term is a bit-vector numeral.

Definition at line 578 of file Expr.cs.

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

IsBVOR

bool IsBVOR

get

Indicates whether the term is a bit-wise OR.

Definition at line 708 of file Expr.cs.

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

IsBVReduceAND

bool IsBVReduceAND

get

Indicates whether the term is a bit-vector reduce AND.

Definition at line 768 of file Expr.cs.

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

IsBVReduceOR

bool IsBVReduceOR

get

Indicates whether the term is a bit-vector reduce OR.

Definition at line 763 of file Expr.cs.

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

IsBVRepeat

bool IsBVRepeat

get

Indicates whether the term is a bit-vector repetition.

Definition at line 758 of file Expr.cs.

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

IsBVRotateLeft

bool IsBVRotateLeft

get

Indicates whether the term is a bit-vector rotate left.

Definition at line 793 of file Expr.cs.

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

IsBVRotateLeftExtended

bool IsBVRotateLeftExtended

get

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

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

Definition at line 804 of file Expr.cs.

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

IsBVRotateRight

bool IsBVRotateRight

get

Indicates whether the term is a bit-vector rotate right.

Definition at line 798 of file Expr.cs.

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

IsBVRotateRightExtended

bool IsBVRotateRightExtended

get

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

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

Definition at line 810 of file Expr.cs.

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

IsBVSDiv

bool IsBVSDiv

get

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

Definition at line 613 of file Expr.cs.

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

IsBVSGE

bool IsBVSGE

get

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

Definition at line 678 of file Expr.cs.

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

IsBVSGT

bool IsBVSGT

get

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

Definition at line 698 of file Expr.cs.

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

IsBVShiftLeft

bool IsBVShiftLeft

get

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

Definition at line 778 of file Expr.cs.

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

IsBVShiftRightArithmetic

bool IsBVShiftRightArithmetic

get

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

Definition at line 788 of file Expr.cs.

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

IsBVShiftRightLogical

bool IsBVShiftRightLogical

get

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

Definition at line 783 of file Expr.cs.

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

IsBVSignExtension

bool IsBVSignExtension

get

Indicates whether the term is a bit-vector sign extension.

Definition at line 743 of file Expr.cs.

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

IsBVSLE

bool IsBVSLE

get

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

Definition at line 668 of file Expr.cs.

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

IsBVSLT

bool IsBVSLT

get

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

Definition at line 688 of file Expr.cs.

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

IsBVSMod

bool IsBVSMod

get

Indicates whether the term is a bit-vector signed modulus.

Definition at line 633 of file Expr.cs.

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

IsBVSRem

bool IsBVSRem

get

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

Definition at line 623 of file Expr.cs.

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

IsBVSub

bool IsBVSub

get

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

Definition at line 603 of file Expr.cs.

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

IsBVToInt

bool IsBVToInt

get

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

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

Definition at line 824 of file Expr.cs.

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

IsBVUDiv

bool IsBVUDiv

get

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

Definition at line 618 of file Expr.cs.

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

IsBVUGE

bool IsBVUGE

get

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

Definition at line 673 of file Expr.cs.

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

IsBVUGT

bool IsBVUGT

get

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

Definition at line 693 of file Expr.cs.

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

IsBVULE

bool IsBVULE

get

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

Definition at line 663 of file Expr.cs.

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

IsBVULT

bool IsBVULT

get

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

Definition at line 683 of file Expr.cs.

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

IsBVUMinus

bool IsBVUMinus

get

Indicates whether the term is a bit-vector unary minus.

Definition at line 593 of file Expr.cs.

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

IsBVURem

bool IsBVURem

get

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

Definition at line 628 of file Expr.cs.

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

IsBVXNOR

bool IsBVXNOR

get

Indicates whether the term is a bit-wise XNOR.

Definition at line 733 of file Expr.cs.

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

IsBVXOR

bool IsBVXOR

get

Indicates whether the term is a bit-wise XOR.

Definition at line 718 of file Expr.cs.

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

IsBVXOR3

bool IsBVXOR3

get

Indicates whether the term is a bit-vector ternary XOR.

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

Definition at line 837 of file Expr.cs.

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

IsBVZeroExtension

bool IsBVZeroExtension

get

Indicates whether the term is a bit-vector zero extension.

Definition at line 748 of file Expr.cs.

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

IsConcat

bool IsConcat

get

Check whether expression is a concatenation.

Returns

a Boolean

Definition at line 873 of file Expr.cs.

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

IsConst

bool IsConst

get

Indicates whether the term represents a constant.

Definition at line 244 of file Expr.cs.

        {
            get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
        }

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

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

IsContains

bool IsContains

get

Check whether expression is a contains.

Returns

a Boolean

Definition at line 891 of file Expr.cs.

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

IsDefaultArray

bool IsDefaultArray

get

Indicates whether the term is a default array.

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

Definition at line 523 of file Expr.cs.

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

IsDistinct

bool IsDistinct

get

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

Definition at line 315 of file Expr.cs.

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

IsDiv

bool IsDiv

get

Indicates whether the term is division (binary)

Definition at line 454 of file Expr.cs.

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

IsEmptyRelation

bool IsEmptyRelation

get

Indicates whether the term is an empty relation.

Definition at line 1427 of file Expr.cs.

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

IsEq

bool IsEq

get

Indicates whether the term is an equality predicate.

Definition at line 310 of file Expr.cs.

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

IsExtract

bool IsExtract

get

Check whether expression is an extract.

Returns

a Boolean

Definition at line 897 of file Expr.cs.

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

IsFalse

bool IsFalse

get

Indicates whether the term is the constant false.

Definition at line 305 of file Expr.cs.

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

IsFiniteDomain

bool IsFiniteDomain

get

Indicates whether the term is of an array sort.

Definition at line 1526 of file Expr.cs.

        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject)  != 0 &&
                        Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
            }
        }

IsFiniteDomainLT

bool IsFiniteDomainLT

get

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

Definition at line 1538 of file Expr.cs.

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

IsFP

bool IsFP

get

Indicates whether the terms is of floating-point sort.

Definition at line 1545 of file Expr.cs.

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

IsFPAbs

bool IsFPAbs

get

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

Definition at line 1691 of file Expr.cs.

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

IsFPAdd

bool IsFPAdd

get

Indicates whether the term is a floating-point addition term.

Definition at line 1660 of file Expr.cs.

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

IsFPDiv

bool IsFPDiv

get

Indicates whether the term is a floating-point division term.

Definition at line 1681 of file Expr.cs.

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

IsFPEq

bool IsFPEq

get

Indicates whether the term is a floating-point equality term.

Definition at line 1721 of file Expr.cs.

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

IsFPFMA

bool IsFPFMA

get

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

Definition at line 1706 of file Expr.cs.

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

IsFPFP

bool IsFPFP

get

Indicates whether the term is a floating-point constructor term.

Definition at line 1781 of file Expr.cs.

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

IsFPGe

bool IsFPGe

get

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

Definition at line 1741 of file Expr.cs.

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

IsFPGt

bool IsFPGt

get

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

Definition at line 1731 of file Expr.cs.

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

IsFPisInf

bool IsFPisInf

get

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

Definition at line 1751 of file Expr.cs.

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

IsFPisNaN

bool IsFPisNaN

get

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

Definition at line 1746 of file Expr.cs.

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

IsFPisNegative

bool IsFPisNegative

get

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

Definition at line 1771 of file Expr.cs.

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

IsFPisNormal

bool IsFPisNormal

get

Indicates whether the term is a floating-point isNormal term.

Definition at line 1761 of file Expr.cs.

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

IsFPisPositive

bool IsFPisPositive

get

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

Definition at line 1776 of file Expr.cs.

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

IsFPisSubnormal

bool IsFPisSubnormal

get

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

Definition at line 1766 of file Expr.cs.

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

IsFPisZero

bool IsFPisZero

get

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

Definition at line 1756 of file Expr.cs.

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

IsFPLe

bool IsFPLe

get

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

Definition at line 1736 of file Expr.cs.

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

IsFPLt

bool IsFPLt

get

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

Definition at line 1726 of file Expr.cs.

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

IsFPMax

bool IsFPMax

get

Indicates whether the term is a floating-point maximum term.

Definition at line 1701 of file Expr.cs.

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

IsFPMin

bool IsFPMin

get

Indicates whether the term is a floating-point minimum term.

Definition at line 1696 of file Expr.cs.

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

IsFPMinusInfinity

bool IsFPMinusInfinity

get

Indicates whether the term is a floating-point -oo.

Definition at line 1640 of file Expr.cs.

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

IsFPMinusZero

bool IsFPMinusZero

get

Indicates whether the term is a floating-point -zero.

Definition at line 1655 of file Expr.cs.

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

IsFPMul

bool IsFPMul

get

Indicates whether the term is a floating-point multiplication term.

Definition at line 1676 of file Expr.cs.

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

IsFPNaN

bool IsFPNaN

get

Indicates whether the term is a floating-point NaN.

Definition at line 1645 of file Expr.cs.

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

IsFPNeg

bool IsFPNeg

get

Indicates whether the term is a floating-point negation term.

Definition at line 1671 of file Expr.cs.

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

IsFPNumeral

bool IsFPNumeral

get

Indicates whether the term is a floating-point numeral.

Definition at line 1561 of file Expr.cs.

{ get { return IsFP && IsNumeral; } }

IsFPPlusInfinity

bool IsFPPlusInfinity

get

Indicates whether the term is a floating-point +oo.

Definition at line 1635 of file Expr.cs.

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

IsFPPlusZero

bool IsFPPlusZero

get

Indicates whether the term is a floating-point +zero

Definition at line 1650 of file Expr.cs.

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

IsFPRem

bool IsFPRem

get

Indicates whether the term is a floating-point remainder term.

Definition at line 1686 of file Expr.cs.

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

IsFPRM

bool IsFPRM

get

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

Definition at line 1553 of file Expr.cs.

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

IsFPRMExpr

bool IsFPRMExpr

get

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

Definition at line 1621 of file Expr.cs.

                               {
            get {
                return IsApp &&
                       (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
            }
        }

IsFPRMExprRNA

bool IsFPRMExprRNA

get

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

Definition at line 1601 of file Expr.cs.

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

IsFPRMExprRNE

bool IsFPRMExprRNE

get

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

Definition at line 1596 of file Expr.cs.

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

IsFPRMExprRTN

bool IsFPRMExprRTN

get

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

Definition at line 1606 of file Expr.cs.

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

IsFPRMExprRTP

bool IsFPRMExprRTP

get

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

Definition at line 1611 of file Expr.cs.

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

IsFPRMExprRTZ

bool IsFPRMExprRTZ

get

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

Definition at line 1616 of file Expr.cs.

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

IsFPRMNumeral

bool IsFPRMNumeral

get

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

Definition at line 1566 of file Expr.cs.

{ get { return IsFPRM && IsNumeral; } }

IsFPRMRoundNearestTiesToAway

bool IsFPRMRoundNearestTiesToAway

get

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

Definition at line 1576 of file Expr.cs.

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

IsFPRMRoundNearestTiesToEven

bool IsFPRMRoundNearestTiesToEven

get

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

Definition at line 1571 of file Expr.cs.

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

IsFPRMRoundTowardNegative

bool IsFPRMRoundTowardNegative

get

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

Definition at line 1581 of file Expr.cs.

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

IsFPRMRoundTowardPositive

bool IsFPRMRoundTowardPositive

get

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

Definition at line 1586 of file Expr.cs.

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

IsFPRMRoundTowardZero

bool IsFPRMRoundTowardZero

get

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

Definition at line 1591 of file Expr.cs.

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

IsFPRoundToIntegral

bool IsFPRoundToIntegral

get

Indicates whether the term is a floating-point roundToIntegral term.

Definition at line 1716 of file Expr.cs.

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

IsFPSqrt

bool IsFPSqrt

get

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

Definition at line 1711 of file Expr.cs.

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

IsFPSub

bool IsFPSub

get

Indicates whether the term is a floating-point subtraction term.

Definition at line 1666 of file Expr.cs.

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

IsFPToFp

bool IsFPToFp

get

Indicates whether the term is a floating-point conversion term.

Definition at line 1786 of file Expr.cs.

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

IsFPToFpUnsigned

bool IsFPToFpUnsigned

get

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

Definition at line 1791 of file Expr.cs.

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

IsFPToIEEEBV

bool IsFPToIEEEBV

get

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

Definition at line 1812 of file Expr.cs.

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

IsFPToReal

bool IsFPToReal

get

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

Definition at line 1806 of file Expr.cs.

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

IsFPToSBV

bool IsFPToSBV

get

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

Definition at line 1801 of file Expr.cs.

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

IsFPToUBV

bool IsFPToUBV

get

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

Definition at line 1796 of file Expr.cs.

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

IsGE

bool IsGE

get

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

Definition at line 419 of file Expr.cs.

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

IsGT

bool IsGT

get

Indicates whether the term is a greater-than.

Definition at line 429 of file Expr.cs.

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

IsIDiv

bool IsIDiv

get

Indicates whether the term is integer division (binary)

Definition at line 459 of file Expr.cs.

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

IsIff

bool IsIff

get

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

Definition at line 335 of file Expr.cs.

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

IsImplies

bool IsImplies

get

Indicates whether the term is an implication.

Definition at line 350 of file Expr.cs.

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

IsIndex

bool IsIndex

get

Check whether expression is a sequence index.

Returns

a Boolean

Definition at line 921 of file Expr.cs.

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

IsInt

bool IsInt

get

Indicates whether the term is of integer sort.

Definition at line 393 of file Expr.cs.

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

IsIntNum

bool IsIntNum

get

Indicates whether the term is an integer numeral.

Definition at line 254 of file Expr.cs.

        {
            get { return IsNumeral && IsInt; }
        }

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

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

IsIntToReal

bool IsIntToReal

get

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

Definition at line 474 of file Expr.cs.

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

IsIsEmptyRelation

bool IsIsEmptyRelation

get

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

Definition at line 1432 of file Expr.cs.

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

IsITE

bool IsITE

get

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

Definition at line 320 of file Expr.cs.

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

IsLabel

bool IsLabel

get

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

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

Definition at line 846 of file Expr.cs.

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

IsLabelLit

bool IsLabelLit

get

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

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

Definition at line 852 of file Expr.cs.

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

IsLE

bool IsLE

get

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

Definition at line 414 of file Expr.cs.

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

IsLength

bool IsLength

get

Check whether expression is a sequence length.

Returns

a Boolean

Definition at line 915 of file Expr.cs.

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

IsLT

bool IsLT

get

Indicates whether the term is a less-than.

Definition at line 424 of file Expr.cs.

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

IsModulus

bool IsModulus

get

Indicates whether the term is modulus (binary)

Definition at line 469 of file Expr.cs.

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

IsMul

bool IsMul

get

Indicates whether the term is multiplication (binary)

Definition at line 449 of file Expr.cs.

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

IsNot

bool IsNot

get

Indicates whether the term is a negation.

Definition at line 345 of file Expr.cs.

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

IsNumeral

bool IsNumeral

get

Indicates whether the term is a numeral.

Definition at line 215 of file Expr.cs.

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

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

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

IsOr

bool IsOr

get

Indicates whether the term is an n-ary disjunction.

Definition at line 330 of file Expr.cs.

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

IsPbEq

bool IsPbEq

get

Indicates whether the term is pbeq.

Definition at line 375 of file Expr.cs.

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

IsPbGe

bool IsPbGe

get

Indicates whether the term is pbge.

Definition at line 385 of file Expr.cs.

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

IsPbLe

bool IsPbLe

get

Indicates whether the term is pble.

Definition at line 380 of file Expr.cs.

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

IsPrefix

bool IsPrefix

get

Check whether expression is a prefix.

Returns

a Boolean

Definition at line 879 of file Expr.cs.

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

IsProofAndElimination

bool IsProofAndElimination

get

Indicates whether the term is a proof by elimination of AND.

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

Definition at line 1063 of file Expr.cs.

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

IsProofApplyDef

bool IsProofApplyDef

get

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

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

Definition at line 1292 of file Expr.cs.

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

IsProofAsserted

bool IsProofAsserted

get

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

Definition at line 942 of file Expr.cs.

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

IsProofCommutativity

bool IsProofCommutativity

get

Indicates whether the term is a proof by commutativity.

f is a commutative operator.

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

Definition at line 1223 of file Expr.cs.

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

IsProofDefAxiom

bool IsProofDefAxiom

get

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

Proof object used to justify Tseitin's like axioms:

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

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

Definition at line 1259 of file Expr.cs.

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

IsProofDefIntro

bool IsProofDefIntro

get

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

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

When e is of Boolean type:

or:

when e only occurs positively.

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

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

Definition at line 1282 of file Expr.cs.

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

IsProofDER

bool IsProofDER

get

Indicates whether the term is a proof for destructive equality resolution.

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

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Definition at line 1153 of file Expr.cs.

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

IsProofDistributivity

bool IsProofDistributivity

get

Indicates whether the term is a distributivity proof object.

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

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

Definition at line 1053 of file Expr.cs.

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

IsProofElimUnusedVars

bool IsProofElimUnusedVars

get

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

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

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

Definition at line 1139 of file Expr.cs.

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

IsProofGoal

bool IsProofGoal

get

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

Definition at line 947 of file Expr.cs.

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

IsProofHypothesis

bool IsProofHypothesis

get

Indicates whether the term is a hypothesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1167 of file Expr.cs.

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

IsProofIFFFalse

bool IsProofIFFFalse

get

Indicates whether the term is a proof by iff-false.

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

Definition at line 1210 of file Expr.cs.

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

IsProofIFFOEQ

bool IsProofIFFOEQ

get

Indicates whether the term is a proof iff-oeq.

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

Definition at line 1301 of file Expr.cs.

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

IsProofIFFTrue

bool IsProofIFFTrue

get

Indicates whether the term is a proof by iff-true.

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

Definition at line 1201 of file Expr.cs.

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

IsProofLemma

bool IsProofLemma

get

Indicates whether the term is a proof by lemma.

T1: false

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

Definition at line 1180 of file Expr.cs.

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

IsProofModusPonens

bool IsProofModusPonens

get

Indicates whether the term is proof via modus ponens.

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

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

Definition at line 958 of file Expr.cs.

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

IsProofModusPonensOEQ

bool IsProofModusPonensOEQ

get

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

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

Definition at line 1378 of file Expr.cs.

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

IsProofMonotonicity

bool IsProofMonotonicity

get

Indicates whether the term is a monotonicity proof object.

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

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

Definition at line 1025 of file Expr.cs.

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

IsProofNNFNeg

bool IsProofNNFNeg

get

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

Proof for a (negative) NNF step. Examples:

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

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

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

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

Definition at line 1354 of file Expr.cs.

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

IsProofNNFPos

bool IsProofNNFPos

get

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

Proof for a (positive) NNF step. Example:

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

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

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

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

Definition at line 1329 of file Expr.cs.

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

IsProofOrElimination

bool IsProofOrElimination

get

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

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

Definition at line 1073 of file Expr.cs.

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

IsProofPullQuant

bool IsProofPullQuant

get

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

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

Definition at line 1113 of file Expr.cs.

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

IsProofPushQuant

bool IsProofPushQuant

get

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

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

Definition at line 1127 of file Expr.cs.

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

IsProofQuantInst

bool IsProofQuantInst

get

Indicates whether the term is a proof for quantifier instantiation.

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

Definition at line 1161 of file Expr.cs.

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

IsProofQuantIntro

bool IsProofQuantIntro

get

Indicates whether the term is a quant-intro proof.

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

Definition at line 1035 of file Expr.cs.

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

IsProofReflexivity

bool IsProofReflexivity

get

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

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

Definition at line 967 of file Expr.cs.

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

IsProofRewrite

bool IsProofRewrite

get

Indicates whether the term is a proof by rewriting.

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

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

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

Definition at line 1092 of file Expr.cs.

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

IsProofRewriteStar

bool IsProofRewriteStar

get

Indicates whether the term is a proof by rewriting.

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

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

Definition at line 1105 of file Expr.cs.

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

IsProofSkolemize

bool IsProofSkolemize

get

Indicates whether the term is a proof for a Skolemization step.

Proof for:

This proof object has no antecedents.

Definition at line 1367 of file Expr.cs.

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

IsProofSymmetry

bool IsProofSymmetry

get

Indicates whether the term is proof by symmetricity of a relation.

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

Definition at line 978 of file Expr.cs.

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

IsProofTheoryLemma

bool IsProofTheoryLemma

get

Indicates whether the term is a proof for theory lemma.

Generic proof for theory lemmas.

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

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

Definition at line 1397 of file Expr.cs.

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

IsProofTransitivity

bool IsProofTransitivity

get

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

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

Definition at line 990 of file Expr.cs.

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

IsProofTransitivityStar

bool IsProofTransitivityStar

get

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

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

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

Definition at line 1011 of file Expr.cs.

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

IsProofTrue

bool IsProofTrue

get

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

Definition at line 937 of file Expr.cs.

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

IsProofUnitResolution

bool IsProofUnitResolution

get

Indicates whether the term is a proof by unit resolution.

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

Definition at line 1192 of file Expr.cs.

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

IsRatNum

bool IsRatNum

get

Indicates whether the term is a real numeral.

Definition at line 264 of file Expr.cs.

        {
            get { return IsNumeral && IsReal; }
        }

IsReal

bool IsReal

get

Indicates whether the term is of sort real.

Definition at line 401 of file Expr.cs.

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

IsRealIsInt

bool IsRealIsInt

get

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

Definition at line 484 of file Expr.cs.

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

IsRealToInt

bool IsRealToInt

get

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

Definition at line 479 of file Expr.cs.

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

IsRelation

bool IsRelation

get

Indicates whether the term is of relation sort.

Definition at line 1404 of file Expr.cs.

        {
            get
            {
                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
                        Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                        == (uint)Z3_sort_kind.Z3_RELATION_SORT);
            }
        }

IsRelationalJoin

bool IsRelationalJoin

get

Indicates whether the term is a relational join.

Definition at line 1437 of file Expr.cs.

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

IsRelationClone

bool IsRelationClone

get

Indicates whether the term is a relational clone (copy)

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

See also

IsRelationUnion

to perform destructive updates to the first argument.

Definition at line 1519 of file Expr.cs.

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

IsRelationComplement

bool IsRelationComplement

get

Indicates whether the term is the complement of a relation.

Definition at line 1497 of file Expr.cs.

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

IsRelationFilter

bool IsRelationFilter

get

Indicates whether the term is a relation filter.

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

Definition at line 1467 of file Expr.cs.

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

IsRelationNegationFilter

bool IsRelationNegationFilter

get

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

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

target = filter_by_negation(pos, neg, columns)

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

Definition at line 1483 of file Expr.cs.

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

IsRelationProject

bool IsRelationProject

get

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

The function takes one argument.

Definition at line 1455 of file Expr.cs.

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

IsRelationRename

bool IsRelationRename

get

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

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

Definition at line 1492 of file Expr.cs.

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

IsRelationSelect

bool IsRelationSelect

get

Indicates whether the term is a relational select.

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

Definition at line 1507 of file Expr.cs.

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

IsRelationStore

bool IsRelationStore

get

Indicates whether the term is an relation store.

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

Definition at line 1422 of file Expr.cs.

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

IsRelationUnion

bool IsRelationUnion

get

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

The function takes two arguments.

Definition at line 1443 of file Expr.cs.

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

IsRelationWiden

bool IsRelationWiden

get

Indicates whether the term is the widening of two relations.

The function takes two arguments.

Definition at line 1449 of file Expr.cs.

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

IsRemainder

bool IsRemainder

get

Indicates whether the term is remainder (binary)

Definition at line 464 of file Expr.cs.

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

IsReplace

bool IsReplace

get

Check whether expression is a replace.

Returns

a Boolean

Definition at line 903 of file Expr.cs.

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

IsSelect

bool IsSelect

get

Indicates whether the term is an array select.

Definition at line 511 of file Expr.cs.

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

IsSetComplement

bool IsSetComplement

get

Indicates whether the term is set complement.

Definition at line 558 of file Expr.cs.

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

IsSetDifference

bool IsSetDifference

get

Indicates whether the term is set difference.

Definition at line 553 of file Expr.cs.

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

IsSetIntersect

bool IsSetIntersect

get

Indicates whether the term is set intersection.

Definition at line 548 of file Expr.cs.

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

IsSetSubset

bool IsSetSubset

get

Indicates whether the term is set subset.

Definition at line 563 of file Expr.cs.

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

IsSetUnion

bool IsSetUnion

get

Indicates whether the term is set union.

Definition at line 543 of file Expr.cs.

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

IsStore

bool IsStore

get

Indicates whether the term is an array store.

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

Definition at line 506 of file Expr.cs.

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

IsString

bool IsString

get

Check whether expression is a string constant.

Returns

a Boolean

Definition at line 861 of file Expr.cs.

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

IsSub

bool IsSub

get

Indicates whether the term is subtraction (binary)

Definition at line 439 of file Expr.cs.

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

IsSuffix

bool IsSuffix

get

Check whether expression is a suffix.

Returns

a Boolean

Definition at line 885 of file Expr.cs.

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

IsTrue

bool IsTrue

get

Indicates whether the term is the constant true.

Definition at line 300 of file Expr.cs.

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

IsUMinus

bool IsUMinus

get

Indicates whether the term is a unary minus.

Definition at line 444 of file Expr.cs.

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

IsWellSorted

bool IsWellSorted

get

Indicates whether the term is well-sorted.

Returns

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

Definition at line 224 of file Expr.cs.

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

IsXor

bool IsXor

get

Indicates whether the term is an exclusive or.

Definition at line 340 of file Expr.cs.

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

NumArgs

uint NumArgs

get

The number of arguments of the expression.

Definition at line 69 of file Expr.cs.

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

Referenced by Expr.Update().

Sort

Sort Sort

get

The Sort of the term.

Definition at line 232 of file Expr.cs.

        {
            get
            {
                return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
            }
        }

String

string String

get

Retrieve string corresponding to string constant.

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

Definition at line 867 of file Expr.cs.

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