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 // Abstract base class for binary symbols with attributes.
25 // This class adds extra functionality needed by:
26 // (1) commutative function symbols;
27 // (2) idempotent function symbols; and
28 // (3) function symbols with an identity.
29 //
30 #ifndef _binarySymbol_hh_
31 #define _binarySymbol_hh_
32 #include "symbol.hh"
33 #include "term.hh"
34 #include "cachedDag.hh"
35
36 class BinarySymbol : public Symbol
37 {
38 public:
39 //
40 // Distinguishing arguments for permutative function symbols is not possible
41 // so only three strategies make sense.
42 //
43 enum PermuteStrategy
44 {
45 EAGER, // [strat (1 2 0)]
46 SEMI_EAGER, // [strat (0 1 2 0)]
47 LAZY // [strat (0)]
48 };
49
50 BinarySymbol(int id, bool memoFlag, Term* identity = 0);
51
52 void setPermuteStrategy(const Vector<int>& userStrategy);
53 PermuteStrategy getPermuteStrategy() const;
54 void setPermuteFrozen(const NatSet& frozen);
55 void setIdentity(Term* id);
56 Term* getIdentity() const;
57 bool hasIdentity() const;
58 bool hasUnequalLeftIdentityCollapse() const;
59 bool hasUnequalRightIdentityCollapse() const;
60 bool hasCyclicIdentity() const;
61 DagNode* getIdentityDag();
62 bool mightMatchOurIdentity(const Term* subterm) const;
63 bool takeIdentity(const Sort* sort);
64 bool interSymbolPass();
65 void reset();
66 int computeSortIndex(int index1, int index2);
67 int computeMultSortIndex(int index1, int index2, int multiplicity);
68 //
69 // Default definition returns true iff we don't have an identity. This must
70 // be overridden for any symbol with other behavior.
71 //
72 bool isStable() const;
73
74 protected:
75 void commutativeSortCompletion();
76 void idempotentSortCheck();
77 void processIdentity();
78 void leftIdentitySortCheck();
79 void rightIdentitySortCheck();
80
81 private:
82 enum IdentityStatus
83 {
84 NOT_NORMALIZED,
85 IN_PROCESS,
86 NORMALIZED
87 };
88
89 bool lookForCycle(Term* term, NatSet& examinedIds) const;
90
91 PermuteStrategy permuteStrategy;
92 CachedDag identityTerm;
93 //
94 // These flags record if we detected a collapse from one sort to another.
95 // Collapsing to a lower sort is legal but complicates unification.
96 //
97 bool unequalLeftIdCollapse;
98 bool unequalRightIdCollapse;
99 //
100 // This flag records if we can reach find a cycle of symbols by examining identities of symbols.
101 // We need this information for breaking non-disjoint cycles during unification.
102 // Because it is potentially expensive to compute we only compute it if needed and therefore
103 // store it as an int so we can have an undecided state.
104 //
105 mutable int cyclicIdentity;
106 };
107
108 inline BinarySymbol::PermuteStrategy
getPermuteStrategy() const109 BinarySymbol::getPermuteStrategy() const
110 {
111 return permuteStrategy;
112 }
113
114 inline void
setIdentity(Term * id)115 BinarySymbol::setIdentity(Term* id)
116 {
117 Assert(identityTerm.getTerm() == 0, "overwriting identity for " << this);
118 identityTerm.setTerm(id);
119 cyclicIdentity = UNDECIDED;
120 }
121
122 inline Term*
getIdentity() const123 BinarySymbol::getIdentity() const
124 {
125 return identityTerm.getTerm();
126 }
127
128 inline bool
hasIdentity() const129 BinarySymbol::hasIdentity() const
130 {
131 return identityTerm.getTerm() != 0;
132 }
133
134 inline bool
hasCyclicIdentity() const135 BinarySymbol::hasCyclicIdentity() const
136 {
137 if (cyclicIdentity == UNDECIDED)
138 {
139 NatSet examinedIds;
140 cyclicIdentity = lookForCycle(getIdentity(), examinedIds);
141 }
142 return cyclicIdentity;
143 }
144
145 inline bool
hasUnequalLeftIdentityCollapse() const146 BinarySymbol::hasUnequalLeftIdentityCollapse() const
147 {
148 return unequalLeftIdCollapse;
149 }
150
151 inline bool
hasUnequalRightIdentityCollapse() const152 BinarySymbol::hasUnequalRightIdentityCollapse() const
153 {
154 return unequalRightIdCollapse;
155 }
156
157 inline bool
takeIdentity(const Sort * sort)158 BinarySymbol::takeIdentity(const Sort* sort)
159 {
160 Term* id = identityTerm.getTerm();
161 return id != 0 && id->leq(sort);
162 }
163
164 inline DagNode*
getIdentityDag()165 BinarySymbol::getIdentityDag()
166 {
167 Assert(identityTerm.getTerm() != 0, "null identity for symbol " << this);
168 return identityTerm.getDag();
169 }
170
171 inline int
computeSortIndex(int index1,int index2)172 BinarySymbol::computeSortIndex(int index1, int index2)
173 {
174 return traverse(traverse(0, index1), index2);
175 }
176
177 inline int
computeMultSortIndex(int index1,int index2,int multiplicity)178 BinarySymbol::computeMultSortIndex(int index1, int index2, int multiplicity)
179 {
180 while (multiplicity > 0)
181 {
182 if (multiplicity & 1)
183 index1 = computeSortIndex(index1, index2);
184 multiplicity >>= 1;
185 index2 = computeSortIndex(index2, index2);
186 }
187 return index1;
188 }
189
190 #endif
191