From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Fri, 29 Jan 2010 20:05:46 +0000 (+0000)
Subject: Fixing boolean operator precedences
X-Git-Tag: cvc5-1.0.0~9329
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=483bbf8afabd02482124b5c9330fe5f3052c3221;p=cvc5.git

Fixing boolean operator precedences
---

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) {