Package daikon.inv.unary.sequence

Class EltOneOfFloat

  • All Implemented Interfaces:
    OneOf, Serializable, Cloneable
    public final class EltOneOfFloat
extends SingleFloatSequence
implements OneOf
    Represents sequences of double values where the elements of the sequence take on only a few distinct values. Prints as either x[] elements == c (when there is only one value), or as x[] elements one of {c1, c2, c3} (when there are multiple values).
    See Also:
    Serialized Form

    • Field Detail

      • debug

        public static final Logger debug
        Debugging logger.

      • dkconfig_enabled

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

      • dkconfig_size

        public static int dkconfig_size
        Positive integer. Specifies the maximum set size for this type of invariant (x is one of size items).

    • Method Detail

      • enabled

        public boolean enabled()
        Description copied from class: Invariant
        Returns whether or not this class of invariants is currently enabled.

        Its implementation is almost always return dkconfig_enabled;.

        Specified by:
        enabled in class Invariant

      • is_boolean

        @Pure
public boolean is_boolean​(@GuardSatisfied EltOneOfFloat this)

      • is_hashcode

        @Pure
public boolean is_hashcode​(@GuardSatisfied EltOneOfFloat this)

      • clone

        @SideEffectFree
public EltOneOfFloat clone​(@GuardSatisfied EltOneOfFloat this)
        Description copied from class: Invariant
        Do nothing special, Overridden to remove exception from declaration.
        Overrides:
        clone in class Invariant

      • num_elts

        public int num_elts()
        Description copied from interface: OneOf
        The number of elements in the OneOf invariant.
        Specified by:
        num_elts in interface OneOf

      • elt

        public Object elt()
        Description copied from interface: OneOf
        The single value represented by the OneOf invariant. Throws an error if not exactly one value is represented by this.
        Specified by:
        elt in interface OneOf

      • min_elt

        public double min_elt()

      • max_elt

        public double max_elt()

      • compare_rep

        public boolean compare_rep​(int num_other_elts,
                           double[] other_elts)

      • repr

        public String repr​(@GuardSatisfied EltOneOfFloat this)
        Description copied from class: Invariant
        For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob() also prints the confidence), and Invariant.format() gives a high-level representation for user output.
        Overrides:
        repr in class Invariant
        Returns:
        a string representation of this

      • format_esc

        public String format_esc​(@GuardSatisfied EltOneOfFloat this)

      • check_modified

        public InvariantStatus check_modified​(double[] a,
                                      int count)
        Description copied from class: SingleFloatSequence
        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 SingleFloatSequence
        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

      • add_mod_elem

        public InvariantStatus add_mod_elem​(double v,
                                    int count)
        Adds a single sample to the invariant. Returns the appropriate InvariantStatus from the result of adding the sample to this.

      • check_mod_elem

        public InvariantStatus check_mod_elem​(double v,
                                      int count)
        Checks a single sample to the invariant. Returns the appropriate InvariantStatus from the result of adding the sample to this.

      • enoughSamples

        public boolean enoughSamples​(@GuardSatisfied EltOneOfFloat this)
        Description copied from class: Invariant
        Returns true if the invariant has enough samples to have its computed constants well-formed. Is overridden in classes like LinearBinary/Ternary and Upper/LowerBound.
        Overrides:
        enoughSamples in class Invariant
        Returns:
        true if the invariant has enough samples to have its computed constants well-formed

      • 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

      • mergeFormulasOk

        public boolean mergeFormulasOk()
        Oneof can merge different formulas from lower points to create a single formula at an upper point.
        Overrides:
        mergeFormulasOk in class Invariant
        Returns:
        true if invariants with different formulas can be merged

      • isSameFormula

        @Pure
public boolean isSameFormula​(Invariant o)
        Description copied from class: Invariant
        Returns true iff the two invariants represent the same mathematical formula. Does not consider the context such as variable names, confidences, sample counts, value counts, or related quantities. As a rule of thumb, if two invariants format the same, this method returns true. Furthermore, in many cases, if an invariant does not involve computed constants (as "x>c" and "y=ax+b" do for constants a, b, and c), then this method vacuously returns true.
        Specified by:
        isSameFormula in class Invariant
        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

      • hasUninterestingConstant

        public boolean hasUninterestingConstant()
        Description copied from class: Invariant
        An invariant that includes an uninteresting constant (say, "size(x[]) < 237") is likely to be an artifact of the way the program was tested, rather than a statement that would in fact hold over all possible executions.
        Overrides:
        hasUninterestingConstant in class Invariant

      • isExact

        @Pure
public boolean isExact()
        Description copied from class: Invariant
        Subclasses should override. An exact invariant indicates that given all but one variable value, the last one can be computed. (I think that's correct, anyway.) Examples are IntComparison (when only equality is possible), LinearBinary, FunctionUnary. OneOf is treated differently, as an interface. The result of this method does not depend on whether the invariant is justified, destroyed, etc.
        Overrides:
        isExact in class Invariant
        Returns:
        true if any variable value can be computed from all the others

      • merge

        public @Nullable EltOneOfFloat merge​(List<Invariant> invs,
                                     PptSlice parent_ppt)
        Merge the invariants in invs to form a new invariant. Each must be a EltOneOfFloat invariant. This code finds all of the oneof values from each of the invariants and returns the merged invariant (if any).
        Overrides:
        merge in class Invariant
        Parameters:
        invs - list of invariants to merge. The invariants must all be of the same type and should come from the children of parent_ppt. They should also all be permuted to match the variable order in parent_ppt.
        parent_ppt - slice that will contain the new invariant
        Returns:
        the merged invariant or null if the invariants didn't represent the same invariant

      • set_one_of_val

        public void set_one_of_val​(double[] vals)
        Setup the invariant with the specified elements. Normally used when searching for a specified OneOf. The elements of vals are not necessarily interned; this method interns each element.

      • state_match

        public boolean state_match​(Object state)
        Returns true if every element in this invariant is contained in the specified state. For example if x = 1 and the state contains 1 and 2, true will be returned.
        Overrides:
        state_match in class Invariant