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 // Class for condition fragment supporting rewrite search.
25 //
26 #ifndef _rewriteConditionFragment_hh_
27 #define _rewriteConditionFragment_hh_
28 #include "conditionFragment.hh"
29 #include "rhsBuilder.hh"
30
31 class RewriteConditionFragment : public ConditionFragment
32 {
33 NO_COPYING(RewriteConditionFragment);
34
35 public:
36 RewriteConditionFragment(Term* lhs, Term* rhs);
37 ~RewriteConditionFragment();
38
39 void check(VariableInfo& varInfo, NatSet& boundVariables);
40 void preprocess();
41 void compileBuild(VariableInfo& variableInfo, TermBag& availableTerms);
42 void compileMatch(VariableInfo& variableInfo, NatSet& boundUniquely);
43 bool solve(bool findFirst,
44 RewritingContext& solution,
45 stack<ConditionState*>& state);
46
47 Term* getLhs() const;
48 Term* getRhs() const;
49 //
50 // Needed for strategy language.
51 //
52 DagNode* makeLhsInstance(Substitution& solution);
53 bool matchRoot(RewritingContext& context, Subproblem*& subproblem);
54
55 private:
56 Term* lhs;
57 Term* rhs;
58 RhsBuilder builder;
59 int lhsIndex;
60 LhsAutomaton* rhsMatcher;
61 };
62
63 inline Term*
getLhs() const64 RewriteConditionFragment::getLhs() const
65 {
66 return lhs;
67 }
68
69 inline Term*
getRhs() const70 RewriteConditionFragment::getRhs() const
71 {
72 return rhs;
73 }
74
75 #endif
76