diff options
Diffstat (limited to 'src/parser/antlr_parser.cpp')
-rw-r--r-- | src/parser/antlr_parser.cpp | 84 |
1 files changed, 77 insertions, 7 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index c4e6eef19..52f3c4668 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -26,12 +26,30 @@ ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) { out << "unknown"; break; default: - CVC4::UnhandledImpl( - "Unhandled ostream case for AntlrParser::BenchmarkStatus"); + Unhandled("Unhandled ostream case for AntlrParser::BenchmarkStatus"); } return out; } +unsigned AntlrParser::getPrecedence(Kind kind) { + switch(kind) { + // Boolean operators + case OR: + return 5; + case AND: + return 4; + case IFF: + return 3; + case IMPLIES: + return 2; + case XOR: + return 1; + default: + Unhandled ("Undefined precedence - necessary for proper parsing of CVC files!"); + } + return 0; +} + AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) : antlr::LLkParser(state, k) { } @@ -56,23 +74,37 @@ Expr AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } +Expr AntlrParser::newExpression(Kind kind, const Expr& child) { + return d_expr_manager->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::newExpression(Kind kind, const std::vector<Expr>& children) { return d_expr_manager->mkExpr(kind, children); } -void AntlrParser::newPredicate(std::string p_name, - std::vector<std::string>& p_sorts) { +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)); 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) + newPredicate(p_names[i], sorts); +} + void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { d_benchmark_status = status; } -void AntlrParser::addExtraSorts(std::vector<std::string>& extra_sorts) { +void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) { } void AntlrParser::setExpressionManager(ExprManager* em) { @@ -88,6 +120,44 @@ bool AntlrParser::isDeclared(string name, SymbolType type) { } } -void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) throw(antlr::SemanticException) { - throw antlr::SemanticException(new_message, getFilename(), LT(0).get()->getLine(), LT(0).get()->getColumn()); +void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) + throw (antlr::SemanticException) { + throw antlr::SemanticException(new_message, getFilename(), + LT(0).get()->getLine(), + LT(0).get()->getColumn()); +} + +Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< + Kind>& kinds) { + return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); +} + +unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, + unsigned start_index, unsigned end_index) const { + + int pivot = start_index; + unsigned pivot_precedence = getPrecedence(kinds[pivot]); + + for(unsigned i = start_index + 1; i <= end_index; ++i) { + unsigned current_precedence = getPrecedence(kinds[i]); + if(current_precedence > pivot_precedence) { + pivot = i; + pivot_precedence = current_precedence; + } + } + + return pivot; +} + +Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, + const std::vector<Kind>& kinds, + unsigned start_index, unsigned 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); } |