001// ***** This file is automatically generated from LinearTernaryCore.java.jpp 002 003package daikon.inv.ternary.threeScalar; 004 005import daikon.*; 006import daikon.inv.*; 007import daikon.inv.binary.twoScalar.*; 008import daikon.inv.unary.scalar.*; 009import java.io.Serializable; 010import java.util.*; 011import java.util.logging.Level; 012import java.util.logging.Logger; 013import org.checkerframework.checker.lock.qual.GuardSatisfied; 014import org.checkerframework.checker.nullness.qual.Nullable; 015import org.checkerframework.dataflow.qual.Pure; 016import org.checkerframework.dataflow.qual.SideEffectFree; 017import org.plumelib.util.ArraysPlume; 018import org.plumelib.util.MathPlume; 019import typequals.prototype.qual.NonPrototype; 020import typequals.prototype.qual.Prototype; 021 022/** 023 * The LinearTernaryCore class is acts as the backend for the invariant (ax + by + cz + d = 0) by 024 * processing samples and computing coefficients. The resulting coefficients a, b, c, and d are 025 * mutually relatively prime, and the coefficient a is always p. 026 */ 027 028// Originally, LinearTernaryCore code was not dealing with degenerate 029// linear ternary invariants correct, namely when the plane 030// (ax+by+cz+d=0) is parallel to one of the axes, so one of the 031// coefficients was 0. In this case, the invariant can be described 032// by a binary invariant (eliminate the 0 coefficient variable). 033// LinearTernaryCore's inability to deal with this degenerate form was 034// (and still is) masked by the suppression of a linear ternary 035// invariant via a binary invariant and a constant (the code threw an 036// exception when seeing this case and falsifies the invariant). As 037// more samples are processed, the ternary invariant may "evolve" from 038// a degenerate form to a full ternary invariant. The 039// linearintervention method deals with the degenerate form and the 040// planarintervention focuses on the full ternary invariant. 041 042@SuppressWarnings({"nullness", // ***** TEMPORARY: def_points is confused (is packed initially with non-nulls at beginning, but is not all non-nulls; and later may not be packed); needs review/refactoring/rewriting 043 "UnnecessaryParentheses" // generated code, parens are sometimes necessary 044 }) 045public final class LinearTernaryCoreFloat implements Serializable, Cloneable { 046 // We are Serializable, so we specify a version to allow changes to 047 // method signatures without breaking serialization. If you add or 048 // remove fields, you should change this number to the current date. 049 static final long serialVersionUID = 20030822L; 050 051 /** Debug tracer. */ 052 static final Logger debug = Logger.getLogger("daikon.inv.ternary.threeScalar.LinearTernaryCoreFloat"); 053 054 // ax + by + cz + d = 0; first argument is x, second is y, third is z 055 // Although the coefficients are guaranteed to be integers, we use doubles to 056 // store the values because regression tests have shown that a long is 057 // not sufficient 058 public double a = 0, b = 0, c = 0, d = 0; 059 public double min_a, max_a, min_b, max_b, min_c, max_c, min_d, max_d; 060 public double separation = 0; 061 062 // coefficients for the invariant in 3D space 063 public double[] coefficients = new double[4]; 064 065 // The values of the flags determine indicate whether a line exists 066 // with the current samples (NO_LINE) and which variables are 067 // constant (constant variables indicate that the 'plane' is 068 // parallel to that axis). For example, XY_CONSTANT means that the 069 // so far, the x and y values have all been constant and only z has 070 // been varying so so the plane is actually a line. 071 // NO_CONSTANT_VARIABLES indicates that the values have not been 072 // constant but do for a plane between variables. 073 public enum Flag {NO_LINE, XY_CONSTANT, XZ_CONSTANT, YZ_CONSTANT, 074 X_CONSTANT, Y_CONSTANT, Z_CONSTANT, NO_CONSTANT_VARIABLES}; 075 076 // The flag indicates whether a line exists in the 3D space instead 077 // of a plane If the flag value is not NO_LINE, then a line does 078 // currently exist among the values seen and the flag specifies 079 // which variables are constant to make the invariant a line rather 080 // than a plane. The value NO_LINE indicates either that not enough 081 // values have been seen to make any decision or that a plane 082 // exists. 083 public Flag line_flag = Flag.NO_LINE; 084 085 // Inner class to store points in for more convenient access. 086 public static class Point implements Serializable, Cloneable { 087 static final long serialVersionUID = 20050923L; 088 089 public double x; 090 public double y; 091 public double z; 092 public Point() { 093 this(0, 0, 0); 094 } 095 public Point(double x, double y, double z) { 096 this.x = x; this.y = y; this.z = z; 097 } 098 @Pure 099 public boolean equals(double x, double y, double z) { 100 return (this.x == x) && (this.y == y) && (this.z == z); 101 } 102 @SideEffectFree 103 @Override 104 protected Point clone(@GuardSatisfied Point this) throws CloneNotSupportedException { 105 return (Point) super.clone(); 106 } 107 @SideEffectFree 108 @Override 109 public String toString(@GuardSatisfied Point this) { 110 return "(" + x + ", " + y + " ," + z + ")"; 111 } 112 } 113 114 // Points that define the plane. The first three are normally the 115 // current definition. The next is a new point for consideration. 116 // However, any slot may be set to null at any time, and points may be 117 // duplicated at any time. 118 // (The invariant appears to be a bit stronger than that, since there are 119 // places that dereference the array unconditionally, assuming that its 120 // elements are non-null. This should be clarified/refactored.) 121 public @Nullable Point[] def_points = new Point[MINTRIPLES]; 122 123 public Invariant wrapper; 124 125 // The number of distinct values (not samples) seen. 126 public int values_seen = 0; 127 128 static final int MINTRIPLES = 5; 129 130 public LinearTernaryCoreFloat(Invariant wrapper) { 131 this.wrapper = wrapper; 132 } 133 134 @SideEffectFree 135 @Override 136 public LinearTernaryCoreFloat clone(@GuardSatisfied LinearTernaryCoreFloat this) { 137 try { 138 LinearTernaryCoreFloat result = (LinearTernaryCoreFloat) super.clone(); 139 result.def_points = new Point[MINTRIPLES]; 140 for (int i = 0; i < MINTRIPLES; i++) { 141 Point p = def_points[i]; 142 if (p != null) { 143 result.def_points[i] = p.clone(); 144 } 145 } 146 return result; 147 } catch (CloneNotSupportedException e) { 148 throw new Error(); // can't happen 149 } 150 } 151 152 /** 153 * Reorganize our already-seen state as if the variables had shifted order underneath us 154 * (rearrangement given by the permutation). 155 */ 156 public void permute(int[] permutation) { 157 assert permutation.length == 3; 158 assert ArraysPlume.fnIsPermutation(permutation); 159 // Fix a, b, c 160 double[] clever = new double[] { a, b, c }; 161 double[] pclever = new double[3]; 162 pclever[permutation[0]] = clever[0]; 163 pclever[permutation[1]] = clever[1]; 164 pclever[permutation[2]] = clever[2]; 165 if (isActive()) { 166 // Seen enough values, so permuting a, b, c is useful 167 if ( a == 0 || b == 0 || c == 0) { 168 throw new Error("Active LTs never have 0 coefficients"); 169 // // Can't handle this form once rotated. But if we've seen 170 // // enough values, yet a, b or c is zero, then this is covered by 171 // // a LinearBinary or a constant, so let me just destroy myself. 172 // values_seen = Integer.MAX_VALUE; 173 // a = b = c = d = 0; 174 // if (debug.isLoggable(Level.FINE)) { 175 // debug.fine (" Ternary invariant destroyed because a, b, or c = 0"); 176 // } 177 // return; 178 } else { 179 // double d = -1.0 / pclever[2]; 180 a = pclever[0]; 181 b = pclever[1]; 182 c = pclever[2]; 183 184 // we still need to guarantee a positive x coefficient 185 if (a < 0) { 186 a = -a; 187 b = -b; 188 c = -c; 189 d = -d; 190 } 191 } 192 } 193 194 // Fix caches 195 { 196 double[] temp = new double[3]; 197 for (int i = 0; i < MINTRIPLES; i++) { 198 Point p = def_points[i]; 199 if (p == null) { 200 continue; 201 } 202 wrapper.log("orig def_points[%s] = %s", i, p); 203 temp[permutation[0]] = p.x; 204 temp[permutation[1]] = p.y; 205 temp[permutation[2]] = p.z; 206 p.x = temp[0]; 207 p.y = temp[1]; 208 p.z = temp[2]; 209 wrapper.log("permuted def_points[%s] = %s", i, p); 210 } 211 } 212 // Assert that caches sync with a,b,c? 213 // This would be a good sanity check, but it would be nontrivial 214 // because we don't keep track of when a, b, and c are really 215 // valid for all the of the points we've cached. If we were 216 // falsified and then resurrected, we might have samples that 217 // didn't fit even before the permutation. -smcc 218 } 219 220 /** 221 * Returns whether or not the invariant is currently active. We become active after MINTRIPLES 222 * values have been seen and a line is not calculated. In addition, the coefficients (a, b, c) 223 * must all be non-zero, else the invariant would be described by a LinearBinary or constant 224 * invariant. Before that, a, b, and c are uninitialized. 225 */ 226 // this is the check used throughout the file as a shortcut because 227 // the invariant must have seen enough samples and not be a line for all the 228 // other calculations and comparisons done to be sensible, meaning that 229 // a full linear ternary invariant exists, not a degenerate one 230 @Pure 231 public boolean isActive(@GuardSatisfied LinearTernaryCoreFloat this) { 232 return line_flag == Flag.NO_LINE && values_seen >= MINTRIPLES && a != 0 && b != 0 && c != 0; 233 } 234 235 /** 236 * Sets up the invariant from a LinearBinary invariant and a constant value for the third 237 * variable. Points are taken from the LinearBinary cache and its min_x/y and max_x/y points and 238 * combined with the constant value. 239 * 240 * @return InvariantStatus.NO_CHANGE if the invariant is valid, InvariantStatus.FALSIFIED if one 241 * of the points invalidated the LinearTernary invariant 242 */ 243 public InvariantStatus setup(LinearBinaryFloat lb, VarInfo con_var, 244 double con_val) { 245 246 if (Debug.logOn()) { 247 wrapper.log("setup from lb %s con var %s con_val %s", 248 lb, con_var, con_val); 249 } 250 251 int con_index = con_var.varinfo_index; 252 int lb_v1_index = lb.ppt.var_infos[0].varinfo_index; 253 int lb_v2_index = lb.ppt.var_infos[1].varinfo_index; 254 255 double[] con_vals = new double [lb.core.values_seen + 2]; 256 double[] lb1_vals = new double [lb.core.values_seen + 2]; 257 double[] lb2_vals = new double [lb.core.values_seen + 2]; 258 259 int mi = lb.core.values_seen; 260 for (int i = 0; i < mi; i++) { 261 con_vals[i] = con_val; 262 lb1_vals[i] = lb.core.x_cache[i]; 263 lb2_vals[i] = lb.core.y_cache[i]; 264 } 265 if (lb.isActive()) { 266 con_vals[mi] = con_val; 267 lb1_vals[mi] = lb.core.min_x; 268 lb2_vals[mi] = lb.core.min_y; 269 con_vals[mi + 1] = con_val; 270 lb1_vals[mi + 1] = lb.core.max_x; 271 lb2_vals[mi + 1] = lb.core.max_y; 272 mi += 2; 273 } 274 275 InvariantStatus sts = InvariantStatus.NO_CHANGE; 276 277 for (int i = 0; i < mi; i++ ) { 278 if (con_index < lb_v1_index) { 279 sts = add_modified(con_vals[i], lb1_vals[i], lb2_vals[i], 1); 280 281 } else if (con_index < lb_v2_index) { 282 sts = add_modified(lb1_vals[i], con_vals[i], lb2_vals[i], 1); 283 284 } else { 285 sts = add_modified(lb1_vals[i], lb2_vals[i], con_vals[i], 1); 286 287 } 288 if (sts != InvariantStatus.NO_CHANGE) { 289 break; 290 } 291 } 292 293 if (sts != InvariantStatus.NO_CHANGE) { 294 System.out.println("lb.core.values_seen=" + lb.core.values_seen); 295 for (int i = 0; i < mi; i++ ) { 296 System.out.printf("LTCore: vals %s %s %s%n", con_vals[i], lb1_vals[i], 297 lb2_vals[i]); 298 } 299 System.out.println("in inv " + wrapper.format() + " " + wrapper.ppt); 300 assert sts == InvariantStatus.NO_CHANGE; 301 } 302 303 return sts; 304 } 305 306 /** 307 * Sets up the invariant from a OneOf and two constants. Points are taken from the OneOf cache 308 * and the constant values. 309 * 310 * @return InvariantStatus.NO_CHANGE if the invariant is valid, or InvariantStatus.FALSIFIED if 311 * one of the points invalidated the LinearTernary invariant 312 */ 313 314 public InvariantStatus setup(OneOfFloat oo, VarInfo v1, double con1, 315 VarInfo v2, double con2) { 316 317 int oo_index = oo.ppt.var_infos[0].varinfo_index; 318 int con1_index = v1.varinfo_index; 319 int con2_index = v2.varinfo_index; 320 321 InvariantStatus sts = InvariantStatus.NO_CHANGE; 322 for (int i = 0; i < oo.num_elts(); i++ ) { 323 if (oo_index < con1_index) { 324 sts = add_modified(((Double)oo.elt(i)).doubleValue(), con1, con2, 1); 325 } else if (oo_index < con2_index) { 326 sts = add_modified(con1, ((Double)oo.elt(i)).doubleValue(), con2, 1); 327 } else { 328 sts = add_modified(con1, con2, ((Double)oo.elt(i)).doubleValue(), 1); 329 } 330 if (sts != InvariantStatus.NO_CHANGE) { 331 break; 332 } 333 } 334 335 if (Debug.logOn()) { 336 wrapper.log("setup from OneOf %s v1=%s v2=%s status = %s", 337 oo, con1, con2, sts); 338 } 339 340 return sts; 341 } 342 343 /** 344 * Looks for points that define a plane (ax + by + cz + d = 0). Collects MINTRIPLE points before 345 * attempting to define a line through the points. Once the equation for the line is found, each 346 * subsequent point is compared to it. If the point does not match, recalculates the maximally 347 * separated points and attempts to fit the points to the new line. If the points do not fit the 348 * line, attempts to define the plane (to hopefully get at least some spread between the points, 349 * so that small errors don't get magnified). Once the equation for the plane is found, each 350 * subsequent point is compared to it. If the point does not match the point is examined to see if 351 * it would is maximally separated when compared to the points originally used to define the 352 * plane. If it is, it is used to recalcalulate the coefficients (a, b, c). If those 353 * coefficients are relatively close to the original coefficients (within the ratio defined by 354 * Global.fuzzy) then the new coefficients are used. 355 * 356 * @see org.plumelib.util.FuzzyFloat 357 */ 358 public InvariantStatus add_modified(double x, double y, double z, int count) { 359 360 if (Debug.logDetail()) { 361 wrapper.log("Adding point, x=%s y=%s z=%s to invariant", x, y, z); 362 } 363 364 if (values_seen < MINTRIPLES) { 365 // We delay computation of a and b until we have seen several triples 366 // so that we can compute a and b based on a far-separated triple. If 367 // the points in a triple are nearby, then roundoff errors in the 368 // computation of the slope can be non-negligible. 369 370 // skip points we've already seen 371 for (int i = 0; i < values_seen; i++) { 372 if (def_points[i].equals(x, y, z)) { 373 return InvariantStatus.NO_CHANGE; 374 } 375 } 376 377 def_points[values_seen] = new Point(x, y, z); 378 wrapper.log("Add: (%s, %s, %s)", x, y, z); 379 values_seen++; 380 wrapper.log("Values seen: %s", values_seen); 381 382 // check to see if we've seen enough values to create the equation 383 if (values_seen == MINTRIPLES) { 384 385 // Try to fit the points to a line first. 386 // The points may form a degenerate linear ternary invariants 387 // especially if one of the variable is constant 388 linearIntervention(def_points); 389 390 // if line can not be formed, try to form a plane 391 if (line_flag == Flag.NO_LINE) { 392 InvariantStatus stat = planarIntervention(def_points); 393 return stat; 394 } else { 395 396 // points fit in a line 397 return InvariantStatus.NO_CHANGE; 398 } 399 } else { 400 401 // still haven't seen enough values 402 return InvariantStatus.NO_CHANGE; 403 } 404 } else { 405 406 // at this point either a line or a plane must have been formed 407 408 // if line already broken, fit to plane equation 409 if (line_flag == Flag.NO_LINE) { 410 // If the new value doesn't fit the equation 411 if (!Global.fuzzy.eq(-d, a * x + b * y + c * z)) { 412 413 // Try to find small changes that will fit better. 414 if (!try_new_equation(x, y, z)) { 415 if (Invariant.logOn() || debug.isLoggable(Level.FINE)) { 416 wrapper.log(debug, "destroying (" + wrapper.format() 417 + ") where x=" + x + " y=" + y + " z=" + z 418 + " a=" + a + " b=" + b + " c=" + c 419 + " values_seen=" + values_seen); 420 } 421 // jiggling the values did not work 422 return InvariantStatus.FALSIFIED; 423 } 424 } else { 425 426 // point fits the current plane equation 427 return InvariantStatus.NO_CHANGE; 428 } 429 } else { 430 431 // try to fit to the current line 432 if (!try_points_linear((x), (y), (z))) { 433 // put the crucial point in, so that it can be tested against the new line 434 def_points[MINTRIPLES - 1] = new Point(x, y, z); 435 436 // try to fit the points onto a line again (not sure if this 437 // is really necessary, maybe the fuzzy equals really does 438 // make a difference) 439 linearIntervention(def_points); 440 } 441 442 // new point has broken the line, try to fit to a plane 443 if (line_flag == Flag.NO_LINE) { 444 InvariantStatus stat = planarIntervention(def_points); 445 return stat; 446 } else { 447 448 // fuzzy equals does make a difference 449 return InvariantStatus.NO_CHANGE; 450 } 451 452 } 453 454 } 455 // should never get here because values_seen is either < or >= MINTRIPLES 456 // return InvariantStatus.NO_CHANGE; 457 throw new Error("at end of add_modified"); 458 } 459 460 /** 461 * Attempts to fit the points in def_point to a plane and calculates the coefficients (a, b, c, d) 462 * if possible. 463 * 464 * @param def_point array of points. Must have at least 3 elements. 465 * 466 * @return the status of the invariant 467 * (whether the plane fitting was successful) 468 */ 469 private InvariantStatus planarIntervention(@Nullable Point[] def_point) { 470 471 // make a copy of the array so that the points don't get clobbered 472 // because we need to check all the points in def_points against the 473 // coefficients calculated 474 475 @Nullable Point[] dummy = new @Nullable Point[def_point.length]; 476 for (int i = 0; i < def_point.length; i++) { 477 dummy[i] = def_point[i]; 478 } 479 480 // Find the three points with the maximum separation 481 maxsep_triples(dummy); 482 // Now, first 3 values of dummy are the maximum-separated 3 points. 483 484 // Null points only show up in the cross-checker, not the regression 485 // tests, as of 5/25/2010. 486 // Sometimes the points are still null. 487 if (dummy[0] == null) { 488 return InvariantStatus.FALSIFIED; 489 } 490 491 // Calculate the coefficients of the equation (a, b, c, d). 492 // Requires that the first 3 elements of dummy must be non-null. 493 double[] coef = calc_tri_linear(dummy); 494 495 a = coef[0]; 496 b = coef[1]; 497 c = coef[2]; 498 d = coef[3]; 499 500 wrapper.log("Calculated tri linear coeff: (%s), b (%s), c(%s), and d(%s)", 501 a, b, c, d); 502 // If one of these coefficients is zero (except for d), this 503 // should be a LinearBinary, not a LinearTernary, term. (It 504 // might not show up as LinearBinary because there might not 505 // have been enough samples; but a random varying third 506 // variable can create enough samples.) Also, throw out the 507 // invariant if any of the coefficients would be not-a-number. 508 if ( a == 0|| b == 0 || c == 0 509 || Double.isNaN(a) || Double.isNaN(b) || Double.isNaN(c)) { 510 511 wrapper.log("problematic coefficient: invariant falsified"); 512 return InvariantStatus.FALSIFIED; 513 } 514 515 // Check all values against a, b, and c. 516 if (!wrapper.is_false()) { 517 for (int i = 0; i < values_seen; i++) { 518 519 // Global.fuzzy.eq works by comparing ratios between numbers, 520 // so comparing the sum of everything to 0 won't work. 521 // wrapper.log("point: " + def_point[i].x + " " 522 // + def_point[i].y + " " + def_point[i].z); 523 // wrapper.log("compare: " + -c * def_point[i].z); 524 // wrapper.log( "to: " + (a*def_point[i].x 525 // + b*def_point[i].y + d)); 526 527 wrapper.log("Trying at index %s: 0 != %s*%s+%s*%s+%s*%s+%s", 528 i, a, def_point[i].x, 529 b, def_point[i].y, 530 c, def_point[i].z, 531 d); 532 533 if (!Global.fuzzy.eq(-d, a * def_point[i].x + b * def_point[i].y + c * def_point[i].z)) { 534 535 if (Debug.logOn() || debug.isLoggable(Level.FINE)) { 536 wrapper.log(debug, "Destroying at index " + i + ": 0 != " 537 + a + "*" + def_point[i].x 538 + "+" + b + "*" + def_point[i].y + "+" + c 539 + "*" + def_point[i].z 540 + "+" + d); 541 } 542 543 return InvariantStatus.FALSIFIED; 544 } 545 } 546 if (Debug.logOn()) { 547 wrapper.log("equation = %s*x %s*y %s*z = %s", a, b, c, -d); 548 } 549 550 // Discard the points not used to define the coefficients. 551 for (int ii = 3; ii < MINTRIPLES; ii++) { 552 def_point[ii] = null; 553 } 554 } 555 556 // if it passes all the checks, then no change to the Invariant 557 return InvariantStatus.NO_CHANGE; 558 } 559 560 /** 561 * Attempts to fit the points in def_point to a line and calculates the corresponding line 562 * classification (line_flag) and coefficients (coefficients[]) if possible. If not (points in 563 * def_point form a plane) resets line_flag to Flag.NO_LINE and coefficients[] elements to -999. 564 * 565 * @param def_point array of points. Must have at least 2 elements. 566 * 567 */ 568 private void linearIntervention(@Nullable Point[] def_point) { 569 570 // find the max separation points 571 Point[] maxsep_doubles = maxsep_doubles(def_point); 572 573 // maxsep_doubles[0] could be null when enough points have a NaN 574 if (maxsep_doubles == null) { 575 // line_flag == Flag.NO_LINE so the invariant 576 // will try to fit a plane to the points and fail 577 return; 578 } else { 579 // find the equation (coefficients now stored in coefficients[]) 580 calc_bi_linear(maxsep_doubles[0], maxsep_doubles[1]); 581 582 // This seems to imply that all elements of def_points are non-null. 583 // Is that true? 584 // check the other points against the coefficients 585 for (int i = 0; i < def_point.length; i++) { 586 // try to fit the current point to the current line 587 boolean ok = try_points_linear((def_point[i].x), (def_point[i].y), (def_point[i].z)); 588 589 if (!ok) { 590 line_flag = Flag.NO_LINE; 591 break; 592 } 593 } 594 } 595 596 } 597 598 /** 599 * Attempts to fit the new point (x,y,z) onto the current line (indicated by line_flag and 600 * coefficients[]). Method should only be called if the current points define a line (line_flag is 601 * not Flag.NO_LINE) 602 * 603 * @param x x component of the point 604 * @param x y component of the point 605 * @param x z component of the point 606 */ 607 private boolean try_points_linear(double x, double y, double z) { 608 609 switch(line_flag) { 610 case XY_CONSTANT: 611 return Global.fuzzy.eq(coefficients[0], x) && Global.fuzzy.eq(coefficients[1], y); 612 613 case XZ_CONSTANT: 614 return Global.fuzzy.eq(coefficients[0], x) && Global.fuzzy.eq(coefficients[1], z); 615 616 case YZ_CONSTANT: 617 return Global.fuzzy.eq(coefficients[0], y) && Global.fuzzy.eq(coefficients[1], z); 618 619 case X_CONSTANT: 620 return Global.fuzzy.eq(coefficients[0], x) && Global.fuzzy.eq(z, coefficients[1] * y + coefficients[2]); 621 622 case Y_CONSTANT: 623 return Global.fuzzy.eq(coefficients[0], y) && Global.fuzzy.eq(z, coefficients[1] * x + coefficients[2]); 624 625 case Z_CONSTANT: 626 return Global.fuzzy.eq(coefficients[0], z) && Global.fuzzy.eq(y, coefficients[1] * x + coefficients[2]); 627 628 case NO_CONSTANT_VARIABLES: 629 return Global.fuzzy.eq(y, coefficients[0] * x + coefficients[1]) && Global.fuzzy.eq(z, coefficients[2] * x + coefficients[3]); 630 631 // error if the code gets here because that means, we are trying to fit the points to a linear 632 // when the points already form a plane 633 default: 634 throw new RuntimeException("try_points_linear called when points already form a plane (line_flag = NO_LINE)"); 635 } 636 } 637 638 /** 639 * Returns the two points that have the maximum separation in pa. 640 * 641 * @param pa array of points. Must have at least 2 elements. Can be any length and can contain 642 * nulls (which will be ignored). 643 * @return a 2-element array containing the most-separated elements. Returns null if no pair of 644 * elements is NaN-free. 645 */ 646 private Point @Nullable [] maxsep_doubles(@Nullable Point[] pa) { 647 648 Point p1 = null; 649 Point p2 = null; 650 651 // max_separation is the separation metric for the most separated 652 // pair of points. We use the sum of the separations as the 653 // metric. 654 double max_separation = Double.MIN_VALUE; 655 656 for (int i = 0; i < pa.length - 1; i++) { 657 for (int j = i + 1; j < pa.length; j++) { 658 double separation = separation(pa[i], pa[j]); 659 if (separation > max_separation) { 660 max_separation = separation; 661 p1 = pa[i]; 662 p2 = pa[j]; 663 } 664 } 665 } 666 667 // This can happen if enough values are NaN. 668 // if (p1 == null) { 669 // throw new IllegalArgumentException(Arrays.toString(pa)); 670 // } 671 672 if (Debug.logDetail()) { 673 wrapper.log("maxsep_doubles = %s %s", p1, p2); 674 } 675 if (p1 == null) { 676 return null; 677 } 678 return new Point[] { p1, p2 }; 679 } 680 681 /** 682 * Calculates the coefficients for the line in 3D 683 * and sets the coefficients[] by side effect. 684 * 685 * @param p0 first point on the line 686 * @param p1 second point on the line 687 */ 688 // 689 // the line can fall under 3 categories 690 // 691 // 1. parallel to an axis which means that 2 of the following is true 692 // x = A 693 // y = B 694 // z = C 695 // 696 // and the two that are true form a line in the 3rd dimension (the one that's 697 // not constant) 698 // 699 // 2. parallel to the plane of an axis, which means that one of the following 700 // is true 701 // x = A 702 // y = B 703 // z = C 704 // 705 // and the line is just a line in the non-constacoefficientble plane projected 706 // onto the third dimension 707 // and the equation for that line is: 708 // x = A [suppose that x is the constant one] 709 // y = Bz + C 710 // 711 // 712 // 3. none of the above and the equation of the line is just: 713 // y = Ax + B 714 // z = Cx + D 715 // 716 // Note that A, B, C, and D are coefficients that are stored in coefficients[] 717 718 private void calc_bi_linear(Point p0, Point p1) { 719 720 if ((p0.x == p1.x) && (p0.y == p1.y) && (p0.z != p1.z)) { 721 // x and y have constant values 722 // line is defined by x = A, y = B 723 line_flag = Flag.XY_CONSTANT; 724 coefficients[0] = p0.x; 725 coefficients[1] = p0.y; 726 coefficients[2] = 0; 727 coefficients[3] = 0; 728 return; 729 } 730 if ((p0.x == p1.x) && (p0.z == p1.z) && (p0.y != p1.y)) { 731 // x and z have constant values 732 // line is defined by x = A, z = C 733 line_flag = Flag.XZ_CONSTANT; 734 coefficients[0] = p0.x; 735 coefficients[1] = p0.z; 736 coefficients[2] = 0; 737 coefficients[3] = 0; 738 return; 739 } 740 if ((p0.y == p1.y) && (p0.z == p1.z) && (p0.x != p1.x)) { 741 // y and z have constant values 742 // line is defined by y = B, z = C 743 line_flag = Flag.YZ_CONSTANT; 744 coefficients[0] = p0.y; 745 coefficients[1] = p0.z; 746 coefficients[2] = 0; 747 coefficients[3] = 0; 748 return; 749 } 750 if ((p0.x == p1.x) && (p0.y != p1.y) && (p0.z != p1.z)) { 751 // x has a constant value 752 // plane (degenerate) is defined by x = A, z = By + C 753 line_flag = Flag.X_CONSTANT; 754 coefficients[0] = p0.x; 755 coefficients[1] = (p1.z - p0.z)/(p1.y - p0.y); 756 coefficients[2] = (p0.z * p1.y - p0.y * p1.z)/(p1.y - p0.y); 757 coefficients[3] = 0; 758 return; 759 } 760 if ((p0.y == p1.y) && (p0.x != p1.x) && (p0.z != p1.z)) { 761 // y has a constant value 762 // plane (degenerate) is defined by y = B, z = Ax + C 763 line_flag = Flag.Y_CONSTANT; 764 coefficients[0] = p0.y; 765 coefficients[1] = (p1.z - p0.z)/(p1.x - p0.x); 766 coefficients[2] = (p0.z * p1.x - p0.x * p1.z)/(p1.x - p0.x); 767 coefficients[3] = 0; 768 return; 769 } 770 if ((p0.z == p1.z) && (p0.x != p1.x) && (p0.y != p1.y)) { 771 // z has a constant value 772 // plane (degenerate) is defined by z = C, y = Ax + B 773 line_flag = Flag.Z_CONSTANT; 774 coefficients[0] = p0.z; 775 coefficients[1] = (p1.y - p0.y)/(p1.x - p0.x); 776 coefficients[2] = (p0.y * p1.x - p0.x * p1.y)/(p1.x - p0.x); 777 coefficients[3] = 0; 778 return; 779 } 780 if ((p0.x != p1.x) && (p0.y != p1.y) && (p0.z != p1.z)) { 781 // no variables have a constant value 782 // plane (degenerate) is defined by y = Ax + B, z = Cx + D 783 line_flag = Flag.NO_CONSTANT_VARIABLES; 784 coefficients[0] = (p1.y - p0.y)/(p1.x - p0.x); 785 coefficients[1] = (p0.y * p1.x - p0.x * p1.y)/(p1.x - p0.x); 786 coefficients[2] = (p1.z - p0.z)/(p1.x - p0.x); 787 coefficients[3] = (p0.z * p1.x - p0.x * p1.z)/(p1.x - p0.x); 788 } 789 } 790 791 /** 792 * Calculates new coefficients that for the new point. Uses the 793 * new coefficients if they are relatively close to to the previous 794 * ones. Kills off the invariant if they are not. 795 * 796 * @return true if the new equation worked, false otherwise 797 */ 798 public boolean try_new_equation(double x, double y, double z) { 799 800 // Calculate max separation using this point and the existing 3 points. 801 def_points[3] = new Point(x, y, z); 802 double sep = maxsep_triples(def_points); 803 804 // If this point increased the separation, recalculate a, b, and c. 805 if (sep > separation) { 806 separation = sep; 807 double[] coef; 808 try { 809 // Requires that the first 3 elements of def_points must be non-null. 810 coef = calc_tri_linear(def_points); 811 if (Debug.logDetail()) { 812 wrapper.log("Calc new plane with points %s %s %s %s", 813 def_points[0], def_points[1], def_points[2], def_points[3]); 814 } 815 } catch (Exception e) { 816 return false; 817 } 818 819 // if the a, b, or c is a new min/max remember it. 820 if (coef[0] < min_a) min_a = coef[0]; 821 if (coef[0] > max_a) max_a = coef[0]; 822 if (coef[1] < min_b) min_b = coef[1]; 823 if (coef[1] > max_b) max_b = coef[1]; 824 if (coef[2] < min_c) min_c = coef[2]; 825 if (coef[2] > max_c) max_c = coef[2]; 826 if (coef[3] < min_d) min_d = coef[3]; 827 if (coef[3] > max_d) { 828 max_d = coef[3]; 829 } 830 831 // Pick a new a, b, and c as the average of their endpoints 832 a = (min_a + max_a) / 2; 833 b = (min_b + max_b) / 2; 834 c = (min_c + max_c) / 2; 835 d = (min_d + max_d) / 2; 836 if (Invariant.logOn() || debug.isLoggable(Level.FINE)) { 837 wrapper.log(debug, wrapper.ppt.name() + ": Trying new a (" + a 838 + "), b (" + b + "), c (" + c + "), and d (" + d + ")"); 839 } 840 wrapper.log("min max: Trying new a (%s), b (%s), c (%s), and d (%s)", 841 a, b, c, d); 842 // if the new coefficients are 'equal' to their min and max and 843 // this point fits, then this new equation is good enough both 844 // for existing points and the new point. 845 if (Global.fuzzy.eq(a, min_a) && Global.fuzzy.eq(a, max_a) 846 && Global.fuzzy.eq(b, min_b) && Global.fuzzy.eq(b, max_b) 847 && Global.fuzzy.eq(c, min_c) && Global.fuzzy.eq(c, max_c) 848 && Global.fuzzy.eq(d, min_d) && Global.fuzzy.eq(d, max_d) 849 && Global.fuzzy.eq(-d, a * x + b * y + c * z)) { 850 if (debug.isLoggable(Level.FINE)) { 851 debug.fine(wrapper.ppt.name() + ": New a (" + a + ") and b (" 852 + b + ") and c (" + c + ")"); 853 } 854 return true; 855 } else { 856 return false; 857 } 858 } else { // this point doesn't increase the separation 859 860 return false; 861 } 862 } 863 864 /** 865 * Calculates the separation between p1 and p2. 866 * 867 * @param p1 first point 868 * @param p2 second point 869 * 870 * @return the distance between p1 and p2, or 0 if either point is null, or NaN if either point 871 * contains a NaN 872 */ 873 double separation(Point p1, Point p2) { 874 875 // Potential problem: This may return 0, for two reasons. First, x1-x2 876 // might be zero due to underflow, even if x1!=x2. Second, squaring a 877 // small x1-x2 might result in 0, even if x1-x2!=0. 878 879 // make sure both points are specified 880 if ((p1 == null) || (p2 == null)) { 881 return 0; 882 } 883 884 double xsep = (p1.x - p2.x); 885 double ysep = (p1.y - p2.y); 886 double zsep = (p1.z - p2.z); 887 return Math.sqrt(xsep * xsep + ysep * ysep + zsep * zsep); 888 } 889 890 /** 891 * Calculates the three points that have the maximum separation in pa and places them as the first 892 * three elements of pa. 893 * 894 * @param pa array of points. Must have at least 3 elements. Can be any length and can contain 895 * nulls (which will be ignored). Is side-effected so that the first three elements contain 896 * the points with the maximum total separation; this may introduce duplicates into the array. 897 * The first three elements are null if no triple of elements is NaN-free. 898 * @return the maximum separation found 899 */ 900 double maxsep_triples(@Nullable Point[] pa) { 901 902 // cache values for the (square of the) distance between each pair of 903 // points, to avoid duplicating work 904 double[][] separations = new double[pa.length][pa.length]; 905 for (int i = 0; i < pa.length - 1; i++) { 906 for (int j = i + 1; j < pa.length; j++) { 907 separations[i][j] = separation(pa[i], pa[j]); 908 } 909 } 910 911 Point p1 = null; 912 Point p2 = null; 913 Point p3 = null; 914 915 // max_separation is the separation metric for the most separated 916 // triple of points. We use the sum of the separations as the 917 // metric. (The metric "min of the three separations" does not work 918 // because it doesn't choose a unique set of points, making the 919 // result dependent on the order in which the points are seen; more 920 // seriously, it may choose a collinear set of points even when a 921 // non-collinear set exists.) 922 double max_separation = Double.MIN_VALUE; 923 924 for (int i = 0; i < pa.length - 2; i++) { 925 for (int j = i + 1; j < pa.length - 1; j++) { 926 double sep_i_j = separations[i][j]; 927 for (int k = j + 1; k < pa.length; k++) { 928 929 // using the sum of separations is valid, as long as 930 // separation is the actual distance between points and not 931 // the square of the distance 932 double separation = sep_i_j + separations[i][k] + separations[j][k]; 933 if (separation > max_separation) { 934 max_separation = separation; 935 p1 = pa[i]; 936 p2 = pa[j]; 937 p3 = pa[k]; 938 } 939 } 940 } 941 } 942 943 pa[0] = p1; 944 pa[1] = p2; 945 pa[2] = p3; 946 947 if (Debug.logDetail()) { 948 wrapper.log("maxsep_triples = %s %s %s", pa[0], pa[1], pa[2]); 949 } 950 return max_separation; 951 } 952 953 // Given ((x0,y0,z0),(x1,y1,z1), (x2,y2,z2), calculate a, b, c and d 954 // such that ax + by + cz + d = 0. 955 // a, b, c and d are mutually prime, integers and a is positive. 956 // 957 // A visual explanation of the math can be found in: 958 // http://www.efm.leeds.ac.uk/CIVE/CIVE2599/cive2599-summary-overheads-full.pdf 959 // 960 // The standard form of a plane can be calculated using a vector 961 // normal "n" <n1, n2, n3> to the plane and a vector from the origin 962 // to the plane "r" e.g. <x0, y0, z0>. 963 // 964 // The vector normal to the plane can be calculated by doing the cross product 965 // of two line segments on the plane (<point2 - point0> and <point1 - point0>) 966 // 967 // Given the normal vector and a point on the plane, the standard form 968 // of the plane is: 969 // n1*x + n2*y + n3*z = p where p is the dot product of r and n 970 // 971 // 972 973 /** 974 * Calculates the coefficients (a, b, c) and constant (d) for the equation ax + by + cz + d = 0 975 * using the first three points in points. 976 * 977 * @param points array of points to use to calculate the coefficents. Only the first three points 978 * (all of which must be non-null) are used. 979 * 980 * @return a four element array where a is the first element, b the second, c the third, and d is 981 * the fourth. All elements are mutually prime, integers and a is positive. 982 */ 983 // TODO: should just pass in the first three elements rather than passing 984 // in the point array. 985 public double[] calc_tri_linear(@Nullable Point[] points) { // TODO: remove annotation after refactoring method 986 987 Point p0 = points[0]; 988 Point p1 = points[1]; 989 Point p2 = points[2]; 990 991 // the following code is taken from the source page of 992 // http://jblanco_60.tripod.com/plane.html (the math behind the 993 // implementation is detailed above) 994 995 double px = p0.x; 996 double py = p0.y; 997 double pz = p0.z; 998 double qx = p1.x; 999 double qy = p1.y; 1000 double qz = p1.z; 1001 double rx = p2.x; 1002 double ry = p2.y; 1003 double rz = p2.z; 1004 1005 // define the i, j, k components of the two line segments on the plane 1006 double a1 = (qx - px); 1007 double a2 = (qy - py); 1008 double a3 = (qz - pz); 1009 1010 double b1 = (rx - px); 1011 double b2 = (ry - py); 1012 double b3 = (rz - pz); 1013 1014 // calculate the i, j, k components of the cross product 1015 double i_var = (a2 * b3) - (b2 * a3); 1016 double j_var = -((a1 * b3) - (b1 * a3)); 1017 double k_var = (a1 * b2) - (b1 * a2); 1018 1019 // Calculate the value of the constant. Note that given the format 1020 // of the point-normal form, we multiply by the negative of P(x,y,z) 1021 1022 double Stand_const = ((i_var*(-px)) + (j_var*(-py)) + (k_var*(-pz))); 1023 1024 // Put the coefficients in lowest terms by dividing by the gcd. 1025 // If the gcd is 1, no harm done -- divide by 1. 1026 // Type is double to ensure floating-point division. 1027 double myGCD = MathPlume.gcd(MathPlume.gcd(i_var, j_var) , MathPlume.gcd(k_var, Stand_const)); 1028 double standard_i_var = i_var / myGCD; 1029 double standard_j_var = j_var / myGCD; 1030 double standard_k_var = k_var / myGCD; 1031 double standard_Stand_const = Stand_const / myGCD; 1032 1033 if (wrapper != null) { 1034 wrapper.log("Preliminary: %s %s GCD: %s", i_var, j_var, MathPlume.gcd(i_var, j_var)); 1035 wrapper.log("Preliminary: %s %s GCD: %s", k_var, Stand_const, MathPlume.gcd(k_var, Stand_const)); 1036 wrapper.log("GCD: %s", myGCD); 1037 } 1038 1039 // Ensure postive x coefficient by negating if "x" term is negative. 1040 if (i_var < 0) { 1041 standard_i_var = - standard_i_var; 1042 standard_j_var = - standard_j_var; 1043 standard_k_var = - standard_k_var; 1044 standard_Stand_const = - standard_Stand_const; 1045 } 1046 1047 double[] coef = new double[] {standard_i_var, 1048 standard_j_var, 1049 standard_k_var, standard_Stand_const }; 1050 1051 return coef; 1052 } 1053 1054 public boolean enoughSamples(@GuardSatisfied LinearTernaryCoreFloat this) { 1055 return isActive(); 1056 } 1057 1058 // If the values form a line, 1059 // we have no confidence that it's a plane. 1060 // The line is less interesting because the invariant 1061 // is already defined by a linear binary invariant. 1062 public double computeConfidence() { 1063 if (isActive()) { 1064 return Invariant.conf_is_ge(values_seen, MINTRIPLES); 1065 } else { 1066 return 0; 1067 } 1068 1069 } 1070 1071 public String repr(@GuardSatisfied LinearTernaryCoreFloat this) { 1072 return "LinearTernaryCoreFloat" + wrapper.varNames() + ": a=" + a 1073 + ",b=" + b 1074 + ",c=" + c 1075 + ",d=" + d 1076 + ",values_seen=" + values_seen; 1077 } 1078 1079 public String point_repr(Point p) { 1080 if (p == null) { 1081 return "null"; 1082 } else { 1083 return "<" + p.x + "," + p.y + "," + p.z + ">"; 1084 } 1085 } 1086 1087 public String cache_repr() { 1088 StringBuilder result = new StringBuilder(); 1089 for (int i = 0; i < MINTRIPLES; i++) { 1090 if (i != 0) result.append("; "); 1091 result.append(point_repr(def_points[i])); 1092 } 1093 return result.toString(); 1094 } 1095 1096 // In this class for convenience (avoid prefixing "LinearBinaryCore"). 1097 static String formatTerm(double coeff, @Nullable String varname, boolean first) { 1098 return LinearBinaryCore.formatTerm(coeff, varname, first); 1099 } 1100 1101 @SideEffectFree 1102 public String format_using(OutputFormat format, 1103 String vix, String viy, String viz, 1104 double a, double b, double c, double d) { 1105 1106 if ((a == 0) && (b == 0) && (c == 0) && (d == 0)) { 1107 return wrapper.format_too_few_samples(format, null); 1108 } 1109 1110 if (format == OutputFormat.SIMPLIFY) { 1111 return format_simplify(vix, viy, viz, a, b, c, d); 1112 } 1113 1114 if ((format.isJavaFamily())) { 1115 1116 return 1117 // Add a 1 to each side of the equation because FuzzyFloat 1118 // doesn't treat 0 as 'fuzzy' when compared against another 1119 // number. 1120 "daikon.Quant.fuzzy.eq(" 1121 + formatTerm(a, vix, true) 1122 + formatTerm(b, viy, (a == 0)) 1123 + formatTerm(c, viz, (a == 0) && (b == 0)) 1124 + formatTerm(d, null, (a == 0) && (b == 0) && (c == 0)) 1125 + " + 1, 1)"; 1126 1127 } 1128 1129 if ((format == OutputFormat.DAIKON) 1130 || (format == OutputFormat.ESCJAVA) 1131 || (format == OutputFormat.CSHARPCONTRACT)) { 1132 String eq = " == "; 1133 return formatTerm(a, vix, true) 1134 + formatTerm(b, viy, (a == 0)) 1135 + formatTerm(c, viz, (a == 0) && (b == 0)) 1136 + formatTerm(d, null, (a == 0) && (b == 0) && (c == 0)) 1137 + eq + "0"; 1138 } 1139 1140 throw new Error("unrecognized output format " + format); 1141 // return null; 1142 } 1143 1144 public static String format_simplify(String vix, String viy, String viz, 1145 double da, double db, double dc, double dd) { 1146 int ia = (int) da; 1147 int ib = (int) db; 1148 int ic = (int) dc; 1149 int id = (int) dd; 1150 1151 String str_a, str_b, str_c, str_d; 1152 if (ia != da || ib != db || ic != dc || id != dd) { 1153 // floating point 1154 1155 // Disabled for the moment, since mixing integers and floating 1156 // literals seems to give Simplify indigestion. For instance: 1157 // (BG_PUSH (<= w 3)) 1158 // (BG_PUSH (EQ 0 (* w 2.0d0))) 1159 // (<= w 1) 1160 1161 // str_a = Invariant.simplify_format_double(da); 1162 // str_b = Invariant.simplify_format_double(db); 1163 // str_c = Invariant.simplify_format_double(dc); 1164 // str_d = Invariant.simplify_format_double(dd); 1165 return "(AND)"; // really s/b format_unimplemented 1166 } else { 1167 // integer 1168 str_a = Invariant.simplify_format_long(ia); 1169 str_b = Invariant.simplify_format_long(ib); 1170 str_c = Invariant.simplify_format_long(ic); 1171 str_d = Invariant.simplify_format_long(id); 1172 } 1173 1174 String str_z = viz; 1175 String str_x = vix; 1176 String str_y = viy; 1177 String str_ax = (da == 1.0) ? str_x : "(* " + str_a + " " + str_x + ")"; 1178 String str_by = (db == 1.0) ? str_y : "(* " + str_b + " " + str_y + ")"; 1179 String str_cz = (dc == 1.0) ? str_z : "(* " + str_c + " " + str_z + ")"; 1180 String str_axPbyPcz = "(+ " + str_ax + " " + str_by + " " + str_cz + ")"; 1181 String str_axPbyPczPd = (dd == 0.0) ? str_axPbyPcz : 1182 "(+ " + str_axPbyPcz + " " + str_d + ")"; 1183 return "(EQ 0 " + str_axPbyPczPd + ")"; 1184 } 1185 1186 @SideEffectFree 1187 public String format_using(OutputFormat format, 1188 String vix, String viy, String viz 1189 ) { 1190 String result = format_using(format, vix, viy, viz, a, b, c, d); 1191 if (result != null) { 1192 return result; 1193 } 1194 1195 return wrapper.format_unimplemented(format); 1196 } 1197 1198 // // Format as "x = cy+d" instead of as "y = ax+b". 1199 // public String format_reversed(String x, String y) { 1200 // assert a == 1 || a == -1; 1201 // return format(y, x, a, -b/a); 1202 // } 1203 1204 @Pure 1205 public boolean isSameFormula(LinearTernaryCoreFloat other) { 1206 1207 // If both have yet to see enough values 1208 if (!isActive() && !other.isActive()) { 1209 1210 // Same formula if all of the points match 1211 if (values_seen != other.values_seen) { 1212 return false; 1213 } 1214 // This and elsewhere seem to assume that values_seen < MINTRIPLES; 1215 // is that necessarily true? 1216 for (int ii = 0; ii < values_seen; ii++) { 1217 // used to use !=, but that test seems wrong 1218 if (!def_points[ii].equals(other.def_points[ii])) { 1219 return false; 1220 } 1221 } 1222 return true; 1223 } else { 1224 return ((values_seen >= MINTRIPLES) 1225 && (other.values_seen >= MINTRIPLES) 1226 && (a == other.a) 1227 && (b == other.b) 1228 && (c == other.c) 1229 && (d == other.d)); 1230 } 1231 } 1232 1233 @Pure 1234 public boolean isExclusiveFormula(LinearTernaryCoreFloat other) { 1235 if (!isActive() 1236 || !other.isActive()) { 1237 return false; 1238 } 1239 1240 return ((a == other.a) 1241 && (b != other.b) 1242 && (c != other.c) 1243 && (d != other.d)); 1244 } 1245 1246 /** 1247 * In general, we can't merge formulas, but we can merge invariants with too few samples to have 1248 * formed a plane with invariants with enough samples. And those will appear to have different 1249 * formulas. 1250 */ 1251 public boolean mergeFormulasOk() { 1252 return true; 1253 } 1254 1255 /** 1256 * Merge the linear ternary cores in cores to form a new core. Any core in the list that has seen 1257 * enough points to define a plane, must define the same plane. Any cores that have not yet seen 1258 * enough points, will have each of their points applied to that invariant. The merged core is 1259 * returned. Null is returned if the cores don't describe the same plane 1260 * 1261 * @param cores list of LinearTernary cores to merge. They should all be permuted to match the 1262 * variable order in ppt. 1263 */ 1264 public @Nullable LinearTernaryCoreFloat merge(List<LinearTernaryCoreFloat> cores, Invariant wrapper) { 1265 1266 // Look for any active planes. All must define the same plane 1267 LinearTernaryCoreFloat first = null; 1268 for (LinearTernaryCoreFloat c : cores) { 1269 if (!c.isActive()) { 1270 continue; 1271 } 1272 if (first == null) { 1273 first = c.clone(); 1274 } else { 1275 if (!Global.fuzzy.eq(first.a, c.a) 1276 || !Global.fuzzy.eq(first.b, c.b) 1277 || !Global.fuzzy.eq(first.c, c.c) 1278 || !Global.fuzzy.eq(first.d, c.d)) 1279 return null; 1280 } 1281 } 1282 1283 // If no active planes were found, created an empty core 1284 if (first == null) { 1285 first = new LinearTernaryCoreFloat(wrapper); 1286 } else { 1287 first.wrapper = wrapper; 1288 } 1289 1290 // Merge in any points from non-active cores 1291 // Note that while null points can't show up in a core that is not active 1292 // because it hasn't seen enough values, they can show up if the core 1293 // is not active because it is a line. 1294 for (LinearTernaryCoreFloat c : cores) { 1295 if (c.isActive()) { 1296 continue; 1297 } 1298 for (int j = 0; j < c.values_seen; j++) { 1299 Point cp = c.def_points[j]; 1300 if (cp == null) { 1301 continue; 1302 } 1303 if (Debug.logDetail()) { 1304 wrapper.log("Adding point %s from %s", cp, c.wrapper.ppt); 1305 } 1306 InvariantStatus stat = first.add_modified(cp.x, cp.y, cp.z, 1); 1307 if (stat == InvariantStatus.FALSIFIED) { 1308 return null; 1309 } 1310 // if (wrapper.is_false()) 1311 // return null; 1312 } 1313 } 1314 1315 return first; 1316 } 1317}