dlvhex
2.5.0
|
00001 /* dlvhex -- Answer-Set Programming with external interfaces. 00002 * Copyright (C) 2005-2007 Roman Schindlauer 00003 * Copyright (C) 2006-2015 Thomas Krennwallner 00004 * Copyright (C) 2009-2016 Peter Schüller 00005 * Copyright (C) 2011-2016 Christoph Redl 00006 * Copyright (C) 2015-2016 Tobias Kaminski 00007 * Copyright (C) 2015-2016 Antonius Weinzierl 00008 * 00009 * This file is part of dlvhex. 00010 * 00011 * dlvhex is free software; you can redistribute it and/or modify it 00012 * under the terms of the GNU Lesser General Public License as 00013 * published by the Free Software Foundation; either version 2.1 of 00014 * the License, or (at your option) any later version. 00015 * 00016 * dlvhex is distributed in the hope that it will be useful, but 00017 * WITHOUT ANY WARRANTY; without even the implied warranty of 00018 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 00019 * Lesser General Public License for more details. 00020 * 00021 * You should have received a copy of the GNU Lesser General Public 00022 * License along with dlvhex; if not, write to the Free Software 00023 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 00024 * 02110-1301 USA. 00025 */ 00026 00034 #ifdef HAVE_CONFIG_H 00035 #include "config.h" 00036 #endif 00037 00038 #ifndef GRINGO3 // GRINGO4 00039 00040 #ifdef HAVE_LIBGRINGO 00041 00042 #ifndef _GRINGOGROUNDER_HPP 00043 #define _GRINGOGROUNDER_HPP 00044 00045 #include "dlvhex2/ProgramCtx.h" 00046 #include "dlvhex2/OrdinaryASPProgram.h" 00047 #include "dlvhex2/Printer.h" 00048 #include "dlvhex2/GenuineSolver.h" 00049 00050 #include <vector> 00051 #include <map> 00052 #include <sstream> 00053 #include <string> 00054 00055 #include "gringo/input/nongroundparser.hh" 00056 #include "gringo/input/programbuilder.hh" 00057 #include "gringo/input/program.hh" 00058 #include "gringo/ground/program.hh" 00059 #include "gringo/output/output.hh" 00060 #include "gringo/logger.hh" 00061 #include "gringo/scripts.hh" 00062 #include "gringo/version.hh" 00063 #include "gringo/control.hh" 00064 #include "program_opts/application.h" 00065 #include "program_opts/typed_value.h" 00066 00067 DLVHEX_NAMESPACE_BEGIN 00068 00072 class GringoGrounder: public GenuineGrounder 00073 { 00074 private: 00076 ProgramCtx& ctx; 00078 OrdinaryASPProgram nongroundProgram; 00080 OrdinaryASPProgram groundProgram; 00082 InterpretationConstPtr frozen; 00084 ID intPred; 00086 ID anonymousPred; 00088 ID unsatPred; 00089 00091 class Printer : public RawPrinter 00092 { 00093 public: 00094 typedef RawPrinter Base; 00096 ID intPred; 00101 Printer(std::ostream& out, RegistryPtr registry, ID intPred) : RawPrinter(out, registry), intPred(intPred) {} 00102 00103 virtual void printRule(ID id); 00104 virtual void printAggregate(ID id); 00105 virtual void printInt(ID id); 00106 virtual void print(ID id); 00107 }; 00108 00110 class GroundHexProgramBuilder : public Gringo::Output::PlainLparseOutputter 00111 { 00112 private: 00113 typedef std::vector<unsigned> WeightVec; 00114 00116 std::stringstream emptyStream; 00117 uint32_t symbols_; 00119 bool hasExternal_; 00121 ProgramCtx& ctx; 00123 OrdinaryASPProgram& groundProgram; 00125 InterpretationPtr mask; 00127 ID intPred; 00129 ID anonymousPred; 00131 ID unsatPred; 00133 bool incAdd; 00134 00136 struct LParseRule 00137 { 00139 enum Type 00140 { 00142 Regular, 00144 Weight 00145 }; 00147 Type type; 00148 00150 AtomVec head; 00152 LitVec body; 00154 WeightVec weights; 00156 int bound; 00160 LParseRule(const AtomVec& h, const LitVec& v) : head(h), body(v), bound(0), type(Regular){} 00164 LParseRule(int h, const LitVec& v) : body(v), bound(0), type(Regular) { 00165 head.push_back(h); 00166 } 00172 LParseRule(int h, const LitVec& v, const WeightVec& w, int bound) : body(v), weights(w), bound(bound), type(Weight) { 00173 head.push_back(h); 00174 } 00177 LParseRule(const LParseRule& r2) { 00178 type = r2.type; 00179 head = r2.head; 00180 body = r2.body; 00181 weights = r2.weights; 00182 bound = r2.bound; 00183 } 00184 }; 00185 00188 void addSymbol(uint32_t symbol); 00189 00191 std::map<int, ID> indexToGroundAtomID; 00193 std::list<LParseRule> rules; 00194 00196 std::stringstream emptystream; 00197 public: 00204 GroundHexProgramBuilder(ProgramCtx& ctx, OrdinaryASPProgram& groundProgram, ID intPred, ID anonymousPred, ID unsatPred, bool incAdd = false); 00206 void transformRules(); 00207 00209 void finishRules(); 00211 void printBasicRule(unsigned head, const LitVec &body); 00213 void printChoiceRule(const AtomVec &head, const LitVec &body); 00215 void printCardinalityRule(unsigned head, unsigned lower, const LitVec &body); 00217 void printWeightRule(unsigned head, unsigned bound, const LitWeightVec &body); 00219 void printMinimizeRule(const LitWeightVec &body); 00221 void printDisjunctiveRule(const AtomVec &head, const LitVec &body); 00222 00224 void printSymbol(unsigned atomUid, Gringo::Value v); 00226 void printExternal(unsigned atomUid, Gringo::TruthValue e); 00228 void forgetStep(int) { } 00230 uint32_t symbol(); 00231 }; 00232 00233 public: 00238 GringoGrounder(ProgramCtx& ctx, const OrdinaryASPProgram& p, InterpretationConstPtr frozen); 00241 const OrdinaryASPProgram& getGroundProgram(); 00242 00243 protected: 00246 int doRun(); 00247 }; 00248 00249 DLVHEX_NAMESPACE_END 00250 #endif 00251 #endif 00252 00253 #else // GRINGO3 00254 00255 #ifdef HAVE_LIBGRINGO 00256 00257 #ifndef _GRINGOGROUNDER_HPP 00258 #define _GRINGOGROUNDER_HPP 00259 00260 #include "dlvhex2/ProgramCtx.h" 00261 #include "dlvhex2/OrdinaryASPProgram.h" 00262 #include "dlvhex2/Printer.h" 00263 #include "dlvhex2/GenuineSolver.h" 00264 00265 #include <vector> 00266 #include <map> 00267 #include <sstream> 00268 00269 #include "gringo/lparseoutput.h" 00270 #include "gringo/streams.h" 00271 00272 DLVHEX_NAMESPACE_BEGIN 00273 00274 namespace detail 00275 { 00277 class GringoOptions 00278 { 00279 public: 00281 enum IExpand { IEXPAND_ALL, IEXPAND_DEPTH }; 00282 00283 public: 00285 GringoOptions(); 00286 00287 // AppOptions interface 00288 //void initOptions(ProgramOptions::OptionGroup& root, ProgramOptions::OptionGroup& hidden); 00289 //bool validateOptions(ProgramOptions::OptionValues& values, Messages&); 00290 //void addDefaults(std::string& def); 00291 //TermExpansionPtr termExpansion(IncConfig &config) const; 00292 00294 std::vector<std::string> consts; 00296 bool smodelsOut; 00298 bool textOut; 00299 bool metaOut; 00301 bool groundOnly; 00302 int ifixed; 00303 bool ibase; 00304 bool groundInput; 00306 bool disjShift; 00308 std::string depGraph; 00309 bool compat; 00311 bool stats; 00313 IExpand iexpand; 00314 }; 00315 } 00316 00317 00321 class GringoGrounder: public GenuineGrounder 00322 { 00323 private: 00325 ProgramCtx& ctx; 00327 OrdinaryASPProgram nongroundProgram; 00329 OrdinaryASPProgram groundProgram; 00331 InterpretationConstPtr frozen; 00333 ID intPred; 00335 ID anonymousPred; 00337 ID unsatPred; 00338 00340 detail::GringoOptions gringo; 00341 00343 class Printer : public RawPrinter 00344 { 00345 public: 00346 typedef RawPrinter Base; 00348 ID intPred; 00353 Printer(std::ostream& out, RegistryPtr registry, ID intPred) : RawPrinter(out, registry), intPred(intPred) {} 00354 00355 virtual void printRule(ID id); 00356 virtual void printAggregate(ID id); 00357 virtual void printInt(ID id); 00358 virtual void print(ID id); 00359 }; 00360 00362 class GroundHexProgramBuilder : public LparseConverter 00363 { 00364 private: 00366 std::stringstream emptyStream; 00368 uint32_t symbols_; 00370 bool hasExternal_; 00372 ProgramCtx& ctx; 00374 OrdinaryASPProgram& groundProgram; 00376 InterpretationPtr mask; 00378 ID intPred; 00380 ID anonymousPred; 00382 ID unsatPred; 00383 00385 struct LParseRule 00386 { 00388 enum Type 00389 { 00391 Regular, 00393 Weight 00394 }; 00396 Type type; 00397 00399 AtomVec head; 00401 AtomVec pos; 00403 AtomVec neg; 00405 WeightVec wpos; 00407 WeightVec wneg; 00409 int bound; 00414 LParseRule(const AtomVec& h, const AtomVec& p, const AtomVec& n) : head(h), pos(p), neg(n), bound(0), type(Regular){} 00419 LParseRule(int h, const AtomVec& p, const AtomVec& n) : pos(p), neg(n), bound(0), type(Regular) { 00420 head.push_back(h); 00421 } 00429 LParseRule(int h, const AtomVec& p, const AtomVec& n, const WeightVec& wp, const WeightVec& wn, int bound) : pos(p), neg(n), wpos(wp), wneg(wn), bound(bound), type(Weight) { 00430 head.push_back(h); 00431 } 00434 LParseRule(const LParseRule& r2) { 00435 type = r2.type; 00436 head = r2.head; 00437 pos = r2.pos; 00438 neg = r2.neg; 00439 wpos = r2.wpos; 00440 wneg = r2.wneg; 00441 bound = r2.bound; 00442 } 00443 00444 }; 00445 00448 void addSymbol(uint32_t symbol); 00449 00451 std::map<int, ID> indexToGroundAtomID; 00453 std::list<LParseRule> rules; 00454 public: 00461 GroundHexProgramBuilder(ProgramCtx& ctx, OrdinaryASPProgram& groundProgram, ID intPred, ID anonymousPred, ID unsatPred); 00463 void doFinalize(); 00464 00466 void printBasicRule(int head, const AtomVec &pos, const AtomVec &neg); 00468 void printConstraintRule(int head, int bound, const AtomVec &pos, const AtomVec &neg); 00470 void printChoiceRule(const AtomVec &head, const AtomVec &pos, const AtomVec &neg); 00472 void printWeightRule(int head, int bound, const AtomVec &pos, const AtomVec &neg, const WeightVec &wPos, const WeightVec &wNeg); 00474 void printMinimizeRule(const AtomVec &pos, const AtomVec &neg, const WeightVec &wPos, const WeightVec &wNeg); 00476 void printDisjunctiveRule(const AtomVec &head, const AtomVec &pos, const AtomVec &neg); 00478 void printComputeRule(int models, const AtomVec &pos, const AtomVec &neg); 00480 void printSymbolTableEntry(const AtomRef &atom, uint32_t arity, const std::string &name); 00482 void printExternalTableEntry(const AtomRef &atom, uint32_t arity, const std::string &name); 00484 void forgetStep(int) { } 00486 uint32_t symbol(); 00487 }; 00488 00489 public: 00494 GringoGrounder(ProgramCtx& ctx, const OrdinaryASPProgram& p, InterpretationConstPtr frozen); 00497 const OrdinaryASPProgram& getGroundProgram(); 00498 00499 protected: 00501 Output *output(); 00505 Streams::StreamPtr constStream() const; 00508 int doRun(); 00509 }; 00510 00511 DLVHEX_NAMESPACE_END 00512 #endif 00513 #endif 00514 #endif 00515 00516 // vim:expandtab:ts=4:sw=4: 00517 // mode: C++ 00518 // End: