BoolExpr Class Reference

Boolean expressions. More...

Inheritance diagram for BoolExpr:

Static Public Member Functions
static BoolExpr	operator| (BoolExpr a, BoolExpr b)
	Disjunction of Boolean expressions.
static BoolExpr	operator& (BoolExpr a, BoolExpr b)
	Conjunction of Boolean expressions.
static BoolExpr	operator^ (BoolExpr a, BoolExpr b)
	Xor of Boolean expressions.
static BoolExpr	operator! (BoolExpr a)
	Negation.
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.

Additional Inherited Members
Public Member Functions inherited from Expr
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
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 inherited from Expr
	Expr (Context ctx, IntPtr obj)
	Constructor for Expr.
Properties inherited from Expr
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.

Detailed Description

Boolean expressions.

Definition at line 31 of file BoolExpr.cs.

Member Function Documentation

operator!()

static BoolExpr operator! ( BoolExpr  a )

inlinestatic

Negation.

Definition at line 49 of file BoolExpr.cs.

{ return a.Context.MkNot(a); }

operator&()

static BoolExpr operator& ( BoolExpr  a, BoolExpr  b  )

inlinestatic

Conjunction of Boolean expressions.

Definition at line 43 of file BoolExpr.cs.

{ return a.Context.MkAnd(a, b); }

operator^()

static BoolExpr operator^ ( BoolExpr  a, BoolExpr  b  )

inlinestatic

Xor of Boolean expressions.

Definition at line 46 of file BoolExpr.cs.

{ return a.Context.MkXor(a, b); }

operator|()

static BoolExpr operator| ( BoolExpr  a, BoolExpr  b  )

inlinestatic

Disjunction of Boolean expressions.

Definition at line 40 of file BoolExpr.cs.

{ return a.Context.MkOr(a, b); }