Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Protected Member Functions | Properties
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.
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.

Protected Member Functions

internal Expr (Context ctx)
 Constructor for Expr.
internal 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 IsInterpolant [get]
 Indicates whether the term is marked for interpolation.
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

Expressions are terms.

Definition at line 29 of file Expr.cs.


Constructor & Destructor Documentation

internal Expr ( Context  ctx) [inline, protected]

Constructor for Expr.

Definition at line 1492 of file Expr.cs.

: base(ctx) { Contract.Requires(ctx != null); }
internal Expr ( Context  ctx,
IntPtr  obj 
) [inline, protected]

Constructor for Expr.

Definition at line 1496 of file Expr.cs.

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

Member Function Documentation

Expr Simplify ( Params  p = null) [inline]

Returns a simplified version of the expression.

Parameters:
pA set of parameters to configure the simplifier
See also:
Context.SimplifyHelp

Definition at line 36 of file Expr.cs.

        {
            Contract.Ensures(Contract.Result<Expr>() != null);

            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));
        }
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 115 of file Expr.cs.

        {
            Contract.Requires(from != null);
            Contract.Requires(to != null);
            Contract.Requires(Contract.ForAll(from, f => f != null));
            Contract.Requires(Contract.ForAll(to, t => t != null));
            Contract.Ensures(Contract.Result<Expr>() != null);

            Context.CheckContextMatch(from);
            Context.CheckContextMatch(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)));
        }
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 134 of file Expr.cs.

        {
            Contract.Requires(from != null);
            Contract.Requires(to != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            return Substitute(new Expr[] { from }, new Expr[] { to });
        }
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 149 of file Expr.cs.

        {
            Contract.Requires(to != null);
            Contract.Requires(Contract.ForAll(to, t => t != null));
            Contract.Ensures(Contract.Result<Expr>() != null);

            Context.CheckContextMatch(to);
            return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
        }
override string ToString ( ) [inline]

Returns a string representation of the expression.

Reimplemented from AST.

Definition at line 178 of file Expr.cs.

Referenced by Expr.ToString().

        {
            return base.ToString();
        }
new Expr Translate ( Context  ctx) [inline]

Translates (copies) the term to the Context ctx .

Parameters:
ctxA context
Returns:
A copy of the term which is associated with ctx

Reimplemented from AST.

Definition at line 164 of file Expr.cs.

        {
            Contract.Requires(ctx != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            if (ReferenceEquals(Context, ctx))
                return this;
            else
                return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
        }
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 96 of file Expr.cs.

        {
            Contract.Requires(args != null);
            Contract.Requires(Contract.ForAll(args, a => a != null));

            Context.CheckContextMatch(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

Expr [] Args [get]

The arguments of the expression.

Definition at line 79 of file Expr.cs.

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

Definition at line 63 of file Expr.cs.

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

Definition at line 50 of file Expr.cs.

Referenced by Model.ConstInterp().

uint Index [get]

The de-Burijn 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 1475 of file Expr.cs.

bool IsAdd [get]

Indicates whether the term is addition (binary)

Definition at line 383 of file Expr.cs.

bool IsAlgebraicNumber [get]

Indicates whether the term is an algebraic number.

Definition at line 247 of file Expr.cs.

bool IsAnd [get]

Indicates whether the term is an n-ary conjunction.

Definition at line 297 of file Expr.cs.

bool IsArithmeticNumeral [get]

Indicates whether the term is an arithmetic numeral.

Definition at line 358 of file Expr.cs.

bool IsArray [get]

Indicates whether the term is of an array sort.

Definition at line 441 of file Expr.cs.

bool IsArrayMap [get]

Indicates whether the term is an array map.

It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.

Definition at line 478 of file Expr.cs.

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

bool IsBool [get]

Indicates whether the term has Boolean sort.

Definition at line 259 of file Expr.cs.

bool IsBV [get]

Indicates whether the terms is of bit-vector sort.

Definition at line 520 of file Expr.cs.

bool IsBVAdd [get]

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

Definition at line 547 of file Expr.cs.

bool IsBVAND [get]

Indicates whether the term is a bit-wise AND.

Definition at line 652 of file Expr.cs.

bool IsBVBitOne [get]

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

Definition at line 532 of file Expr.cs.

bool IsBVBitZero [get]

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

Definition at line 537 of file Expr.cs.

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

bool IsBVComp [get]

Indicates whether the term is a bit-vector comparison.

Definition at line 722 of file Expr.cs.

bool IsBVConcat [get]

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

Definition at line 687 of file Expr.cs.

bool IsBVExtract [get]

Indicates whether the term is a bit-vector extraction.

Definition at line 702 of file Expr.cs.

bool IsBVMul [get]

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

Definition at line 557 of file Expr.cs.

bool IsBVNAND [get]

Indicates whether the term is a bit-wise NAND.

Definition at line 672 of file Expr.cs.

bool IsBVNOR [get]

Indicates whether the term is a bit-wise NOR.

Definition at line 677 of file Expr.cs.

bool IsBVNOT [get]

Indicates whether the term is a bit-wise NOT.

Definition at line 662 of file Expr.cs.

bool IsBVNumeral [get]

Indicates whether the term is a bit-vector numeral.

Definition at line 527 of file Expr.cs.

bool IsBVOR [get]

Indicates whether the term is a bit-wise OR.

Definition at line 657 of file Expr.cs.

bool IsBVReduceAND [get]

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

Definition at line 717 of file Expr.cs.

bool IsBVReduceOR [get]

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

Definition at line 712 of file Expr.cs.

bool IsBVRepeat [get]

Indicates whether the term is a bit-vector repetition.

Definition at line 707 of file Expr.cs.

bool IsBVRotateLeft [get]

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

Definition at line 742 of file Expr.cs.

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

bool IsBVRotateRight [get]

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

Definition at line 747 of file Expr.cs.

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

bool IsBVSDiv [get]

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

Definition at line 562 of file Expr.cs.

bool IsBVSGE [get]

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

Definition at line 627 of file Expr.cs.

bool IsBVSGT [get]

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

Definition at line 647 of file Expr.cs.

bool IsBVShiftLeft [get]

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

Definition at line 727 of file Expr.cs.

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

Definition at line 737 of file Expr.cs.

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

Definition at line 732 of file Expr.cs.

bool IsBVSignExtension [get]

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

Definition at line 692 of file Expr.cs.

bool IsBVSLE [get]

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

Definition at line 617 of file Expr.cs.

bool IsBVSLT [get]

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

Definition at line 637 of file Expr.cs.

bool IsBVSMod [get]

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

Definition at line 582 of file Expr.cs.

bool IsBVSRem [get]

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

Definition at line 572 of file Expr.cs.

bool IsBVSub [get]

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

Definition at line 552 of file Expr.cs.

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

bool IsBVUDiv [get]

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

Definition at line 567 of file Expr.cs.

bool IsBVUGE [get]

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

Definition at line 622 of file Expr.cs.

bool IsBVUGT [get]

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

Definition at line 642 of file Expr.cs.

bool IsBVULE [get]

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

Definition at line 612 of file Expr.cs.

bool IsBVULT [get]

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

Definition at line 632 of file Expr.cs.

bool IsBVUMinus [get]

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

Definition at line 542 of file Expr.cs.

bool IsBVURem [get]

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

Definition at line 577 of file Expr.cs.

bool IsBVXNOR [get]

Indicates whether the term is a bit-wise XNOR.

Definition at line 682 of file Expr.cs.

bool IsBVXOR [get]

Indicates whether the term is a bit-wise XOR.

Definition at line 667 of file Expr.cs.

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

bool IsBVZeroExtension [get]

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

Definition at line 697 of file Expr.cs.

bool IsConst [get]

Indicates whether the term represents a constant.

Definition at line 217 of file Expr.cs.

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

bool IsDefaultArray [get]

Indicates whether the term is a default array.

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

Definition at line 472 of file Expr.cs.

bool IsDistinct [get]

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

Definition at line 287 of file Expr.cs.

bool IsDiv [get]

Indicates whether the term is division (binary)

Definition at line 403 of file Expr.cs.

bool IsEmptyRelation [get]

Indicates whether the term is an empty relation.

Definition at line 1339 of file Expr.cs.

bool IsEq [get]

Indicates whether the term is an equality predicate.

Definition at line 282 of file Expr.cs.

bool IsFalse [get]

Indicates whether the term is the constant false.

Definition at line 277 of file Expr.cs.

bool IsFiniteDomain [get]

Indicates whether the term is of an array sort.

Definition at line 1439 of file Expr.cs.

bool IsFiniteDomainLT [get]

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

Definition at line 1450 of file Expr.cs.

bool IsGE [get]

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

Definition at line 368 of file Expr.cs.

bool IsGT [get]

Indicates whether the term is a greater-than.

Definition at line 378 of file Expr.cs.

bool IsIDiv [get]

Indicates whether the term is integer division (binary)

Definition at line 408 of file Expr.cs.

bool IsIff [get]

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

Definition at line 307 of file Expr.cs.

bool IsImplies [get]

Indicates whether the term is an implication.

Definition at line 322 of file Expr.cs.

bool IsInt [get]

Indicates whether the term is of integer sort.

Definition at line 339 of file Expr.cs.

bool IsInterpolant [get]

Indicates whether the term is marked for interpolation.

Definition at line 331 of file Expr.cs.

bool IsIntNum [get]

Indicates whether the term is an integer numeral.

Definition at line 227 of file Expr.cs.

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

bool IsIntToReal [get]

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

Definition at line 423 of file Expr.cs.

bool IsIsEmptyRelation [get]

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

Definition at line 1344 of file Expr.cs.

bool IsITE [get]

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

Definition at line 292 of file Expr.cs.

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

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

bool IsLE [get]

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

Definition at line 363 of file Expr.cs.

bool IsLT [get]

Indicates whether the term is a less-than.

Definition at line 373 of file Expr.cs.

bool IsModulus [get]

Indicates whether the term is modulus (binary)

Definition at line 418 of file Expr.cs.

bool IsMul [get]

Indicates whether the term is multiplication (binary)

Definition at line 398 of file Expr.cs.

bool IsNot [get]

Indicates whether the term is a negation.

Definition at line 317 of file Expr.cs.

bool IsNumeral [get]

Indicates whether the term is a numeral.

Definition at line 187 of file Expr.cs.

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

bool IsOr [get]

Indicates whether the term is an n-ary disjunction.

Definition at line 302 of file Expr.cs.

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) [and-elim T1]: l_i

Definition at line 941 of file Expr.cs.

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

bool IsProofAsserted [get]

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

Definition at line 820 of file Expr.cs.

bool IsProofCNFStar [get]

Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.

A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1266 of file Expr.cs.

Indicates whether the term is a proof by commutativity.

[comm]: (= (f a b) (f b a))

f is a commutative operator.

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

Definition at line 1113 of file Expr.cs.

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

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: [def-intro]: (and (or n (not e)) (or (not n) e))

or: [def-intro]: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))

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

Definition at line 1172 of file Expr.cs.

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

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

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

bool IsProofGoal [get]

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

Definition at line 825 of file Expr.cs.

bool IsProofHypothesis [get]

Indicates whether the term is a hypthesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1057 of file Expr.cs.

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

bool IsProofIFFOEQ [get]

Indicates whether the term is a proof iff-oeq.

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

Definition at line 1191 of file Expr.cs.

bool IsProofIFFTrue [get]

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

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

Definition at line 1091 of file Expr.cs.

bool IsProofLemma [get]

Indicates whether the term is a proof by lemma.

T1: false [lemma T1]: (or (not l_1) ... (not l_n))

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

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) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).

Definition at line 836 of file Expr.cs.

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) [mp~ T1 T2]: q

Definition at line 1290 of file Expr.cs.

bool IsProofMonotonicity [get]

Indicates whether the term is a monotonicity proof object.

T1: (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space.

Definition at line 903 of file Expr.cs.

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 [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... 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' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))

Definition at line 1244 of file Expr.cs.

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' [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_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 [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) 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 1219 of file Expr.cs.

bool IsProofNNFStar [get]

Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.

A proof for (~ P Q) where Q is in negation normal form.

This proof object is only used if the parameter PROOF_MODE is 1.

This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1256 of file Expr.cs.

Indicates whether the term is a proof by eliminiation 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 951 of file Expr.cs.

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

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

A proof for (iff P Q) where Q is in prenex normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents

Definition at line 1004 of file Expr.cs.

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

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

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) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))

Definition at line 913 of file Expr.cs.

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

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

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 is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are:

  • When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
  • When converting bit-vectors to Booleans (BIT2BOOL=true)
  • When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)

Definition at line 986 of file Expr.cs.

bool IsProofSkolemize [get]

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

Proof for:

[sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x (p x y)) (p (sk y) y))

This proof object has no antecedents.

Definition at line 1279 of file Expr.cs.

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

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

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

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

Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. 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 889 of file Expr.cs.

bool IsProofTrue [get]

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

Definition at line 815 of file Expr.cs.

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

bool IsRatNum [get]

Indicates whether the term is a real numeral.

Definition at line 237 of file Expr.cs.

bool IsReal [get]

Indicates whether the term is of sort real.

Definition at line 351 of file Expr.cs.

bool IsRealIsInt [get]

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

Definition at line 433 of file Expr.cs.

bool IsRealToInt [get]

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

Definition at line 428 of file Expr.cs.

bool IsRelation [get]

Indicates whether the term is of an array sort.

Definition at line 1317 of file Expr.cs.

bool IsRelationalJoin [get]

Indicates whether the term is a relational join.

Definition at line 1349 of file Expr.cs.

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

Indicates whether the term is the complement of a relation.

Definition at line 1409 of file Expr.cs.

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-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Definition at line 1379 of file Expr.cs.

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

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

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

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

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

bool IsRelationUnion [get]

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

The function takes two arguments.

Definition at line 1355 of file Expr.cs.

bool IsRelationWiden [get]

Indicates whether the term is the widening of two relations.

The function takes two arguments.

Definition at line 1361 of file Expr.cs.

bool IsRemainder [get]

Indicates whether the term is remainder (binary)

Definition at line 413 of file Expr.cs.

bool IsSelect [get]

Indicates whether the term is an array select.

Definition at line 460 of file Expr.cs.

bool IsSetComplement [get]

Indicates whether the term is set complement.

Definition at line 507 of file Expr.cs.

bool IsSetDifference [get]

Indicates whether the term is set difference.

Definition at line 502 of file Expr.cs.

bool IsSetIntersect [get]

Indicates whether the term is set intersection.

Definition at line 497 of file Expr.cs.

bool IsSetSubset [get]

Indicates whether the term is set subset.

Definition at line 512 of file Expr.cs.

bool IsSetUnion [get]

Indicates whether the term is set union.

Definition at line 492 of file Expr.cs.

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

bool IsSub [get]

Indicates whether the term is subtraction (binary)

Definition at line 388 of file Expr.cs.

bool IsTrue [get]

Indicates whether the term is the constant true.

Definition at line 272 of file Expr.cs.

bool IsUMinus [get]

Indicates whether the term is a unary minus.

Definition at line 393 of file Expr.cs.

bool IsWellSorted [get]

Indicates whether the term is well-sorted.

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

Definition at line 196 of file Expr.cs.

bool IsXor [get]

Indicates whether the term is an exclusive or.

Definition at line 312 of file Expr.cs.

uint NumArgs [get]

The number of arguments of the expression.

Definition at line 71 of file Expr.cs.

Sort Sort [get]

The Sort of the term.

Definition at line 204 of file Expr.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines