1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 2014 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 // Implementation for class SMT_NumberSymbol.
25 //
26
27 // utility stuff
28 #include "macros.hh"
29 #include "vector.hh"
30
31 // forward declarations
32 #include "interface.hh"
33 #include "core.hh"
34 #include "NA_Theory.hh"
35 #include "SMT.hh"
36
37 // interface class definitions
38 #include "term.hh"
39
40 // core class definitions
41 #include "rewritingContext.hh"
42 #include "symbolMap.hh"
43
44 // built in stuff
45 #include "bindingMacros.hh"
46
47 // SMT stuff
48 #include "SMT_Info.hh"
49 #include "SMT_NumberSymbol.hh"
50 #include "SMT_NumberTerm.hh"
51 #include "SMT_NumberDagNode.hh"
52
SMT_NumberSymbol(int id)53 SMT_NumberSymbol::SMT_NumberSymbol(int id)
54 : NA_Symbol(id)
55 {
56 numberSystem = NONE;
57 }
58
59 bool
attachData(const Vector<Sort * > & opDeclaration,const char * purpose,const Vector<const char * > & data)60 SMT_NumberSymbol::attachData(const Vector<Sort*>& opDeclaration,
61 const char* purpose,
62 const Vector<const char*>& data)
63 {
64 BIND_OP(purpose, SMT_NumberSymbol, numberSystem, data);
65 return NA_Symbol::attachData(opDeclaration, purpose, data);
66 }
67
68 void
copyAttachments(Symbol * original,SymbolMap * map)69 SMT_NumberSymbol::copyAttachments(Symbol* original, SymbolMap* map)
70 {
71 SMT_NumberSymbol* orig = safeCast(SMT_NumberSymbol*, original);
72 numberSystem = orig->numberSystem;
73 NA_Symbol::copyAttachments(original, map);
74 }
75
76 void
getDataAttachments(const Vector<Sort * > & opDeclaration,Vector<const char * > & purposes,Vector<Vector<const char * >> & data)77 SMT_NumberSymbol::getDataAttachments(const Vector<Sort*>& opDeclaration,
78 Vector<const char*>& purposes,
79 Vector<Vector<const char*> >& data)
80 {
81 if (numberSystem != NONE)
82 {
83 int nrDataAttachments = purposes.length();
84 purposes.resize(nrDataAttachments + 1);
85 purposes[nrDataAttachments] = "SMT_NumberSymbol";
86 data.resize(nrDataAttachments + 1);
87 data[nrDataAttachments].resize(1);
88 const char*& d = data[nrDataAttachments][0];
89
90 switch (numberSystem)
91 {
92 CODE_CASE(d, 'i', 'n', "integers");
93 CODE_CASE(d, 'r', 'e', "reals");
94 default:
95 CantHappen("bad SMT number system");
96 }
97 }
98 NA_Symbol::getDataAttachments(opDeclaration, purposes, data);
99 }
100
101 void
fillOutSMT_Info(SMT_Info & info)102 SMT_NumberSymbol::fillOutSMT_Info(SMT_Info& info)
103 {
104 //
105 // If we are the construction operator for some SMT type, fill out that information.
106 //
107 switch (numberSystem)
108 {
109 case CODE('i', 'n'):
110 {
111 info.setType(getRangeSort(), SMT_Info::INTEGER);
112 break;
113 }
114 case CODE('r', 'e'):
115 {
116 info.setType(getRangeSort(), SMT_Info::REAL);
117 break;
118 }
119 default:
120 break;
121 }
122 }
123
124 Term*
termify(DagNode * dagNode)125 SMT_NumberSymbol::termify(DagNode* dagNode)
126 {
127 return new SMT_NumberTerm(this, safeCast(SMT_NumberDagNode*, dagNode)->getValue());
128 }
129