1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2008 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 unification subproblems in the C theory.
25 // It consists of a vector of unification problems of the form f(u, v) =? f(s, t) where f is a C symbol.
26 //
27 #ifndef _CUI_UnificationSubproblem_hh_
28 #define _CUI_UnificationSubproblem_hh_
29 //#include <list>
30 #include "unificationSubproblem.hh"
31 #include "simpleRootContainer.hh"
32 //#include "natSet.hh"
33 //#include "dagNode.hh"
34 //#include "dagNodeSet.hh"
35 #include "substitution.hh"
36 #include "pendingUnificationStack.hh"
37
38 class CUI_UnificationSubproblem : public UnificationSubproblem, private SimpleRootContainer
39 {
40 NO_COPYING(CUI_UnificationSubproblem);
41
42 public:
43 CUI_UnificationSubproblem();
44 ~CUI_UnificationSubproblem();
45
46 void addUnification(DagNode* lhs, DagNode* rhs, bool marked, UnificationContext& solution);
47 bool solve(bool findFirst, UnificationContext& solution, PendingUnificationStack& pending);
48
49 #ifdef DUMP
50 //void dump(ostream& s, const VariableInfo& variableInfo, int indentLevel);
51 #endif
52
53 private:
54 struct Problem
55 {
56 Problem(CUI_DagNode* lhs, CUI_DagNode* rhs);
57 Problem();
58 Problem(const Problem& original);
59
60 CUI_DagNode* const lhs;
61 CUI_DagNode* const rhs;
62 Substitution savedSubstitution;
63 PendingUnificationStack::Marker savedPendingState;
64 bool reverseTried;
65 };
66
67 void markReachableNodes();
68
69 Vector<Problem> problems;
70 };
71
72 inline
Problem()73 CUI_UnificationSubproblem::Problem::Problem() // HACK
74 : lhs(0),
75 rhs(0),
76 savedSubstitution(0)
77 {
78 }
79
80 inline
Problem(CUI_DagNode * lhs,CUI_DagNode * rhs)81 CUI_UnificationSubproblem::Problem::Problem(CUI_DagNode* lhs, CUI_DagNode* rhs)
82 : lhs(lhs),
83 rhs(rhs),
84 savedSubstitution(0)
85 {
86 }
87
88 inline
Problem(const Problem & original)89 CUI_UnificationSubproblem::Problem::Problem(const Problem& original)
90 : lhs(original.lhs),
91 rhs(original.rhs),
92 savedSubstitution(0) // HACK
93 {
94 }
95
96 #endif
97