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 symbols belonging to the free theory.
25 //
26 #ifndef _freeSymbol_hh_
27 #define _freeSymbol_hh_
28 #include "symbol.hh"
29 #include "freeNet.hh"
30
31 #define GET_NET getNet
32 #define DISC_NET discriminationNet
33 #define FREE_NET FreeNet
34
35 class FreeSymbol : public Symbol
36 {
37 NO_COPYING(FreeSymbol);
38
39 public:
40 FreeSymbol(int id, int arity, const Vector<int>& strategy = standard, bool memoFlag = false);
41 static FreeSymbol* newFreeSymbol(int id,
42 int arity,
43 const Vector<int>& strategy = standard,
44 bool memoFlag = false);
45
46 Term* makeTerm(const Vector<Term*>& args);
47 DagNode* makeDagNode(const Vector<DagNode*>& args);
48 void compileEquations();
49 bool eqRewrite(DagNode* subject, RewritingContext& context);
50 void computeBaseSort(DagNode* subject);
51 void normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context);
52 void stackArguments(DagNode* subject,
53 Vector<RedexPosition>& stack,
54 int parentIndex);
55 Term* termify(DagNode* dagNode);
56 //
57 // Unification stuff.
58 //
59 int unificationPriority() const;
60 void computeGeneralizedSort(const SortBdds& sortBdds,
61 const Vector<int>& realToBdd,
62 DagNode* subject,
63 Vector<Bdd>& generalizedSort);
64 void computeGeneralizedSort2(const SortBdds& sortBdds,
65 const Vector<int>& realToBdd,
66 DagNode* subject,
67 Vector<Bdd>& outputBdds);
68 bool isStable() const;
69 //
70 // Hash cons stuff.
71 //
72 DagNode* makeCanonical(DagNode* original, HashConsSet* hcs);
73 DagNode* makeCanonicalCopy(DagNode* original, HashConsSet* hcs);
74 //
75 // Stack machine stuff.
76 //
77 Instruction* generateFinalInstruction(const Vector<int>& argumentSlots);
78 Instruction* generateInstruction(int destination, const Vector<int>& argumentSlots, Instruction* nextInstruction);
79 FreeNet& getNet();
80
81 #ifdef COMPILER
82 void generateCode(CompilationContext& context) const;
83 void generateCons(CompilationContext& context, int indentLevel) const;
84 #endif
85
86 #ifdef DUMP
87 void dump(ostream& s, int indentLevel = 0);
88 #endif
89
90 private:
91 bool complexStrategy(DagNode* subject, RewritingContext& context);
92 void memoStrategy(MemoTable::SourceSet& from, DagNode* subject, RewritingContext& context);
93
94 protected:
95 FreeNet discriminationNet;
96 };
97
98 inline FreeNet&
getNet()99 FreeSymbol::getNet()
100 {
101 return discriminationNet;
102 }
103
104 #endif
105