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 // Class for DAG nodes in the A, AUl, AUr and AU theories.
25 //
26 #ifndef _AU_DagNode_hh_
27 #define _AU_DagNode_hh_
28 #include "AU_BaseDagNode.hh"
29 #include "argVec.hh"
30
31 class AU_DagNode : public AU_BaseDagNode
32 {
33 NO_COPYING(AU_DagNode);
34
35 public:
36 AU_DagNode(AU_Symbol* symbol, int size);
37 //
38 // Functions required by theory interface.
39 //
40 RawDagArgumentIterator* arguments();
41 size_t getHashValue();
42 int compareArguments(const DagNode* other) const;
43 void overwriteWithClone(DagNode* old);
44 DagNode* makeClone();
45 DagNode* copyWithReplacement(int argIndex, DagNode* replacement);
46 DagNode* copyWithReplacement(Vector<RedexPosition>& redexStack,
47 int first,
48 int last);
49 void stackArguments(Vector<RedexPosition>& stack,
50 int parentIndex,
51 bool respectFrozen);
52 //
53 // Functions required to handle extension information.
54 //
55 bool matchVariableWithExtension(int index,
56 const Sort* sort,
57 Substitution& solution,
58 Subproblem*& returnedSubproblem,
59 ExtensionInfo* extensionInfo);
60 void partialReplace(DagNode* replacement, ExtensionInfo* extensionInfo);
61 DagNode* partialConstruct(DagNode* replacement, ExtensionInfo* extensionInfo);
62 ExtensionInfo* makeExtensionInfo();
63 //
64 // Although we currently don't support unification or narrowing in AU nodes
65 // we still need some functionality from the unification and narrowing interfaces
66 // to allow narrowing to happen below us or in a sibling branch.
67 //
68 // Unification member functions.
69 //
70 DagNode* instantiate2(const Substitution& substitution);
71 //
72 // Supported for A only.
73 //
74 ReturnResult computeBaseSortForGroundSubterms();
75 bool computeSolvedForm2(DagNode* rhs, UnificationContext& solution, PendingUnificationStack& pending);
76 void insertVariables2(NatSet& occurs);
77
78 //
79 // Interface for narrowing.
80 //
81 bool indexVariables2(NarrowingVariableInfo& indices, int baseIndex);
82 DagNode* instantiateWithReplacement(const Substitution& substitution, const Vector<DagNode*>& eagerCopies, int argIndex, DagNode* newDag);
83 DagNode* instantiateWithCopies2(const Substitution& substitution, const Vector<DagNode*>& eagerCopies);
84 //
85 // Functions particular to AU_DagNode.
86 //
87 void setProducedByAssignment();
88
89 private:
90 enum NormalizationResult
91 {
92 COLLAPSED,
93 DEQUED,
94 NORMAL,
95 FLATTENED
96 };
97 //
98 // Functions required by theory interface.
99 //
100 DagNode* markArguments();
101 DagNode* copyEagerUptoReduced2();
102 void clearCopyPointers2();
103 //
104 // Functions particular to AU_DagNode.
105 //
106 bool disappear(AU_Symbol* s, ArgVec<DagNode*>::const_iterator i);
107 NormalizationResult normalizeAtTop(bool dumb = false);
108 bool eliminateForward(DagNode* target, int& pos, int limit) const;
109 bool eliminateBackward(DagNode* target, int& pos, int limit) const;
110 DagNode* makeFragment(int start, int nrSubterms, bool extraId) const;
111
112 ArgVec<DagNode*> argArray;
113
114 friend class AU_Symbol; // to reduce subterms prior to rewriting
115 friend class AU_Term; // for term->DAG conversion & comparison
116 friend class AU_LhsAutomaton; // for matching DAG subject
117 friend class AU_RhsAutomaton; // for constructing replacement DAG
118 friend class AU_Layer; // for constructing substitution
119 friend class AU_Subproblem; // for constructing substitution
120 friend class AU_ExtensionInfo; // for constructing matched portion
121 friend class AU_DequeDagNode; // for conversion & comparison
122 friend class AU_UnificationSubproblem;
123 friend class AU_UnificationSubproblem2;
124 };
125
126 AU_DagNode* getAU_DagNode(DagNode* dagNode);
127
128 inline
AU_DagNode(AU_Symbol * symbol,int size)129 AU_DagNode::AU_DagNode(AU_Symbol* symbol, int size)
130 : AU_BaseDagNode(symbol),
131 argArray(size)
132 {
133 setNormalizationStatus(FRESH);
134 }
135
136 inline void
setProducedByAssignment()137 AU_DagNode::setProducedByAssignment()
138 {
139 setNormalizationStatus(ASSIGNMENT);
140
141 #ifndef NO_ASSERT
142 //
143 // Look for Riesco 1/18/10 bug.
144 //
145 for (int i = 0; i < argArray.length(); ++i)
146 {
147 DagNode* d = argArray[i];
148 Assert(d->getSortIndex() != Sort::SORT_UNKNOWN,
149 "AU_DagNode::setProducedByAssignment(): unknown sort for AU argument " << d <<
150 " at index " << i << " in subject " << this);
151 }
152 #endif
153
154 }
155
156 #endif
157