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

Nested Classes
Modifier and Type	Class	Description
`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

Fields
Modifier and Type Field Description

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

Constructor Summary

Constructors
Modifier Constructor Description

protected FunctionBinary()

protected FunctionBinary(PptSlice ppt)

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_ordered(long result, long arg1, long arg2, int count)`	Apply the specified sample to the function, returning the result.
`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.
`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_csharp_contract()`
`String`	`format_simplify()`
`String`	`format_using(OutputFormat format)`	Return a printed representation of this invariant, in the given 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()`
`@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.
`boolean`	`isPower()`
`boolean`	`isRshiftSigned()`
`boolean`	`isRshiftUnsigned()`
`boolean`	`isSameFormula(Invariant other)`	Returns true iff the two invariants represent the same mathematical formula.
`String`	`repr()`	For printing invariants, there are two interfaces: repr gives a low-level representation (`Invariant.repr_prob()` also prints the confidence), and `Invariant.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, add_modified, add_unmodified, check, check_modified, check_unmodified, valid_types, var1, var2, var3

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, 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, isExact, 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

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
    
    Specified by:
    
    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 new permutation.
    
    Overrides:
    
    resurrect_done in class TernaryInvariant
    
    Parameters:
    
    permutation - the permutation
    
    Returns:
    
    the permuted invariant
  - repr
```
public String repr(@GuardSatisfied FunctionBinary this)
```
    Description copied from class: Invariant
    
    For printing invariants, there are two interfaces: repr gives a low-level representation (Invariant.repr_prob() also prints the confidence), and Invariant.format() gives a high-level representation for user output.
    
    Overrides:
    
    repr in class Invariant
    
    Returns:
    
    a string representation of this
  - format_using
```
@SideEffectFree
public String format_using(@GuardSatisfied FunctionBinary this,
                           OutputFormat format)
```
    Description copied from class: Invariant
    
    Return a printed representation of this invariant, in the given format.
    
    Specified by:
    
    format_using in class Invariant
  - format_simplify
```
public String format_simplify(@GuardSatisfied FunctionBinary this)
```
  - format_csharp_contract
```
public String format_csharp_contract(@GuardSatisfied FunctionBinary this)
```
  - isSameFormula
```
@Pure
public boolean isSameFormula(Invariant other)
```
    Description copied from 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.
    
    Specified by:
    
    isSameFormula in class Invariant
    
    Parameters:
    
    other - the invariant to compare to this one
    
    Returns:
    
    true iff the two invariants represent the same mathematical formula. Does not consider
  - computeConfidence
```
public double computeConfidence()
```
    Description copied from class: Invariant
    
    This method computes the confidence that this invariant occurred by chance. Clients should call Invariant.getConfidence() instead.
    This method need not check the value of field "falsified", as the caller does that.
    
    Specified by:
    
    computeConfidence in class Invariant
    
    Returns:
    
    confidence of this invariant
    
    See Also:
    
    Invariant.getConfidence()
  - 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 class Invariant
  - isMultiply
```
@Pure
public boolean isMultiply()
```
  - isMinimum
```
@Pure
public boolean isMinimum()
```
  - isMaximum
```
@Pure
public boolean isMaximum()
```
  - isDivision
```
@Pure
public boolean isDivision()
```
  - isPower
```
@Pure
public boolean isPower()
```
  - isBitwiseAnd
```
@Pure
public boolean isBitwiseAnd()
```
  - isLogicalAnd
```
@Pure
public boolean isLogicalAnd()
```
  - isBitwiseXor
```
@Pure
public boolean isBitwiseXor()
```
  - isLogicalXor
```
@Pure
public boolean isLogicalXor()
```
  - isBitwiseOr
```
@Pure
public boolean isBitwiseOr()
```
  - isLogicalOr
```
@Pure
public boolean isLogicalOr()
```
  - isGcd
```
@Pure
public boolean isGcd()
```
  - isMod
```
@Pure
public boolean isMod()
```
  - isLshift
```
@Pure
public boolean isLshift()
```
  - isRshiftSigned
```
@Pure
public boolean isRshiftSigned()
```
  - isRshiftUnsigned
```
@Pure
public boolean isRshiftUnsigned()
```

Modifier and Type	Field	Description
`static Logger`	`debug`
`static boolean`	`dkconfig_enabled`	Boolean.

Modifier	Constructor	Description
`protected`	`FunctionBinary()`
`protected`	`FunctionBinary(PptSlice ppt)`

Class FunctionBinary

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Field Summary

Fields inherited from class Invariant

Constructor Summary

Method Summary

Methods inherited from class ThreeScalar

Methods inherited from class Invariant

Methods inherited from class Object

Field Detail

dkconfig_enabled

debug

Constructor Detail

FunctionBinary

FunctionBinary

Method Detail

enabled

instantiate_ok

get_proto_all

resultVar

argVar1

argVar2

check_ordered

add_ordered

resurrect_done

repr

format_using

format_simplify

format_csharp_contract

isSameFormula

computeConfidence

isObviousDynamically

isMultiply

isMinimum

isMaximum

isDivision

isPower

isBitwiseAnd

isLogicalAnd

isBitwiseXor

isLogicalXor

isBitwiseOr

isLogicalOr

isGcd

isMod

isLshift

isRshiftSigned

isRshiftUnsigned