00001 00005 package edu.mit.csail.sdg.squander.engine; 00006 00007 import java.lang.reflect.Field; 00008 import java.util.LinkedHashMap; 00009 import java.util.List; 00010 import java.util.Map; 00011 import java.util.Set; 00012 00013 import edu.mit.csail.sdg.squander.log.Log; 00014 import edu.mit.csail.sdg.squander.utils.ReflectionUtils; 00015 import forge.solve.ForgeReporter; 00016 00023 public class SquanderReporter extends ForgeReporter { 00024 00025 public static final String BUILDING_ANALYSIS = "buildingAnalysis"; 00026 public static final String TRANSLATING_FORGE = "translatingForge"; 00027 public static final String PACKAGIN_ANALYSIS = "packaginAnalysis"; 00028 public static final String LOADING_JIMPLE = "loadingJimple"; 00029 public static final String ANALYSIS = "analysis"; 00030 public static final String TRANSLATING_SPECS = "translatingSpecs"; 00031 public static final String CREATING_BOUNDS = "creatingBounds"; 00032 public static final String CREATING_KK_BOUNDS = "creatingKKBounds"; 00033 public static final String RESTORING_HEAP = "restoringHeap"; 00034 public static final String RESTORING_SF = "restoringSpecFields"; 00035 public static final String TRAVERSING_HEAP = "traversingHeap"; 00036 public static final String CREATING_KK_UNIV = "creatingKKUniverse"; 00037 public static final String CREATING_FRESH_OBJECTS = "creatingFreshObjects"; 00038 public static final String CONVERTING_METHOD = "convertingMethod"; 00039 public static final String LOADING_JAVA_SCENE = "loadingJavaScene"; 00040 00041 public static final String TRANSLATING_TO_KODKOD = "translatingToKodkod"; 00042 public static final String TRANSLATING_TO_CNF = "translatingToCNF"; 00043 public static final String TRANSLATING_TO_BOOLEAN = "translatingToBoolean"; 00044 public static final String TRANSOFMING_PROCEDURE = "transofmingProcedure"; 00045 public static final String SOLVING_CNF = "solvingCNF"; 00046 public static final String SOLVING_ANALYSIS = "solvingAnalysis"; 00047 public static final String SCOLEMIZING = "scolemizing"; 00048 public static final String OPTIMIZING_BOUNDS_AND_FORMULA = "optimizingBoundsAndFormula"; 00049 public static final String GENERATING_SBP = "generatingSBP"; 00050 public static final String FLATTENING = "flattening"; 00051 public static final String DETECTING_SYMMETRIES = "detectingSymmetries"; 00052 public static final String DETECTED_SYMMETRIES = "detectedSymmetries"; 00053 00054 public static final SquanderReporter INSTANCE = new SquanderReporter(); 00055 00056 private Map<String, Long> times = new LinkedHashMap<String, Long>(); 00057 00058 private long sTime; 00059 private String task; 00060 private boolean busy; 00061 00062 private void start(String task) { 00063 Log.log("^^^ started: " + task); 00064 this.sTime = System.currentTimeMillis(); 00065 this.task = task; 00066 this.busy = true; 00067 } 00068 00069 public void end() { 00070 if (!busy) return; 00071 long dt = System.currentTimeMillis() - sTime; 00072 times.put(task, dt); 00073 this.busy = false; 00074 Log.log("~~~ done: %s (%ss)", task, dt/1000.0); 00075 } 00076 00077 private kodkod.engine.config.Reporter kkRep; 00078 public kodkod.engine.config.Reporter kkReporter() { 00079 if (kkRep == null) { 00080 Field f = ReflectionUtils.getField(getClass(), "kkReporter"); 00081 kkRep = (kodkod.engine.config.Reporter) ReflectionUtils.getFieldValue(this, f); 00082 } 00083 return kkRep; 00084 } 00085 00086 public void loadingJavaScene() { end(); start(LOADING_JAVA_SCENE); } 00087 public void convertingMethod() { end(); start(CONVERTING_METHOD); } 00088 public void creatingFreshObjects() { end(); start(CREATING_FRESH_OBJECTS); } 00089 public void traversingHeap() { end(); start(TRAVERSING_HEAP); } 00090 public void creatingBounds() { end(); start(CREATING_BOUNDS); } 00091 public void translatingSpecs() { end(); start(TRANSLATING_SPECS); } 00092 public void creatingKodkodUniverse() { end(); start(CREATING_KK_UNIV); } 00093 public void creatingKodkodBounds() { end(); start(CREATING_KK_BOUNDS); } 00094 public void restoringJavaHeap() { end(); start(RESTORING_HEAP); } 00095 public void restoringSpecFields() { end(); start(RESTORING_SF); } 00096 public void startedAnalysis() { end(); start(ANALYSIS); } 00097 public void packagingAnalysis() { end(); start(PACKAGIN_ANALYSIS); } 00098 public void translatingForge() { end(); start(TRANSLATING_FORGE); } 00099 public void buildingAnalysis() { end(); start(BUILDING_ANALYSIS); } 00100 public void finishedAnalysis() { end(); } 00101 00102 @Override 00103 public void detectedSymmetries(Set<?> parts) { 00104 end(); 00105 start(DETECTED_SYMMETRIES); 00106 } 00107 00108 @Override 00109 public void detectingSymmetries(Object bounds) { 00110 end(); 00111 start(DETECTING_SYMMETRIES); 00112 } 00113 00114 @Override 00115 public void flattening(Object circuit) { 00116 end(); 00117 start(FLATTENING); 00118 } 00119 00120 @Override 00121 public void generatingSBP() { 00122 end(); 00123 start(GENERATING_SBP); 00124 } 00125 00126 @Override 00127 public void optimizingBoundsAndFormula() { 00128 end(); 00129 start(OPTIMIZING_BOUNDS_AND_FORMULA); 00130 } 00131 00132 @Override 00133 public void skolemizing(Object decl, Object skolem, List<?> context) { 00134 end(); 00135 start(SCOLEMIZING); 00136 } 00137 00138 @Override 00139 public void solvingAnalysis() { 00140 end(); 00141 start(SOLVING_ANALYSIS); 00142 } 00143 00144 @Override 00145 public void solvingCNF(int primaryVars, int vars, int clauses) { 00146 end(); 00147 start(SOLVING_CNF); 00148 } 00149 00150 @Override 00151 public void transformingProcedure() { 00152 end(); 00153 start(TRANSOFMING_PROCEDURE); 00154 } 00155 00156 @Override 00157 public void translatingToBoolean(Object formula, Object bounds) { 00158 end(); 00159 start(TRANSLATING_TO_BOOLEAN); 00160 } 00161 00162 @Override 00163 public void translatingToCNF(Object circuit) { 00164 end(); 00165 start(TRANSLATING_TO_CNF); 00166 } 00167 00168 @Override 00169 public void translatingToKodkod() { 00170 end(); 00171 start(TRANSLATING_TO_KODKOD); 00172 } 00173 00174 public long getTaskTime(String task) { 00175 return times.get(task); 00176 } 00177 00178 @Override 00179 public String toString() { 00180 StringBuilder sb = new StringBuilder(); 00181 for (String task : times.keySet()) { 00182 Long t = times.get(task); 00183 sb.append(String.format("## task_%s: %d seconds %d milliseconds", task, t/1000, t%1000)); 00184 sb.append("\n"); 00185 } 00186 return sb.toString(); 00187 } 00188 00189 private SquanderReporter() {} 00190 00191 }