1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2015 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 // Implementation for class WordSystem.
25 //
26 #include "macros.hh"
27 #include "vector.hh"
28 #include "wordLevel.hh"
29 #include "indent.hh"
30 #include "natSet.hh"
31
32 // our stuff
33 #include "wordLevel-simplifyAssignments.cc"
34 #include "wordLevel-simplifyEquations.cc"
35
WordLevel(int nrVariables,int nrEquations)36 WordLevel::WordLevel(int nrVariables, int nrEquations)
37 : constraintMap(nrVariables),
38 partialSolution(nrVariables),
39 unsolvedEquations(nrEquations)
40 {
41 //
42 // Unbound variables must be bound to themselves; by default variables are unconstrained.
43 //
44 for (int i = 0; i < nrVariables; ++i)
45 {
46 partialSolution[i].append(i);
47 constraintMap[i] = NONE;
48 }
49 chosenEquation = NOT_YET_CHOSEN;
50 pigPug = 0;
51 incompletenessFlag = 0;
52 }
53
~WordLevel()54 WordLevel::~WordLevel()
55 {
56 delete pigPug;
57 }
58
59 WordLevel::ResultPair
findNextPartialSolution()60 WordLevel::findNextPartialSolution()
61 {
62 if (chosenEquation == NOT_YET_CHOSEN)
63 {
64 //
65 // Must be first call.
66 //
67 if (!simplify())
68 return ResultPair(FAILURE, 0); // occurs check failure or constraint clash during simplification
69 //
70 // Need to chose an equation and create a PigPug.
71 //
72 bool strictLeftLinear = chooseEquation();
73 if (chosenEquation == NONE)
74 return ResultPair(SUCCESS, 0); // no equations left to solve
75 makePigPug(strictLeftLinear);
76 }
77 if (pigPug == 0)
78 return ResultPair(FAILURE, 0); // must have already returned the unique solution
79 //
80 // Get next PigPug solution; create a new WordLevel.
81 //
82 Subst unifier;
83 PigPug::ResultPair result = pigPug->getNextUnifier(unifier);
84 int nextFreshVariable = result.second;
85 if (nextFreshVariable == NONE)
86 return ResultPair(result.first, 0); // failure
87
88 WordLevel* next = makeNewLevel(unifier, nextFreshVariable);
89 return ResultPair(result.first, next);
90 }
91
92 bool
simplify()93 WordLevel::simplify()
94 {
95 //
96 // We start by simplifying the partial solution.
97 //
98 if (!fullyExpandAssignments())
99 return false;
100 //
101 // Then we simplify the equations until there is no change in the partial solution.
102 //
103 for (;;)
104 {
105 Result result = simplifyEquations();
106 if (result == FAIL)
107 return false;
108 if (result == DONE)
109 break;
110 }
111 return true;
112 }
113
114 WordLevel*
makeNewLevel(const Subst & unifier,int nextFreshVariable)115 WordLevel::makeNewLevel(const Subst& unifier, int nextFreshVariable)
116 {
117 //
118 // We have a PigPug solution - need to copy old stuff and new solution into a new WordLevel object.
119 //
120 int equationCount = 0;
121 FOR_EACH_CONST(i, EquationVec, unsolvedEquations)
122 {
123 if (!(i->lhs.empty()))
124 ++equationCount;
125 }
126 WordLevel* newLevel = new WordLevel(nextFreshVariable, equationCount - 1);
127 //
128 // Copy in old information and unifier.
129 //
130 int nrConstraints = constraintMap.size();
131 for (int i = 0; i < nrConstraints; ++i)
132 newLevel->addConstraint(i, constraintMap[i]);
133 int nrVariables = partialSolution.size();
134 for (int i = 0; i < nrVariables; ++i)
135 {
136 const Word& u = unifier[i];
137 if (u.size() != 1 || u[0] != i)
138 newLevel->addAssignment(i, u);
139 else
140 newLevel->addAssignment(i, partialSolution[i]);
141 }
142 int equationIndex = 0;
143 int nrEquations = unsolvedEquations.size();
144 for (int i = 0; i < nrEquations; ++i)
145 {
146 if (i != chosenEquation)
147 {
148 Equation& e = unsolvedEquations[i];
149 if (!(e.lhs.empty()))
150 {
151 newLevel->addEquation(equationIndex, e.lhs, e.rhs);
152 ++equationIndex;
153 }
154 }
155 }
156 return newLevel;
157 }
158
159 bool
chooseEquation()160 WordLevel::chooseEquation()
161 {
162 //
163 // Chosen an unsolved equation and set chosenEquation to it true.
164 // If there are no unsolved equations set chosenEquation to NONE.
165 // Returns true if chosen equation is strict left-linear and false otherwise.
166 //
167 chosenEquation = NONE; // if we don't find one
168 int nrEquations = unsolvedEquations.size();
169 for (int i = 0; i < nrEquations; ++i)
170 {
171 Equation& e = unsolvedEquations[i];
172 if (!(e.lhs.empty()))
173 {
174 //
175 // Examine unconstrained variables.
176 //
177 NatSet lhsOccurs;
178 NatSet lhsNonlinear;
179 checkUnconstrainedVariables(e.lhs, lhsOccurs, lhsNonlinear);
180 NatSet rhsOccurs;
181 NatSet rhsNonlinear;
182 checkUnconstrainedVariables(e.rhs, rhsOccurs, rhsNonlinear);
183 if (lhsOccurs.disjoint(rhsOccurs))
184 {
185 if (lhsNonlinear.empty())
186 {
187 //
188 // We found a strict left-linear equation so choose it.
189 //
190 chosenEquation = i;
191 return true;
192 }
193 if (rhsNonlinear.empty())
194 {
195 //
196 // We found a strict right-linear equation so flip it into a
197 // strict left-linear equation and choose it.
198 //
199 e.lhs.swap(e.rhs);
200 chosenEquation = i;
201 return true;
202 }
203 chosenEquation = i; // prefer an equation with disjoint lhs/rhs variable sets
204 }
205 if (chosenEquation == NONE)
206 chosenEquation = i; // we'll take this one if we don't see anything better
207 }
208 }
209 return false; // we didn't find a strict left-linear equation
210 }
211
212 void
checkUnconstrainedVariables(const Word & word,NatSet & occurs,NatSet & nonlinear)213 WordLevel::checkUnconstrainedVariables(const Word& word, NatSet& occurs, NatSet& nonlinear)
214 {
215 FOR_EACH_CONST(i, Word, word)
216 {
217 int index = *i;
218 if (constraintMap[index] == NONE)
219 {
220 if (occurs.contains(index))
221 nonlinear.insert(index);
222 else
223 occurs.insert(index);
224 }
225 }
226 }
227
228 void
makePigPug(bool strictLeftLinear)229 WordLevel::makePigPug(bool strictLeftLinear)
230 {
231 Equation& e = unsolvedEquations[chosenEquation];
232 int nrVariables = partialSolution.size();
233 pigPug = new PigPug(e.lhs, e.rhs, constraintMap, nrVariables - 1, nrVariables, strictLeftLinear);
234 }
235
236 void
dump(ostream & s,int indentLevel)237 WordLevel::dump(ostream& s, int indentLevel)
238 {
239 s << Indent(indentLevel) << "begin{WordLevel}" << endl;
240 {
241 s << Indent(indentLevel + 1) << "constraintMap = " << endl;
242 int nrVariables = constraintMap.size();
243 for (int i = 0; i < nrVariables; ++i)
244 {
245 s << Indent(indentLevel + 2) << "X" << i << " : ";
246 int c = constraintMap[i];
247 if (c == PigPug::ELEMENT)
248 s << "ELEMENT";
249 else if (c == NONE)
250 s << "NONE";
251 else
252 s << "theory" << c;
253 s << endl;
254 }
255 }
256 {
257 s << Indent(indentLevel + 1) << "partialSolution = " << endl;
258 int nrVariables = partialSolution.size();
259 for (int i = 0; i < nrVariables; ++i)
260 {
261 s << Indent(indentLevel + 2) << "x" << i << " |-> ";
262 dumpWord(s, partialSolution[i]);
263 s << endl;
264 }
265 }
266 {
267 s << Indent(indentLevel + 1) << "unsolvedEquations = " << endl;
268 int nrEquations = unsolvedEquations.size();
269 for (int i = 0; i < nrEquations; ++i)
270 {
271 s << Indent(indentLevel + 2) << "e" << i << " : ";
272 if (unsolvedEquations[i].lhs.empty())
273 s << "(cancelled)" << endl;
274 else
275 {
276 dumpWord(s, unsolvedEquations[i].lhs);
277 s << " =? ";
278 dumpWord(s, unsolvedEquations[i].rhs);
279 s << endl;
280 }
281 }
282 }
283 }
284
285 void
dumpWord(ostream & s,const Word & word)286 WordLevel::dumpWord(ostream& s, const Word& word)
287 {
288 FOR_EACH_CONST(i, Word, word)
289 s << "x" << *i << " ";
290 }
291