daikon.inv.ternary.threeScalar
Class LinearTernary

Object
  Invariant
      TernaryInvariant
          ThreeScalar
              LinearTernary

All Implemented Interfaces:

Serializable, Cloneable

public class LinearTernary
extends ThreeScalar

Represents a Linear invariant over three long scalars x, y, and z, of the form ax + by + cz + d = 0. The constants a, b, c, and d are mutually relatively prime, and the constant a is always positive.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

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

Field Summary

LinearTernaryCore	core
static boolean	debugLinearTernary
static boolean	dkconfig_enabled Boolean.

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

protected	LinearTernary()
protected	LinearTernary(PptSlice ppt)

Method Summary

InvariantStatus	add_modified(long x, long y, long z, int count) This method need not check for falsified; that is done by the caller.
InvariantStatus	check_modified(long x, long y, long z, int count)
LinearTernary	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 invariant is enabled
boolean	enoughSamples()
static LinearTernary	find(PptSlice ppt)
static Vector<LinearTernary>	findAll(VarInfo vi)
String	format_using(OutputFormat format)
static LinearTernary	get_proto() Returns the prototype invariant for LinearTernary
LinearTernary	instantiate_dyn(PptSlice slice) Instantiate the invariant on the specified slice
boolean	instantiate_ok(VarInfo[] vis) LinearTernary is only valid on non-constant integral types
boolean	isActive() Returns whether or not the invariant is currently active.
boolean	isExact() Subclasses should override.
boolean	isExclusiveFormula(Invariant other)
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.
boolean	isSameFormula(Invariant other)
Invariant	merge(List<Invariant> invs, PptSlice parent_ppt) Merge the invariants in invs to form a new invariant.
boolean	mergeFormulasOk() Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points.
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.
protected Invariant	resurrect_done(int[] permutation) Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
InvariantStatus	setup(LinearBinary lb, VarInfo con_var, long con_val)
InvariantStatus	setup(OneOfScalar oo, VarInfo v1, long con1, VarInfo v2, long con2)

Methods inherited from class ThreeScalar

add_unmodified, add, check_unmodified, check, valid_types, var1, var2, var3

Methods inherited from class Invariant

add_sample, asInvClass, clear_falsified, clone_and_permute, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, falsify, find, format_too_few_samples, format_unimplemented, format, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, is_false, is_ni_suppressed, isAllPrestate, isInteresting, isObvious, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousDynamically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, isReflexive, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, 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

Methods inherited from class Object

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

Field Detail

dkconfig_enabled

public static boolean dkconfig_enabled

Boolean. True iff LinearTernary invariants should be considered.

debugLinearTernary

public static final boolean debugLinearTernary

See Also:

Constant Field Values

core

public LinearTernaryCore core

Constructor Detail

LinearTernary

protected LinearTernary(PptSlice ppt)

LinearTernary

protected LinearTernary()

Method Detail

get_proto

public static LinearTernary get_proto()

Returns the prototype invariant for LinearTernary

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)

LinearTernary is only valid on non-constant integral types

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

instantiate_dyn

public LinearTernary instantiate_dyn(PptSlice slice)

Instantiate the invariant on the specified slice

Overrides:

instantiate_dyn in class Invariant

Returns:

the new invariant

clone

public LinearTernary clone()

Description copied from class: Invariant

Do nothing special, Overridden to remove exception from declaration

Overrides:

clone in class Invariant

resurrect_done

protected Invariant resurrect_done(int[] permutation)

Description copied from class: Invariant

Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.

Overrides:

resurrect_done in class TernaryInvariant

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.

Overrides:

repr in class Invariant

format_using

public String format_using(OutputFormat format)

Specified by:

format_using in class Invariant

isActive

public boolean isActive()

Description copied from class: Invariant

Returns whether or not the invariant is currently active. This is used to identify those invariants that require a certain number of points before they actually do computation (eg, LinearBinary) This is used during suppresion. Any invariant that is not active cannot suppress another invariant

Overrides:

isActive in class Invariant

setup

public InvariantStatus setup(LinearBinary lb,
                             VarInfo con_var,
                             long con_val)

setup

public InvariantStatus setup(OneOfScalar oo,
                             VarInfo v1,
                             long con1,
                             VarInfo v2,
                             long con2)

check_modified

public InvariantStatus check_modified(long x,
                                      long y,
                                      long z,
                                      int count)

Specified by:

check_modified in class ThreeScalar

add_modified

public InvariantStatus add_modified(long x,
                                    long y,
                                    long z,
                                    int count)

Description copied from class: ThreeScalar

This method need not check for falsified; that is done by the caller.

Specified by:

add_modified in class ThreeScalar

enoughSamples

public boolean enoughSamples()

Overrides:

enoughSamples in class Invariant

Returns:

true if the invariant has enough samples to have its computed constants well-formed. Is overridden in classes like LinearBinary/Ternary and Upper/LowerBound.

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()

isExact

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.

Overrides:

isExact in class Invariant

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

isSameFormula

public boolean isSameFormula(Invariant other)

Overrides:

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

isExclusiveFormula

public boolean isExclusiveFormula(Invariant other)

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.

find

public static LinearTernary find(PptSlice ppt)

findAll

public static Vector<LinearTernary> findAll(VarInfo vi)

mergeFormulasOk

public boolean mergeFormulasOk()

Description copied from class: Invariant

Returns whether or not it is possible to merge invariants of the same class but with different formulas when combining invariants from lower ppts to build invariants at upper program points. Invariants that have this characteristic (eg, bound, oneof) should override this function. Note that invariants that can do this, normally need special merge code as well (to merge the different formulas into a single formula at the upper point

Overrides:

mergeFormulasOk in class Invariant

merge

public Invariant merge(List<Invariant> invs,
                       PptSlice parent_ppt)

Merge the invariants in invs to form a new invariant. Each must be a LinearTernary invariant. The work is done by the LinearTernary core

Overrides:

merge in class Invariant

Parameters:

invs - List of invariants to merge. They should 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.