Class TwoScalar

  • All Implemented Interfaces:
    Serializable, Cloneable
    Direct Known Subclasses:
    IntEqual, IntGreaterEqual, IntGreaterThan, IntLessEqual, IntLessThan, IntNonEqual, LinearBinary, NumericInt

    public abstract class TwoScalar
    extends BinaryInvariant
    Base class for invariants over two variables of type long. An example is y = abs(x).

    Provides a simpler mechanism for non-symmetric invariants to function over both permutations of their variables.

    Non-symmetric invariants must instantiate two objects (one for each argument order). This is tracked by the variable swap. They must always access their variables via the methods var1() and var2() which return the correct variable (based on the swap setting). No other work is necessary, all permuations and resurrection is handled here.

    Symmetric invariants should define symmetric() to return true or override resurrect_done_swapped to do nothing. Non-symmetric invariants that use converse operations (eg, less than and greater than) rather than argument swapping should override resurrect_done_swapped to return the correct class.

    See Also:
    Serialized Form
    • Field Detail

      • swap

        protected boolean swap
    • Method Detail

      • get_swap

        public boolean get_swap()
        Returns whether or not the variable order is currently swapped for this invariant.
        Overrides:
        get_swap in class BinaryInvariant
      • resurrect_done

        protected Invariant resurrect_done​(int[] permutation)
        Checks to see if the variable order was swapped and calls the correct routine to handle it.
        Specified by:
        resurrect_done in class Invariant
        Parameters:
        permutation - the permutation
        Returns:
        the permuted invariant
      • var1

        public VarInfo var1​(@GuardSatisfied TwoScalar this)
        Returns the first variable. This is the only mechanism by which subclasses should access variables.
      • var2

        public VarInfo var2​(@GuardSatisfied TwoScalar this)
        Returns the first variable. This is the only mechanism by which subclasses should access variables.
      • var1

        public VarInfo var1​(VarInfo[] vis)
        Returns the first variable from the specified vis. This is the only mechanism by which subclasses should access variables.
      • var2

        public VarInfo var2​(VarInfo[] vis)
        Returns the first variable in the specified vis. This is the only mechanism by which subclasses should access variables.
      • check_modified

        public abstract InvariantStatus check_modified​(long v1,
                                                       long v2,
                                                       int count)
        Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.
        Parameters:
        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_modified

        public InvariantStatus add_modified​(long v1,
                                            long v2,
                                            int count)
        Default implementation simply calls check. Subclasses can override.
      • add_unmodified

        public InvariantStatus add_unmodified​(long v1,
                                              long v2,
                                              int count)
        By default, do nothing if the value hasn't been seen yet. Subclasses can override this.
      • repr

        public String repr​(@GuardSatisfied TwoScalar this)
        Returns a representation of the class. This includes the classname, variables, and swap state.
        Overrides:
        repr in class Invariant
        Returns:
        a string representation of this
      • isSameFormula

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