daikon.inv.ternary.threeScalar
Class FunctionBinary

Object
  Invariant
      TernaryInvariant
          ThreeScalar
              FunctionBinary

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

FunctionBinary.BitwiseAndLong_xyz, FunctionBinary.BitwiseAndLong_yxz, FunctionBinary.BitwiseAndLong_zxy, FunctionBinary.BitwiseOrLong_xyz, FunctionBinary.BitwiseOrLong_yxz, FunctionBinary.BitwiseOrLong_zxy, FunctionBinary.BitwiseXorLong_xyz, FunctionBinary.BitwiseXorLong_yxz, FunctionBinary.BitwiseXorLong_zxy, FunctionBinary.DivisionLong_xyz, FunctionBinary.DivisionLong_xzy, FunctionBinary.DivisionLong_yxz, FunctionBinary.DivisionLong_yzx, FunctionBinary.DivisionLong_zxy, FunctionBinary.DivisionLong_zyx, FunctionBinary.GcdLong_xyz, FunctionBinary.GcdLong_yxz, FunctionBinary.GcdLong_zxy, FunctionBinary.LogicalAndLong_xyz, FunctionBinary.LogicalAndLong_yxz, FunctionBinary.LogicalAndLong_zxy, FunctionBinary.LogicalOrLong_xyz, FunctionBinary.LogicalOrLong_yxz, FunctionBinary.LogicalOrLong_zxy, FunctionBinary.LogicalXorLong_xyz, FunctionBinary.LogicalXorLong_yxz, FunctionBinary.LogicalXorLong_zxy, FunctionBinary.LshiftLong_xyz, FunctionBinary.LshiftLong_xzy, FunctionBinary.LshiftLong_yxz, FunctionBinary.LshiftLong_yzx, FunctionBinary.LshiftLong_zxy, FunctionBinary.LshiftLong_zyx, FunctionBinary.MaximumLong_xyz, FunctionBinary.MaximumLong_yxz, FunctionBinary.MaximumLong_zxy, FunctionBinary.MinimumLong_xyz, FunctionBinary.MinimumLong_yxz, FunctionBinary.MinimumLong_zxy, FunctionBinary.ModLong_xyz, FunctionBinary.ModLong_xzy, FunctionBinary.ModLong_yxz, FunctionBinary.ModLong_yzx, FunctionBinary.ModLong_zxy, FunctionBinary.ModLong_zyx, FunctionBinary.MultiplyLong_xyz, FunctionBinary.MultiplyLong_yxz, FunctionBinary.MultiplyLong_zxy, FunctionBinary.PowerLong_xyz, FunctionBinary.PowerLong_xzy, FunctionBinary.PowerLong_yxz, FunctionBinary.PowerLong_yzx, FunctionBinary.PowerLong_zxy, FunctionBinary.PowerLong_zyx, FunctionBinary.RshiftSignedLong_xyz, FunctionBinary.RshiftSignedLong_xzy, FunctionBinary.RshiftSignedLong_yxz, FunctionBinary.RshiftSignedLong_yzx, FunctionBinary.RshiftSignedLong_zxy, FunctionBinary.RshiftSignedLong_zyx, FunctionBinary.RshiftUnsignedLong_xyz, FunctionBinary.RshiftUnsignedLong_xzy, FunctionBinary.RshiftUnsignedLong_yxz, FunctionBinary.RshiftUnsignedLong_yzx, FunctionBinary.RshiftUnsignedLong_zxy, FunctionBinary.RshiftUnsignedLong_zyx

public abstract class FunctionBinary
extends ThreeScalar

Base class for each of the FunctionBinary functions and permutatons. Most of the work is done here. The subclasses basically define the function and return information describing the function and permutation to these methods

See Also:

Serialized Form

Nested Class Summary

static class	FunctionBinary.BitwiseAndLong_xyz Represents the invariant x = BitwiseAnd (y, z) over three long scalars.
static class	FunctionBinary.BitwiseAndLong_yxz Represents the invariant y = BitwiseAnd (x, z) over three long scalars.
static class	FunctionBinary.BitwiseAndLong_zxy Represents the invariant z = BitwiseAnd (x, y) over three long scalars.
static class	FunctionBinary.BitwiseOrLong_xyz Represents the invariant x = BitwiseOr (y, z) over three long scalars.
static class	FunctionBinary.BitwiseOrLong_yxz Represents the invariant y = BitwiseOr (x, z) over three long scalars.
static class	FunctionBinary.BitwiseOrLong_zxy Represents the invariant z = BitwiseOr (x, y) over three long scalars.
static class	FunctionBinary.BitwiseXorLong_xyz Represents the invariant x = BitwiseXor (y, z) over three long scalars.
static class	FunctionBinary.BitwiseXorLong_yxz Represents the invariant y = BitwiseXor (x, z) over three long scalars.
static class	FunctionBinary.BitwiseXorLong_zxy Represents the invariant z = BitwiseXor (x, y) over three long scalars.
static class	FunctionBinary.DivisionLong_xyz Represents the invariant x = Division (y, z) over three long scalars.
static class	FunctionBinary.DivisionLong_xzy Represents the invariant x = Division (z, y) over three long scalars.
static class	FunctionBinary.DivisionLong_yxz Represents the invariant y = Division (x, z) over three long scalars.
static class	FunctionBinary.DivisionLong_yzx Represents the invariant y = Division (z, x) over three long scalars.
static class	FunctionBinary.DivisionLong_zxy Represents the invariant z = Division (x, y) over three long scalars.
static class	FunctionBinary.DivisionLong_zyx Represents the invariant z = Division (y, x) over three long scalars.
static class	FunctionBinary.GcdLong_xyz Represents the invariant x = Gcd (y, z) over three long scalars.
static class	FunctionBinary.GcdLong_yxz Represents the invariant y = Gcd (x, z) over three long scalars.
static class	FunctionBinary.GcdLong_zxy Represents the invariant z = Gcd (x, y) over three long scalars.
static class	FunctionBinary.LogicalAndLong_xyz Represents the invariant x = LogicalAnd (y, z) over three long scalars.
static class	FunctionBinary.LogicalAndLong_yxz Represents the invariant y = LogicalAnd (x, z) over three long scalars.
static class	FunctionBinary.LogicalAndLong_zxy Represents the invariant z = LogicalAnd (x, y) over three long scalars.
static class	FunctionBinary.LogicalOrLong_xyz Represents the invariant x = LogicalOr (y, z) over three long scalars.
static class	FunctionBinary.LogicalOrLong_yxz Represents the invariant y = LogicalOr (x, z) over three long scalars.
static class	FunctionBinary.LogicalOrLong_zxy Represents the invariant z = LogicalOr (x, y) over three long scalars.
static class	FunctionBinary.LogicalXorLong_xyz Represents the invariant x = LogicalXor (y, z) over three long scalars.
static class	FunctionBinary.LogicalXorLong_yxz Represents the invariant y = LogicalXor (x, z) over three long scalars.
static class	FunctionBinary.LogicalXorLong_zxy Represents the invariant z = LogicalXor (x, y) over three long scalars.
static class	FunctionBinary.LshiftLong_xyz Represents the invariant x = Lshift (y, z) over three long scalars.
static class	FunctionBinary.LshiftLong_xzy Represents the invariant x = Lshift (z, y) over three long scalars.
static class	FunctionBinary.LshiftLong_yxz Represents the invariant y = Lshift (x, z) over three long scalars.
static class	FunctionBinary.LshiftLong_yzx Represents the invariant y = Lshift (z, x) over three long scalars.
static class	FunctionBinary.LshiftLong_zxy Represents the invariant z = Lshift (x, y) over three long scalars.
static class	FunctionBinary.LshiftLong_zyx Represents the invariant z = Lshift (y, x) over three long scalars.
static class	FunctionBinary.MaximumLong_xyz Represents the invariant x = Maximum (y, z) over three long scalars.
static class	FunctionBinary.MaximumLong_yxz Represents the invariant y = Maximum (x, z) over three long scalars.
static class	FunctionBinary.MaximumLong_zxy Represents the invariant z = Maximum (x, y) over three long scalars.
static class	FunctionBinary.MinimumLong_xyz Represents the invariant x = Minimum (y, z) over three long scalars.
static class	FunctionBinary.MinimumLong_yxz Represents the invariant y = Minimum (x, z) over three long scalars.
static class	FunctionBinary.MinimumLong_zxy Represents the invariant z = Minimum (x, y) over three long scalars.
static class	FunctionBinary.ModLong_xyz Represents the invariant x = Mod (y, z) over three long scalars.
static class	FunctionBinary.ModLong_xzy Represents the invariant x = Mod (z, y) over three long scalars.
static class	FunctionBinary.ModLong_yxz Represents the invariant y = Mod (x, z) over three long scalars.
static class	FunctionBinary.ModLong_yzx Represents the invariant y = Mod (z, x) over three long scalars.
static class	FunctionBinary.ModLong_zxy Represents the invariant z = Mod (x, y) over three long scalars.
static class	FunctionBinary.ModLong_zyx Represents the invariant z = Mod (y, x) over three long scalars.
static class	FunctionBinary.MultiplyLong_xyz Represents the invariant x = Multiply (y, z) over three long scalars.
static class	FunctionBinary.MultiplyLong_yxz Represents the invariant y = Multiply (x, z) over three long scalars.
static class	FunctionBinary.MultiplyLong_zxy Represents the invariant z = Multiply (x, y) over three long scalars.
static class	FunctionBinary.PowerLong_xyz Represents the invariant x = Power (y, z) over three long scalars.
static class	FunctionBinary.PowerLong_xzy Represents the invariant x = Power (z, y) over three long scalars.
static class	FunctionBinary.PowerLong_yxz Represents the invariant y = Power (x, z) over three long scalars.
static class	FunctionBinary.PowerLong_yzx Represents the invariant y = Power (z, x) over three long scalars.
static class	FunctionBinary.PowerLong_zxy Represents the invariant z = Power (x, y) over three long scalars.
static class	FunctionBinary.PowerLong_zyx Represents the invariant z = Power (y, x) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_xyz Represents the invariant x = RshiftSigned (y, z) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_xzy Represents the invariant x = RshiftSigned (z, y) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_yxz Represents the invariant y = RshiftSigned (x, z) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_yzx Represents the invariant y = RshiftSigned (z, x) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_zxy Represents the invariant z = RshiftSigned (x, y) over three long scalars.
static class	FunctionBinary.RshiftSignedLong_zyx Represents the invariant z = RshiftSigned (y, x) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_xyz Represents the invariant x = RshiftUnsigned (y, z) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_xzy Represents the invariant x = RshiftUnsigned (z, y) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_yxz Represents the invariant y = RshiftUnsigned (x, z) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_yzx Represents the invariant y = RshiftUnsigned (z, x) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_zxy Represents the invariant z = RshiftUnsigned (x, y) over three long scalars.
static class	FunctionBinary.RshiftUnsignedLong_zyx Represents the invariant z = RshiftUnsigned (y, x) over three long scalars.

Nested classes/interfaces inherited from class Invariant

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

Field Summary

static Logger	debug
static boolean	dkconfig_enabled Boolean.

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	FunctionBinary()
protected	FunctionBinary(PptSlice ppt)

Method Summary

InvariantStatus	add_ordered(long result, long arg1, long arg2, int count) Apply the specified sample to the function, returning the result The caller is responsible for permuting the arguments.
VarInfo	argVar1() Permuted arg1 var.
VarInfo	argVar2() Permuted arg2 var.
InvariantStatus	check_ordered(long result, long arg1, long arg2, int count) Apply the specified sample to the function, returning the result The caller is responsible for permuting the arguments.
double	computeConfidence() This method computes the confidence that this invariant occurred by chance.
boolean	enabled() returns whether or not this invariant is enabled
String	format_simplify()
String	format_using(OutputFormat format)
static List<Invariant>	get_proto_all() Returns a list of all of the FunctionBinary prototype invariants
boolean	instantiate_ok(VarInfo[] vis) FunctionBinary is only valid on isIntegral() types
boolean	isBitwiseAnd()
boolean	isBitwiseOr()
boolean	isBitwiseXor()
boolean	isDivision()
boolean	isGcd()
boolean	isLogicalAnd()
boolean	isLogicalOr()
boolean	isLogicalXor()
boolean	isLshift()
boolean	isMaximum()
boolean	isMinimum()
boolean	isMod()
boolean	isMultiply()
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	isPower()
boolean	isRshiftSigned()
boolean	isRshiftUnsigned()
boolean	isSameFormula(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.
VarInfo	resultVar() Permuted result var.
protected Invariant	resurrect_done(int[] permutation) Reorganize our already-seen state as if the variables had shifted order underneath us (re-arrangement given by the permutation).

Methods inherited from class ThreeScalar

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

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, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate_dyn, instantiate, is_false, is_ni_suppressed, isActive, isAllPrestate, isExact, isExclusiveFormula, 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, 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

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 if FunctionBinary invariants should be considered.

debug

public static Logger debug

Constructor Detail

FunctionBinary

protected FunctionBinary(PptSlice ppt)

FunctionBinary

protected FunctionBinary()

Method Detail

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)

FunctionBinary is only valid on isIntegral() types

Overrides:

instantiate_ok in class Invariant

See Also:

Invariant.valid_types(VarInfo[])

get_proto_all

public static List<Invariant> get_proto_all()

Returns a list of all of the FunctionBinary prototype invariants

resultVar

public VarInfo resultVar()

Permuted result var.

argVar1

public VarInfo argVar1()

Permuted arg1 var.

argVar2

public VarInfo argVar2()

Permuted arg2 var.

check_ordered

public InvariantStatus check_ordered(long result,
                                     long arg1,
                                     long arg2,
                                     int count)

Apply the specified sample to the function, returning the result The caller is responsible for permuting the arguments.

add_ordered

public InvariantStatus add_ordered(long result,
                                   long arg1,
                                   long arg2,
                                   int count)

Apply the specified sample to the function, returning the result The caller is responsible for permuting the arguments.

resurrect_done

protected Invariant resurrect_done(int[] permutation)

Reorganize our already-seen state as if the variables had shifted order underneath us (re-arrangement given by the permutation). We accomplish this by returning the class that corresponds to the the new permutation.

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

format_simplify

public String format_simplify()

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.

computeConfidence

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

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

isMultiply

public boolean isMultiply()

isMinimum

public boolean isMinimum()

isMaximum

public boolean isMaximum()

isDivision

public boolean isDivision()

isPower

public boolean isPower()

isBitwiseAnd

public boolean isBitwiseAnd()

isLogicalAnd

public boolean isLogicalAnd()

isBitwiseXor

public boolean isBitwiseXor()

isLogicalXor

public boolean isLogicalXor()

isBitwiseOr

public boolean isBitwiseOr()

isLogicalOr

public boolean isLogicalOr()

isGcd

public boolean isGcd()

isMod

public boolean isMod()

isLshift

public boolean isLshift()

isRshiftSigned

public boolean isRshiftSigned()

isRshiftUnsigned

public boolean isRshiftUnsigned()