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 // Class to store and simplify a level in the solution of a word system.
25 //
26 // A level constains a map from variable to constraints, partial solution and a set
27 // of unsolved equations.
28 //
29 // As we solve equations, we may introduce new variables, or in the worst case
30 // constrain existing variables to ensure termination. We will generate bindings
31 // for unbound variables, and substitute new bindings into existing bindings
32 // and unsolved equations.
33 //
34 // Whenever we make a nondeterministic choice we need a new level so we can backtrack
35 // to the old level to consider the other choices.
36 //
37 #include <list>
38 #include <map>
39 #include "pigPug.hh"
40
41 #ifndef _wordLevel_hh_
42 #define _wordLevel_hh_
43
44 class WordLevel
45 {
46 public:
47 enum OutcomeFlags
48 {
49 FAILURE = 0, // no solution found
50 SUCCESS = 1, // solution was found
51 INCOMPLETE = 2 // solutions may have been missed
52 };
53
54 typedef pair<int, WordLevel*> ResultPair;
55 //
56 // Local names for PigPug data types.
57 //
58 typedef PigPug::Word Word;
59 typedef PigPug::Subst Subst;
60 typedef PigPug::ConstraintMap ConstraintMap;
61
62 WordLevel(int nrVariables, int nrEquations);
63 ~WordLevel();
64
65 void addConstraint(int variable, int constraint);
66 void addAssignment(int variable, const Word& value);
67 void addEquation(int index, const Word& lhs, const Word& rhs);
68
69 ResultPair findNextPartialSolution();
70 const Word& getAssignment(int variable) const;
71 int getNrVariables() const;
72
73 bool simplify();
74
75 void dump(ostream& s, int indentLevel = 0);
76 void dumpWord(ostream& s, const Word& word);
77
78 private:
79 enum Result
80 {
81 FAIL, // occur-check fail or constraint clash - need to fall back to last decision point
82 DONE, // successful completion, no change to partial solution
83 CHANGED, // successful completion, partial solution changed
84 CONTINUE // successful step, maybe more work to do
85 };
86
87 enum EquationIndex
88 {
89 NOT_YET_CHOSEN = -2 // initial value; we use NONE (= -1) if there is no equation to chose
90 };
91
92 struct Equation
93 {
94 Word lhs;
95 Word rhs;
96 };
97
98 typedef Vector<Equation> EquationVec;
99
100 WordLevel* makeNewLevel(const Subst& unifier, int nextFreshVariable);
101 bool chooseEquation();
102 void checkUnconstrainedVariables(const Word& word, NatSet& occurs, NatSet& nonlinear);
103 void makePigPug(bool strictLeftLinear);
104 //
105 // Functions for simplifying partial solution.
106 //
107 bool fullyExpandAssignments();
108 Result expandAssignments();
109 Result expandAssignment(int var, Word& word);
110 bool reallyExpandAssignment(int var,
111 Word& word,
112 Word::const_iterator firstToExpand,
113 const Word& expansion);
114 bool append(Word& newWord, const Word& word, int var);
115 //
116 // Functions for simplifying equations.
117 //
118 Result simplifyEquations();
119 Result simplifyEquation(Equation& equation);
120 void expandWord(Word& newWord, const Word& oldWord);
121 void append(Word& newWord, const Word& word);
122 void updateRemainder(Word& word, int leftCursor, int rightCursor);
123 Result cancel(int lhsVar, int rhsVar);
124 Result checkForSingleton(const Word& newLhs, int lhsLeftCursor, int lhsRightCursor,
125 const Word& newRhs, int rhsLeftCursor, int rhsRightCursor);
126 Result unifyVariables(int lhsVar, int rhsVar);
127 Result makeAssignment(int variable, const Word& source, int leftCursor, int rightCursor);
128 void copyBack(Word& destination, const Word& source, int leftCursor, int rightCursor);
129
130
131 ConstraintMap constraintMap;
132 Subst partialSolution;
133 EquationVec unsolvedEquations;
134 //
135 // If there are unsolved equations we need to pick one and solve it with PigPug.
136 //
137 int chosenEquation;
138 PigPug* pigPug;
139 int incompletenessFlag; // to record the use of a transformation that does not preserve completeness
140 };
141
142 inline void
addConstraint(int variable,int constraint)143 WordLevel::addConstraint(int variable, int constraint)
144 {
145 constraintMap[variable] = constraint;
146 }
147
148 inline void
addAssignment(int variable,const Word & value)149 WordLevel::addAssignment(int variable, const Word& value)
150 {
151 Word& rhs = partialSolution[variable];
152 if (rhs.size() == 1 && rhs[0] == variable)
153 partialSolution[variable] = value; // deep copy
154 else
155 {
156 //
157 // Already have an assignement for variable so turn extra assignment into an equation.
158 //
159 int nrEquations = unsolvedEquations.size();
160 unsolvedEquations.expandBy(1);
161 addEquation(nrEquations, value, rhs);
162 }
163 }
164
165 inline void
addEquation(int index,const Word & lhs,const Word & rhs)166 WordLevel::addEquation(int index, const Word& lhs, const Word& rhs)
167 {
168 Equation& e = unsolvedEquations[index];
169 e.lhs = lhs; // deep copy
170 e.rhs = rhs; // deep copy
171 }
172
173 inline const WordLevel::Word&
getAssignment(int variable) const174 WordLevel::getAssignment(int variable) const
175 {
176 return partialSolution[variable];
177 }
178
179 inline int
getNrVariables() const180 WordLevel::getNrVariables() const
181 {
182 return partialSolution.size();
183 }
184
185 #endif
186