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 S_Subproblem.
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 #include "S_Theory.hh"
36
37 // interface class definitions
38 //#include "dagNode.hh"
39 //#include "subproblem.hh"
40
41 // core class definitions
42 #include "variableInfo.hh"
43 #include "substitution.hh"
44 #include "rewritingContext.hh"
45 #include "localBinding.hh"
46
47 // S theory class definitions
48 #include "S_Symbol.hh"
49 #include "S_DagNode.hh"
50 #include "S_ExtensionInfo.hh"
51 #include "S_Subproblem.hh"
52
S_Subproblem(S_DagNode * subject,const mpz_class & leftOver,int varIndex,const Sort * varSort,S_ExtensionInfo * extensionInfo,int mustMatchAtLeast)53 S_Subproblem::S_Subproblem(S_DagNode* subject,
54 const mpz_class& leftOver,
55 int varIndex,
56 const Sort* varSort,
57 S_ExtensionInfo* extensionInfo,
58 int mustMatchAtLeast)
59 : subject(subject),
60 leftOver(leftOver),
61 extensionInfo(extensionInfo),
62 varIndex(varIndex),
63 varSort(varSort),
64 mustMatchAtLeast(mustMatchAtLeast)
65 {
66 Assert(leftOver > 0, "only makes sense with leftOver > 0");
67 Assert(extensionInfo != 0, "only makes sense with extensionInfo");
68 Assert(mustMatchAtLeast == 0 || mustMatchAtLeast == 1, "mustMatchAtLeast must be 0 or 1");
69 }
70
71 bool
solve(bool findFirst,RewritingContext & solution)72 S_Subproblem::solve(bool findFirst, RewritingContext& solution)
73 {
74 if (findFirst)
75 {
76 S_DagNode* d = new S_DagNode(subject->symbol(), leftOver, subject->getArgument());
77 solution.bind(varIndex, d); // to protect new dagnode
78 if (d->checkSort(varSort, solution))
79 {
80 extensionInfo->setMatchedWhole(true);
81 extensionInfo->setUnmatched(0);
82 return true;
83 }
84 }
85 for (;;)
86 {
87 mpz_class newUnmatched = extensionInfo->getUnmatched() + 1;
88 mpz_class matched = leftOver - newUnmatched;
89 if (matched < mustMatchAtLeast)
90 break; // fail
91
92 extensionInfo->setUnmatched(newUnmatched);
93 DagNode* d = subject->getArgument();
94 if (matched > 0)
95 d = new S_DagNode(subject->symbol(), matched, d);
96 solution.bind(varIndex, d); // to protect potentially new dagnode
97
98 if (d->checkSort(varSort, solution))
99 {
100 extensionInfo->setMatchedWhole(false);
101 return true;
102 }
103 }
104 return false;
105 }
106
107 #ifdef DUMP
108 void
dump(ostream & s,const VariableInfo & variableInfo,int indentLevel)109 S_Subproblem::dump(ostream& s, const VariableInfo& variableInfo, int indentLevel)
110 {
111 s << Indent(indentLevel) << "Begin{S_Subproblem}\n";
112 ++indentLevel;
113 s << Indent(indentLevel) << "subject = " << subject << '\n';
114 s << Indent(indentLevel) << "leftOver = " << leftOver << '\n';
115 s << Indent(indentLevel) << "varIndex = " << varIndex <<
116 " \"" << variableInfo.index2Variable(varIndex) << "\"\n";
117 s << Indent(indentLevel) << "varSort = " << varSort << '\n';
118 s << Indent(indentLevel) << "extensionInfo = " << extensionInfo << '\n';
119 s << Indent(indentLevel - 1) << "End{S_Subproblem}\n";
120 }
121 #endif
122