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 rewrite rules
25 //
26 #ifndef _rule_hh_
27 #define _rule_hh_
28 #include "preEquation.hh"
29 #include "rhsBuilder.hh"
30
31 class Rule : public PreEquation
32 {
33 public:
34 Rule(int label,
35 Term* lhs,
36 Term* rhs,
37 const Vector<ConditionFragment*>& condition = noCondition);
38 ~Rule();
39
40 Term* getRhs() const;
41 void check();
42 void preprocess();
43 void compile(bool compileLhs);
44 const RhsBuilder& getRhsBuilder() const;
45 LhsAutomaton* getNonExtLhsAutomaton();
46 LhsAutomaton* getExtLhsAutomaton();
47 void print(ostream& s) const;
48
49 private:
50 int traceBeginTrial(DagNode* subject, RewritingContext& context) const;
51
52 Term* rhs;
53 RhsBuilder builder;
54 LhsAutomaton* nonExtLhsAutomaton;
55 LhsAutomaton* extLhsAutomaton;
56 DagRoot lhsDag; // for unification
57 };
58
59 inline Term*
getRhs() const60 Rule::getRhs() const
61 {
62 return rhs;
63 }
64
65 inline const RhsBuilder&
getRhsBuilder() const66 Rule::getRhsBuilder() const
67 {
68 return builder;
69 }
70
71 //
72 // Output function for Rule must be defined by library user
73 //
74 ostream& operator<<(ostream& s, const Rule* rule);
75
76 #endif
77