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 // Common ancestor for equations, rules and sort constraints.
25 //
26 #ifndef _preEquation_hh_
27 #define _preEquation_hh_
28 #include <stack>
29 #include "lineNumber.hh"
30 #include "variableInfo.hh"
31 #include "badFlag.hh"
32 #include "label.hh"
33 #include "natSet.hh"
34 #include "dagRoot.hh"
35
36 class PreEquation : public LineNumber, public ModuleItem, public VariableInfo, public BadFlag
37 {
38 public:
39 PreEquation(int label, Term* lhs, const Vector<ConditionFragment*>& cond);
40 virtual ~PreEquation();
41
42 const Label& getLabel() const;
43 Term* getLhs() const;
44 const Vector<ConditionFragment*>& getCondition() const;
45 bool hasCondition() const;
46 LhsAutomaton* getLhsAutomaton() const;
47 bool isNonexec() const;
48 void setNonexec();
49 //
50 // This is the most general condition checking function that allows
51 // multiple distinct successes; caller must provide trialRef variable
52 // and condition state stack in order to preserve this information
53 // between calls.
54 //
55 bool checkCondition(bool findFirst,
56 DagNode* subject,
57 RewritingContext& context,
58 Subproblem* subproblem,
59 int& trialRef,
60 stack<ConditionState*>& state) const;
61 //
62 // Simplified interface to the above for the common case where we only care
63 // if a condition succeeds at least once or fails.
64 //
65 bool checkCondition(DagNode* subject,
66 RewritingContext& context,
67 Subproblem* subproblem) const;
68
69 DagNode* getLhsDag();
70 virtual void reset();
71 virtual void print(ostream& s) const = 0;
72
73 #ifdef DUMP
74 void dump(ostream& s, int indentLevel);
75 #endif
76
77 protected:
78 void check(NatSet& boundVariables);
79 void preprocess();
80 void compileBuild(TermBag& availableTerms, bool eagerContext);
81 void compileMatch(bool compileLhs, bool withExtension);
82 //
83 // This function must be defined by all derived classes
84 //
85 virtual int traceBeginTrial(DagNode* subject, RewritingContext& context) const = 0;
86
87 static const Vector<ConditionFragment*> noCondition;
88
89 bool isCompiled() const;
90 void setCompiled();
91
92 private:
93 static void cleanStack(stack<ConditionState*>& conditionStack);
94
95 enum Flags
96 {
97 COMPILED = 2,
98 NONEXEC = 4
99 };
100
101 bool solveCondition(bool findFirst,
102 int trialRef,
103 RewritingContext& solution,
104 stack<ConditionState*>& state) const;
105
106 Label label;
107 Term* lhs;
108 LhsAutomaton* lhsAutomaton;
109 DagRoot lhsDag; // for unification
110 Vector<ConditionFragment*> condition;
111 };
112
113 inline bool
isCompiled() const114 PreEquation::isCompiled() const
115 {
116 return getFlag(COMPILED);
117 }
118
119 inline void
setCompiled()120 PreEquation::setCompiled()
121 {
122 setFlags(COMPILED);
123 }
124
125 inline bool
isNonexec() const126 PreEquation::isNonexec() const
127 {
128 return getFlag(NONEXEC);
129 }
130
131 inline void
setNonexec()132 PreEquation::setNonexec()
133 {
134 setFlags(NONEXEC);
135 }
136
137 inline const Label&
getLabel() const138 PreEquation::getLabel() const
139 {
140 return label;
141 }
142
143 inline Term*
getLhs() const144 PreEquation::getLhs() const
145 {
146 return lhs;
147 }
148
149 inline const Vector<ConditionFragment*>&
getCondition() const150 PreEquation::getCondition() const
151 {
152 return condition;
153 }
154
155 inline bool
hasCondition() const156 PreEquation::hasCondition() const
157 {
158 return !(condition.isNull());
159 }
160
161 inline LhsAutomaton*
getLhsAutomaton() const162 PreEquation::getLhsAutomaton() const
163 {
164 return lhsAutomaton;
165 }
166
167 ostream&
168 operator<<(ostream& s, const PreEquation* pe); // we define this to call a virtual function
169
170 #endif
171