1 // 2 // Copyright (c) 2016-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_ASPIF_TEXT_H_INCLUDED 25 #define POTASSCO_ASPIF_TEXT_H_INCLUDED 26 #include <potassco/match_basic_types.h> 27 #include <potassco/theory_data.h> 28 #include <cstring> 29 #include <string> 30 namespace Potassco { 31 //! Class for parsing logic programs in ground text format. 32 /*! 33 * \ingroup ParseType 34 */ 35 class AspifTextInput : public ProgramReader { 36 public: 37 //! Creates a new object and associates it with the given output if any. 38 AspifTextInput(AbstractProgram* out); 39 //! Sets the program to which parsed elements should be output. 40 void setOutput(AbstractProgram& out); 41 protected: 42 //! Checks whether stream starts with a valid token. 43 virtual bool doAttach(bool& inc); 44 //! Attempts to parses the current step or throws an exception on error. 45 /*! 46 * The function calls beginStep()/endStep() on the associated 47 * output object before/after parsing the current step. 48 */ 49 virtual bool doParse(); 50 //! Parses statements until next step directive or input is exhausted. 51 bool parseStatements(); 52 private: 53 void skipws(); 54 bool matchDirective(); 55 void matchRule(char peek); 56 void matchAtoms(const char* seps); 57 void matchLits(); 58 void matchCondition(); 59 void matchAgg(); 60 bool match(const char* ts, bool required = true); 61 Atom_t matchId(); 62 Lit_t matchLit(); 63 int matchInt(); 64 void matchTerm(); 65 void matchAtomArg(); 66 void matchStr(); 67 void push(char c); 68 AbstractProgram* out_; 69 struct Data; 70 Data* data_; 71 }; 72 73 //! Class for writing logic programs in ground text format. 74 /*! 75 * Writes a logic program in human-readable text format. 76 * \ingroup WriteType 77 */ 78 class AspifTextOutput : public Potassco::AbstractProgram { 79 public: 80 AspifTextOutput(std::ostream& os); 81 ~AspifTextOutput(); 82 virtual void initProgram(bool incremental); 83 virtual void beginStep(); 84 virtual void rule(Head_t ht, const AtomSpan& head, const LitSpan& body); 85 virtual void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits); 86 virtual void minimize(Weight_t prio, const WeightLitSpan& lits); 87 virtual void output(const StringSpan& str, const LitSpan& cond); 88 virtual void external(Atom_t a, Value_t v); 89 virtual void assume(const LitSpan& lits); 90 virtual void project(const AtomSpan& atoms); 91 virtual void acycEdge(int s, int t, const LitSpan& condition); 92 virtual void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition); 93 94 virtual void theoryTerm(Id_t termId, int number); 95 virtual void theoryTerm(Id_t termId, const StringSpan& name); 96 virtual void theoryTerm(Id_t termId, int compound, const IdSpan& args); 97 virtual void theoryElement(Id_t elementId, const IdSpan& terms, const LitSpan& cond); 98 virtual void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements); 99 virtual void theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements, Id_t op, Id_t rhs); 100 virtual void endStep(); 101 102 void addAtom(Atom_t id, const StringSpan& str); 103 private: 104 std::ostream& printName(std::ostream& os, Lit_t lit) const; 105 void writeDirectives(); 106 void visitTheories(); 107 AspifTextOutput& push(uint32_t x); 108 AspifTextOutput& push(const AtomSpan& atoms); 109 AspifTextOutput& push(const LitSpan& lits); 110 AspifTextOutput& push(const WeightLitSpan& wlits); 111 template <class T> T get(); 112 AspifTextOutput(const AspifTextOutput&); 113 AspifTextOutput& operator=(const AspifTextOutput&); 114 std::ostream& os_; 115 struct Data; 116 TheoryData theory_; 117 Data* data_; 118 int step_; 119 }; 120 121 //! Converts a given theory atom to a string. 122 class TheoryAtomStringBuilder { 123 public: 124 std::string toString(const TheoryData& td, const TheoryAtom& a); 125 private: add(char c)126 TheoryAtomStringBuilder& add(char c) { res_.append(1, c); return *this; } add(const char * s)127 TheoryAtomStringBuilder& add(const char* s) { res_.append(s); return *this; } add(const std::string & s)128 TheoryAtomStringBuilder& add(const std::string& s) { res_.append(s); return *this; } 129 TheoryAtomStringBuilder& term(const TheoryData& td, const TheoryTerm& a); 130 TheoryAtomStringBuilder& element(const TheoryData& td, const TheoryElement& a); 131 bool function(const TheoryData& td, const TheoryTerm& f); 132 133 virtual LitSpan getCondition(Id_t condId) const = 0; 134 virtual std::string getName(Atom_t atomId) const = 0; 135 std::string res_; 136 }; 137 138 } // namespace Potassco 139 #endif 140