Package daikon.inv.ternary.threeScalar

Class FunctionBinaryFloat.DivisionDouble_xzy

Object

Invariant

TernaryInvariant

ThreeFloat

FunctionBinaryFloat

DivisionDouble_xzy

All Implemented Interfaces:

Serializable, Cloneable

Enclosing class:

FunctionBinaryFloat

public static class FunctionBinaryFloat.DivisionDouble_xzy
extends FunctionBinaryFloat

Represents the invariant x = Division(z, y) 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
DivisionDouble_xzy()

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 z, double y)
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.DivisionDouble_xzy	get_proto()	Returns the prototype invariant for DivisionDouble_xzy
int	get_var_order()
protected FunctionBinaryFloat.DivisionDouble_xzy	instantiate_dyn(PptSlice slice)	instantiate an invariant on the specified slice
boolean	is_symmetric()
boolean	isDivision()
boolean	isExact()	Subclasses should override.
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, isMaximum, 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, 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

DivisionDouble_xzy

public DivisionDouble_xzy()

Method Detail

get_proto

public static FunctionBinaryFloat.DivisionDouble_xzy get_proto()

Returns the prototype invariant for DivisionDouble_xzy

instantiate_dyn

protected FunctionBinaryFloat.DivisionDouble_xzy instantiate_dyn( FunctionBinaryFloat.DivisionDouble_xzy 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.DivisionDouble_xzy 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.DivisionDouble_xzy this)

is_symmetric

@Pure
public boolean is_symmetric()

func

public double func(double z,
                   double y)

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

isDivision

@Pure
public boolean isDivision()

Overrides:

isDivision in class FunctionBinaryFloat

isExact

@Pure
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

Returns:

true if any variable value can be computed from all the others

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