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 ConditionFragment.
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 "higher.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 #include "rewriteConditionState.hh"
48 #include "rewriteConditionFragment.hh"
49
RewriteConditionFragment(Term * lhs,Term * rhs)50 RewriteConditionFragment::RewriteConditionFragment(Term* lhs, Term* rhs)
51 : lhs(lhs),
52 rhs(rhs)
53 {
54 lhsIndex = NONE;
55 rhsMatcher = 0;
56 }
57
~RewriteConditionFragment()58 RewriteConditionFragment::~RewriteConditionFragment()
59 {
60 lhs->deepSelfDestruct();
61 rhs->deepSelfDestruct();
62 delete rhsMatcher;
63 }
64
65 void
check(VariableInfo & variableInfo,NatSet & boundVariables)66 RewriteConditionFragment::check(VariableInfo& variableInfo, NatSet& boundVariables)
67 {
68 NatSet unboundVariables;
69
70 lhs = lhs->normalize(false);
71 lhs->indexVariables(variableInfo);
72 variableInfo.addConditionVariables(lhs->occursBelow());
73 unboundVariables.insert(lhs->occursBelow());
74
75 rhs = rhs->normalize(true);
76 rhs->indexVariables(variableInfo);
77 variableInfo.addConditionVariables(rhs->occursBelow());
78
79 unboundVariables.subtract(boundVariables);
80 variableInfo.addUnboundVariables(unboundVariables);
81 boundVariables.insert(rhs->occursBelow());
82 }
83
84 void
preprocess()85 RewriteConditionFragment::preprocess()
86 {
87 lhs->symbol()->fillInSortInfo(lhs);
88 rhs->symbol()->fillInSortInfo(rhs);
89 Assert(lhs->getComponent() == rhs->getComponent(), "component clash");
90 rhs->analyseCollapses();
91 }
92
93 void
compileBuild(VariableInfo & variableInfo,TermBag & availableTerms)94 RewriteConditionFragment::compileBuild(VariableInfo& variableInfo, TermBag& availableTerms)
95 {
96
97 lhsIndex = lhs->compileRhs(builder, variableInfo, availableTerms, true);
98 variableInfo.useIndex(lhsIndex);
99 rhs->findAvailableTerms(availableTerms, true);
100 rhs->determineContextVariables();
101 rhs->insertAbstractionVariables(variableInfo);
102 variableInfo.endOfFragment();
103 }
104
105 void
compileMatch(VariableInfo & variableInfo,NatSet & boundUniquely)106 RewriteConditionFragment::compileMatch(VariableInfo& variableInfo, NatSet& boundUniquely)
107 {
108 builder.remapIndices(variableInfo);
109 lhsIndex = variableInfo.remapIndex(lhsIndex);
110 bool subproblemLikely;
111 rhsMatcher = rhs->compileLhs(false, variableInfo, boundUniquely, subproblemLikely);
112 boundUniquely.insert(rhs->occursBelow());
113 }
114
115 bool
solve(bool findFirst,RewritingContext & solution,stack<ConditionState * > & state)116 RewriteConditionFragment::solve(bool findFirst,
117 RewritingContext& solution,
118 stack<ConditionState*>& state)
119 {
120 if (findFirst)
121 {
122 builder.safeConstruct(solution);
123 RewriteConditionState* cs =
124 new RewriteConditionState(solution, solution.value(lhsIndex), rhsMatcher);
125 if (cs->solve(true, solution))
126 {
127 state.push(cs);
128 return true;
129 }
130 delete cs;
131 }
132 else
133 {
134 RewriteConditionState* cs = safeCast(RewriteConditionState*, state.top());
135 if (cs->solve(false, solution))
136 return true;
137 delete cs;
138 state.pop();
139 }
140 return false;
141 }
142
143 DagNode*
makeLhsInstance(Substitution & solution)144 RewriteConditionFragment::makeLhsInstance(Substitution& solution)
145 {
146 builder.safeConstruct(solution);
147 return solution.value(lhsIndex);
148 }
149
150 bool
matchRoot(RewritingContext & context,Subproblem * & subproblem)151 RewriteConditionFragment::matchRoot(RewritingContext& context, Subproblem*& subproblem)
152 {
153 subproblem = 0;
154 return rhsMatcher->match(context.root(), context, subproblem);
155 }
156