00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include <clasp/cli/clasp_output.h>
00021 #include <clasp/solver.h>
00022 #include <clasp/satelite.h>
00023 #include <clasp/minimize_constraint.h>
00024 #include <clasp/util/timer.h>
00025 #include <stdio.h>
00026 #include <stdarg.h>
00027 #include <string.h>
00028 #include <climits>
00029 #include <string>
00030 #include <cstdlib>
00031 #if !defined(_WIN32)
00032 #include <signal.h>
00033 #elif !defined(SIGALRM)
00034 #define SIGALRM 14
00035 #endif
00036 namespace Clasp { namespace Cli {
00038
00040 static void null_term_copy(const char* in, int inSize, char* buf, uint32 bufSize) {
00041 if (!in || !buf || !bufSize) return;
00042 uint32 n = inSize < 0 ? static_cast<uint32>(0) : std::min(bufSize-1, static_cast<uint32>(inSize));
00043 std::memcpy(buf, in, n);
00044 buf[n] = 0;
00045 }
00046 void format(const Clasp::BasicSolveEvent& ev, char* out, uint32 outSize) {
00047 char buf[1024]; int n;
00048 const Solver& s = *ev.solver;
00049 n = sprintf(buf, "%2u:%c|%7u/%-7u|%8u/%-8u|%10" PRIu64"/%-6.3f|%8" PRId64"/%-10" PRId64"|"
00050 , s.id()
00051 , static_cast<char>(ev.op)
00052 , s.numFreeVars()
00053 , (s.decisionLevel() > 0 ? s.levelStart(1) : s.numAssignedVars())
00054 , s.numConstraints()
00055 , s.numLearntConstraints()
00056 , s.stats.conflicts
00057 , s.stats.conflicts/std::max(1.0,double(s.stats.choices))
00058 , ev.cLimit <= (UINT32_MAX) ? (int64)ev.cLimit:-1
00059 , ev.lLimit != (UINT32_MAX) ? (int64)ev.lLimit:-1
00060 );
00061 null_term_copy(buf, n, out, outSize);
00062 }
00063 void format(const Clasp::SolveTestEvent& ev, char* out, uint32 outSize) {
00064 char buf[1024]; int n;
00065 char ct = ev.partial ? 'P' : 'F';
00066 if (ev.result == -1) { n = sprintf(buf, "%2u:%c| HC: %-5u %-60s|", ev.solver->id(), ct, ev.scc, "..."); }
00067 else {
00068 n = sprintf(buf, "%2u:%c| HC: %-5u %-4s|%8u/%-8u|%10" PRIu64"/%-6.3f| T: %-15.3f|", ev.solver->id(), ct, ev.scc, (ev.result == 1 ? "OK" : "FAIL")
00069 , ev.solver->numConstraints()
00070 , ev.solver->numLearntConstraints()
00071 , ev.conflicts()
00072 , ev.conflicts()/std::max(1.0,double(ev.choices()))
00073 , ev.time
00074 );
00075 }
00076 null_term_copy(buf, n, out, outSize);
00077 }
00078 #if WITH_THREADS
00079 void format(const Clasp::mt::MessageEvent& ev, char* out, uint32 outSize) {
00080 typedef Clasp::mt::MessageEvent EV;
00081 char buf[1024]; int n;
00082 if (ev.op != EV::completed) { n = sprintf(buf, "%2u:X| %-15s %-53s |", ev.solver->id(), ev.msg, ev.op == EV::sent ? "sent" : "received"); }
00083 else { n = sprintf(buf, "%2u:X| %-15s %-33s after %12.3fs |", ev.solver->id(), ev.msg, "completed", ev.time); }
00084 null_term_copy(buf, n, out, outSize);
00085 }
00086 #endif
00087
00088
00090 Output::Output(uint32 verb) : summary_(0), verbose_(0), hidePref_(0) {
00091 std::memset(quiet_, 0, sizeof(quiet_));
00092 setCallQuiet(print_no);
00093 setVerbosity(verb);
00094 }
00095 Output::~Output() {}
00096 void Output::setVerbosity(uint32 verb) {
00097 verbose_ = verb;
00098 Event::Verbosity x = (Event::Verbosity)std::min(verb, (uint32)Event::verbosity_max);
00099 EventHandler::setVerbosity(Event::subsystem_facade , x);
00100 EventHandler::setVerbosity(Event::subsystem_load , x);
00101 EventHandler::setVerbosity(Event::subsystem_prepare, x);
00102 EventHandler::setVerbosity(Event::subsystem_solve , x);
00103 }
00104 void Output::setModelQuiet(PrintLevel model){ quiet_[0] = static_cast<uint8>(model); }
00105 void Output::setOptQuiet(PrintLevel opt) { quiet_[1] = static_cast<uint8>(opt); }
00106 void Output::setCallQuiet(PrintLevel call) { quiet_[2] = static_cast<uint8>(call); }
00107 void Output::setHide(char c) { hidePref_ = c; }
00108
00109 void Output::saveModel(const Model& m) {
00110 vals_ = *m.values;
00111 saved_ = m;
00112 saved_.values = &vals_;
00113 }
00114
00115 void Output::onEvent(const Event& ev) {
00116 typedef ClaspFacade::StepStart StepStart;
00117 typedef ClaspFacade::StepReady StepReady;
00118 if (const StepStart* start = event_cast<StepStart>(ev)) {
00119 startStep(*start->facade);
00120 }
00121 else if (const StepReady* ready = event_cast<StepReady>(ev)) {
00122 stopStep(*ready->summary);
00123 }
00124 }
00125 bool Output::onModel(const Solver& s, const Model& m) {
00126 if (modelQ() == print_all || (optQ() == print_all && m.costs)) {
00127 printModel(s.symbolTable(), m, print_all);
00128 }
00129 if (modelQ() == print_best || (optQ() == print_best && m.costs)) {
00130 if (m.opt == 1 && !m.consequences()) { printModel(s.symbolTable(), m, print_best); clearModel(); }
00131 else { saveModel(m); }
00132 }
00133 return true;
00134 }
00135 void Output::startStep(const ClaspFacade&) { clearModel(); summary_ = 0; }
00136 void Output::stopStep(const ClaspFacade::Summary& s){
00137 if (getModel()) {
00138 printModel(s.ctx().symbolTable(), *getModel(), print_best);
00139 clearModel();
00140 }
00141 if (callQ() == print_all) {
00142 printSummary(s, false);
00143 if (s.stats()) { printStatistics(s, false); }
00144 }
00145 else if (callQ() == print_best) {
00146 summary_ = &s;
00147 }
00148 }
00149 void Output::shutdown(const ClaspFacade::Summary& summary) {
00150 if (summary_) {
00151 printSummary(*summary_, false);
00152 if (summary_->stats()) { printStatistics(*summary_, false); }
00153 }
00154 printSummary(summary, true);
00155 if (summary.stats()) { printStatistics(summary, true); }
00156 shutdown();
00157 }
00159
00161 StatsVisitor::~StatsVisitor() {}
00162 void StatsVisitor::accuStats(const SharedContext& ctx, SolverStats& out) const {
00163 for (uint32 i = 0; ctx.hasSolver(i); ++i) {
00164 const SolverStats& x = ctx.stats(*ctx.solver(i), accu);
00165 out.enableStats(x);
00166 out.accu(x);
00167 }
00168 }
00169 void StatsVisitor::visitStats(const SharedContext& ctx, const Asp::LpStats* lp, bool accu) {
00170 this->accu = accu;
00171 SolverStats stats;
00172 accuStats(ctx, stats);
00173 visitSolverStats(stats, true);
00174 visitProblemStats(ctx.stats(), lp);
00175 if (stats.level() > 1) {
00176 if (ctx.hasSolver(1)) { visitThreads(ctx); }
00177 if (ctx.sccGraph.get() && ctx.sccGraph->numNonHcfs()) { visitHccs(ctx); }
00178 }
00179 }
00180 void StatsVisitor::visitProblemStats(const Clasp::ProblemStats& stats, const Clasp::Asp::LpStats* lp) {
00181 if (lp) { visitLogicProgramStats(*lp); }
00182 visitProblemStats(stats);
00183 }
00184
00185 void StatsVisitor::visitSolverStats(const Clasp::SolverStats& stats, bool accu) {
00186 ExtendedStats e;
00187 const ExtendedStats* ext = stats.extra ? stats.extra : &e;
00188 visitCoreSolverStats(ext->cpuTime, ext->models, stats, accu);
00189 if (stats.extra) { visitExtSolverStats(*stats.extra, accu); }
00190 if (stats.jumps) { visitJumpStats(*stats.jumps, accu); }
00191 }
00192
00193 void StatsVisitor::visitThreads(const SharedContext& ctx) {
00194 for (uint32 i = 0; ctx.hasSolver(i); ++i) {
00195 const SolverStats& x = ctx.stats(*ctx.solver(i), accu);
00196 visitThread(i, x);
00197 }
00198 }
00199 void StatsVisitor::visitHccs(const SharedContext& ctx) {
00200 if (const SharedDependencyGraph* g = ctx.sccGraph.get()) {
00201 for (uint32 i = 0; i != g->numNonHcfs(); ++i) {
00202 visitHcc(i, (g->nonHcfBegin() + i)->second->ctx());
00203 }
00204 }
00205 }
00206 void StatsVisitor::visitHcc(uint32, const SharedContext& ctx) {
00207 SolverStats stats;
00208 accuStats(ctx, stats);
00209 visitProblemStats(ctx.stats(), 0);
00210 visitSolverStats(stats, false);
00211 }
00213
00215 JsonOutput::JsonOutput(uint32 v) : Output(std::min(v, uint32(1))), open_("") {
00216 objStack_.reserve(10);
00217 }
00218 JsonOutput::~JsonOutput() { JsonOutput::shutdown(); }
00219 void JsonOutput::run(const char* solver, const char* version, const std::string* iBeg, const std::string* iEnd) {
00220 if (indent() == 0) {
00221 open_ = "";
00222 JsonOutput::pushObject();
00223 }
00224 printKeyValue("Solver", std::string(solver).append(" version ").append(version).c_str());
00225 pushObject("Input", type_array);
00226 printf("%-*s", indent(), " ");
00227 for (const char* sep = ""; iBeg != iEnd; ++iBeg, sep = ",") {
00228 printString(iBeg->c_str(), sep);
00229 }
00230 popObject();
00231 pushObject("Call", type_array);
00232 }
00233 void JsonOutput::shutdown(const ClaspFacade::Summary& summary) {
00234 while (!objStack_.empty() && *objStack_.rbegin() == '[') {
00235 popObject();
00236 }
00237 Output::shutdown(summary);
00238 }
00239
00240 void JsonOutput::shutdown() {
00241 if (!objStack_.empty()) {
00242 do { popObject(); } while (!objStack_.empty());
00243 printf("\n");
00244 }
00245 fflush(stdout);
00246 }
00247 void JsonOutput::startStep(const ClaspFacade& f) {
00248 Output::startStep(f);
00249 pushObject(0, type_object);
00250 }
00251 void JsonOutput::stopStep(const ClaspFacade::Summary& s) {
00252 assert(!objStack_.empty());
00253 Output::stopStep(s);
00254 while (popObject() != '{') { ; }
00255 }
00256
00257 void JsonOutput::visitCoreSolverStats(double cpuTime, uint64 models, const SolverStats& st, bool) {
00258 pushObject("Core");
00259 printKeyValue("CPU Time" , cpuTime);
00260 printKeyValue("Models" , models);
00261 printKeyValue("Choices" , st.choices);
00262 printKeyValue("Conflicts" , st.conflicts);
00263 printKeyValue("Backtracks" , st.backtracks());
00264 printKeyValue("Backjumps" , st.backjumps());
00265 printKeyValue("Restarts" , st.restarts);
00266 printKeyValue("RestartAvg" , st.avgRestart());
00267 printKeyValue("RestartLast", st.lastRestart);
00268 popObject();
00269 }
00270
00271 void JsonOutput::visitExtSolverStats(const ExtendedStats& stx, bool accu) {
00272 pushObject("More");
00273 if (stx.domChoices) {
00274 printKeyValue("DomChoices", stx.domChoices);
00275 }
00276 if (stx.hccTests) {
00277 pushObject("StabTests");
00278 printKeyValue("Sum", stx.hccTests);
00279 printKeyValue("Full", stx.hccTests - stx.hccPartial);
00280 printKeyValue("Partial", stx.hccPartial);
00281 popObject();
00282 }
00283 if (stx.models) {
00284 printKeyValue("AvgModel", stx.avgModel());
00285 }
00286 printKeyValue("Splits", stx.splits);
00287 printKeyValue("Problems", stx.gps);
00288 printKeyValue("AvgGPLength", stx.avgGp());
00289 pushObject("Lemma");
00290 printKeyValue("Sum", stx.lemmas());
00291 printKeyValue("Deleted" , stx.deleted);
00292 pushObject("Type", type_array);
00293 const char* names[] = {"Short", "Conflict", "Loop", "Other"};
00294 for (int i = Constraint_t::static_constraint; i <= Constraint_t::learnt_other; ++i) {
00295 pushObject();
00296 printKeyValue("Type", names[i]);
00297 if (i == 0) {
00298 printKeyValue("Sum", stx.binary+stx.ternary);
00299 printKeyValue("Ratio", percent(stx.binary+stx.ternary, stx.lemmas()));
00300 printKeyValue("Binary", stx.binary);
00301 printKeyValue("Ternary", stx.ternary);
00302 }
00303 else {
00304 printKeyValue("Sum", stx.lemmas(ConstraintType(i)));
00305 printKeyValue("AvgLen", stx.avgLen(ConstraintType(i)));
00306 }
00307 popObject();
00308 }
00309 popObject();
00310 popObject();
00311 if (stx.distributed || stx.integrated) {
00312 pushObject("Distribution");
00313 printKeyValue("Distributed", stx.distributed);
00314 printKeyValue("Ratio", stx.distRatio());
00315 printKeyValue("AvgLbd", stx.avgDistLbd());
00316 popObject();
00317 pushObject("Integration");
00318 printKeyValue("Integrated", stx.integrated);
00319 printKeyValue("Units", stx.intImps);
00320 printKeyValue("AvgJump", stx.avgIntJump());
00321 if (accu) { printKeyValue("Ratio", stx.intRatio()); }
00322 popObject();
00323 }
00324 popObject();
00325 }
00326 void JsonOutput::visitJumpStats(const JumpStats& st, bool) {
00327 pushObject("Jumps");
00328 printKeyValue("Sum", st.jumps);
00329 printKeyValue("Max", st.maxJump);
00330 printKeyValue("MaxExec", st.maxJumpEx);
00331 printKeyValue("Avg", st.avgJump());
00332 printKeyValue("AvgExec", st.avgJumpEx());
00333 printKeyValue("Levels", st.jumpSum);
00334 printKeyValue("LevelsExec", st.jumped());
00335 pushObject("Bounded");
00336 printKeyValue("Sum", st.bounded);
00337 printKeyValue("Max", st.maxBound);
00338 printKeyValue("Avg", st.avgBound());
00339 printKeyValue("Levels", st.boundSum);
00340 popObject();
00341 popObject();
00342 }
00343 void JsonOutput::visitLogicProgramStats(const Asp::LpStats& lp) {
00344 using namespace Asp;
00345 pushObject("LP");
00346 printKeyValue("Atoms", lp.atoms);
00347 if (lp.auxAtoms) { printKeyValue("AuxAtoms", lp.auxAtoms); }
00348 pushObject("Rules");
00349 printKeyValue("Sum", lp.rules());
00350 char buf[10];
00351 LpStats::RPair r;
00352 for (RuleType i = BASICRULE; i != ENDRULE; ++i) {
00353 r = lp.rules(i);
00354 if (r.first) {
00355 sprintf(buf, "R%u", i);
00356 printKeyValue(buf, r.first);
00357 }
00358 }
00359 r = lp.rules(BASICRULE);
00360 if (lp.tr()) {
00361 printKeyValue("Created", r.second - r.first);
00362 pushObject("Translated");
00363 for (RuleType i = BASICRULE; ++i != ENDRULE;) {
00364 r = lp.rules(i);
00365 if (r.first > 0) {
00366 sprintf(buf, "R%u", i);
00367 printKeyValue(buf, r.first-r.second);
00368 }
00369 }
00370 popObject();
00371 }
00372 popObject();
00373 printKeyValue("Bodies", lp.bodies);
00374 if (lp.sccs == 0) { printKeyValue("Tight", "yes"); }
00375 else if (lp.sccs == PrgNode::noScc) { printKeyValue("Tight", "N/A"); }
00376 else {
00377 printKeyValue("Tight", "no");
00378 printKeyValue("SCCs", lp.sccs);
00379 printKeyValue("NonHcfs", lp.nonHcfs);
00380 printKeyValue("UfsNodes", lp.ufsNodes);
00381 printKeyValue("NonHcfGammas", lp.gammas);
00382 }
00383 pushObject("Equivalences");
00384 printKeyValue("Sum", lp.eqs());
00385 printKeyValue("Atom", lp.eqs(Var_t::atom_var));
00386 printKeyValue("Body", lp.eqs(Var_t::body_var));
00387 printKeyValue("Other", lp.eqs(Var_t::atom_body_var));
00388 popObject();
00389 popObject();
00390 }
00391 void JsonOutput::visitProblemStats(const ProblemStats& p) {
00392 pushObject("Problem");
00393 printKeyValue("Variables", p.vars);
00394 printKeyValue("Eliminated", p.vars_eliminated);
00395 printKeyValue("Frozen", p.vars_frozen);
00396 pushObject("Constraints");
00397 uint32 sum = p.constraints + p.constraints_binary + p.constraints_ternary;
00398 printKeyValue("Sum", sum);
00399 printKeyValue("Binary", p.constraints_binary);
00400 printKeyValue("Ternary", p.constraints_ternary);
00401 popObject();
00402 popObject();
00403 }
00404
00405 void JsonOutput::printKey(const char* k) {
00406 printf("%s%-*s\"%s\": ", open_, indent(), " ", k);
00407 open_ = ",\n";
00408 }
00409
00410 void JsonOutput::printString(const char* v, const char* sep) {
00411 assert(v);
00412 const uint32 BUF_SIZE = 1024;
00413 char buf[BUF_SIZE];
00414 uint32 n = 0;
00415 buf[n++] = '"';
00416 while (*v) {
00417 if (*v != '\\' && *v != '"') { buf[n++] = *v++; }
00418 else if (*v == '"' || !strchr("\"\\/\b\f\n\r\t", v[1])) { buf[n++] = '\\'; buf[n++] = *v++; }
00419 else { buf[n++] = v[0]; buf[n++] = v[1]; v += 2; }
00420 if (n > BUF_SIZE - 2) { buf[n] = 0; printf("%s%s", sep, buf); n = 0; sep = ""; }
00421 }
00422 buf[n] = 0;
00423 printf("%s%s\"", sep, buf);
00424 }
00425
00426 void JsonOutput::printKeyValue(const char* k, const char* v) {
00427 printf("%s%-*s\"%s\": ", open_, indent(), " ", k);
00428 printString(v,"");
00429 open_ = ",\n";
00430 }
00431 void JsonOutput::printKeyValue(const char* k, uint64 v) {
00432 printf("%s%-*s\"%s\": %" PRIu64, open_, indent(), " ", k, v);
00433 open_ = ",\n";
00434 }
00435 void JsonOutput::printKeyValue(const char* k, uint32 v) { return printKeyValue(k, uint64(v)); }
00436 void JsonOutput::printKeyValue(const char* k, double v) {
00437 printf("%s%-*s\"%s\": %.3f", open_, indent(), " ", k, v);
00438 open_ = ",\n";
00439 }
00440
00441 void JsonOutput::pushObject(const char* k, ObjType t) {
00442 if (k) {
00443 printKey(k);
00444 }
00445 else {
00446 printf("%s%-*.*s", open_, indent(), indent(), " ");
00447 }
00448 char o = t == type_object ? '{' : '[';
00449 objStack_ += o;
00450 printf("%c\n", o);
00451 open_ = "";
00452 }
00453 char JsonOutput::popObject() {
00454 assert(!objStack_.empty());
00455 char o = *objStack_.rbegin();
00456 objStack_.erase(objStack_.size()-1);
00457 printf("\n%-*.*s%c", indent(), indent(), " ", o == '{' ? '}' : ']');
00458 open_ = ",\n";
00459 return o;
00460 }
00461 void JsonOutput::startModel() {
00462 if (!hasWitness()) {
00463 pushObject("Witnesses", type_array);
00464 }
00465 pushObject();
00466 }
00467
00468 void JsonOutput::printModel(const SymbolTable& index, const Model& m, PrintLevel x) {
00469 bool hasModel = false;
00470 if (x == modelQ()) {
00471 startModel();
00472 hasModel = true;
00473 pushObject("Value", type_array);
00474 const char* sep = "";
00475 printf("%-*s", indent(), " ");
00476 if (index.type() == SymbolTable::map_indirect) {
00477 for (SymbolTable::const_iterator it = index.begin(); it != index.end(); ++it) {
00478 if (m.value(it->second.lit.var()) == trueValue(it->second.lit) && doPrint(it->second)) {
00479 printString(it->second.name.c_str(), sep);
00480 sep = ", ";
00481 }
00482 }
00483 }
00484 else {
00485 for (Var v = 1; v < index.size(); ++v) {
00486 printf("%s%d", sep, (m.value(v) == value_false ? -static_cast<int>(v) : static_cast<int>(v)));
00487 sep = ", ";
00488 }
00489 }
00490 popObject();
00491 }
00492 if (x == optQ() && m.costs) {
00493 if (!hasModel) { startModel(); hasModel = true; }
00494 printCosts(*m.costs);
00495 }
00496 if (hasModel) { popObject(); }
00497 }
00498 void JsonOutput::printCosts(const SharedMinimizeData& opt) {
00499 pushObject("Costs", type_array);
00500 printf("%-*s", indent(), " ");
00501 const char* sep = "";
00502 for (uint32 i = 0, end = opt.numRules(); i != end; ++i) {
00503 printf("%s%" PRId64, sep, opt.optimum(i));
00504 sep = ", ";
00505 }
00506 popObject();
00507 }
00508
00509 void JsonOutput::printSummary(const ClaspFacade::Summary& run, bool final) {
00510 if (hasWitness()) { popObject(); }
00511 const char* res = "UNKNOWN";
00512 if (run.unsat()) { res = "UNSATISFIABLE"; }
00513 else if (run.sat()) { res = !run.optimum() ? "SATISFIABLE" : "OPTIMUM FOUND"; }
00514 printKeyValue("Result", res);
00515 if (verbosity()) {
00516 if (run.result.interrupted()){ printKeyValue(run.result.signal != SIGALRM ? "INTERRUPTED" : "TIME LIMIT", uint32(1)); }
00517 pushObject("Models");
00518 printKeyValue("Number", run.enumerated());
00519 printKeyValue("More" , run.complete() ? "no" : "yes");
00520 if (run.sat()) {
00521 if (run.consequences()){ printKeyValue(run.consequences(), run.complete() ? "yes":"unknown"); }
00522 if (run.optimize()) {
00523 printKeyValue("Optimum", run.optimum()?"yes":"unknown");
00524 printKeyValue("Optimal", run.optimal());
00525 printCosts(*run.costs());
00526 }
00527 }
00528 popObject();
00529 if (final) { printKeyValue("Calls", run.step + 1); }
00530 pushObject("Time");
00531 printKeyValue("Total", run.totalTime);
00532 printKeyValue("Solve", run.solveTime);
00533 printKeyValue("Model", run.satTime);
00534 printKeyValue("Unsat", run.unsatTime);
00535 printKeyValue("CPU" , run.cpuTime);
00536 popObject();
00537 if (run.ctx().concurrency() > 1) {
00538 printKeyValue("Threads", run.ctx().concurrency());
00539 printKeyValue("Winner", run.ctx().winner());
00540 }
00541 }
00542 }
00543 void JsonOutput::printStatistics(const ClaspFacade::Summary& summary, bool final) {
00544 if (hasWitness()) { popObject(); }
00545 pushObject("Stats", type_object);
00546 StatsVisitor::visitStats(summary.ctx(), summary.lpStats(), final && summary.step);
00547 popObject();
00548 }
00550
00552 #define printKeyValue(k, fmt, value) printf("%s%-*s: " fmt, format[cat_comment], width_, (k), (value))
00553 #define printLN(cat, fmt, ...) printf("%s" fmt "\n", format[cat], __VA_ARGS__)
00554 #define printBR(cat) printf("%s\n", format[cat])
00555 #define printKey(k) printf("%s%-*s: ", format[cat_comment], width_, (k))
00556 const char* const rowSep = "----------------------------------------------------------------------------|";
00557 const char* const finalSep = "=============================== Accumulation ===============================|";
00558
00559 static inline std::string prettify(const std::string& str) {
00560 if (str.size() < 40) return str;
00561 std::string t("...");
00562 t.append(str.end()-38, str.end());
00563 return t;
00564 }
00565 TextOutput::TextOutput(uint32 verbosity, Format f, const char* catAtom, char ifs) : Output(verbosity), stTime_(0.0), state_(0) {
00566 result[res_unknonw] = "UNKNOWN";
00567 result[res_sat] = "SATISFIABLE";
00568 result[res_unsat] = "UNSATISFIABLE";
00569 result[res_opt] = "OPTIMUM FOUND";
00570 format[cat_comment] = "";
00571 format[cat_value] = "";
00572 format[cat_objective] = "Optimization: ";
00573 format[cat_result] = "";
00574 format[cat_value_term] = "";
00575 format[cat_atom] = "%s";
00576 if (f == format_aspcomp) {
00577 format[cat_comment] = "% ";
00578 format[cat_value] = "ANSWER\n";
00579 format[cat_objective] = "COST ";
00580 format[cat_atom] = "%s.";
00581 result[res_sat] = "";
00582 result[res_unsat] = "INCONSISTENT";
00583 result[res_opt] = "OPTIMUM";
00584 setModelQuiet(print_best);
00585 setOptQuiet(print_best);
00586 }
00587 else if (f == format_sat09 || f == format_pb09) {
00588 format[cat_comment] = "c ";
00589 format[cat_value] = "v ";
00590 format[cat_objective] = "o ";
00591 format[cat_result] = "s ";
00592 format[cat_value_term]= "0";
00593 format[cat_atom] = "%d";
00594 if (f == format_pb09) {
00595 format[cat_value_term]= "";
00596 format[cat_atom] = "x%d";
00597 setModelQuiet(print_best);
00598 }
00599 }
00600 if (catAtom && *catAtom) {
00601 format[cat_atom] = catAtom;
00602 char ca = f == format_sat09 || f == format_pb09 ? 'd' : 's';
00603 while (*catAtom) {
00604 if (*catAtom == '\n'){ break; }
00605 else if (*catAtom == '%') {
00606 if (!*++catAtom) { ca = '%'; break; }
00607 else if (*catAtom == ca) { ca = 0; }
00608 else if (*catAtom != '%'){ break; }
00609 }
00610 ++catAtom;
00611 }
00612 CLASP_FAIL_IF(ca != 0 , "cat_atom: Invalid format string - format '%%%c' expected!", ca);
00613 CLASP_FAIL_IF(*catAtom == '\n', "cat_atom: Invalid format string - new line not allowed!");
00614 CLASP_FAIL_IF(*catAtom != 0 , "cat_atom: Invalid format string - '%%%c' too many arguments!", *catAtom);
00615 }
00616 ifs_[0] = ifs;
00617 ifs_[1] = 0;
00618 width_ = 13+(int)strlen(format[cat_comment]);
00619 ev_ = -1;
00620 }
00621 TextOutput::~TextOutput() {}
00622
00623 void TextOutput::comment(uint32 v, const char* fmt, ...) const {
00624 if (verbosity() >= v) {
00625 printf("%s", format[cat_comment]);
00626 va_list args;
00627 va_start(args, fmt);
00628 vfprintf(stdout, fmt, args);
00629 va_end(args);
00630 fflush(stdout);
00631 }
00632 }
00633
00634 void TextOutput::run(const char* solver, const char* version, const std::string* begInput, const std::string* endInput) {
00635 if (!version) version = "";
00636 if (solver) comment(1, "%s version %s\n", solver, version);
00637 if (begInput != endInput) {
00638 comment(1, "Reading from %s%s\n", prettify(*begInput).c_str(), (endInput - begInput) > 1 ? " ..." : "");
00639 }
00640 }
00641 void TextOutput::shutdown() {}
00642 void TextOutput::printSummary(const ClaspFacade::Summary& run, bool final) {
00643 if (final && callQ() != print_no){
00644 comment(1, "%s\n", finalSep);
00645 }
00646 const char* res = result[res_unknonw];
00647 if (run.unsat()) { res = result[res_unsat]; }
00648 else if (run.sat()) { res = !run.optimum() ? result[res_sat] : result[res_opt]; }
00649 if (std::strlen(res)) { printLN(cat_result, "%s", res); }
00650 if (verbosity() || run.stats()) {
00651 printBR(cat_comment);
00652 if (run.result.interrupted()){ printKeyValue((run.result.signal != SIGALRM ? "INTERRUPTED" : "TIME LIMIT"), "%u\n", uint32(1)); }
00653 printKey("Models");
00654 char buf[64];
00655 int wr = sprintf(buf, "%" PRIu64, run.enumerated());
00656 if (!run.complete()) { buf[wr++] = '+'; }
00657 buf[wr]=0;
00658 printf("%-6s\n", buf);
00659 if (run.sat()) {
00660 if (run.consequences()) { printLN(cat_comment, " %-*s: %s", width_-2, run.consequences(), (run.complete()?"yes":"unknown")); }
00661 if (run.costs()) { printKeyValue(" Optimum", "%s\n", run.optimum()?"yes":"unknown"); }
00662 if (run.optimize()) {
00663 if (run.optimal() > 1){ printKeyValue(" Optimal", "%" PRIu64"\n", run.optimal()); }
00664 printKey("Optimization");
00665 printCosts(*run.costs());
00666 printf("\n");
00667 }
00668 }
00669 if (final) { printKeyValue("Calls", "%u\n", run.step + 1); }
00670 printKey("Time");
00671 printf("%.3fs (Solving: %.2fs 1st Model: %.2fs Unsat: %.2fs)\n"
00672 , run.totalTime
00673 , run.solveTime
00674 , run.satTime
00675 , run.unsatTime);
00676 printKeyValue("CPU Time", "%.3fs\n", run.cpuTime);
00677 if (run.ctx().concurrency() > 1) {
00678 printKeyValue("Threads", "%-8u", run.ctx().concurrency());
00679 printf(" (Winner: %u)\n", run.ctx().winner());
00680 }
00681 }
00682 }
00683 void TextOutput::printStatistics(const ClaspFacade::Summary& run, bool final) {
00684 printBR(cat_comment);
00685 StatsVisitor::visitStats(run.ctx(), run.lpStats(), final && run.step);
00686 }
00687 void TextOutput::startStep(const ClaspFacade& f) {
00688 Output::startStep(f);
00689 if (callQ() != print_no) { comment(1, "%s\n", rowSep); comment(2, "%-13s: %d\n", "Call", f.step()+1); }
00690 }
00691 void TextOutput::onEvent(const Event& ev) {
00692 typedef SatElite::SatElite::Progress SatPre;
00693 if (ev.verb <= verbosity()) {
00694 if (ev.system == 0) { setState(0,0,0); }
00695 else if (ev.system == state_) {
00696 if (ev.system == Event::subsystem_solve) { printSolveProgress(ev); }
00697 else if (const SatPre* sat = event_cast<SatPre>(ev)){
00698 if (sat->op != SatElite::SatElite::Progress::event_algorithm) { comment(2, "Sat-Prepro : %c: %8u/%-8u\r", (char)sat->op, sat->cur, sat->max); }
00699 else if (sat->cur!= sat->max) {
00700 setState(0,0,0); comment(2, "Sat-Prepro :\r");
00701 state_ = Event::subsystem_prepare;
00702 }
00703 else {
00704 SatPreprocessor* p = sat->self;
00705 double tEnd = RealTime::getTime();
00706 comment(2, "Sat-Prepro : %.3f (ClRemoved: %u ClAdded: %u LitsStr: %u)\n", tEnd - stTime_, p->stats.clRemoved, p->stats.clAdded, p->stats.litsRemoved);
00707 state_ = 0;
00708 }
00709 }
00710 }
00711 else if (const LogEvent* log = event_cast<LogEvent>(ev)) {
00712 setState(ev.system, ev.verb, log->msg);
00713 }
00714 }
00715 Output::onEvent(ev);
00716 }
00717
00718 void TextOutput::setState(uint32 state, uint32 verb, const char* m) {
00719 if (state != state_ && verb <= verbosity()) {
00720 double tEnd = RealTime::getTime();
00721 if (state_ == Event::subsystem_solve) { comment(2, "%s\n", rowSep); line_ = 20; }
00722 else if (state_ != Event::subsystem_facade){ printf("%.3f\n", tEnd - stTime_); }
00723 stTime_ = tEnd;
00724 state_ = state;
00725 ev_ = -1;
00726 if (state_ == Event::subsystem_load) { comment(2, "%-13s: ", m ? m : "Reading"); }
00727 else if (state_ == Event::subsystem_prepare){ comment(2, "%-13s: ", m ? m : "Preprocessing"); }
00728 else if (state_ == Event::subsystem_solve) { comment(1, "Solving...\n"); line_ = 0; }
00729 }
00730 }
00731
00732 void TextOutput::printSolveProgress(const Event& ev) {
00733 if (ev.id == SolveTestEvent::id_s && (verbosity() & 4) == 0) { return; }
00734 if (ev.id == BasicSolveEvent::id_s && (verbosity() & 1) == 0) { return; }
00735 char lEnd = '\n';
00736 char line[128];
00737 if (const BasicSolveEvent* be = event_cast<BasicSolveEvent>(ev)) { Clasp::Cli::format(*be, line, 128); }
00738 else if (const SolveTestEvent* te = event_cast<SolveTestEvent>(ev) ) { Clasp::Cli::format(*te, line, 128); lEnd= te->result == -1 ? '\r' : '\n'; }
00739 #if WITH_THREADS
00740 else if (const mt::MessageEvent*me = event_cast<mt::MessageEvent>(ev)){ Clasp::Cli::format(*me, line, 128); }
00741 #endif
00742 else if (const LogEvent* log = event_cast<LogEvent>(ev)) { printLN(cat_comment, "%2u:L| %-69s |", log->solver->id(), log->msg); return; }
00743 else { return; }
00744 bool newEvent = (uint32)ev_.fetch_and_store(ev.id) != ev.id;
00745 if ((lEnd == '\n' && --line_ == 0) || newEvent) {
00746 if (line_ <= 0) {
00747 line_ = 20;
00748 printf("%s%s\n"
00749 "%sID:T Vars Constraints State Limits |\n"
00750 "%s #free/#fixed #problem/#learnt #conflicts/ratio #conflict/#learnt |\n"
00751 "%s%s\n", format[cat_comment], rowSep, format[cat_comment], format[cat_comment], format[cat_comment], rowSep);
00752 }
00753 else { printLN(cat_comment, "%s", rowSep); }
00754 }
00755 printf("%s%s%c", format[cat_comment], line, lEnd);
00756 fflush(stdout);
00757 }
00758
00759 int TextOutput::printSep(CategoryKey k) const {
00760 return printf("%s%s", ifs_, *ifs_ != '\n' ? "" : format[k]);
00761 }
00762 void TextOutput::printModel(const SymbolTable& sym, const Model& m, PrintLevel x) {
00763 if (x == modelQ()) {
00764 comment(1, "Answer: %" PRIu64"\n", m.num);
00765 printf("%s", format[cat_value]);
00766 if (sym.type() == SymbolTable::map_indirect) { printNames(sym, m); }
00767 else {
00768 uint32 const maxLineLen = *ifs_ == ' ' ? 70 : UINT32_MAX;
00769 uint32 printed = 0;
00770 bool const onlyTrue = m.consequences();
00771 std::string fmt("%s"); fmt += format[cat_atom];
00772 for (Var v = 1; v < sym.size(); ++v) {
00773 if (!onlyTrue || m.isTrue(posLit(v))) {
00774 if (printed) { printed += printSep(cat_value); }
00775 printed += printf(fmt.c_str(), m.value(v) == value_false ? "-":"", int(v));
00776 if (printed >= maxLineLen) {
00777 printed = 0;
00778 printf("\n%s", format[cat_value]);
00779 }
00780 }
00781 }
00782 }
00783 if (*format[cat_value_term]) {
00784 printSep(cat_value);
00785 printf("%s", format[cat_value_term]);
00786 }
00787 printf("\n");
00788 }
00789 if (x == optQ() && m.costs) {
00790 printf("%s", format[cat_objective]);
00791 printCosts(*m.costs);
00792 printf("\n");
00793 }
00794 fflush(stdout);
00795 }
00796
00797 void TextOutput::printNames(const Clasp::SymbolTable& sym, const Clasp::Model& m) {
00798 bool first = true;
00799 for (SymbolTable::const_iterator it = sym.begin(); it != sym.end(); ++it) {
00800 if (m.isTrue(it->second.lit) && doPrint(it->second)) {
00801 if (!first) { printSep(cat_value); }
00802 printf(format[cat_atom], it->second.name.c_str());
00803 first = false;
00804 }
00805 }
00806 }
00807
00808 void TextOutput::printCosts(const SharedMinimizeData& costs) const {
00809 printf("%" PRId64, costs.optimum(0));
00810 for (uint32 i = 1, end = costs.numRules(); i != end; ++i) {
00811 printSep(cat_objective);
00812 printf("%" PRId64, costs.optimum(i));
00813 }
00814 }
00815 void TextOutput::startSection(const char* n) const {
00816 printLN(cat_comment, "============ %s Stats ============", n);
00817 printBR(cat_comment);
00818 }
00819 void TextOutput::startObject(const char* n, uint32 i) const {
00820 printLN(cat_comment, "[%s %u]", n, i);
00821 printBR(cat_comment);
00822 }
00823 void TextOutput::visitProblemStats(const ProblemStats& stats, const Asp::LpStats* lp) {
00824 StatsVisitor::visitProblemStats(stats, lp);
00825 printBR(cat_comment);
00826 }
00827 void TextOutput::visitSolverStats(const Clasp::SolverStats& s, bool accu) {
00828 StatsVisitor::visitSolverStats(s, accu);
00829 printBR(cat_comment);
00830 }
00831
00832 void TextOutput::visitLogicProgramStats(const Asp::LpStats& lp) {
00833 using namespace Asp;
00834 printKeyValue("Atoms", "%-8u", lp.atoms);
00835 if (lp.auxAtoms) {
00836 printf(" (Original: %u Auxiliary: %u)", lp.atoms-lp.auxAtoms, lp.auxAtoms);
00837 }
00838 printf("\n");
00839 printKeyValue("Rules", "%-8u", lp.rules());
00840 printf(" ");
00841 char space = '(', close = ' ';
00842 for (Asp::RuleType i = BASICRULE; i != ENDRULE; ++i) {
00843 LpStats::RPair r = lp.rules(i);
00844 if (r.first) {
00845 printf("%c%d: %u", space, i, r.first);
00846 if (lp.tr()) { printf("/%u", r.second); }
00847 space = ' ';
00848 close = ')';
00849 }
00850 }
00851 printf("%c\n", close);
00852 printKeyValue("Bodies", "%-8u\n", lp.bodies);
00853 if (lp.eqs() > 0) {
00854 printKeyValue("Equivalences", "%-8u", lp.eqs());
00855 printf(" (Atom=Atom: %u Body=Body: %u Other: %u)\n"
00856 , lp.eqs(Var_t::atom_var)
00857 , lp.eqs(Var_t::body_var)
00858 , lp.eqs(Var_t::atom_body_var));
00859 }
00860 printKey("Tight");
00861 if (lp.sccs == 0) { printf("Yes"); }
00862 else if (lp.sccs != PrgNode::noScc) { printf("%-8s (SCCs: %u Non-Hcfs: %u Nodes: %u Gammas: %u)", "No", lp.sccs, lp.nonHcfs, lp.ufsNodes, lp.gammas); }
00863 else { printf("N/A"); }
00864 printf("\n");
00865 }
00866 void TextOutput::visitProblemStats(const ProblemStats& ps) {
00867 uint32 sum = ps.constraints + ps.constraints_binary + ps.constraints_ternary;
00868 printKeyValue("Variables", "%-8u", ps.vars);
00869 printf(" (Eliminated: %4u Frozen: %4u)\n", ps.vars_eliminated, ps.vars_frozen);
00870 printKeyValue("Constraints", "%-8u", sum);
00871 printf(" (Binary:%5.1f%% Ternary:%5.1f%% Other:%5.1f%%)\n"
00872 , percent(ps.constraints_binary, sum)
00873 , percent(ps.constraints_ternary, sum)
00874 , percent(ps.constraints, sum));
00875 }
00876 void TextOutput::visitCoreSolverStats(double cpuTime, uint64 models, const SolverStats& st, bool accu) {
00877 if (!accu) {
00878 printKeyValue("CPU Time", "%.3fs\n", cpuTime);
00879 printKeyValue("Models", "%" PRIu64"\n", models);
00880 }
00881 printKeyValue("Choices", "%-8" PRIu64, st.choices);
00882 if (st.extra && st.extra->domChoices) { printf(" (Domain: %" PRIu64")", st.extra->domChoices); }
00883 printf("\n");
00884 printKeyValue("Conflicts", "%-8" PRIu64"", st.conflicts);
00885 printf(" (Analyzed: %" PRIu64")\n", st.backjumps());
00886 printKeyValue("Restarts", "%-8" PRIu64"", st.restarts);
00887 if (st.restarts) {
00888 printf(" (Average: %.2f Last: %" PRIu64")", st.avgRestart(), st.lastRestart);
00889 }
00890 printf("\n");
00891 }
00892 void TextOutput::visitExtSolverStats(const ExtendedStats& stx, bool accu) {
00893 if (stx.hccTests) {
00894 printKeyValue("Stab. Tests", "%-8" PRIu64, stx.hccTests);
00895 printf(" (Full: %" PRIu64" Partial: %" PRIu64")\n", stx.hccTests - stx.hccPartial, stx.hccPartial);
00896 }
00897 if (stx.models) {
00898 printKeyValue("Model-Level", "%-8.1f\n", stx.avgModel());
00899 }
00900 printKeyValue("Problems", "%-8" PRIu64, (uint64)stx.gps);
00901 printf(" (Average Length: %.2f Splits: %" PRIu64")\n", stx.avgGp(), (uint64)stx.splits);
00902 uint64 sum = stx.lemmas();
00903 printKeyValue("Lemmas", "%-8" PRIu64, sum);
00904 printf(" (Deleted: %" PRIu64")\n", stx.deleted);
00905 const char* names[] = {" Conflict", " Loop", " Other"};
00906 for (int i = 0; i <= Constraint_t::learnt_other; ++i) {
00907 if (i == 0) {
00908 printKeyValue(" Binary", "%-8" PRIu64, uint64(stx.binary));
00909 printf(" (Ratio: %6.2f%%)\n", percent(stx.binary, sum));
00910 printKeyValue(" Ternary", "%-8" PRIu64, uint64(stx.ternary));
00911 printf(" (Ratio: %6.2f%%)\n", percent(stx.ternary, sum));
00912 }
00913 else {
00914 printKeyValue(names[i-1], "%-8" PRIu64, stx.lemmas(ConstraintType(i)));
00915 printf(" (Average Length: %6.1f Ratio: %6.2f%%) \n", stx.avgLen(ConstraintType(i)), percent(stx.lemmas(ConstraintType(i)), sum));
00916 }
00917 }
00918 if (stx.distributed || stx.integrated) {
00919 printKeyValue(" Distributed", "%-8" PRIu64, stx.distributed);
00920 printf(" (Ratio: %6.2f%% Average LBD: %.2f) \n", stx.distRatio()*100.0, stx.avgDistLbd());
00921 printKeyValue(" Integrated", "%-8" PRIu64, stx.integrated);
00922 if (accu){ printf(" (Ratio: %6.2f%% ", stx.intRatio()*100.0); }
00923 else { printf(" ("); }
00924 printf("Unit: %" PRIu64" Average Jumps: %.2f)\n", stx.intImps, stx.avgIntJump());
00925 }
00926 }
00927 void TextOutput::visitJumpStats(const JumpStats& st, bool) {
00928 printKeyValue("Backjumps", "%-8" PRIu64, st.jumps);
00929 printf(" (Average: %5.2f Max: %3u Sum: %6" PRIu64")\n", st.avgJump(), st.maxJump, st.jumpSum);
00930 printKeyValue(" Executed", "%-8" PRIu64, st.jumps-st.bounded);
00931 printf(" (Average: %5.2f Max: %3u Sum: %6" PRIu64" Ratio: %6.2f%%)\n", st.avgJumpEx(), st.maxJumpEx, st.jumped(), st.jumpedRatio()*100.0);
00932 printKeyValue(" Bounded", "%-8" PRIu64, st.bounded);
00933 printf(" (Average: %5.2f Max: %3u Sum: %6" PRIu64" Ratio: %6.2f%%)\n", st.avgBound(), st.maxBound, st.boundSum, 100.0 - (st.jumpedRatio()*100.0));
00934 }
00935
00936 #undef printKeyValue
00937 #undef printKey
00938 #undef printLN
00939 #undef printBR
00940 }}