001// ***** This file is automatically generated from LinearBinary.java.jpp
002
003package daikon.inv.binary.twoScalar;
004
005import daikon.*;
006import daikon.derive.unary.SequenceLength;
007import daikon.inv.*;
008import java.util.*;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import org.checkerframework.checker.nullness.qual.NonNull;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.checkerframework.checker.nullness.qual.Nullable;
013import org.checkerframework.dataflow.qual.Pure;
014import org.checkerframework.dataflow.qual.SideEffectFree;
015import typequals.prototype.qual.NonPrototype;
016import typequals.prototype.qual.Prototype;
017
018/**
019 * Represents a Linear invariant between two double scalars {@code x} and {@code y}, of
020 * the form {@code ax + by + c = 0}. The constants {@code a}, {@code b} and
021 * {@code c} are mutually relatively prime, and the constant {@code a} is always positive.
022 */
023public class LinearBinaryFloat extends TwoFloat {
024  static final long serialVersionUID = 20030822L;
025
026  // Variables starting with dkconfig_ should only be set via the
027  // daikon.config.Configuration interface.
028  /** Boolean. True iff LinearBinary invariants should be considered. */
029  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
030
031  public LinearBinaryCoreFloat core;
032
033  @SuppressWarnings("nullness") // circular initialization
034  protected LinearBinaryFloat(PptSlice ppt) {
035    super(ppt);
036    core = new LinearBinaryCoreFloat(this);
037  }
038
039  @SuppressWarnings("nullness") // circular initialization
040  protected @Prototype LinearBinaryFloat() {
041    super();
042    // Do we need core to be set for a prototype invariant?
043    core = new LinearBinaryCoreFloat(this);
044  }
045
046  private static @Prototype LinearBinaryFloat proto = new @Prototype LinearBinaryFloat();
047
048  /** Returns a prototype LinearBinaryFloat invariant. */
049  public static @Prototype LinearBinaryFloat get_proto() {
050    return proto;
051  }
052
053  @Override
054  public boolean enabled() {
055    return dkconfig_enabled;
056  }
057
058  @Override
059  public boolean instantiate_ok(VarInfo[] vis) {
060
061    if (!valid_types(vis)) {
062      return false;
063    }
064
065    return true;
066  }
067
068  @Override
069  protected LinearBinaryFloat instantiate_dyn(@Prototype LinearBinaryFloat this, PptSlice slice) {
070    return new LinearBinaryFloat(slice);
071  }
072
073  @SideEffectFree
074  @Override
075  public LinearBinaryFloat clone(@GuardSatisfied LinearBinaryFloat this) {
076    LinearBinaryFloat result = (LinearBinaryFloat) super.clone();
077    result.core = core.clone();
078    result.core.wrapper = result;
079    return result;
080  }
081
082  @Override
083  protected Invariant resurrect_done_swapped() {
084    core.swap();
085    return this;
086  }
087
088  @Override
089  public String repr(@GuardSatisfied LinearBinaryFloat this) {
090    return "LinearBinaryFloat" + varNames() + ": falsified=" + falsified
091      + "; " + core.repr();
092  }
093
094  @SideEffectFree
095  @Override
096  public String format_using(@GuardSatisfied LinearBinaryFloat this, OutputFormat format) {
097    return core.format_using(format, var1().name_using(format),
098                             var2().name_using(format));
099  }
100
101  @Pure
102  @Override
103  public boolean isActive() {
104    return core.isActive();
105  }
106
107  @Override
108  public boolean mergeFormulasOk() {
109    return core.mergeFormulasOk();
110  }
111
112  /**
113   * Merge the invariants in invs to form a new invariant. Each must be a LinearBinaryFloat invariant. The
114   * work is done by the LinearBinary core
115   *
116   * @param invs list of invariants to merge. They should all be permuted to match the variable
117   *     order in parent_ppt.
118   * @param parent_ppt slice that will contain the new invariant
119   */
120  @Override
121  public @Nullable LinearBinaryFloat merge(List<Invariant> invs, PptSlice parent_ppt) {
122
123    // Create a matching list of cores
124    List<LinearBinaryCoreFloat> cores = new ArrayList<>();
125    for (Invariant inv : invs) {
126      cores.add(((LinearBinaryFloat) inv).core);
127    }
128
129    // Merge the cores and build a new invariant containing the merged core
130    LinearBinaryFloat result = new LinearBinaryFloat(parent_ppt);
131    LinearBinaryCoreFloat newcore = core.merge(cores, result);
132    if (newcore == null) {
133      return null;
134    }
135    result.core = newcore;
136    return result;
137  }
138
139  @Override
140  public InvariantStatus check_modified(double x, double y, int count) {
141    return clone().add_modified(x, y, count);
142  }
143
144  @Override
145  public InvariantStatus add_modified(double x, double y, int count) {
146    return core.add_modified(x, y, count);
147  }
148
149  @Override
150  public boolean enoughSamples(@GuardSatisfied LinearBinaryFloat this) {
151    return core.enoughSamples();
152  }
153
154  @Override
155  protected double computeConfidence() {
156    return core.computeConfidence();
157  }
158
159  @Pure
160  @Override
161  public boolean isExact() {
162    return true;
163  }
164
165  @Pure
166  @Override
167  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
168    // Obvious derived
169    VarInfo var1 = vis[0];
170    VarInfo var2 = vis[1];
171    // avoid comparing "size(a)" to "size(a)-1"; yields "size(a)-1 = size(a) - 1"
172    if (var1.isDerived()
173        && (var1.derived instanceof SequenceLength)
174        && var2.isDerived()
175        && (var2.derived instanceof SequenceLength)) {
176      @NonNull SequenceLength sl1 = (SequenceLength) var1.derived;
177      @NonNull SequenceLength sl2 = (SequenceLength) var2.derived;
178      if (sl1.base == sl2.base) {
179        String discardString = var1.name()+" and "+var2.name()+" derived from "+
180          "same sequence: "+sl1.base.name();
181        return new DiscardInfo(this, DiscardCode.obvious, discardString);
182      }
183    }
184    // avoid comparing "size(a)-1" to anything; should compare "size(a)" instead
185    if (var1.isDerived()
186        && (var1.derived instanceof SequenceLength)
187        && ((SequenceLength) var1.derived).shift != 0) {
188      String discardString = "Variables of the form 'size(a)-1' are not compared since 'size(a)' "+
189        "will be compared";
190      return new DiscardInfo(this, DiscardCode.obvious, discardString);
191    }
192    if (var2.isDerived()
193        && (var2.derived instanceof SequenceLength)
194        && ((SequenceLength) var2.derived).shift != 0) {
195      String discardString = "Variables of the form 'size(a)-1' are not compared since 'size(a)' "+
196        "will be compared";
197      return new DiscardInfo(this, DiscardCode.obvious, discardString);
198    }
199
200    return super.isObviousStatically(vis);
201  }
202
203  @Pure
204  @Override
205  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
206    DiscardInfo super_result = super.isObviousDynamically(vis);
207    if (super_result != null) {
208      return super_result;
209    }
210
211    if (core.a == 0) {
212      return new DiscardInfo(this, DiscardCode.obvious, var2().name() + " is constant");
213    }
214    if (core.b == 0) {
215      return new DiscardInfo(this, DiscardCode.obvious, var1().name() + " is constant");
216    }
217//    if (core.a == 1 && core.b == 0) {
218//      return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
219//    }
220    if (core.a == -core.b && core.c == 0) {
221     return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
222    }
223    return null;
224  }
225
226  @Pure
227  @Override
228  public boolean isSameFormula(Invariant other) {
229    return core.isSameFormula(((LinearBinaryFloat) other).core);
230  }
231
232  @Pure
233  @Override
234  public boolean isExclusiveFormula(Invariant other) {
235    if (other instanceof LinearBinaryFloat) {
236      return core.isExclusiveFormula(((LinearBinaryFloat) other).core);
237    }
238    return false;
239  }
240
241  // Look up a previously instantiated invariant.
242  public static @Nullable LinearBinaryFloat find(PptSlice ppt) {
243    assert ppt.arity() == 2;
244    for (Invariant inv : ppt.invs) {
245      if (inv instanceof LinearBinaryFloat) {
246        return (LinearBinaryFloat) inv;
247      }
248    }
249    return null;
250  }
251
252  // Returns a vector of LinearBinary objects.
253  // This ought to produce an iterator instead.
254  public static List<LinearBinaryFloat> findAll(VarInfo vi) {
255    List<LinearBinaryFloat> result = new ArrayList<>();
256    for (PptSlice view : vi.ppt.views_iterable()) {
257      if ((view.arity() == 2) && view.usesVar(vi)) {
258        LinearBinaryFloat lb = LinearBinaryFloat.find(view);
259        if (lb != null) {
260          result.add(lb);
261        }
262      }
263    }
264    return result;
265  }
266}