001// ***** This file is automatically generated from Reverse.java.jpp 002 003package daikon.inv.binary.twoSequence; 004 005import daikon.*; 006import daikon.inv.*; 007import java.util.logging.Logger; 008import org.checkerframework.checker.interning.qual.Interned; 009import org.checkerframework.checker.lock.qual.GuardSatisfied; 010import org.checkerframework.dataflow.qual.Pure; 011import org.checkerframework.dataflow.qual.SideEffectFree; 012import org.plumelib.util.Intern; 013import typequals.prototype.qual.NonPrototype; 014import typequals.prototype.qual.Prototype; 015 016/** 017 * Represents two sequences of double where one is in the reverse order of the other. Prints as 018 * {@code x[] is the reverse of y[]}. 019 */ 020public class ReverseFloat extends TwoSequenceFloat { 021 // We are Serializable, so we specify a version to allow changes to 022 // method signatures without breaking serialization. If you add or 023 // remove fields, you should change this number to the current date. 024 static final long serialVersionUID = 20030822L; 025 026 public static final Logger debug = 027 Logger.getLogger("daikon.inv.binary.twoSequence.ReverseFloat"); 028 029 // Variables starting with dkconfig_ should only be set via the 030 // daikon.config.Configuration interface. 031 /** Boolean. True iff Reverse invariants should be considered. */ 032 public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault; 033 034 protected ReverseFloat(PptSlice ppt) { 035 super(ppt); 036 } 037 038 protected @Prototype ReverseFloat() { 039 super(); 040 } 041 042 private static @Prototype ReverseFloat proto = new @Prototype ReverseFloat(); 043 044 /** Returns the prototype invariant for ReverseFloat */ 045 public static @Prototype ReverseFloat get_proto() { 046 return proto; 047 } 048 049 /** returns whether or not this invariant is enabled */ 050 @Override 051 public boolean enabled() { 052 return dkconfig_enabled; 053 } 054 055 /** Reverse only makes sense on ordered arrays. */ 056 @Override 057 public boolean instantiate_ok(VarInfo[] vis) { 058 059 if (!valid_types(vis)) { 060 return false; 061 } 062 063 // Check to see that both arrays are ordered 064 if (!vis[0].aux.hasOrder() || !vis[1].aux.hasOrder()) { 065 return false; 066 } 067 068 return true; 069 } 070 071 /** instantiates the invariant on the specified slice */ 072 @Override 073 public ReverseFloat instantiate_dyn(@Prototype ReverseFloat this, PptSlice slice) { 074 return new ReverseFloat(slice); 075 } 076 077 @Override 078 protected Invariant resurrect_done_swapped() { 079 // "reverse of" is symmetric 080 return this; 081 } 082 083 @Override 084 public String repr(@GuardSatisfied ReverseFloat this) { 085 return "ReverseFloat" + varNames() + ": falsified=" + falsified; 086 } 087 088 @SideEffectFree 089 @Override 090 public String format_using(@GuardSatisfied ReverseFloat this, OutputFormat format) { 091 if (format.isJavaFamily()) { 092 return format_java_family(format); 093 } 094 095 if (format == OutputFormat.DAIKON) { 096 return format_daikon(); 097 } 098 if (format == OutputFormat.CSHARPCONTRACT) { 099 return format_csharp(); 100 } 101 if (format == OutputFormat.SIMPLIFY) { 102 return format_simplify(); 103 } 104 105 return format_unimplemented(format); 106 } 107 108 public String format_daikon(@GuardSatisfied ReverseFloat this) { 109 return var1().name() + " is the reverse of " + var2().name(); 110 } 111 112 public String format_java_family(@GuardSatisfied ReverseFloat this, OutputFormat format) { 113 return "daikon.Quant.isReverse(" + var1().name_using(format) 114 + ", " + var2().name_using(format) + ")"; 115 } 116 117 public String format_csharp(@GuardSatisfied ReverseFloat this) { 118 String[] split1 = var1().csharp_array_split(); 119 String[] split2 = var2().csharp_array_split(); 120 return "Contract.ForAll(0, " + split1[0] + ".Count(), i => " + split1[0] + "[i]" + split1[1] + ".Equals(" + split2[0] + "[" +split1[0] + ".Count()-1-i]" + split2[1] +"))"; 121 } 122 123 public String format_simplify(@GuardSatisfied ReverseFloat this) { 124 if (Invariant.dkconfig_simplify_define_predicates) { 125 return format_simplify_defined(); 126 } else { 127 return format_simplify_explicit(); 128 } 129 } 130 131 private String format_simplify_defined(@GuardSatisfied ReverseFloat this) { 132 VarInfo onevar = var1(); 133 VarInfo othervar = var2(); 134 String[] one_name = onevar.simplifyNameAndBounds(); 135 String[] other_name = othervar.simplifyNameAndBounds(); 136 137 if (one_name == null || other_name == null) { 138 return "format_simplify() can't handle one of these sequences: " + format(); 139 } 140 141 return "(|is-reverse-of| " 142 + one_name[0] + " " + one_name[1] + " " + one_name[2] + " " 143 + other_name[0] + " " + other_name[1] + " " + other_name[2] + ")"; 144 } 145 146 private String format_simplify_explicit(@GuardSatisfied ReverseFloat this) { 147 VarInfo onevar = var1(); 148 VarInfo othervar = var2(); 149 String[] one_name = onevar.simplifyNameAndBounds(); 150 String[] other_name = othervar.simplifyNameAndBounds(); 151 152 if (one_name == null || other_name == null) { 153 return "format_simplify() can't handle one of these sequences: " + format(); 154 } 155 156 String index = VarInfo.get_simplify_free_index(onevar, othervar); 157 158 // (FORALL (a i j b ip jp) 159 // (IFF (|is-reverse-of| a i j b ip jp) 160 // (AND (EQ (- j i) (- jp ip)) 161 // (<= 0 i) 162 // (< j (arrayLength a)) 163 // (<= 0 ip) 164 // (< jp (arrayLength b)) 165 // (FORALL (x) 166 // (IMPLIES 167 // (AND (<= 0 x) (< x (- j i))) 168 // (EQ (select (select elems a) (+ i x)) 169 // (select (select elems b) (- jp x)))))))) 170 171 return "(AND (EQ (- " + one_name[2] + " " + one_name[1] + ") (- " 172 + other_name[2] + " " + other_name[1] + ")) (<= 0 " + one_name[1] 173 + ") (< " + one_name[2] + " (arrayLength " + one_name[0] 174 + ")) (<= 0 " + other_name[1] + ") (< " + other_name[2] 175 + " (arrayLength " + other_name[0] + ")) (FORALL (" + index 176 + ") (IMPLIES (AND (<= 0 " + index + ") (< " + index + " (- " 177 + one_name[2] + " " + one_name[1] + "))) (EQ (select (select elems " 178 + one_name[0] + ") (+ " + one_name[1] + " " + index 179 + ")) (select (select elems " + other_name[0] + ") (- " + other_name[2] 180 + " " + index + "))))))"; 181 } 182 183 @Override 184 public InvariantStatus check_modified(double @Interned [] a1, double @Interned [] a2, int count) { 185 if (a1.length != a2.length) { 186 return InvariantStatus.FALSIFIED; 187 } 188 int len = a1.length; 189 for (int i = 0, j = len - 1; i < len; i++, j--) { 190 if (!Global.fuzzy.eq(a1[i], a2[j])) { 191 return InvariantStatus.FALSIFIED; 192 } 193 } 194 return InvariantStatus.NO_CHANGE; 195 } 196 197 @Override 198 public InvariantStatus add_modified(double @Interned [] a1, double @Interned [] a2, int count) { 199 return check_modified(a1, a2, count); 200 } 201 202 @Override 203 protected double computeConfidence() { 204 return Invariant.CONFIDENCE_JUSTIFIED; 205 } 206 207 @Pure 208 @Override 209 public boolean isSameFormula(Invariant other) { 210 assert other instanceof ReverseFloat; 211 return true; 212 } 213}