CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
translator.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file translator.h
4
* \brief An exception to be thrown by the smtlib translator.
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Sat Jun 25 18:03:09 2005
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
#ifndef _cvc3__translator_h_
23
#define _cvc3__translator_h_
24
25
#include <string>
26
#include <fstream>
27
#include <vector>
28
#include <map>
29
#include "
queryresult.h
"
30
#include "
compat_hash_map.h
"
31
32
namespace
CVC3 {
33
34
class
Expr;
35
template
<
class
Data>
class
ExprMap;
36
class
Type;
37
class
ExprManager;
38
class
ExprStream;
39
class
TheoryCore;
40
class
TheoryUF;
41
class
TheoryArith;
42
class
TheoryArray;
43
class
TheoryQuant;
44
class
TheoryRecords;
45
class
TheorySimulate;
46
class
TheoryBitvector;
47
class
TheoryDatatype;
48
template
<
class
Data>
class
ExprMap;
49
50
//! Used to keep track of which subset of arith is being used
51
typedef
enum
{
52
NOT_USED
= 0,
53
TERMS_ONLY
,
54
DIFF_ONLY
,
55
LINEAR
,
56
NONLINEAR
57
}
ArithLang
;
58
59
//All the translation code should go here
60
class
Translator
{
61
ExprManager
*
d_em
;
62
const
bool
&
d_translate
;
63
const
bool
&
d_real2int
;
64
const
bool
&
d_convertArith
;
65
const
std::string&
d_convertToDiff
;
66
bool
d_iteLiftArith
;
67
const
std::string&
d_expResult
;
68
std::string
d_category
;
69
bool
d_convertArray
;
70
bool
d_combineAssump
;
71
72
/** Private class for hashing strings; copied from ExprManager */
73
class
HashString
{
74
std::hash<char*>
h
;
75
public
:
76
size_t
operator()
(
const
std::string& s)
const
{
77
return
h
(const_cast<char*>(s.c_str()));
78
}
79
};
80
std::hash_map<std::string, std::string, HashString>
d_replaceSymbols
;
81
82
//! The log file for top-level API calls in the CVC3 input language
83
std::ostream*
d_osdump
;
84
std::ofstream
d_osdumpFile
;
85
std::ifstream
d_tmpFile
;
86
bool
d_dump
,
d_dumpFileOpen
;
87
88
bool
d_intIntArray
,
d_intRealArray
,
d_intIntRealArray
,
d_ax
,
d_unknown
;
89
bool
d_realUsed
;
90
bool
d_intUsed
;
91
bool
d_intConstUsed
;
92
ArithLang
d_langUsed
;
93
bool
d_UFIDL_ok
;
94
bool
d_arithUsed
;
95
96
Expr
*
d_zeroVar
;
97
int
d_convertToBV
;
98
99
TheoryCore
*
d_theoryCore
;
100
TheoryUF
*
d_theoryUF
;
101
TheoryArith
*
d_theoryArith
;
102
TheoryArray
*
d_theoryArray
;
103
TheoryQuant
*
d_theoryQuant
;
104
TheoryRecords
*
d_theoryRecords
;
105
TheorySimulate
*
d_theorySimulate
;
106
TheoryBitvector
*
d_theoryBitvector
;
107
TheoryDatatype
*
d_theoryDatatype
;
108
109
std::vector<Expr>
d_dumpExprs
;
110
111
std::map<std::string, Type>*
d_arrayConvertMap
;
112
Type
*
d_indexType
;
113
Type
*
d_elementType
;
114
Type
*
d_arrayType
;
115
std::vector<Expr>
d_equalities
;
116
117
// Name of benchmark in SMT-LIB
118
std::string
d_benchName
;
119
// Status of benchmark in SMT-LIB
120
std::string
d_status
;
121
// Source of benchmark in SMT-LIB
122
std::string
d_source
;
123
124
std::string
fileToSMTLIBIdentifier
(
const
std::string& filename);
125
Expr
preprocessRec
(
const
Expr
& e,
ExprMap<Expr>
& cache);
126
Expr
preprocess
(
const
Expr
& e,
ExprMap<Expr>
& cache);
127
Expr
preprocess2Rec
(
const
Expr
& e,
ExprMap<Expr>
& cache,
Type
desiredType);
128
Expr
preprocess2
(
const
Expr
& e,
ExprMap<Expr>
& cache);
129
bool
containsArray
(
const
Expr
& e);
130
Expr
processType
(
const
Expr
& e);
131
132
/*
133
Expr spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,
134
std::vector<Expr>& functions,
135
std::vector<Expr>& predicates);
136
*/
137
138
public
:
139
// Constructors
140
Translator
(
ExprManager
* em,
141
const
bool
& translate,
142
const
bool
& real2int,
143
const
bool
& convertArith,
144
const
std::string& convertToDiff,
145
bool
iteLiftArith,
146
const
std::string& expResult,
147
const
std::string&
category
,
148
bool
convertArray,
149
bool
combineAssump,
150
int
convertToBV);
151
~Translator
();
152
153
bool
start
(
const
std::string& dumpFile);
154
/*! Dump the expression in the current output language
155
\param dumpOnly When false, the expression is output both when
156
translating and when producing a trace of commands. When true, the
157
expression is only output when producing a trace of commands
158
(i.e. ignored during translation).
159
*/
160
void
dump
(
const
Expr
& e,
bool
dumpOnly =
false
);
161
bool
dumpAssertion
(
const
Expr
& e);
162
bool
dumpQuery
(
const
Expr
& e);
163
void
dumpQueryResult
(
QueryResult
qres);
164
void
finish
();
165
166
void
setTheoryCore
(
TheoryCore
* theoryCore) {
d_theoryCore
= theoryCore; }
167
void
setTheoryUF
(
TheoryUF
* theoryUF) {
d_theoryUF
= theoryUF; }
168
void
setTheoryArith
(
TheoryArith
* theoryArith) {
d_theoryArith
= theoryArith; }
169
void
setTheoryArray
(
TheoryArray
* theoryArray) {
d_theoryArray
= theoryArray; }
170
void
setTheoryQuant
(
TheoryQuant
* theoryQuant) {
d_theoryQuant
= theoryQuant; }
171
void
setTheoryRecords
(
TheoryRecords
* theoryRecords) {
d_theoryRecords
= theoryRecords; }
172
void
setTheorySimulate
(
TheorySimulate
* theorySimulate) {
d_theorySimulate
= theorySimulate; }
173
void
setTheoryBitvector
(
TheoryBitvector
* theoryBitvector) {
d_theoryBitvector
= theoryBitvector; }
174
void
setTheoryDatatype
(
TheoryDatatype
* theoryDatatype) {
d_theoryDatatype
= theoryDatatype; }
175
176
void
setBenchName
(std::string name) {
d_benchName
= name; }
177
std::string
benchName
() {
return
d_benchName
; }
178
void
setStatus
(std::string
status
) {
d_status
=
status
; }
179
std::string
status
() {
return
d_status
; }
180
void
setSource
(std::string
source
) {
d_source
=
source
; }
181
std::string
source
() {
return
d_source
; }
182
void
setCategory
(std::string
category
) {
d_category
=
category
; }
183
std::string
category
() {
return
d_category
; }
184
185
const
std::string
fixConstName
(
const
std::string& s);
186
const
std::string
escapeSymbol
(
const
std::string& s);
187
const
std::string
quoteAnnotation
(
const
std::string& s);
188
//! Returns true if expression has been printed
189
/*! If false is returned, array theory should print expression as usual */
190
bool
printArrayExpr
(
ExprStream
& os,
const
Expr
& e);
191
192
Expr
zeroVar
();
193
194
};
// end of class Translator
195
196
}
// end of namespace CVC3
197
198
#endif
Generated on Sat Aug 3 2013 07:58:39 for CVC3 by
1.8.4