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 ACU_GndLhsAutomaton.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "indent.hh"
30 #include "vector.hh"
31
32 // forward declarations
33 #include "interface.hh"
34 #include "core.hh"
35 #include "variable.hh"
36 #include "ACU_Persistent.hh"
37 #include "ACU_Theory.hh"
38
39 // interface class definitions
40 #include "associativeSymbol.hh"
41 #include "dagNode.hh"
42 #include "term.hh"
43 #include "extensionInfo.hh"
44
45 // core class definitions
46 #include "substitution.hh"
47
48 // ACU Red-Black class definitions
49 #include "ACU_SlowIter.hh"
50
51 // ACU theory class definitions
52 #include "ACU_Symbol.hh"
53 #include "ACU_DagNode.hh"
54 #include "ACU_GndLhsAutomaton.hh"
55 #include "ACU_TreeDagNode.hh"
56
ACU_GndLhsAutomaton(ACU_Symbol * symbol,bool matchAtTop,bool collapsePossible,int nrVariables,Term * stripperTerm,VariableTerm * collector)57 ACU_GndLhsAutomaton::ACU_GndLhsAutomaton(ACU_Symbol* symbol,
58 bool matchAtTop,
59 bool collapsePossible,
60 int nrVariables,
61 Term* stripperTerm,
62 VariableTerm* collector)
63 : ACU_CollectorLhsAutomaton(symbol,
64 matchAtTop,
65 collapsePossible,
66 nrVariables,
67 collector),
68 stripperTerm(stripperTerm)
69 {
70 Assert(stripperTerm->ground(), "stripper term must be ground");
71 }
72
73 bool
match(DagNode * subject,Substitution & solution,Subproblem * & returnedSubproblem,ExtensionInfo * extensionInfo)74 ACU_GndLhsAutomaton::match(DagNode* subject,
75 Substitution& solution,
76 Subproblem*& returnedSubproblem,
77 ExtensionInfo* extensionInfo)
78 {
79 if (collectorFree(solution))
80 {
81 if (subject->symbol() == getSymbol())
82 {
83 //
84 // Non-collapse case.
85 //
86 if (safeCast(ACU_BaseDagNode*, subject)->isTree())
87 {
88 //
89 // Red-black case.
90 //
91 ACU_TreeDagNode* s = safeCast(ACU_TreeDagNode*, subject);
92 ACU_SlowIter i;
93 if (!(s->getTree().find(stripperTerm, i)))
94 return false;
95 if (collect(i, s, solution))
96 {
97 returnedSubproblem = 0;
98 if (extensionInfo)
99 {
100 extensionInfo->setValidAfterMatch(true);
101 extensionInfo->setMatchedWhole(true);
102 }
103 return true;
104 }
105 }
106 else
107 {
108 //
109 // ArgVec case.
110 //
111 ACU_DagNode* s = safeCast(ACU_DagNode*, subject);
112 int pos = s->binarySearch(stripperTerm);
113 if (pos < 0)
114 return false;
115 if (collect(pos, s, solution))
116 {
117 returnedSubproblem = 0;
118 if (extensionInfo)
119 {
120 extensionInfo->setValidAfterMatch(true);
121 extensionInfo->setMatchedWhole(true);
122 }
123 return true;
124 }
125 }
126 if (extensionInfo == 0)
127 return false; // no extension implies true failure
128 }
129 else
130 {
131 //
132 // Collapse case.
133 //
134 if (!getCollapsePossible())
135 return false;
136 Assert(extensionInfo == 0 &&
137 subject->getSortIndex() != Sort::SORT_UNKNOWN,
138 "collapse to top not handled by ACU_GndLhsAutomaton");
139 if (!(stripperTerm->equal(subject)))
140 return false;
141 returnedSubproblem = 0;
142 collapse(solution);
143 return true;
144 }
145 }
146 return ACU_LhsAutomaton::match(subject, solution, returnedSubproblem, extensionInfo);
147 }
148
149 #ifdef DUMP
150 void
dump(ostream & s,const VariableInfo & variableInfo,int indentLevel)151 ACU_GndLhsAutomaton::dump(ostream& s, const VariableInfo& variableInfo, int indentLevel)
152 {
153 s << Indent(indentLevel) << "Begin{ACU_GndLhsAutomaton}\n";
154 ++indentLevel;
155 s << Indent(indentLevel) << "stripperTerm = \"" << stripperTerm << '\n';
156 ACU_CollectorLhsAutomaton::dump(s, variableInfo, indentLevel);
157 s << Indent(indentLevel - 1) << "End{ACU_GndLhsAutomaton}\n";
158 }
159 #endif
160