Arithmetic expressions (int/real) More...

Inheritance diagram for ArithExpr:

Protected Member Functions
	ArithExpr (Context ctx)
	Constructor for ArithExpr

Protected Member Functions inherited from Expr
	Expr (Context ctx)
	Constructor for Expr

	Expr (Context ctx, IntPtr obj)
	Constructor for Expr

Additional Inherited Members
Public Member Functions inherited from Expr
Expr	Simplify (Params p=null)
	Returns a simplified version 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 .

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

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.

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	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	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 eliminiation 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	IsProofPullQuantStar `[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 hypthesis 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	IsProofNNFStar `[get]`
	Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.

bool	IsProofCNFStar `[get]`
	Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.

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

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

Detailed Description

Arithmetic expressions (int/real)

Definition at line 1568 of file Expr.cs.

Constructor & Destructor Documentation

ArithExpr ( Context ctx )

inlineprotected

Constructor for ArithExpr

Definition at line 1572 of file Expr.cs.

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

Protected Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation