1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2012 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 // Code for variant narrowing descent functions.
25 //
26 #include "variantSearch.hh"
27
28 local_inline bool
getCachedVariantSearch(MetaModule * m,FreeDagNode * subject,RewritingContext & context,Int64 solutionNr,VariantSearch * & search,Int64 & lastSolutionNr)29 MetaLevelOpSymbol::getCachedVariantSearch(MetaModule* m,
30 FreeDagNode* subject,
31 RewritingContext& context,
32 Int64 solutionNr,
33 VariantSearch*& search,
34 Int64& lastSolutionNr)
35 {
36 CacheableState* cachedState;
37 if (m->remove(subject, cachedState, lastSolutionNr))
38 {
39 if (lastSolutionNr <= solutionNr)
40 {
41 search = safeCast(VariantSearch*, cachedState);
42 //
43 // The parent context pointer of the root context in the VariantSearch is possibly
44 // stale since it points the context from a different descent function call.
45 //
46 safeCast(UserLevelRewritingContext*, search->getContext())->
47 beAdoptedBy(safeCast(UserLevelRewritingContext*, &context));
48 return true;
49 }
50 delete cachedState;
51 }
52 return false;
53 }
54
55 bool
metaGetVariant2(FreeDagNode * subject,RewritingContext & context,bool irredundant)56 MetaLevelOpSymbol::metaGetVariant2(FreeDagNode* subject, RewritingContext& context, bool irredundant)
57 {
58 DebugAdvisory(Tty(Tty::CYAN) << "meta variant call: " << Tty(Tty::GREEN) << (DagNode*) subject << Tty(Tty::RESET));
59 //
60 // We handle both metaGenerateVariant() and metaGenerateIrredundantVariant().
61 //
62 if (MetaModule* m = metaLevel->downModule(subject->getArgument(0)))
63 {
64 DagNode* metaVarIndex = subject->getArgument(3);
65 Int64 solutionNr;
66 if (metaLevel->isNat(metaVarIndex) &&
67 metaLevel->downSaturate64(subject->getArgument(4), solutionNr) && solutionNr >= 0)
68 {
69 const mpz_class& varIndex = metaLevel->getNat(metaVarIndex);
70 VariantSearch* vs;
71 Int64 lastSolutionNr;
72 if (getCachedVariantSearch(m, subject, context, solutionNr, vs, lastSolutionNr))
73 m->protect(); // Use cached state
74 else
75 {
76 Term* start;
77 Vector<Term*> blockerTerms;
78 if ((start = metaLevel->downTerm(subject->getArgument(1), m)) &&
79 metaLevel->downTermList(subject->getArgument(2), m, blockerTerms))
80 {
81 m->protect();
82 RewritingContext* startContext = term2RewritingContext(start, context);
83
84 Vector<DagNode*> blockerDags;
85 FOR_EACH_CONST(i, Vector<Term*>, blockerTerms)
86 {
87 Term* t = *i;
88 t = t->normalize(true); // we don't really need to normalize but we do need to set hash values
89 blockerDags.append(t->term2Dag());
90 t->deepSelfDestruct();
91 }
92 vs = new VariantSearch(startContext, blockerDags, new FreshVariableSource(m, varIndex), false, irredundant);
93 lastSolutionNr = -1;
94 }
95 else
96 return false;
97 }
98
99 DagNode* result;
100 const Vector<DagNode*>* variant;
101 int nrFreeVariables;
102 int parentIndex = -1; // dummy
103 bool moreInLayer = false; // dummy
104
105 if (lastSolutionNr == solutionNr)
106 {
107 //
108 // So the user can ask for the same variant over and over again without
109 // a horrible loss of performance.
110 //
111 variant = vs->getLastReturnedVariant(nrFreeVariables, parentIndex, moreInLayer);
112 }
113 else
114 {
115 while (lastSolutionNr < solutionNr)
116 {
117 variant = vs->getNextVariant(nrFreeVariables, parentIndex, moreInLayer);
118 if (variant == 0)
119 {
120 bool incomplete = vs->isIncomplete();
121 delete vs;
122 result = metaLevel->upNoVariant(incomplete);
123 goto fail;
124 }
125
126 context.transferCount(*(vs->getContext()));
127 ++lastSolutionNr;
128 }
129 }
130 {
131 m->insert(subject, vs, solutionNr);
132 mpz_class lastVarIndex = varIndex + nrFreeVariables;
133 mpz_class parentIndexBig(parentIndex);
134 result = metaLevel->upVariant(*variant, vs->getVariableInfo(), lastVarIndex, parentIndexBig, moreInLayer, m); // dummy args
135 }
136 fail:
137 (void) m->unprotect();
138 return context.builtInReplace(subject, result);
139 }
140 }
141 return false;
142 }
143
144 bool
metaGetVariant(FreeDagNode * subject,RewritingContext & context)145 MetaLevelOpSymbol::metaGetVariant(FreeDagNode* subject, RewritingContext& context)
146 {
147 //
148 // op metaGenerateVariant : Module Term TermList Nat Nat ~> Variant? .
149 //
150 return metaGetVariant2(subject, context, false);
151 }
152
153 bool
metaGetIrredundantVariant(FreeDagNode * subject,RewritingContext & context)154 MetaLevelOpSymbol::metaGetIrredundantVariant(FreeDagNode* subject, RewritingContext& context)
155 {
156 //
157 // op metaGenerateIrredundantVariant : Module Term TermList Nat Nat ~> Variant? .
158 //
159 return metaGetVariant2(subject, context, true);
160 }
161
162 bool
metaVariantUnify2(FreeDagNode * subject,RewritingContext & context,bool disjoint)163 MetaLevelOpSymbol::metaVariantUnify2(FreeDagNode* subject, RewritingContext& context, bool disjoint)
164 {
165 DebugAdvisory(Tty(Tty::CYAN) << "meta variant unify call: " << Tty(Tty::GREEN) << (DagNode*) subject << Tty(Tty::RESET));
166 //
167 // We handle both metaVariantUnify() and metaVariantDisjointUnify().
168 //
169 if (MetaModule* m = metaLevel->downModule(subject->getArgument(0)))
170 {
171 Int64 solutionNr;
172 DagNode* metaVarIndex = subject->getArgument(3);
173 if (metaLevel->isNat(metaVarIndex) &&
174 metaLevel->downSaturate64(subject->getArgument(4), solutionNr) && solutionNr >= 0)
175 {
176 const mpz_class& varIndex = metaLevel->getNat(metaVarIndex);
177 VariantSearch* vs;
178 Int64 lastSolutionNr;
179 if (getCachedVariantSearch(m, subject, context, solutionNr, vs, lastSolutionNr))
180 m->protect(); // Use cached state
181 else
182 {
183 Vector<Term*> lhs;
184 Vector<Term*> rhs;
185 if (!metaLevel->downUnificationProblem(subject->getArgument(1), lhs, rhs, m, disjoint))
186 return false;
187
188 Vector<Term*> blockerTerms;
189 if (!metaLevel->downTermList(subject->getArgument(2), m, blockerTerms))
190 {
191 FOR_EACH_CONST(i, Vector<Term*>, lhs)
192 (*i)->deepSelfDestruct();
193 FOR_EACH_CONST(j, Vector<Term*>, rhs)
194 (*j)->deepSelfDestruct();
195 return false;
196 }
197
198 m->protect();
199 DagNode* d = m->makeUnificationProblemDag(lhs, rhs);
200 RewritingContext* startContext = context.makeSubcontext(d, UserLevelRewritingContext::META_EVAL);
201
202 Vector<DagNode*> blockerDags;
203 FOR_EACH_CONST(i, Vector<Term*>, blockerTerms)
204 {
205 Term* t = *i;
206 t = t->normalize(true); // we don't really need to normalize but we do need to set hash values
207 blockerDags.append(t->term2Dag());
208 t->deepSelfDestruct();
209 }
210 vs = new VariantSearch(startContext, blockerDags, new FreshVariableSource(m, varIndex), true, false);
211 lastSolutionNr = -1;
212 }
213
214 DagNode* result;
215 const Vector<DagNode*>* unifier;
216 int nrFreeVariables;
217 if (lastSolutionNr == solutionNr)
218 {
219 //
220 // So the user can ask for the same unifier over and over again without
221 // a horrible loss of performance.
222 //
223 unifier = vs->getLastReturnedUnifier(nrFreeVariables);
224 }
225 else
226 {
227 while (lastSolutionNr < solutionNr)
228 {
229 unifier = vs->getNextUnifier(nrFreeVariables);
230 if (unifier == 0)
231 {
232 bool incomplete = vs->isIncomplete();
233 delete vs;
234 result = disjoint ? metaLevel->upNoUnifierTriple(incomplete) : metaLevel->upNoUnifierPair(incomplete);
235 goto fail;
236 }
237
238 context.transferCount(*(vs->getContext()));
239 ++lastSolutionNr;
240 }
241 }
242 {
243 m->insert(subject, vs, solutionNr);
244 mpz_class lastVarIndex = varIndex + nrFreeVariables;
245 result = disjoint ?
246 metaLevel->upUnificationTriple(*unifier, vs->getVariableInfo(), lastVarIndex, m) :
247 metaLevel->upUnificationPair(*unifier, vs->getVariableInfo(), lastVarIndex, m);
248 }
249 fail:
250 (void) m->unprotect();
251 return context.builtInReplace(subject, result);
252 }
253 }
254 return false;
255 }
256
257 bool
metaVariantUnify(FreeDagNode * subject,RewritingContext & context)258 MetaLevelOpSymbol::metaVariantUnify(FreeDagNode* subject, RewritingContext& context)
259 {
260 //
261 // op metaVariantUnify : Module UnificationProblem TermList Nat Nat ~> UnificationPair? .
262 //
263 return metaVariantUnify2(subject, context, false);
264 }
265
266 bool
metaVariantDisjointUnify(FreeDagNode * subject,RewritingContext & context)267 MetaLevelOpSymbol::metaVariantDisjointUnify(FreeDagNode* subject, RewritingContext& context)
268 {
269 //
270 // op metaVariantDisjointUnify : Module UnificationProblem TermList Nat Nat ~> UnificationTriple? .
271 //
272 return metaVariantUnify2(subject, context, true);
273 }
274