Class NonModulus

  • All Implemented Interfaces:
    Serializable, Cloneable

    public class NonModulus
    extends SingleScalar
    Represents long scalars that are never equal to r (mod m) where all other numbers in the same range (i.e., all the values that x doesn't take from min(x) to max(x)) are equal to r (mod m). Prints as x != r (mod m), where r is the remainder and m is the modulus.
    See Also:
    Serialized Form
    • Field Detail

      • dkconfig_enabled

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

      • get_proto

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

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

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

        public String repr​(@GuardSatisfied NonModulus 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
      • check_modified

        public InvariantStatus check_modified​(long value,
                                              int count)
        Description copied from class: SingleScalar
        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 SingleScalar
        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: 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
      • hasModulusRemainder

        public boolean hasModulusRemainder​(long modulus,
                                           long remainder)
        Returns true if this has the given modulus and remainder.
      • 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