From 2163539a8b839acf98bda0e1a65f1fcca5232fb2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 8 Dec 2009 10:10:20 +0000 Subject: work on propositional layer, expression builder support for large expressions, output classes, and minisat --- src/parser/antlr_parser.cpp | 15 +++++-- src/parser/antlr_parser.h | 2 +- src/parser/cvc/Makefile.am | 6 ++- src/parser/parser.cpp | 2 +- src/parser/smt/Makefile.am | 6 ++- src/parser/symbol_table.h | 99 ++++++++++++++++++++++++--------------------- 6 files changed, 74 insertions(+), 56 deletions(-) (limited to 'src/parser') 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& 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& 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 #include #include @@ -31,63 +34,65 @@ namespace parser { * Generic symbol table for looking up variables by name. */ template - class SymbolTable { +class SymbolTable { - private: +private: - /** The name to expression bindings */ - typedef __gnu_cxx ::hash_map > - 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 > + 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 */ -- cgit v1.2.3