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 variable terms.
25 //
26 #ifndef _variableTerm_hh_
27 #define _variableTerm_hh_
28 #include "term.hh"
29 #include "namedEntity.hh"
30 #include "variableSymbol.hh"
31
32 class VariableTerm : public Term, public NamedEntity
33 {
34 NO_COPYING(VariableTerm);
35
36 public:
37 VariableTerm(VariableSymbol* symbol, int name);
38
39 RawArgumentIterator* arguments();
40 void deepSelfDestruct();
41 Term* deepCopy2(SymbolMap* translator) const;
42 Term* normalize(bool full, bool& changed);
43 int compareArguments(const Term* other) const;
44 int compareArguments(const DagNode* other) const;
45
46 void findEagerVariables(bool atTop, NatSet& eagerVariables) const;
47 void analyseConstraintPropagation(NatSet& boundUniquely) const;
48 LhsAutomaton* compileLhs2(bool matchAtTop,
49 const VariableInfo& variableInfo,
50 NatSet& boundUniquely,
51 bool& subproblemLikely);
52 void markEagerArguments(int nrVariables,
53 const NatSet& eagerVariables,
54 Vector<int>& problemVariables);
55 DagNode* dagify2();
56
57 void findAvailableTerms(TermBag& availableTerms, bool eagerContext, bool atTop);
58 int compileRhs2(RhsBuilder& rhsBuilder,
59 VariableInfo& variableInfo,
60 TermBag& availableTerms,
61 bool eagerContext);
62 //
63 // Optional stuff that is easy to define for variable terms.
64 //
65 bool subsumes(const Term* other, bool sameVariableSet) const;
66 int partialCompareUnstable(const Substitution& partialSubstitution,
67 DagNode* other) const;
68 //
69 // Needed because we actually do the instantiation of variables.
70 //
71 Term* instantiate2(const Vector<Term*>& varBindings, SymbolMap* translator);
72 //
73 // Functions particular to variable terms.
74 //
75 Sort* getSort() const;
76 int getIndex() const;
77 void setIndex(int indx);
78
79 private:
80 int index;
81 };
82
83 inline Sort*
getSort() const84 VariableTerm::getSort() const
85 {
86 return safeCast(VariableSymbol*, symbol())->getSort();
87 }
88
89 inline int
getIndex() const90 VariableTerm::getIndex() const
91 {
92 return index;
93 }
94
95 inline void
setIndex(int indx)96 VariableTerm::setIndex(int indx)
97 {
98 index = indx;
99 }
100
101 #endif
102