1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 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 RewriteSequenceSearch.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 #include "higher.hh"
35
36 // interface class definitions
37 #include "symbol.hh"
38 #include "dagNode.hh"
39
40 // core class definitions
41 #include "rewritingContext.hh"
42 #include "pattern.hh"
43 #include "rewriteSearchState.hh"
44 #include "rewriteSequenceSearch.hh"
45
46
RewriteSequenceSearch(RewritingContext * initial,SearchType searchType,Pattern * goal,int maxDepth)47 RewriteSequenceSearch::RewriteSequenceSearch(RewritingContext* initial,
48 SearchType searchType,
49 Pattern* goal,
50 int maxDepth)
51 : StateTransitionGraph(initial),
52 goal(goal),
53 maxDepth((searchType == ONE_STEP) ? 1 : maxDepth)
54 {
55 matchState = 0;
56 explore = -1;
57 exploreDepth = -1;
58 firstDeeperNodeNr = 0;
59 needToTryInitialState = (searchType == ANY_STEPS);
60 reachingInitialStateOK = (searchType == AT_LEAST_ONE_STEP || searchType == ONE_STEP);
61 normalFormNeeded = (searchType == NORMAL_FORM);
62 nextArc = NONE;
63 }
64
~RewriteSequenceSearch()65 RewriteSequenceSearch::~RewriteSequenceSearch()
66 {
67 delete matchState;
68 delete goal;
69 }
70
71 bool
findNextMatch()72 RewriteSequenceSearch::findNextMatch()
73 {
74 if (matchState != 0)
75 goto tryMatch; // non-startup case
76
77 for(;;)
78 {
79 stateNr = findNextInterestingState();
80 if (stateNr == NONE)
81 break;
82 matchState = new MatchSearchState(getContext()->makeSubcontext(getStateDag(stateNr)),
83 goal,
84 MatchSearchState::GC_CONTEXT);
85 tryMatch:
86 bool foundMatch = matchState->findNextMatch();
87 matchState->transferCount(*(getContext()));
88 if (foundMatch)
89 return true;
90 delete matchState;
91 }
92
93 matchState = 0;
94 return false;
95 }
96
97 int
findNextInterestingState()98 RewriteSequenceSearch::findNextInterestingState()
99 {
100 if (needToTryInitialState)
101 {
102 //
103 // Special case: return the initail state.
104 //
105 needToTryInitialState = false; // don't do this again
106 return 0;
107 }
108
109 if (nextArc != NONE)
110 goto exploreArcs;
111
112 for(;;)
113 {
114 //
115 // Get next state to explore.
116 //
117 ++explore;
118 if (explore == getNrStates())
119 break;
120 if (explore == firstDeeperNodeNr)
121 {
122 ++exploreDepth;
123 if (normalFormNeeded)
124 {
125 if (maxDepth > 0 && exploreDepth > maxDepth)
126 break;
127 }
128 else
129 {
130 if (exploreDepth == maxDepth)
131 break;
132 }
133 firstDeeperNodeNr = getNrStates();
134 }
135 nextArc = 0;
136
137 exploreArcs:
138 int nrStates = getNrStates();
139 int nextStateNr;
140 while ((nextStateNr = getNextState(explore, nextArc)) != NONE)
141 {
142 ++nextArc;
143 if (normalFormNeeded)
144 {
145 if (exploreDepth == maxDepth)
146 break; // no point looking for further arcs
147 }
148 else
149 {
150 if (nextStateNr == nrStates) // new state reached
151 return nextStateNr;
152 if (nextStateNr == 0 && reachingInitialStateOK)
153 {
154 //
155 // We have arrived back at our initial state, but because
156 // we didn't try matching the initial state, we do it now.
157 //
158 reachingInitialStateOK = false; // don't do this again
159 return 0;
160 }
161 }
162 }
163 if (getContext()->traceAbort())
164 return NONE;
165 if (normalFormNeeded && nextArc == 0)
166 {
167 nextArc = NONE;
168 return explore;
169 }
170 }
171
172 return NONE;
173 }
174
175 Rule*
getStateRule(int stateNr) const176 RewriteSequenceSearch::getStateRule(int stateNr) const
177 {
178 const ArcMap& fwdArcs = getStateFwdArcs(getStateParent(stateNr));
179 return *(fwdArcs.find(stateNr)->second.begin());
180 }
181