@c BEGIN AUTO-GENERATED INVARIANTS LISTING
@c Automatically generated by class daikon.config.InvariantDoclet


@item AndJoiner
This is a special invariant used internally by Daikon to represent an antecedent invariant in an
implication where that antecedent consists of two invariants anded together.

@item CommonFloatSequence
Represents sequences of double values that contain a common subset. Prints as
@code{@{e1, e2, e3, ...@} subset of x[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.CommonFloatSequence.enabled}.

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.CommonFloatSequence.hashcode_seqs}
    @end itemize

@item CommonSequence
Represents sequences of long values that contain a common subset. Prints as
@code{@{e1, e2, e3, ...@} subset of x[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.CommonSequence.enabled}.

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.CommonSequence.hashcode_seqs}
    @end itemize

@item CommonStringSequence
Represents string sequences that contain a common subset. Prints as @code{@{s1, s2, s3, ...@}
 subset of x[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.stringsequence.CommonStringSequence.enabled}.

@item CompleteOneOfScalar
Tracks every unique value and how many times it occurs. Prints as either @code{x has no values}
or as @code{x has values: v1 v2 v3 ...}. The set has no maximum size; it may be arbitrarily
large.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.scalar.CompleteOneOfScalar.enabled}.

@item CompleteOneOfString
Tracks every unique value and how many times it occurs. Prints as either @code{x has no values}
or as @code{x has values: "v1" "v2" "v3" ...}. The set has no maximum size; it may be
arbitrarily large.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.string.CompleteOneOfString.enabled}.

@item DummyInvariant
This is a special invariant used internally by Daikon to represent invariants whose meaning
Daikon doesn't understand. The only operation that can be performed on a DummyInvariant is to
print it. In particular, the invariant cannot be tested against a sample: the invariant is always
assumed to hold and is always considered to be statistically justified.

The main use for a dummy invariant is to represent a splitting condition that appears in a
@code{.spinfo} file. The @code{.spinfo} file can indicate an arbitrary Java expression, which
might not be equivalent to any invariant in Daikon's grammar.

Ordinarily, Daikon uses splitting conditions to split data, then seeks to use that split data
to form conditional invariants out of its standard built-in invariants. If you wish the
expression in the .spinfo file to be printed as an invariant, whether or not it is itself
discovered by Daikon during invariant detection, then the configuration option @code{daikon.split.PptSplitter.dummy_invariant_level} must be set, and formatting information must be
supplied in the splitter info file.

@item EltLowerBound
Represents the invariant that each element of a sequence of long values is greater than or
equal to a constant. Prints as @code{x[] elements >= c}.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltLowerBound.minimal_interesting}
    @item @samp{daikon.inv.unary.sequence.EltLowerBound.maximal_interesting}
    @end itemize

@item EltLowerBoundFloat
Represents the invariant that each element of a sequence of double values is greater than or
equal to a constant. Prints as @code{x[] elements >= c}.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltLowerBoundFloat.minimal_interesting}
    @item @samp{daikon.inv.unary.sequence.EltLowerBoundFloat.maximal_interesting}
    @end itemize

@item EltNonZero
Represents the invariant "x != 0" where x represents all of the elements of a sequence of
long. Prints as @code{x[] elements != 0}.

@item EltNonZeroFloat
Represents the invariant "x != 0" where x represents all of the elements of a sequence of
double. Prints as @code{x[] elements != 0}.

@item EltOneOf
Represents sequences of long values where the elements of the sequence take on only a
few distinct values. Prints as either @code{x[] elements == c} (when there is only one value),
or as @code{x[] elements one of @{c1, c2, c3@}} (when there are multiple values).

May print as @code{x[] elements has only one value} when @code{x} is an array of hashcodes
(pointers) -- this is because the numerical value of the hashcode (pointer) is uninteresting.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltOneOf.size}
    @item @samp{daikon.inv.unary.sequence.EltOneOf.omit_hashcode_values_Simplify}
    @end itemize

@item EltOneOfFloat
Represents sequences of double values where the elements of the sequence take on only a
few distinct values. Prints as either @code{x[] elements == c} (when there is only one value),
or as @code{x[] elements one of @{c1, c2, c3@}} (when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltOneOfFloat.size}
    @end itemize

@item EltOneOfString
Represents sequences of String values where the elements of the sequence take on only a
few distinct values. Prints as either @code{x[] elements == c} (when there is only one value),
or as @code{x[] elements one of @{c1, c2, c3@}} (when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.stringsequence.EltOneOfString.size}
    @end itemize

@item EltRangeFloat.EqualMinusOne
Internal invariant representing double scalars that are equal to minus one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeFloat.EqualOne
Internal invariant representing double scalars that are equal to one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeFloat.EqualZero
Internal invariant representing double scalars that are equal to zero. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeFloat.GreaterEqual64
Internal invariant representing double scalars that are greater than or equal to 64. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item EltRangeFloat.GreaterEqualZero
Internal invariant representing double scalars that are greater than or equal to 0. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item EltRangeInt.BooleanVal
Internal invariant representing longs whose values are always 0 or 1. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeInt.Bound0_63
Internal invariant representing longs whose values are between 0 and 63. Used for
non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item EltRangeInt.EqualMinusOne
Internal invariant representing long scalars that are equal to minus one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeInt.EqualOne
Internal invariant representing long scalars that are equal to one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeInt.EqualZero
Internal invariant representing long scalars that are equal to zero. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item EltRangeInt.Even
Invariant representing longs whose values are always even. Used for non-instantiating
suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints
as @code{x is even}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.EltRangeInt.Even.enabled}.

@item EltRangeInt.GreaterEqual64
Internal invariant representing long scalars that are greater than or equal to 64. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item EltRangeInt.GreaterEqualZero
Internal invariant representing long scalars that are greater than or equal to 0. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item EltRangeInt.PowerOfTwo
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf
invariants it is printed. Prints as @code{x is a power of 2}.

@item EltUpperBound
Represents the invariant that each element of a sequence of long values is less than or
equal to a constant. Prints as @code{x[] elements <= c}.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltUpperBound.minimal_interesting}
    @item @samp{daikon.inv.unary.sequence.EltUpperBound.maximal_interesting}
    @end itemize

@item EltUpperBoundFloat
Represents the invariant that each element of a sequence of double values is less than or
equal to a constant. Prints as @code{x[] elements <= c}.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.EltUpperBoundFloat.minimal_interesting}
    @item @samp{daikon.inv.unary.sequence.EltUpperBoundFloat.maximal_interesting}
    @end itemize

@item EltwiseFloatEqual
Represents equality between adjacent elements (x[i], x[i+1]) of a double sequence. Prints as
@code{x[] elements are equal}.

@item EltwiseFloatGreaterEqual
Represents the invariant >= between adjacent elements
(x[i], x[i+1]) of a double sequence. Prints as
@code{x[] sorted by >=}.

@item EltwiseFloatGreaterThan
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a double sequence. Prints as
@code{x[] sorted by >}.

@item EltwiseFloatLessEqual
Represents the invariant <= between adjacent elements
(x[i], x[i+1]) of a double sequence. Prints as
@code{x[] sorted by <=}.

@item EltwiseFloatLessThan
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a double sequence. Prints as
@code{x[] sorted by <}.

@item EltwiseIntEqual
Represents equality between adjacent elements (x[i], x[i+1]) of a long sequence. Prints as
@code{x[] elements are equal}.

@item EltwiseIntGreaterEqual
Represents the invariant >= between adjacent elements
(x[i], x[i+1]) of a long sequence. Prints as
@code{x[] sorted by >=}.

@item EltwiseIntGreaterThan
Represents the invariant > between adjacent elements
(x[i], x[i+1]) of a long sequence. Prints as
@code{x[] sorted by >}.

@item EltwiseIntLessEqual
Represents the invariant <= between adjacent elements
(x[i], x[i+1]) of a long sequence. Prints as
@code{x[] sorted by <=}.

@item EltwiseIntLessThan
Represents the invariant < between adjacent elements
(x[i], x[i+1]) of a long sequence. Prints as
@code{x[] sorted by <}.

@item Equality
Keeps track of sets of variables that are equal. Other invariants are instantiated for only one
member of the Equality set, the leader. If variables @code{x}, @code{y}, and @code{z} are
members of the Equality set and @code{x} is chosen as the leader, then the Equality will
internally convert into binary comparison invariants that print as @code{x == y} and @code{x ==
 z}.

@item FloatEqual
Represents an invariant of == between two double scalars. Prints as @code{x == y}.

@item FloatGreaterEqual
Represents an invariant of >= between two double scalars. Prints as @code{x >= y}.

@item FloatGreaterThan
Represents an invariant of > between two double scalars. Prints as @code{x > y}.

@item FloatLessEqual
Represents an invariant of <= between two double scalars. Prints as @code{x <= y}.

@item FloatLessThan
Represents an invariant of < between two double scalars. Prints as @code{x < y}.

@item FloatNonEqual
Represents an invariant of != between two double scalars. Prints as @code{x != y}.

@item FunctionBinary.BitwiseAndLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = BitwiseAnd(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.BitwiseOrLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = BitwiseOr(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.BitwiseXorLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = BitwiseXor(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.DivisionLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = Division(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinary.GcdLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Gcd(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.LogicalAndLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = LogicalAnd(y, z)} over three long
scalars. For logical operations, Daikon treats 0 as false and all other values as true.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.LogicalOrLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = LogicalOr(y, z)} over three long
scalars. For logical operations, Daikon treats 0 as false and all other values as true.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.LogicalXorLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = LogicalXor(y, z)} over three long
scalars. For logical operations, Daikon treats 0 as false and all other values as true.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.LshiftLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = Lshift(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinary.MaximumLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Maximum(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.MinimumLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Minimum(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.ModLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = Mod(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinary.MultiplyLong_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Multiply(y, z)} over three long
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinary.PowerLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = Power(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinary.RshiftSignedLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = RshiftSigned(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinary.RshiftUnsignedLong_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = RshiftUnsigned(y, z)} over three long
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinaryFloat.DivisionDouble_@{xyz, xzy, yxz, yzx, zxy, zyx@}
Represents the invariant @code{x = Division(y, z)} over three double
scalars.
Since the function is non-symmetric, all six permutations of the variables are checked.

@item FunctionBinaryFloat.MaximumDouble_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Maximum(y, z)} over three double
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinaryFloat.MinimumDouble_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Minimum(y, z)} over three double
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item FunctionBinaryFloat.MultiplyDouble_@{xyz, yxz, zxy@}
Represents the invariant @code{x = Multiply(y, z)} over three double
scalars.
Since the function is symmetric, only the permutations xyz, yxz, and zxy are checked.

@item GuardingImplication
This is a special implication invariant that guards any invariants that are over variables that
are sometimes missing. For example, if the invariant @code{a.x = 0} is true, the guarded
implication is @code{a != null => a.x = 0}.

@item Implication
The Implication invariant class is used internally within Daikon to handle invariants that are
only true when certain other conditions are also true (splitting).

@item IntEqual
Represents an invariant of == between two long scalars. Prints as @code{x == y}.

@item IntGreaterEqual
Represents an invariant of >= between two long scalars. Prints as @code{x >= y}.

@item IntGreaterThan
Represents an invariant of > between two long scalars. Prints as @code{x > y}.

@item IntLessEqual
Represents an invariant of <= between two long scalars. Prints as @code{x <= y}.

@item IntLessThan
Represents an invariant of < between two long scalars. Prints as @code{x < y}.

@item IntNonEqual
Represents an invariant of != between two long scalars. Prints as @code{x != y}.

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.binary.twoScalar.IntNonEqual.integral_only}
    @end itemize

@item IsPointer
IsPointer is an invariant that heuristically determines whether an integer represents a pointer
(a 32-bit memory address). Since both a 32-bit integer and an address have the same
representation, sometimes a a pointer can be mistaken for an integer. When this happens, several
scalar invariants are computed for integer variables. Most of them would not make any sense for
pointers. Determining whether a 32-bit variable is a pointer can thus spare the computation of
many irrelevant invariants.

The basic approach is to discard the invariant if any values that are not valid pointers are
encountered. By default values between -100,000 and 100,000 (except 0) are considered to be
invalid pointers. This approach has been experimentally confirmed on Windows x86 executables.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.scalar.IsPointer.enabled}.

@item LinearBinary
Represents a Linear invariant between two long scalars @code{x} and @code{y}, of
the form @code{ax + by + c = 0}. The constants @code{a}, @code{b} and
@code{c} are mutually relatively prime, and the constant @code{a} is always positive.

@item LinearBinaryFloat
Represents a Linear invariant between two double scalars @code{x} and @code{y}, of
the form @code{ax + by + c = 0}. The constants @code{a}, @code{b} and
@code{c} are mutually relatively prime, and the constant @code{a} is always positive.

@item LinearTernary
Represents a Linear invariant over three long scalars @code{x},
@code{y}, and @code{z}, of the form
@code{ax + by + cz + d = 0}.
The constants @code{a}, @code{b}, @code{c}, and
@code{d} are mutually relatively prime, and the constant
@code{a} is always positive.

@item LinearTernaryFloat
Represents a Linear invariant over three double scalars @code{x},
@code{y}, and @code{z}, of the form
@code{ax + by + cz + d = 0}.
The constants @code{a}, @code{b}, @code{c}, and
@code{d} are mutually relatively prime, and the constant
@code{a} is always positive.

@item LowerBound
Represents the invariant @code{x >= c}, where @code{c} is a constant and
@code{x} is a long scalar.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.LowerBound.minimal_interesting}
    @item @samp{daikon.inv.unary.scalar.LowerBound.maximal_interesting}
    @end itemize

@item LowerBoundFloat
Represents the invariant @code{x >= c}, where @code{c} is a constant and
@code{x} is a double scalar.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.LowerBoundFloat.minimal_interesting}
    @item @samp{daikon.inv.unary.scalar.LowerBoundFloat.maximal_interesting}
    @end itemize

@item Member
Represents long scalars that are always members of a sequence of long values. Prints as
@code{x in y[]} where @code{x} is a long scalar and @code{y[]} is a sequence
of long.

@item MemberFloat
Represents double scalars that are always members of a sequence of double values. Prints as
@code{x in y[]} where @code{x} is a double scalar and @code{y[]} is a sequence
of double.

@item MemberString
Represents String scalars that are always members of a sequence of String values. Prints as
@code{x in y[]} where @code{x} is a String scalar and @code{y[]} is a sequence
of String.

@item Modulus
Represents the invariant @code{x == r (mod m)} where @code{x} is a long scalar variable, @code{r} is the (constant) remainder, and @code{m} is the (constant) modulus.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.scalar.Modulus.enabled}.

@item NoDuplicates
Represents sequences of long that contain no duplicate elements. Prints as
@code{x[] contains no duplicates}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.NoDuplicates.enabled}.

@item NoDuplicatesFloat
Represents sequences of double that contain no duplicate elements. Prints as
@code{x[] contains no duplicates}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.NoDuplicatesFloat.enabled}.

@item NonModulus
Represents long scalars that are never equal to @code{r (mod m)} where all other numbers in the
same range (i.e., all the values that @code{x} doesn't take from @code{min(x)} to @code{max(x)}) are equal to @code{r (mod m)}. Prints as @code{x != r (mod m)}, where @code{r} is the
remainder and @code{m} is the modulus.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.scalar.NonModulus.enabled}.

@item NonZero
Represents long scalars that are non-zero. Prints as @code{x != 0}, or as @code{x !=
 null} for pointer types.

@item NonZeroFloat
Represents double scalars that are non-zero. Prints as @code{x != 0}.

@item NumericFloat.Divides
Represents the divides without remainder invariant between two double scalars.
Prints as @code{x % y == 0}.

@item NumericFloat.Square
Represents the square invariant between two double scalars.
Prints as @code{x = y**2}.

@item NumericFloat.ZeroTrack
Represents the zero tracks invariant between
two double scalars; that is, when @code{x} is zero,
@code{y} is also zero.
Prints as @code{x = 0 => y = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericFloat.ZeroTrack.enabled}.

@item NumericInt.BitwiseAndZero
Represents the BitwiseAnd == 0 invariant between two long scalars; that is, @code{x} and
@code{y} have no bits in common.
Prints as @code{x & y == 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericInt.BitwiseAndZero.enabled}.

@item NumericInt.BitwiseComplement
Represents the bitwise complement invariant between two long scalars.
Prints as @code{x = ~y}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericInt.BitwiseComplement.enabled}.

@item NumericInt.BitwiseSubset
Represents the bitwise subset invariant between two long scalars; that is, the bits of
@code{y} are a subset of the bits of @code{x}.
Prints as @code{x = y | x}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericInt.BitwiseSubset.enabled}.

@item NumericInt.Divides
Represents the divides without remainder invariant between two long scalars.
Prints as @code{x % y == 0}.

@item NumericInt.ShiftZero
Represents the ShiftZero invariant between two long scalars; that is, @code{x}
right-shifted by @code{y} is always zero.
Prints as @code{x >> y = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericInt.ShiftZero.enabled}.

@item NumericInt.Square
Represents the square invariant between two long scalars.
Prints as @code{x = y**2}.

@item NumericInt.ZeroTrack
Represents the zero tracks invariant between
two long scalars; that is, when @code{x} is zero,
@code{y} is also zero.
Prints as @code{x = 0 => y = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoScalar.NumericInt.ZeroTrack.enabled}.

@item OneOfFloat
Represents double variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.OneOfFloat.size}
    @end itemize

@item OneOfFloatSequence
Represents double[] variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.OneOfFloatSequence.size}
    @end itemize

@item OneOfScalar
Represents long variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

May print as @code{x has only one value} when @code{x} is a hashcode (pointer) -- this is
because the numerical value of the hashcode (pointer) is uninteresting.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.OneOfScalar.size}
    @item @samp{daikon.inv.unary.scalar.OneOfScalar.omit_hashcode_values_Simplify}
    @end itemize

@item OneOfSequence
Represents long[] variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.sequence.OneOfSequence.size}
    @item @samp{daikon.inv.unary.sequence.OneOfSequence.omit_hashcode_values_Simplify}
    @end itemize

@item OneOfString
Represents String variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.string.OneOfString.size}
    @end itemize

@item OneOfStringSequence
Represents String[] variables that take on only a few distinct values. Prints as either
@code{x == c} (when there is only one value) or as @code{x one of @{c1, c2, c3@}}
(when there are multiple values).

See also the following configuration option:
    @itemize @bullet
    @item @samp{daikon.inv.unary.stringsequence.OneOfStringSequence.size}
    @end itemize

@item PairwiseFloatEqual
Represents an invariant between corresponding elements of two sequences of double values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] == y[]}.

@item PairwiseFloatGreaterEqual
Represents an invariant between corresponding elements of two sequences of double values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] >= y[]}.

@item PairwiseFloatGreaterThan
Represents an invariant between corresponding elements of two sequences of double values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] > y[]}.

@item PairwiseFloatLessEqual
Represents an invariant between corresponding elements of two sequences of double values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] <= y[]}.

@item PairwiseFloatLessThan
Represents an invariant between corresponding elements of two sequences of double values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] < y[]}.

@item PairwiseIntEqual
Represents an invariant between corresponding elements of two sequences of long values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] == y[]}.

@item PairwiseIntGreaterEqual
Represents an invariant between corresponding elements of two sequences of long values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] >= y[]}.

@item PairwiseIntGreaterThan
Represents an invariant between corresponding elements of two sequences of long values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] > y[]}.

@item PairwiseIntLessEqual
Represents an invariant between corresponding elements of two sequences of long values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] <= y[]}.

@item PairwiseIntLessThan
Represents an invariant between corresponding elements of two sequences of long values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] < y[]}.

@item PairwiseLinearBinary
Represents a linear invariant (i.e., @code{y = ax + b}) between the corresponding elements
of two sequences of long values. Each @code{(x[i], y[i])} pair is examined. Thus,
@code{x[0]} is compared to @code{y[0]}, @code{x[1]} to @code{y[1]} and so
forth. Prints as @code{y[] = a * x[] + b}.

@item PairwiseLinearBinaryFloat
Represents a linear invariant (i.e., @code{y = ax + b}) between the corresponding elements
of two sequences of double values. Each @code{(x[i], y[i])} pair is examined. Thus,
@code{x[0]} is compared to @code{y[0]}, @code{x[1]} to @code{y[1]} and so
forth. Prints as @code{y[] = a * x[] + b}.

@item PairwiseNumericFloat.Divides
Represents the divides without remainder invariant between corresponding elements of two sequences of double.
Prints as @code{x[] % y[] == 0}.

@item PairwiseNumericFloat.Square
Represents the square invariant between corresponding elements of two sequences of double.
Prints as @code{x[] = y[]**2}.

@item PairwiseNumericFloat.ZeroTrack
Represents the zero tracks invariant between
corresponding elements of two sequences of double; that is, when @code{x[]} is zero,
@code{y[]} is also zero.
Prints as @code{x[] = 0 => y[] = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericFloat.ZeroTrack.enabled}.

@item PairwiseNumericInt.BitwiseAndZero
Represents the BitwiseAnd == 0 invariant between corresponding elements of two sequences of long; that is, @code{x[]} and
@code{y[]} have no bits in common.
Prints as @code{x[] & y[] == 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseAndZero.enabled}.

@item PairwiseNumericInt.BitwiseComplement
Represents the bitwise complement invariant between corresponding elements of two sequences of long.
Prints as @code{x[] = ~y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseComplement.enabled}.

@item PairwiseNumericInt.BitwiseSubset
Represents the bitwise subset invariant between corresponding elements of two sequences of long; that is, the bits of
@code{y[]} are a subset of the bits of @code{x[]}.
Prints as @code{x[] = y[] | x[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericInt.BitwiseSubset.enabled}.

@item PairwiseNumericInt.Divides
Represents the divides without remainder invariant between corresponding elements of two sequences of long.
Prints as @code{x[] % y[] == 0}.

@item PairwiseNumericInt.ShiftZero
Represents the ShiftZero invariant between corresponding elements of two sequences of long; that is, @code{x[]}
right-shifted by @code{y[]} is always zero.
Prints as @code{x[] >> y[] = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericInt.ShiftZero.enabled}.

@item PairwiseNumericInt.Square
Represents the square invariant between corresponding elements of two sequences of long.
Prints as @code{x[] = y[]**2}.

@item PairwiseNumericInt.ZeroTrack
Represents the zero tracks invariant between
corresponding elements of two sequences of long; that is, when @code{x[]} is zero,
@code{y[]} is also zero.
Prints as @code{x[] = 0 => y[] = 0}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseNumericInt.ZeroTrack.enabled}.

@item PairwiseString.SubString
Represents the substring invariant between corresponding elements of two sequences of String.
Prints as @code{x[] is a substring of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.PairwiseString.SubString.enabled}.

@item PairwiseStringEqual
Represents an invariant between corresponding elements of two sequences of String values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] == y[]}.

@item PairwiseStringGreaterEqual
Represents an invariant between corresponding elements of two sequences of String values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] >= y[]}.

@item PairwiseStringGreaterThan
Represents an invariant between corresponding elements of two sequences of String values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] > y[]}.

@item PairwiseStringLessEqual
Represents an invariant between corresponding elements of two sequences of String values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] <= y[]}.

@item PairwiseStringLessThan
Represents an invariant between corresponding elements of two sequences of String values. The
length of the sequences must match for the invariant to hold. A comparison is made over each
@code{(x[i], y[i])} pair. Thus, @code{x[0]} is compared to @code{y[0]},
@code{x[1]} to @code{y[1]}, and so forth. Prints as @code{x[] < y[]}.

@item Positive
Represents the invariant @code{x > 0} where @code{x} is a long scalar. This exists only as an
example for the purposes of the manual. It isn't actually used (it is replaced by the more
general invariant LowerBound).

@item PrintableString
Represents a string that contains only printable ascii characters (values 32 through 126 plus 9
(tab).

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.string.PrintableString.enabled}.

@item RangeFloat.EqualMinusOne
Internal invariant representing double scalars that are equal to minus one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeFloat.EqualOne
Internal invariant representing double scalars that are equal to one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeFloat.EqualZero
Internal invariant representing double scalars that are equal to zero. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeFloat.GreaterEqual64
Internal invariant representing double scalars that are greater than or equal to 64. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item RangeFloat.GreaterEqualZero
Internal invariant representing double scalars that are greater than or equal to 0. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item RangeInt.BooleanVal
Internal invariant representing longs whose values are always 0 or 1. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeInt.Bound0_63
Internal invariant representing longs whose values are between 0 and 63. Used for
non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item RangeInt.EqualMinusOne
Internal invariant representing long scalars that are equal to minus one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeInt.EqualOne
Internal invariant representing long scalars that are equal to one. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeInt.EqualZero
Internal invariant representing long scalars that are equal to zero. Used for
non-instantiating suppressions. Will never print since OneOf accomplishes the same thing.

@item RangeInt.Even
Invariant representing longs whose values are always even. Used for non-instantiating
suppressions. Since this is not covered by the Bound or OneOf invariants it is printed. Prints
as @code{x is even}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.scalar.RangeInt.Even.enabled}.

@item RangeInt.GreaterEqual64
Internal invariant representing long scalars that are greater than or equal to 64. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item RangeInt.GreaterEqualZero
Internal invariant representing long scalars that are greater than or equal to 0. Used
for non-instantiating suppressions. Will never print since Bound accomplishes the same thing.

@item RangeInt.PowerOfTwo
Invariant representing longs whose values are always a power of 2 (exactly one bit is set).
Used for non-instantiating suppressions. Since this is not covered by the Bound or OneOf
invariants it is printed. Prints as @code{x is a power of 2}.

@item Reverse
Represents two sequences of long where one is in the reverse order of the other. Prints as
@code{x[] is the reverse of y[]}.

@item ReverseFloat
Represents two sequences of double where one is in the reverse order of the other. Prints as
@code{x[] is the reverse of y[]}.

@item SeqFloatEqual
Represents an invariant between a double scalar and a a sequence of double values. Prints
as @code{x[] elements == y} where @code{x} is a double sequence and
@code{y} is a double scalar.

@item SeqFloatGreaterEqual
Represents an invariant between a double scalar and a a sequence of double values. Prints
as @code{x[] elements >= y} where @code{x} is a double sequence and
@code{y} is a double scalar.

@item SeqFloatGreaterThan
Represents an invariant between a double scalar and a a sequence of double values. Prints
as @code{x[] elements > y} where @code{x} is a double sequence and
@code{y} is a double scalar.

@item SeqFloatLessEqual
Represents an invariant between a double scalar and a a sequence of double values. Prints
as @code{x[] elements <= y} where @code{x} is a double sequence and
@code{y} is a double scalar.

@item SeqFloatLessThan
Represents an invariant between a double scalar and a a sequence of double values. Prints
as @code{x[] elements < y} where @code{x} is a double sequence and
@code{y} is a double scalar.

@item SeqIndexFloatEqual
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] == i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatEqual.enabled}.

@item SeqIndexFloatGreaterEqual
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] >= i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatGreaterEqual.enabled}.

@item SeqIndexFloatGreaterThan
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] > i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatGreaterThan.enabled}.

@item SeqIndexFloatLessEqual
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] <= i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatLessEqual.enabled}.

@item SeqIndexFloatLessThan
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] < i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatLessThan.enabled}.

@item SeqIndexFloatNonEqual
Represents an invariant over sequences of double values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] != i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexFloatNonEqual.enabled}.

@item SeqIndexIntEqual
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] == i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntEqual.enabled}.

@item SeqIndexIntGreaterEqual
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] >= i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntGreaterEqual.enabled}.

@item SeqIndexIntGreaterThan
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] > i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntGreaterThan.enabled}.

@item SeqIndexIntLessEqual
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] <= i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntLessEqual.enabled}.

@item SeqIndexIntLessThan
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] < i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntLessThan.enabled}.

@item SeqIndexIntNonEqual
Represents an invariant over sequences of long values between the index of an element of the
sequence and the element itself. Prints as @code{x[i] != i}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.unary.sequence.SeqIndexIntNonEqual.enabled}.

@item SeqIntEqual
Represents an invariant between a long scalar and a a sequence of long values. Prints
as @code{x[] elements == y} where @code{x} is a long sequence and
@code{y} is a long scalar.

@item SeqIntGreaterEqual
Represents an invariant between a long scalar and a a sequence of long values. Prints
as @code{x[] elements >= y} where @code{x} is a long sequence and
@code{y} is a long scalar.

@item SeqIntGreaterThan
Represents an invariant between a long scalar and a a sequence of long values. Prints
as @code{x[] elements > y} where @code{x} is a long sequence and
@code{y} is a long scalar.

@item SeqIntLessEqual
Represents an invariant between a long scalar and a a sequence of long values. Prints
as @code{x[] elements <= y} where @code{x} is a long sequence and
@code{y} is a long scalar.

@item SeqIntLessThan
Represents an invariant between a long scalar and a a sequence of long values. Prints
as @code{x[] elements < y} where @code{x} is a long sequence and
@code{y} is a long scalar.

@item SeqSeqFloatEqual
Represents invariants between two sequences of double values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] == y[] lexically}.


If order doesn't matter for each variable, then the sequences are compared to see if they are
set equivalent. Prints as @code{x[] == y[]}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqFloatGreaterEqual
Represents invariants between two sequences of double values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] >= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqFloatGreaterThan
Represents invariants between two sequences of double values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] > y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqFloatLessEqual
Represents invariants between two sequences of double values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] <= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqFloatLessThan
Represents invariants between two sequences of double values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] < y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqIntEqual
Represents invariants between two sequences of long values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] == y[] lexically}.


If order doesn't matter for each variable, then the sequences are compared to see if they are
set equivalent. Prints as @code{x[] == y[]}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqIntGreaterEqual
Represents invariants between two sequences of long values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] >= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqIntGreaterThan
Represents invariants between two sequences of long values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] > y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqIntLessEqual
Represents invariants between two sequences of long values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] <= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqIntLessThan
Represents invariants between two sequences of long values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] < y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqStringEqual
Represents invariants between two sequences of String values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] == y[] lexically}.


If order doesn't matter for each variable, then the sequences are compared to see if they are
set equivalent. Prints as @code{x[] == y[]}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqStringGreaterEqual
Represents invariants between two sequences of String values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] >= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqStringGreaterThan
Represents invariants between two sequences of String values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] > y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqStringLessEqual
Represents invariants between two sequences of String values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] <= y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item SeqSeqStringLessThan
Represents invariants between two sequences of String values. If order matters for each
variable (which it does by default), then the sequences are compared lexically. Prints as
@code{x[] < y[] lexically}.


If the auxiliary information (e.g., order matters) doesn't match between two variables, then
this invariant cannot apply to those variables.

@item StdString.SubString
Represents the substring invariant between two String scalars.
Prints as @code{x is a substring of y}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoString.StdString.SubString.enabled}.

@item StringEqual
Represents an invariant of == between two String scalars. Prints as @code{x == y}.

@item StringGreaterEqual
Represents an invariant of >= between two String scalars. Prints as @code{x >= y}.

@item StringGreaterThan
Represents an invariant of > between two String scalars. Prints as @code{x > y}.

@item StringLessEqual
Represents an invariant of <= between two String scalars. Prints as @code{x <= y}.

@item StringLessThan
Represents an invariant of < between two String scalars. Prints as @code{x < y}.

@item StringNonEqual
Represents an invariant of != between two String scalars. Prints as @code{x != y}.

@item SubSequence
Represents two sequences of long values where one sequence is a subsequence of the
other. Prints as @code{x[] is a subsequence of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SubSequence.enabled}.

@item SubSequenceFloat
Represents two sequences of double values where one sequence is a subsequence of the
other. Prints as @code{x[] is a subsequence of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SubSequenceFloat.enabled}.

@item SubSet
Represents two sequences of long values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other. Prints as either
@code{x[] is a subset of y[]} or as @code{x[] is a superset of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SubSet.enabled}.

@item SubSetFloat
Represents two sequences of double values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other. Prints as either
@code{x[] is a subset of y[]} or as @code{x[] is a superset of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SubSetFloat.enabled}.

@item SuperSequence
Represents two sequences of long values where one sequence is a subsequence of the
other. Prints as @code{x[] is a subsequence of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SuperSequence.enabled}.

@item SuperSequenceFloat
Represents two sequences of double values where one sequence is a subsequence of the
other. Prints as @code{x[] is a subsequence of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SuperSequenceFloat.enabled}.

@item SuperSet
Represents two sequences of long values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other. Prints as either
@code{x[] is a subset of y[]} or as @code{x[] is a superset of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SuperSet.enabled}.

@item SuperSetFloat
Represents two sequences of double values where one of the sequences is a subset of the other; that
is each element of one sequence appears in the other. Prints as either
@code{x[] is a subset of y[]} or as @code{x[] is a superset of y[]}.

This invariant is not enabled by default.  See the configuration option
@samp{daikon.inv.binary.twoSequence.SuperSetFloat.enabled}.

@item UpperBound
Represents the invariant @code{x <= c}, where @code{c} is a constant and
@code{x} is a long scalar.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.UpperBound.minimal_interesting}
    @item @samp{daikon.inv.unary.scalar.UpperBound.maximal_interesting}
    @end itemize

@item UpperBoundFloat
Represents the invariant @code{x <= c}, where @code{c} is a constant and
@code{x} is a double scalar.

See also the following configuration options:
    @itemize @bullet
    @item @samp{daikon.inv.unary.scalar.UpperBoundFloat.minimal_interesting}
    @item @samp{daikon.inv.unary.scalar.UpperBoundFloat.maximal_interesting}
    @end itemize

@c END AUTO-GENERATED INVARIANTS LISTING
