clasp_facade.h
Go to the documentation of this file.
00001 // 
00002 // Copyright (c) 2006-2012, Benjamin Kaufmann
00003 // 
00004 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
00005 // 
00006 // Clasp is free software; you can redistribute it and/or modify
00007 // it under the terms of the GNU General Public License as published by
00008 // the Free Software Foundation; either version 2 of the License, or
00009 // (at your option) any later version.
00010 // 
00011 // Clasp is distributed in the hope that it will be useful,
00012 // but WITHOUT ANY WARRANTY; without even the implied warranty of
00013 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
00014 // GNU General Public License for more details.
00015 // 
00016 // You should have received a copy of the GNU General Public License
00017 // along with Clasp; if not, write to the Free Software
00018 // Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
00019 //
00020 #ifndef CLASP_CLASP_FACADE_H_INCLUDED
00021 #define CLASP_CLASP_FACADE_H_INCLUDED
00022 
00023 #ifdef _MSC_VER
00024 #pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
00025 #pragma once
00026 #endif
00027 
00028 #if !defined(CLASP_VERSION)
00029 #define CLASP_VERSION "3.0.3"
00030 #endif
00031 #if !defined(CLASP_LEGAL)
00032 #define CLASP_LEGAL \
00033 "Copyright (C) Benjamin Kaufmann\n"\
00034 "License GPLv2+: GNU GPL version 2 or later <http://gnu.org/licenses/gpl.html>\n"\
00035 "clasp is free software: you are free to change and redistribute it.\n"\
00036 "There is NO WARRANTY, to the extent permitted by law."
00037 #endif
00038 
00039 #if !defined(WITH_THREADS)
00040 #error Invalid thread configuration - use WITH_THREADS=0 for single-threaded or WITH_THREADS=1 for multi-threaded version of libclasp!
00041 #endif
00042 
00043 #if WITH_THREADS
00044 #include <clasp/parallel_solve.h>
00045 namespace Clasp { typedef Clasp::mt::ParallelSolveOptions SolveOptions; }
00046 #else
00047 #include <clasp/shared_context.h>
00048 #include <clasp/solve_algorithms.h>
00049 namespace Clasp { typedef Clasp::BasicSolveOptions SolveOptions; }
00050 #endif
00051 
00052 #include <clasp/program_builder.h>
00053 #include <clasp/logic_program.h>
00054 #include <clasp/enumerator.h>
00061 namespace Clasp {
00063 // Configuration
00066 class ClaspConfig : public BasicSatConfig {
00067 public:
00068         typedef BasicSatConfig UserConfig;
00069         typedef Solver**       SolverIt;
00070         typedef Asp::LogicProgram::AspOptions AspOptions;       
00071         ClaspConfig();
00072         ~ClaspConfig();
00073         // Base interface
00074         void         prepare(SharedContext&);
00075         void         reset();
00076         // own interface
00077         UserConfig*  testerConfig() const { return tester_; } 
00078         UserConfig*  addTesterConfig();
00079         void         setSolvers(uint32 n);
00080         
00081         SolveOptions solve;    
00082         EnumOptions  enumerate;
00083         AspOptions   asp;      
00084 private:
00085         ClaspConfig(const ClaspConfig&);
00086         ClaspConfig& operator=(const ClaspConfig&);
00087         UserConfig* tester_;
00088 };
00090 // ClaspFacade
00093 struct ExpectedQuantity {
00094         enum Error { error_none = 0, error_unknown_quantity = 1, error_ambiguous_quantity = 2, error_not_available = 3 };
00095         ExpectedQuantity(double d);
00096         ExpectedQuantity(uint32 x) : rep(static_cast<double>(x)) {}
00097         ExpectedQuantity(uint64 x) : rep(static_cast<double>(x)) {}
00098         explicit ExpectedQuantity(const void* x) : rep(static_cast<double>(reinterpret_cast<uintp>(x))) {}
00099         ExpectedQuantity(Error e);
00100         bool     valid()  const { return error() == error_none; }
00101         Error    error()  const;
00102         operator double() const;
00103         double rep;
00104 };
00105 
00107 class ClaspFacade : public EventHandler {
00108         struct SolveImpl;
00109         struct SolveStrategy;
00110 public:
00112         struct Result {
00114                 enum Base {
00115                         UNKNOWN  = 0, 
00116                         SAT      = 1, 
00117                         UNSAT    = 2, 
00118                 };
00119                 enum Ext {
00120                         EXT_EXHAUST  = 4, 
00121                         EXT_INTERRUPT= 8, 
00122                         EXT_ERROR    = 16,
00123                 };
00124                 bool sat()        const { return *this == SAT; }
00125                 bool unsat()      const { return *this == UNSAT; }
00126                 bool unknown()    const { return *this == UNKNOWN; }
00127                 bool exhausted()  const { return (flags & EXT_EXHAUST)   != 0; }
00128                 bool interrupted()const { return (flags & EXT_INTERRUPT) != 0; }
00129                 bool error()      const { return (flags & EXT_ERROR)     != 0; }
00130                 operator Base()   const { return static_cast<Base>(flags & 3u);}
00131                 operator double() const { return (double(signal)*256.0) + flags; }
00132                 uint8 flags;  // result flags
00133                 uint8 signal; // term signal or 0
00134         };
00136         struct Summary {
00137                 typedef SharedMinimizeData SharedMinData;
00138                 void init(ClaspFacade& f);
00139                 const SharedContext& ctx()          const { return facade->ctx; }       
00140                 const Asp::LpStats*  lpStats()      const { return facade->lpStats_.get(); }
00141                 uint64               enumerated()   const { return numEnum; }
00142                 bool                 sat()          const { return result.sat();   }
00143                 bool                 unsat()        const { return result.unsat(); }
00144                 bool                 complete()     const { return result.exhausted(); }
00145                 bool                 optimum()      const;
00146                 uint64               optimal()      const; 
00147                 bool                 optimize()     const;
00148                 const SharedMinData* costs()        const;
00149                 const char*          consequences() const;
00150                 int                  stats()        const;
00151                 const Model*         model()        const;
00152                 const ClaspFacade* facade;    
00153                 double             totalTime; 
00154                 double             cpuTime;   
00155                 double             solveTime; 
00156                 double             unsatTime; 
00157                 double             satTime;   
00158                 uint64             numEnum;   
00159                 uint32             step;      
00160                 Result             result;    
00161         };
00163         struct StepStart : Event_t<StepStart> {
00164                 explicit StepStart(const ClaspFacade& f) : Event_t<StepStart>(subsystem_facade, verbosity_quiet), facade(&f) {}
00165                 const ClaspFacade* facade;
00166         };
00168         struct StepReady : Event_t<StepReady> {
00169                 explicit StepReady(const Summary& x) : Event_t<StepReady>(subsystem_facade, verbosity_quiet), summary(&x) {}
00170                 const Summary* summary;
00171         };
00172         ClaspFacade();
00173         ~ClaspFacade();
00174         SharedContext ctx; 
00184 
00185         Asp::LogicProgram& startAsp(ClaspConfig& config, bool allowUpdate = false);
00187         SatBuilder&        startSat(ClaspConfig& config, bool allowUpdate = false);
00189         PBBuilder&         startPB(ClaspConfig& config , bool allowUpdate = false);
00191         ProgramBuilder&    start(ClaspConfig& config, ProblemType t, bool allowUpdate = false);
00192         
00193         enum EnumMode { enum_volatile, enum_static };
00195 
00202         bool               prepare(EnumMode m = enum_volatile);
00204         void               assume(Literal p);
00206         void               assume(const LitVec& ext);
00208 
00211         ProgramBuilder&    update(bool updateConfig = false);
00213         
00215 
00223         Result             solve(Clasp::EventHandler* onModel = 0);
00224 #if WITH_THREADS
00225         struct AsyncSolve;
00227         class AsyncResult {
00228         public:
00229                 typedef  StepReady Ready;
00230                 explicit AsyncResult(SolveImpl& x);
00231                 ~AsyncResult();
00232                 AsyncResult(const AsyncResult&);
00233                 AsyncResult& operator=(AsyncResult temp)            { swap(*this, temp); return *this; }
00234                 friend void swap(AsyncResult& lhs, AsyncResult& rhs){ std::swap(lhs.state_, rhs.state_); }
00235                 // blocking operations
00237                 Result get()              const;
00239                 void   wait()             const;
00241                 bool   waitFor(double sec)const;
00243                 bool   cancel()           const;
00244 
00245                 // non-blocking operations
00247                 bool   ready()            const;
00249                 bool   ready(Result& r)   const;
00251                 int    interrupted()      const;
00253                 bool   error()            const;
00255                 bool   running()          const;
00256 
00257                 // model iterator operations
00258                 // Example:
00259                 //  for (AsyncResult it = facade.startSolveAsync(); !it.end(); it.next()) {
00260                 //    printModel(it.model());
00261                 //  }
00263                 bool               end()    const;
00265                 void               next()   const;
00267                 const Model&       model()  const;
00268         private:
00269                 AsyncSolve* state_;
00270         };
00272 
00278         AsyncResult        solveAsync(Clasp::EventHandler* handler = 0);
00279 
00281 
00289         AsyncResult        startSolveAsync();
00290 #endif
00291 
00292         bool               ok()                  const { return program() ? program()->ok() : ctx.ok(); }
00294         bool               terminate(int signal);
00295         const Summary&     shutdown();
00297         bool               solving()             const;
00299         const Summary&     summary()             const { return step_; }
00301         const ClaspConfig* config()              const { return config_;}
00303         int                step()                const { return (int)step_.step;}
00305         Result             result()              const { return step_.result; }
00307         ProgramBuilder*    program()             const { return builder_.get(); }
00308         
00309         ExpectedQuantity   getStat(const char* path)const;
00310         const char*        getKeys(const char* path)const;
00311 private:
00312         typedef SingleOwnerPtr<ProgramBuilder> BuilderPtr;
00313         typedef SingleOwnerPtr<Asp::LpStats>   LpStatsPtr;
00314         typedef SingleOwnerPtr<SolveImpl>      SolvePtr;
00315         typedef SingleOwnerPtr<Summary>        SummaryPtr;
00316         ExpectedQuantity getStatImpl(const char* path, bool keys)const;
00317         ExpectedQuantity getStat(const SharedContext& ctx, const char* key, bool accu, const Range<uint32>& r) const;
00318         void   init(ClaspConfig& cfg, bool discardProblem);
00319         void   initBuilder(ProgramBuilder* in, bool incremental);
00320         void   discardProblem();
00321         void   startStep(uint32 num);
00322         Result stopStep(int signal, bool complete);
00323         void   accuStep();
00324         bool   onModel(const Solver& s, const Model& m);
00325         ClaspConfig* config_;
00326         BuilderPtr   builder_;
00327         LpStatsPtr   lpStats_;
00328         SolvePtr     solve_;
00329         SummaryPtr   accu_;
00330         LitVec       assume_;
00331         Summary      step_;
00332 };
00333 }
00334 #endif


clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:38