1 // 2 // Copyright (c) 2015-2017 Benjamin Kaufmann 3 // 4 // This file is part of Potassco. 5 // 6 // Permission is hereby granted, free of charge, to any person obtaining a copy 7 // of this software and associated documentation files (the "Software"), to 8 // deal in the Software without restriction, including without limitation the 9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10 // sell copies of the Software, and to permit persons to whom the Software is 11 // furnished to do so, subject to the following conditions: 12 // 13 // The above copyright notice and this permission notice shall be included in 14 // all copies or substantial portions of the Software. 15 // 16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22 // IN THE SOFTWARE. 23 // 24 #ifndef POTASSCO_SMODELS_H_INCLUDED 25 #define POTASSCO_SMODELS_H_INCLUDED 26 #include <potassco/match_basic_types.h> 27 namespace Potassco { 28 /*! 29 * \addtogroup ParseType 30 */ 31 ///@{ 32 33 //! Interface representing an smodels-style symbol table. 34 class AtomTable { 35 public: 36 virtual ~AtomTable(); 37 //! Associate a name with the given (output) atom. 38 virtual void add(Atom_t id, const StringSpan& name, bool output) = 0; 39 //! Return the atom with the given name or 0 if no such atom was previously added. 40 virtual Atom_t find(const StringSpan& name) = 0; 41 }; 42 43 //! Class for parsing logic programs in (extended) smodels format. 44 class SmodelsInput : public ProgramReader { 45 public: 46 //! Options for configuring reading of smodels format. 47 struct Options { OptionsOptions48 Options() : claspExt(false), cEdge(false), cHeuristic(false), filter(false) {} 49 //! Enable clasp extensions for handling incremental programs. enableClaspExtOptions50 Options& enableClaspExt() { claspExt = true; return *this; } 51 //! Convert _edge/_acyc_ atoms to edge directives. convertEdgesOptions52 Options& convertEdges() { cEdge = true; return *this; } 53 //! Convert _heuristic atoms to heuristic directives. convertHeuristicOptions54 Options& convertHeuristic() { cHeuristic = true; return *this; } 55 //! Remove converted atoms from output. dropConvertedOptions56 Options& dropConverted() { filter = true; return *this; } 57 bool claspExt; 58 bool cEdge; 59 bool cHeuristic; 60 bool filter; 61 }; 62 //! Creates a new parser object that calls out on each parsed element. 63 SmodelsInput(AbstractProgram& out, const Options& opts, AtomTable* symTab = 0); 64 virtual ~SmodelsInput(); 65 protected: 66 //! Checks whether stream starts with a valid smodels token. 67 virtual bool doAttach(bool& inc); 68 //! Parses the current step and throws exception on error. 69 /*! 70 * The function calls beginStep()/endStep() on the associated 71 * output object before/after parsing the current step. 72 */ 73 virtual bool doParse(); 74 //! Resets internal parsing state. 75 virtual void doReset(); 76 //! Reads the current rule block. 77 virtual bool readRules(); 78 //! Reads the current smodels symbol table block. 79 virtual bool readSymbols(); 80 //! Reads the current part of the compute statement. 81 virtual bool readCompute(const char* sec, bool val); 82 //! Reads an optional external block and the number of models. 83 virtual bool readExtra(); 84 private: 85 struct NodeTab; 86 struct SymTab; 87 void matchBody(RuleBuilder& rule); 88 void matchSum(RuleBuilder& rule, bool weights); 89 AbstractProgram& out_; 90 AtomTable* atoms_; 91 NodeTab* nodes_; 92 Options opts_; 93 bool delSyms_; 94 }; 95 96 /*! 97 * Parses the given program in smodels format and calls out on each parsed element. 98 * The error handler h is called on error. If h is 0, std::exceptions are used to signal errors. 99 */ 100 int readSmodels(std::istream& prg, AbstractProgram& out, ErrorHandler h = 0, const SmodelsInput::Options& opts = SmodelsInput::Options()); 101 102 ///@} 103 104 /*! 105 * \addtogroup WriteType 106 */ 107 ///@{ 108 109 //! Returns a non-zero value if head can be represented in smodels format (i.e. is not empty). 110 int isSmodelsHead(Head_t ht, const AtomSpan& head); 111 //! Returns a non-zero value if rule can be represented in smodels format. 112 int isSmodelsRule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body); 113 114 //! Writes a program in smodels numeric format to the given output stream. 115 /*! 116 * \note The class only supports program constructs that can be directly 117 * expressed in smodels numeric format. 118 */ 119 class SmodelsOutput : public AbstractProgram { 120 public: 121 //! Creates a new object and associates it with the given output stream. 122 /*! 123 * If enableClaspExt is true, rules with numbers 90, 91, and 92 124 * are used to enable incremental programs and external atoms. 125 * 126 * The falseAtom is used to write integrity constraints and can be 127 * set to 0 if integrity constraints are not used. 128 */ 129 SmodelsOutput(std::ostream& os, bool enableClaspExt, Atom_t falseAtom); 130 //! Prepares the object for a new program. 131 /*! 132 * Requires enableClaspExt or inc must be false. 133 */ 134 virtual void initProgram(bool inc); 135 //! Starts a new step. 136 virtual void beginStep(); 137 //! Writes the given rule provided that isSmodelsHead(head) returns a non-zero value. 138 virtual void rule(Head_t t, const AtomSpan& head, const LitSpan& body); 139 //! Writes the given rule provided that isSmodelsRule(head, bound, body) returns a non-zero value. 140 virtual void rule(Head_t t, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body); 141 //! Writes the given minimize rule while ignoring its priority. 142 virtual void minimize(Weight_t prio, const WeightLitSpan& lits); 143 //! Writes the entry (a, str) to the symbol table provided that condition equals a. 144 /*! 145 * \note Symbols shall only be added once after all rules were added. 146 */ 147 virtual void output(const StringSpan& str, const LitSpan& cond); 148 //! Writes lits as a compute statement. 149 /*! 150 * \note The function shall be called at most once per step and only after all rules and symbols were added. 151 */ 152 virtual void assume(const LitSpan& lits); 153 //! Requires enableClaspExt or throws exception. 154 virtual void external(Atom_t a, Value_t v); 155 //! Terminates the current step. 156 virtual void endStep(); 157 protected: 158 //! Starts writing an smodels-rule of type rt. 159 SmodelsOutput& startRule(int rt); 160 //! Writes the given head. 161 SmodelsOutput& add(Head_t ht, const AtomSpan& head); 162 //! Writes the given normal body in smodels format, i.e. size(lits) size(B-) atoms in B- atoms in B+ 163 SmodelsOutput& add(const LitSpan& lits); 164 //! Writes the given extended body in smodels format. 165 SmodelsOutput& add(Weight_t bound, const WeightLitSpan& lits, bool card); 166 //! Writes i. 167 SmodelsOutput& add(unsigned i); 168 //! Terminates the active rule by writing a newline. 169 SmodelsOutput& endRule(); 170 //! Returns whether the current program is incremental. incremental()171 bool incremental() const { return inc_; } 172 //! Returns whether clasp extensions are enabled. extended()173 bool extended() const { return ext_; } 174 private: 175 SmodelsOutput(const SmodelsOutput&); 176 SmodelsOutput& operator=(const SmodelsOutput&); 177 std::ostream& os_; 178 Atom_t false_; 179 int sec_; 180 bool ext_; 181 bool inc_; 182 bool fHead_; 183 }; 184 ///@} 185 186 } // namespace Potassco 187 #endif 188