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 terms in the AC and ACU theories.
25 //
26 #ifndef _ACU_Term_hh_
27 #define _ACU_Term_hh_
28 #include "ACU_Symbol.hh"
29 #include "term.hh"
30
31 class ACU_Term : public Term
32 {
33 NO_COPYING(ACU_Term);
34
35 public:
36 ACU_Term(ACU_Symbol* symbol, const Vector<Term*>& arguments);
37 ACU_Term(ACU_Symbol* symbol, const Vector<Term*>& arguments, const Vector<int>& multiplicities);
38 //
39 // Member functions required by theory interface.
40 //
41 RawArgumentIterator* arguments();
42 void deepSelfDestruct();
43 Term* deepCopy2(SymbolMap* translator) const;
44 Term* normalize(bool full, bool& changed);
45 int compareArguments(const Term* other) const;
46 int compareArguments(const DagNode* other) const;
47 void findEagerVariables(bool atTop, NatSet& eagerVariables) const;
48 void analyseConstraintPropagation(NatSet& boundUniquely) const;
49 void analyseCollapses2();
50 void insertAbstractionVariables(VariableInfo& variableInfo);
51 LhsAutomaton* compileLhs2(bool matchAtTop,
52 const VariableInfo& variableInfo,
53 NatSet& boundUniquely,
54 bool& subproblemLikely);
55 void markEagerArguments(int nrVariables,
56 const NatSet& eagerVariables,
57 Vector<int>& problemVariables);
58 DagNode* dagify2();
59
60 void findAvailableTerms(TermBag& availableTerms, bool eagerContext, bool atTop);
61 int compileRhs2(RhsBuilder& rhsBuilder,
62 VariableInfo& variableInfo,
63 TermBag& availableTerms,
64 bool eagerContext);
65 //
66 // Functions particular to ACU_Term.
67 //
68 ACU_Symbol* symbol() const;
69
70 #ifdef DUMP
71 void dump(ostream& s, const VariableInfo& variableInfo, int indentLevel);
72 #endif
73
74 private:
75 struct Pair // misnomer!
76 {
77 Term* term;
78 int multiplicity;
79 short abstractionVariableIndex; // if subterm could enter our theory we abstract it
80 Bool collapseToOurSymbol; // first possible reason for variable abstraction
81 Bool matchOurIdentity; // second possible reason for variable abstraction
82 };
83
84 struct CP_Sequence;
85
86 ACU_Term(const ACU_Term& original, ACU_Symbol* symbol, SymbolMap* translator);
87 bool normalizeAliensAndFlatten();
88 static bool pairLt(const Pair& p1, const Pair& p2);
89 static void weakConstraintPropagation(const Vector<Pair>& aliens,
90 const NatSet& boundUniquely,
91 int step,
92 Vector<int>& sequence);
93 void compileLhs3(bool matchAtTop,
94 const VariableInfo& variableInfo,
95 NatSet& boundUniquely,
96 bool& subproblemLikely,
97 ACU_LhsAutomaton* automaton);
98 //
99 // Fuctions for compiling special case automata.
100 //
101 ACU_LhsAutomaton* tryToMakeSpecialCaseAutomaton(bool matchAtTop,
102 const VariableInfo& variableInfo,
103 NatSet& boundUniquely);
104 ACU_LhsAutomaton* tryToMakeNonLinearLhsAutomaton(const VariableInfo& variableInfo,
105 NatSet& boundUniquely);
106 ACU_LhsAutomaton* tryToMakeCollectorLhsAutomaton(bool matchAtTop,
107 const VariableInfo& variableInfo,
108 NatSet& boundUniquely,
109 int collectorCandidate);
110 //
111 // Functions needed to compile aliens only case matching.
112 //
113 static void compileAliensOnlyCase(ACU_LhsAutomaton* automaton,
114 const Vector<Pair>& nonGroundAliens,
115 const VariableInfo& variableInfo,
116 NatSet& boundUniquely,
117 bool& subproblemLikely);
118 static void findConstraintPropagationSequence(const Vector<Pair>& aliens,
119 const NatSet& boundUniquely,
120 CP_Sequence& bestSequence);
121 static void findConstraintPropagationSequence(const Vector<Pair>& aliens,
122 const Vector<int>& currentSequence,
123 const NatSet& boundUniquely,
124 int step,
125 CP_Sequence& bestSequence);
126 //
127 // Functions needed to compile full and greedy case matching.
128 //
129 static void compileGreedyAndFullCases(ACU_LhsAutomaton* automaton,
130 const Vector<Pair>& nonGroundAliens,
131 const VariableInfo& variableInfo,
132 NatSet& boundUniquely,
133 bool& subproblemLikely);
134 static int findGreedySequence(const Vector<Pair>& aliens, Vector<int>& sequence);
135 static void findIndependentSets(const Vector<Pair>& aliens,
136 Vector<Vector<int> >& independents);
137 static void findLongestIncreasingSequence(const Vector<Pair>& aliens,
138 Vector<int>& dependents,
139 Vector<int>& sequence);
140 static void findFullSequence(const Vector<Pair>& aliens,
141 const NatSet& boundUniquely,
142 Vector<int>& sequence);
143
144 Vector<Pair> argArray;
145 int uniqueCollapseSubtermIndex;
146
147 friend class ACU_ArgumentIterator;
148 };
149
150 inline ACU_Symbol*
symbol() const151 ACU_Term::symbol() const
152 {
153 return safeCast(ACU_Symbol*, Term::symbol());
154 }
155
156 #endif
157