summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/getopt.cpp10
-rw-r--r--src/main/main.cpp49
-rw-r--r--src/parser/antlr_parser.cpp79
-rw-r--r--src/parser/antlr_parser.h69
-rw-r--r--src/parser/cvc/Makefile.am2
-rw-r--r--src/parser/cvc/Makefile.in5
-rw-r--r--src/parser/cvc/cvc_parser.cpp82
-rw-r--r--src/parser/cvc/cvc_parser.g120
-rw-r--r--src/parser/cvc/cvc_parser.h80
-rw-r--r--src/parser/parser.cpp89
-rw-r--r--src/parser/parser.h83
-rw-r--r--src/parser/smt/Makefile.am2
-rw-r--r--src/parser/smt/Makefile.in5
-rw-r--r--src/parser/smt/smt_parser.cpp79
-rw-r--r--src/parser/smt/smt_parser.g185
-rw-r--r--src/parser/smt/smt_parser.h79
-rw-r--r--src/parser/symbol_table.h19
-rw-r--r--src/util/command.cpp75
-rw-r--r--src/util/command.h50
-rw-r--r--src/util/options.h9
20 files changed, 571 insertions, 600 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index c191b2a15..81cbc2df8 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -30,9 +30,11 @@
#include "about.h"
#include "util/output.h"
#include "util/options.h"
+#include "parser/parser.h"
using namespace std;
using namespace CVC4;
+using namespace CVC4::parser;
namespace CVC4 {
namespace main {
@@ -97,13 +99,13 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
case 'L':
if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
- opts->lang = Options::LANG_CVC4;
+ opts->lang = Parser::LANG_CVC4;
break;
} else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
- opts->lang = Options::LANG_SMTLIB;
+ opts->lang = Parser::LANG_SMTLIB;
break;
} else if(!strcmp(optarg, "auto")) {
- opts->lang = Options::LANG_AUTO;
+ opts->lang = Parser::LANG_AUTO;
break;
}
@@ -126,7 +128,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
// silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
opts->smtcomp_mode = true;
opts->verbosity = -1;
- opts->lang = Options::LANG_SMTLIB;
+ opts->lang = Parser::LANG_SMTLIB;
break;
case '?':
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 6f32e474b..595915100 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -23,8 +23,6 @@
#include "main.h"
#include "usage.h"
#include "parser/parser.h"
-#include "parser/smt/smt_parser.h"
-#include "parser/cvc/cvc_parser.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "util/command.h"
@@ -69,13 +67,14 @@ int main(int argc, char *argv[]) {
bool inputFromStdin = firstArgIndex >= argc;
// Auto-detect input language by filename extension
- if(!inputFromStdin && options.lang == Options::LANG_AUTO) {
+ if(!inputFromStdin && options.lang == Parser::LANG_AUTO) {
if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4)) {
- options.lang = Options::LANG_SMTLIB;
- }
- else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) ||
- !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5)) {
- options.lang = Options::LANG_CVC4;
+ options.lang = Parser::LANG_SMTLIB;
+ } else if(!strcmp(".cvc", argv[firstArgIndex]
+ + strlen(argv[firstArgIndex]) - 4)
+ || !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex])
+ - 5)) {
+ options.lang = Parser::LANG_CVC4;
}
}
@@ -100,34 +99,12 @@ int main(int argc, char *argv[]) {
}
}
- // Set up the input stream, either cin or a file
- const char* fname;
- istream* in;
- ifstream* file;
- if(inputFromStdin) {
- fname = "stdin";
- in = &cin;
- } else {
- fname = argv[firstArgIndex];
- file = new ifstream(fname);
- in = file;
- }
-
// Create the parser
Parser* parser;
- switch(options.lang) {
- case Options::LANG_SMTLIB:
- parser = new SmtParser(&exprMgr, *in, fname);
- break;
- case Options::LANG_CVC4:
- parser = new CvcParser(&exprMgr, *in, fname);
- break;
- case Options::LANG_AUTO:
- cerr << "Auto language detection not supported yet." << endl;
- abort();
- default:
- cerr << "Unknown language" << endl;
- abort();
+ if(inputFromStdin) {
+ parser = Parser::getNewParser(&exprMgr, options.lang, cin);
+ } else {
+ parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]);
}
// Parse and execute commands until we are done
@@ -145,10 +122,6 @@ int main(int argc, char *argv[]) {
// Remove the parser
delete parser;
- if(! inputFromStdin) {
- // Delete handle to input file
- delete file;
- }
} catch(OptionException& e) {
if(options.smtcomp_mode) {
cout << "unknown" << endl;
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index c42415c54..be51aee6b 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -33,23 +33,6 @@ using namespace CVC4::parser;
namespace CVC4 {
namespace parser {
-ostream& operator<<(ostream& out, AntlrParser::BenchmarkStatus status) {
- switch(status) {
- case AntlrParser::SMT_SATISFIABLE:
- out << "sat";
- break;
- case AntlrParser::SMT_UNSATISFIABLE:
- out << "unsat";
- break;
- case AntlrParser::SMT_UNKNOWN:
- out << "unknown";
- break;
- default:
- Unhandled("Unhandled ostream case for AntlrParser::BenchmarkStatus");
- }
- return out;
-}
-
unsigned AntlrParser::getPrecedence(Kind kind) {
switch(kind) {
// Boolean operators
@@ -82,60 +65,56 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
}
Expr AntlrParser::getVariable(std::string var_name) {
- Expr e = d_var_symbol_table.getObject(var_name);
+ Expr e = d_varSymbolTable.getObject(var_name);
Debug("parser") << "getvar " << var_name << " gives " << e << endl;
return e;
}
Expr AntlrParser::getTrueExpr() const {
- return d_expr_manager->mkExpr(TRUE);
+ return d_exprManager->mkExpr(TRUE);
}
Expr AntlrParser::getFalseExpr() const {
- return d_expr_manager->mkExpr(FALSE);
+ return d_exprManager->mkExpr(FALSE);
}
-Expr AntlrParser::newExpression(Kind kind, const Expr& child) {
- return d_expr_manager->mkExpr(kind, child);
+Expr AntlrParser::mkExpr(Kind kind, const Expr& child) {
+ return d_exprManager->mkExpr(kind, child);
}
-Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) {
- return d_expr_manager->mkExpr(kind, child_1, child_2);
+Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1,
+ const Expr& child_2) {
+ return d_exprManager->mkExpr(kind, child_1, child_2);
}
-Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
- return d_expr_manager->mkExpr(kind, children);
+Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
+ return d_exprManager->mkExpr(kind, children);
}
void AntlrParser::newPredicate(std::string p_name, const std::vector<
std::string>& p_sorts) {
- if(p_sorts.size() == 0)
- d_var_symbol_table.bindName(p_name, d_expr_manager->mkVar());
- else
+ if(p_sorts.size() == 0) {
+ d_varSymbolTable.bindName(p_name, d_exprManager->mkVar());
+ } else {
Unhandled("Non unary predicate not supported yet!");
+ }
}
void AntlrParser::newPredicates(const std::vector<std::string>& p_names) {
vector<string> sorts;
- for(unsigned i = 0; i < p_names.size(); ++i)
+ for(unsigned i = 0; i < p_names.size(); ++i) {
newPredicate(p_names[i], sorts);
-}
-
-void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) {
- d_benchmark_status = status;
-}
-
-void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) {
+ }
}
void AntlrParser::setExpressionManager(ExprManager* em) {
- d_expr_manager = em;
+ d_exprManager = em;
}
bool AntlrParser::isDeclared(string name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
- return d_var_symbol_table.isBound(name);
+ return d_varSymbolTable.isBound(name);
default:
Unhandled("Unhandled symbol type!");
}
@@ -148,8 +127,8 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
LT(0).get()->getColumn());
}
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs,
- const vector<Kind>& kinds) {
+Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
+ Kind>& kinds) {
Assert( exprs.size() > 0, "Expected non-empty vector expr");
Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs");
return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
@@ -184,14 +163,28 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
Assert( end_index < exprs.size(), "Expected end_index < exprs.size. ");
Assert( start_index <= end_index, "Expected start_index <= end_index. ");
- if(start_index == end_index)
+ if(start_index == end_index) {
return exprs[start_index];
+ }
unsigned pivot = findPivot(kinds, start_index, end_index - 1);
Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
- return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
+ return d_exprManager->mkExpr(kinds[pivot], child_1, child_2);
+}
+
+bool AntlrParser::checkDeclation(string varName, DeclarationCheck check) {
+ switch(check) {
+ case CHECK_DECLARED:
+ return isDeclared(varName, SYM_VARIABLE);
+ case CHECK_UNDECLARED:
+ return !isDeclared(varName, SYM_VARIABLE);
+ case CHECK_NONE:
+ return true;
+ default:
+ Unhandled("Unknown check type!");
+ }
}
}/* CVC4::parser namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 8a9dea5ad..271171281 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -42,14 +42,14 @@ class AntlrParser : public antlr::LLkParser {
public:
- /** The status an SMT benchmark can have */
- enum BenchmarkStatus {
- /** Benchmark is satisfiable */
- SMT_SATISFIABLE,
- /** Benchmark is unsatisfiable */
- SMT_UNSATISFIABLE,
- /** The status of the benchmark is unknown */
- SMT_UNKNOWN
+ /** 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
};
/**
@@ -58,6 +58,18 @@ public:
*/
void setExpressionManager(ExprManager* expr_manager);
+ /**
+ * Parse a command.
+ * @return a command
+ */
+ virtual Command* parseCommand() = 0;
+
+ /**
+ * Parse an expression.
+ * @return the expression
+ */
+ virtual Expr parseExpr() = 0;
+
protected:
/**
@@ -97,6 +109,14 @@ protected:
Expr getVariable(std::string var_name);
/**
+ * Return true if the the declaration policy we want to enforce is true.
+ * @param varName the symbol to check
+ * @oaram check the kind of check to perform
+ * @return true if the check holds
+ */
+ bool checkDeclation(std::string varName, DeclarationCheck check);
+
+ /**
* Types of symbols.
*/
enum SymbolType {
@@ -131,21 +151,21 @@ protected:
* @param kind the kind of the expression
* @param child the child
*/
- Expr newExpression(Kind kind, const Expr& child);
+ Expr mkExpr(Kind kind, const Expr& child);
/**
* Creates a new binary CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
- Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2);
+ Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2);
/**
* Creates a new CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
- Expr newExpression(Kind kind, const std::vector<Expr>& children);
+ Expr mkExpr(Kind kind, const std::vector<Expr>& children);
/**
* Creates a new expression based on the given string of expressions and kinds,
@@ -170,24 +190,6 @@ protected:
void newPredicates(const std::vector<std::string>& p_names);
/**
- * Sets the status of the benchmark.
- * @param status the status of the benchmark
- */
- void setBenchmarkStatus(BenchmarkStatus status);
-
- /**
- * Returns the status of the parsed benchmark.
- * @return the status of the parsed banchmark
- */
- BenchmarkStatus getBenchmarkStatus() const;
-
- /**
- * Adds the extra sorts to the signature of the benchmark.
- * @param extra_sorts the sorts to add
- */
- void addExtraSorts(const std::vector<std::string>& extra_sorts);
-
- /**
* Returns the precedence rank of the kind.
*/
static unsigned getPrecedence(Kind kind);
@@ -206,18 +208,13 @@ private:
*/
Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
- /** The status of the benchmark */
- BenchmarkStatus d_benchmark_status;
-
/** The expression manager */
- ExprManager* d_expr_manager;
+ ExprManager* d_exprManager;
/** The symbol table lookup */
- SymbolTable<Expr> d_var_symbol_table;
+ SymbolTable<Expr> d_varSymbolTable;
};
-std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 666c408cf..ad0eb70d8 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -24,8 +24,6 @@ ANTLR_STUFF = \
libparsercvc_la_SOURCES = \
cvc_lexer.g \
cvc_parser.g \
- cvc_parser.h \
- cvc_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index 3fd1701c8..28b80800e 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
am__objects_2 = AntlrCvcLexer.lo $(am__objects_1)
am__objects_3 = AntlrCvcParser.lo
am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4)
+am_libparsercvc_la_OBJECTS = $(am__objects_4)
libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -249,8 +249,6 @@ ANTLR_STUFF = \
libparsercvc_la_SOURCES = \
cvc_lexer.g \
cvc_parser.g \
- cvc_parser.h \
- cvc_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
@@ -310,7 +308,6 @@ distclean-compile:
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
deleted file mode 100644
index 57d5e6c96..000000000
--- a/src/parser/cvc/cvc_parser.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-/********************* -*- C++ -*- */
-/** cvc_parser.cpp
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** CVC presentation language parser implementation.
- **/
-
-#include <iostream>
-#include <fstream>
-
-#include "parser/parser.h"
-#include "util/command.h"
-#include "util/Assert.h"
-#include "parser/parser_exception.h"
-#include "parser/antlr_parser.h"
-#include "parser/cvc/cvc_parser.h"
-#include "parser/cvc/generated/AntlrCvcParser.hpp"
-#include "parser/cvc/generated/AntlrCvcLexer.hpp"
-
-using namespace std;
-
-namespace CVC4 {
-namespace parser {
-
-Command* CvcParser::parseNextCommand() throw(ParserException) {
- Command* cmd = 0;
- if(!done()) {
- try {
- cmd = d_antlr_parser->command();
- if(cmd == 0) {
- setDone();
- cmd = new EmptyCommand("EOF");
- }
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return cmd;
-}
-
-Expr CvcParser::parseNextExpression() throw(ParserException) {
- Expr result;
- if(!done()) {
- try {
- result = d_antlr_parser->formula();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return result;
-}
-
-CvcParser::~CvcParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
-}
-
-CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
- Parser(em), d_input(input) {
- if(!d_input) {
- throw ParserException(string("Read error") +
- ((file_name != NULL) ? (string(" on ") + file_name) : ""));
- }
- d_antlr_lexer = new AntlrCvcLexer(d_input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 864719cfa..c7f932a0c 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -29,6 +29,23 @@ options {
}
/**
+ * Parses the next command.
+ * @return command or 0 if EOF
+ */
+parseCommand returns [CVC4::Command* cmd]
+ : cmd = command
+ ;
+
+/**
+ * Parses the next expression.
+ * @return the parsed expression (null expression if EOF)
+ */
+parseExpr returns [CVC4::Expr expr]
+ : expr = formula
+ | EOF
+ ;
+
+/**
* Matches a command of the input. If a declaration, it will return an empty
* command.
*/
@@ -41,64 +58,118 @@ command returns [CVC4::Command* cmd = 0]
| QUERY f = formula { cmd = new QueryCommand(f); }
| CHECKSAT f = formula { cmd = new CheckSatCommand(f); }
| CHECKSAT { cmd = new CheckSatCommand(); }
- | identifierList[ids] COLON type {
+ | identifierList[ids, CHECK_UNDECLARED] COLON type {
// [chris 12/15/2009] FIXME: decls may not be BOOLEAN
newPredicates(ids);
- cmd = new EmptyCommand("Declaration");
+ cmd = new DeclarationCommand(ids);
}
| EOF
;
-identifierList[std::vector<std::string>& id_list]
- : id1:IDENTIFIER { id_list.push_back(id1->getText()); }
- (
- COMMA
- id2:IDENTIFIER { id_list.push_back(id2->getText()); }
- )*
+/**
+ * Mathches a list of identifiers separated by a comma and puts them in the
+ * given list.
+ * @param idList the list to fill with identifiers.
+ * @param check what kinds of check to perform on the symbols
+ */
+identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE]
+{
+ string id;
+}
+ : id = identifier { idList.push_back(id); }
+ (COMMA id = identifier { idList.push_back(id); })*
;
+
+/**
+ * Matches an identifier and returns a string.
+ */
+identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
+ : x:IDENTIFIER { checkDeclation(x->getText(), check) }?
+ {
+ id = x->getText();
+ }
+ exception catch [antlr::SemanticException& ex] {
+ switch (check) {
+ case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
+ case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+ default: throw ex;
+ }
+ }
+ ;
+
+/**
+ * Matches a type.
+ * TODO: parse more types
+ */
type
: BOOLEAN
;
+/**
+ * Matches a CVC4 formula.
+ * @return the expression representing the formula
+ */
formula returns [CVC4::Expr formula]
- : formula = bool_formula
+ : formula = boolFormula
;
-bool_formula returns [CVC4::Expr formula]
+/**
+ * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of
+ * operands (primaryBoolFormulas) and operators (Kinds) and then calls the
+ * createPrecedenceExpr method to build the expression using the precedence
+ * and associativity of the operators.
+ * @return the expression representing the formula
+ */
+boolFormula returns [CVC4::Expr formula]
{
vector<Expr> formulas;
vector<Kind> kinds;
Expr f1, f2;
Kind k;
}
- : f1 = primary_bool_formula { formulas.push_back(f1); }
- ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )*
+ : f1 = primaryBoolFormula { formulas.push_back(f1); }
+ ( k = boolOperator { kinds.push_back(k); } f2 = primaryBoolFormula { formulas.push_back(f2); } )*
{
// Create the expression based on precedences
formula = createPrecedenceExpr(formulas, kinds);
}
;
-primary_bool_formula returns [CVC4::Expr formula]
- : formula = bool_atom
- | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
- | LPAREN formula = bool_formula RPAREN
+/**
+ * Parses a primary Boolean formula. A primary Boolean formula is either a
+ * Boolean atom (variables and predicates) a negation of a primary Boolean
+ * formula or a formula enclosed in parenthesis.
+ * @return the expression representing the formula
+ */
+primaryBoolFormula returns [CVC4::Expr formula]
+ : formula = boolAtom
+ | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); }
+ | LPAREN formula = boolFormula RPAREN
;
-bool_operator returns [CVC4::Kind kind]
+/**
+ * Parses the Boolean operators and returns the corresponding CVC4 expression
+ * kind.
+ * @param the kind of the Boolean operator
+ */
+boolOperator returns [CVC4::Kind kind]
: IMPLIES { kind = CVC4::IMPLIES; }
| AND { kind = CVC4::AND; }
| OR { kind = CVC4::OR; }
| XOR { kind = CVC4::XOR; }
| IFF { kind = CVC4::IFF; }
;
-
-bool_atom returns [CVC4::Expr atom]
+
+/**
+ * Parses the Boolean atoms (variables and predicates).
+ * @return the expression representing the atom.
+ */
+boolAtom returns [CVC4::Expr atom]
{
string p;
}
- : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
+ : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); }
exception catch [antlr::SemanticException ex] {
rethrow(ex, "Undeclared variable " + p);
}
@@ -106,7 +177,12 @@ bool_atom returns [CVC4::Expr atom]
| FALSE { atom = getFalseExpr(); }
;
-predicate_sym returns [std::string p]
- : id:IDENTIFIER { p = id->getText(); }
+/**
+ * Parses a predicate symbol (an identifier).
+ * @param what kind of check to perform on the id
+ * @return the predicate symol
+ */
+predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
+ : pSymbol = identifier[check]
;
\ No newline at end of file
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
deleted file mode 100644
index 82d659566..000000000
--- a/src/parser/cvc/cvc_parser.h
+++ /dev/null
@@ -1,80 +0,0 @@
-/********************* -*- C++ -*- */
-/** cvc_parser.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** CVC presentation language parser abstraction.
- **/
-
-#ifndef __CVC4__PARSER__CVC_PARSER_H
-#define __CVC4__PARSER__CVC_PARSER_H
-
-#include <string>
-#include <iostream>
-#include <fstream>
-#include "cvc4_config.h"
-#include "parser/parser_exception.h"
-#include "parser/parser.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * The CVC parser.
- */
-class CVC4_PUBLIC CvcParser : public Parser {
-
-public:
-
- /**
- * Construct the parser that uses the given expression manager and parses
- * from the given input stream.
- * @param em the expression manager to use
- * @param input the input stream to parse
- * @param file_name the name of the file (for diagnostic output)
- */
- CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
-
- /**
- * Destructor.
- */
- ~CvcParser();
-
- /**
- * Parses the next command. By default, the CVC parser produces one
- * CommandSequence command. If parsing is successful, we should be
- * done after the first call to this command.
- * @return the CommandSequence command that includes the whole
- * benchmark
- */
- Command* parseNextCommand() throw(ParserException);
-
- /**
- * Parses the next complete expression of the stream.
- * @return the expression parsed
- */
- Expr parseNextExpression() throw(ParserException);
-
-protected:
-
- /** The ANTLR smt lexer */
- AntlrCvcLexer* d_antlr_lexer;
-
- /** The ANTLR smt parser */
- AntlrCvcParser* d_antlr_parser;
-
- /** The file stream we might be using */
- std::istream& d_input;
-};
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__CVC_PARSER_H */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2ff409686..e919a53e8 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -15,6 +15,7 @@
#include <iostream>
#include <fstream>
+#include <antlr/CharScanner.hpp>
#include "parser.h"
#include "util/command.h"
@@ -27,14 +28,11 @@
#include "parser/cvc/generated/AntlrCvcLexer.hpp"
using namespace std;
+using namespace antlr;
namespace CVC4 {
namespace parser {
-Parser::Parser(ExprManager* em) :
- d_expr_manager(em), d_done(false) {
-}
-
void Parser::setDone(bool done) {
d_done = done;
}
@@ -43,5 +41,88 @@ bool Parser::done() const {
return d_done;
}
+Command* Parser::parseNextCommand() throw (ParserException) {
+ Command* cmd = 0;
+ if(!done()) {
+ try {
+ cmd = d_antlrParser->parseCommand();
+ if(cmd == 0) {
+ setDone();
+ cmd = new EmptyCommand("EOF");
+ }
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return cmd;
+}
+
+Expr Parser::parseNextExpression() throw (ParserException) {
+ Expr result;
+ if(!done()) {
+ try {
+ result = d_antlrParser->parseExpr();
+ if(result.isNull())
+ setDone();
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return result;
+}
+
+Parser::~Parser() {
+ delete d_antlrParser;
+ delete d_antlrLexer;
+ if (d_deleteInput) delete d_input;
+}
+
+Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) :
+ d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) {
+}
+
+Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
+ istream* input, string filename, bool deleteInput) {
+
+ AntlrParser* antlrParser = 0;
+ antlr::CharScanner* antlrLexer = 0;
+
+ switch(lang) {
+ case LANG_CVC4: {
+ antlrLexer = new AntlrCvcLexer(*input);
+ antlrLexer->setFilename(filename);
+ antlrParser = new AntlrCvcParser(*antlrLexer);
+ antlrParser->setFilename(filename);
+ antlrParser->setExpressionManager(em);
+ break;
+ }
+ case LANG_SMTLIB: {
+ antlrLexer = new AntlrSmtLexer(*input);
+ antlrLexer->setFilename(filename);
+ antlrParser = new AntlrSmtParser(*antlrLexer);
+ antlrParser->setFilename(filename);
+ antlrParser->setExpressionManager(em);
+ break;
+ }
+ default:
+ Unhandled("Unknown Input language!");
+ }
+
+ return new Parser(input, antlrParser, antlrLexer, deleteInput);
+}
+
+Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
+ string filename) {
+ istream* input = new ifstream(filename.c_str());
+ return getNewParser(em, lang, input, filename, true);
+}
+
+Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
+ istream& input) {
+ return getNewParser(em, lang, &input, "", false);
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index b448cd2a6..d6180b9a3 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -18,9 +18,13 @@
#include <string>
#include <iostream>
-#include <fstream>
#include "cvc4_config.h"
#include "parser_exception.h"
+#include "antlr_parser.h"
+
+namespace antlr {
+ class CharScanner;
+}
namespace CVC4 {
@@ -31,57 +35,88 @@ class ExprManager;
namespace parser {
-class AntlrSmtLexer;
-class AntlrSmtParser;
-class AntlrCvcLexer;
-class AntlrCvcParser;
-
/**
- * The parser.
+ * The parser. The parser should be obtained by calling the static methods
+ * getNewParser, and should be deleted when done.
*/
class CVC4_PUBLIC Parser {
public:
- /**
- * Construct the parser that uses the given expression manager.
- * @param em the expression manager.
- */
- Parser(ExprManager* em);
+ /** The input language option */
+ enum InputLanguage {
+ /** The SMTLIB input language */
+ LANG_SMTLIB,
+ /** The CVC4 input language */
+ LANG_CVC4,
+ /** Auto-detect the language */
+ LANG_AUTO
+ };
+
+ static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::string filename);
+ static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input);
/**
* Destructor.
*/
- virtual ~Parser() {
- }
+ ~Parser();
/**
- * Parse the next command of the input
+ * Parse the next command of the input. If EOF is encountered a EmptyCommand
+ * is returned and done flag is set.
*/
- virtual Command* parseNextCommand() throw (ParserException) = 0;
+ Command* parseNextCommand() throw (ParserException);
/**
- * Parse the next expression of the stream
+ * Parse the next expression of the stream. If EOF is encountered a null
+ * expression is returned and done flag is set.
+ * @return the parsed expression
*/
- virtual Expr parseNextExpression() throw (ParserException) = 0;
+ Expr parseNextExpression() throw (ParserException);
/**
- * Check if we are done -- either the end of input has been reached.
+ * 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;
-protected:
+private:
+
+ /**
+ * Create a new parser.
+ * @param em the expression manager to usee
+ * @param lang the language to parse
+ * @param input the input stream to parse
+ * @param filename the filename to attach to the stream
+ * @param deleteInput wheather to delete the input
+ * @return the parser
+ */
+ static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream* input, std::string filename, bool deleteInput);
+
+ /**
+ * Create a new parser given the actual antlr parser.
+ * @param antlrParser the antlr parser to user
+ */
+ Parser(std::istream* input, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer, bool deleteInput);
/** Sets the done flag */
void setDone(bool done = true);
- /** Expression manager the parser will be using */
- ExprManager* d_expr_manager;
-
/** Are we done */
bool d_done;
-}; // end of class Parser
+ /** The antlr parser */
+ AntlrParser* d_antlrParser;
+
+ /** The entlr lexer */
+ antlr::CharScanner* d_antlrLexer;
+
+ /** The input stream we are using */
+ std::istream* d_input;
+
+ /** Wherther to de-allocate the input */
+ bool d_deleteInput;}; // end of class Parser
}/* CVC4::parser namespace */
}/* CVC4 namespace */
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 6f5f1bfd4..96ad9c27f 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -24,8 +24,6 @@ ANTLR_STUFF = \
libparsersmt_la_SOURCES = \
smt_lexer.g \
smt_parser.g \
- smt_parser.h \
- smt_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 721ff0e2b..6145b4c4e 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -56,7 +56,7 @@ am__objects_1 =
am__objects_2 = AntlrSmtLexer.lo $(am__objects_1)
am__objects_3 = AntlrSmtParser.lo
am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4)
+am_libparsersmt_la_OBJECTS = $(am__objects_4)
libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -249,8 +249,6 @@ ANTLR_STUFF = \
libparsersmt_la_SOURCES = \
smt_lexer.g \
smt_parser.g \
- smt_parser.h \
- smt_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
@@ -310,7 +308,6 @@ distclean-compile:
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
deleted file mode 100644
index 8c5773e32..000000000
--- a/src/parser/smt/smt_parser.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-/********************* -*- C++ -*- */
-/** smt_parser.cpp
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** SMT-LIB language parser implementation.
- **/
-
-#include <iostream>
-#include <fstream>
-
-#include "parser/parser.h"
-#include "util/command.h"
-#include "util/Assert.h"
-#include "parser/parser_exception.h"
-#include "parser/antlr_parser.h"
-#include "parser/smt/smt_parser.h"
-#include "parser/smt/generated/AntlrSmtParser.hpp"
-#include "parser/smt/generated/AntlrSmtLexer.hpp"
-
-using namespace std;
-
-namespace CVC4 {
-namespace parser {
-
-Command* SmtParser::parseNextCommand() throw(ParserException) {
- Command* cmd = 0;
- if(!done()) {
- try {
- cmd = d_antlr_parser->benchmark();
- setDone();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return cmd;
-}
-
-Expr SmtParser::parseNextExpression() throw(ParserException) {
- Expr result;
- if(!done()) {
- try {
- result = d_antlr_parser->an_formula();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return result;
-}
-
-SmtParser::~SmtParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
-}
-
-SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
- Parser(em), d_input(input) {
- if(!d_input) {
- throw ParserException(string("Read error") +
- ((file_name != NULL) ? (string(" on ") + file_name) : ""));
- }
- d_antlr_lexer = new AntlrSmtLexer(input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
-}
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 6e0051821..f7045fa7e 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -27,6 +27,108 @@ options {
defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
k = 2;
}
+
+/**
+ * Parses an expression.
+ * @return the parsed expression
+ */
+parseExpr returns [CVC4::Expr expr]
+ : expr = annotatedFormula
+ ;
+
+/**
+ * Parses a command (the whole benchmark)
+ * @return the command of the benchmark
+ */
+parseCommand returns [CVC4::Command* cmd]
+ : cmd = benchmark
+ ;
+
+/**
+ * Matches the whole SMT-LIB benchmark.
+ * @return the sequence command containing the whole problem
+ */
+benchmark returns [Command* cmd]
+ : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN
+ | EOF { cmd = 0; }
+ ;
+
+/**
+ * Matchecs sequence of benchmark attributes and returns a pointer to a command
+ * sequence command.
+ * @return the command sequence
+ */
+benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
+{
+ Command* cmd;
+}
+ : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+
+ ;
+
+/**
+ * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns
+ * a corresponding command
+ * @retrurn a command corresponding to the attribute
+ */
+benchAttribute returns [ Command* smt_command = 0]
+{
+ Expr formula;
+ string logic;
+ SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
+}
+ : C_LOGIC logic = identifier { smt_command = new SetBenchmarkLogicCommand(logic); }
+ | C_ASSUMPTION formula = annotatedFormula { smt_command = new AssertCommand(formula); }
+ | C_FORMULA formula = annotatedFormula { smt_command = new CheckSatCommand(formula); }
+ | C_STATUS b_status = status { smt_command = new SetBenchmarkStatusCommand(b_status); }
+ | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN
+ | C_NOTES STRING_LITERAL
+ | annotation
+ ;
+
+/**
+ * Matches an identifier and returns a string.
+ * @param check what kinds of check to do on the symbol
+ * @return the id string
+ */
+identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
+ : x:IDENTIFIER { checkDeclation(x->getText(), check) }?
+ {
+ id = x->getText();
+ }
+ exception catch [antlr::SemanticException& ex] {
+ switch (check) {
+ case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
+ case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+ default: throw ex;
+ }
+ }
+ ;
+
+/**
+ * Matches an annotated formula.
+ * @return the expression representing the formula
+ */
+annotatedFormula returns [CVC4::Expr formula]
+{
+ Kind kind;
+ vector<Expr> children;
+}
+ : formula = annotatedAtom
+ | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); }
+ ;
+
+/**
+ * Matches an annotated proposition atom, which is either a propositional atom
+ * or built of other atoms using a predicate symbol.
+ */
+annotatedAtom returns [CVC4::Expr atom]
+ : atom = propositionalAtom
+ ;
+
+
+
+
+
/**
* Matches an attribute name from the input (:attribute_name).
@@ -34,7 +136,7 @@ options {
attribute
: C_IDENTIFIER
;
-
+
/**
* Matches the sort symbol, which can be an arbitrary identifier.
*/
@@ -60,7 +162,7 @@ pred_symb returns [std::string p]
/**
* Matches a propositional atom.
*/
-prop_atom returns [CVC4::Expr atom]
+propositionalAtom returns [CVC4::Expr atom]
{
std::string p;
}
@@ -71,22 +173,11 @@ prop_atom returns [CVC4::Expr atom]
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
-
-/**
- * Matches an annotated proposition atom, which is either a propositional atom
- * or built of other atoms using a predicate symbol. Annotation can be added if
- * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
- * here in order to get rid of the ugly antlr non-determinism warnings.
- */
- // [chris 12/15/2009] FIXME: Where is the annotation?
-an_atom returns [CVC4::Expr atom]
- : atom = prop_atom
- ;
-
+
/**
* Matches on of the unary Boolean connectives.
*/
-bool_connective returns [CVC4::Kind kind]
+boolConnective returns [CVC4::Kind kind]
: NOT { kind = CVC4::NOT; }
| IMPLIES { kind = CVC4::IMPLIES; }
| AND { kind = CVC4::AND; }
@@ -94,24 +185,12 @@ bool_connective returns [CVC4::Kind kind]
| XOR { kind = CVC4::XOR; }
| IFF { kind = CVC4::IFF; }
;
-
-/**
- * Matches an annotated formula.
- */
-an_formula returns [CVC4::Expr formula]
-{
- Kind kind;
- vector<Expr> children;
-}
- : formula = an_atom
- | LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children); }
- ;
-
-an_formulas[std::vector<Expr>& formulas]
+
+annotatedFormulas[std::vector<Expr>& formulas]
{
Expr f;
}
- : ( f = an_formula { formulas.push_back(f); } )+
+ : ( f = annotatedFormula { formulas.push_back(f); } )+
;
/**
@@ -138,44 +217,8 @@ sort_symbs[std::vector<std::string>& sorts]
/**
* Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
*/
-status returns [ AntlrParser::BenchmarkStatus status ]
- : SAT { status = SMT_SATISFIABLE; }
- | UNSAT { status = SMT_UNSATISFIABLE; }
- | UNKNOWN { status = SMT_UNKNOWN; }
- ;
-
-/**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', etc.
- */
-bench_attribute returns [ Command* smt_command = 0]
-{
- BenchmarkStatus b_status = SMT_UNKNOWN;
- Expr formula;
- vector<string> sorts;
-}
- : C_LOGIC IDENTIFIER
- | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); }
- | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); }
- | C_STATUS b_status = status { setBenchmarkStatus(b_status); }
- | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); }
- | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN
- | C_NOTES STRING_LITERAL
- | annotation
- ;
-
-/**
- * Returns a pointer to a command sequence command.
- */
-bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
-{
- Command* cmd;
-}
- : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+
- ;
-
-/**
- * Matches the whole SMT-LIB benchmark.
- */
-benchmark returns [Command* cmd]
- : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN
- ;
+status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ]
+ : SAT { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE; }
+ | UNSAT { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE; }
+ | UNKNOWN { status = SetBenchmarkStatusCommand::SMT_UNKNOWN; }
+ ; \ No newline at end of file
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
deleted file mode 100644
index 21c278a37..000000000
--- a/src/parser/smt/smt_parser.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/********************* -*- C++ -*- */
-/** smt_parser.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** SMT-LIB language parser abstraction.
- **/
-
-#ifndef __CVC4__PARSER__SMT_PARSER_H
-#define __CVC4__PARSER__SMT_PARSER_H
-
-#include <string>
-#include <iostream>
-#include <fstream>
-#include "cvc4_config.h"
-#include "parser/parser_exception.h"
-#include "parser/parser.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * The SMT parser.
- */
-class CVC4_PUBLIC SmtParser : public Parser {
-
-public:
-
- /**
- * Construct the parser that uses the given expression manager and input stream.
- * @param em the expression manager to use
- * @param input the input stream to parse
- * @param file_name the name of the file (for diagnostic output)
- */
- SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
-
- /**
- * Destructor.
- */
- ~SmtParser();
-
- /**
- * Parses the next command. By default, the SMT-LIB parser produces
- * one CommandSequence command. If parsing is successful, we should
- * be done after the first call to this command.
- * @return the CommandSequence command that includes the whole
- * benchmark
- */
- Command* parseNextCommand() throw(ParserException);
-
- /**
- * Parses the next complete expression of the stream.
- * @return the expression parsed
- */
- Expr parseNextExpression() throw(ParserException);
-
-protected:
-
- /** The ANTLR smt lexer */
- AntlrSmtLexer* d_antlr_lexer;
-
- /** The ANTLR smt parser */
- AntlrSmtParser* d_antlr_parser;
-
- /** The file stream we might be using */
- std::istream& d_input;
-};
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__SMT_PARSER_H */
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 66d5727d6..8c9582762 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -49,7 +49,7 @@ private:
typedef typename LookupTable::const_iterator const_table_iterator;
/** Bindings for the names */
- LookupTable d_name_bindings;
+ LookupTable d_nameBindings;
public:
@@ -58,18 +58,18 @@ public:
* has been bind before, this will redefine it until its undefined.
*/
void bindName(const std::string name, const ObjectType& obj) throw () {
- d_name_bindings[name].push(obj);
+ d_nameBindings[name].push(obj);
}
/**
* Unbinds the last binding of the name to the expression.
*/
void unbindName(const std::string name) throw () {
- table_iterator find = d_name_bindings.find(name);
- if(find != d_name_bindings.end()) {
+ table_iterator find = d_nameBindings.find(name);
+ if(find != d_nameBindings.end()) {
find->second.pop();
if(find->second.empty()) {
- d_name_bindings.erase(find);
+ d_nameBindings.erase(find);
}
}
}
@@ -79,9 +79,10 @@ public:
*/
ObjectType getObject(const std::string name) throw () {
ObjectType result;
- table_iterator find = d_name_bindings.find(name);
- if(find != d_name_bindings.end())
+ table_iterator find = d_nameBindings.find(name);
+ if(find != d_nameBindings.end()) {
result = find->second.top();
+ }
return result;
}
@@ -89,8 +90,8 @@ public:
* Returns true is name is bound to an expression.
*/
bool isBound(const std::string name) const throw () {
- const_table_iterator find = d_name_bindings.find(name);
- return (find != d_name_bindings.end());
+ const_table_iterator find = d_nameBindings.find(name);
+ return (find != d_nameBindings.end());
}
};
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 5a5b766cb..b80851233 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -20,8 +20,9 @@
* Author: dejan
*/
-#include <map>
+#include <sstream>
#include "util/command.h"
+#include "util/Assert.h"
#include "smt/smt_engine.h"
using namespace std;
@@ -29,10 +30,16 @@ using namespace std;
namespace CVC4 {
ostream& operator<<(ostream& out, const Command& c) {
- c.toString(out);
+ c.toStream(out);
return out;
}
+std::string Command::toString() const {
+ stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
EmptyCommand::EmptyCommand(string name) :
d_name(name) {
}
@@ -87,26 +94,26 @@ void CommandSequence::addCommand(Command* cmd) {
d_command_sequence.push_back(cmd);
}
-void EmptyCommand::toString(ostream& out) const {
+void EmptyCommand::toStream(ostream& out) const {
out << "EmptyCommand(" << d_name << ")";
}
-void AssertCommand::toString(ostream& out) const {
+void AssertCommand::toStream(ostream& out) const {
out << "Assert(" << d_expr << ")";
}
-void CheckSatCommand::toString(ostream& out) const {
+void CheckSatCommand::toStream(ostream& out) const {
if(d_expr.isNull())
out << "CheckSat()";
else
out << "CheckSat(" << d_expr << ")";
}
-void QueryCommand::toString(ostream& out) const {
+void QueryCommand::toStream(ostream& out) const {
out << "Query(" << d_expr << ")";
}
-void CommandSequence::toString(ostream& out) const {
+void CommandSequence::toStream(ostream& out) const {
out << "CommandSequence[" << endl;
for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) {
out << *d_command_sequence[i] << endl;
@@ -114,4 +121,58 @@ void CommandSequence::toString(ostream& out) const {
out << "]";
}
+DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+void DeclarationCommand::toStream(std::ostream& out) const {
+ out << "Declare(";
+ bool first = true;
+ for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
+ if(first) {
+ out << ", ";
+ first = false;
+ }
+ out << d_declaredSymbols[i];
+ }
+ out << ")";
+}
+
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+ d_status(status) {
+}
+
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // TODO: something to be done with the status
+}
+
+void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(";
+ switch(d_status) {
+ case SMT_SATISFIABLE:
+ out << "sat";
+ break;
+ case SMT_UNSATISFIABLE:
+ out << "unsat";
+ break;
+ case SMT_UNKNOWN:
+ out << "unknown";
+ break;
+ default:
+ Unhandled("Unknown benchmark status");
+ }
+ out << ")";
+}
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic)
+ {}
+
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // TODO: something to be done with the logic
+}
+
+void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 9cc009d01..b41be4592 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -35,14 +35,15 @@ class CVC4_PUBLIC Command {
public:
virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
virtual ~Command() {};
- virtual void toString(std::ostream&) const = 0;
+ virtual void toStream(std::ostream&) const = 0;
+ std::string toString() const;
};/* class Command */
class CVC4_PUBLIC EmptyCommand : public Command {
public:
EmptyCommand(std::string name = "");
void invoke(CVC4::SmtEngine* smt_engine);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
private:
std::string d_name;
};/* class EmptyCommand */
@@ -52,18 +53,26 @@ class CVC4_PUBLIC AssertCommand : public Command {
public:
AssertCommand(const BoolExpr& e);
void invoke(CVC4::SmtEngine* smt_engine);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
};/* class AssertCommand */
+class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
+public:
+ DeclarationCommand(const std::vector<std::string>& ids);
+ void toStream(std::ostream& out) const;
+protected:
+ std::vector<std::string> d_declaredSymbols;
+};
+
class CVC4_PUBLIC CheckSatCommand : public Command {
public:
CheckSatCommand();
CheckSatCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
};/* class CheckSatCommand */
@@ -73,19 +82,48 @@ class CVC4_PUBLIC QueryCommand : public Command {
public:
QueryCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
};/* class QueryCommand */
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+public:
+ /** The status an SMT benchmark can have */
+ enum BenchmarkStatus {
+ /** Benchmark is satisfiable */
+ SMT_SATISFIABLE,
+ /** Benchmark is unsatisfiable */
+ SMT_UNSATISFIABLE,
+ /** The status of the benchmark is unknown */
+ SMT_UNKNOWN
+ };
+ SetBenchmarkStatusCommand(BenchmarkStatus status);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ BenchmarkStatus d_status;
+};/* class QueryCommand */
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+public:
+ SetBenchmarkLogicCommand(std::string logic);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ std::string d_logic;
+};/* class QueryCommand */
+
+
+
class CVC4_PUBLIC CommandSequence : public Command {
public:
CommandSequence();
~CommandSequence();
void invoke(SmtEngine* smt);
void addCommand(Command* cmd);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
private:
/** All the commands to be executed (in sequence) */
std::vector<Command*> d_command_sequence;
diff --git a/src/util/options.h b/src/util/options.h
index 2bfbf675f..d6c4e9009 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -13,11 +13,12 @@
** Global (command-line or equivalent) tuning parameters.
**/
-#include <iostream>
-
#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
+#include <iostream>
+#include "parser/parser.h"
+
namespace CVC4 {
struct Options {
@@ -48,7 +49,7 @@ struct Options {
};
/** The input language */
- InputLanguage lang;
+ parser::Parser::InputLanguage lang;
Options() : binary_name(),
smtcomp_mode(false),
@@ -56,7 +57,7 @@ struct Options {
out(0),
err(0),
verbosity(0),
- lang(LANG_AUTO)
+ lang(parser::Parser::LANG_AUTO)
{}
};/* struct Options */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback