001// ***** This file is automatically generated from SequenceArbitrarySubsequenceFactory.java.jpp 002 003package daikon.derive.ternary; 004 005import org.checkerframework.checker.nullness.qual.Nullable; 006import daikon.*; 007import daikon.inv.binary.twoScalar.*; // for IntComparison 008import java.util.*; 009 010public final class SequenceStringArbitrarySubsequenceFactory extends TernaryDerivationFactory { 011 012 // When calling/creating the derivations, arrange that: 013 // base1 is the sequence 014 // base2 and base3 are the scalars 015 016 @Override 017 public TernaryDerivation @Nullable [] instantiate(VarInfo vi1, VarInfo vi2, VarInfo vi3) { 018 019 // check if the derivations are globally disabled 020 boolean enable_subsequence = SequenceStringArbitrarySubsequence.dkconfig_enabled; 021 if (!enable_subsequence) { 022 return null; 023 } 024 025 // This is not the very most efficient way to do this, but at 026 // least it is comprehensible. 027 VarInfo seqvar; 028 VarInfo sclvar1; 029 VarInfo sclvar2; 030 031 if ((vi1.rep_type == ProglangType.STRING_ARRAY) 032 && (vi2.rep_type == ProglangType.STRING) 033 && (vi3.rep_type == ProglangType.STRING)) { 034 seqvar = vi1; 035 sclvar1 = vi2; 036 sclvar2 = vi3; 037 } else if ((vi2.rep_type == ProglangType.STRING_ARRAY) 038 && (vi1.rep_type == ProglangType.STRING) 039 && (vi3.rep_type == ProglangType.STRING)) { 040 seqvar = vi2; 041 sclvar1 = vi1; 042 sclvar2 = vi3; 043 } else if ((vi3.rep_type == ProglangType.STRING_ARRAY) 044 && (vi1.rep_type == ProglangType.STRING) 045 && (vi2.rep_type == ProglangType.STRING)) { 046 seqvar = vi3; 047 sclvar1 = vi1; 048 sclvar2 = vi2; 049 } else { 050 return null; 051 } 052 053 if (!seqvar.aux.hasOrder()) { 054 // Indexing doesn't make sense if order doesn't matter 055 return null; 056 } 057 058 if (!seqvar.indexCompatible(sclvar1)) { 059 return null; 060 } 061 if (!seqvar.indexCompatible(sclvar2)) { 062 return null; 063 } 064 065 // For now, do nothing if the sequence is itself derived. 066 if (seqvar.derived != null) { 067 return null; 068 } 069 // For now, do nothing if the scalar is itself derived. 070 if (sclvar1.derived != null) { 071 return null; 072 } 073 if (sclvar2.derived != null) { 074 return null; 075 } 076 077 List<TernaryDerivation> results1 = instantiateWithOrder(seqvar, sclvar1, sclvar2); 078 List<TernaryDerivation> results2 = instantiateWithOrder(seqvar, sclvar2, sclvar1); 079 080 results1.addAll(results2); 081 return results1.toArray(new TernaryDerivation[0]); 082 } 083 084 private List<TernaryDerivation> instantiateWithOrder( 085 VarInfo seqvar, VarInfo startvar, VarInfo endvar) { 086 List<TernaryDerivation> results = new ArrayList<>(); 087 VarInfo seqsize = seqvar.sequenceSize(); 088 if (seqsize != null) { 089 seqsize = seqsize.canonicalRep(); 090 } 091 092 // SUPPRESS DERIVED VARIABLE: a[..i] where i == a.length 093 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i == a.length 094 // SUPPRESS DERIVED VARIABLE: a[i..] where i == a.length 095 // SUPPRESS DERIVED VARIABLE: a[i+1..] where i == a.length 096 // Since both are canonical, this is equivalent to 097 // "if (sclvar.canonicalRep() == seqsize.canonicalRep()) ..." 098 if (startvar == seqsize || endvar == seqsize) { 099 Global.tautological_suppressed_derived_variables += 4; 100 return results; 101 } 102 103 // SUPPRESS DERIVED VARIABLE: a[i] where (i >= a.length) can be true 104 // SUPPRESS DERIVED VARIABLE: a[i-1] where (i > a.length) can be true 105 // SUPPRESS DERIVED VARIABLE: a[..i] where (i >= a.length) can be true 106 // SUPPRESS DERIVED VARIABLE: a[..i-1] where (i > a.length) can be true 107 // SUPPRESS DERIVED VARIABLE: a[i..] where (i > a.length) can be true 108 // SUPPRESS DERIVED VARIABLE: a[i+1..] where (i >= a.length) can be true 109 // ***** This eliminates the derivation if it can *ever* be 110 // nonsensical/missing. Is that what I want? 111 // Find an IntComparison relationship over the scalar and the sequence 112 // size, if possible. 113 // PptSlice compar_slice = null; 114 // if (seqsize != null) { 115 // assert sclvar.ppt == seqsize.ppt; 116 // compar_slice = sclvar.ppt.findSlice_unordered(sclvar, seqsize); 117 // } 118 // if (compar_slice != null) { 119 // if ((sclvar.varinfo_index < seqsize.varinfo_index) 120 // ? IntLessEqual.find(compar_slice) == null // sclvar can be more than seqsize 121 // : IntGreaterEqual.find(compar_slice) == null // seqsize can be less than sclvar 122 // ) { 123 // Global.nonsensical_suppressed_derived_variables += 6; 124 // return null; 125 // } else if (IntEqual.find(compar_slice) != null) { 126 // Global.nonsensical_suppressed_derived_variables += 3; 127 // ArrayList<BinaryDerivation> result = new ArrayList<>(); 128 // if (enable_subscript) { 129 // result.add(new SEQUENCESCALARSUBSCRIPT(seqvar, sclvar, true)); // a[i-1] 130 // } 131 // if (enable_subsequence) { 132 // result.add(new SequenceStringArbitrarySubsequence(seqvar, sclvar, true, true)); // a[..i-1] 133 // result.add(new SequenceStringArbitrarySubsequence(seqvar, sclvar, false, false)); // a[i..] 134 // }; 135 // return result.toArray(new BinaryDerivation[0]); 136 // } 137 // } 138 139 // Abstract out these next two. 140 141 // If the scalar is a constant, then do all the following checks: 142 // 143 // If the scalar is a constant < 0: 144 // all derived variables are nonsensical 145 // SUPPRESS DERIVED VARIABLE: a[i] where i<0 and i is constant 146 // SUPPRESS DERIVED VARIABLE: a[i-1] where i<0 and i is constant 147 // SUPPRESS DERIVED VARIABLE: a[..i] where i<0 and i is constant 148 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i<0 and i is constant 149 // SUPPRESS DERIVED VARIABLE: a[i..] where i<0 and i is constant 150 // SUPPRESS DERIVED VARIABLE: a[i+1..] where i<0 and i is constant 151 // If the scalar is the constant 0: 152 // array[0] is already extracted 153 // array[-1] is nonsensical 154 // array[0..0] is already extracted 155 // array[0..-1] is nonsensical 156 // array[0..] is the same as array[] 157 // array[1..] should be extracted 158 // SUPPRESS DERIVED VARIABLE: a[i] where i==0 159 // SUPPRESS DERIVED VARIABLE: a[i-1] where i==0 160 // SUPPRESS DERIVED VARIABLE: a[..i] where i==0 161 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i==0 162 // SUPPRESS DERIVED VARIABLE: a[i..] where i==0 163 // If the scalar is the constant 1: 164 // array[1] is already extracted 165 // array[0] is already extracted 166 // array[0..1] should be extracted 167 // array[0..0] is already extracted 168 // array[1..] should be extracted 169 // array[2..] should be extracted 170 // SUPPRESS DERIVED VARIABLE: a[i] where i==1 171 // SUPPRESS DERIVED VARIABLE: a[i-1] where i==1 172 // SUPPRESS DERIVED VARIABLE: a[..i] where i==1 173 // SUPPRESS DERIVED VARIABLE: a[..i-1] where i==1 174 boolean suppress_i = false; 175 boolean suppress_j = false; 176 boolean suppress_i_plus_1 = false; 177 boolean suppress_j_minus_1 = false; 178 179 // If, for some canonical k, k=index+1, don't create array[index+1..]. 180 // If k=index-1, then don't create array[index-1] or array[0..index-1]. 181 // (k can have higher or lower VarInfo index than i.) 182 183 { 184 assert startvar.ppt == seqvar.ppt; 185 List<LinearBinary> lbs = LinearBinary.findAll(startvar); 186 for (Object lbObject : lbs) { 187 LinearBinary lb = (LinearBinary) lbObject; 188 // lb asserts that lb.var2() = lb.core.a * lb.var1() + lb.core.b <-- old 189 // Note that var2 comes before var1; this makes the most sense 190 // if you think of them as "y" and "x". <-- old 191 192 // lb asserts that lb.core.a * lb.var1() + lb.core.b * lb.var2() + lb.core.c == 0 193 // or lb.var2() == - (lb.core.a / lb.core.b) * lb.var1() - lb.core.c / lb.core.b 194 195 // if (lb.core.a == 1) { 196 if (-lb.core.a / lb.core.b == 1) { 197 // Don't set unconditionally, and don't break: we want to check 198 // other variables as well. 199 // if (lb.core.b == -1) { 200 if (-lb.core.c / lb.core.b == -1) { 201 if (lb.var1() != startvar) { 202 // i = k - 1, so k = i + 1 203 suppress_i_plus_1 = true; 204 } 205 } 206 // if (lb.core.b == 1) { 207 if (-lb.core.c / lb.core.b == 1) { 208 if (lb.var1() == startvar) { 209 // k = i + 1 210 suppress_i_plus_1 = true; 211 } 212 } 213 } 214 } 215 } 216 217 { 218 assert endvar.ppt == seqvar.ppt; 219 List<LinearBinary> lbs = LinearBinary.findAll(endvar); 220 for (Object lbObject : lbs) { 221 LinearBinary lb = (LinearBinary) lbObject; 222 // lb asserts that lb.var2() = lb.core.a * lb.var1() + lb.core.b <-- old 223 // Note that var2 comes before var1; this makes the most sense 224 // if you think of them as "y" and "x". <-- old 225 226 // lb asserts that lb.core.a * lb.var1() + lb.core.b * lb.var2() + lb.core.c == 0 227 // or lb.var2() == - (lb.core.a / lb.core.b) * lb.var1() - lb.core.c / lb.core.b 228 229 // if (lb.core.a == 1) { 230 if (-lb.core.a / lb.core.b == 1) { 231 // Don't set unconditionally, and don't break: we want to check 232 // other variables as well. 233 // if (lb.core.b == -1) { 234 if (-lb.core.c / lb.core.b == -1) { 235 if (lb.var1() == endvar) { 236 // k = j - 1 237 suppress_j_minus_1 = true; 238 } 239 } 240 // if (lb.core.b == 1) { 241 if (-lb.core.c / lb.core.b == 1) { 242 if (lb.var1() != endvar) { 243 // j = k + 1, so k = j - 1 244 suppress_j_minus_1 = true; 245 } 246 } 247 } 248 } 249 } 250 251 // End of applicability tests; now actually create the invariants 252 253 // a[i..j] 254 if (suppress_i || suppress_j) { 255 results.add(new SequenceStringArbitrarySubsequence(seqvar, startvar, endvar, true, true)); 256 } else { 257 Global.tautological_suppressed_derived_variables++; 258 } 259 260 // a[i+1..j] 261 if (suppress_i_plus_1 || suppress_j) { 262 Global.tautological_suppressed_derived_variables++; 263 } else { 264 results.add(new SequenceStringArbitrarySubsequence(seqvar, startvar, endvar, false, true)); 265 } 266 267 // a[i..j-1] 268 if (suppress_j_minus_1 || suppress_i) { 269 Global.tautological_suppressed_derived_variables++; 270 } else { 271 results.add(new SequenceStringArbitrarySubsequence(seqvar, startvar, endvar, true, false)); 272 } 273 274 // a[i+1..j-1] 275 if (suppress_i_plus_1 || suppress_j_minus_1) { 276 Global.tautological_suppressed_derived_variables++; 277 } else { 278 results.add(new SequenceStringArbitrarySubsequence(seqvar, startvar, endvar, false, false)); 279 } 280 281 return results; 282 } 283}