RetroSearch Browse

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_quantifier.html below:

Z3: Quantifier Class Reference

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

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4