1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2008 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 // Class for a stack of pending unification problems.
25 //
26 // Problems get pushed on the stack because they potentially have multiple solutions.
27 // Great pains are taken to ensure that when we solve such a problem we solve all existing
28 // problems that are in the same theory simultaneously since this is crucial for termination
29 // in some theories.
30 //
31 #ifndef _pendingUnificationStack_hh_
32 #define _pendingUnificationStack_hh_
33 #include "simpleRootContainer.hh"
34 #include "substitution.hh"
35
36 class PendingUnificationStack : private SimpleRootContainer
37 {
38 NO_COPYING(PendingUnificationStack);
39
40 public:
41 typedef int Marker;
42
43 PendingUnificationStack();
44 ~PendingUnificationStack();
45
46 void push(Symbol* controllingSymbol, DagNode* lhs, DagNode* rhs, bool marked = false);
47 bool resolveTheoryClash(DagNode* lhs, DagNode* rhs);
48
49 Marker checkPoint() const;
50 void restore(Marker mark);
51
52 bool solve(bool findFirst, UnificationContext& solution);
53
54 void flagAsIncomplete(Symbol* symbol);
55 bool isIncomplete() const;
56
57 void dump(ostream& s);
58
59 private:
60 struct Theory
61 {
62 Symbol* controllingSymbol; // controlling symbol for this theory
63 int firstProblemInTheory; // index into stack of first problem in this theory that isn't active (or NONE)
64 };
65
66 struct PendingUnification
67 {
68 int theoryIndex; // index into the theory table
69 int nextProblemInTheory; // index into the stack for the next problem in our theory that isn't active (or NONE)
70 DagNode* lhs;
71 DagNode* rhs;
72 bool marked; // set this to force the lhs to collapse;
73 };
74
75 struct ActiveSubproblem
76 {
77 int theoryIndex; // index into the theory table
78 int savedFirstProblem; // saved value of firstProblemInTheory
79 UnificationSubproblem* subproblem;
80 };
81
82 void markReachableNodes();
83 int chooseTheoryToSolve();
84 bool makeNewSubproblem(UnificationContext& solution);
85 void killTopSubproblem();
86
87 Vector<Theory> theoryTable;
88 Vector<PendingUnification> unificationStack;
89 Vector<ActiveSubproblem> subproblemStack;
90 NatSet incompleteSymbols;
91 //
92 // Cycle handling.
93 //
94 enum Status
95 {
96 UNEXPLORED = -1,
97 EXPLORED = -2
98 };
99
100 enum SpecialTheory
101 {
102 COMPOUND_CYCLE = -2
103 };
104
105 int findCycle(UnificationContext& solution);
106 int findCycleFrom(int index, UnificationContext& solution);
107 //
108 // variableStatus[i] holds the index of the variable occuring in variable i's binding that we are about to explore;
109 // or one of the special values:
110 // UNEXPLORED : haven't visited variable i on this cycle check
111 // EXPLORED : fully explored variable i and didn't find cycle
112 //
113 Vector<int> variableStatus;
114 //
115 // variableOrder stores the variable indices in an order which they can be safely instantiated.
116 //
117 Vector<int> variableOrder;
118 };
119
120 inline PendingUnificationStack::Marker
checkPoint() const121 PendingUnificationStack::checkPoint() const
122 {
123 return unificationStack.size();
124 }
125
126 inline void
flagAsIncomplete(Symbol * symbol)127 PendingUnificationStack::flagAsIncomplete(Symbol* symbol)
128 {
129 int index = symbol->getIndexWithinModule();
130 if (!(incompleteSymbols.contains(index)))
131 {
132 incompleteSymbols.insert(index);
133 IssueWarning("Unification modulo the theory of operator " << QUOTE(symbol) <<
134 " has encountered an instance for which it may not be complete.");
135 }
136 }
137
138 inline bool
isIncomplete() const139 PendingUnificationStack::isIncomplete() const
140 {
141 return !(incompleteSymbols.empty());
142 }
143
144 #endif
145