001// ***** This file is automatically generated from PairwiseLinearBinary.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import daikon.*; 006import daikon.Quantify.QuantFlags; 007import daikon.inv.*; 008import daikon.inv.DiscardCode; 009import daikon.inv.DiscardInfo; 010import daikon.inv.binary.twoScalar.*; 011import java.util.*; 012import org.checkerframework.checker.interning.qual.Interned; 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.Intern; 018import typequals.prototype.qual.NonPrototype; 019import typequals.prototype.qual.Prototype; 020 021/** 022 * Represents a linear invariant (i.e., {@code y = ax + b}) between the corresponding elements 023 * of two sequences of double values. Each {@code (x[i], y[i])} pair is examined. Thus, 024 * {@code x[0]} is compared to {@code y[0]}, {@code x[1]} to {@code y[1]} and so 025 * forth. Prints as {@code y[] = a * x[] + b}. 026 */ 027public class PairwiseLinearBinaryFloat extends TwoSequenceFloat { 028 static final long serialVersionUID = 20030822L; 029 030 // Variables starting with dkconfig_ should only be set via the 031 // daikon.config.Configuration interface. 032 /** Boolean. True iff PairwiseLinearBinary invariants should be considered. */ 033 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 034 035 public LinearBinaryCoreFloat core; 036 037 @SuppressWarnings("nullness") // circular initialization 038 protected PairwiseLinearBinaryFloat(PptSlice ppt) { 039 super(ppt); 040 core = new LinearBinaryCoreFloat(this); 041 } 042 043 @SuppressWarnings("nullness") // circular initialization 044 protected @Prototype PairwiseLinearBinaryFloat() { 045 super(); 046 // Do we need a core in a prototype invariant? 047 core = new LinearBinaryCoreFloat(this); 048 } 049 050 private static @Prototype PairwiseLinearBinaryFloat proto = new @Prototype PairwiseLinearBinaryFloat(); 051 052 /** Returns the prototype invariant for PairwiseLinearBinaryFloat. */ 053 public static @Prototype PairwiseLinearBinaryFloat get_proto() { 054 return proto; 055 } 056 057 @Override 058 public boolean enabled() { 059 return dkconfig_enabled; 060 } 061 062 @Override 063 protected PairwiseLinearBinaryFloat instantiate_dyn(@Prototype PairwiseLinearBinaryFloat this, PptSlice slice) { 064 return new PairwiseLinearBinaryFloat(slice); 065 } 066 067 @SideEffectFree 068 @Override 069 public PairwiseLinearBinaryFloat clone(@GuardSatisfied PairwiseLinearBinaryFloat this) { 070 PairwiseLinearBinaryFloat result = (PairwiseLinearBinaryFloat) super.clone(); 071 result.core = core.clone(); 072 result.core.wrapper = result; 073 return result; 074 } 075 076 @Override 077 protected Invariant resurrect_done_swapped() { 078 core.swap(); 079 return this; 080 } 081 082 @Override 083 public String repr(@GuardSatisfied PairwiseLinearBinaryFloat this) { 084 return "PairwiseLinearBinaryFloat" + varNames() + ": falsified=" + falsified 085 + "; " + core.repr(); 086 } 087 088 @SideEffectFree 089 @Override 090 public String format_using(@GuardSatisfied PairwiseLinearBinaryFloat this, OutputFormat format) { 091 if (core.a == 0 && core.b == 0 && core.c == 0) { 092 return format_too_few_samples(format, null); 093 } 094 095 if (format == OutputFormat.DAIKON) { 096 return format_daikon(); 097 } 098 // if (format == OutputFormat.JML) { 099 // return format_jml(); 100 // } 101 if (format == OutputFormat.SIMPLIFY) { 102 return format_simplify(); 103 } 104 if (format == OutputFormat.CSHARPCONTRACT) { 105 return format_csharp(); 106 } 107 108 return format_unimplemented(format); 109 } 110 111 public String format_daikon(@GuardSatisfied PairwiseLinearBinaryFloat this) { 112 return core.format_using(OutputFormat.DAIKON, var1().name(), 113 var2().name()); 114 } 115 116 public String format_simplify(@GuardSatisfied PairwiseLinearBinaryFloat this) { 117 String[] form = VarInfo.simplify_quantify(QuantFlags.element_wise(), 118 var1(), var2()); 119 return form[0] + LinearBinaryCoreFloat.format_simplify(form[1], form[2], 120 core.a, core.b, core.c) 121 + form[3]; 122 } 123 124 public String format_csharp(@GuardSatisfied PairwiseLinearBinaryFloat this) { 125 126 String[] split1 = var1().csharp_array_split(); 127 String[] split2 = var2().csharp_array_split(); 128 129 return "Contract.ForAll(0, " + split1[0] 130 + ".Count(), i => " 131 + core.format_using(OutputFormat.CSHARPCONTRACT, split1[0] + "[i]" + split1[1], split2[0] + "[i]" + split2[1]) 132 + ")"; 133 } 134 135 @Override 136 public InvariantStatus check_modified(double @Interned [] x_arr, double @Interned [] y_arr, int count) { 137 return clone().add_modified(x_arr, y_arr, count); 138 } 139 140 @Override 141 public InvariantStatus add_modified(double @Interned [] x_arr, double @Interned [] y_arr, int count) { 142 if (x_arr.length != y_arr.length) { 143 return InvariantStatus.FALSIFIED; 144 } 145 int len = x_arr.length; 146 // int len = Math.min(x_arr.length, y_arr.length); 147 148 for (int i = 0; i < len; i++) { 149 double x = x_arr[i]; 150 double y = y_arr[i]; 151 152 if (core.add_modified(x, y, count) == InvariantStatus.FALSIFIED) { 153 return InvariantStatus.FALSIFIED; 154 } 155 } 156 return InvariantStatus.NO_CHANGE; 157 } 158 159 @Override 160 protected double computeConfidence() { 161 return core.computeConfidence(); 162 } 163 164 @Pure 165 @Override 166 public boolean isSameFormula(Invariant other) { 167 return core.isSameFormula(((PairwiseLinearBinaryFloat) other).core); 168 } 169 170 @Pure 171 @Override 172 public boolean isExclusiveFormula(Invariant other) { 173 if (other instanceof PairwiseLinearBinaryFloat) { 174 return core.isExclusiveFormula(((PairwiseLinearBinaryFloat) other).core); 175 } 176 return false; 177 } 178 179 @Pure 180 @Override 181 public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) { 182 DiscardInfo super_result = super.isObviousDynamically(vis); 183 if (super_result != null) { 184 return super_result; 185 } 186 187 if (core.a == 0) { 188 return new DiscardInfo(this, DiscardCode.obvious, var2().name() + " is constant"); 189 } 190 if (core.b == 0) { 191 return new DiscardInfo(this, DiscardCode.obvious, var1().name() + " is constant"); 192 } 193// if (core.a == 1 && core.b == 0) { 194// return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal"); 195// } 196 if (core.a == -core.b && core.c == 0) { 197 return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal"); 198 } 199 return null; 200 } 201 202 @Pure 203 @Override 204 public boolean isActive() { 205 return core.isActive(); 206 } 207 208 @Override 209 public boolean mergeFormulasOk() { 210 return core.mergeFormulasOk(); 211 } 212 213 /** 214 * Merge the invariants in invs to form a new invariant. Each must be a PairwiseLinearBinaryFloat invariant. The 215 * work is done by the LinearBinary core 216 * 217 * @param invs list of invariants to merge. They should all be permuted to match the variable 218 * order in parent_ppt. 219 * @param parent_ppt slice that will contain the new invariant 220 */ 221 @Override 222 public @Nullable PairwiseLinearBinaryFloat merge(List<Invariant> invs, PptSlice parent_ppt) { 223 224 // Create a matching list of cores 225 List<LinearBinaryCoreFloat> cores = new ArrayList<>(); 226 for (Invariant inv : invs) { 227 cores.add(((PairwiseLinearBinaryFloat) inv).core); 228 } 229 230 // Merge the cores and build a new invariant containing the merged core 231 PairwiseLinearBinaryFloat result = new PairwiseLinearBinaryFloat(parent_ppt); 232 LinearBinaryCoreFloat newcore = core.merge(cores, result); 233 if (newcore == null) { 234 return null; 235 } 236 result.core = newcore; 237 return result; 238 } 239}