| 1 | package tuffy.util; |
| 2 | |
| 3 | import java.io.FileInputStream; |
| 4 | import java.io.FileNotFoundException; |
| 5 | import java.io.FileOutputStream; |
| 6 | import java.io.PrintStream; |
| 7 | import java.lang.management.ManagementFactory; |
| 8 | import java.util.Hashtable; |
| 9 | |
| 10 | import org.antlr.runtime.ANTLRInputStream; |
| 11 | import org.antlr.runtime.CommonTokenStream; |
| 12 | import org.kohsuke.args4j.CmdLineException; |
| 13 | import org.kohsuke.args4j.CmdLineParser; |
| 14 | |
| 15 | import tuffy.parse.CommandOptions; |
| 16 | import tuffy.parse.ConfigLexer; |
| 17 | import tuffy.parse.ConfigParser; |
| 18 | |
| 19 | /** |
| 20 | * Container of user-interface utilities. |
| 21 | */ |
| 22 | public class UIMan { |
| 23 | |
| 24 | protected static boolean silent = false; |
| 25 | protected static boolean silentErr = false; |
| 26 | |
| 27 | |
| 28 | public static void setSilentErr(boolean v){ |
| 29 | silentErr = v; |
| 30 | } |
| 31 | |
| 32 | public static void setSilent(boolean v){ |
| 33 | silent = v; |
| 34 | } |
| 35 | |
| 36 | public static void println(String... strings){ |
| 37 | if(silent) return; |
| 38 | if(Config.console_line_header != null){ |
| 39 | System.out.print("@" + Config.console_line_header + " "); |
| 40 | } |
| 41 | for(String s : strings){ |
| 42 | System.out.print(s); |
| 43 | writeToDribbleFile(s); |
| 44 | } |
| 45 | System.out.println(); |
| 46 | writeToDribbleFile("\n"); |
| 47 | } |
| 48 | |
| 49 | public static void print(String... strings){ |
| 50 | if(silent) return; |
| 51 | for(String s : strings){ |
| 52 | System.out.print(s); |
| 53 | writeToDribbleFile(s); |
| 54 | } |
| 55 | } |
| 56 | |
| 57 | public static void warn(String... strings){ |
| 58 | if(silentErr) return; |
| 59 | System.err.print("WARNING: "); |
| 60 | writeToDribbleFile("WARNING: "); |
| 61 | for(String s : strings){ |
| 62 | System.err.print(s); |
| 63 | } |
| 64 | System.err.println(); |
| 65 | writeToDribbleFile("\n"); |
| 66 | } |
| 67 | |
| 68 | public static void error(String... strings){ |
| 69 | if(silentErr) return; |
| 70 | System.err.print("ERROR: "); |
| 71 | writeToDribbleFile("ERROR: "); |
| 72 | for(String s : strings){ |
| 73 | System.err.print(s); |
| 74 | } |
| 75 | System.err.println(); |
| 76 | writeToDribbleFile("\n"); |
| 77 | } |
| 78 | |
| 79 | |
| 80 | private static PrintStream dribbleStream = null; |
| 81 | public static String dribbleFileName = null; |
| 82 | |
| 83 | public static void writeToDribbleFile(String str) { |
| 84 | if (dribbleStream != null) { |
| 85 | dribbleStream.print(str); |
| 86 | } |
| 87 | } |
| 88 | |
| 89 | public static void closeDribbleFile() { |
| 90 | dribbleFileName = null; |
| 91 | if (dribbleStream == null) { return; } |
| 92 | dribbleStream.close(); |
| 93 | dribbleStream = null; |
| 94 | } |
| 95 | |
| 96 | /* |
| 97 | public static void createDribbleFile(String fileName) { |
| 98 | // Utils.waitHere("createDribbleFile: " + fileName); |
| 99 | if (dribbleStream != null) { |
| 100 | dribbleStream.println("\n\n// Closed by a createDribble call with file = " + fileName); |
| 101 | } |
| 102 | createDribbleFile(fileName, false); |
| 103 | } |
| 104 | */ |
| 105 | |
| 106 | public static void createDribbleFile(String fileName) { |
| 107 | closeDribbleFile(); |
| 108 | try { |
| 109 | FileOutputStream outStream = new FileOutputStream(fileName); |
| 110 | dribbleStream = new PrintStream(outStream, false); // No auto-flush (can slow down code). |
| 111 | dribbleFileName = fileName; |
| 112 | } catch (FileNotFoundException e) { |
| 113 | e.printStackTrace(); |
| 114 | System.err.println("Unable to open file for logging:\n " + fileName + ".\nError message: " + e.getMessage()); |
| 115 | } |
| 116 | } |
| 117 | |
| 118 | public static String comma(int value) { // Always use separators (e.g., "100,000"). |
| 119 | return String.format("%,d", value); |
| 120 | } |
| 121 | public static String comma(long value) { |
| 122 | return String.format("%,d", value); |
| 123 | } |
| 124 | public static String comma(double value) { |
| 125 | return String.format("%,.3f", value); |
| 126 | } |
| 127 | |
| 128 | |
| 129 | public static String decimalRound(int digits, double num){ |
| 130 | return String.format("%." + digits + "f", num); |
| 131 | } |
| 132 | |
| 133 | public static CommandOptions processOptions(CommandOptions opt){ |
| 134 | |
| 135 | if(opt.pathConf != null){ |
| 136 | Config.path_conf = opt.pathConf; |
| 137 | } |
| 138 | boolean okconf = UIMan.parseConfigFile(Config.path_conf); |
| 139 | //if(!okconf){ |
| 140 | // return null; |
| 141 | //} |
| 142 | |
| 143 | Config.soft_evidence_activation_threshold = opt.softT; |
| 144 | |
| 145 | Config.snapshot_mode = opt.snapshot; |
| 146 | |
| 147 | Config.mcsat_sample_para = opt.mcsatPara; |
| 148 | Config.avoid_breaking_hard_clauses = opt.avoidBreakingHardClauses; |
| 149 | Config.output_prolog_format = opt.outputProlog; |
| 150 | |
| 151 | Config.max_threads = opt.maxThreads; |
| 152 | //Config.use_atom_blocking = opt.block; |
| 153 | |
| 154 | Config.evidDBSchema = opt.evidDBSchema; |
| 155 | Config.dbNeedTranslate = opt.dbNeedTranslate; |
| 156 | |
| 157 | Config.disable_partition = opt.disablePartition; |
| 158 | Config.output_files_in_gzip = opt.outputGz; |
| 159 | if(Config.output_files_in_gzip && !opt.fout.toLowerCase().endsWith(".gz")){ |
| 160 | opt.fout += ".gz"; |
| 161 | } |
| 162 | |
| 163 | Config.mcsatDumpPeriodSeconds = opt.mcsatDumpPeriodSec; |
| 164 | Config.timeout = opt.timeout; |
| 165 | |
| 166 | Config.marginal_output_min_prob = opt.minProb; |
| 167 | /* |
| 168 | if(opt.timeout > 0){ |
| 169 | Config.timeout = opt.timeout; |
| 170 | } |
| 171 | */ |
| 172 | Config.dir_out = FileMan.getParentDir(opt.fout); |
| 173 | Config.file_stats = opt.fout + ".stats"; |
| 174 | //Config.file_stats = Config.dir_out + "/tuffy_stats.txt"; |
| 175 | |
| 176 | /* |
| 177 | if(opt.reportingFreq > 0 && opt.marginal == false){ |
| 178 | Config.num_tries_per_periodic_flush = opt.reportingFreq; |
| 179 | } |
| 180 | |
| 181 | */ |
| 182 | Config.mark_all_atoms_active = opt.activateAllAtoms; |
| 183 | Config.keep_db_data = opt.keepData; |
| 184 | |
| 185 | Config.console_line_header = opt.consoleLineHeader; |
| 186 | |
| 187 | if(opt.fDribble != null){ |
| 188 | createDribbleFile(opt.fDribble); |
| 189 | } |
| 190 | |
| 191 | if(opt.fquery == null && opt.queryAtoms == null){ |
| 192 | System.err.println("Please specify queries with -q or -queryFiles"); |
| 193 | return null; |
| 194 | } |
| 195 | |
| 196 | Config.verbose_level = opt.verboseLevel; |
| 197 | |
| 198 | return opt; |
| 199 | |
| 200 | } |
| 201 | |
| 202 | public static CommandOptions parseCommand(String[] args){ |
| 203 | CommandOptions opt = new CommandOptions(); |
| 204 | CmdLineParser parser = new CmdLineParser(opt); |
| 205 | try{ |
| 206 | parser.parseArgument(args); |
| 207 | if(opt.showHelp){ |
| 208 | UIMan.println("USAGE:"); |
| 209 | parser.printUsage(System.out); |
| 210 | return null; |
| 211 | } |
| 212 | }catch(CmdLineException e){ |
| 213 | System.err.println(e.getMessage()); |
| 214 | UIMan.println("USAGE:"); |
| 215 | parser.printUsage(System.out); |
| 216 | return null; |
| 217 | } |
| 218 | |
| 219 | return processOptions(opt); |
| 220 | } |
| 221 | |
| 222 | public static boolean parseConfigFile(String fconf){ |
| 223 | try { |
| 224 | FileInputStream fis = null; |
| 225 | try{ |
| 226 | fis = new FileInputStream(fconf); |
| 227 | }catch(Exception e){ |
| 228 | System.out.println("Failed to open config file."); |
| 229 | System.err.println(e.getMessage()); |
| 230 | return false; |
| 231 | } |
| 232 | ANTLRInputStream input = new ANTLRInputStream(fis); |
| 233 | ConfigLexer lexer = new ConfigLexer(input); |
| 234 | CommonTokenStream tokens = new CommonTokenStream(lexer); |
| 235 | ConfigParser parser = new ConfigParser(tokens); |
| 236 | try{ |
| 237 | parser.config(); |
| 238 | }catch(Exception e){ |
| 239 | System.out.println("Ill-formed config file: " + fconf); |
| 240 | System.err.println(e.getMessage()); |
| 241 | return false; |
| 242 | } |
| 243 | Hashtable<String, String> map = parser.map; |
| 244 | String value; |
| 245 | |
| 246 | value = map.get("db_url"); |
| 247 | if(value == null){ |
| 248 | ExceptionMan.die("missing db_url in config file " + fconf); |
| 249 | }else{ |
| 250 | Config.db_url = value.trim(); |
| 251 | } |
| 252 | |
| 253 | value = map.get("db_username"); |
| 254 | if(value == null){ |
| 255 | //Config.db_username = "tuffer"; |
| 256 | ExceptionMan.die("missing db_username in config file " + fconf); |
| 257 | }else{ |
| 258 | Config.db_username = value.trim(); |
| 259 | } |
| 260 | |
| 261 | value = map.get("db_password"); |
| 262 | if(value == null){ |
| 263 | //Config.db_password = "tuffer"; |
| 264 | ExceptionMan.die("missing db_password in config file " + fconf); |
| 265 | }else{ |
| 266 | Config.db_password = value.trim(); |
| 267 | } |
| 268 | |
| 269 | value = map.get("dir_working"); |
| 270 | if(value != null){ |
| 271 | Config.dir_working = value.trim().replace('\\', '/'); |
| 272 | } |
| 273 | String pid = ManagementFactory.getRuntimeMXBean().getName().split("@")[0]; |
| 274 | String user = System.getProperty("user.name").toLowerCase().replaceAll("\\W", "_"); |
| 275 | String machine = java.net.InetAddress.getLocalHost().getHostName().toLowerCase().replaceAll("\\W", "_"); |
| 276 | |
| 277 | String prod = Config.product_line; |
| 278 | Config.dir_working += "/" + prod + "_" + machine + "_" + user + "_" + pid; |
| 279 | |
| 280 | if(Config.evidDBSchema == null){ |
| 281 | Config.db_schema = prod + "_" + machine + "_" + user + "_" + pid; |
| 282 | }else{ |
| 283 | Config.db_schema = Config.evidDBSchema; |
| 284 | } |
| 285 | |
| 286 | String curDir = System.getProperty("user.dir"); |
| 287 | |
| 288 | |
| 289 | println("Database schema = " + Config.db_schema); |
| 290 | println("Current directory = " + curDir); |
| 291 | println("Temporary directory = " + Config.dir_working); |
| 292 | |
| 293 | } catch (Exception e) { |
| 294 | e.printStackTrace(); |
| 295 | return false; |
| 296 | } |
| 297 | return true; |
| 298 | |
| 299 | } |
| 300 | |
| 301 | public static void verbose(int level, String s){ |
| 302 | if(Config.verbose_level >= level){ |
| 303 | println(s); |
| 304 | } |
| 305 | } |
| 306 | |
| 307 | |
| 308 | public static void verboseInline(int level, String s){ |
| 309 | if(Config.verbose_level >= level){ |
| 310 | print(s); |
| 311 | } |
| 312 | } |
| 313 | |
| 314 | |
| 315 | |
| 316 | |
| 317 | |
| 318 | |
| 319 | |
| 320 | } |