clasp_facade.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2012, 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_CLASP_FACADE_H_INCLUDED
#define CLASP_CLASP_FACADE_H_INCLUDED

#ifdef _MSC_VER
#pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
#pragma once
#endif

#if !defined(CLASP_VERSION)
#define CLASP_VERSION "3.0.4-p8"
#endif
#if !defined(CLASP_LEGAL)
#define CLASP_LEGAL \
"Copyright (C) Benjamin Kaufmann\n"\
"License GPLv2+: GNU GPL version 2 or later <http://gnu.org/licenses/gpl.html>\n"\
"clasp is free software: you are free to change and redistribute it.\n"\
"There is NO WARRANTY, to the extent permitted by law."
#endif

#if !defined(WITH_THREADS)
#error Invalid thread configuration - use WITH_THREADS=0 for single-threaded or WITH_THREADS=1 for multi-threaded version of libclasp!
#endif

#if WITH_THREADS
#include <clasp/parallel_solve.h>
namespace Clasp { typedef Clasp::mt::ParallelSolveOptions SolveOptions; }
#else
#include <clasp/shared_context.h>
#include <clasp/solve_algorithms.h>
namespace Clasp { typedef Clasp::BasicSolveOptions SolveOptions; }
#endif

#include <clasp/program_builder.h>
#include <clasp/logic_program.h>
#include <clasp/enumerator.h>
namespace Clasp {
// Configuration
class ClaspConfig : public BasicSatConfig {
public:
    typedef BasicSatConfig UserConfig;
    typedef Solver**       SolverIt;
    typedef Asp::LogicProgram::AspOptions AspOptions;   
    ClaspConfig();
    ~ClaspConfig();
    // Base interface
    void         prepare(SharedContext&);
    void         reset();
    // own interface
    UserConfig*  testerConfig() const { return tester_; } 
    UserConfig*  addTesterConfig();
    void         setSolvers(uint32 n);
    
    SolveOptions solve;    
    EnumOptions  enumerate;
    AspOptions   asp;      
private:
    ClaspConfig(const ClaspConfig&);
    ClaspConfig& operator=(const ClaspConfig&);
    UserConfig* tester_;
};
// ClaspFacade
struct ExpectedQuantity {
    enum Error { error_none = 0, error_unknown_quantity = 1, error_ambiguous_quantity = 2, error_not_available = 3 };
    ExpectedQuantity(double d);
    ExpectedQuantity(uint32 x) : rep(static_cast<double>(x)) {}
    ExpectedQuantity(uint64 x) : rep(static_cast<double>(x)) {}
    explicit ExpectedQuantity(const void* x) : rep(static_cast<double>(reinterpret_cast<uintp>(x))) {}
    ExpectedQuantity(Error e);
    bool     valid()  const { return error() == error_none; }
    Error    error()  const;
    operator double() const;
    double rep;
};

class ClaspFacade : public EventHandler {
    struct SolveImpl;
    struct SolveStrategy;
public:
    struct Result {
        enum Base {
            UNKNOWN  = 0, 
            SAT      = 1, 
            UNSAT    = 2, 
        };
        enum Ext {
            EXT_EXHAUST  = 4, 
            EXT_INTERRUPT= 8, 
            EXT_ERROR    = 16,
        };
        bool sat()        const { return *this == SAT; }
        bool unsat()      const { return *this == UNSAT; }
        bool unknown()    const { return *this == UNKNOWN; }
        bool exhausted()  const { return (flags & EXT_EXHAUST)   != 0; }
        bool interrupted()const { return (flags & EXT_INTERRUPT) != 0; }
        bool error()      const { return (flags & EXT_ERROR)     != 0; }
        operator Base()   const { return static_cast<Base>(flags & 3u);}
        operator double() const { return (double(signal)*256.0) + flags; }
        uint8 flags;  // result flags
        uint8 signal; // term signal or 0
    };
    struct Summary {
        typedef SharedMinimizeData SharedMinData;
        void init(ClaspFacade& f);
        const SharedContext& ctx()          const { return facade->ctx; }   
        const Asp::LpStats*  lpStats()      const { return facade->lpStats_.get(); }
        uint64               enumerated()   const { return numEnum; }
        bool                 sat()          const { return result.sat();   }
        bool                 unsat()        const { return result.unsat(); }
        bool                 complete()     const { return result.exhausted(); }
        bool                 optimum()      const;
        uint64               optimal()      const; 
        bool                 optimize()     const;
        const SharedMinData* costs()        const;
        const char*          consequences() const;
        int                  stats()        const;
        const Model*         model()        const;
        const ClaspFacade* facade;    
        double             totalTime; 
        double             cpuTime;   
        double             solveTime; 
        double             unsatTime; 
        double             satTime;   
        uint64             numEnum;   
        uint32             step;      
        Result             result;    
    };
    struct StepStart : Event_t<StepStart> {
        explicit StepStart(const ClaspFacade& f) : Event_t<StepStart>(subsystem_facade, verbosity_quiet), facade(&f) {}
        const ClaspFacade* facade;
    };
    struct StepReady : Event_t<StepReady> {
        explicit StepReady(const Summary& x) : Event_t<StepReady>(subsystem_facade, verbosity_quiet), summary(&x) {}
        const Summary* summary;
    };
    ClaspFacade();
    ~ClaspFacade();
    SharedContext ctx; 
    Asp::LogicProgram& startAsp(ClaspConfig& config, bool allowUpdate = false);
    SatBuilder&        startSat(ClaspConfig& config, bool allowUpdate = false);
    PBBuilder&         startPB(ClaspConfig& config , bool allowUpdate = false);
    ProgramBuilder&    start(ClaspConfig& config, ProblemType t, bool allowUpdate = false);
    
    enum EnumMode { enum_volatile, enum_static };

    bool               prepare(EnumMode m = enum_volatile);
    void               assume(Literal p);
    void               assume(const LitVec& ext);

    ProgramBuilder&    update(bool updateConfig = false);
    

    Result             solve(Clasp::EventHandler* onModel = 0);
#if WITH_THREADS
    struct AsyncSolve;
    class AsyncResult {
    public:
        typedef  StepReady Ready;
        explicit AsyncResult(SolveImpl& x);
        ~AsyncResult();
        AsyncResult(const AsyncResult&);
        AsyncResult& operator=(AsyncResult temp)            { swap(*this, temp); return *this; }
        friend void swap(AsyncResult& lhs, AsyncResult& rhs){ std::swap(lhs.state_, rhs.state_); }
        // blocking operations
        Result get()              const;
        void   wait()             const;
        bool   waitFor(double sec)const;
        bool   cancel()           const;

        // non-blocking operations
        bool   ready()            const;
        bool   ready(Result& r)   const;
        int    interrupted()      const;
        bool   error()            const;
        bool   running()          const;

        // model iterator operations
        // Example:
        //  for (AsyncResult it = facade.startSolveAsync(); !it.end(); it.next()) {
        //    printModel(it.model());
        //  }
        bool               end()    const;
        void               next()   const;
        const Model&       model()  const;
    private:
        AsyncSolve* state_;
    };

    AsyncResult        solveAsync(Clasp::EventHandler* handler = 0);


    AsyncResult        startSolveAsync();
#endif
    bool               ok()                  const { return program() ? program()->ok() : ctx.ok(); }
    bool               terminate(int signal);
    const Summary&     shutdown();
    bool               solving()             const;
    const Summary&     summary()             const { return step_; }
    const ClaspConfig* config()              const { return config_;}
    int                step()                const { return (int)step_.step;}
    Result             result()              const { return step_.result; }
    ProgramBuilder*    program()             const { return builder_.get(); }
    
    ExpectedQuantity   getStat(const char* path)const;
    const char*        getKeys(const char* path)const;
private:
    typedef SingleOwnerPtr<ProgramBuilder> BuilderPtr;
    typedef SingleOwnerPtr<Asp::LpStats>   LpStatsPtr;
    typedef SingleOwnerPtr<SolveImpl>      SolvePtr;
    typedef SingleOwnerPtr<Summary>        SummaryPtr;
    ExpectedQuantity getStatImpl(const char* path, bool keys)const;
    ExpectedQuantity getStat(const SharedContext& ctx, const char* key, bool accu, const Range<uint32>& r) const;
    void   init(ClaspConfig& cfg, bool discardProblem);
    void   initBuilder(ProgramBuilder* in, bool incremental);
    void   discardProblem();
    void   startStep(uint32 num);
    Result stopStep(int signal, bool complete);
    void   accuStep();
    bool   onModel(const Solver& s, const Model& m);
    ClaspConfig* config_;
    BuilderPtr   builder_;
    LpStatsPtr   lpStats_;
    SolvePtr     solve_;
    SummaryPtr   accu_;
    LitVec       assume_;
    Summary      step_;
};
}
#endif