Object
- Invariant
- - UnaryInvariant
  - - SingleSequence
    - - SingleScalarSequence
      - EltNonZero

All Implemented Interfaces:

Serializable, Cloneable
```
public final class EltNonZero
extends SingleScalarSequence
```
Represents the invariant "x != 0" where x represents all of the elements of a sequence of long. Prints as x[] elements != 0.

See Also:

Serialized Form

Nested Class Summary
- Nested classes/interfaces inherited from class Invariant
  Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

Fields
Modifier and Type Field Description

static Logger debug
Debug tracer.

static boolean dkconfig_enabled
Boolean.
- Fields inherited from class SingleSequence
  dkconfig_SeqIndexDisableAll
- Fields inherited from class Invariant
  CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, invariantEnabledDefault, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_modified(long @Interned [] a, int count)`	Similar to `SingleScalarSequence.check_modified(long[], int)` except that it can change the state of the invariant if necessary.
`InvariantStatus`	`check_modified(long @Interned [] a, int count)`	Presents a sample to the invariant.
`protected double`	`computeConfidence()`	This method computes the confidence that this invariant occurred by chance.
`boolean`	`enabled()`	returns whether or not this invariant is enabled
`static @Nullable EltNonZero`	`find(PptSlice ppt)`
`String`	`format_csharp_contract()`
`String`	`format_daikon()`
`String`	`format_esc()`
`String`	`format_java_family(OutputFormat format)`
`String`	`format_simplify()`
`String`	`format_using(OutputFormat format)`	Return a printed representation of this invariant, in the given format.
`NISuppressionSet`	`get_ni_suppressions()`	returns the ni-suppressions for EltNonZero
`static EltNonZero`	`get_proto()`	Returns the prototype invariant for EltNonZero
`protected EltNonZero`	`instantiate_dyn(PptSlice slice)`	instantiate an invariant on the specified slice
`boolean`	`isExclusiveFormula(Invariant other)`	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.
`@Nullable DiscardInfo`	`isObviousDynamically(VarInfo[] vis)`	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.
`@Nullable DiscardInfo`	`isObviousStatically(VarInfo[] vis)`	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.
`boolean`	`isSameFormula(Invariant other)`	Returns true iff the two invariants represent the same mathematical formula.
`boolean`	`isValidEscExpression()`	Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general.
`String`	`repr()`	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.

Methods inherited from class SingleScalarSequence
add, add_unmodified, check, check_unmodified, valid_types, valid_types_static, var

Methods inherited from class UnaryInvariant
resurrect_done

Methods inherited from class Invariant
add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_ok, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames

Methods inherited from class Object
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - debug
```
public static final Logger debug
```
    Debug tracer.
  - dkconfig_enabled
```
public static boolean dkconfig_enabled
```
    Boolean. True iff EltNonZero invariants should be considered.
- Method Detail
  - get_proto
```
public static EltNonZero get_proto()
```
    Returns the prototype invariant for EltNonZero
  - enabled
```
public boolean enabled()
```
    returns whether or not this invariant is enabled
    
    Specified by:
    
    enabled in class Invariant
  - instantiate_dyn
```
protected EltNonZero instantiate_dyn( EltNonZero this,
                                     PptSlice slice)
```
    instantiate an invariant on the specified slice
    
    Specified by:
    
    instantiate_dyn in class Invariant
    
    Returns:
    
    the new invariant
  - repr
```
public String repr(@GuardSatisfied EltNonZero 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_using
```
@SideEffectFree
public String format_using(@GuardSatisfied EltNonZero this,
                           OutputFormat format)
```
    Description copied from class: Invariant
    
    Return a printed representation of this invariant, in the given format.
    
    Specified by:
    
    format_using in class Invariant
  - format_daikon
```
public String format_daikon(@GuardSatisfied EltNonZero this)
```
  - isValidEscExpression
```
@Pure
public boolean isValidEscExpression()
```
    Description copied from class: Invariant
    
    Returns a conjuction of mapping the same function of our expresssions's VarInfos, in general. Subclasses may override if they are able to handle generally-inexpressible properties in special-case ways.
    
    Overrides:
    
    isValidEscExpression in class Invariant
    
    Returns:
    
    conjuction of mapping the same function of our expresssions's VarInfos
    
    See Also:
    
    VarInfo.isValidEscExpression()
  - format_esc
```
public String format_esc(@GuardSatisfied EltNonZero this)
```
  - format_java_family
```
public String format_java_family(@GuardSatisfied EltNonZero this,
                                 OutputFormat format)
```
  - format_csharp_contract
```
public String format_csharp_contract(@GuardSatisfied EltNonZero this)
```
  - format_simplify
```
public String format_simplify(@GuardSatisfied EltNonZero this)
```
  - check_modified
```
public InvariantStatus check_modified(long @Interned [] a,
                                      int count)
```
    Description copied from class: SingleScalarSequence
    
    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 SingleScalarSequence
    
    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 @Interned [] a,
                                    int count)
```
    Description copied from class: SingleScalarSequence
    
    Similar to SingleScalarSequence.check_modified(long[], int) except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply call SingleScalarSequence.check_modified(long[], int). This method need not check for falsification; that is done by the caller.
    
    Specified by:
    
    add_modified in class SingleScalarSequence
  - computeConfidence
```
protected double computeConfidence()
```
    Description copied from class: Invariant
    
    This method computes the confidence that this invariant occurred by chance. Clients should call Invariant.getConfidence() instead.
    This method need not check the value of field "falsified", as the caller does that.
    
    Specified by:
    
    computeConfidence in class Invariant
    
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    Invariant.getConfidence()
  - isSameFormula
```
@Pure
public boolean isSameFormula(Invariant other)
```
    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:
    
    other - 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 other)
```
    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:
    
    other - the other invariant to compare to this one
    
    Returns:
    
    true iff the two invariants represent mutually exclusive mathematical formulas
  - 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
  - find
```
public static @Nullable EltNonZero find(PptSlice ppt)
```
  - get_ni_suppressions
```
@Pure
public NISuppressionSet get_ni_suppressions()
```
    returns the ni-suppressions for EltNonZero
    
    Overrides:
    
    get_ni_suppressions in class Invariant
    
    Returns:
    
    the set of non-instantiating suppressions for this invariant

Modifier and Type	Field	Description
`static Logger`	`debug`	Debug tracer.
`static boolean`	`dkconfig_enabled`	Boolean.

Class EltNonZero

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Field Summary

Fields inherited from class SingleSequence

Fields inherited from class Invariant

Method Summary

Methods inherited from class SingleScalarSequence

Methods inherited from class UnaryInvariant

Methods inherited from class Invariant

Methods inherited from class Object

Field Detail

debug

dkconfig_enabled

Method Detail

get_proto

enabled

instantiate_dyn

repr

format_using

format_daikon

isValidEscExpression

format_esc

format_java_family

format_csharp_contract

format_simplify

check_modified

add_modified

computeConfidence

isSameFormula

isExclusiveFormula

isObviousStatically

isObviousDynamically

find

get_ni_suppressions