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_CONVERT_H_INCLUDED 25 #define POTASSCO_CONVERT_H_INCLUDED 26 27 #include <potassco/smodels.h> 28 namespace Potassco { 29 30 //! Converts a given program so that it can be expressed in smodels format. 31 /*! 32 * \ingroup WriteType 33 */ 34 class SmodelsConvert : public AbstractProgram { 35 public: 36 //! Creates a new object that passes converted programs to out. 37 /*! 38 * The parameter enableClaspExt determines how heuristic, edge, and external 39 * directives are handled. 40 * If true, heuristic and edge directives are converted to _heuristic and 41 * _edge predicates, while external directives passed to out. 42 * Otherwise, heuristic and edge directives are not converted but 43 * directly passed to out, while external directives are mapped to 44 * choice rules or integrity constraints. 45 */ 46 SmodelsConvert(AbstractProgram& out, bool enableClaspExt); 47 ~SmodelsConvert(); 48 //! Calls initProgram() on the associated output program. 49 virtual void initProgram(bool incremental); 50 //! Calls beginStep() on the associated output program. 51 virtual void beginStep(); 52 //! Converts the given rule into one or more smodels rules. 53 virtual void rule(Head_t t, const AtomSpan& head, const LitSpan& body); 54 //! Converts the given rule into one or more smodels rules. 55 virtual void rule(Head_t t, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body); 56 //! Converts literals associated with a priority to a set of corresponding smodels minimize rules. 57 virtual void minimize(Weight_t prio, const WeightLitSpan& lits); 58 //! Adds an atom named str that is equivalent to the condition to the symbol table. 59 virtual void output(const StringSpan& str, const LitSpan& cond); 60 //! Marks the atom that is equivalent to a as external. 61 virtual void external(Atom_t a, Value_t v); 62 //! Adds an _heuristic predicate over the given atom to the symbol table that is equivalent to condition. 63 virtual void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition); 64 //! Adds an _edge(s,t) predicate to the symbol table that is equivalent to condition. 65 virtual void acycEdge(int s, int t, const LitSpan& condition); 66 67 //! Finalizes conversion and calls endStep() on the associated output program. 68 virtual void endStep(); 69 70 //! Returns the output literal associated to in. 71 Lit_t get(Lit_t in) const; 72 //! Returns the name associated with the given (output) smodels atom or 0 if no name exists. 73 const char* getName(Atom_t a) const; 74 //! Returns the max used smodels atom (valid atoms are [1..n]). 75 unsigned maxAtom() const; 76 protected: 77 //! Creates a (named) atom that is equivalent to the given condition. 78 Atom_t makeAtom(const LitSpan& lits, bool named); 79 //! Processes all outstanding conversions. 80 void flush(); 81 //! Converts external atoms. 82 void flushExternal(); 83 //! Converts minimize statements. 84 void flushMinimize(); 85 //! Converts heuristic directives to _heuristic predicates. 86 void flushHeuristic(); 87 //! Converts (atom,name) pairs to output directives. 88 void flushSymbols(); 89 private: 90 SmodelsConvert(const SmodelsConvert&); 91 SmodelsConvert& operator=(const SmodelsConvert&); 92 struct SmData; 93 AbstractProgram& out_; 94 SmData* data_; 95 bool ext_; 96 }; 97 98 } // namespace Potassco 99 #endif 100