Package daikon.inv.unary.sequence
Class EltRangeFloat
- Object
-
- Invariant
-
- UnaryInvariant
-
- SingleSequence
-
- SingleFloatSequence
-
- EltRangeFloat
-
- All Implemented Interfaces:
Serializable
,Cloneable
- Direct Known Subclasses:
EltRangeFloat.EqualMinusOne
,EltRangeFloat.EqualOne
,EltRangeFloat.EqualZero
,EltRangeFloat.GreaterEqual64
,EltRangeFloat.GreaterEqualZero
public abstract class EltRangeFloat extends SingleFloatSequence
Baseclass for unary range based invariants. Each invariant is a special stateless version of bound or oneof. For example EqualZero, BooleanVal, etc). These are never printed, but are used internally as suppressors for ni-suppressions. Each specific invariant is implemented in a subclass (typically in this file).- See Also:
- Serialized Form
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static class
EltRangeFloat.EqualMinusOne
Internal invariant representing double scalars that are equal to minus one.static class
EltRangeFloat.EqualOne
Internal invariant representing double scalars that are equal to one.static class
EltRangeFloat.EqualZero
Internal invariant representing double scalars that are equal to zero.static class
EltRangeFloat.GreaterEqual64
Internal invariant representing double scalars that are greater than or equal to 64.static class
EltRangeFloat.GreaterEqualZero
Internal invariant representing double scalars that are greater than or equal to 0.-
Nested classes/interfaces inherited from class Invariant
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match
-
-
Field Summary
-
Fields inherited from class SingleSequence
dkconfig_SeqIndexDisableAll
-
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
EltRangeFloat()
protected
EltRangeFloat(PptSlice ppt)
-
Method Summary
All Methods Static Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double @Interned [] x, int count)
Similar toSingleFloatSequence.check_modified(double[], int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_modified(double @Interned [] x, int count)
Presents a sample to the invariant.protected double
computeConfidence()
This method computes the confidence that this invariant occurred by chance.abstract boolean
eq_check(double x)
Returns true if x and y don't invalidate the invariant.protected @Nullable EltOneOfFloat
find_oneof(VarInfo[] vis)
Looks for a OneOf invariant over vis.String
format_using(OutputFormat format)
Returns a string in the specified format that describes the invariant.abstract String
get_format_str(OutputFormat format)
Return a format string for the specified output format.static List<Invariant>
get_proto_all()
Returns a list of prototypes of all of the range invariants.boolean
instantiate_ok(VarInfo[] vis)
Check that instantiation is ok.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)
All range invariants except Even and PowerOfTwo are obvious since they represented by some version of OneOf or Bound.boolean
isSameFormula(Invariant other)
Returns true iff the two invariants represent the same mathematical formula.-
Methods inherited from class SingleFloatSequence
add, add_unmodified, check, check_unmodified, valid_types
-
Methods inherited from class SingleSequence
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, enabled, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_dyn, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, 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, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames
-
-
-
-
Constructor Detail
-
EltRangeFloat
protected EltRangeFloat(PptSlice ppt)
-
EltRangeFloat
protected EltRangeFloat()
-
-
Method Detail
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Check that instantiation is ok. The type must be integral (not boolean or hash code).- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied EltRangeFloat this, OutputFormat format)
Returns a string in the specified format that describes the invariant. The generic format string is obtained from the subclass specific get_format_str(). Instances of %var1% are replaced by the variable name in the specified format.- Specified by:
format_using
in classInvariant
-
check_modified
public InvariantStatus check_modified(double @Interned [] x, int count)
Description copied from class:SingleFloatSequence
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 classSingleFloatSequence
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 [] x, int count)
Description copied from class:SingleFloatSequence
Similar toSingleFloatSequence.check_modified(double[], 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 callSingleFloatSequence.check_modified(double[], int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classSingleFloatSequence
-
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.
- Specified by:
computeConfidence
in classInvariant
- 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 classInvariant
- 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 classInvariant
- Parameters:
other
- the other invariant to compare to this one- Returns:
- true iff the two invariants represent mutually exclusive mathematical formulas
-
isObviousDynamically
@Pure public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis)
All range invariants except Even and PowerOfTwo are obvious since they represented by some version of OneOf or Bound.- Overrides:
isObviousDynamically
in classInvariant
-
find_oneof
protected @Nullable EltOneOfFloat find_oneof(VarInfo[] vis)
Looks for a OneOf invariant over vis. Used by Even and PowerOfTwo to dynamically suppress those invariants if a OneOf exists.
-
get_format_str
public abstract String get_format_str(@GuardSatisfied EltRangeFloat this, OutputFormat format)
Return a format string for the specified output format. Each instance of %varN% will be replaced by the correct name for varN.
-
eq_check
public abstract boolean eq_check(double x)
Returns true if x and y don't invalidate the invariant.
-
get_proto_all
public static List<Invariant> get_proto_all()
Returns a list of prototypes of all of the range invariants.
-
-