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.3"
#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