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 symbols for built in operations on numbers.
25 //
26 #ifndef _numberOpSymbol_hh_
27 #define _numberOpSymbol_hh_
28 #include "freeSymbol.hh"
29 #include "cachedDag.hh"
30 #include "gmpxx.h"
31
32 class NumberOpSymbol : public FreeSymbol
33 {
34 public:
35 NumberOpSymbol(int id, int arity);
36
37 bool attachData(const Vector<Sort*>& opDeclaration,
38 const char* purpose,
39 const Vector<const char*>& data);
40 bool attachSymbol(const char* purpose, Symbol* symbol);
41 bool attachTerm(const char* purpose, Term* term);
42 void copyAttachments(Symbol* original, SymbolMap* map);
43 void getDataAttachments(const Vector<Sort*>& opDeclaration,
44 Vector<const char*>& purposes,
45 Vector<Vector<const char*> >& data);
46 void getSymbolAttachments(Vector<const char*>& purposes,
47 Vector<Symbol*>& symbols);
48 void getTermAttachments(Vector<const char*>& purposes,
49 Vector<Term*>& terms);
50
51 void postInterSymbolPass();
52 void reset();
53 bool eqRewrite(DagNode* subject, RewritingContext& context);
54 //
55 // Functions special to NumberOpSymbol.
56 //
57 /*
58 DagNode* makeNegDag(const mpz_class& integer);
59 bool isNeg(const DagNode* dagNode) const;
60 const mpz_class& getNeg(const DagNode* dagNode, mpz_class& result) const;
61 */
62
63 protected:
64 SuccSymbol* getSuccSymbol() const;
65 MinusSymbol* getMinusSymbol() const;
66 bool getNumber(DagNode* dagNode, mpz_class& value) const;
67
68 private:
69 enum ImplementationConstants
70 {
71 EXPONENT_BOUND = 1000000 // max allowed exponent to limit runaway memory use
72 };
73
74 int op;
75 SuccSymbol* succSymbol;
76 MinusSymbol* minusSymbol;
77 CachedDag trueTerm;
78 CachedDag falseTerm;
79 };
80
81 inline SuccSymbol*
getSuccSymbol() const82 NumberOpSymbol::getSuccSymbol() const
83 {
84 return succSymbol;
85 }
86 inline MinusSymbol*
getMinusSymbol() const87 NumberOpSymbol::getMinusSymbol() const
88 {
89 return minusSymbol;
90 }
91
92 #endif
93