1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2006 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 to storage bdds associated with each sort index and each component.
25 // These are currently only used for order-sorted unification and can take up
26 // a fair amount of computation and storage. Thus they are computed on demand
27 // and cached in this structure.
28 //
29 #ifndef _sortBdds_hh_
30 #define _sortBdds_hh_
31 #include "bdd.hh"
32 #include "bddUser.hh"
33
34 class SortBdds : private BddUser
35 {
36 public:
37 SortBdds(Module* module);
38
39 int getFirstAvailableVariable() const;
40 int getNrVariables(int componentIndex) const;
41 Bdd getGtRelation(int componentIndex) const;
42 Bdd getLeqRelation(int sortIndex) const;
43 Bdd getRemappedLeqRelation(Sort* sort, int firstVariable) const;
44 Bdd applyLeqRelation(Sort* sort, const Vector<Bdd>& argument) const;
45 const Vector<Bdd>& getSortFunction(Symbol* symbol) const;
46
47 void makeIndexVector(int nrBdds, int index, Vector<Bdd>& vec) const;
48 Bdd makeIndexBdd(int firstVariable, int nrVariables, int index) const;
49 void makeVariableVector(int firstVariable, int nrVariables, Vector<Bdd>& vec) const; // might delete this eventually
50 void appendVariableVector(int firstBddVariable, int nrBddVariables, Vector<Bdd>& vec) const;
51 Bdd makeVariableBdd(int firstVariable, int nrVariables) const;
52
53 void appendIndexVector(int nrBdds, int index, Vector<Bdd>& vec) const;
54 void operatorCompose(Symbol* op, const Vector<Bdd>& inputBdds, Vector<Bdd>& outputBdds) const;
55
56 private:
57 struct ComponentInfo
58 {
59 int nrVariables; // number of bits needed to represent a sort in this component
60 Bdd gtRelation; // bdd for relation s1 valid /\ s2 valid /\ s1 > s2
61 };
62
63 int calculateNrBits(int nrIndicies);
64
65 int maxNrVariables; // the max number of variables needed for any component
66 //
67 // For each component we keep the number of variables needed to encode a sort
68 // in this component and the bdd for relation s1 valid /\ s2 valid /\ s1 > s2.
69 //
70 Vector<ComponentInfo> componentInfo;
71 //
72 // For each sort s we keep the bdd for the relation x <= s.
73 //
74 Vector<Bdd> leqRelations;
75 //
76 // For each symbol, we keep a vector of BDDs to hold its sort function - which
77 // may or may not be filled out.
78 //
79 mutable Vector<Vector<Bdd> > sortFunctions;
80 };
81
82 inline int
getFirstAvailableVariable() const83 SortBdds::getFirstAvailableVariable() const
84 {
85 return maxNrVariables;
86 }
87
88 inline int
getNrVariables(int componentIndex) const89 SortBdds::getNrVariables(int componentIndex) const
90 {
91 return componentInfo[componentIndex].nrVariables;
92 }
93
94 inline Bdd
getGtRelation(int componentIndex) const95 SortBdds::getGtRelation(int componentIndex) const
96 {
97 return componentInfo[componentIndex].gtRelation;
98 }
99
100 inline Bdd
getLeqRelation(int sortIndex) const101 SortBdds::getLeqRelation(int sortIndex) const
102 {
103 return leqRelations[sortIndex];
104 }
105
106 #endif
107