Package daikon.inv.ternary.threeScalar
Class FunctionBinary.ModLong_xyz
- Object
-
- Invariant
-
- TernaryInvariant
-
- ThreeScalar
-
- FunctionBinary
-
- ModLong_xyz
-
- All Implemented Interfaces:
Serializable
,Cloneable
- Enclosing class:
- FunctionBinary
public static class FunctionBinary.ModLong_xyz extends FunctionBinary
Represents the invariantx = Mod(y, z)
over three long scalars.- See Also:
- Serialized Form
-
-
Nested Class Summary
-
Nested classes/interfaces inherited from class FunctionBinary
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
-
Nested classes/interfaces inherited from class Invariant
Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match
-
-
Field Summary
-
Fields inherited from class FunctionBinary
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 ModLong_xyz()
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description InvariantStatus
add_modified(long x, long y, long z, int count)
Similar toThreeScalar.check_modified(long, long, long, int)
except that it can change the state of the invariant if necessary.InvariantStatus
check_modified(long x, long y, long z, int count)
Presents a sample to the invariant.long
func(long y, long 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 FunctionBinary.ModLong_xyz
get_proto()
Returns the prototype invariant for ModLong_xyzint
get_var_order()
protected FunctionBinary.ModLong_xyz
instantiate_dyn(PptSlice slice)
instantiate an invariant on the specified sliceboolean
is_symmetric()
boolean
isMod()
void
set_function_id(int function_id)
-
Methods inherited from class FunctionBinary
add_ordered, argVar1, argVar2, check_ordered, computeConfidence, enabled, format_csharp_contract, format_simplify, format_using, get_proto_all, instantiate_ok, isBitwiseAnd, isBitwiseOr, isBitwiseXor, isDivision, isGcd, isLogicalAnd, isLogicalOr, isLogicalXor, isLshift, isMaximum, isMinimum, isMultiply, isObviousDynamically, isPower, isRshiftSigned, isRshiftUnsigned, isSameFormula, repr, resultVar, resurrect_done
-
Methods inherited from class ThreeScalar
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
-
ModLong_xyz
public ModLong_xyz()
-
-
Method Detail
-
get_proto
public static FunctionBinary.ModLong_xyz get_proto()
Returns the prototype invariant for ModLong_xyz
-
instantiate_dyn
protected FunctionBinary.ModLong_xyz instantiate_dyn( FunctionBinary.ModLong_xyz 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 FunctionBinary.ModLong_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 FunctionBinary.ModLong_xyz this)
-
is_symmetric
@Pure public boolean is_symmetric()
-
func
public long func(long y, long z)
-
check_modified
public InvariantStatus check_modified(long x, long y, long z, int count)
Description copied from class:ThreeScalar
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 classThreeScalar
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(long x, long y, long z, int count)
Description copied from class:ThreeScalar
Similar toThreeScalar.check_modified(long, long, long, 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 callThreeScalar.check_modified(long, long, long, int)
. This method need not check for falsification; that is done by the caller.- Specified by:
add_modified
in classThreeScalar
-
isMod
@Pure public boolean isMod()
- Overrides:
isMod
in classFunctionBinary
-
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
-
-