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}