clasp_output.h

Go to the documentation of this file.

// 
// Copyright (c) 2009-2013, Benjamin Kaufmann
// 
// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
// 
// Clasp is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
// 
// Clasp is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
// 
// You should have received a copy of the GNU General Public License
// along with Clasp; if not, write to the Free Software
// Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
//
#ifndef CLASP_CLI_OUTPUT_H_INCLUDED
#define CLASP_CLI_OUTPUT_H_INCLUDED
#include <clasp/clasp_facade.h>
#include <clasp/dependency_graph.h>
#include <clasp/solver_types.h>
#include <string>
namespace Clasp { namespace Cli {
void format(const Clasp::BasicSolveEvent& ev, char* out, uint32 outSize);
void format(const Clasp::SolveTestEvent&  ev, char* out, uint32 outSize);
#if WITH_THREADS
void format(const Clasp::mt::MessageEvent& ev, char* out, uint32 outSize);
#endif

class Output : public EventHandler {
public:
        enum PrintLevel { 
                print_all  = 0, 
                print_best = 1, 
                print_no   = 2, 
        };
        explicit Output(uint32 verb = 1);
        virtual ~Output();
        uint32 verbosity()               const { return verbose_; }
        bool   quiet()                   const { return modelQ() == 2 && optQ() == 2; }
        int    modelQ()                  const { return static_cast<int>(quiet_[0]); }
        int    optQ()                    const { return static_cast<int>(quiet_[1]); }
        int    callQ()                   const { return static_cast<int>(quiet_[2]); }
        
        using  EventHandler::setVerbosity;
        void   setVerbosity(uint32 verb);
        void   setModelQuiet(PrintLevel model);
        void   setOptQuiet(PrintLevel opt);
        void   setCallQuiet(PrintLevel call);
        void   setHide(char c);

        virtual void run(const char* solver, const char* version, const std::string* begInput, const std::string* endInput) = 0;
        virtual void shutdown(const ClaspFacade::Summary& summary);
        virtual void shutdown() = 0;
        virtual void onEvent(const Event& ev);
        virtual bool onModel(const Solver& s, const Model& m);  
        virtual void printModel(const SymbolTable& sym, const Model& m, PrintLevel x) = 0;
        virtual void startStep(const ClaspFacade&);
        virtual void stopStep(const ClaspFacade::Summary& summary);
        virtual void printSummary(const ClaspFacade::Summary& summary, bool final)    = 0;
        virtual void printStatistics(const ClaspFacade::Summary& summary, bool final) = 0;
protected:
        const Model* getModel() const { return saved_.values ? &saved_ : 0; }
        void         saveModel(const Model& m);
        void         clearModel() { saved_.values = 0; }
        bool         doPrint(const SymbolTable::symbol_type& sym) const {
                return !sym.name.empty() && *sym.name.c_str() != hidePref_;
        }
private:
        Output(const Output&);
        Output& operator=(const Output&);
        typedef const ClaspFacade::Summary* SumPtr ;
        SumPtr    summary_ ; // summary of last step
        ValueVec  vals_    ; // saved values from most recent model
        Model     saved_   ; // most recent model
        uint32    verbose_ ; // verbosity level
        uint8     quiet_[3]; // quiet levels for models, optimize, calls
        char      hidePref_; // hide printing of symbols starting with this char
};

class StatsVisitor {
public:
        virtual ~StatsVisitor();
        virtual void visitStats(const SharedContext& ctx, const Asp::LpStats* lp, bool accu);
        // compound
        virtual void visitSolverStats(const SolverStats& stats, bool accu);
        virtual void visitProblemStats(const ProblemStats& stats, const Asp::LpStats* lp);
        virtual void visitThreads(const SharedContext& ctx);
        virtual void visitHccs(const SharedContext& ctx);
        virtual void visitThread(uint32, const SolverStats& stats) { visitSolverStats(stats, false); }
        virtual void visitHcc(uint32, const SharedContext& stats);
        // leafs
        virtual void visitLogicProgramStats(const Asp::LpStats& stats) = 0;
        virtual void visitProblemStats(const ProblemStats& stats) = 0;
        virtual void visitCoreSolverStats(double cpuTime, uint64 models, const SolverStats& stats, bool accu) = 0;
        virtual void visitExtSolverStats(const ExtendedStats& stats, bool accu) = 0;
        virtual void visitJumpStats(const JumpStats& stats, bool accu) = 0;
        virtual void accuStats(const SharedContext& ctx, SolverStats& out) const;

        bool accu;
};

class JsonOutput : public Output, private StatsVisitor {
public:
        explicit JsonOutput(uint32 verb);
        ~JsonOutput();
        virtual void run(const char* solver, const char* version, const std::string* begInput, const std::string* endInput);
        virtual void shutdown(const ClaspFacade::Summary& summary);
        virtual void shutdown();
        virtual void printSummary(const ClaspFacade::Summary&    summary, bool final);
        virtual void printStatistics(const ClaspFacade::Summary& summary, bool final);
private:
        virtual void startStep(const ClaspFacade&);
        virtual void stopStep(const ClaspFacade::Summary& summary);
        virtual void visitThreads(const SharedContext& ctx)         { pushObject("Thread", type_array); StatsVisitor::visitThreads(ctx);    popObject(); }
        virtual void visitHccs(const SharedContext& ctx)            { pushObject("HCC", type_array);    StatsVisitor::visitHccs(ctx);       popObject(); }
        virtual void visitThread(uint32 i, const SolverStats& stats){ pushObject(0, type_object);       StatsVisitor::visitThread(i, stats);popObject(); }
        virtual void visitHcc(uint32 i, const SharedContext& ctx)   { pushObject(0, type_object);       StatsVisitor::visitHcc(i, ctx);     popObject(); }
        virtual void visitLogicProgramStats(const Asp::LpStats& stats);
        virtual void visitProblemStats(const ProblemStats& stats);
        virtual void visitCoreSolverStats(double cpuTime, uint64 models, const SolverStats& stats, bool accu);
        virtual void visitExtSolverStats(const ExtendedStats& stats, bool accu);
        virtual void visitJumpStats(const JumpStats& stats, bool accu);
        enum ObjType { type_object, type_array };
        void pushObject(const char* k = 0, ObjType t = type_object);
        char popObject();
        void printKeyValue(const char* k, const char* v) ;
        void printKeyValue(const char* k, uint64 v);
        void printKeyValue(const char* k, uint32 v);
        void printKeyValue(const char* k, double d);
        void printString(const char* s, const char* sep);
        void printKey(const char* k);
        void printModel(const SymbolTable& sym, const Model& m, PrintLevel x);
        void printCosts(const SharedMinimizeData& costs);
        void startModel();
        bool hasWitness() const { return !objStack_.empty() && *objStack_.rbegin() == '['; }
        uint32 indent()   const { return static_cast<uint32>(objStack_.size() * 2); }
        const char* open_;
        std::string objStack_;
};


class TextOutput : public Output, private StatsVisitor {
public:
        enum Format      { format_asp, format_aspcomp, format_sat09, format_pb09 };
        enum ResultStr   { res_unknonw = 0, res_sat = 1, res_unsat = 2, res_opt = 3, num_str };
        enum CategoryKey { cat_comment, cat_value, cat_objective, cat_result, cat_value_term, cat_atom, num_cat };
        
        const char* result[num_str]; 
        const char* format[num_cat]; 
        TextOutput(uint32 verbosity, Format f, const char* catAtom = 0, char ifs = ' ');
        ~TextOutput();

        virtual void run(const char* solver, const char* version, const std::string* begInput, const std::string* endInput);
        virtual void shutdown();

        virtual void printModel(const SymbolTable& sym, const Model& m, PrintLevel x);

        virtual void printSummary(const ClaspFacade::Summary& s   , bool final);
        virtual void printStatistics(const ClaspFacade::Summary& s, bool final);
        virtual void onEvent(const Event& ev);
        virtual void startStep(const ClaspFacade&);
        void comment(uint32 v, const char* fmt, ...) const;
private:
        virtual void printNames(const SymbolTable& sym, const Model& m);
        virtual void visitProblemStats(const ProblemStats& stats, const Asp::LpStats* lp);
        virtual void visitSolverStats(const Clasp::SolverStats& s, bool accu);
        virtual void visitLogicProgramStats(const Asp::LpStats& stats);
        virtual void visitProblemStats(const ProblemStats& stats);
        virtual void visitCoreSolverStats(double cpuTime, uint64 models, const SolverStats& stats, bool accu);
        virtual void visitExtSolverStats(const ExtendedStats& stats, bool accu);
        virtual void visitJumpStats(const JumpStats& stats, bool accu);
        virtual void visitThreads(const SharedContext& ctx)      { startSection("Thread");   StatsVisitor::visitThreads(ctx); }
        virtual void visitThread(uint32 i, const SolverStats& s)  { startObject("Thread", i); StatsVisitor::visitThread(i, s); }
        virtual void visitHccs(const SharedContext& ctx)         { startSection("Tester");   StatsVisitor::visitHccs(ctx);    }
        virtual void visitHcc(uint32 i, const SharedContext& ctx){ startObject("HCC", i);    StatsVisitor::visitHcc(i, ctx);  }
        int  printSep(CategoryKey c) const;
        void printCosts(const SharedMinimizeData&) const;
        void startSection(const char* n)     const;
        void startObject(const char* n, uint32 i) const;
        void setState(uint32 state, uint32 verb, const char* st);
        void printSolveProgress(const Event& ev);
        double             stTime_;// time on state enter
        Clasp::atomic<int> ev_;    // last event type
        int                width_; // output width
        int                line_;  // lines to print until next separator
        uint32             state_; // active state
        char               ifs_[2];// field separator
};
}}
#endif