diff options
| -rw-r--r-- | src/parser/antlr_parser.cpp | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index be51aee6b..dd052ca2e 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -36,16 +36,16 @@ namespace parser { unsigned AntlrParser::getPrecedence(Kind kind) { switch(kind) { // Boolean operators - case OR: - return 5; - case AND: - return 4; case IFF: - return 3; + return 1; case IMPLIES: return 2; + case OR: + return 3; case XOR: - return 1; + return 4; + case AND: + return 5; default: Unhandled ("Undefined precedence - necessary for proper parsing of CVC files!"); } @@ -134,6 +134,7 @@ Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } + /* Find the index of the kind with the lowest precedence. */ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) const { Assert( start_index >= 0, "Expected start_index >= 0. "); @@ -145,7 +146,7 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, for(unsigned i = start_index + 1; i <= end_index; ++i) { unsigned current_precedence = getPrecedence(kinds[i]); - if(current_precedence > pivot_precedence) { + if(current_precedence < pivot_precedence) { pivot = i; pivot_precedence = current_precedence; } @@ -154,6 +155,16 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, return pivot; } + /* "Tree-ify" an unparenthesized expression: + e_1 op_1 e_2 op_2 ... e_(n-1) op_(n-1) e_n + represented as a vector of exprs <e_1,e_2,...,e_n> and + kinds <k_1,k_2,...,k_(n-1)>. + + This works by finding the lowest precedence operator op_i, + then recursively tree-ifying lhs = (e1 op_1 ... op_(i-1) e_i), + rhs = (e_(i+1) op_(i+1) ... op_(n-1) e_N), and forming the + expression (lhs op_i rhs). + */ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) { |