Class TwoScalar
- Object
-
- Invariant
-
- BinaryInvariant
-
- TwoScalar
-
- All Implemented Interfaces:
Serializable
,Cloneable
- Direct Known Subclasses:
IntEqual
,IntGreaterEqual
,IntGreaterThan
,IntLessEqual
,IntLessThan
,IntNonEqual
,LinearBinary
,NumericInt
public abstract class TwoScalar extends BinaryInvariant
Base class for invariants over two variables of type long. An example isy = abs(x)
.Provides a simpler mechanism for non-symmetric invariants to function over both permutations of their variables.
Non-symmetric invariants must instantiate two objects (one for each argument order). This is tracked by the variable swap. They must always access their variables via the methods var1() and var2() which return the correct variable (based on the swap setting). No other work is necessary, all permuations and resurrection is handled here.
Symmetric invariants should define symmetric() to return true or override resurrect_done_swapped to do nothing. Non-symmetric invariants that use converse operations (eg, less than and greater than) rather than argument swapping should override resurrect_done_swapped to return the correct class.
- 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 protected boolean
swap
-
Fields inherited from class Invariant
checkedMergeOverridden, 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
-
-
Method Summary
All Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add(@Interned Object val1, @Interned Object val2, int mod_index, int count)
InvariantStatus
add_modified(long v1, long v2, int count)
Default implementation simply calls check.InvariantStatus
add_unmodified(long v1, long v2, int count)
By default, do nothing if the value hasn't been seen yet.InvariantStatus
check(@Interned Object val1, @Interned Object val2, int mod_index, int count)
abstract InvariantStatus
check_modified(long v1, long v2, int count)
Presents a sample to the invariant.InvariantStatus
check_unmodified(long v1, long v2, int count)
protected double
computeConfidence()
This method computes the confidence that this invariant occurred by chance.boolean
get_swap()
Returns whether or not the variable order is currently swapped for this invariant.boolean
isSameFormula(Invariant other)
Return true if both invariants are the same class and the order of the variables (swap) is the same.String
repr()
Returns a representation of the class.protected Invariant
resurrect_done(int[] permutation)
Checks to see if the variable order was swapped and calls the correct routine to handle it.protected Invariant
resurrect_done_swapped()
Swaps the variables by inverting the state of swap.protected Invariant
resurrect_done_unswapped()
Subclasses can override in the rare cases they need to fix things even when not swapped.boolean
valid_types(VarInfo[] vis)
Returns whether or not the invariant is valid over the basic types in vis.VarInfo
var1()
Returns the first variable.VarInfo
var1(VarInfo[] vis)
Returns the first variable from the specified vis.VarInfo
var2()
Returns the first variable.VarInfo
var2(VarInfo[] vis)
Returns the first variable in the specified vis.-
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, enabled, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, format_using, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_dyn, instantiate_ok, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isExclusiveFormula, isObvious, isObviousDynamically, 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
-
-
-
-
Field Detail
-
swap
protected boolean swap
-
-
Method Detail
-
valid_types
public final boolean valid_types(VarInfo[] vis)
Description copied from class:Invariant
Returns whether or not the invariant is valid over the basic types in vis. This only checks basic types (scalar, string, array, etc) and should match the basic superclasses of invariant (SingleFloat, SingleScalarSequence, ThreeScalar, etc). More complex checks that depend on variable details can be implemented in instantiate_ok().- Specified by:
valid_types
in classInvariant
- See Also:
Invariant.instantiate_ok(VarInfo[])
-
get_swap
public boolean get_swap()
Returns whether or not the variable order is currently swapped for this invariant.- Overrides:
get_swap
in classBinaryInvariant
-
resurrect_done
protected Invariant resurrect_done(int[] permutation)
Checks to see if the variable order was swapped and calls the correct routine to handle it.- Specified by:
resurrect_done
in classInvariant
- Parameters:
permutation
- the permutation- Returns:
- the permuted invariant
-
resurrect_done_swapped
protected Invariant resurrect_done_swapped()
Swaps the variables by inverting the state of swap.
-
resurrect_done_unswapped
protected Invariant resurrect_done_unswapped()
Subclasses can override in the rare cases they need to fix things even when not swapped.
-
var1
public VarInfo var1(@GuardSatisfied TwoScalar this)
Returns the first variable. This is the only mechanism by which subclasses should access variables.
-
var2
public VarInfo var2(@GuardSatisfied TwoScalar this)
Returns the first variable. This is the only mechanism by which subclasses should access variables.
-
var1
public VarInfo var1(VarInfo[] vis)
Returns the first variable from the specified vis. This is the only mechanism by which subclasses should access variables.
-
var2
public VarInfo var2(VarInfo[] vis)
Returns the first variable in the specified vis. This is the only mechanism by which subclasses should access variables.
-
check
public InvariantStatus check(@Interned Object val1, @Interned Object val2, int mod_index, int count)
- Specified by:
check
in classBinaryInvariant
-
add
public InvariantStatus add(@Interned Object val1, @Interned Object val2, int mod_index, int count)
- Specified by:
add
in classBinaryInvariant
-
check_modified
public abstract InvariantStatus check_modified(long v1, long v2, int count)
Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.- Parameters:
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
-
check_unmodified
public InvariantStatus check_unmodified(long v1, long v2, int count)
-
add_modified
public InvariantStatus add_modified(long v1, long v2, int count)
Default implementation simply calls check. Subclasses can override.
-
add_unmodified
public InvariantStatus add_unmodified(long v1, long v2, int count)
By default, do nothing if the value hasn't been seen yet. Subclasses can override this.
-
repr
public String repr(@GuardSatisfied TwoScalar this)
Returns a representation of the class. This includes the classname, variables, and swap state.
-
isSameFormula
@Pure public boolean isSameFormula(Invariant other)
Return true if both invariants are the same class and the order of the variables (swap) is the same.- 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
-
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()
-
-