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 // Implementation for class AssignmentConditionFragment.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 //#include "variable.hh"
35
36 // interface class definitions
37 //#include "symbol.hh"
38 //#include "dagNode.hh"
39 #include "term.hh"
40 #include "lhsAutomaton.hh"
41 #include "rhsAutomaton.hh"
42 #include "subproblem.hh"
43
44 // core class definitions
45 #include "rewritingContext.hh"
46 #include "variableInfo.hh"
47
48 // higher class definitions
49 #include "assignmentConditionState.hh"
50 #include "assignmentConditionFragment.hh"
51
AssignmentConditionFragment(Term * lhs,Term * rhs)52 AssignmentConditionFragment::AssignmentConditionFragment(Term* lhs, Term* rhs)
53 : lhs(lhs),
54 rhs(rhs)
55 {
56 lhsMatcher = 0;
57 rhsIndex = NONE;
58 }
59
~AssignmentConditionFragment()60 AssignmentConditionFragment::~AssignmentConditionFragment()
61 {
62 lhs->deepSelfDestruct();
63 rhs->deepSelfDestruct();
64 delete lhsMatcher;
65 }
66
67 void
check(VariableInfo & variableInfo,NatSet & boundVariables)68 AssignmentConditionFragment::check(VariableInfo& variableInfo, NatSet& boundVariables)
69 {
70 NatSet unboundVariables;
71
72 lhs = lhs->normalize(true);
73 lhs->indexVariables(variableInfo);
74 variableInfo.addConditionVariables(lhs->occursBelow());
75
76 rhs = rhs->normalize(false);
77 rhs->indexVariables(variableInfo);
78 variableInfo.addConditionVariables(rhs->occursBelow());
79 unboundVariables.insert(rhs->occursBelow());
80
81 unboundVariables.subtract(boundVariables);
82 variableInfo.addUnboundVariables(unboundVariables);
83 boundVariables.insert(lhs->occursBelow());
84 }
85
86 void
preprocess()87 AssignmentConditionFragment::preprocess()
88 {
89 lhs->symbol()->fillInSortInfo(lhs);
90 lhs->analyseCollapses();
91 rhs->symbol()->fillInSortInfo(rhs);
92 Assert(lhs->getComponent() == rhs->getComponent(), "component clash");
93 }
94
95 void
compileBuild(VariableInfo & variableInfo,TermBag & availableTerms)96 AssignmentConditionFragment::compileBuild(VariableInfo& variableInfo, TermBag& availableTerms)
97 {
98 rhsIndex = rhs->compileRhs(builder, variableInfo, availableTerms, true);
99 variableInfo.useIndex(rhsIndex);
100 lhs->findAvailableTerms(availableTerms, true);
101 lhs->determineContextVariables();
102 lhs->insertAbstractionVariables(variableInfo);
103 variableInfo.endOfFragment();
104 }
105
106 void
compileMatch(VariableInfo & variableInfo,NatSet & boundUniquely)107 AssignmentConditionFragment::compileMatch(VariableInfo& variableInfo, NatSet& boundUniquely)
108 {
109 builder.remapIndices(variableInfo);
110 rhsIndex = variableInfo.remapIndex(rhsIndex);
111 bool subproblemLikely;
112 lhsMatcher = lhs->compileLhs(false, variableInfo, boundUniquely, subproblemLikely);
113 boundUniquely.insert(lhs->occursBelow());
114 }
115
116 bool
solve(bool findFirst,RewritingContext & solution,stack<ConditionState * > & state)117 AssignmentConditionFragment::solve(bool findFirst,
118 RewritingContext& solution,
119 stack<ConditionState*>& state)
120 {
121 if (findFirst)
122 {
123 builder.safeConstruct(solution);
124 AssignmentConditionState* cs =
125 new AssignmentConditionState(solution, lhsMatcher, solution.value(rhsIndex));
126 if (cs->solve(true, solution))
127 {
128 state.push(cs);
129 return true;
130 }
131 delete cs;
132 }
133 else
134 {
135 AssignmentConditionState* cs = safeCast(AssignmentConditionState*, state.top());
136 if (cs->solve(false, solution))
137 return true;
138 delete cs;
139 state.pop();
140 }
141 return false;
142 }
143
144 DagNode*
makeRhsInstance(Substitution & solution)145 AssignmentConditionFragment::makeRhsInstance(Substitution& solution)
146 {
147 builder.safeConstruct(solution);
148 return solution.value(rhsIndex);
149 }
150
151 bool
matchRoot(RewritingContext & context,Subproblem * & subproblem)152 AssignmentConditionFragment::matchRoot(RewritingContext& context, Subproblem*& subproblem)
153 {
154 subproblem = 0;
155 return lhsMatcher->match(context.root(), context, subproblem);
156 }
157