Package daikon.inv.binary.twoScalar
Class LinearBinaryFloat
- Object
-
- Invariant
-
- BinaryInvariant
-
- TwoFloat
-
- LinearBinaryFloat
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class LinearBinaryFloat extends TwoFloat
Represents a Linear invariant between two double scalarsx
andy
, of the formax + by + c = 0
. The constantsa
,b
andc
are mutually relatively prime, and the constanta
is always positive.- 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 LinearBinaryCoreFloat
core
static boolean
dkconfig_enabled
Boolean.-
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
LinearBinaryFloat()
protected
LinearBinaryFloat(PptSlice ppt)
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double x, double y, int count)
Default implementation simply calls check.InvariantStatus
check_modified(double x, double y, int count)
Presents a sample to the invariant.LinearBinaryFloat
clone()
Do nothing special, Overridden to remove exception from declaration.protected double
computeConfidence()
This method computes the confidence that this invariant occurred by chance.boolean
enabled()
Returns whether or not this invariant is enabled.boolean
enoughSamples()
Returns true if the invariant has enough samples to have its computed constants well-formed.static @Nullable LinearBinaryFloat
find(PptSlice ppt)
static List<LinearBinaryFloat>
findAll(VarInfo vi)
String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.static LinearBinaryFloat
get_proto()
Returns a prototype LinearBinaryFloat invariant.protected LinearBinaryFloat
instantiate_dyn(PptSlice slice)
Instantiate an invariant on the specified slice.boolean
instantiate_ok(VarInfo[] vis)
LinearBinary is only valid on integral types.boolean
isActive()
Returns whether or not the invariant is currently active.boolean
isExact()
Subclasses should override.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)
Return true if both invariants are the same class and the order of the variables (swap) is the same.@Nullable Invariant
merge(List<Invariant> invs, PptSlice parent_ppt)
Merge the invariants in invs to form a new invariant.boolean
mergeFormulasOk()
Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points.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 TwoFloat
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_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isAllPrestate, isEqualityComparison, isObvious, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, 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
-
-
-
-
Field Detail
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff LinearBinary invariants should be considered.
-
core
public LinearBinaryCoreFloat core
-
-
Constructor Detail
-
LinearBinaryFloat
protected LinearBinaryFloat(PptSlice ppt)
-
LinearBinaryFloat
protected LinearBinaryFloat()
-
-
Method Detail
-
get_proto
public static LinearBinaryFloat get_proto()
Returns a prototype LinearBinaryFloat invariant.
-
enabled
public boolean enabled()
Returns whether or not this invariant is enabled.
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
LinearBinary is only valid on integral types.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
instantiate_dyn
protected LinearBinaryFloat instantiate_dyn( LinearBinaryFloat this, PptSlice slice)
Instantiate an invariant on the specified slice.- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
clone
@SideEffectFree public LinearBinaryFloat clone(@GuardSatisfied LinearBinaryFloat this)
Description copied from class:Invariant
Do nothing special, Overridden to remove exception from declaration.
-
resurrect_done_swapped
protected Invariant resurrect_done_swapped()
Description copied from class:TwoFloat
Swaps the variables by inverting the state of swap.- Overrides:
resurrect_done_swapped
in classTwoFloat
-
repr
public String repr(@GuardSatisfied LinearBinaryFloat this)
Description copied from class:TwoFloat
Returns a representation of the class. This includes the classname, variables, and swap state.
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied LinearBinaryFloat 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
-
isActive
@Pure public boolean isActive()
Description copied from class:Invariant
Returns whether or not the invariant is currently active. This is used to identify those invariants that require a certain number of points before they actually do computation (eg, LinearBinary)This is used during suppresion. Any invariant that is not active cannot suppress another invariant.
-
mergeFormulasOk
public boolean mergeFormulasOk()
Description copied from class:Invariant
Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points. Invariants that have this characteristic (eg, bound, oneof) should override this function. Note that invariants that can do this, normally need special merge code as well (to merge the different formulas into a single formula at the upper point.- Overrides:
mergeFormulasOk
in classInvariant
- Returns:
- true if invariants with different formulas can be merged
-
merge
public @Nullable Invariant merge(List<Invariant> invs, PptSlice parent_ppt)
Merge the invariants in invs to form a new invariant. Each must be a LinearBinaryFloat invariant. The work is done by the LinearBinary core- Overrides:
merge
in classInvariant
- Parameters:
invs
- list of invariants to merge. They should all be permuted to match the variable order in parent_ppt.parent_ppt
- slice that will contain the new invariant- Returns:
- the merged invariant or null if the invariants didn't represent the same invariant
-
check_modified
public InvariantStatus check_modified(double x, double y, int count)
Description copied from class:TwoFloat
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 classTwoFloat
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 x, double y, int count)
Description copied from class:TwoFloat
Default implementation simply calls check. Subclasses can override.- Overrides:
add_modified
in classTwoFloat
-
enoughSamples
public boolean enoughSamples(@GuardSatisfied LinearBinaryFloat this)
Description copied from class:Invariant
Returns true if the invariant has enough samples to have its computed constants well-formed. Is overridden in classes like LinearBinary/Ternary and Upper/LowerBound.- Overrides:
enoughSamples
in classInvariant
- Returns:
- true if the invariant has enough samples to have its computed constants well-formed
-
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 classTwoFloat
- Returns:
- confidence of this invariant
- See Also:
Invariant.getConfidence()
-
isExact
@Pure public boolean isExact()
Description copied from class:Invariant
Subclasses should override. An exact invariant indicates that given all but one variable value, the last one can be computed. (I think that's correct, anyway.) Examples are IntComparison (when only equality is possible), LinearBinary, FunctionUnary. OneOf is treated differently, as an interface. The result of this method does not depend on whether the invariant is justified, destroyed, etc.
-
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
-
isSameFormula
@Pure public boolean isSameFormula(Invariant other)
Description copied from class:TwoFloat
Return true if both invariants are the same class and the order of the variables (swap) is the same.- Overrides:
isSameFormula
in classTwoFloat
- 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
-
find
public static @Nullable LinearBinaryFloat find(PptSlice ppt)
-
findAll
public static List<LinearBinaryFloat> findAll(VarInfo vi)
-
-