Package daikon.inv.binary.twoSequence

Class PairwiseNumericFloat.Divides

Object

Invariant

BinaryInvariant

TwoSequenceFloat

PairwiseNumericFloat

Divides

All Implemented Interfaces:

Serializable, Cloneable

Enclosing class:

PairwiseNumericFloat

public static class PairwiseNumericFloat.Divides
extends PairwiseNumericFloat

Represents the divides without remainder invariant between corresponding elements of two sequences of double. Prints as x[] % y[] == 0.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class PairwiseNumericFloat

PairwiseNumericFloat.Divides, PairwiseNumericFloat.Square, PairwiseNumericFloat.ZeroTrack

Nested classes/interfaces inherited from class Invariant

Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

Fields

Modifier and Type	Field	Description
static boolean	dkconfig_enabled	Boolean.

Fields inherited from class PairwiseNumericFloat

var1_eq_0, var1_eq_1, var1_eq_minus_1, var1_eq_var2, var1_ge_0, var1_le_var2, var1_ne_0, var2_eq_0, var2_eq_1, var2_eq_minus_1, var2_eq_var1, var2_ge_0, var2_ne_0

Fields inherited from class TwoSequenceFloat

swap

Fields inherited from class Invariant

CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debug, 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

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	Divides(boolean swap)
protected	Divides(PptSlice ppt, boolean swap)

Method Summary

Modifier and Type	Method	Description
boolean	enabled()	Returns whether or not this invariant is enabled.
boolean	eq_check(double x, double y)	Returns true if x and y don't invalidate the invariant.
String	get_format_str(OutputFormat format)	Return a format string for the specified output format.
NISuppressionSet	get_ni_suppressions()	Returns a list of non-instantiating suppressions for this invariant.
static PairwiseNumericFloat	get_proto(boolean swap)	Returns the prototype invariant.
protected PairwiseNumericFloat.Divides	instantiate_dyn(PptSlice slice)	Instantiates (creates) an invariant of the same class on the specified slice.
@Nullable DiscardInfo	isObviousDynamically(VarInfo[] vis)	Returns non-null if this invariant is obvious from an existing, non-falsified linear binary invariant in the same slice as this invariant.
InvDef[][]	obvious_checks(VarInfo[] vis)	This needs to be an obvious check and not a suppression for sequences because there is no consistent way to check that var1 and var2 have the same length (for derivations).

Methods inherited from class PairwiseNumericFloat

array_sizes_eq, check_modified, format_using, get_array_size, get_proto_all, instantiate_ok, is_subsequence, isExact, repr

Methods inherited from class TwoSequenceFloat

add, add_modified, add_unmodified, check, check_unmodified, computeConfidence, get_swap, isSameFormula, resurrect_done, resurrect_done_swapped, resurrect_done_unswapped, valid_types, var1, var1, var2, var2

Methods inherited from class BinaryInvariant

add_unordered, check_unordered, find, is_symmetric

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, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExclusiveFormula, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidEscExpression, 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

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff divides invariants should be considered.

Constructor Detail

Divides

protected Divides(PptSlice ppt,
                  boolean swap)

Divides

protected Divides(boolean swap)

Method Detail

get_proto

public static PairwiseNumericFloat get_proto(boolean swap)

Returns the prototype invariant.

enabled

public boolean enabled()

Returns whether or not this invariant is enabled.

Specified by:

enabled in class Invariant

instantiate_dyn

protected PairwiseNumericFloat.Divides instantiate_dyn( PairwiseNumericFloat.Divides this,
                                                       PptSlice slice)

Description copied from class: Invariant

Instantiates (creates) an invariant of the same class on the specified slice. Must be overridden in each class. Must be used rather than Invariant.clone() so that checks in Invariant.instantiate(daikon.PptSlice) for reasonable invariants are done.

The implementation of this method is almost always return new <em>InvName</em>(slice);

Specified by:

instantiate_dyn in class Invariant

Returns:

the new invariant

get_format_str

public String get_format_str(@GuardSatisfied PairwiseNumericFloat.Divides this,
                             OutputFormat format)

Description copied from class: PairwiseNumericFloat

Return a format string for the specified output format. Each instance of %varN% will be replaced by the correct name for varN.

Specified by:

get_format_str in class PairwiseNumericFloat

eq_check

public boolean eq_check(double x,
                        double y)

Description copied from class: PairwiseNumericFloat

Returns true if x and y don't invalidate the invariant.

Specified by:

eq_check in class PairwiseNumericFloat

obvious_checks

public InvDef[][] obvious_checks(VarInfo[] vis)

This needs to be an obvious check and not a suppression for sequences because there is no consistent way to check that var1 and var2 have the same length (for derivations).

Overrides:

obvious_checks in class PairwiseNumericFloat

get_ni_suppressions

@Pure
public NISuppressionSet get_ni_suppressions()

Returns a list of non-instantiating suppressions for this invariant.

Overrides:

get_ni_suppressions in class Invariant

Returns:

the set of non-instantiating suppressions for this invariant

isObviousDynamically

@Pure
public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)

Returns non-null if this invariant is obvious from an existing, non-falsified linear binary invariant in the same slice as this invariant. This invariant of the form "x % y == 0" is falsified if a linear binary invariant is found of the form "a*y - 1*x + 0 == 0"

Overrides:

isObviousDynamically in class PairwiseNumericFloat

Returns:

non-null value iff this invariant is obvious from other invariants in the same slice