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