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 // Implementation for class CUI_Symbol.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 #include "variable.hh"
35 #include "CUI_Theory.hh"
36
37 // interface class definitions
38 #include "symbol.hh"
39 #include "dagNode.hh"
40 #include "term.hh"
41 #include "lhsAutomaton.hh"
42 #include "rhsAutomaton.hh"
43 #include "subproblem.hh"
44
45 // core class definitions
46 #include "rewritingContext.hh"
47 #include "variableInfo.hh"
48 #include "sortBdds.hh"
49 #include "hashConsSet.hh"
50
51 // CUI theory class definitions
52 #include "CUI_Symbol.hh"
53 #include "CUI_DagNode.hh"
54 #include "CUI_Term.hh"
55 #include "CUI_UnificationSubproblem.hh"
56 #include "CUI_UnificationSubproblem2.hh"
57
CUI_Symbol(int id,const Vector<int> & strategy,bool memoFlag,Axioms axioms,Term * identity)58 CUI_Symbol::CUI_Symbol(int id,
59 const Vector<int>& strategy,
60 bool memoFlag,
61 Axioms axioms,
62 Term* identity)
63 : BinarySymbol(id, memoFlag, identity),
64 axioms(axioms)
65 {
66 if (axioms & COMM)
67 setPermuteStrategy(strategy);
68 else
69 setStrategy(strategy, 2, memoFlag);
70 }
71
72 void
compileOpDeclarations()73 CUI_Symbol::compileOpDeclarations()
74 {
75 if (axioms & COMM)
76 commutativeSortCompletion();
77 Symbol::compileOpDeclarations(); // do default sort processing
78 if (axioms & IDEM)
79 idempotentSortCheck();
80 }
81
82 void
postOpDeclarationPass()83 CUI_Symbol::postOpDeclarationPass()
84 {
85 processIdentity();
86 if (axioms & LEFT_ID)
87 leftIdentitySortCheck();
88 //
89 // If we are commutative, a problem that shows up with rightIdentitySortCheck()
90 // will already have shown up with leftIdentitySortCheck() and the latter is faster.
91 //
92 if (!(axioms & COMM))
93 {
94 if (axioms & RIGHT_ID)
95 rightIdentitySortCheck();
96 }
97 }
98
99 Term*
makeTerm(const Vector<Term * > & args)100 CUI_Symbol::makeTerm(const Vector<Term*>& args)
101 {
102 return new CUI_Term(this, args);
103 }
104
105 DagNode*
makeDagNode(const Vector<DagNode * > & args)106 CUI_Symbol::makeDagNode(const Vector<DagNode*>& args)
107 {
108 CUI_DagNode* c = new CUI_DagNode(this);
109 c->argArray[0] = args[0];
110 c->argArray[1] = args[1];
111 return c;
112 }
113
114 bool
eqRewrite(DagNode * subject,RewritingContext & context)115 CUI_Symbol::eqRewrite(DagNode* subject, RewritingContext& context)
116 {
117 Assert(this == subject->symbol(), "bad symbol");
118 CUI_DagNode* s = static_cast<CUI_DagNode*>(subject);
119 DagNode** args = s->argArray;
120 if (standardStrategy())
121 {
122 args[0]->reduce(context);
123 args[1]->reduce(context);
124 if (s->normalizeAtTop())
125 return false;
126 return !(equationFree()) && applyReplace(s, context);
127 }
128 else
129 {
130 if (isMemoized())
131 {
132 MemoTable::SourceSet from;
133 bool result = memoStrategy(from, subject, context);
134 memoEnter(from, subject);
135 //
136 // We may need to return true in the case we collapse to a unreduced subterm.
137 //
138 return result;
139 }
140 //
141 // Execute user supplied strategy.
142 //
143 const Vector<int>& userStrategy = getStrategy();
144 int stratLen = userStrategy.length();
145 bool seenZero = false;
146 for (int i = 0; i < stratLen; i++)
147 {
148 int a = userStrategy[i];
149 if(a == 0)
150 {
151 if (!seenZero)
152 {
153 args[0]->computeTrueSort(context);
154 args[1]->computeTrueSort(context);
155 seenZero = true;
156 }
157 //
158 // If we collapse to one of our subterms which has not been
159 // reduced we pretend that we did a rewrite so that the
160 // reduction process continues.
161 //
162 if (s->normalizeAtTop())
163 return !(s->isReduced());
164 if ((i + 1 == stratLen) ? applyReplace(s, context) :
165 applyReplaceNoOwise(s, context))
166 return true;
167 }
168 else
169 {
170 --a; // real arguments start at 0 not 1
171 if (seenZero)
172 {
173 args[a] = args[a]->copyReducible();
174 //
175 // A previous call to applyReplace() may have
176 // computed a true sort for our subject which will be
177 // invalidated by the reduce we are about to do.
178 //
179 s->repudiateSortInfo();
180 }
181 args[a]->reduce(context);
182 }
183 }
184 return false;
185 }
186 }
187
188 bool
memoStrategy(MemoTable::SourceSet & from,DagNode * subject,RewritingContext & context)189 CUI_Symbol::memoStrategy(MemoTable::SourceSet& from,
190 DagNode* subject,
191 RewritingContext& context)
192 {
193 CUI_DagNode* s = static_cast<CUI_DagNode*>(subject);
194 DagNode** args = s->argArray;
195 //
196 // Execute user supplied strategy.
197 //
198 const Vector<int>& userStrategy = getStrategy();
199 int stratLen = userStrategy.length();
200 bool seenZero = false;
201 for (int i = 0; i < stratLen; i++)
202 {
203 int a = userStrategy[i];
204 if(a == 0)
205 {
206 if (!seenZero)
207 {
208 args[0]->computeTrueSort(context);
209 args[1]->computeTrueSort(context);
210 seenZero = true;
211 }
212 //
213 // If we collapse to one of our subterms which has not been
214 // reduced we pretend that we did a rewrite so that the
215 // reduction process continues.
216 //
217 if (s->normalizeAtTop())
218 return !(s->isReduced());
219 if (memoRewrite(from, subject, context))
220 return false;
221 if ((i + 1 == stratLen) ? applyReplace(s, context) :
222 applyReplaceNoOwise(s, context))
223 {
224 subject->reduce(context);
225 return false;
226 }
227 }
228 else
229 {
230 --a; // real arguments start at 0 not 1
231 if (seenZero)
232 {
233 args[a] = args[a]->copyReducible();
234 //
235 // A previous call to applyReplace() may have
236 // computed a true sort for our subject which will be
237 // invalidated by the reduce we are about to do.
238 //
239 s->repudiateSortInfo();
240 }
241 args[a]->reduce(context);
242 }
243 }
244 return false;
245 }
246
247 void
computeBaseSort(DagNode * subject)248 CUI_Symbol::computeBaseSort(DagNode* subject)
249 {
250 Assert(this == subject->symbol(), "bad symbol");
251 DagNode** args = static_cast<CUI_DagNode*>(subject)->argArray;
252 int i0 = args[0]->getSortIndex();
253 int i1 = args[1]->getSortIndex();
254 Assert(i0 >= 0 && i1 >= 0, "bad sort index");
255 subject->setSortIndex(traverse(traverse(0, i0), i1));
256 }
257
258 void
normalizeAndComputeTrueSort(DagNode * subject,RewritingContext & context)259 CUI_Symbol::normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context)
260 {
261 Assert(this == subject->symbol(), "bad symbol");
262 CUI_DagNode* s = static_cast<CUI_DagNode*>(subject);
263 DagNode** args = s->argArray;
264 //
265 // Make sure each subterm has a sort.
266 //
267 args[0]->computeTrueSort(context);
268 args[1]->computeTrueSort(context);
269 //
270 // Put subject in normal form (could collapse to a subterm).
271 //
272 if (s->normalizeAtTop())
273 return;
274 //
275 // Finally compute subjects true sort.
276 //
277 fastComputeTrueSort(subject, context);
278 }
279
280 void
stackArguments(DagNode * subject,Vector<RedexPosition> & stack,int parentIndex)281 CUI_Symbol::stackArguments(DagNode* subject,
282 Vector<RedexPosition>& stack,
283 int parentIndex)
284 {
285 DagNode** args = safeCast(CUI_DagNode*, subject)->argArray;
286 const NatSet& frozen = getFrozen();
287
288 DagNode* d = args[0];
289 if (!(frozen.contains(0)) && !(d->isUnstackable()))
290 stack.append(RedexPosition(args[0], parentIndex, 0, eagerArgument(0)));
291
292 d = args[1];
293 if (!(frozen.contains(1)) && !(d->isUnstackable()))
294 stack.append(RedexPosition(args[1], parentIndex, 1, eagerArgument(1)));
295 }
296
297 void
setFrozen(const NatSet & frozen)298 CUI_Symbol::setFrozen(const NatSet& frozen)
299 {
300 if (axioms & COMM)
301 setPermuteFrozen(frozen);
302 else
303 BinarySymbol::setFrozen(frozen);
304 }
305
306 Term*
termify(DagNode * dagNode)307 CUI_Symbol::termify(DagNode* dagNode)
308 {
309 Vector<Term*> arguments(2);
310 DagNode** argArray = safeCast(CUI_DagNode*, dagNode)->argArray;
311 DagNode* d0 = argArray[0];
312 DagNode* d1 = argArray[1];
313 arguments[0] = d0->symbol()->termify(d0);
314 arguments[1] = d1->symbol()->termify(d1);
315 return new CUI_Term(this, arguments);
316 }
317
318 //
319 // Unification code.
320 //
321
322 void
computeGeneralizedSort(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & generalizedSort)323 CUI_Symbol::computeGeneralizedSort(const SortBdds& sortBdds,
324 const Vector<int>& realToBdd,
325 DagNode* subject,
326 Vector<Bdd>& generalizedSort)
327 {
328 DagNode** args = safeCast(CUI_DagNode*, subject)->argArray;
329 int varCounter = 0;
330 bddPair* argMap = bdd_newpair();
331 for (int i = 0; i < 2; i++)
332 {
333 Vector<Bdd> argGenSort;
334 args[i]->computeGeneralizedSort(sortBdds, realToBdd, argGenSort);
335 int nrBdds = argGenSort.size();
336 for (int j = 0; j < nrBdds; ++j, ++varCounter)
337 bdd_setbddpair(argMap, varCounter, argGenSort[j]);
338 }
339 const Vector<Bdd>& sortFunction = sortBdds.getSortFunction(this);
340 int nrBdds = sortFunction.size();
341 generalizedSort.resize(nrBdds);
342 for (int i = 0; i < nrBdds; ++i)
343 generalizedSort[i] = bdd_veccompose(sortFunction[i], argMap);
344 bdd_freepair(argMap);
345 }
346
347
348 // experimental code for faster sort computations
349 void
computeGeneralizedSort2(const SortBdds & sortBdds,const Vector<int> & realToBdd,DagNode * subject,Vector<Bdd> & outputBdds)350 CUI_Symbol::computeGeneralizedSort2(const SortBdds& sortBdds,
351 const Vector<int>& realToBdd,
352 DagNode* subject,
353 Vector<Bdd>& outputBdds)
354 {
355 DagNode** args = safeCast(CUI_DagNode*, subject)->argArray;
356 Vector<Bdd> inputBdds;
357 args[0]->computeGeneralizedSort2(sortBdds, realToBdd, inputBdds);
358 args[1]->computeGeneralizedSort2(sortBdds, realToBdd, inputBdds);
359 sortBdds.operatorCompose(this, inputBdds, outputBdds);
360 }
361
362 UnificationSubproblem*
makeUnificationSubproblem()363 CUI_Symbol::makeUnificationSubproblem()
364 {
365 if (leftId() || rightId())
366 return new CUI_UnificationSubproblem2();
367 return new CUI_UnificationSubproblem();
368 }
369
370 int
unificationPriority() const371 CUI_Symbol::unificationPriority() const
372 {
373 if (idem())
374 return Symbol::unificationPriority(); // unimplemented
375 //
376 // Make a rough guess about how branchy we are.
377 //
378 return comm() + 2 * (leftId() + rightId());
379 }
380
381 bool
canResolveTheoryClash()382 CUI_Symbol::canResolveTheoryClash()
383 {
384 return leftId() || rightId();
385 }
386
387 //
388 // Hash cons code.
389 //
390
391 DagNode*
makeCanonical(DagNode * original,HashConsSet * hcs)392 CUI_Symbol::makeCanonical(DagNode* original, HashConsSet* hcs)
393 {
394 DagNode** p = safeCast(CUI_DagNode*, original)->argArray;
395 DagNode* d = p[0];
396 DagNode* c = hcs->getCanonical(hcs->insert(d));
397 DagNode* d1 = p[1];
398 DagNode* c1 = hcs->getCanonical(hcs->insert(d1));
399 if (c == d && c1 == d1)
400 return original; // can use the original dag node as the canonical version
401 //
402 // Need to make new node.
403 //
404 CUI_DagNode* n = new CUI_DagNode(this);
405 n->copySetRewritingFlags(original);
406 n->setSortIndex(original->getSortIndex());
407 n->argArray[0] = c;
408 n->argArray[1] = c1;
409 return n;
410 }
411
412 DagNode*
makeCanonicalCopy(DagNode * original,HashConsSet * hcs)413 CUI_Symbol::makeCanonicalCopy(DagNode* original, HashConsSet* hcs)
414 {
415 //
416 // We have a unreduced node - copy forced.
417 //
418 CUI_DagNode* n = new CUI_DagNode(this);
419 n->copySetRewritingFlags(original);
420 n->setSortIndex(original->getSortIndex());
421 DagNode** p = safeCast(CUI_DagNode*, original)->argArray;
422 n->argArray[0] = hcs->getCanonical(hcs->insert(p[0]));
423 n->argArray[1] = hcs->getCanonical(hcs->insert(p[1]));
424 return n;
425 }
426