1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
|
/********************* */
/*! \file tptp.cpp
** \verbatim
** Original author: Francois Bobot
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Definitions of TPTP constants.
**
** Definitions of TPTP constants.
**/
#include "expr/type.h"
#include "parser/parser.h"
#include "parser/tptp/tptp.h"
#include "parser/antlr_input.h"
// ANTLR defines these, which is really bad!
#undef true
#undef false
namespace CVC4 {
namespace parser {
Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
Parser(exprManager,input,strictMode,parseOnly) {
addTheory(Tptp::THEORY_CORE);
/* Try to find TPTP dir */
// From tptp4x FileUtilities
//----Try the TPTP directory, and TPTP variations
char* home = getenv("TPTP");
if(home == NULL) {
home = getenv("TPTP_HOME");
// //----If no TPTP_HOME, try the tptp user (aaargh)
// if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
// home = PasswdEntry->pw_dir;
// }
//----Now look in the TPTP directory from there
if(home != NULL) {
d_tptpDir = home;
d_tptpDir.append("/TPTP/");
}
} else {
d_tptpDir = home;
//add trailing "/"
if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
d_tptpDir.append("/");
}
}
d_hasConjecture = false;
}
void Tptp::addTheory(Theory theory) {
ExprManager * em = getExprManager();
switch(theory) {
case THEORY_CORE:
//TPTP (CNF and FOF) is unsorted so we define this common type
{
std::string d_unsorted_name = "$$unsorted";
d_unsorted = em->mkSort(d_unsorted_name);
preemptCommand( new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted) );
}
// propositionnal
defineType("Bool", em->booleanType());
defineVar("$true", em->mkConst(true));
defineVar("$false", em->mkConst(false));
addOperator(kind::AND);
addOperator(kind::EQUAL);
addOperator(kind::IFF);
addOperator(kind::IMPLIES);
//addOperator(kind::ITE); //only for tff thf
addOperator(kind::NOT);
addOperator(kind::OR);
addOperator(kind::XOR);
addOperator(kind::APPLY_UF);
//Add quantifiers?
break;
default:
std::stringstream ss;
ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
throw ParserException(ss.str());
}
}
/* The include are managed in the lexer but called in the parser */
// Inspired by http://www.antlr3.org/api/C/interop.html
bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) {
Debug("parser") << "Including " << fileName << std::endl;
// Create a new input stream and take advantage of built in stream stacking
// in C target runtime.
//
pANTLR3_INPUT_STREAM in;
#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) fileName.c_str());
#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
if(in == NULL) {
Debug("parser") << "Can't open " << fileName << std::endl;
return false;
}
// Same thing as the predefined PUSHSTREAM(in);
lexer->pushCharStream(lexer,in);
// restart it
//lexer->rec->state->tokenStartCharIndex = -10;
//lexer->emit(lexer);
// Note that the input stream is not closed when it EOFs, I don't bother
// to do it here, but it is up to you to track streams created like this
// and destroy them when the whole parse session is complete. Remember that you
// don't want to do this until all tokens have been manipulated all the way through
// your tree parsers etc as the token does not store the text it just refers
// back to the input stream and trying to get the text for it will abort if you
// close the input stream too early.
//
//TODO what said before
return true;
}
/* overridden popCharStream for the lexer - necessary if we had symbol
* filtering in file inclusion.
void Tptp::myPopCharStream(pANTLR3_LEXER lexer) {
((Tptp*)lexer->super)->d_oldPopCharStream(lexer);
((Tptp*)lexer->super)->popScope();
}
*/
void Tptp::includeFile(std::string fileName) {
// security for online version
if(!canIncludeFile()) {
parseError("include-file feature was disabled for this run.");
}
// Get the lexer
AntlrInput * ai = static_cast<AntlrInput *>(getInput());
pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
// set up popCharStream - would be necessary for handling symbol
// filtering in inclusions
/*
if(d_oldPopCharStream == NULL) {
d_oldPopCharStream = lexer->popCharStream;
lexer->popCharStream = myPopCharStream;
}
*/
// push the inclusion scope; will be popped by our special popCharStream
// would be necessary for handling symbol filtering in inclusions
//pushScope();
// get the name of the current stream "Does it work inside an include?"
const std::string inputName = ai->getInputStreamName();
// Test in the directory of the actual parsed file
std::string currentDirFileName;
if(inputName != "<stdin>") {
// TODO: Use dirname or Boost::filesystem?
size_t pos = inputName.rfind('/');
if(pos != std::string::npos) {
currentDirFileName = std::string(inputName, 0, pos + 1);
}
currentDirFileName.append(fileName);
if(newInputStream(currentDirFileName,lexer)) {
return;
}
} else {
currentDirFileName = "<unknown current directory for stdin>";
}
if(d_tptpDir.empty()) {
parseError("Couldn't open included file: " + fileName
+ " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
};
std::string tptpDirFileName = d_tptpDir + fileName;
if(! newInputStream(tptpDirFileName,lexer)) {
parseError("Couldn't open included file: " + fileName
+ " at " + currentDirFileName + " or " + tptpDirFileName);
}
}
void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) {
if(lhs.getKind() != CVC4::kind::APPLY_UF) {
parseError("malformed let: LHS must be a flat function application");
}
std::vector<CVC4::Expr> v = lhs.getChildren();
if(formula && !lhs.getType().isBoolean()) {
parseError("malformed let: LHS must be formula");
}
for(size_t i = 0; i < v.size(); ++i) {
if(v[i].hasOperator()) {
parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString());
}
}
std::sort(v.begin(), v.end());
std::sort(bvlist.begin(), bvlist.end());
// ensure all let-bound variables appear on the LHS, and appear only once
for(size_t i = 0; i < bvlist.size(); ++i) {
std::vector<CVC4::Expr>::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]);
if(found == v.end() || *found != bvlist[i]) {
parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'");
}
std::vector<CVC4::Expr>::const_iterator found2 = found + 1;
if(found2 != v.end() && *found2 == *found) {
parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString());
}
}
}
}/* CVC4::parser namespace */
}/* CVC4 namespace */
|
