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