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 terms in the sucessor theory.
25 //
26 #ifndef _S_Term_hh_
27 #define _S_Term_hh_
28 #include <gmpxx.h>
29 #include "term.hh"
30
31 class S_Term : public Term
32 {
33 NO_COPYING(S_Term);
34
35 public:
36 S_Term(S_Symbol* symbol, const mpz_class& number, Term* arg);
37 //
38 // Functions required by theory interface.
39 //
40 RawArgumentIterator* arguments();
41 void deepSelfDestruct();
42 Term* deepCopy2(SymbolMap* map) const;
43 Term* normalize(bool full, bool& changed);
44 int compareArguments(const Term* other) const;
45 int compareArguments(const DagNode* other) const;
46 void findEagerVariables(bool atTop, NatSet& eagerVariables) const;
47 void analyseConstraintPropagation(NatSet& boundUniquely) const;
48 void insertAbstractionVariables(VariableInfo& variableInfo);
49 LhsAutomaton* compileLhs2(bool matchAtTop,
50 const VariableInfo& variableInfo,
51 NatSet& boundUniquely,
52 bool& subproblemLikely);
53 void markEagerArguments(int nrVariables,
54 const NatSet& eagerVariables,
55 Vector<int>& problemVariables);
56 DagNode* dagify2();
57 void findAvailableTerms(TermBag& availableTerms, bool eagerContext, bool atTop);
58 int compileRhs2(RhsBuilder& rhsBuilder,
59 VariableInfo& variableInfo,
60 TermBag& availableTerms,
61 bool eagerContext);
62 //
63 // Needed because we have hidden data.
64 //
65 Term* instantiate2(const Vector<Term*>& varBindings, SymbolMap* translator);
66
67 #ifdef DUMP
68 void dump(ostream& s, const VariableInfo& variableInfo, int indentLevel);
69 #endif
70 //
71 // Functions specific to S_Term.
72 //
73 S_Symbol* symbol() const;
74 const mpz_class& getNumber() const;
75 Term* getArgument() const;
76
77 private:
78 S_Term(const S_Term& original, S_Symbol* symbol, SymbolMap* translator);
79
80 mpz_class number;
81 Term* arg;
82 int abstractionVariableIndex;
83 };
84
85 inline S_Symbol*
symbol() const86 S_Term::symbol() const
87 {
88 return safeCast(S_Symbol*, Term::symbol());
89 }
90
91 inline const mpz_class&
getNumber() const92 S_Term::getNumber() const
93 {
94 return number;
95 }
96
97 inline Term*
getArgument() const98 S_Term::getArgument() const
99 {
100 return arg;
101 }
102
103 #endif
104