daikon.inv
Class AndJoiner

Object
  Invariant
      Joiner
          AndJoiner

All Implemented Interfaces:

Serializable, Cloneable

public class AndJoiner
extends Joiner

This is a special invariant used internally by Daikon to represent an antecedent invariant in an implication where that antecedent consists of two invariants anded together.

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 inherited from class Joiner

left, right

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, isGuardingPredicate, min_mod_non_missing_samples, ppt, PROBABILITY_JUSTIFIED, PROBABILITY_NEVER, PROBABILITY_UNJUSTIFIED

Constructor Summary

AndJoiner(PptTopLevel ppt, Invariant left, Invariant right)

Method Summary

protected double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
List<Invariant>	conjuncts()
String	format_using(OutputFormat format)
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(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	isSameInvariant(Invariant other)
String	repr() For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

Methods inherited from class Joiner

isInteresting, isObviousDerived, isObviousImplied, isSameFormula, isValidEscExpression, resurrect_done

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, enabled, enoughSamples, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate_dyn, instantiate_ok, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isExact, isExclusiveFormula, isObvious, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isReflexive, 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, valid_types, varNames

Methods inherited from class Object

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

Constructor Detail

AndJoiner

public AndJoiner(PptTopLevel ppt,
                 Invariant left,
                 Invariant right)

Method Detail

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.

Specified by:

computeConfidence in class Invariant

See Also:

Invariant.getConfidence()

repr

public String repr()

Description copied from class: Invariant

For printing invariants, there are two interfaces: repr gives a low-level representation (repr_prop also prints the confidence), and format gives a high-level representation for user output.

Specified by:

repr in class Joiner

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Joiner

conjuncts

public List<Invariant> conjuncts()

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

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.

isSameInvariant

public boolean isSameInvariant(Invariant other)

Overrides:

isSameInvariant in class Joiner

Returns:

true iff the argument is the "same" invariant as this. Same, in this case, means a matching type, formula, and variable names.