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 DAG nodes in the successor theory.
25 //
26 #ifndef _S_DagNode_hh_
27 #define _S_DagNode_hh_
28 #include "gmpxx.h"
29 #include "dagNode.hh"
30
31 class S_DagNode : public DagNode
32 {
33 NO_COPYING(S_DagNode);
34
35 public:
36 S_DagNode(S_Symbol* symbol, const mpz_class& number, DagNode* arg);
37 ~S_DagNode();
38 //
39 // Functions required by theory interface.
40 //
41 RawDagArgumentIterator* arguments();
42 size_t getHashValue();
43 int compareArguments(const DagNode* other) const;
44 void overwriteWithClone(DagNode* old);
45 DagNode* makeClone();
46 DagNode* copyWithReplacement(int argIndex, DagNode* replacement);
47 DagNode* copyWithReplacement(Vector<RedexPosition>& redexStack,
48 int first,
49 int last);
50 void stackArguments(Vector<RedexPosition>& stack,
51 int parentIndex,
52 bool respectFrozen);
53 //
54 // Functions required to handle extension information.
55 //
56 bool matchVariableWithExtension(int index,
57 const Sort* sort,
58 Substitution& solution,
59 Subproblem*& returnedSubproblem,
60 ExtensionInfo* extensionInfo);
61 void partialReplace(DagNode* replacement, ExtensionInfo* extensionInfo);
62 DagNode* partialConstruct(DagNode* replacement, ExtensionInfo* extensionInfo);
63 ExtensionInfo* makeExtensionInfo();
64 //
65 // Unification member functions.
66 //
67 ReturnResult computeBaseSortForGroundSubterms();
68 bool computeSolvedForm2(DagNode* rhs, UnificationContext& solution, PendingUnificationStack& pending);
69
70 void insertVariables2(NatSet& occurs);
71 DagNode* instantiate2(const Substitution& substitution);
72 //
73 // Narrowing member functions.
74 //
75 DagNode* instantiateWithReplacement(const Substitution& substitution, const Vector<DagNode*>& eagerCopies, int argIndex, DagNode* newDag);
76 DagNode* instantiateWithCopies2(const Substitution& substitution, const Vector<DagNode*>& eagerCopies);
77 //
78 // Functions specific to S_DagNode.
79 //
80 S_Symbol* symbol() const;
81 const mpz_class& getNumber() const;
82 DagNode* getArgument() const;
83
84 private:
85 //
86 // Functions required by theory interface.
87 //
88 DagNode* markArguments();
89 DagNode* copyEagerUptoReduced2();
90 void clearCopyPointers2();
91 //
92 // Normalization functions.
93 //
94 void normalizeAtTop();
95
96 mpz_class* number;
97 DagNode* arg;
98
99 friend class S_Symbol; // to reduce subterms prior to rewrite, normalization
100 };
101
102 inline S_Symbol*
symbol() const103 S_DagNode::symbol() const
104 {
105 return safeCast(S_Symbol*, DagNode::symbol());
106 }
107
108 inline const mpz_class&
getNumber() const109 S_DagNode::getNumber() const
110 {
111 return *number;
112 }
113
114 inline DagNode*
getArgument() const115 S_DagNode::getArgument() const
116 {
117 return arg;
118 }
119
120 #endif
121