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 // Implementation for class CUI_UnificationSubproblem.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30 #include "indent.hh"
31
32 // forward declarations
33 #include "interface.hh"
34 #include "core.hh"
35
36 // interface class definitions
37 #include "dagNode.hh"
38
39 // core class definitions
40 #include "unificationSubproblemDisjunction.hh"
41
42 void
addUnification(DagNode * lhs,DagNode * rhs,bool,UnificationContext &)43 UnificationSubproblemDisjunction::addUnification(DagNode* lhs, DagNode* rhs, bool /* marked */, UnificationContext& /* solution */)
44 {
45 int nrProblems = problems.size();
46 problems.expandBy(1);
47 problems[nrProblems].lhs = lhs;
48 problems[nrProblems].rhs = rhs;
49 }
50
51 bool
solve(bool findFirst,UnificationContext &,PendingUnificationStack & pending)52 UnificationSubproblemDisjunction::solve(bool findFirst, UnificationContext& /* solution */, PendingUnificationStack& pending)
53 {
54 //
55 // We only push problems on the pending stack and restore the pending stack.
56 // We don't touch the substitution so we don't need to save or restore it.
57 //
58 int nrProblems = problems.size();
59 int i;
60 if (findFirst)
61 i = 0;
62 else
63 {
64 for (i = nrProblems - 1;; --i)
65 {
66 TheoryClash& p = problems[i];
67 if (p.lhsControlling)
68 {
69 //
70 // Restore the state to what it was before we pushed the
71 // problem with the lhs controlling.
72 //
73 pending.restore(p.savedPendingState);
74 p.lhsControlling = false;
75 pending.push(p.rhs->symbol(), p.rhs, p.lhs, true); // swap lhs and rhs
76 ++i;
77 break;
78 }
79 if (i == 0)
80 {
81 //
82 // All combinations exhausted; restore intial state.
83 //
84 pending.restore(p.savedPendingState);
85 return false;
86 }
87 }
88 }
89 //
90 // Give lhs control of any remaining problems.
91 //
92 for (; i < nrProblems; ++i)
93 {
94 TheoryClash& p = problems[i];
95 p.savedPendingState = pending.checkPoint();
96 p.lhsControlling = true;
97 pending.push(p.lhs->symbol(), p.lhs, p.rhs, true);
98 }
99 return true;
100 }
101