1 // 2 // Copyright (c) 2006-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 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 25 #ifndef CLASP_PREPROCESSOR_H_INCLUDED 26 #define CLASP_PREPROCESSOR_H_INCLUDED 27 28 #ifdef _MSC_VER 29 #pragma once 30 #endif 31 #include <clasp/claspfwd.h> 32 #include <clasp/literal.h> 33 namespace Clasp { namespace Asp { 34 35 /** 36 * \addtogroup asp 37 */ 38 //@{ 39 40 //! Preprocesses (i.e. simplifies) a logic program. 41 /*! 42 * Preprocesses (i.e. simplifies) a logic program and associates variables with 43 * the nodes of the simplified logic program. 44 */ 45 class Preprocessor { 46 public: Preprocessor()47 Preprocessor() : prg_(0), dfs_(true) {} 48 //! Possible eq-preprocessing types. 49 enum EqType { 50 no_eq, //!< No eq-preprocessing, associate a new var with each supported atom and body. 51 full_eq //!< Check for all kinds of equivalences between atoms and bodies. 52 }; 53 program()54 const LogicProgram* program() const { return prg_; } program()55 LogicProgram* program() { return prg_; } 56 57 //! Starts preprocessing of the logic program. 58 /*! 59 * Computes the maximum consequences of prg and associates a variable 60 * with each supported atom and body. 61 * \param prg The logic program to preprocess. 62 * \param t Type of eq-preprocessing. 63 * \param maxIters If t == full_eq, maximal number of iterations during eq preprocessing. 64 * \param dfs If t == full_eq, classify in df-order (true) or bf-order (false). 65 */ 66 bool preprocess(LogicProgram& prg, EqType t, uint32 maxIters, bool dfs = true) { 67 prg_ = &prg; 68 dfs_ = dfs; 69 type_ = t; 70 return t == full_eq 71 ? preprocessEq(maxIters) 72 : preprocessSimple(); 73 } 74 eq()75 bool eq() const { return type_ == full_eq; } getRootAtom(Literal p)76 Var getRootAtom(Literal p) const { return p.id() < litToNode_.size() ? litToNode_[p.id()] : varMax; } setRootAtom(Literal p,uint32 atomId)77 void setRootAtom(Literal p, uint32 atomId) { 78 if (p.id() >= litToNode_.size()) litToNode_.resize(p.id()+1, varMax); 79 litToNode_[p.id()] = atomId; 80 } 81 private: 82 Preprocessor(const Preprocessor&); 83 Preprocessor& operator=(const Preprocessor&); 84 bool preprocessEq(uint32 maxIters); 85 bool preprocessSimple(); 86 // ------------------------------------------------------------------------ 87 typedef PrgHead* const * HeadIter; 88 typedef std::pair<HeadIter,HeadIter> HeadRange; 89 // Eq-Preprocessing 90 struct BodyExtra { BodyExtraBodyExtra91 BodyExtra() : known(0), mBody(0), bSeen(0) {} 92 uint32 known :30; // Number of predecessors already classified, only used for bodies 93 uint32 mBody : 1; // A flag for marking bodies 94 uint32 bSeen : 1; // First time we see this body? 95 }; 96 bool classifyProgram(const VarVec& supportedBodies); 97 ValueRep simplifyClassifiedProgram(const HeadRange& atoms, bool more, VarVec& supported); 98 PrgBody* addBodyVar(uint32 bodyId); 99 bool addHeadsToUpper(PrgBody* body); 100 bool addHeadToUpper(PrgHead* head, PrgEdge support); 101 bool propagateAtomVar(PrgAtom*, PrgEdge source); 102 bool propagateAtomValue(PrgAtom*, ValueRep val, PrgEdge source); 103 bool mergeEqBodies(PrgBody* b, Var rootId, bool equalLits); 104 bool hasRootLiteral(PrgBody* b) const; 105 bool superfluous(PrgBody* b) const; 106 ValueRep simplifyHead(PrgHead* h, bool reclassify); 107 ValueRep simplifyBody(PrgBody* b, bool reclassify, VarVec& supported); nextBodyId(VarVec::size_type & idx)108 uint32 nextBodyId(VarVec::size_type& idx) { 109 if (follow_.empty() || idx == follow_.size()) { return varMax; } 110 if (dfs_) { 111 uint32 id = follow_.back(); 112 follow_.pop_back(); 113 return id; 114 } 115 return follow_[idx++];; 116 } 117 // ------------------------------------------------------------------------ 118 typedef PodVector<BodyExtra>::type BodyData; 119 LogicProgram* prg_; // program to preprocess 120 VarVec follow_; // bodies yet to classify 121 BodyData bodyInfo_; // information about the program nodes 122 VarVec litToNode_;// the roots of our equivalence classes 123 uint32 pass_; // current iteration number 124 uint32 maxPass_; // force stop after maxPass_ iterations 125 EqType type_; // type of eq-preprocessing 126 bool dfs_; // classify bodies in DF or BF order 127 }; 128 //@} 129 } } 130 #endif 131 132