Inheritance diagram for Quantifier:

Public Member Functions
new Quantifier	Translate (Context ctx)
	Translates (copies) the quantifier to the Context ctx . More...

Public Member Functions inherited from Expr
Expr	Simplify (Params p=null)
	Returns a simplified version of the expression. More...

Expr	Arg (uint i)
	The i'th argument of the expression. More...

void	Update (Expr[] args)
	Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments. More...

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

Expr	Substitute (Expr from, Expr to)
	Substitute every occurrence of `from` in the expression with `to`. More...

Expr	SubstituteVars (Expr[] to)
	Substitute the free variables in the expression with the expressions in to More...

new Expr	Translate (Context ctx)
	Translates (copies) the term to the Context ctx . More...

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

override string	ToString ()
	Returns a string representation of the expression. More...

Public Member Functions inherited from AST
override bool	Equals (object o)
	Object comparison. More...

virtual int	CompareTo (object other)
	Object Comparison. More...

override int	GetHashCode ()
	The AST's hash code. More...

AST	Translate (Context ctx)
	Translates (copies) the AST to the Context ctx . More...

override string	ToString ()
	A string representation of the AST. More...

string	SExpr ()
	A string representation of the AST in s-expression notation. More...

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
bool	IsUniversal `[get]`
	Indicates whether the quantifier is universal. More...

bool	IsExistential `[get]`
	Indicates whether the quantifier is existential. More...

uint	Weight `[get]`
	The weight of the quantifier. More...

uint	NumPatterns `[get]`
	The number of patterns. More...

Pattern[]	Patterns `[get]`
	The patterns. More...

uint	NumNoPatterns `[get]`
	The number of no-patterns. More...

Pattern[]	NoPatterns `[get]`
	The no-patterns. More...

uint	NumBound `[get]`
	The number of bound variables. More...

Symbol[]	BoundVariableNames `[get]`
	The symbols for the bound variables. More...

Sort[]	BoundVariableSorts `[get]`
	The sorts of the bound variables. More...

Expr	Body `[get]`
	The body of the quantifier. More...

Properties inherited from Expr
FuncDecl	FuncDecl `[get]`
	The function declaration of the function that is applied in this expression. More...

Z3_lbool	BoolValue `[get]`
	Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF). More...

uint	NumArgs `[get]`
	The number of arguments of the expression. More...

Expr[]	Args `[get]`
	The arguments of the expression. More...

bool	IsNumeral `[get]`
	Indicates whether the term is a numeral More...

bool	IsWellSorted `[get]`
	Indicates whether the term is well-sorted. More...

Sort	Sort `[get]`
	The Sort of the term. More...

bool	IsConst `[get]`
	Indicates whether the term represents a constant. More...

bool	IsIntNum `[get]`
	Indicates whether the term is an integer numeral. More...

bool	IsRatNum `[get]`
	Indicates whether the term is a real numeral. More...

bool	IsAlgebraicNumber `[get]`
	Indicates whether the term is an algebraic number More...

bool	IsBool `[get]`
	Indicates whether the term has Boolean sort. More...

bool	IsTrue `[get]`
	Indicates whether the term is the constant true. More...

bool	IsFalse `[get]`
	Indicates whether the term is the constant false. More...

bool	IsEq `[get]`
	Indicates whether the term is an equality predicate. More...

bool	IsDistinct `[get]`
	Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). More...

bool	IsITE `[get]`
	Indicates whether the term is a ternary if-then-else term More...

bool	IsAnd `[get]`
	Indicates whether the term is an n-ary conjunction More...

bool	IsOr `[get]`
	Indicates whether the term is an n-ary disjunction More...

bool	IsIff `[get]`
	Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) More...

bool	IsXor `[get]`
	Indicates whether the term is an exclusive or More...

bool	IsNot `[get]`
	Indicates whether the term is a negation More...

bool	IsImplies `[get]`
	Indicates whether the term is an implication More...

bool	IsAtMost `[get]`
	Indicates whether the term is at-most More...

uint	AtMostBound `[get]`
	Retrieve bound of at-most More...

bool	IsAtLeast `[get]`
	Indicates whether the term is at-least More...

uint	AtLeastBound `[get]`
	Retrieve bound of at-least More...

bool	IsPbEq `[get]`
	Indicates whether the term is pbeq More...

bool	IsPbLe `[get]`
	Indicates whether the term is pble More...

bool	IsPbGe `[get]`
	Indicates whether the term is pbge More...

bool	IsInt `[get]`
	Indicates whether the term is of integer sort. More...

bool	IsReal `[get]`
	Indicates whether the term is of sort real. More...

bool	IsArithmeticNumeral `[get]`
	Indicates whether the term is an arithmetic numeral. More...

bool	IsLE `[get]`
	Indicates whether the term is a less-than-or-equal More...

bool	IsGE `[get]`
	Indicates whether the term is a greater-than-or-equal More...

bool	IsLT `[get]`
	Indicates whether the term is a less-than More...

bool	IsGT `[get]`
	Indicates whether the term is a greater-than More...

bool	IsAdd `[get]`
	Indicates whether the term is addition (binary) More...

bool	IsSub `[get]`
	Indicates whether the term is subtraction (binary) More...

bool	IsUMinus `[get]`
	Indicates whether the term is a unary minus More...

bool	IsMul `[get]`
	Indicates whether the term is multiplication (binary) More...

bool	IsDiv `[get]`
	Indicates whether the term is division (binary) More...

bool	IsIDiv `[get]`
	Indicates whether the term is integer division (binary) More...

bool	IsRemainder `[get]`
	Indicates whether the term is remainder (binary) More...

bool	IsModulus `[get]`
	Indicates whether the term is modulus (binary) More...

bool	IsIntToReal `[get]`
	Indicates whether the term is a coercion of integer to real (unary) More...

bool	IsRealToInt `[get]`
	Indicates whether the term is a coercion of real to integer (unary) More...

bool	IsRealIsInt `[get]`
	Indicates whether the term is a check that tests whether a real is integral (unary) More...

bool	IsArray `[get]`
	Indicates whether the term is of an array sort. More...

bool	IsStore `[get]`
	Indicates whether the term is an array store. More...

bool	IsSelect `[get]`
	Indicates whether the term is an array select. More...

bool	IsConstantArray `[get]`
	Indicates whether the term is a constant array. More...

bool	IsDefaultArray `[get]`
	Indicates whether the term is a default array. More...

bool	IsArrayMap `[get]`
	Indicates whether the term is an array map. More...

bool	IsAsArray `[get]`
	Indicates whether the term is an as-array term. More...

bool	IsSetUnion `[get]`
	Indicates whether the term is set union More...

bool	IsSetIntersect `[get]`
	Indicates whether the term is set intersection More...

bool	IsSetDifference `[get]`
	Indicates whether the term is set difference More...

bool	IsSetComplement `[get]`
	Indicates whether the term is set complement More...

bool	IsSetSubset `[get]`
	Indicates whether the term is set subset More...

bool	IsBV `[get]`
	Indicates whether the terms is of bit-vector sort. More...

bool	IsBVNumeral `[get]`
	Indicates whether the term is a bit-vector numeral More...

bool	IsBVBitOne `[get]`
	Indicates whether the term is a one-bit bit-vector with value one More...

bool	IsBVBitZero `[get]`
	Indicates whether the term is a one-bit bit-vector with value zero More...

bool	IsBVUMinus `[get]`
	Indicates whether the term is a bit-vector unary minus More...

bool	IsBVAdd `[get]`
	Indicates whether the term is a bit-vector addition (binary) More...

bool	IsBVSub `[get]`
	Indicates whether the term is a bit-vector subtraction (binary) More...

bool	IsBVMul `[get]`
	Indicates whether the term is a bit-vector multiplication (binary) More...

bool	IsBVSDiv `[get]`
	Indicates whether the term is a bit-vector signed division (binary) More...

bool	IsBVUDiv `[get]`
	Indicates whether the term is a bit-vector unsigned division (binary) More...

bool	IsBVSRem `[get]`
	Indicates whether the term is a bit-vector signed remainder (binary) More...

bool	IsBVURem `[get]`
	Indicates whether the term is a bit-vector unsigned remainder (binary) More...

bool	IsBVSMod `[get]`
	Indicates whether the term is a bit-vector signed modulus More...

bool	IsBVULE `[get]`
	Indicates whether the term is an unsigned bit-vector less-than-or-equal More...

bool	IsBVSLE `[get]`
	Indicates whether the term is a signed bit-vector less-than-or-equal More...

bool	IsBVUGE `[get]`
	Indicates whether the term is an unsigned bit-vector greater-than-or-equal More...

bool	IsBVSGE `[get]`
	Indicates whether the term is a signed bit-vector greater-than-or-equal More...

bool	IsBVULT `[get]`
	Indicates whether the term is an unsigned bit-vector less-than More...

bool	IsBVSLT `[get]`
	Indicates whether the term is a signed bit-vector less-than More...

bool	IsBVUGT `[get]`
	Indicates whether the term is an unsigned bit-vector greater-than More...

bool	IsBVSGT `[get]`
	Indicates whether the term is a signed bit-vector greater-than More...

bool	IsBVAND `[get]`
	Indicates whether the term is a bit-wise AND More...

bool	IsBVOR `[get]`
	Indicates whether the term is a bit-wise OR More...

bool	IsBVNOT `[get]`
	Indicates whether the term is a bit-wise NOT More...

bool	IsBVXOR `[get]`
	Indicates whether the term is a bit-wise XOR More...

bool	IsBVNAND `[get]`
	Indicates whether the term is a bit-wise NAND More...

bool	IsBVNOR `[get]`
	Indicates whether the term is a bit-wise NOR More...

bool	IsBVXNOR `[get]`
	Indicates whether the term is a bit-wise XNOR More...

bool	IsBVConcat `[get]`
	Indicates whether the term is a bit-vector concatenation (binary) More...

bool	IsBVSignExtension `[get]`
	Indicates whether the term is a bit-vector sign extension More...

bool	IsBVZeroExtension `[get]`
	Indicates whether the term is a bit-vector zero extension More...

bool	IsBVExtract `[get]`
	Indicates whether the term is a bit-vector extraction More...

bool	IsBVRepeat `[get]`
	Indicates whether the term is a bit-vector repetition More...

bool	IsBVReduceOR `[get]`
	Indicates whether the term is a bit-vector reduce OR More...

bool	IsBVReduceAND `[get]`
	Indicates whether the term is a bit-vector reduce AND More...

bool	IsBVComp `[get]`
	Indicates whether the term is a bit-vector comparison More...

bool	IsBVShiftLeft `[get]`
	Indicates whether the term is a bit-vector shift left More...

bool	IsBVShiftRightLogical `[get]`
	Indicates whether the term is a bit-vector logical shift right More...

bool	IsBVShiftRightArithmetic `[get]`
	Indicates whether the term is a bit-vector arithmetic shift left More...

bool	IsBVRotateLeft `[get]`
	Indicates whether the term is a bit-vector rotate left More...

bool	IsBVRotateRight `[get]`
	Indicates whether the term is a bit-vector rotate right More...

bool	IsBVRotateLeftExtended `[get]`
	Indicates whether the term is a bit-vector rotate left (extended) More...

bool	IsBVRotateRightExtended `[get]`
	Indicates whether the term is a bit-vector rotate right (extended) More...

bool	IsIntToBV `[get]`
	Indicates whether the term is a coercion from integer to bit-vector More...

bool	IsBVToInt `[get]`
	Indicates whether the term is a coercion from bit-vector to integer More...

bool	IsBVCarry `[get]`
	Indicates whether the term is a bit-vector carry More...

bool	IsBVXOR3 `[get]`
	Indicates whether the term is a bit-vector ternary XOR More...

bool	IsLabel `[get]`
	Indicates whether the term is a label (used by the Boogie Verification condition generator). More...

bool	IsLabelLit `[get]`
	Indicates whether the term is a label literal (used by the Boogie Verification condition generator). More...

bool	IsString `[get]`
	Check whether expression is a string constant. More...

string	String `[get]`
	Retrieve string corresponding to string constant. More...

bool	IsConcat `[get]`
	Check whether expression is a concatenation. More...

bool	IsPrefix `[get]`
	Check whether expression is a prefix. More...

bool	IsSuffix `[get]`
	Check whether expression is a suffix. More...

bool	IsContains `[get]`
	Check whether expression is a contains. More...

bool	IsExtract `[get]`
	Check whether expression is an extract. More...

bool	IsReplace `[get]`
	Check whether expression is a replace. More...

bool	IsAt `[get]`
	Check whether expression is an at. More...

bool	IsLength `[get]`
	Check whether expression is a sequence length. More...

bool	IsIndex `[get]`
	Check whether expression is a sequence index. More...

bool	IsOEQ `[get]`
	Indicates whether the term is a binary equivalence modulo namings. More...

bool	IsProofTrue `[get]`
	Indicates whether the term is a Proof for the expression 'true'. More...

bool	IsProofAsserted `[get]`
	Indicates whether the term is a proof for a fact asserted by the user. More...

bool	IsProofGoal `[get]`
	Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. More...

bool	IsProofModusPonens `[get]`
	Indicates whether the term is proof via modus ponens More...

bool	IsProofReflexivity `[get]`
	Indicates whether the term is a proof for (R t t), where R is a reflexive relation. More...

bool	IsProofSymmetry `[get]`
	Indicates whether the term is proof by symmetricity of a relation More...

bool	IsProofTransitivity `[get]`
	Indicates whether the term is a proof by transitivity of a relation More...

bool	IsProofTransitivityStar `[get]`
	Indicates whether the term is a proof by condensed transitivity of a relation More...

bool	IsProofMonotonicity `[get]`
	Indicates whether the term is a monotonicity proof object. More...

bool	IsProofQuantIntro `[get]`
	Indicates whether the term is a quant-intro proof More...

bool	IsProofDistributivity `[get]`
	Indicates whether the term is a distributivity proof object. More...

bool	IsProofAndElimination `[get]`
	Indicates whether the term is a proof by elimination of AND More...

bool	IsProofOrElimination `[get]`
	Indicates whether the term is a proof by elimination of not-or More...

bool	IsProofRewrite `[get]`
	Indicates whether the term is a proof by rewriting More...

bool	IsProofRewriteStar `[get]`
	Indicates whether the term is a proof by rewriting More...

bool	IsProofPullQuant `[get]`
	Indicates whether the term is a proof for pulling quantifiers out. More...

bool	IsProofPushQuant `[get]`
	Indicates whether the term is a proof for pushing quantifiers in. More...

bool	IsProofElimUnusedVars `[get]`
	Indicates whether the term is a proof for elimination of unused variables. More...

bool	IsProofDER `[get]`
	Indicates whether the term is a proof for destructive equality resolution More...

bool	IsProofQuantInst `[get]`
	Indicates whether the term is a proof for quantifier instantiation More...

bool	IsProofHypothesis `[get]`
	Indicates whether the term is a hypothesis marker. More...

bool	IsProofLemma `[get]`
	Indicates whether the term is a proof by lemma More...

bool	IsProofUnitResolution `[get]`
	Indicates whether the term is a proof by unit resolution More...

bool	IsProofIFFTrue `[get]`
	Indicates whether the term is a proof by iff-true More...

bool	IsProofIFFFalse `[get]`
	Indicates whether the term is a proof by iff-false More...

bool	IsProofCommutativity `[get]`
	Indicates whether the term is a proof by commutativity More...

bool	IsProofDefAxiom `[get]`
	Indicates whether the term is a proof for Tseitin-like axioms More...

bool	IsProofDefIntro `[get]`
	Indicates whether the term is a proof for introduction of a name More...

bool	IsProofApplyDef `[get]`
	Indicates whether the term is a proof for application of a definition More...

bool	IsProofIFFOEQ `[get]`
	Indicates whether the term is a proof iff-oeq More...

bool	IsProofNNFPos `[get]`
	Indicates whether the term is a proof for a positive NNF step More...

bool	IsProofNNFNeg `[get]`
	Indicates whether the term is a proof for a negative NNF step More...

bool	IsProofSkolemize `[get]`
	Indicates whether the term is a proof for a Skolemization step More...

bool	IsProofModusPonensOEQ `[get]`
	Indicates whether the term is a proof by modus ponens for equi-satisfiability. More...

bool	IsProofTheoryLemma `[get]`
	Indicates whether the term is a proof for theory lemma More...

bool	IsRelation `[get]`
	Indicates whether the term is of relation sort. More...

bool	IsRelationStore `[get]`
	Indicates whether the term is an relation store More...

bool	IsEmptyRelation `[get]`
	Indicates whether the term is an empty relation More...

bool	IsIsEmptyRelation `[get]`
	Indicates whether the term is a test for the emptiness of a relation More...

bool	IsRelationalJoin `[get]`
	Indicates whether the term is a relational join More...

bool	IsRelationUnion `[get]`
	Indicates whether the term is the union or convex hull of two relations. More...

bool	IsRelationWiden `[get]`
	Indicates whether the term is the widening of two relations More...

bool	IsRelationProject `[get]`
	Indicates whether the term is a projection of columns (provided as numbers in the parameters). More...

bool	IsRelationFilter `[get]`
	Indicates whether the term is a relation filter More...

bool	IsRelationNegationFilter `[get]`
	Indicates whether the term is an intersection of a relation with the negation of another. More...

bool	IsRelationRename `[get]`
	Indicates whether the term is the renaming of a column in a relation More...

bool	IsRelationComplement `[get]`
	Indicates whether the term is the complement of a relation More...

bool	IsRelationSelect `[get]`
	Indicates whether the term is a relational select More...

bool	IsRelationClone `[get]`
	Indicates whether the term is a relational clone (copy) More...

bool	IsFiniteDomain `[get]`
	Indicates whether the term is of an array sort. More...

bool	IsFiniteDomainLT `[get]`
	Indicates whether the term is a less than predicate over a finite domain. More...

bool	IsFP `[get]`
	Indicates whether the terms is of floating-point sort. More...

bool	IsFPRM `[get]`
	Indicates whether the terms is of floating-point rounding mode sort. More...

bool	IsFPNumeral `[get]`
	Indicates whether the term is a floating-point numeral More...

bool	IsFPRMNumeral `[get]`
	Indicates whether the term is a floating-point rounding mode numeral More...

bool	IsFPRMRoundNearestTiesToEven `[get]`
	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More...

bool	IsFPRMRoundNearestTiesToAway `[get]`
	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More...

bool	IsFPRMRoundTowardNegative `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardNegative More...

bool	IsFPRMRoundTowardPositive `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardPositive More...

bool	IsFPRMRoundTowardZero `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardZero More...

bool	IsFPRMExprRNE `[get]`
	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More...

bool	IsFPRMExprRNA `[get]`
	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More...

bool	IsFPRMExprRTN `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardNegative More...

bool	IsFPRMExprRTP `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardPositive More...

bool	IsFPRMExprRTZ `[get]`
	Indicates whether the term is the floating-point rounding numeral roundTowardZero More...

bool	IsFPRMExpr `[get]`
	Indicates whether the term is a floating-point rounding mode numeral More...

bool	IsFPPlusInfinity `[get]`
	Indicates whether the term is a floating-point +oo More...

bool	IsFPMinusInfinity `[get]`
	Indicates whether the term is a floating-point -oo More...

bool	IsFPNaN `[get]`
	Indicates whether the term is a floating-point NaN More...

bool	IsFPPlusZero `[get]`

bool	IsFPMinusZero `[get]`
	Indicates whether the term is a floating-point -zero More...

bool	IsFPAdd `[get]`
	Indicates whether the term is a floating-point addition term More...

bool	IsFPSub `[get]`
	Indicates whether the term is a floating-point subtraction term More...

bool	IsFPNeg `[get]`
	Indicates whether the term is a floating-point negation term More...

bool	IsFPMul `[get]`
	Indicates whether the term is a floating-point multiplication term More...

bool	IsFPDiv `[get]`
	Indicates whether the term is a floating-point division term More...

bool	IsFPRem `[get]`
	Indicates whether the term is a floating-point remainder term More...

bool	IsFPAbs `[get]`
	Indicates whether the term is a floating-point term absolute value term More...

bool	IsFPMin `[get]`
	Indicates whether the term is a floating-point minimum term More...

bool	IsFPMax `[get]`
	Indicates whether the term is a floating-point maximum term More...

bool	IsFPFMA `[get]`
	Indicates whether the term is a floating-point fused multiply-add term More...

bool	IsFPSqrt `[get]`
	Indicates whether the term is a floating-point square root term More...

bool	IsFPRoundToIntegral `[get]`
	Indicates whether the term is a floating-point roundToIntegral term More...

bool	IsFPEq `[get]`
	Indicates whether the term is a floating-point equality term More...

bool	IsFPLt `[get]`
	Indicates whether the term is a floating-point less-than term More...

bool	IsFPGt `[get]`
	Indicates whether the term is a floating-point greater-than term More...

bool	IsFPLe `[get]`
	Indicates whether the term is a floating-point less-than or equal term More...

bool	IsFPGe `[get]`
	Indicates whether the term is a floating-point greater-than or equal term More...

bool	IsFPisNaN `[get]`
	Indicates whether the term is a floating-point isNaN predicate term More...

bool	IsFPisInf `[get]`
	Indicates whether the term is a floating-point isInf predicate term More...

bool	IsFPisZero `[get]`
	Indicates whether the term is a floating-point isZero predicate term More...

bool	IsFPisNormal `[get]`
	Indicates whether the term is a floating-point isNormal term More...

bool	IsFPisSubnormal `[get]`
	Indicates whether the term is a floating-point isSubnormal predicate term More...

bool	IsFPisNegative `[get]`
	Indicates whether the term is a floating-point isNegative predicate term More...

bool	IsFPisPositive `[get]`
	Indicates whether the term is a floating-point isPositive predicate term More...

bool	IsFPFP `[get]`
	Indicates whether the term is a floating-point constructor term More...

bool	IsFPToFp `[get]`
	Indicates whether the term is a floating-point conversion term More...

bool	IsFPToFpUnsigned `[get]`
	Indicates whether the term is a floating-point conversion from unsigned bit-vector term More...

bool	IsFPToUBV `[get]`
	Indicates whether the term is a floating-point conversion to unsigned bit-vector term More...

bool	IsFPToSBV `[get]`
	Indicates whether the term is a floating-point conversion to signed bit-vector term More...

bool	IsFPToReal `[get]`
	Indicates whether the term is a floating-point conversion to real term More...

bool	IsFPToIEEEBV `[get]`
	Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term More...

uint	Index `[get]`
	The de-Bruijn index of a bound variable. More...

Properties inherited from AST
uint	Id `[get]`
	A unique identifier for the AST (unique among all ASTs). More...

Z3_ast_kind	ASTKind `[get]`
	The kind of the AST. More...

bool	IsExpr `[get]`
	Indicates whether the AST is an Expr More...

bool	IsApp `[get]`
	Indicates whether the AST is an application More...

bool	IsVar `[get]`
	Indicates whether the AST is a BoundVariable More...

bool	IsQuantifier `[get]`
	Indicates whether the AST is a Quantifier More...

bool	IsSort `[get]`
	Indicates whether the AST is a Sort More...

bool	IsFuncDecl `[get]`
	Indicates whether the AST is a FunctionDeclaration More...

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object More...

Additional Inherited Members
Static Public Member Functions inherited from BoolExpr
static BoolExpr	operator\| (BoolExpr a, BoolExpr b)
	Disjunction of Boolean expressions More...

static BoolExpr	operator& (BoolExpr a, BoolExpr b)
	Conjunction of Boolean expressions More...

static BoolExpr	operator^ (BoolExpr a, BoolExpr b)
	Xor of Boolean expressions More...

static BoolExpr	operator! (BoolExpr a)
	Negation More...

Static Public Member Functions inherited from AST
static bool	operator== (AST a, AST b)
	Comparison operator. More...

static bool	operator!= (AST a, AST b)
	Comparison operator. More...

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

Detailed Description

Quantifier expressions.

Definition at line 29 of file Quantifier.cs.

Member Function Documentation

◆ Translate()

new Quantifier Translate ( Context ctx )

inline

Translates (copies) the quantifier to the Context ctx .

Parameters

ctx A context

Returns: A copy of the quantifier which is associated with ctx

Definition at line 160 of file Quantifier.cs.

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

Referenced by Quantifier.Translate().

Property Documentation

◆ Body

Expr Body

get

The body of the quantifier.

Definition at line 146 of file Quantifier.cs.

         {
             get
             {
  
                 return Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
             }
         }

◆ BoundVariableNames

Symbol [] BoundVariableNames

get

The symbols for the bound variables.

Definition at line 114 of file Quantifier.cs.

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

◆ BoundVariableSorts

Sort [] BoundVariableSorts

get

The sorts of the bound variables.

Definition at line 130 of file Quantifier.cs.

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

◆ IsExistential

bool IsExistential

get

Indicates whether the quantifier is existential.

Definition at line 42 of file Quantifier.cs.

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

◆ IsUniversal

bool IsUniversal

get

Indicates whether the quantifier is universal.

Definition at line 34 of file Quantifier.cs.

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

◆ NoPatterns

Pattern [] NoPatterns

get

The no-patterns.

Definition at line 90 of file Quantifier.cs.

         {
             get
             {
  
                 uint n = NumNoPatterns;
                 Pattern[] res = new Pattern[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = new Pattern(Context, Native.Z3_get_quantifier_no_pattern_ast(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

◆ NumBound

uint NumBound

get

The number of bound variables.

Definition at line 106 of file Quantifier.cs.

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

◆ NumNoPatterns

uint NumNoPatterns

get

The number of no-patterns.

Definition at line 82 of file Quantifier.cs.

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

◆ NumPatterns

uint NumPatterns

get

The number of patterns.

Definition at line 58 of file Quantifier.cs.

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

◆ Patterns

Pattern [] Patterns

get

The patterns.

Definition at line 66 of file Quantifier.cs.

         {
             get
             {
  
                 uint n = NumPatterns;
                 Pattern[] res = new Pattern[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = new Pattern(Context, Native.Z3_get_quantifier_pattern_ast(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

◆ Weight

uint Weight

get

The weight of the quantifier.

Definition at line 50 of file Quantifier.cs.

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

Public Member Functions

Properties

Additional Inherited Members