Class SuperSet

  • All Implemented Interfaces:
    Serializable, Cloneable

    public class SuperSet
    extends TwoSequence
    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 x[] is a subset of y[] or as x[] is a superset of y[].
    See Also:
    Serialized Form
    • Field Detail

      • dkconfig_enabled

        public static boolean dkconfig_enabled
        Boolean. True iff SubSet invariants should be considered.
    • Method Detail

      • get_proto

        public static SuperSet get_proto()
        Returns the prototype invariant for SuperSet
      • enabled

        public boolean enabled()
        returns whether or not this invariant is enabled
        Specified by:
        enabled in class Invariant
      • repr

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

        @SideEffectFree
        public String format​(@GuardSatisfied SuperSet this)
        Description copied from class: Invariant
        Returns a high-level printed representation of the invariant, for user output. format produces normal output, while the Invariant.repr() formatting routine produces low-level, detailed output for debugging, and Invariant.repr_prob() also prints the confidence.
        Overrides:
        format in class Invariant
        Returns:
        a string representation of this
      • check_modified

        public InvariantStatus check_modified​(long[] a1,
                                              long[] a2,
                                              int count)
        Description copied from class: TwoSequence
        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 TwoSequence
        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
      • 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.
      • isSameFormula

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