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 RewriteSearchState.
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
35 // interface class definitions
36 #include "symbol.hh"
37 #include "dagNode.hh"
38
39 // core class definitions
40 #include "rewritingContext.hh"
41 #include "rhsAutomaton.hh"
42 #include "rule.hh"
43 #include "rewriteSearchState.hh"
44
RewriteSearchState(RewritingContext * context,int label,int flags,int minDepth,int maxDepth)45 RewriteSearchState::RewriteSearchState(RewritingContext* context,
46 int label,
47 int flags,
48 int minDepth,
49 int maxDepth)
50 : SearchState(context, flags | RESPECT_FROZEN, minDepth, maxDepth),
51 label(label),
52 withExtension(maxDepth >= 0)
53 {
54 Assert(label == NONE || !(getFlags() & SET_UNREWRITABLE),
55 "shouldn't set unrewritable flag if only looking at rules with a given label");
56 ruleIndex = -1;
57 }
58
59 bool
findNextRewrite()60 RewriteSearchState::findNextRewrite()
61 {
62 bool rewriteSeenAtCurrentPosition;
63 if (ruleIndex > -1)
64 {
65 if (findNextSolution())
66 return true;
67 rewriteSeenAtCurrentPosition = true;
68 }
69 else
70 {
71 if (!findNextPosition())
72 return false;
73 rewriteSeenAtCurrentPosition = false;
74 }
75 ++ruleIndex;
76 bool allowNonexec = getFlags() & ALLOW_NONEXEC;
77 do
78 {
79 DagNode* d = getDagNode();
80 if (!(d->isUnrewritable()))
81 {
82 const Vector<Rule*>& rules = d->symbol()->getRules();
83 for (int nrRules = rules.length(); ruleIndex < nrRules; ruleIndex++)
84 {
85 Rule* rl = rules[ruleIndex];
86 if ((allowNonexec || !(rl->isNonexec())) &&
87 (label == UNDEFINED || rl->getLabel().id() == label))
88 {
89 LhsAutomaton* a = withExtension ? rl->getExtLhsAutomaton() :
90 rl->getNonExtLhsAutomaton();
91 if (findFirstSolution(rl, a))
92 return true;
93 }
94 }
95 if (!rewriteSeenAtCurrentPosition && (getFlags() & SET_UNREWRITABLE))
96 d->setUnrewritable();
97 }
98 rewriteSeenAtCurrentPosition = false;
99 ruleIndex = 0;
100 }
101 while (findNextPosition());
102 return false;
103 }
104
105 Rule*
getRule() const106 RewriteSearchState::getRule() const
107 {
108 return (getDagNode()->symbol()->getRules())[ruleIndex];
109 }
110
111 DagNode*
getReplacement() const112 RewriteSearchState::getReplacement() const
113 {
114 return getRule()->getRhsBuilder().construct(*(getContext()));
115 }
116