Package daikon.inv.binary.twoSequence

Class SeqSeqStringGreaterThan

  • All Implemented Interfaces:
    Serializable, Cloneable
    public class SeqSeqStringGreaterThan
extends TwoSequenceString
    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 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.

    See Also:
    Serialized Form

    • Field Detail

      • dkconfig_enabled

        public static boolean dkconfig_enabled
        Boolean. True iff SeqSeqStringGreaterThan invariants should be considered.

    • Method Detail

      • enabled

        public boolean enabled()
        Returns whether or not this invariant is enabled.
        Specified by:
        enabled in class Invariant

      • repr

        public String repr​(@GuardSatisfied SeqSeqStringGreaterThan this)
        Description copied from class: TwoSequenceString
        Returns a representation of the class. This includes the classname, variables, and swap state.
        Overrides:
        repr in class TwoSequenceString
        Returns:
        a string representation of this

      • check_modified

        public InvariantStatus check_modified​(String @Interned [] v1,
                                      String @Interned [] v2,
                                      int count)
        Description copied from class: TwoSequenceString
        Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.
        Specified by:
        check_modified in class TwoSequenceString
        count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.
        Returns:
        whether or not the sample is consistent with the invariant

      • isSameFormula

        @Pure
public boolean isSameFormula​(Invariant o)
        Description copied from class: TwoSequenceString
        Return true if both invariants are the same class and the order of the variables (swap) is the same.
        Overrides:
        isSameFormula in class TwoSequenceString
        Parameters:
        o - the invariant to compare to this one
        Returns:
        true iff the two invariants represent the same mathematical formula. Does not consider

      • isExclusiveFormula

        @Pure
public boolean isExclusiveFormula​(Invariant o)
        Description copied from class: Invariant
        Returns true iff the two invariants represent mutually exclusive mathematical formulas -- that is, if one of them is true, then the other must be false. This method does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities.
        Overrides:
        isExclusiveFormula in class Invariant
        Parameters:
        o - the other invariant to compare to this one
        Returns:
        true iff the two invariants represent mutually exclusive mathematical formulas

      • isObviousStatically_SomeInEquality

        @Pure
public @Nullable DiscardInfo isObviousStatically_SomeInEquality()
        Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.
        Overrides:
        isObviousStatically_SomeInEquality in class Invariant
        Returns:
        the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

      • isObviousDynamically_SomeInEquality

        @Pure
public @Nullable DiscardInfo isObviousDynamically_SomeInEquality()
        Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.
        Overrides:
        isObviousDynamically_SomeInEquality in class Invariant
        Returns:
        the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

      • isObviousStatically

        @Pure
public @Nullable DiscardInfo isObviousStatically​(VarInfo[] vis)
        Description copied from class: Invariant
        Return true if this invariant is necessarily true from a fact that can be determined statically -- for the given varInfos rather than the varInfos of this. Conceptually, this means "is this invariant statically obvious if its VarInfos were switched with vis?" Intended to be overridden by subclasses. Should only do static checking.

        Precondition: vis.length == this.ppt.var_infos.length

        Overrides:
        isObviousStatically in class Invariant
        Parameters:
        vis - the VarInfos this invariant is obvious over. The position and data type of the variables is the *same* as that of this.ppt.var_infos.

      • isObviousDynamically

        @Pure
public @Nullable DiscardInfo isObviousDynamically​(VarInfo[] vis)
        Description copied from class: Invariant
        Return non-null if this invariant is necessarily true from a fact that can be determined dynamically (after checking data) -- for the given varInfos rather than the varInfos of this. Conceptually, this means, "Is this invariant dynamically obvious if its VarInfos were switched with vis?" Intended to be overriden by subclasses so they can filter invariants after checking; the overriding method should first call "super.isObviousDynamically(vis)". Since this method is dynamic, it should only be called after all processing.
        Overrides:
        isObviousDynamically in class Invariant

      • isEqual

        @Pure
public boolean isEqual()