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 VariableSymbol.
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 #include "term.hh"
39
40 // core class definitions
41 #include "sortBdds.hh"
42
43 // variable class definitions
44 #include "variableSymbol.hh"
45 #include "variableTerm.hh"
46 #include "variableDagNode.hh"
47
VariableSymbol(int id)48 VariableSymbol::VariableSymbol(int id)
49 : Symbol(id, 0)
50 {
51 }
52
53 Term*
makeTerm(const Vector<Term * > & args)54 VariableSymbol::makeTerm(const Vector<Term*>& args)
55 {
56 Assert(false, "makeTerm() not useable on variable symbol " << this);
57 return 0;
58 }
59
60 DagNode*
makeDagNode(const Vector<DagNode * > & args)61 VariableSymbol::makeDagNode(const Vector<DagNode*>& args)
62 {
63 Assert(false, "makeDagNode() not useable on variable symbol " << this);
64 return 0;
65 }
66
67 bool
eqRewrite(DagNode * subject,RewritingContext & context)68 VariableSymbol::eqRewrite(DagNode* subject, RewritingContext& context)
69 {
70 return applyReplace(subject, context);
71 }
72
73 void
computeBaseSort(DagNode * subject)74 VariableSymbol::computeBaseSort(DagNode* subject)
75 {
76 subject->setSortIndex(getSort()->index());
77 }
78
79 void
normalizeAndComputeTrueSort(DagNode * subject,RewritingContext & context)80 VariableSymbol::normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context)
81 {
82 fastComputeTrueSort(subject, context);
83 }
84
85 void
stackArguments(DagNode *,Vector<RedexPosition> &,int)86 VariableSymbol::stackArguments(DagNode* /* subject */,
87 Vector<RedexPosition>& /* stack */,
88 int /* parentIndex */)
89 {
90 }
91
92 Term*
termify(DagNode * dagNode)93 VariableSymbol::termify(DagNode* dagNode)
94 {
95 VariableDagNode* v = safeCast(VariableDagNode*, dagNode);
96 return new VariableTerm(this, v->id());
97 }
98
99 //
100 // Unification code.
101 //
102
103 void
computeGeneralizedSort(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & generalizedSort)104 VariableSymbol::computeGeneralizedSort(const SortBdds& sortBdds,
105 const Vector<int>& realToBdd,
106 DagNode* subject,
107 Vector<Bdd>& generalizedSort)
108 {
109 int firstVariable = realToBdd[safeCast(VariableDagNode*, subject)->getIndex()]; // first BDD variable for this variable
110 int nrVariables = sortBdds.getNrVariables(rangeComponent()->getIndexWithinModule()); // number of BDD variables depends on sort
111 sortBdds.makeVariableVector(firstVariable, nrVariables, generalizedSort);
112 }
113
114 void
computeGeneralizedSort2(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & outputBdds)115 VariableSymbol::computeGeneralizedSort2(const SortBdds& sortBdds,
116 const Vector<int>& realToBdd,
117 DagNode* subject,
118 Vector<Bdd>& outputBdds)
119 {
120 sortBdds.appendVariableVector(realToBdd[safeCast(VariableDagNode*, subject)->getIndex()], // first BDD variable
121 sortBdds.getNrVariables(rangeComponent()->getIndexWithinModule()), // # BDD variables
122 outputBdds);
123 }
124
125 bool
isStable() const126 VariableSymbol::isStable() const
127 {
128 return false;
129 }
130
131 //
132 // Hash cons code.
133 //
134
135 DagNode*
makeCanonical(DagNode * original,HashConsSet *)136 VariableSymbol::makeCanonical(DagNode* original, HashConsSet* /* hcs */)
137 {
138 //
139 // No arguments that could be non-canonical so we can make the original
140 // instance into the canonical instance.
141 //
142 return original;
143 }
144
145 DagNode*
makeCanonicalCopy(DagNode * original,HashConsSet *)146 VariableSymbol::makeCanonicalCopy(DagNode* original, HashConsSet* /* hcs */)
147 {
148 //
149 // We have a unreduced node - copy forced - in principle variable could rewrite to something else!
150 //
151 VariableDagNode* v = safeCast(VariableDagNode*, original);
152 VariableDagNode* n = new VariableDagNode(this, v->id(), v->getIndex());
153 n->copySetRewritingFlags(original);
154 n->setSortIndex(original->getSortIndex());
155 return n;
156 }
157