1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2014 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 // Classic to solve sequence assignment problems arising from single elementary
25 // linear associative and AU unification problems.
26 //
27
28 #ifndef _sequenceAssignment_hh_
29 #define _sequenceAssignment_hh_
30
31 class SequenceAssignment
32 {
33 public:
34 SequenceAssignment(int nrLhsVariables, int nrRhsVariables);
35
36 void setLhsBound(int varIndex, int bound);
37 void setRhsBound(int varIndex, int bound);
38 //
39 // Solutions are recorded as a sequence of moves on a grid. The number
40 // of free variables needed to express the correpsonding unifier is 1 plus
41 // the number of moves.
42 //
43 enum Move
44 {
45 NEXT_RIGHT = 1,
46 NEXT_LEFT = 2,
47 NEXT_BOTH = NEXT_RIGHT | NEXT_LEFT
48 };
49
50 static int leftDelta(int move);
51 static int rightDelta(int move);
52
53 typedef Vector<int> Solution;
54
55 bool findNextSolution(bool findFirst);
56 const Solution& getSolution() const;
57
58 private:
59 typedef Vector<int> IntVec;
60
61 void computeBoundSum(const IntVec& bounds, IntVec& boundSum);
62 bool checkAndMakeMove(int move, int& lIndex, int& rIndex);
63 int unmakeMove(int moveIndex, int& lIndex, int& rIndex);
64
65 IntVec lhsBounds;
66 IntVec rhsBounds;
67 IntVec lhsBoundSum;
68 IntVec rhsBoundSum;
69 IntVec lhsCount;
70 IntVec rhsCount;
71
72 Solution currentSolution;
73 };
74
75 inline void
setLhsBound(int varIndex,int bound)76 SequenceAssignment::setLhsBound(int varIndex, int bound)
77 {
78 lhsBounds[varIndex] = bound;
79 }
80
81 inline void
setRhsBound(int varIndex,int bound)82 SequenceAssignment::setRhsBound(int varIndex, int bound)
83 {
84 rhsBounds[varIndex] = bound;
85 }
86
87 inline const SequenceAssignment::Solution&
getSolution() const88 SequenceAssignment::getSolution() const
89 {
90 return currentSolution;
91 }
92
93 inline int
leftDelta(int move)94 SequenceAssignment::leftDelta(int move)
95 {
96 return move >> 1;
97 }
98
99 inline int
rightDelta(int move)100 SequenceAssignment::rightDelta(int move)
101 {
102 return move & 1;
103 }
104
105 #endif
106