Package daikon.inv.ternary.threeScalar
Class FunctionBinaryFloat.MinimumDouble_yxz
- Object
-
- Invariant
-
- TernaryInvariant
-
- ThreeFloat
-
- FunctionBinaryFloat
-
- MinimumDouble_yxz
-
- All Implemented Interfaces:
Serializable
,Cloneable
- Enclosing class:
- FunctionBinaryFloat
public static class FunctionBinaryFloat.MinimumDouble_yxz extends FunctionBinaryFloat
Represents the invarianty = Minimum(x, 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 MinimumDouble_yxz()
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(double x, double y, double z, int count)
Similar toThreeFloat.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 x, 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.MinimumDouble_yxz
get_proto()
Returns the prototype invariant for MinimumDouble_yxzint
get_var_order()
protected FunctionBinaryFloat.MinimumDouble_yxz
instantiate_dyn(PptSlice slice)
instantiate an invariant on the specified sliceboolean
is_symmetric()
boolean
isMinimum()
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, isMaximum, 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
-
-
-
-
Constructor Detail
-
MinimumDouble_yxz
public MinimumDouble_yxz()
-
-
Method Detail
-
get_proto
public static FunctionBinaryFloat.MinimumDouble_yxz get_proto()
Returns the prototype invariant for MinimumDouble_yxz
-
instantiate_dyn
protected FunctionBinaryFloat.MinimumDouble_yxz instantiate_dyn( FunctionBinaryFloat.MinimumDouble_yxz this, PptSlice slice)
instantiate an invariant on the specified slice- Specified by:
instantiate_dyn
in classInvariant
- Returns:
- the new invariant
-
get_method_name
public String[] get_method_name(@GuardSatisfied FunctionBinaryFloat.MinimumDouble_yxz 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.MinimumDouble_yxz this)
-
is_symmetric
@Pure public boolean is_symmetric()
-
func
public double func(double x, 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 classThreeFloat
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 toThreeFloat.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 callThreeFloat.check_modified(double, double, double, int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classThreeFloat
-
isMinimum
@Pure public boolean isMinimum()
- Overrides:
isMinimum
in classFunctionBinaryFloat
-
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 classInvariant
- Returns:
- the set of non-instantiating suppressions for this invariant
-
-