Object
- Invariant
- - TernaryInvariant
  - - ThreeFloat
    - - FunctionBinaryFloat

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

FunctionBinaryFloat.DivisionDouble_xyz, FunctionBinaryFloat.DivisionDouble_xzy, FunctionBinaryFloat.DivisionDouble_yxz, FunctionBinaryFloat.DivisionDouble_yzx, FunctionBinaryFloat.DivisionDouble_zxy, FunctionBinaryFloat.DivisionDouble_zyx, FunctionBinaryFloat.MaximumDouble_xyz, FunctionBinaryFloat.MaximumDouble_yxz, FunctionBinaryFloat.MaximumDouble_zxy, FunctionBinaryFloat.MinimumDouble_xyz, FunctionBinaryFloat.MinimumDouble_yxz, FunctionBinaryFloat.MinimumDouble_zxy, FunctionBinaryFloat.MultiplyDouble_xyz, FunctionBinaryFloat.MultiplyDouble_yxz, FunctionBinaryFloat.MultiplyDouble_zxy, FunctionBinaryFloat.PowerDouble_xyz, FunctionBinaryFloat.PowerDouble_xzy, FunctionBinaryFloat.PowerDouble_yxz, FunctionBinaryFloat.PowerDouble_yzx, FunctionBinaryFloat.PowerDouble_zxy, FunctionBinaryFloat.PowerDouble_zyx
```
public abstract class FunctionBinaryFloat
extends ThreeFloat
```
Base class for each of the FunctionBinaryFloat 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`	`FunctionBinaryFloat.DivisionDouble_xyz`	Represents the invariant `x = Division(y, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.DivisionDouble_xzy`	Represents the invariant `x = Division(z, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.DivisionDouble_yxz`	Represents the invariant `y = Division(x, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.DivisionDouble_yzx`	Represents the invariant `y = Division(z, x)` over three double scalars.
`static class`	`FunctionBinaryFloat.DivisionDouble_zxy`	Represents the invariant `z = Division(x, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.DivisionDouble_zyx`	Represents the invariant `z = Division(y, x)` over three double scalars.
`static class`	`FunctionBinaryFloat.MaximumDouble_xyz`	Represents the invariant `x = Maximum(y, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MaximumDouble_yxz`	Represents the invariant `y = Maximum(x, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MaximumDouble_zxy`	Represents the invariant `z = Maximum(x, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.MinimumDouble_xyz`	Represents the invariant `x = Minimum(y, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MinimumDouble_yxz`	Represents the invariant `y = Minimum(x, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MinimumDouble_zxy`	Represents the invariant `z = Minimum(x, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.MultiplyDouble_xyz`	Represents the invariant `x = Multiply(y, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MultiplyDouble_yxz`	Represents the invariant `y = Multiply(x, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.MultiplyDouble_zxy`	Represents the invariant `z = Multiply(x, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_xyz`	Represents the invariant `x = Power(y, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_xzy`	Represents the invariant `x = Power(z, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_yxz`	Represents the invariant `y = Power(x, z)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_yzx`	Represents the invariant `y = Power(z, x)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_zxy`	Represents the invariant `z = Power(x, y)` over three double scalars.
`static class`	`FunctionBinaryFloat.PowerDouble_zyx`	Represents the invariant `z = Power(y, x)` over three double 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 FunctionBinaryFloat()

protected FunctionBinaryFloat(PptSlice ppt)

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add_ordered(double result, double arg1, double 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(double result, double arg1, double 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 FunctionBinaryFloat prototype invariants.
`boolean`	`instantiate_ok(VarInfo[] vis)`	FunctionBinaryFloat is only valid on isFloat() types.
`boolean`	`isDivision()`
`boolean`	`isMaximum()`
`boolean`	`isMinimum()`
`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`	`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 ThreeFloat
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 FunctionBinaryFloat invariants should be considered.
  - debug
```
public static Logger debug
```
- Constructor Detail
  - FunctionBinaryFloat
```
protected FunctionBinaryFloat(PptSlice ppt)
```
  - FunctionBinaryFloat
```
protected FunctionBinaryFloat()
```
- 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)
```
    FunctionBinaryFloat is only valid on isFloat() 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 FunctionBinaryFloat 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(double result,
                                     double arg1,
                                     double 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(double result,
                                   double arg1,
                                   double 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 FunctionBinaryFloat 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 FunctionBinaryFloat 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 FunctionBinaryFloat this)
```
  - format_csharp_contract
```
public String format_csharp_contract(@GuardSatisfied FunctionBinaryFloat 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()
```

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

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

Class FunctionBinaryFloat

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 ThreeFloat

Methods inherited from class Invariant

Methods inherited from class Object

Field Detail

dkconfig_enabled

debug

Constructor Detail

FunctionBinaryFloat

FunctionBinaryFloat

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