dlvhex/doc2x/_gringo_grounder_8h_source.html

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: