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