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 // Detailed analysis of a preregularity or constuctor consistancy issue to impress the user.
25 //
26 #include <gmpxx.h>
27 #include <map>
28 //#include <iterator>
29
30 struct SortTable::Node
31 {
32 mpz_class pathCount;
33 int parent;
34 int sortIndex;
35 };
36
37 void
sortErrorAnalysis(bool preregProblem,const set<int> & badTerminals)38 SortTable::sortErrorAnalysis(bool preregProblem,
39 const set<int>& badTerminals)
40 {
41 //copy(badTerminals.begin(), badTerminals.end(), ostream_iterator<const int>(cout, " "));
42 //cout << endl;
43 //
44 // First we build a spanning tree with a path count, parent node and sort index
45 // (from parent) for each node. Nonterminal nodes are named by their start index
46 // in the diagram vector while terminals are named by the absolute index of the
47 // terminal in the diagram vector.
48 //
49 const Vector<int>& diagram = preregProblem ? sortDiagram : ctorDiagram;
50 typedef map<int, Node> SpanningTree;
51 SpanningTree spanningTree;
52 spanningTree[0].pathCount = 1;
53 spanningTree[0].parent = NONE;
54 spanningTree[0].sortIndex = NONE;
55 mpz_class product = 1;
56 mpz_class badCount = 0;
57 Vector<int> firstBad(nrArgs);
58
59 set<int> currentNodes;
60 currentNodes.insert(0);
61
62 for (int i = 0; i < nrArgs; i++)
63 {
64 set<int> nextNodes;
65 const ConnectedComponent* component = componentVector[i];
66 int nrSorts = component->nrSorts();
67 product *= nrSorts;
68
69 FOR_EACH_CONST(j, set<int>, currentNodes)
70 {
71 int parent = *j;
72 mpz_class& pathCount = spanningTree[parent].pathCount;
73
74 for (int k = 0; k < nrSorts; k++)
75 {
76 int index = parent + k;
77 if (i == nrArgs - 1)
78 {
79 //
80 // Terminal node - see if it is bad.
81 //
82 if (badTerminals.find(index) != badTerminals.end())
83 {
84 //cerr << " pathCount = " << pathCount << endl;
85 if (badCount == 0)
86 {
87 badCount = pathCount;
88 firstBad[nrArgs - 1] = k;
89 int n = parent;
90 for (int l = nrArgs - 2; l >= 0; --l)
91 {
92 SpanningTree::const_iterator t = spanningTree.find(n);
93 Assert(t != spanningTree.end(), "missing node");
94 firstBad[l] = t->second.sortIndex;
95 n = t->second.parent;
96 }
97 //copy(firstBad.begin(), firstBad.end(), ostream_iterator<const int>(cout, " "));
98 //cout << endl;
99
100 }
101 else
102 badCount += pathCount;
103 }
104 }
105 else
106 {
107 //
108 // Nonterminal node - generate next nodes.
109 //
110 int target = diagram[index];
111 pair<SpanningTree::iterator, bool> p =
112 spanningTree.insert(SpanningTree::value_type(target, Node()));
113 if (p.second)
114 {
115 p.first->second.pathCount = pathCount;
116 p.first->second.parent = parent;
117 p.first->second.sortIndex = k;
118 nextNodes.insert(target);
119 }
120 else
121 p.first->second.pathCount += pathCount;
122 }
123 }
124 }
125 currentNodes.swap(nextNodes);
126 }
127
128 ComplexWarning((preregProblem ? "sort" : "constructor") <<
129 " declarations for operator " <<
130 QUOTE(safeCast(Symbol*, this)) << " failed " <<
131 (preregProblem ? "preregularity" : "constructor consistency") <<
132 " check on " << badCount << " out of " << product <<
133 " sort tuples. First such tuple is (");
134 for (int i = 0; i < nrArgs; i++)
135 {
136 cerr << QUOTE(componentVector[i]->sort(firstBad[i]));
137 if (i != nrArgs - 1)
138 cerr << ", ";
139 }
140 cerr << ")." << endl;
141 }
142