Package daikon.inv.ternary.threeScalar
Class LinearTernaryCore
- Object
-
- LinearTernaryCore
-
- All Implemented Interfaces:
Serializable
,Cloneable
public final class LinearTernaryCore extends Object implements Serializable, Cloneable
The LinearTernaryCore class is acts as the backend for the invariant (ax + by + cz + d = 0) by processing samples and computing coefficients. The resulting coefficients a, b, c, and d are mutually relatively prime, and the coefficient a is always p.- See Also:
- Serialized Form
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description static class
LinearTernaryCore.Flag
static class
LinearTernaryCore.Point
-
Field Summary
Fields Modifier and Type Field Description double
a
double
b
double
c
double[]
coefficients
double
d
@Nullable LinearTernaryCore.Point[]
def_points
LinearTernaryCore.Flag
line_flag
double
max_a
double
max_b
double
max_c
double
max_d
double
min_a
double
min_b
double
min_c
double
min_d
double
separation
int
values_seen
Invariant
wrapper
-
Constructor Summary
Constructors Constructor Description LinearTernaryCore(Invariant wrapper)
-
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)
Looks for points that define a plane (ax + by + cz + d = 0).String
cache_repr()
double[]
calc_tri_linear(@Nullable LinearTernaryCore.Point[] points)
Calculates the coefficients (a, b, c) and constant (d) for the equation ax + by + cz + d = 0 using the first three points in points.LinearTernaryCore
clone()
double
computeConfidence()
boolean
enoughSamples()
static String
format_simplify(String vix, String viy, String viz, double da, double db, double dc, double dd)
String
format_using(OutputFormat format, String vix, String viy, String viz)
String
format_using(OutputFormat format, String vix, String viy, String viz, double a, double b, double c, double d)
boolean
isActive()
Returns whether or not the invariant is currently active.boolean
isExclusiveFormula(LinearTernaryCore other)
boolean
isSameFormula(LinearTernaryCore other)
@Nullable LinearTernaryCore
merge(List<LinearTernaryCore> cores, Invariant wrapper)
Merge the linear ternary cores in cores to form a new core.boolean
mergeFormulasOk()
In general, we can't merge formulas, but we can merge invariants with too few samples to have formed a plane with invariants with enough samples.void
permute(int[] permutation)
Reorganize our already-seen state as if the variables had shifted order underneath us (rearrangement given by the permutation).String
point_repr(LinearTernaryCore.Point p)
String
repr()
InvariantStatus
setup(LinearBinary lb, VarInfo con_var, long con_val)
Sets up the invariant from a LinearBinary invariant and a constant value for the third variable.InvariantStatus
setup(OneOfScalar oo, VarInfo v1, long con1, VarInfo v2, long con2)
Sets up the invariant from a OneOf and two constants.boolean
try_new_equation(long x, long y, long z)
Calculates new coefficients that for the new point.
-
-
-
Field Detail
-
a
public double a
-
b
public double b
-
c
public double c
-
d
public double d
-
min_a
public double min_a
-
max_a
public double max_a
-
min_b
public double min_b
-
max_b
public double max_b
-
min_c
public double min_c
-
max_c
public double max_c
-
min_d
public double min_d
-
max_d
public double max_d
-
separation
public double separation
-
coefficients
public double[] coefficients
-
line_flag
public LinearTernaryCore.Flag line_flag
-
def_points
public @Nullable LinearTernaryCore.Point[] def_points
-
values_seen
public int values_seen
-
-
Constructor Detail
-
LinearTernaryCore
public LinearTernaryCore(Invariant wrapper)
-
-
Method Detail
-
clone
@SideEffectFree public LinearTernaryCore clone(@GuardSatisfied LinearTernaryCore this)
-
permute
public void permute(int[] permutation)
Reorganize our already-seen state as if the variables had shifted order underneath us (rearrangement given by the permutation).
-
isActive
@Pure public boolean isActive(@GuardSatisfied LinearTernaryCore this)
Returns whether or not the invariant is currently active. We become active after MINTRIPLES values have been seen and a line is not calculated. In addition, the coefficients (a, b, c) must all be non-zero, else the invariant would be described by a LinearBinary or constant invariant. Before that, a, b, and c are uninitialized.
-
setup
public InvariantStatus setup(LinearBinary lb, VarInfo con_var, long con_val)
Sets up the invariant from a LinearBinary invariant and a constant value for the third variable. Points are taken from the LinearBinary cache and its min_x/y and max_x/y points and combined with the constant value.- Returns:
- InvariantStatus.NO_CHANGE if the invariant is valid, InvariantStatus.FALSIFIED if one of the points invalidated the LinearTernary invariant
-
setup
public InvariantStatus setup(OneOfScalar oo, VarInfo v1, long con1, VarInfo v2, long con2)
Sets up the invariant from a OneOf and two constants. Points are taken from the OneOf cache and the constant values.- Returns:
- InvariantStatus.NO_CHANGE if the invariant is valid, or InvariantStatus.FALSIFIED if one of the points invalidated the LinearTernary invariant
-
add_modified
public InvariantStatus add_modified(long x, long y, long z, int count)
Looks for points that define a plane (ax + by + cz + d = 0). Collects MINTRIPLE points before attempting to define a line through the points. Once the equation for the line is found, each subsequent point is compared to it. If the point does not match, recalculates the maximally separated points and attempts to fit the points to the new line. If the points do not fit the line, attempts to define the plane (to hopefully get at least some spread between the points, so that small errors don't get magnified). Once the equation for the plane is found, each subsequent point is compared to it. If the point does not match the point is examined to see if it would is maximally separated when compared to the points originally used to define the plane. If it is, it is used to recalcalulate the coefficients (a, b, c). If those coefficients are relatively close to the original coefficients (within the ratio defined by Global.fuzzy) then the new coefficients are used.- See Also:
FuzzyFloat
-
try_new_equation
public boolean try_new_equation(long x, long y, long z)
Calculates new coefficients that for the new point. Uses the new coefficients if they are relatively close to to the previous ones. Kills off the invariant if they are not.- Returns:
- true if the new equation worked, false otherwise
-
calc_tri_linear
public double[] calc_tri_linear(@Nullable LinearTernaryCore.Point[] points)
Calculates the coefficients (a, b, c) and constant (d) for the equation ax + by + cz + d = 0 using the first three points in points.- Parameters:
points
- array of points to use to calculate the coefficents. Only the first three points (all of which must be non-null) are used.- Returns:
- a four element array where a is the first element, b the second, c the third, and d is the fourth. All elements are mutually prime, integers and a is positive.
-
enoughSamples
public boolean enoughSamples(@GuardSatisfied LinearTernaryCore this)
-
computeConfidence
public double computeConfidence()
-
point_repr
public String point_repr(LinearTernaryCore.Point p)
-
cache_repr
public String cache_repr()
-
format_using
@SideEffectFree public String format_using(OutputFormat format, String vix, String viy, String viz, double a, double b, double c, double d)
-
format_simplify
public static String format_simplify(String vix, String viy, String viz, double da, double db, double dc, double dd)
-
format_using
@SideEffectFree public String format_using(OutputFormat format, String vix, String viy, String viz)
-
isSameFormula
@Pure public boolean isSameFormula(LinearTernaryCore other)
-
isExclusiveFormula
@Pure public boolean isExclusiveFormula(LinearTernaryCore other)
-
mergeFormulasOk
public boolean mergeFormulasOk()
In general, we can't merge formulas, but we can merge invariants with too few samples to have formed a plane with invariants with enough samples. And those will appear to have different formulas.
-
merge
public @Nullable LinearTernaryCore merge(List<LinearTernaryCore> cores, Invariant wrapper)
Merge the linear ternary cores in cores to form a new core. Any core in the list that has seen enough points to define a plane, must define the same plane. Any cores that have not yet seen enough points, will have each of their points applied to that invariant. The merged core is returned. Null is returned if the cores don't describe the same plane- Parameters:
cores
- list of LinearTernary cores to merge. They should all be permuted to match the variable order in ppt.
-
-