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