Package daikon.inv.ternary.threeScalar

Class FunctionBinaryFloat.MaximumDouble_xyz

Object

Invariant

TernaryInvariant

ThreeFloat

FunctionBinaryFloat

MaximumDouble_xyz

All Implemented Interfaces:

Serializable, Cloneable

Enclosing class:

FunctionBinaryFloat

public static class FunctionBinaryFloat.MaximumDouble_xyz
extends FunctionBinaryFloat

Represents the invariant x = Maximum(y, z) over three double scalars.

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class FunctionBinaryFloat

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

Nested classes/interfaces inherited from class Invariant

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

Field Summary

Fields inherited from class FunctionBinaryFloat

debug, dkconfig_enabled

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

Constructor	Description
MaximumDouble_xyz()

Method Summary

Modifier and Type	Method	Description
InvariantStatus	add_modified(double x, double y, double z, int count)	Similar to ThreeFloat.check_modified(double, double, double, int) except that it can change the state of the invariant if necessary.
InvariantStatus	check_modified(double x, double y, double z, int count)	Presents a sample to the invariant.
double	func(double y, double z)
int	get_function_id()
String[]	get_method_name()
@Nullable NISuppressionSet	get_ni_suppressions()	Returns a list of non-instantiating suppressions for this invariant.
static FunctionBinaryFloat.MaximumDouble_xyz	get_proto()	Returns the prototype invariant for MaximumDouble_xyz
int	get_var_order()
protected FunctionBinaryFloat.MaximumDouble_xyz	instantiate_dyn(PptSlice slice)	instantiate an invariant on the specified slice
boolean	is_symmetric()
boolean	isMaximum()
void	set_function_id(int function_id)

Methods inherited from class FunctionBinaryFloat

add_ordered, argVar1, argVar2, check_ordered, computeConfidence, enabled, format_csharp_contract, format_simplify, format_using, get_proto_all, instantiate_ok, isDivision, isMinimum, isMultiply, isObviousDynamically, isPower, isSameFormula, repr, resultVar, resurrect_done

Methods inherited from class ThreeFloat

add, add_unmodified, check, 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, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, 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

Constructor Detail

MaximumDouble_xyz

public MaximumDouble_xyz()

Method Detail

get_proto

public static FunctionBinaryFloat.MaximumDouble_xyz get_proto()

Returns the prototype invariant for MaximumDouble_xyz

instantiate_dyn

protected FunctionBinaryFloat.MaximumDouble_xyz instantiate_dyn( FunctionBinaryFloat.MaximumDouble_xyz this,
                                                                PptSlice slice)

instantiate an invariant on the specified slice

Specified by:

instantiate_dyn in class Invariant

Returns:

the new invariant

get_method_name

public String[] get_method_name(@GuardSatisfied FunctionBinaryFloat.MaximumDouble_xyz this)

get_function_id

public int get_function_id()

set_function_id

public void set_function_id(int function_id)

get_var_order

public int get_var_order(@GuardSatisfied FunctionBinaryFloat.MaximumDouble_xyz this)

is_symmetric

@Pure
public boolean is_symmetric()

func

public double func(double y,
                   double z)

check_modified

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

Description copied from class: ThreeFloat

Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.

Specified by:

check_modified in class ThreeFloat

count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.

Returns:

whether or not the sample is consistent with the invariant

add_modified

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

Description copied from class: ThreeFloat

Similar to ThreeFloat.check_modified(double, double, double, int) except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply call ThreeFloat.check_modified(double, double, double, int). This method need not check for falsification; that is done by the caller.

Specified by:

add_modified in class ThreeFloat

isMaximum

@Pure
public boolean isMaximum()

Overrides:

isMaximum in class FunctionBinaryFloat

get_ni_suppressions

@Pure
public @Nullable NISuppressionSet get_ni_suppressions()

Returns a list of non-instantiating suppressions for this invariant.

Overrides:

get_ni_suppressions in class Invariant

Returns:

the set of non-instantiating suppressions for this invariant