cout << unitbuf;
#endif
- /* NOTE: ANTLR3 doesn't support input from stdin */
- if(firstArgIndex >= argc) {
- throw Exception("No input file specified.");
- }
-
// We only accept one input file
if(argc > firstArgIndex + 1) {
throw Exception("Too many input files specified.");
SmtEngine smt(&exprMgr, &options);
// If no file supplied we read from standard input
- // bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+ bool inputFromStdin =
+ firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
// Auto-detect input language by filename extension
- if(/*!inputFromStdin && */options.lang == parser::LANG_AUTO) {
- const char* filename = argv[firstArgIndex];
- unsigned len = strlen(filename);
- if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
- options.lang = parser::LANG_SMTLIB_V2;
- } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- options.lang = parser::LANG_SMTLIB;
- } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
- || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+ const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+
+ if(options.lang == parser::LANG_AUTO) {
+ if( inputFromStdin ) {
+ // We can't do any fancy detection on stdin
options.lang = parser::LANG_CVC4;
+ } else {
+ unsigned len = strlen(filename);
+ if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+ options.lang = parser::LANG_SMTLIB_V2;
+ } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+ options.lang = parser::LANG_SMTLIB;
+ } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+ || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+ options.lang = parser::LANG_CVC4;
+ }
}
}
}
}
- /* TODO: Hack ANTLR3 to support input from streams */
- ParserBuilder parserBuilder(options.lang, argv[firstArgIndex]);
-
- Parser *parser =
- parserBuilder.withExprManager(exprMgr)
+ ParserBuilder parserBuilder =
+ ParserBuilder(exprMgr, filename)
+ .withInputLanguage(options.lang)
.withMmap(options.memoryMap)
- .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() )
- .withStrictMode( options.strictParsing )
- .build();
+ .withChecks(options.semanticChecks &&
+ !Configuration::isMuzzledBuild() )
+ .withStrictMode( options.strictParsing );
+
+ if( inputFromStdin ) {
+ parserBuilder.withStreamInput(cin);
+ }
+
+ Parser *parser = parserBuilder.build();
// Parse and execute commands until we are done
Command* cmd;
namespace CVC4 {
namespace parser {
-AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
- InputStream(name),
+AntlrInputStream::AntlrInputStream(std::string name,
+ pANTLR3_INPUT_STREAM input,
+ bool fileIsTemporary) :
+ InputStream(name,fileIsTemporary),
d_input(input) {
AlwaysAssert( input != NULL );
}
return d_input;
}
-AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap)
+AntlrInputStream*
+AntlrInputStream::newFileInputStream(const std::string& name,
+ bool useMmap)
throw (InputStreamException) {
pANTLR3_INPUT_STREAM input = NULL;
if( useMmap ) {
return new AntlrInputStream( name, input );
}
-AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name)
+AntlrInputStream*
+AntlrInputStream::newStreamInputStream(std::istream& input,
+ const std::string& name)
+ throw (InputStreamException) {
+ // // TODO: make this more portable
+ // char *filename = strdup("/tmp/streaminput.XXXXXX");
+ // int fd = mkstemp(filename);
+ // if( fd == -1 ) {
+ // throw InputStreamException("Couldn't create temporary for stream input: " + name);
+ // }
+
+ // // We don't want to use the temp file directly, so first close it
+ // close(fd);
+
+ // // Make a FIFO with our reserved temporary name
+ // int fd = mkfifo(filename, s_IRUSR);
+
+ // // Just stuff everything from the istream into the FIFO
+ // char buf[4096];
+ // while( !input.eof() && !input.fail() ) {
+ // input.read( buf, sizeof(buf) );
+ // write( fd, buf, input.gcount() );
+ // }
+
+ // if( !input.eof() ) {
+ // throw InputStreamException("Stream input failed: " + name);
+ // }
+
+ // // Now create the ANTLR stream
+ // pANTLR3_INPUT_STREAM input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename);
+
+ // if( input == NULL ) {
+ // throw InputStreamException("Couldn't create stream input: " + name);
+ // }
+
+ // // Create the stream with fileIsTemporary = true
+ // return new AntlrInputStream( name, input, true );
+
+ stringstream ss( ios_base::out );
+ ss << input.rdbuf();
+ return newStringInputStream( ss.str(), name );
+}
+
+
+AntlrInputStream*
+AntlrInputStream::newStringInputStream(const std::string& input,
+ const std::string& name)
throw (InputStreamException) {
char* inputStr = strdup(input.c_str());
char* nameStr = strdup(name.c_str());
class AntlrInputStream : public InputStream {
pANTLR3_INPUT_STREAM d_input;
- AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input);
+ AntlrInputStream(std::string name,
+ pANTLR3_INPUT_STREAM input,
+ bool fileIsTemporary = false);
/* This is private and unimplemented, because you should never use it. */
AntlrInputStream(const AntlrInputStream& inputStream);
* @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
* input will use the standard ANTLR3 I/O implementation.
*/
- static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false)
+ static AntlrInputStream* newFileInputStream(const std::string& name,
+ bool useMmap = false)
throw (InputStreamException);
/** Create an input from an istream. */
- // AntlrInputStream newInputStream(std::istream& input, const std::string& name);
+ static AntlrInputStream* newStreamInputStream(std::istream& input,
+ const std::string& name)
+ throw (InputStreamException);
/** Create a string input.
*
* @param input the string to read
* @param name the "filename" to use when reporting errors
*/
- static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name)
+ static AntlrInputStream* newStringInputStream(const std::string& input,
+ const std::string& name)
throw (InputStreamException);
};
const std::string& filename,
bool useMmap)
throw (InputStreamException) {
- AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap);
+ AntlrInputStream *inputStream =
+ AntlrInputStream::newFileInputStream(filename,useMmap);
+ return AntlrInput::newInput(lang,*inputStream);
+}
+
+Input* Input::newStreamInput(InputLanguage lang,
+ std::istream& input,
+ const std::string& name)
+ throw (InputStreamException) {
+ AntlrInputStream *inputStream =
+ AntlrInputStream::newStreamInputStream(input,name);
return AntlrInput::newInput(lang,*inputStream);
}
#include <iostream>
#include <string>
+#include <stdio.h>
#include <vector>
#include "expr/expr.h"
/** The name of this input stream. */
std::string d_name;
+ /** Indicates whether the input file is a temporary that we should
+ * delete on exit. */
+ bool d_fileIsTemporary;
+
protected:
/** Initialize the input stream with a name. */
- InputStream(std::string name) :
- d_name(name) {
+ InputStream(std::string name, bool isTemporary=false) :
+ d_name(name),
+ d_fileIsTemporary(isTemporary) {
}
public:
- /** Do-nothing destructor. */
- virtual ~InputStream() { }
+ /** Destructor. */
+ virtual ~InputStream() {
+ if( d_fileIsTemporary ) {
+ remove(d_name.c_str());
+ }
+ }
/** Get the name of this input stream. */
const std::string getName() const;
* @param filename the input filename
* @param useMmap true if the parser should use memory-mapped I/O (default: false)
*/
- static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false)
+ static Input* newFileInput(InputLanguage lang,
+ const std::string& filename,
+ bool useMmap=false)
throw (InputStreamException);
/** Create an input for the given stream.
* @param input the input stream
* @param name the name of the stream, for use in error messages
*/
- //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name);
+ static Input* newStreamInput(InputLanguage lang,
+ std::istream& input,
+ const std::string& name)
+ throw (InputStreamException);
/** Create an input for the given string
*
* @param input the input string
* @param name the name of the stream, for use in error messages
*/
- static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
+ static Input* newStringInput(InputLanguage lang,
+ const std::string& input,
+ const std::string& name)
throw (InputStreamException);
public:
}
};*/
-ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) :
+ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) :
d_inputType(FILE_INPUT),
- d_lang(lang),
+ d_lang(LANG_AUTO),
d_filename(filename),
- d_exprManager(NULL),
+ d_streamInput(NULL),
+ d_exprManager(exprManager),
d_checksEnabled(true),
d_strictMode(false),
d_mmap(false) {
}
-Parser *ParserBuilder::build() throw (InputStreamException) {
+Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
Input *input;
switch( d_inputType ) {
case FILE_INPUT:
input = Input::newFileInput(d_lang,d_filename,d_mmap);
break;
+ case STREAM_INPUT:
+ AlwaysAssert( d_streamInput != NULL,
+ "Uninitialized stream input in ParserBuilder::build()" );
+ input = Input::newStreamInput(d_lang,*d_streamInput,d_filename);
+ break;
case STRING_INPUT:
input = Input::newStringInput(d_lang,d_stringInput,d_filename);
break;
}
switch(d_lang) {
case LANG_SMTLIB_V2:
- return new Smt2(d_exprManager, input, d_strictMode);
+ return new Smt2(&d_exprManager, input, d_strictMode);
default:
- return new Parser(d_exprManager, input, d_strictMode);
+ return new Parser(&d_exprManager, input, d_strictMode);
}
}
return *this;
}
+ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
+ d_exprManager = exprManager;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withFileInput() {
+ d_inputType = FILE_INPUT;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withFilename(const std::string& filename) {
+ d_filename = filename;
+ return *this;
+}
+
+ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
+ d_lang = lang;
+ return *this;
+}
+
+
ParserBuilder& ParserBuilder::withMmap(bool flag) {
d_mmap = flag;
return *this;
return *this;
}
-ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
- d_exprManager = &exprManager;
+ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
+ d_inputType = STREAM_INPUT;
+ d_streamInput = &input;
return *this;
}
class Parser;
+/**
+ * A builder for input language parsers. <code>build()</code> can be
+ * called any number of times on an instance and will generate a fresh
+ * parser each time.
+ */
class CVC4_PUBLIC ParserBuilder {
enum InputType {
FILE_INPUT,
+ STREAM_INPUT,
STRING_INPUT
};
/** The string input, if any. */
std::string d_stringInput;
+ /** The stream input, if any. */
+ std::istream *d_streamInput;
+
/** The expression manager */
- ExprManager *d_exprManager;
+ ExprManager& d_exprManager;
/** Should semantic checks be enabled during parsing? */
bool d_checksEnabled;
bool d_mmap;
public:
- ParserBuilder(InputLanguage lang, const std::string& filename);
- Parser *build() throw (InputStreamException);
+
+ /** Create a parser builder using the given ExprManager and filename. */
+ ParserBuilder(ExprManager& exprManager, const std::string& filename);
+
+ /** Build the parser, using the current settings. */
+ Parser *build() throw (InputStreamException,AssertionException);
+
+ /** Should semantic checks be enabled in the parser? (Default: yes) */
ParserBuilder& withChecks(bool flag = true);
+
+ /** Set the ExprManager to use with the parser. */
+ ParserBuilder& withExprManager(ExprManager& exprManager);
+
+ /** Set the parser to read a file for its input. (Default) */
+ ParserBuilder& withFileInput();
+
+ /** Set the filename for use by the parser. If file input is used,
+ * this file will be opened and read by the parser. Otherwise, the
+ * filename string (possibly a non-existent path) will only be used
+ * in error messages. */
+ ParserBuilder& withFilename(const std::string& filename);
+
+ /** Set the input language to be used by the parser. (Default:
+ LANG_AUTO). */
+ ParserBuilder& withInputLanguage(InputLanguage lang);
+
+ /** Should the parser memory-map its input? This is only relevant if
+ * the parser will have a file input. (Default: no) */
ParserBuilder& withMmap(bool flag = true);
+
+ /** Should the parser use strict mode? (Default: no) */
ParserBuilder& withStrictMode(bool flag = true);
- ParserBuilder& withExprManager(ExprManager& exprManager);
+
+ /** Set the parser to use the given stream for its input. */
+ ParserBuilder& withStreamInput(std::istream& input);
+
+ /** Set the parser to use the given string for its input. */
ParserBuilder& withStringInput(const std::string& input);
};
case AUFNIRA:
case QF_AUFBV:
case QF_AUFLIA:
+ case QF_AX:
+ case QF_BV:
Unhandled(name);
}
}
expr/attribute_black \
expr/declaration_scope_black \
parser/parser_black \
+ parser/parser_builder_black \
prop/cnf_stream_black \
context/context_black \
context/context_white \
/********************* */
-/** parser_white.h
+/** parser_black.h
** Original author: cconway
** Major contributors: none
** Minor contributors (to current version): dejan, mdeters
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** White box testing of CVC4::parser::SmtParser.
+ ** Black box testing of CVC4::parser::Parser, including CVC, SMT and
+ ** SMT v2 inputs.
**/
#include <cxxtest/TestSuite.h>
-//#include <string>
#include <sstream>
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
+#include "parser/parser_options.h"
#include "parser/smt2/smt2.h"
#include "expr/command.h"
#include "util/output.h"
using namespace CVC4::parser;
using namespace std;
-
-
class ParserBlack {
InputLanguage d_lang;
ExprManager *d_exprManager;
// Debug.on("parser-extra");
// cerr << "Testing good input: <<" << goodInput << ">>" << endl;
// istringstream stream(goodInputs[i]);
- ParserBuilder parserBuilder(d_lang,"test");
Parser *parser =
- parserBuilder.withStringInput(goodInput)
- .withExprManager(*d_exprManager)
+ ParserBuilder(*d_exprManager,"test")
+ .withStringInput(goodInput)
+ .withInputLanguage(d_lang)
.build();
TS_ASSERT( !parser->done() );
Command* cmd;
void tryBadInput(const string badInput, bool strictMode = false) {
// cerr << "Testing bad input: '" << badInput << "'\n";
// Debug.on("parser");
- ParserBuilder parserBuilder(d_lang,"test");
+
Parser *parser =
- parserBuilder.withStringInput(badInput)
- .withExprManager(*d_exprManager)
+ ParserBuilder(*d_exprManager,"test")
+ .withStringInput(badInput)
+ .withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
TS_ASSERT_THROWS
// cerr << "Testing good expr: '" << goodExpr << "'\n";
// Debug.on("parser");
// istringstream stream(context + goodBooleanExprs[i]);
- ParserBuilder parserBuilder(d_lang,"test");
+
Parser *parser =
- parserBuilder.withStringInput(goodExpr)
- .withExprManager(*d_exprManager)
+ ParserBuilder(*d_exprManager,"test")
+ .withStringInput(goodExpr)
+ .withInputLanguage(d_lang)
.build();
+
TS_ASSERT( !parser->done() );
setupContext(*parser);
TS_ASSERT( !parser->done() );
// Debug.on("parser");
// Debug.on("parser-extra");
// cout << "Testing bad expr: '" << badExpr << "'\n";
- ParserBuilder parserBuilder(d_lang,"test");
+
Parser *parser =
- parserBuilder.withStringInput(badExpr)
- .withExprManager(*d_exprManager)
+ ParserBuilder(*d_exprManager,"test")
+ .withStringInput(badExpr)
+ .withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
setupContext(*parser);
--- /dev/null
+/********************* */
+/** parser_builder_black.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::parser::ParserBuilder.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <ext/stdio_filebuf.h>
+#include <fstream>
+#include <iostream>
+#include <stdio.h>
+#include <string.h>
+#include <sys/stat.h>
+#include <unistd.h>
+
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/parser_options.h"
+
+typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+class ParserBuilderBlack : public CxxTest::TestSuite {
+
+ ExprManager *d_exprManager;
+
+ void checkEmptyInput(ParserBuilder& builder) {
+ Parser *parser = builder.build();
+ TS_ASSERT( parser != NULL );
+
+ Expr e = parser->nextExpression();
+ TS_ASSERT( e.isNull() );
+
+ delete parser;
+ }
+
+ void checkTrueInput(ParserBuilder& builder) {
+ Parser *parser = builder.build();
+ TS_ASSERT( parser != NULL );
+
+ Expr e = parser->nextExpression();
+ TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) );
+
+ e = parser->nextExpression();
+ TS_ASSERT( e.isNull() );
+ delete parser;
+ }
+
+ char* mkTemp() {
+ char *filename = strdup("/tmp/testinput.XXXXXX");
+ int fd = mkstemp(filename);
+ TS_ASSERT( fd != -1 );
+ close(fd);
+ return filename;
+ }
+
+public:
+
+ void setUp() {
+ d_exprManager = new ExprManager;
+ }
+
+ void tearDown() {
+ delete d_exprManager;
+ }
+
+ void testEmptyFileInput() {
+ char *filename = mkTemp();
+
+ /* FILE *fp = tmpfile(); */
+ /* filebuf_gnu fs( fd, ios_base::out ); */
+
+ /* ptr = tmpnam(filename); */
+ /* std::fstream fs( ptr, fstream::out ); */
+ /* fs.close(); */
+
+ checkEmptyInput(
+ ParserBuilder(*d_exprManager,filename)
+ .withInputLanguage(LANG_CVC4)
+ );
+
+ remove(filename);
+ // mkfifo(ptr, S_IWUSR | s_IRUSR);
+ }
+
+ void testSimpleFileInput() {
+ char *filename = mkTemp();
+
+ std::fstream fs( filename, fstream::out );
+ fs << "TRUE" << std::endl;
+ fs.close();
+
+ checkTrueInput(
+ ParserBuilder(*d_exprManager,filename)
+ .withInputLanguage(LANG_CVC4)
+ );
+
+ remove(filename);
+ }
+
+ void testEmptyStringInput() {
+ checkEmptyInput(
+ ParserBuilder(*d_exprManager,"foo")
+ .withInputLanguage(LANG_CVC4)
+ .withStringInput("")
+ );
+ }
+
+ void testTrueStringInput() {
+ checkTrueInput(
+ ParserBuilder(*d_exprManager,"foo")
+ .withInputLanguage(LANG_CVC4)
+ .withStringInput("TRUE")
+ );
+ }
+
+ void testEmptyStreamInput() {
+ stringstream ss( "", ios_base::in );
+ checkEmptyInput(
+ ParserBuilder(*d_exprManager,"foo")
+ .withInputLanguage(LANG_CVC4)
+ .withStreamInput(ss)
+ );
+ }
+
+ void testTrueStreamInput() {
+ stringstream ss( "TRUE", ios_base::in );
+ checkTrueInput(
+ ParserBuilder(*d_exprManager,"foo")
+ .withInputLanguage(LANG_CVC4)
+ .withStreamInput(ss)
+ );
+ }
+
+
+
+}; // class ParserBuilderBlack
projects / cvc5.git / commitdiff