}
// Create the parser
- Input* parser;
- istream* input = NULL;
+ Input* input;
+ /* TODO: Hack ANTLR3 to support input from streams */
// if(inputFromStdin) {
// parser = Parser::getNewParser(&exprMgr, options.lang, cin, "<stdin>");
// } else {
- parser = Input::newFileParser(&exprMgr, options.lang, argv[firstArgIndex],
+ input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex],
options.memoryMap);
// }
if(!options.semanticChecks) {
- parser->disableChecks();
+ input->disableChecks();
}
// Parse and execute commands until we are done
Command* cmd;
- while((cmd = parser->parseNextCommand())) {
+ while((cmd = input->parseNextCommand())) {
if( !options.parseOnly ) {
doCommand(smt, cmd);
}
}
// Remove the parser
- delete parser;
+ delete input;
delete input;
switch(lastResult.asSatisfiabilityResult().isSAT()) {
memory_mapped_input_buffer.cpp \
parser_options.h \
parser_exception.h \
+ parser_state.h \
+ parser_state.cpp \
symbol_table.h
#include <limits.h>
#include <antlr3.h>
+#include "antlr_input.h"
+#include "bounded_token_buffer.h"
+#include "bounded_token_factory.h"
+#include "memory_mapped_input_buffer.h"
+#include "parser_exception.h"
+#include "parser_state.h"
+
#include "util/output.h"
#include "util/Assert.h"
#include "expr/command.h"
#include "expr/type.h"
-#include "parser/antlr_input.h"
-#include "parser/bounded_token_buffer.h"
-#include "parser/bounded_token_factory.h"
-#include "parser/memory_mapped_input_buffer.h"
-#include "parser/parser_exception.h"
using namespace std;
using namespace CVC4;
void AntlrInput::parseError(const std::string& message)
throw (ParserException) {
- Debug("parser") << "Throwing exception: " << getFilename() << ":"
+ Debug("parser") << "Throwing exception: "
+ << getParserState()->getFilename() << ":"
<< d_lexer->getLine(d_lexer) << "."
<< d_lexer->getCharPositionInLine(d_lexer) << ": "
<< message << endl;
- throw ParserException(message, getFilename(), d_lexer->getLine(d_lexer),
- d_lexer->getCharPositionInLine(d_lexer));
+ throw ParserException(message, getParserState()->getFilename(),
+ d_lexer->getLine(d_lexer),
+ d_lexer->getCharPositionInLine(d_lexer));
}
void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
// Now get ready to throw an exception
pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super);
AlwaysAssert(parser!=NULL);
- AntlrInput *input = (AntlrInput*)(parser->super);
- AlwaysAssert(input!=NULL);
+ ParserState *parserState = (ParserState*)(parser->super);
+ AlwaysAssert(parserState!=NULL);
// Call the error display routine
- input->parseError(ss.str());
+ parserState->parseError(ss.str());
}
void AntlrInput::setLexer(pANTLR3_LEXER pLexer) {
// We could also use @parser::context to add a field to the generated parser, but then
// it would have to be declared separately in every input's grammar and we'd have to
// pass it in as an address anyway.
- d_parser->super = this;
+ d_parser->super = getParserState();
d_parser->rec->reportError = &reportError;
}
@parser::includes {
#include "expr/command.h"
-#include "parser/input.h"
+#include "parser/parser_state.h"
namespace CVC4 {
class Expr;
#include "expr/kind.h"
#include "expr/type.h"
#include "parser/antlr_input.h"
+#include "parser/parser_state.h"
#include "util/output.h"
#include <vector>
/* These need to be macros so they can refer to the PARSER macro, which will be defined
* by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef ANTLR_INPUT
-#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef PARSER_STATE
+#define PARSER_STATE ((ParserState*)PARSER->super)
#undef EXPR_MANAGER
-#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#define EXPR_MANAGER PARSER_STATE->getExprManager()
#undef MK_EXPR
#define MK_EXPR EXPR_MANAGER->mkExpr
#undef MK_CONST
}
: /* A sort declaration (e.g., "T : TYPE") */
TYPE_TOK
- { ANTLR_INPUT->newSorts(idList);
+ { PARSER_STATE->newSorts(idList);
t = EXPR_MANAGER->kindType(); }
| /* A variable declaration */
- type[t] { ANTLR_INPUT->mkVars(idList,t); }
+ type[t] { PARSER_STATE->mkVars(idList,t); }
;
/**
CVC4::parser::SymbolType type]
: IDENTIFIER
{ id = AntlrInput::tokenText($IDENTIFIER);
- ANTLR_INPUT->checkDeclaration(id, check, type); }
+ PARSER_STATE->checkDeclaration(id, check, type); }
;
/**
Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: identifier[id,CHECK_DECLARED,SYM_SORT]
- { t = ANTLR_INPUT->getSort(id); }
+ { t = PARSER_STATE->getSort(id); }
;
/**
| /* variable */
identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { f = ANTLR_INPUT->getVariable(name); }
+ { f = PARSER_STATE->getVariable(name); }
;
/**
std::string name;
}
: identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { ANTLR_INPUT->checkFunction(name);
- f = ANTLR_INPUT->getVariable(name); }
+ { PARSER_STATE->checkFunction(name);
+ f = PARSER_STATE->getVariable(name); }
;
** Parser implementation.
**/
-#include <iostream>
-#include <fstream>
#include <stdint.h>
#include "input.h"
+#include "parser_exception.h"
+#include "parser_options.h"
+#include "parser_state.h"
#include "expr/command.h"
#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
-#include "util/output.h"
-#include "util/Assert.h"
-#include "parser/parser_exception.h"
#include "parser/cvc/cvc_input.h"
#include "parser/smt/smt_input.h"
+#include "util/output.h"
+#include "util/Assert.h"
using namespace std;
-using namespace CVC4::kind;
namespace CVC4 {
namespace parser {
-void Input::setDone(bool done) {
- d_done = done;
+bool Input::done() const {
+ return d_parserState->done();
}
-bool Input::done() const {
- return d_done;
+void Input::disableChecks() {
+ d_parserState->disableChecks();
+}
+
+void Input::enableChecks() {
+ d_parserState->enableChecks();
}
Command* Input::parseNextCommand() throw (ParserException) {
try {
cmd = doParseCommand();
if(cmd == NULL) {
- setDone();
+ d_parserState->setDone();
}
} catch(ParserException& e) {
- setDone();
+ d_parserState->setDone();
throw ParserException(e.toString());
}
}
try {
result = doParseExpr();
if(result.isNull())
- setDone();
+ d_parserState->setDone();
} catch(ParserException& e) {
- setDone();
+ d_parserState->setDone();
throw ParserException(e.toString());
}
}
return result;
}
-Input::~Input() {
+Input::Input(ExprManager* exprManager, const std::string& filename) {
+ d_parserState = new ParserState(exprManager,filename,this);
}
-Input::Input(ExprManager* exprManager, const std::string& filename) :
- d_exprManager(exprManager),
- d_filename(filename),
- d_done(false),
- d_checksEnabled(true) {
+Input::~Input() {
+ delete d_parserState;
}
-Input* Input::newFileParser(ExprManager* em, InputLanguage lang,
- const std::string& filename, bool useMmap) {
+Input* Input::newFileInput(ExprManager* em, InputLanguage lang,
+ const std::string& filename, bool useMmap) {
- Input* parser = 0;
+ Input* input = 0;
switch(lang) {
case LANG_CVC4:
- parser = new CvcInput(em,filename,useMmap);
+ input = new CvcInput(em,filename,useMmap);
break;
case LANG_SMTLIB:
- parser = new SmtInput(em,filename,useMmap);
+ input = new SmtInput(em,filename,useMmap);
break;
default:
Unhandled(lang);
}
- return parser;
-}
-
-/*
-Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
- istream& input, string filename) {
- antlr::CharBuffer* inputBuffer = new CharBuffer(input);
- return getNewParser(em, lang, inputBuffer, filename);
-}
-*/
-
-/*
-Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
- std::istream& input, const std::string& name) {
- Parser* parser = 0;
-
- switch(lang) {
- case LANG_CVC4: {
- antlrLexer = new AntlrCvcLexer(*inputBuffer);
- antlrParser = new AntlrCvcParser(*antlrLexer);
- break;
- }
- case LANG_SMTLIB:
- parser = new Smt(em,input,name);
- break;
-
- default:
- Unhandled("Unknown Input language!");
- }
- return parser;
+ return input;
}
-*/
-Input* Input::newStringParser(ExprManager* em, InputLanguage lang,
- const std::string& input, const std::string& name) {
- Input* parser = 0;
+Input* Input::newStringInput(ExprManager* em, InputLanguage lang,
+ const std::string& str, const std::string& name) {
+ Input* input = 0;
switch(lang) {
case LANG_CVC4: {
- parser = new CvcInput(em,input,name);
+ input = new CvcInput(em,str,name);
break;
}
case LANG_SMTLIB:
- parser = new SmtInput(em,input,name);
+ input = new SmtInput(em,str,name);
break;
default:
Unhandled(lang);
}
- return parser;
+ return input;
}
-Expr Input::getSymbol(const std::string& name, SymbolType type) {
- Assert( isDeclared(name, type) );
-
-
- switch( type ) {
-
- case SYM_VARIABLE: // Functions share var namespace
- return d_varSymbolTable.getObject(name);
-
- default:
- Unhandled(type);
- }
-}
-
-
-Expr Input::getVariable(const std::string& name) {
- return getSymbol(name, SYM_VARIABLE);
-}
-
-Type*
-Input::getType(const std::string& var_name,
- SymbolType type) {
- Assert( isDeclared(var_name, type) );
- Type* t = getSymbol(var_name,type).getType();
- return t;
-}
-
-Type* Input::getSort(const std::string& name) {
- Assert( isDeclared(name, SYM_SORT) );
- Type* t = d_sortTable.getObject(name);
- return t;
-}
-
-/* Returns true if name is bound to a boolean variable. */
-bool Input::isBoolean(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
-}
-
-/* Returns true if name is bound to a function. */
-bool Input::isFunction(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
-}
-
-/* Returns true if name is bound to a function returning boolean. */
-bool Input::isPredicate(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
-}
-
-Expr
-Input::mkVar(const std::string& name, Type* type) {
- Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
- Expr expr = d_exprManager->mkVar(type, name);
- defineVar(name,expr);
- return expr;
-}
-
-const std::vector<Expr>
-Input::mkVars(const std::vector<std::string> names,
- Type* type) {
- std::vector<Expr> vars;
- for(unsigned i = 0; i < names.size(); ++i) {
- vars.push_back(mkVar(names[i], type));
- }
- return vars;
-}
-
-void
-Input::defineVar(const std::string& name, const Expr& val) {
- Assert(!isDeclared(name));
- d_varSymbolTable.bindName(name,val);
- Assert(isDeclared(name));
-}
-
-void
-Input::undefineVar(const std::string& name) {
- Assert(isDeclared(name));
- d_varSymbolTable.unbindName(name);
- Assert(!isDeclared(name));
-}
-
-void
-Input::setLogic(const std::string& name) {
- if( name == "QF_UF" ) {
- newSort("U");
- } else {
- Unhandled(name);
- }
-}
-
-Type*
-Input::newSort(const std::string& name) {
- Debug("parser") << "newSort(" << name << ")" << std::endl;
- Assert( !isDeclared(name, SYM_SORT) ) ;
- Type* type = d_exprManager->mkSort(name);
- d_sortTable.bindName(name, type);
- Assert( isDeclared(name, SYM_SORT) ) ;
- return type;
-}
-
-const std::vector<Type*>
-Input::newSorts(const std::vector<std::string>& names) {
- std::vector<Type*> types;
- for(unsigned i = 0; i < names.size(); ++i) {
- types.push_back(newSort(names[i]));
- }
- return types;
-}
-
-bool Input::isDeclared(const std::string& name, SymbolType type) {
- switch(type) {
- case SYM_VARIABLE:
- return d_varSymbolTable.isBound(name);
- case SYM_SORT:
- return d_sortTable.isBound(name);
- default:
- Unhandled(type);
- }
-}
-
-void Input::checkDeclaration(const std::string& varName,
- DeclarationCheck check,
- SymbolType type)
- throw (ParserException) {
- if(!d_checksEnabled) {
- return;
- }
-
- switch(check) {
- case CHECK_DECLARED:
- if( !isDeclared(varName, type) ) {
- parseError("Symbol " + varName + " not declared");
- }
- break;
-
- case CHECK_UNDECLARED:
- if( isDeclared(varName, type) ) {
- parseError("Symbol " + varName + " previously declared");
- }
- break;
-
- case CHECK_NONE:
- break;
-
- default:
- Unhandled(check);
- }
-}
-
-void Input::checkFunction(const std::string& name)
- throw (ParserException) {
- if( d_checksEnabled && !isFunction(name) ) {
- parseError("Expecting function symbol, found '" + name + "'");
- }
-}
-
-void Input::checkArity(Kind kind, unsigned int numArgs)
- throw (ParserException) {
- if(!d_checksEnabled) {
- return;
- }
-
- unsigned int min = d_exprManager->minArity(kind);
- unsigned int max = d_exprManager->maxArity(kind);
-
- if( numArgs < min || numArgs > max ) {
- stringstream ss;
- ss << "Expecting ";
- if( numArgs < min ) {
- ss << "at least " << min << " ";
- } else {
- ss << "at most " << max << " ";
- }
- ss << "arguments for operator '" << kind << "', ";
- ss << "found " << numArgs;
- parseError(ss.str());
- }
-}
-
-void Input::enableChecks() {
- d_checksEnabled = true;
-}
-
-void Input::disableChecks() {
- d_checksEnabled = false;
-}
-
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#include "cvc4parser_public.h"
-#ifndef __CVC4__PARSER__PARSER_H
-#define __CVC4__PARSER__PARSER_H
+#ifndef __CVC4__PARSER__INPUT_H
+#define __CVC4__PARSER__INPUT_H
#include <string>
-#include <iostream>
#include "expr/expr.h"
-#include "expr/kind.h"
#include "parser/parser_exception.h"
#include "parser/parser_options.h"
-#include "parser/symbol_table.h"
-#include "util/Assert.h"
namespace CVC4 {
// Forward declarations
-class BooleanType;
class ExprManager;
class Command;
-class FunctionType;
-class KindType;
class Type;
namespace parser {
-/** Types of check for the symols */
-enum DeclarationCheck {
- /** Enforce that the symbol has been declared */
- CHECK_DECLARED,
- /** Enforce that the symbol has not been declared */
- CHECK_UNDECLARED,
- /** Don't check anything */
- CHECK_NONE
-};
-
-/** Returns a string representation of the given object (for
- debugging). */
-inline std::string toString(DeclarationCheck check) {
- switch(check) {
- case CHECK_NONE: return "CHECK_NONE";
- case CHECK_DECLARED: return "CHECK_DECLARED";
- case CHECK_UNDECLARED: return "CHECK_UNDECLARED";
- default: Unreachable();
- }
-}
-
-/**
- * Types of symbols. Used to define namespaces.
- */
-enum SymbolType {
- /** Variables */
- SYM_VARIABLE,
- /** Sorts */
- SYM_SORT
-};
-
-/** Returns a string representation of the given object (for
- debugging). */
-inline std::string toString(SymbolType type) {
- switch(type) {
- case SYM_VARIABLE: return "SYM_VARIABLE";
- case SYM_SORT: return "SYM_SORT";
- default: Unreachable();
- }
-}
+class ParserState;
/**
- * The parser. The parser should be obtained by calling the static methods
- * getNewParser, and should be deleted when done.
+ * An input to be parsed. This class serves two purposes: to the client, it provides
+ * the methods <code>parseNextCommand</code> and <code>parseNextExpression</code> to
+ * extract a stream of <code>Command</code>'s and <code>Expr</code>'s from the input;
+ * to the parser, it provides a repository for state data, like the variable symbol
+ * table, and a variety of convenience functions for updating and checking the state.
*
- * This class includes convenience methods for interacting with the ExprManager
- * from within a grammar.
+ * An Input should be created using the static factory methods,
+ * e.g., <code>newFileParser</code> and <code>newStringInput</code>, and
+ * should be deleted when done.
*/
class CVC4_PUBLIC Input {
+ friend class ParserState;
/** Whether to de-allocate the input */
-// bool d_deleteInput;
-
- /** The expression manager */
- ExprManager* d_exprManager;
-
- /** The symbol table lookup */
- SymbolTable<Expr> d_varSymbolTable;
-
- /** The sort table */
- SymbolTable<Type*> d_sortTable;
-
- /** The name of the input file. */
- std::string d_filename;
-
- /** Are we done */
- bool d_done;
+ // bool d_deleteInput;
- /** Are semantic checks enabled during parsing? */
- bool d_checksEnabled;
+ ParserState *d_parserState;
public:
/**
* Destructor.
*/
- ~Input();
+ virtual ~Input();
- /** Create a parser for the given file.
+ /** Create an input for the given file.
*
* @param exprManager the ExprManager for creating expressions from the input
* @param lang the input language
* @param filename the input filename
*/
- static Input* newFileParser(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
+ static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
- /** Create a parser for the given input stream.
+ /** Create an input for the given stream.
*
* @param exprManager the ExprManager for creating expressions from the input
* @param lang the input language
*/
//static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name);
- /** Create a parser for the given input string
+ /** Create an input for the given string
*
* @param exprManager the ExprManager for creating expressions from the input
* @param lang the input language
* @param input the input string
* @param name the name of the stream, for use in error messages
*/
- static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
+ static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
- /** Get the <code>ExprManager</code> associated with this input. */
- inline ExprManager* getExprManager() const {
- return d_exprManager;
- }
+ /**
+ * Check if we are done -- either the end of input has been reached, or some
+ * error has been encountered.
+ * @return true if parser is done
+ */
+ bool done() const;
+
+ /** Enable semantic checks during parsing. */
+ void enableChecks();
+
+ /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+ void disableChecks();
/**
* Parse the next command of the input. If EOF is encountered a EmptyCommand
*/
Expr parseNextExpression() throw(ParserException);
- /**
- * Check if we are done -- either the end of input has been reached, or some
- * error has been encountered.
- * @return true if parser is done
- */
- bool done() const;
-
- /** Enable semantic checks during parsing. */
- void enableChecks();
-
- /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
- void disableChecks();
-
- /** Get the name of the input file. */
- inline const std::string getFilename() {
- return d_filename;
- }
-
- /**
- * Sets the logic for the current benchmark. Declares any logic symbols.
- *
- * @param name the name of the logic (e.g., QF_UF, AUFLIA)
- */
- void setLogic(const std::string& name);
-
- /**
- * Returns a variable, given a name and a type.
- * @param var_name the name of the variable
- * @return the variable expression
- */
- Expr getVariable(const std::string& var_name);
-
- /**
- * Returns a sort, given a name
- */
- Type* getSort(const std::string& sort_name);
-
- /**
- * Checks if a symbol has been declared.
- * @param name the symbol name
- * @param type the symbol type
- * @return true iff the symbol has been declared with the given type
- */
- bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
-
- /**
- * Checks if the declaration policy we want to enforce holds
- * for the given symbol.
- * @param name the symbol to check
- * @param check the kind of check to perform
- * @param type the type of the symbol
- * @throws ParserException if checks are enabled and the check fails
- */
- void checkDeclaration(const std::string& name,
- DeclarationCheck check,
- SymbolType type = SYM_VARIABLE)
- throw (ParserException);
-
- /**
- * Checks whether the given name is bound to a function.
- * @param name the name to check
- * @throws ParserException if checks are enabled and name is not bound to a function
- */
- void checkFunction(const std::string& name) throw (ParserException);
-
- /**
- * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
- * @param kind the built-in operator to check
- * @param numArgs the number of actual arguments
- * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
- * applied to <code>numArgs</code> arguments.
- */
- void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
-
- /**
- * Returns the type for the variable with the given name.
- * @param name the symbol to lookup
- * @param type the (namespace) type of the symbol
- */
- Type* getType(const std::string& var_name,
- SymbolType type = SYM_VARIABLE);
-
- /** Create a new CVC4 variable expression of the given type. */
- Expr mkVar(const std::string& name, Type* type);
-
- /** Create a set of new CVC4 variable expressions of the given
- type. */
- const std::vector<Expr>
- mkVars(const std::vector<std::string> names,
- Type* type);
-
-
- /** Create a new variable definition (e.g., from a let binding). */
- void defineVar(const std::string& name, const Expr& val);
- /** Remove a variable definition (e.g., from a let binding). */
- void undefineVar(const std::string& name);
-
- /**
- * Creates a new sort with the given name.
- */
- Type* newSort(const std::string& name);
-
- /**
- * Creates a new sorts with the given names.
- */
- const std::vector<Type*>
- newSorts(const std::vector<std::string>& names);
-
- /** Is the symbol bound to a boolean variable? */
- bool isBoolean(const std::string& name);
-
- /** Is the symbol bound to a function? */
- bool isFunction(const std::string& name);
-
- /** Is the symbol bound to a predicate? */
- bool isPredicate(const std::string& name);
-
- /** Throws a <code>ParserException</code> with the given error message.
- * Implementations should fill in the <code>ParserException</code> with
- * line number information, etc. */
- virtual void parseError(const std::string& msg) throw (ParserException) = 0;
protected:
*/
virtual Expr doParseExpr() throw(ParserException) = 0;
-private:
+ inline ParserState* getParserState() const {
+ return d_parserState;
+ }
- /** Sets the done flag */
- void setDone(bool done = true);
+private:
- /** Lookup a symbol in the given namespace. */
- Expr getSymbol(const std::string& var_name, SymbolType type);
+ /** Throws a <code>ParserException</code> with the given error message.
+ * Implementations should fill in the <code>ParserException</code> with
+ * line number information, etc. */
+ virtual void parseError(const std::string& msg) throw (ParserException) = 0;
-}; // end of class Parser
+}; // end of class Input
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PARSER__PARSER_H */
+#endif /* __CVC4__PARSER__INPUT_H */
--- /dev/null
+/********************* */
+/** parser_state.cpp
+ ** Original author: cconway
+ ** Major contributors: dejan, mdeters
+ ** Minor contributors (to current version): none
+ ** 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.
+ **
+ ** Parser state implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+#include <stdint.h>
+
+#include "input.h"
+#include "expr/command.h"
+#include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "util/output.h"
+#include "util/Assert.h"
+#include "parser/parser_exception.h"
+#include "parser/symbol_table.h"
+#include "parser/cvc/cvc_input.h"
+#include "parser/smt/smt_input.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace parser {
+
+ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) :
+ d_exprManager(exprManager),
+ d_input(input),
+ d_filename(filename),
+ d_done(false),
+ d_checksEnabled(true) {
+}
+
+Expr ParserState::getSymbol(const std::string& name, SymbolType type) {
+ Assert( isDeclared(name, type) );
+
+
+ switch( type ) {
+
+ case SYM_VARIABLE: // Functions share var namespace
+ return d_varTable.getObject(name);
+
+ default:
+ Unhandled(type);
+ }
+}
+
+
+Expr ParserState::getVariable(const std::string& name) {
+ return getSymbol(name, SYM_VARIABLE);
+}
+
+Type*
+ParserState::getType(const std::string& var_name,
+ SymbolType type) {
+ Assert( isDeclared(var_name, type) );
+ Type* t = getSymbol(var_name,type).getType();
+ return t;
+}
+
+Type* ParserState::getSort(const std::string& name) {
+ Assert( isDeclared(name, SYM_SORT) );
+ Type* t = d_sortTable.getObject(name);
+ return t;
+}
+
+/* Returns true if name is bound to a boolean variable. */
+bool ParserState::isBoolean(const std::string& name) {
+ return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
+}
+
+/* Returns true if name is bound to a function. */
+bool ParserState::isFunction(const std::string& name) {
+ return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
+}
+
+/* Returns true if name is bound to a function returning boolean. */
+bool ParserState::isPredicate(const std::string& name) {
+ return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
+}
+
+Expr
+ParserState::mkVar(const std::string& name, Type* type) {
+ Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(type, name);
+ defineVar(name,expr);
+ return expr;
+}
+
+const std::vector<Expr>
+ParserState::mkVars(const std::vector<std::string> names,
+ Type* type) {
+ std::vector<Expr> vars;
+ for(unsigned i = 0; i < names.size(); ++i) {
+ vars.push_back(mkVar(names[i], type));
+ }
+ return vars;
+}
+
+void
+ParserState::defineVar(const std::string& name, const Expr& val) {
+ Assert(!isDeclared(name));
+ d_varTable.bindName(name,val);
+ Assert(isDeclared(name));
+}
+
+void
+ParserState::undefineVar(const std::string& name) {
+ Assert(isDeclared(name));
+ d_varTable.unbindName(name);
+ Assert(!isDeclared(name));
+}
+
+void
+ParserState::setLogic(const std::string& name) {
+ if( name == "QF_UF" ) {
+ newSort("U");
+ } else {
+ Unhandled(name);
+ }
+}
+
+Type*
+ParserState::newSort(const std::string& name) {
+ Debug("parser") << "newSort(" << name << ")" << std::endl;
+ Assert( !isDeclared(name, SYM_SORT) ) ;
+ Type* type = d_exprManager->mkSort(name);
+ d_sortTable.bindName(name, type);
+ Assert( isDeclared(name, SYM_SORT) ) ;
+ return type;
+}
+
+const std::vector<Type*>
+ParserState::newSorts(const std::vector<std::string>& names) {
+ std::vector<Type*> types;
+ for(unsigned i = 0; i < names.size(); ++i) {
+ types.push_back(newSort(names[i]));
+ }
+ return types;
+}
+
+bool ParserState::isDeclared(const std::string& name, SymbolType type) {
+ switch(type) {
+ case SYM_VARIABLE:
+ return d_varTable.isBound(name);
+ case SYM_SORT:
+ return d_sortTable.isBound(name);
+ default:
+ Unhandled(type);
+ }
+}
+
+void ParserState::checkDeclaration(const std::string& varName,
+ DeclarationCheck check,
+ SymbolType type)
+ throw (ParserException) {
+ if(!d_checksEnabled) {
+ return;
+ }
+
+ switch(check) {
+ case CHECK_DECLARED:
+ if( !isDeclared(varName, type) ) {
+ parseError("Symbol " + varName + " not declared");
+ }
+ break;
+
+ case CHECK_UNDECLARED:
+ if( isDeclared(varName, type) ) {
+ parseError("Symbol " + varName + " previously declared");
+ }
+ break;
+
+ case CHECK_NONE:
+ break;
+
+ default:
+ Unhandled(check);
+ }
+}
+
+void ParserState::checkFunction(const std::string& name)
+ throw (ParserException) {
+ if( d_checksEnabled && !isFunction(name) ) {
+ parseError("Expecting function symbol, found '" + name + "'");
+ }
+}
+
+void ParserState::checkArity(Kind kind, unsigned int numArgs)
+ throw (ParserException) {
+ if(!d_checksEnabled) {
+ return;
+ }
+
+ unsigned int min = d_exprManager->minArity(kind);
+ unsigned int max = d_exprManager->maxArity(kind);
+
+ if( numArgs < min || numArgs > max ) {
+ stringstream ss;
+ ss << "Expecting ";
+ if( numArgs < min ) {
+ ss << "at least " << min << " ";
+ } else {
+ ss << "at most " << max << " ";
+ }
+ ss << "arguments for operator '" << kind << "', ";
+ ss << "found " << numArgs;
+ parseError(ss.str());
+ }
+}
+
+void ParserState::enableChecks() {
+ d_checksEnabled = true;
+}
+
+void ParserState::disableChecks() {
+ d_checksEnabled = false;
+}
+
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/** parser_state.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): 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.
+ **
+ ** A collection of state for use by parser implementations.
+ **/
+
+#ifndef __CVC4__PARSER__PARSER_STATE_H_
+#define __CVC4__PARSER__PARSER_STATE_H_
+
+#include <string>
+
+#include "expr/expr.h"
+#include "expr/kind.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
+#include "parser/parser_options.h"
+#include "parser/symbol_table.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+// Forward declarations
+class BooleanType;
+class ExprManager;
+class Command;
+class FunctionType;
+class KindType;
+class Type;
+
+namespace parser {
+
+/** Types of check for the symols */
+enum DeclarationCheck {
+ /** Enforce that the symbol has been declared */
+ CHECK_DECLARED,
+ /** Enforce that the symbol has not been declared */
+ CHECK_UNDECLARED,
+ /** Don't check anything */
+ CHECK_NONE
+};
+
+/** Returns a string representation of the given object (for
+ debugging). */
+inline std::string toString(DeclarationCheck check) {
+ switch(check) {
+ case CHECK_NONE:
+ return "CHECK_NONE";
+ case CHECK_DECLARED:
+ return "CHECK_DECLARED";
+ case CHECK_UNDECLARED:
+ return "CHECK_UNDECLARED";
+ default:
+ Unreachable();
+ }
+}
+
+/**
+ * Types of symbols. Used to define namespaces.
+ */
+enum SymbolType {
+ /** Variables */
+ SYM_VARIABLE,
+ /** Sorts */
+ SYM_SORT
+};
+
+/** Returns a string representation of the given object (for
+ debugging). */
+inline std::string toString(SymbolType type) {
+ switch(type) {
+ case SYM_VARIABLE:
+ return "SYM_VARIABLE";
+ case SYM_SORT:
+ return "SYM_SORT";
+ default:
+ Unreachable();
+ }
+}
+
+class ParserState {
+
+ /** The expression manager */
+ ExprManager *d_exprManager;
+
+ /** The input that we're parsing. */
+ Input *d_input;
+
+ /** The symbol table lookup */
+ SymbolTable<Expr> d_varTable;
+
+ /** The sort table */
+ SymbolTable<Type*> d_sortTable;
+
+ /** The name of the input file. */
+ std::string d_filename;
+
+ /** Are we done */
+ bool d_done;
+
+ /** Are semantic checks enabled during parsing? */
+ bool d_checksEnabled;
+
+
+ /** Lookup a symbol in the given namespace. */
+ Expr getSymbol(const std::string& var_name, SymbolType type);
+
+public:
+ ParserState(ExprManager* exprManager, const std::string& filename, Input* input);
+
+ /** Get the associated <code>ExprManager</code>. */
+ inline ExprManager* getExprManager() const {
+ return d_exprManager;
+ }
+
+ /** Get the associated input. */
+ inline Input* getInput() const {
+ return d_input;
+ }
+
+ /**
+ * Check if we are done -- either the end of input has been reached, or some
+ * error has been encountered.
+ * @return true if parser is done
+ */
+ inline bool done() const {
+ return d_done;
+ }
+
+ /** Sets the done flag */
+ inline void setDone(bool done = true) {
+ d_done = done;
+ }
+
+ /** Enable semantic checks during parsing. */
+ void enableChecks();
+
+ /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+ void disableChecks();
+
+ /** Get the name of the input file. */
+ inline const std::string getFilename() {
+ return d_filename;
+ }
+
+ /**
+ * Sets the logic for the current benchmark. Declares any logic symbols.
+ *
+ * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+ */
+ void setLogic(const std::string& name);
+
+ /**
+ * Returns a variable, given a name and a type.
+ * @param var_name the name of the variable
+ * @return the variable expression
+ */
+ Expr getVariable(const std::string& var_name);
+
+ /**
+ * Returns a sort, given a name
+ */
+ Type* getSort(const std::string& sort_name);
+
+ /**
+ * Checks if a symbol has been declared.
+ * @param name the symbol name
+ * @param type the symbol type
+ * @return true iff the symbol has been declared with the given type
+ */
+ bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
+
+ /**
+ * Checks if the declaration policy we want to enforce holds
+ * for the given symbol.
+ * @param name the symbol to check
+ * @param check the kind of check to perform
+ * @param type the type of the symbol
+ * @throws ParserException if checks are enabled and the check fails
+ */
+ void checkDeclaration(const std::string& name, DeclarationCheck check,
+ SymbolType type = SYM_VARIABLE) throw (ParserException);
+
+ /**
+ * Checks whether the given name is bound to a function.
+ * @param name the name to check
+ * @throws ParserException if checks are enabled and name is not bound to a function
+ */
+ void checkFunction(const std::string& name) throw (ParserException);
+
+ /**
+ * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
+ * @param kind the built-in operator to check
+ * @param numArgs the number of actual arguments
+ * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
+ * applied to <code>numArgs</code> arguments.
+ */
+ void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
+
+ /**
+ * Returns the type for the variable with the given name.
+ * @param name the symbol to lookup
+ * @param type the (namespace) type of the symbol
+ */
+ Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
+
+ /** Create a new CVC4 variable expression of the given type. */
+ Expr mkVar(const std::string& name, Type* type);
+
+ /** Create a set of new CVC4 variable expressions of the given
+ type. */
+ const std::vector<Expr>
+ mkVars(const std::vector<std::string> names, Type* type);
+
+ /** Create a new variable definition (e.g., from a let binding). */
+ void defineVar(const std::string& name, const Expr& val);
+ /** Remove a variable definition (e.g., from a let binding). */
+ void undefineVar(const std::string& name);
+
+ /**
+ * Creates a new sort with the given name.
+ */
+ Type* newSort(const std::string& name);
+
+ /**
+ * Creates a new sorts with the given names.
+ */
+ const std::vector<Type*>
+ newSorts(const std::vector<std::string>& names);
+
+ /** Is the symbol bound to a boolean variable? */
+ bool isBoolean(const std::string& name);
+
+ /** Is the symbol bound to a function? */
+ bool isFunction(const std::string& name);
+
+ /** Is the symbol bound to a predicate? */
+ bool isPredicate(const std::string& name);
+
+ inline void parseError(const std::string& msg) throw (ParserException) {
+ d_input->parseError(msg);
+ }
+
+}; // class ParserState
+
+} // namespace parser
+
+} // namespace CVC4
+
+#endif /* __CVC4__PARSER__PARSER_STATE_H_ */
@parser::includes {
#include "expr/command.h"
-#include "parser/input.h"
+#include "parser/parser_state.h"
namespace CVC4 {
class Expr;
#include "expr/kind.h"
#include "expr/type.h"
#include "parser/antlr_input.h"
+#include "parser/parser_state.h"
#include "util/output.h"
#include <vector>
/* These need to be macros so they can refer to the PARSER macro, which will be defined
* by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
-#undef ANTLR_INPUT
-#define ANTLR_INPUT ((Input*)PARSER->super)
+#undef PARSER_STATE
+#define PARSER_STATE ((ParserState*)PARSER->super)
#undef EXPR_MANAGER
-#define EXPR_MANAGER ANTLR_INPUT->getExprManager()
+#define EXPR_MANAGER PARSER_STATE->getExprManager()
#undef MK_EXPR
#define MK_EXPR EXPR_MANAGER->mkExpr
#undef MK_CONST
Expr expr;
}
: LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
- { ANTLR_INPUT->setLogic(name);
+ { PARSER_STATE->setLogic(name);
smt_command = new SetBenchmarkLogicCommand(name); }
| ASSUMPTION_TOK annotatedFormula[expr]
{ smt_command = new AssertCommand(expr); }
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
- { ANTLR_INPUT->checkArity(kind, args.size());
+ { PARSER_STATE->checkArity(kind, args.size());
if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
(LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
| FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
annotatedFormula[expr] RPAREN_TOK
- { ANTLR_INPUT->defineVar(name,expr); }
+ { PARSER_STATE->defineVar(name,expr); }
annotatedFormula[expr]
RPAREN_TOK
- { ANTLR_INPUT->undefineVar(name); }
+ { PARSER_STATE->undefineVar(name); }
| /* a variable */
( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
| let_identifier[name,CHECK_DECLARED]
| flet_identifier[name,CHECK_DECLARED] )
- { expr = ANTLR_INPUT->getVariable(name); }
+ { expr = PARSER_STATE->getVariable(name); }
/* constants */
| TRUE_TOK { expr = MK_CONST(true); }
std::string name;
}
: functionName[name,CHECK_DECLARED]
- { ANTLR_INPUT->checkFunction(name);
- fun = ANTLR_INPUT->getVariable(name); }
+ { PARSER_STATE->checkFunction(name);
+ fun = PARSER_STATE->getVariable(name); }
;
/**
} else {
t = EXPR_MANAGER->mkFunctionType(sorts);
}
- ANTLR_INPUT->mkVar(name, t); }
+ PARSER_STATE->mkVar(name, t); }
;
/**
} else {
t = EXPR_MANAGER->mkPredicateType(p_sorts);
}
- ANTLR_INPUT->mkVar(name, t); }
+ PARSER_STATE->mkVar(name, t); }
;
sortDeclaration
}
: sortName[name,CHECK_UNDECLARED]
{ Debug("parser") << "sort decl: '" << name << "'" << std::endl;
- ANTLR_INPUT->newSort(name); }
+ PARSER_STATE->newSort(name); }
;
/**
std::string name;
}
: sortName[name,CHECK_NONE]
- { $t = ANTLR_INPUT->getSort(name); }
+ { $t = PARSER_STATE->getSort(name); }
;
/**
Debug("parser") << "identifier: " << id
<< " check? " << toString(check)
<< " type? " << toString(type) << std::endl;
- ANTLR_INPUT->checkDeclaration(id, check, type); }
+ PARSER_STATE->checkDeclaration(id, check, type); }
;
/**
{ id = AntlrInput::tokenText($LET_IDENTIFIER);
Debug("parser") << "let_identifier: " << id
<< " check? " << toString(check) << std::endl;
- ANTLR_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
+ PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
;
/**
{ id = AntlrInput::tokenText($FLET_IDENTIFIER);
Debug("parser") << "flet_identifier: " << id
<< " check? " << toString(check) << std::endl;
- ANTLR_INPUT->checkDeclaration(id, check); }
+ PARSER_STATE->checkDeclaration(id, check); }
;
expr/node_manager_white \
expr/attribute_white \
expr/attribute_black \
- parser/parser_black \
+ parser/parser_white \
context/context_black \
context/context_mm_black \
context/cdo_black \
--- /dev/null
+/********************* */
+/** parser_white.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::SmtParser.
+ **/
+
+#include <cxxtest/TestSuite.h>
+//#include <string>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser_state.h"
+#include "expr/command.h"
+#include "util/output.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+
+/************************** CVC test inputs ********************************/
+
+const string goodCvc4Inputs[] = {
+ "", // empty string is OK
+ "ASSERT TRUE;",
+ "QUERY TRUE;",
+ "CHECKSAT FALSE;",
+ "a, b : BOOLEAN;",
+ "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
+ "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;",
+ "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;",
+ "%% nothing but a comment",
+ "% a comment\nASSERT TRUE; %a command\n% another comment",
+ };
+
+const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string);
+
+
+/* The following expressions are valid after setupContext. */
+const string goodCvc4Exprs[] = {
+ "a AND b",
+ "a AND b OR c",
+ "(a => b) AND a => b",
+ "(a <=> b) AND (NOT a)",
+ "(a XOR b) <=> (a OR b) AND (NOT (a AND b))"
+};
+
+const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string);
+
+const string badCvc4Inputs[] = {
+ ";", // no command
+ "ASSERT;", // no args
+ "QUERY",
+ "CHECKSAT",
+ "a, b : boolean;", // lowercase boolean isn't a type
+ "0x : INT;", // 0x isn't an identifier
+ "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl
+ "a : BOOLEAN; a: BOOLEAN;" // double decl
+ "a, b: BOOLEAN; QUERY a(b);" // non-function used as function
+ };
+
+const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string);
+
+/* The following expressions are invalid even after setupContext. */
+const string badCvc4Exprs[] = {
+ "a AND", // wrong arity
+ "AND(a,b)", // not infix
+ "(OR (AND a b) c)", // not infix
+ "a IMPLIES b", // should be =>
+ "a NOT b", // wrong arity, not infix
+ "a and b" // wrong case
+};
+
+const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string);
+
+/************************** SMT test inputs ********************************/
+
+const string goodSmtInputs[] = {
+ "", // empty string is OK
+ "(benchmark foo :assumption true)",
+ "(benchmark bar :formula true)",
+ "(benchmark qux :formula false)",
+ "(benchmark baz :extrapreds ( (a) (b) ) )",
+ "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))",
+ "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))",
+ "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))",
+ ";; nothing but a comment",
+ "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)"
+ };
+
+const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);
+
+/* The following expressions are valid after setupContext. */
+const string goodSmtExprs[] = {
+ "(and a b)",
+ "(or (and a b) c)",
+ "(implies (and (implies a b) a) b)",
+ "(and (iff a b) (not a))",
+ "(iff (xor a b) (and (or a b) (not (and a b))))",
+ "(ite a (f x) y)",
+ "(if_then_else a (f x) y)"
+};
+
+const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string);
+
+const string badSmtInputs[] = {
+ "(benchmark foo)", // empty benchmark is not OK
+ "(benchmark bar :assumption)", // no args
+ "(benchmark bar :formula)",
+ "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl
+ "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens
+ };
+
+const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string);
+
+/* The following expressions are invalid even after setupContext. */
+const string badSmtExprs[] = {
+ "(and)", // wrong arity
+ "(and a b", // no closing paren
+ "(a and b)", // infix
+ "(OR (AND a b) c)", // wrong case
+ "(a IMPLIES b)", // infix AND wrong case
+ "(not a b)", // wrong arity
+ "not a", // needs parens
+ "(ite a x)", // wrong arity
+ "(a b)" // using non-function as function
+};
+
+const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
+
+class ParserBlack : public CxxTest::TestSuite {
+ ExprManager *d_exprManager;
+
+ /* Set up declaration context for expr inputs */
+
+ void setupContext(ParserState* parserState) {
+ /* a, b, c: BOOLEAN */
+ parserState->mkVar("a",(Type*)d_exprManager->booleanType());
+ parserState->mkVar("b",(Type*)d_exprManager->booleanType());
+ parserState->mkVar("c",(Type*)d_exprManager->booleanType());
+ /* t, u, v: TYPE */
+ Type *t = parserState->newSort("t");
+ Type *u = parserState->newSort("u");
+ Type *v = parserState->newSort("v");
+ /* f : t->u; g: u->v; h: v->t; */
+ parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
+ parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
+ parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+ /* x:t; y:u; z:v; */
+ parserState->mkVar("x",t);
+ parserState->mkVar("y",u);
+ parserState->mkVar("z",v);
+ }
+
+ void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
+ for(int i = 0; i < numInputs; ++i) {
+ try {
+// Debug.on("parser");
+// Debug.on("parser-extra");
+ Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n";
+// istringstream stream(goodInputs[i]);
+ Input* parser = Input::newStringInput(d_exprManager, d_lang, goodInputs[i], "test");
+ TS_ASSERT( !parser->done() );
+ Command* cmd;
+ while((cmd = parser->parseNextCommand())) {
+ // cout << "Parsed command: " << (*cmd) << endl;
+ }
+ TS_ASSERT( parser->parseNextCommand() == NULL );
+ TS_ASSERT( parser->done() );
+ delete parser;
+// Debug.off("parser");
+// Debug.off("parser-extra");
+ } catch (Exception& e) {
+ cout << "\nGood input failed:\n" << goodInputs[i] << endl
+ << e << endl;
+// Debug.off("parser-extra");
+ throw;
+ }
+ }
+ }
+
+ void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) {
+ for(int i = 0; i < numInputs; ++i) {
+// cout << "Testing bad input: '" << badInputs[i] << "'\n";
+// Debug.on("parser");
+ Input* parser = Input::newStringInput(d_exprManager, d_lang, badInputs[i], "test");
+ TS_ASSERT_THROWS
+ ( while(parser->parseNextCommand());
+ cout << "\nBad input succeeded:\n" << badInputs[i] << endl;,
+ ParserException );
+// Debug.off("parser");
+ delete parser;
+ }
+ }
+
+ void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) {
+ // cout << "Using context: " << context << endl;
+// Debug.on("parser");
+// Debug.on("parser-extra");
+ for(int i = 0; i < numExprs; ++i) {
+ try {
+ // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n";
+ // Debug.on("parser");
+// istringstream stream(context + goodBooleanExprs[i]);
+ Input* input = Input::newStringInput(d_exprManager, d_lang,
+ goodBooleanExprs[i], "test");
+ TS_ASSERT( !input->done() );
+ setupContext(input->getParserState());
+ TS_ASSERT( !input->done() );
+ Expr e = input->parseNextExpression();
+ TS_ASSERT( !e.isNull() );
+ e = input->parseNextExpression();
+ TS_ASSERT( input->done() );
+ TS_ASSERT( e.isNull() );
+ delete input;
+ } catch (Exception& e) {
+ cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl;
+ cout << e;
+ throw e;
+ }
+ }
+ }
+
+ void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) {
+ //Debug.on("parser");
+ for(int i = 0; i < numExprs; ++i) {
+ // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n";
+// istringstream stream(context + badBooleanExprs[i]);
+ Input* input = Input::newStringInput(d_exprManager, d_lang,
+ badBooleanExprs[i], "test");
+
+ TS_ASSERT( !input->done() );
+ setupContext(input->getParserState());
+ TS_ASSERT( !input->done() );
+ TS_ASSERT_THROWS
+ ( input->parseNextExpression();
+ cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;,
+ ParserException );
+ delete input;
+ }
+ //Debug.off("parser");
+ }
+
+public:
+ void setUp() {
+ d_exprManager = new ExprManager();
+ }
+
+ void tearDown() {
+ delete d_exprManager;
+ }
+
+ void testGoodCvc4Inputs() {
+ tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
+ }
+
+ void testBadCvc4Inputs() {
+ tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs);
+ }
+
+ void testGoodCvc4Exprs() {
+ tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs);
+ }
+
+ void testBadCvc4Exprs() {
+ tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs);
+ }
+
+ void testGoodSmtInputs() {
+ tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs);
+ }
+
+ void testBadSmtInputs() {
+ tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs);
+ }
+
+ void testGoodSmtExprs() {
+ tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs);
+ }
+
+ void testBadSmtExprs() {
+ tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs);
+ }
+};
projects / cvc5.git / commitdiff