summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/antlr_parser.cpp15
-rw-r--r--src/parser/antlr_parser.h2
-rw-r--r--src/parser/cvc/Makefile.am6
-rw-r--r--src/parser/parser.cpp2
-rw-r--r--src/parser/smt/Makefile.am6
-rw-r--r--src/parser/symbol_table.h99
6 files changed, 74 insertions, 56 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 52f3c4668..04a82f721 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -9,12 +9,16 @@
#include "antlr_parser.h"
#include "expr/expr_manager.h"
+#include "util/output.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
-ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) {
+namespace CVC4 {
+namespace parser {
+
+ostream& operator<<(ostream& out, AntlrParser::BenchmarkStatus status) {
switch(status) {
case AntlrParser::SMT_SATISFIABLE:
out << "sat";
@@ -63,7 +67,9 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
}
Expr AntlrParser::getVariable(std::string var_name) {
- return d_var_symbol_table.getObject(var_name);
+ Expr e = d_var_symbol_table.getObject(var_name);
+ Debug("parser") << "getvar " << var_name << " gives " << e << endl;
+ return e;
}
Expr AntlrParser::getTrueExpr() const {
@@ -89,7 +95,7 @@ Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& 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->mkExpr(VARIABLE));
+ d_var_symbol_table.bindName(p_name, d_expr_manager->mkVar());
else
Unhandled("Non unary predicate not supported yet!");
}
@@ -161,3 +167,6 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 0db12a0f0..ad23d45f8 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -18,7 +18,7 @@
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
#include "parser/symbol_table.h"
namespace CVC4 {
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 4c1a5d92b..b132ede5c 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -18,7 +18,9 @@ libparsercvc_la_SOURCES = \
BUILT_SOURCES = $(ANTLR_STUFF)
CLEAN_FILES = $(ANTLR_STUFF)
-AntlrCvcLexer.cpp AntlrCvcLexer.hpp: CvcLexer.g
+AntlrCvcLexer.cpp: CvcLexer.g
$(ANTLR) -o "@builddir@" "$<"
-AntlrCvcParser.cpp AntlrCvcParser.hpp: CvcParser.g
+AntlrCvcParser.cpp: CvcParser.g CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt
$(ANTLR) -o "@builddir@" "$<"
+AntlrCvcLexer.hpp CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt: AntlrCvcLexer.cpp
+AntlrCvcParser.hpp: AntlrCvcParser.cpp
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 65a5d11c1..4c7e28dc0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -15,7 +15,7 @@
#include "parser.h"
#include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
#include "parser_exception.h"
#include "parser/antlr_parser.h"
#include "parser/smt/AntlrSmtParser.hpp"
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 6017409fd..9769fabcb 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -18,7 +18,9 @@ libparsersmt_la_SOURCES = \
BUILT_SOURCES = $(ANTLR_STUFF)
CLEAN_FILES = $(ANTLR_STUFF)
-AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
+AntlrSmtLexer.cpp: SmtLexer.g
$(ANTLR) -o "@builddir@" "$<"
-AntlrSmtParser.cpp AntlrSmtParser.hpp: SmtParser.g
+AntlrSmtParser.cpp: SmtParser.g SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt
$(ANTLR) -o "@builddir@" "$<"
+AntlrSmtLexer.hpp SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt: AntlrSmtLexer.cpp
+AntlrSmtParser.hpp: AntlrSmtParser.cpp
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 3b08aa5f5..32532c734 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -9,6 +9,9 @@
**
**/
+#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
+#define __CVC4__PARSER__SYMBOL_TABLE_H
+
#include <string>
#include <stack>
#include <ext/hash_map>
@@ -31,63 +34,65 @@ namespace parser {
* Generic symbol table for looking up variables by name.
*/
template<typename ObjectType>
- class SymbolTable {
+class SymbolTable {
- private:
+private:
- /** The name to expression bindings */
- typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
- LookupTable;
- /** The table iterator */
- typedef typename LookupTable::iterator table_iterator;
- /** The table iterator */
- typedef typename LookupTable::const_iterator const_table_iterator;
+ /** The name to expression bindings */
+ typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
+ LookupTable;
+ /** The table iterator */
+ typedef typename LookupTable::iterator table_iterator;
+ /** The table iterator */
+ typedef typename LookupTable::const_iterator const_table_iterator;
- /** Bindings for the names */
- LookupTable d_name_bindings;
+ /** Bindings for the names */
+ LookupTable d_name_bindings;
- public:
+public:
- /**
- * Bind the name of the variable to the given expression. If the variable
- * 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);
- }
+ /**
+ * Bind the name of the variable to the given expression. If the variable
+ * 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);
+ }
- /**
- * 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()) {
- find->second.pop();
- if(find->second.empty()) {
- d_name_bindings.erase(find);
- }
+ /**
+ * 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()) {
+ find->second.pop();
+ if(find->second.empty()) {
+ d_name_bindings.erase(find);
}
}
+ }
- /**
- * Returns the last binding expression of the name.
- */
- ObjectType getObject(const std::string name) throw () {
- ObjectType result;
- table_iterator find = d_name_bindings.find(name);
- if(find != d_name_bindings.end())
- result = find->second.top();
- return result;
- }
+ /**
+ * Returns the last binding expression of the name.
+ */
+ ObjectType getObject(const std::string name) throw () {
+ ObjectType result;
+ table_iterator find = d_name_bindings.find(name);
+ if(find != d_name_bindings.end())
+ result = find->second.top();
+ return result;
+ }
- /**
- * 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());
- }
- };
+ /**
+ * 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());
+ }
+};
}/* CVC4::parser namespace */
}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback