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 symbols.
25 //
26 #ifndef _variableSymbol_hh_
27 #define _variableSymbol_hh_
28 #include "symbol.hh"
29
30 class VariableSymbol : public Symbol
31 {
32 NO_COPYING(VariableSymbol);
33
34 public:
35 VariableSymbol(int id);
36
37 Term* makeTerm(const Vector<Term*>& args);
38 DagNode* makeDagNode(const Vector<DagNode*>& args);
39 bool eqRewrite(DagNode* subject, RewritingContext& context);
40 void computeBaseSort(DagNode* subject);
41 void normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context);
42 void stackArguments(DagNode* subject,
43 Vector<RedexPosition>& stack,
44 int parentIndex);
45 Term* termify(DagNode* dagNode);
46 //
47 // Unification stuff.
48 //
49 void computeGeneralizedSort(const SortBdds& sortBdds,
50 const Vector<int>& realToBdd,
51 DagNode* subject,
52 Vector<Bdd>& generalizedSort);
53 void computeGeneralizedSort2(const SortBdds& sortBdds,
54 const Vector<int>& realToBdd,
55 DagNode* subject,
56 Vector<Bdd>& outputBdds);
57
58 bool isStable() const;
59 //
60 // Hash cons stuff.
61 //
62 DagNode* makeCanonical(DagNode* original, HashConsSet* /* hcs */);
63 DagNode* makeCanonicalCopy(DagNode* original, HashConsSet* /* hcs */);
64 //
65 // VariableSymbol specific functions.
66 //
67 Sort* getSort();
68 };
69
70 inline Sort*
getSort()71 VariableSymbol::getSort()
72 {
73 //
74 // Temporary hack until sorts mechanism revised.
75 //
76 const Vector<OpDeclaration>& s = getOpDeclarations();
77 Assert(s.length() == 1, "s.length() != 1");
78 const Vector<Sort*>& v = s[0].getDomainAndRange();
79 Assert(v.length() == 1, "v.length() != 1");
80 return v[0];
81 }
82
83 #endif
84