1 /* 2 3 This file is part of the Maude 2 interpreter. 4 5 Copyright 1997-2014 SRI International, Menlo Park, CA 94025, USA. 6 7 This program is free software; you can redistribute it and/or modify 8 it under the terms of the GNU General Public License as published by 9 the Free Software Foundation; either version 2 of the License, or 10 (at your option) any later version. 11 12 This program is distributed in the hope that it will be useful, 13 but WITHOUT ANY WARRANTY; without even the implied warranty of 14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15 GNU General Public License for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software 19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. 20 21 */ 22 23 // 24 // Class to implement a modified PIG-PUG to solve 25 // associative unification problems with constraints on variables. 26 // 27 // An equation is strict left linear if each variable in the lhs is 28 // either constrained or occurs exactly once in the equation. PIG-PUG 29 // can be shown to terminate on such equation with a finite complete 30 // set of unifiers. 31 // 32 // For other equations we resort to incomplete methods to ensure termination. 33 // 34 35 #ifndef _pigPug_hh_ 36 #define _pigPug_hh_ 37 #include <list> 38 #include <map> 39 #include <vector> 40 #include "natSet.hh" 41 42 class PigPug 43 { 44 public: 45 enum OutcomeFlags 46 { 47 FAILURE = 0, // no solution found 48 SUCCESS = 1, // solution was found 49 INCOMPLETE = 2 // solutions may have been missed 50 }; 51 52 typedef pair<int, int> ResultPair; // <outcome flags, next fresh variable> 53 54 enum Constraints 55 { 56 ELEMENT = -2, 57 }; 58 // 59 // Constraint for each variable is ELEMENT, NONE or non-negative integer indexing a (collapse-free) theory. 60 // 61 typedef Vector<int> ConstraintMap; 62 63 typedef Vector<int> Word; 64 typedef Vector<Word> Subst; 65 66 PigPug(const Word& lhs, 67 const Word& rhs, 68 const ConstraintMap& constraintMap, 69 int lastOriginalVariable, 70 int freshVariableStart, 71 bool strictLeftLinear); 72 // 73 // Returns NONE, or the index for the next unused variable, and fills out unifier. 74 // 75 ResultPair getNextUnifier(Subst& unifier); 76 77 #ifdef DUMP 78 static void dumpWord(ostream& s, const Word& word); 79 #endif 80 81 private: 82 enum Moves 83 { 84 INC_RHS = 1, 85 INC_LHS = 2, 86 MOVES = INC_RHS | INC_LHS, 87 BOTH = INC_RHS | INC_LHS, 88 // 89 // 3 basic moves. 90 // 91 // RHS_PEEL = 1, 92 // LHS_PEEL = 2, 93 // EQUATE = 3, 94 // 95 // We OR this flag with EQUATE to indicate that the rhs variable 96 // was instantiated rather than the lhs variable (the usual case). 97 // This happens when the rhs variable is strictly less constrained 98 // than the lhs variable. 99 // 100 RHS_ASSIGN = 4, 101 // 102 // We OR this flag with RHS_PEEL or EQUATE to record the fact 103 // that a modified lhs unificand was pushed on the stack. 104 // 105 PUSH_LHS = 8, 106 // 107 // We OR this flag with LHS_PEEL or EQUATE to record the fact 108 // that a modified rhs unificand was pushed on the stack. 109 // 110 PUSH_RHS = 16, 111 // 112 // We OR this flag with EQUATE to indicate a canceling of equal variables. 113 // We need in the cycle detection case so we don't try to pop a state 114 // that doesn't exist. 115 // 116 CANCEL = 32 117 }; 118 119 enum SpecialValues 120 { 121 DELIMITER = -1 // no variable can have this value 122 }; 123 124 enum Result 125 { 126 NOT_ENTERED = -1, // for cycle detection version only, we didn't enter the state 127 FAIL = 0, // move failed 128 LHS_DONE = 1, // move reduced lhs (and possibly rhs) to a single variable 129 RHS_DONE = 2, // move reduced rhs (but not lhs) to a single variable 130 OK = 4 // move succeeded without hitting an end case 131 }; 132 133 struct Unificand 134 { 135 int index; // to record the size of the cancelled prefix 136 Word word; // the word of variables 137 }; 138 139 140 typedef list<Unificand> UnificandStack; 141 typedef Vector<int> Path; 142 typedef Vector<int> VariableRenaming; 143 // 144 // Cycle detection data structures 145 // 146 typedef vector<int> CombinedWord; // use STL vector in order to have comparison 147 typedef map<CombinedWord, int> WordMap; 148 typedef Vector<int> StateStack; 149 150 struct StateInfo 151 { 152 bool onStack; 153 bool onCycle; 154 bool onLivePath; 155 }; 156 // 157 // PIG-PUG with cycle detection functions. 158 // 159 void makeStateKey(CombinedWord& stateKey); 160 bool variableOccurrencesBoundedBy2(const Word& lhs, const Word& rhs, int maxVarNumber); 161 int firstMoveWithCycleDetection(); 162 int nextMoveWithCycleDetection(); 163 int runWithCycleDetection(int result); 164 bool arrive(const CombinedWord& word); 165 void depart(); 166 void confirmedLive(); 167 // 168 // PIG-PUG without cycle detection functions. 169 // 170 int firstMove(); 171 int nextMove(); 172 int run(int result); 173 // 174 // Stuff for general case. 175 // 176 Result lhsPeelGeneralCase(); 177 Result rhsPeelGeneralCase(); 178 bool feasibleGeneralCase(); 179 bool canCancelUnconstrained(const Unificand& big, const Unificand& small); 180 // 181 // Stuff for strict left-linear case. 182 // 183 Result lhsPeel(); 184 Result rhsPeel(); 185 bool feasible(); 186 bool fullyConstrained(const Unificand& unificand); 187 // 188 // Common code. 189 // 190 Result cancel(); 191 Result equate(); 192 bool checkUnificand(UnificandStack& unificandStack, int oldVar, int newVar); 193 bool checkUnificand2(UnificandStack& unificandStack, int oldVar, int newVar, int offset); 194 int undoMove(); 195 bool occurs(int variable, const Unificand& unificand); 196 int completed(int status); 197 // 198 // Unifier extraction code. 199 // 200 int extractUnifier(Subst& unifier); 201 void compose(Subst& subst, int oldVar, int replacement); 202 void compose2(Subst& subst, int oldVar, int replacement); 203 void compose(Subst& subst, int oldVar, const Word& replacement, int index); 204 void renameVariables(Subst& subst, const VariableRenaming& variableRenaming); 205 void collectRangeVariables(const Subst& subst, NatSet& occursInRange); 206 207 #ifdef DUMP 208 void dump(ostream& s, Subst& subst); 209 #endif 210 211 const ConstraintMap& constraintMap; 212 const int lastOriginalVariable; 213 const int freshVariableStart; 214 const bool strictLeftLinear; 215 bool cycleDetection; // true means we will use cycle detection 216 int depthBound; // NONE means we will fully explore the search tree 217 int incompletenessFlag; // 0 or INCOMPLETE 218 219 UnificandStack lhsStack; 220 UnificandStack rhsStack; 221 Path path; 222 // 223 // Cycle detection data. 224 // 225 WordMap wordMap; 226 Vector<StateInfo> stateInfo; 227 StateStack traversalStack; 228 }; 229 230 #endif 231