Package daikon.inv.binary.twoString
Class StdString
- Object
-
- Invariant
-
- BinaryInvariant
-
- TwoString
-
- StdString
-
- All Implemented Interfaces:
Serializable
,Cloneable
- Direct Known Subclasses:
StdString.SubString
public abstract class StdString extends TwoString
Baseclass for binary numeric invariants. Each specific invariant is implemented in a subclass (typically, in this file). The subclass must provide the methods instantiate(), check(), and format(). Symmetric functions should define is_symmetric() to return true.- See Also:
- Serialized Form
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static class
StdString.SubString
Represents the substring invariant between two String scalars.-
Nested classes/interfaces inherited from class Invariant
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match
-
-
Field Summary
Fields Modifier and Type Field Description protected static NISuppressor
var1_eq_var2
protected static NISuppressor
var2_eq_var1
-
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
-
-
Method Summary
All Methods Static Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description InvariantStatus
check_modified(String x, String y, int count)
Calls the function specific equal check and returns the correct status.abstract boolean
eq_check(String x, String y)
Returns true if x and y don't invalidate the invariant.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()
boolean
instantiate_ok(VarInfo[] vis)
Returns true if it is ok to instantiate a numeric invariant over the specified slice.@Nullable DiscardInfo
is_subscript(VarInfo[] vis)
Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'.boolean
isExact()
Subclasses should override.@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.InvDef[][]
obvious_checks(VarInfo[] vis)
Returns an array of arrays of antecedents.String
repr()
Returns a representation of the class.-
Methods inherited from class TwoString
add, add_modified, add_unmodified, check, check_unmodified, computeConfidence, get_swap, isSameFormula, resurrect_done, resurrect_done_swapped, 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, 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, isExclusiveFormula, 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_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames
-
-
-
-
Field Detail
-
var1_eq_var2
protected static NISuppressor var1_eq_var2
-
var2_eq_var1
protected static NISuppressor var2_eq_var1
-
-
Method Detail
-
instantiate_ok
public boolean instantiate_ok(VarInfo[] vis)
Returns true if it is ok to instantiate a numeric invariant over the specified slice.- Overrides:
instantiate_ok
in classInvariant
- See Also:
Invariant.valid_types(VarInfo[])
-
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.
-
repr
public String repr(@GuardSatisfied StdString this)
Description copied from class:TwoString
Returns a representation of the class. This includes the classname, variables, and swap state.
-
format_using
@SideEffectFree public String format_using(@GuardSatisfied StdString 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 %varN% are replaced by the variable name in the specified format.- Specified by:
format_using
in classInvariant
-
check_modified
public InvariantStatus check_modified(String x, String y, int count)
Calls the function specific equal check and returns the correct status.- Specified by:
check_modified
in classTwoString
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
-
is_subscript
public @Nullable DiscardInfo is_subscript(VarInfo[] vis)
Checks to see if 'x[a] op y[b]' where 'x[] op y[]' and 'a == b'. Doesn't catch the case where a = b+1.
-
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
-
get_format_str
public abstract String get_format_str(@GuardSatisfied StdString 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(String x, String y)
Returns true if x and y don't invalidate the invariant.
-
obvious_checks
public InvDef[][] obvious_checks(VarInfo[] vis)
Returns an array of arrays of antecedents. If all of the antecedents in any array are true, then the invariant is obvious.
-
get_proto_all
public static List<Invariant> get_proto_all()
-
-