Package daikon.inv.unary.scalar
Class NonModulus
- Object
-
- Invariant
-
- UnaryInvariant
-
- SingleScalar
-
- NonModulus
-
- All Implemented Interfaces:
Serializable
,Cloneable
public class NonModulus extends SingleScalar
Represents long scalars that are never equal tor (mod m)
where all other numbers in the same range (i.e., all the values thatx
doesn't take frommin(x)
tomax(x)
) are equal tor (mod m)
. Prints asx != r (mod m)
, wherer
is the remainder andm
is the modulus.- 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 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 Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(long value, int count)
Similar toSingleScalar.check_modified(long, int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_modified(long value, int count)
Presents a sample to the invariant.NonModulus
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 class of invariants is currently enabled.String
format_using(OutputFormat format)
Return a printed representation of this invariant, in the given format.static NonModulus
get_proto()
Returns the prototype invariant for NonModulus.boolean
hasModulusRemainder(long modulus, long remainder)
Returns true if this has the given modulus and remainder.protected NonModulus
instantiate_dyn(PptSlice slice)
Instantiates (creates) an invariant of the same class on the specified slice.boolean
instantiate_ok(VarInfo[] vis)
Returns true if it makes sense to instantiate this invariant over the specified variables.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.boolean
isSameFormula(Invariant o)
Returns true iff the two invariants represent the same mathematical formula.@Nullable NonModulus
merge(List<Invariant> invs, PptSlice parent_ppt)
Merge the invariants in invs to form a new invariant.String
repr()
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.-
Methods inherited from class SingleScalar
add, add_unmodified, check, check_unmodified, valid_types, valid_types_static, var
-
Methods inherited from class UnaryInvariant
resurrect_done
-
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, enoughSamples, 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, isActive, isAllPrestate, isEqualityComparison, isExact, 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, 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
-
dkconfig_enabled
public static boolean dkconfig_enabled
Boolean. True iff NonModulus invariants should be considered.
-
-
Method Detail
-
get_proto
public static NonModulus get_proto()
Returns the prototype invariant for NonModulus.
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Description copied from class:Invariant
Returns true if it makes sense to instantiate this invariant over the specified variables. Checks details beyond what is provided byInvariant.valid_types(daikon.VarInfo[])
. This should never be called without calling valid_types() first (implementations should be able to presume that valid_types() returns true).This method does not have to be overridden; the default implementation in Invariant returns true.
- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
enabled
public boolean enabled()
Description copied from class:Invariant
Returns whether or not this class of invariants is currently enabled.Its implementation is almost always
return dkconfig_enabled;
.
-
instantiate_dyn
protected NonModulus instantiate_dyn( NonModulus 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 thanInvariant.clone()
so that checks inInvariant.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 classInvariant
- Returns:
- the new invariant
-
clone
@SideEffectFree public NonModulus clone(@GuardSatisfied NonModulus this)
Description copied from class:Invariant
Do nothing special, Overridden to remove exception from declaration.
-
repr
public String repr(@GuardSatisfied NonModulus this)
Description copied from class:Invariant
For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob()
also prints the confidence), andInvariant.format()
gives a high-level representation for user output.
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied NonModulus 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
-
check_modified
public InvariantStatus check_modified(long value, int count)
Description copied from class:SingleScalar
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 classSingleScalar
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(long value, int count)
Description copied from class:SingleScalar
Similar toSingleScalar.check_modified(long, 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 callSingleScalar.check_modified(long, int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classSingleScalar
-
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 o)
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:
o
- the invariant to compare to this one- Returns:
- true iff the two invariants represent the same mathematical formula. Does not consider
-
hasModulusRemainder
public boolean hasModulusRemainder(long modulus, long remainder)
Returns true if this has the given modulus and remainder.
-
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
-
merge
public @Nullable NonModulus merge( NonModulus this, List<Invariant> invs, PptSlice parent_ppt)
Description copied from class:Invariant
Merge the invariants in invs to form a new invariant. This implementation merely returns a clone of the first invariant in the list. This is correct for simple invariants whose equation or statistics don't depend on the actual samples seen. It should be overriden for more complex invariants (eg, bound, oneof, linearbinary, etc).- Overrides:
merge
in classInvariant
- Parameters:
invs
- list of invariants to merge. The invariants must all be of the same type and should come from the children of parent_ppt. They should also 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
-
-