Package daikon.inv.binary.twoSequence
Class SeqSeqFloatGreaterThan
- Object
-
- Invariant
-
- BinaryInvariant
-
- TwoSequenceFloat
-
- SeqSeqFloatGreaterThan
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class SeqSeqFloatGreaterThan extends TwoSequenceFloat
Represents invariants between two sequences of double values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints asx[] > y[] lexically
.If the auxiliary information (e.g., order matters) doesn't match between two variables, then this invariant cannot apply to those variables.
- 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 boolean
dkconfig_enabled
Boolean.-
Fields inherited from class TwoSequenceFloat
swap
-
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
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
SeqSeqFloatGreaterThan(boolean order)
protected
SeqSeqFloatGreaterThan(SeqSeqFloatLessThan seq_swap)
protected
SeqSeqFloatGreaterThan(PptSlice ppt, boolean order)
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double @Interned [] v1, double @Interned [] v2, int count)
Default implementation simply calls check.InvariantStatus
check_modified(double @Interned [] v1, double @Interned [] v2, 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 SeqSeqFloatGreaterThan
find(PptSlice ppt)
String
format_simplify()
String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.@Nullable NISuppressionSet
get_ni_suppressions()
Returns a list of non-instantiating suppressions for this invariant.static SeqSeqFloatGreaterThan
get_proto()
Returns the prototype invariant for SeqSeqFloatGreaterThanprotected SeqSeqFloatGreaterThan
instantiate_dyn(PptSlice slice)
Instantiates the invariant on the specified slice.boolean
instantiate_ok(VarInfo[] vis)
Non-Equal SeqComparison is only valid on integral types.boolean
isEqual()
boolean
isExclusiveFormula(Invariant o)
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
isObviousDynamically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.@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.@Nullable DiscardInfo
isObviousStatically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.boolean
isSameFormula(Invariant o)
Return true if both invariants are the same class and the order of the variables (swap) is the same.void
repCheck()
Check the rep invariants of this.String
repr()
Returns a representation of the class.protected Invariant
resurrect_done_swapped()
Swaps the variables by inverting the state of swap.-
Methods inherited from class TwoSequenceFloat
add, add_unmodified, check, check_unmodified, get_swap, resurrect_done, 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, isExact, isObvious, isObviousDynamically, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, 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, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff SeqSeqFloatGreaterThan invariants should be considered.
-
-
Constructor Detail
-
SeqSeqFloatGreaterThan
protected SeqSeqFloatGreaterThan(PptSlice ppt, boolean order)
-
SeqSeqFloatGreaterThan
protected SeqSeqFloatGreaterThan(boolean order)
-
SeqSeqFloatGreaterThan
protected SeqSeqFloatGreaterThan(SeqSeqFloatLessThan seq_swap)
-
-
Method Detail
-
get_proto
public static SeqSeqFloatGreaterThan get_proto()
Returns the prototype invariant for SeqSeqFloatGreaterThan
-
enabled
public boolean enabled()
Returns whether or not this invariant is enabled.
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Non-Equal SeqComparison is only valid on integral types.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
protected SeqSeqFloatGreaterThan instantiate_dyn( SeqSeqFloatGreaterThan this, PptSlice slice)
Instantiates the invariant on the specified slice.- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
resurrect_done_swapped
protected Invariant resurrect_done_swapped()
Description copied from class:TwoSequenceFloat
Swaps the variables by inverting the state of swap.- Overrides:
resurrect_done_swapped
in classTwoSequenceFloat
-
repr
public String repr(@GuardSatisfied SeqSeqFloatGreaterThan this)
Description copied from class:TwoSequenceFloat
Returns a representation of the class. This includes the classname, variables, and swap state.- Overrides:
repr
in classTwoSequenceFloat
- Returns:
- a string representation of this
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied SeqSeqFloatGreaterThan this, OutputFormat format)
Description copied from class:Invariant
Return a printed representation of this invariant, in the given format.- Specified by:
format_using
in classInvariant
-
format_simplify
public String format_simplify(@GuardSatisfied SeqSeqFloatGreaterThan this)
-
check_modified
public InvariantStatus check_modified(double @Interned [] v1, double @Interned [] v2, int count)
Description copied from class:TwoSequenceFloat
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 classTwoSequenceFloat
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(double @Interned [] v1, double @Interned [] v2, int count)
Description copied from class:TwoSequenceFloat
Default implementation simply calls check. Subclasses can override.- Overrides:
add_modified
in classTwoSequenceFloat
-
computeConfidence
protected double computeConfidence()
Description copied from class:Invariant
This method computes the confidence that this invariant occurred by chance. Clients should callInvariant.getConfidence()
instead.This method need not check the value of field "falsified", as the caller does that.
- Overrides:
computeConfidence
in classTwoSequenceFloat
- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
isSameFormula
@Pure public boolean isSameFormula(Invariant o)
Description copied from class:TwoSequenceFloat
Return true if both invariants are the same class and the order of the variables (swap) is the same.- Overrides:
isSameFormula
in classTwoSequenceFloat
- 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 classInvariant
- Parameters:
o
- the other invariant to compare to this one- Returns:
- true iff the two invariants represent mutually exclusive mathematical formulas
-
isObviousStatically_SomeInEquality
@Pure public @Nullable DiscardInfo isObviousStatically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.- Overrides:
isObviousStatically_SomeInEquality
in classInvariant
- Returns:
- the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.
-
isObviousDynamically_SomeInEquality
@Pure public @Nullable DiscardInfo isObviousDynamically_SomeInEquality()
Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.- Overrides:
isObviousDynamically_SomeInEquality
in classInvariant
- Returns:
- the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.
-
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 classInvariant
- 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 classInvariant
-
repCheck
public void repCheck()
Description copied from class:Invariant
Check the rep invariants of this.
-
isEqual
@Pure public boolean isEqual()
-
find
public static @Nullable SeqSeqFloatGreaterThan find(PptSlice ppt)
-
get_ni_suppressions
@Pure public @Nullable NISuppressionSet get_ni_suppressions()
Returns a list of non-instantiating suppressions for this invariant.- Overrides:
get_ni_suppressions
in classInvariant
- Returns:
- the set of non-instantiating suppressions for this invariant
-
-