1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2010 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 // Abstract class for table of operation sort declarations for a symbol.
25 //
26 #ifndef _sortTable_hh_
27 #define _sortTable_hh_
28 #include <set>
29 #include "bdd.hh"
30 #include "opDeclaration.hh"
31 #include "fullCompiler.hh"
32 #include "connectedComponent.hh"
33
34 class SortTable
35 {
36 NO_COPYING(SortTable);
37
38 public:
39 enum CtorStatus
40 {
41 IS_CTOR = 1,
42 IS_NON_CTOR = 2,
43 IS_COMPLEX = IS_CTOR | IS_NON_CTOR
44 };
45
46 SortTable(int arity);
47 int arity() const;
48 void addOpDeclaration(const Vector<Sort*>& domainAndRange,
49 bool constructorFlag);
50 const Vector<OpDeclaration>& getOpDeclarations() const;
51 /* const */ ConnectedComponent* rangeComponent() const;
52 const ConnectedComponent* domainComponent(int argNr) const;
53 Sort* getRangeSort() const;
54 Sort* getSingleNonErrorSort() const;
55 int getCtorStatus() const;
56 virtual void compileOpDeclarations();
57 virtual void fillInSortInfo(Term* subject) = 0;
58 virtual void finalizeSortInfo();
59 virtual bool canProduceErrorSort() const;
60 int traverse(int position, int sortIndex) const;
61 bool kindLevelDeclarationsOnly() const;
62 const NatSet& getMaximalOpDeclSet(Sort* target);
63 //
64 // Unification stuff.
65 //
66 virtual void computeSortFunctionBdds(const SortBdds& sortBdds, Vector<Bdd>& sortFunctionBdds) const;
computeGeneralizedSort(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & generalizedSort)67 virtual void computeGeneralizedSort(const SortBdds& sortBdds,
68 const Vector<int>& realToBdd, // first BDD variable for each free real variable
69 DagNode* subject,
70 Vector<Bdd>& generalizedSort) { CantHappen("not implemented"); }
71
computeGeneralizedSort2(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & generalizedSort)72 virtual void computeGeneralizedSort2(const SortBdds& sortBdds,
73 const Vector<int>& realToBdd, // first BDD variable for each free real variable
74 DagNode* subject,
75 Vector<Bdd>& generalizedSort) { CantHappen("not implemented"); }
76
77 #ifdef COMPILER
78 void generateSortDiagram(CompilationContext& context) const;
79 #endif
80
81 protected:
82 bool specialSortHandling() const;
83 int ctorTraverse(int position, int sortIndex) const;
84
85 #ifdef DUMP
86 void dumpSortDiagram(ostream& s, int indentLevel);
87 #endif
88
89 private:
90 typedef Vector<Bdd> BddVector;
91 typedef Vector<BddVector> BddTable;
92
93 struct Node;
94 struct SpanningTree;
95
96 void buildSortDiagram();
97 void buildCtorDiagram();
98 void sortErrorAnalysis(bool preregProblem,
99 const set<int>& badTerminals);
100 void computeMaximalOpDeclSetTable();
101 bool domainSubsumes(int subsumer, int victim) const;
102 int findStateNumber(Vector<NatSet>& stateSet, const NatSet& state);
103 int findMinSortIndex(const NatSet& state, bool& unique);
104 bool partiallySubsumes(int subsumer, int victim, int argNr);
105 void minimize(NatSet& alive, int argNr);
106
107 void computeBddVector(const SortBdds& sortBdds,
108 int bddVarNr,
109 int argNr,
110 BddTable& table,
111 int nodeNr) const;
112 // void panic() const; // HACK
113
114 bool containsConstructor(const NatSet& state, bool& unique);
115 static bool partlyMoreGeneral(const OpDeclaration& subsumer,
116 const OpDeclaration& victim,
117 int argNr);
118 static bool ctorSubsumes(const OpDeclaration& subsumer,
119 const OpDeclaration& victim,
120 int argNr);
121 void minimizeWrtCtor(NatSet& alive, int argNr) const;
122
123 void linearComputeSortFunctionBdds(const SortBdds& sortBdds, Vector<Bdd>& sortFunctionBdds) const;
124 void recursiveComputeSortFunctionBdds(const SortBdds& sortBdds, Vector<Bdd>& sortFunctionBdds) const;
125
126 const int nrArgs;
127 Vector<OpDeclaration> opDeclarations;
128 Vector<ConnectedComponent*> componentVector;
129 Vector<int> sortDiagram;
130 Sort* singleNonErrorSort; // if we can only generate one non error sort
131 Vector<int> ctorDiagram;
132 int ctorStatus; // place holder
133 Vector<NatSet> maximalOpDeclSetTable; // indices of maximal op decls with range <= each sort
134 };
135
136 inline int
arity() const137 SortTable::arity() const
138 {
139 return nrArgs;
140 }
141
142 inline const NatSet&
getMaximalOpDeclSet(Sort * target)143 SortTable::getMaximalOpDeclSet(Sort* target)
144 {
145 if (maximalOpDeclSetTable.isNull())
146 computeMaximalOpDeclSetTable();
147 return maximalOpDeclSetTable[target->index()];
148 }
149
150 inline bool
specialSortHandling() const151 SortTable::specialSortHandling() const
152 {
153 return sortDiagram.isNull();
154 }
155
156 inline void
addOpDeclaration(const Vector<Sort * > & domainAndRange,bool constructorFlag)157 SortTable::addOpDeclaration(const Vector<Sort*>& domainAndRange, bool constructorFlag)
158 {
159 Assert(domainAndRange.length() - 1 == nrArgs,
160 "bad domain length of " <<
161 domainAndRange.length() - 1 << " instead of " << nrArgs);
162 int nrOpDeclarations = opDeclarations.length();
163 opDeclarations.resize(nrOpDeclarations + 1);
164 opDeclarations[nrOpDeclarations].setInfo(domainAndRange, constructorFlag);
165 ctorStatus |= constructorFlag ? IS_CTOR : IS_NON_CTOR;
166 }
167
168 inline const Vector<OpDeclaration>&
getOpDeclarations() const169 SortTable::getOpDeclarations() const
170 {
171 return opDeclarations;
172 }
173
174 inline /* const */ ConnectedComponent*
rangeComponent() const175 SortTable::rangeComponent() const
176 {
177 return opDeclarations[0].getDomainAndRange()[nrArgs]->component();
178 }
179
180 inline Sort*
getRangeSort() const181 SortTable::getRangeSort() const
182 {
183 //
184 // If an operator has been declared with multiple range sort, this
185 // function just returns the first, which is good enough for some
186 // purposes.
187 //
188 return opDeclarations[0].getDomainAndRange()[nrArgs];
189 }
190
191 inline const ConnectedComponent*
domainComponent(int argNr) const192 SortTable::domainComponent(int argNr) const
193 {
194 return opDeclarations[0].getDomainAndRange()[argNr]->component();
195 }
196
197 inline Sort*
getSingleNonErrorSort() const198 SortTable::getSingleNonErrorSort() const
199 {
200 return singleNonErrorSort;
201 }
202
203 inline int
getCtorStatus() const204 SortTable::getCtorStatus() const
205 {
206 return ctorStatus;
207 }
208
209 inline int
traverse(int position,int sortIndex) const210 SortTable::traverse(int position, int sortIndex) const
211 {
212 /*
213 if (position + sortIndex >= sortDiagram.length()) // HACK
214 panic();
215 */
216 return sortDiagram[position + sortIndex];
217 }
218
219 inline int
ctorTraverse(int position,int sortIndex) const220 SortTable::ctorTraverse(int position, int sortIndex) const
221 {
222 return ctorDiagram[position + sortIndex];
223 }
224
225 #endif
226