daikon.inv.binary.twoSequence
Class SeqSeqStringLessThan

Object
  Invariant
      BinaryInvariant
          TwoSequenceString
              SeqSeqStringLessThan

All Implemented Interfaces:

Comparison, Serializable, Cloneable

public class SeqSeqStringLessThan
extends TwoSequenceString
implements Comparison

Represents invariants between two sequences of String values. If order matters for each variable (which it does by default), then the sequences are compared lexically. Prints as x[] < y[] lexically. If the auxiliary information (e.g., order matters) doesn't match between two variables, then this invariant cannot apply to those variables.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Field Summary

static boolean

dkconfig_enabled Boolean.

Fields inherited from class TwoSequenceString

swap

Fields inherited from class Invariant

CONFIDENCE_JUSTIFIED, CONFIDENCE_NEVER, CONFIDENCE_UNJUSTIFIED, debugFlow, debugGuarding, debugIsObvious, debugIsWorthPrinting, debugPrint, debugPrintEquality, dkconfig_confidence_limit, dkconfig_fuzzy_ratio, dkconfig_simplify_define_predicates, falsified, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

protected	SeqSeqStringLessThan(PptSlice ppt, boolean order)
protected	SeqSeqStringLessThan(SeqSeqStringGreaterThan seq_swap)

Method Summary

InvariantStatus	add_modified(String[] v1, String[] v2, int count) Default implementation simply calls check.
InvariantStatus	check_modified(String[] v1, String[] v2, int count)
protected double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
boolean	enabled() Returns whether or not this invariant is enabled
double	eq_confidence() If the invariant is a equality invariant, then its confidence.
static SeqSeqStringLessThan	find(PptSlice ppt)
String	format_simplify()
String	format_using(OutputFormat format)
NISuppressionSet	get_ni_suppressions() Returns a list of non-instantiating suppressions for this invariant.
static SeqSeqStringLessThan	get_proto() Returns the prototype invariant for SeqSeqStringLessThan
protected SeqSeqStringLessThan	instantiate_dyn(PptSlice slice) Instantiates the invariant on the specified slice
boolean	instantiate_ok(VarInfo[] vis) Non-Equal SeqComparison is only valid on integral types
boolean	isEqual()
boolean	isExclusiveFormula(Invariant o)
DiscardInfo	isObviousDynamically_SomeInEquality() Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.
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.
DiscardInfo	isObviousStatically_SomeInEquality() Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.
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 o) Return true if both invariants are the same class and the order of the variables (swap) is the same.
void	repCheck() Check the rep invariants of this.
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 TwoSequenceString

add_unmodified, add, check_unmodified, check, get_swap, resurrect_done_unswapped, resurrect_done, 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, clear_falsified, clone_and_permute, clone, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enoughSamples, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isExact, isInteresting, isObvious, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames

Methods inherited from class Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface Comparison

var1, var2

Field Detail

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff SeqSeqStringLessThan invariants should be considered.

Constructor Detail

SeqSeqStringLessThan

protected SeqSeqStringLessThan(PptSlice ppt,
                               boolean order)

SeqSeqStringLessThan

protected SeqSeqStringLessThan(SeqSeqStringGreaterThan seq_swap)

Method Detail

get_proto

public static SeqSeqStringLessThan get_proto()

Returns the prototype invariant for SeqSeqStringLessThan

enabled

public boolean enabled()

Returns whether or not this invariant is enabled

Overrides:

enabled in class Invariant

instantiate_ok

public boolean instantiate_ok(VarInfo[] vis)

Non-Equal SeqComparison is only valid on integral types

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

instantiate_dyn

protected SeqSeqStringLessThan instantiate_dyn(PptSlice slice)

Instantiates the invariant on the specified slice

Overrides:

instantiate_dyn in class Invariant

Returns:

the new invariant

resurrect_done_swapped

protected Invariant resurrect_done_swapped()

Description copied from class: TwoSequenceString

Swaps the variables by inverting the state of swap.

Overrides:

resurrect_done_swapped in class TwoSequenceString

repr

public String repr()

Description copied from class: TwoSequenceString

Returns a representation of the class. This includes the classname, variables, and swap state.

Overrides:

repr in class TwoSequenceString

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Invariant

format_simplify

public String format_simplify()

check_modified

public InvariantStatus check_modified(String[] v1,
                                      String[] v2,
                                      int count)

Specified by:

check_modified in class TwoSequenceString

add_modified

public InvariantStatus add_modified(String[] v1,
                                    String[] v2,
                                    int count)

Description copied from class: TwoSequenceString

Default implementation simply calls check. Subclasses can override.

Overrides:

add_modified in class TwoSequenceString

computeConfidence

protected double computeConfidence()

Description copied from class: Invariant

This method computes the confidence that this invariant occurred by chance. Users should use getConfidence() instead.

Overrides:

computeConfidence in class TwoSequenceString

See Also:

Invariant.getConfidence()

eq_confidence

public double eq_confidence()

Description copied from interface: Comparison

If the invariant is a equality invariant, then its confidence. Otherwise, Invariant.CONFIDENCE_NEVER.

Specified by:

eq_confidence in interface Comparison

isSameFormula

public boolean isSameFormula(Invariant o)

Description copied from class: TwoSequenceString

Return true if both invariants are the same class and the order of the variables (swap) is the same.

Overrides:

isSameFormula in class TwoSequenceString

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.

isExclusiveFormula

public boolean isExclusiveFormula(Invariant o)

Overrides:

isExclusiveFormula in 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.

isObviousStatically_SomeInEquality

public DiscardInfo isObviousStatically_SomeInEquality()

Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.

Overrides:

isObviousStatically_SomeInEquality in class Invariant

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isObviousDynamically_SomeInEquality

public DiscardInfo isObviousDynamically_SomeInEquality()

Since this invariant can be a postProcessed equality, we have to handle isObvious especially to avoid circular isObvious relations.

Overrides:

isObviousDynamically_SomeInEquality in class Invariant

Returns:

the VarInfo array that contains the VarInfos that showed this invariant to be obvious. The contains variables that are elementwise in the same equality set as this.ppt.var_infos. Can be null if no such assignment exists.

isObviousStatically

public 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 class Invariant

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

public 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 class Invariant

repCheck

public void repCheck()

Description copied from class: Invariant

Check the rep invariants of this.

Overrides:

repCheck in class Invariant

isEqual

public boolean isEqual()

find

public static SeqSeqStringLessThan find(PptSlice ppt)

get_ni_suppressions

public NISuppressionSet get_ni_suppressions()

Returns a list of non-instantiating suppressions for this invariant.

Overrides:

get_ni_suppressions in class Invariant