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 successor theory.
25 //
26 #ifndef _S_Symbol_hh_
27 #define _S_Symbol_hh_
28 #include "symbol.hh"
29 #include "gmpxx.h"
30
31 class S_Symbol : public Symbol
32 {
33 public:
34 S_Symbol(int id, const Vector<int>& strategy = standard, bool memoFlag = false);
35 //
36 // Member functions required by theory interface.
37 //
38 Term* makeTerm(const Vector<Term*>& args);
39 DagNode* makeDagNode(const Vector<DagNode*>& args);
40 void computeBaseSort(DagNode* subject);
41 void normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& context);
42 bool eqRewrite(DagNode* subject, RewritingContext& context);
43 DagNode* ruleRewrite(DagNode* subject, RewritingContext& context);
44 void stackArguments(DagNode* subject,
45 Vector<RedexPosition>& stack,
46 int parentIndex);
47 Term* termify(DagNode* dagNode);
48 //
49 // Member function overiding default handling.
50 //
51 void compileOpDeclarations();
52 void finalizeSortInfo();
53 bool isConstructor(DagNode* subject);
54 void fillInSortInfo(Term* subject);
55 //
56 // Unification stuff.
57 //
58 int unificationPriority() const;
59 void computeSortFunctionBdds(const SortBdds& sortBdds, Vector<Bdd>& sortFunctionBdds) 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 // Member function specific to S_Symbol.
76 //
77 bool mightCollapseToOurSymbol(const Term* subterm) const;
78
79 private:
80 struct SortPath
81 {
82 int computeSortIndex(const mpz_class& number);
83
84 Vector<int> sortIndices;
85 int leadLength;
86 //
87 // If we have a number greater than nonCtorBound we have at least
88 // one non-constructor and treat the whole thing as a non-constructor.
89 // If nonCtorBound is NONE we have a pure ctor.
90 //
91 int nonCtorBound;
92 };
93
94 void computePath(int sortIndex, SortPath& path);
95 void memoStrategy(MemoTable::SourceSet& from,
96 DagNode* subject,
97 RewritingContext& context);
98
99 Vector<SortPath> sortPathTable;
100 };
101
102 inline int
computeSortIndex(const mpz_class & number)103 S_Symbol::SortPath::computeSortIndex(const mpz_class& number)
104 {
105 int pathLength = sortIndices.length();
106 if (number <= pathLength)
107 return sortIndices[number.get_si() - 1];
108 int cycleLength = pathLength - leadLength;
109 mpz_class cycleSteps = number - (leadLength + 1);
110 int remainder = mpz_tdiv_ui(cycleSteps.get_mpz_t(), cycleLength);
111 return sortIndices[leadLength + remainder];
112 }
113
114 #endif
115