如何在野牛中为LTL公式编写非歧义语法答案

【问题标题】：How to write non-ambiguous grammar for LTL formula in bison如何在野牛中为LTL公式编写非歧义语法
【发布时间】：2015-05-02 19:18:41
【问题描述】：

我正在为LTL公式编写CFG语法，其中原子命题直接由逻辑公式表示。但是，当我尝试为逻辑和 LTL 公式实现括号时，我的语法变得模糊不清（逻辑公式的括号应该具有更高的优先级）。这是我的语法；当我取消注释 ltl nonterminal 中的括号规则时，我遇到了 shift/reduce 冲突。如何解决？

%left TPLUS TMINUS
%left TMUL TDIV
%left TAND TOR TIMP
%left TRSHIFT TLSHIFT
%left TEQUAL TCNE TCGE TCGT TCLE TCLT
%left TUNTIL TWEAK TFUT TGLOB TREL TNEG

%start ltlformula

%%

ltlformula
  : ltl   {}

formula
  : lexpr  {}
  ;

lterm
  : TLPAREN lexpr TRPAREN         {}
  | arexpr binary_la_oper arexpr  {}
  ;

lnterm
  : lterm      {}
  | TNEG lnterm {}
  ;

lexpr
  : lterm                         {}
  | lexpr binary_ll_oper lnterm    {}
  ;

ltl
  : formula               {}
  | TFUT ltl              {}
  | TGLOB ltl             {}
  | ltl TUNTIL ltl        {}
  | ltl TREL ltl          {}
  | ltl TWEAK ltl         {}
  | TNEG ltl              {}
//  | TLPAREN ltl TRPAREN   { } - here comes the trouble...
  ;

【问题讨论】：

标签： parsing grammar bison context-free-grammar

【解决方案1】：

基本问题是ltl 可以通过两种方式匹配带括号的lexpr：

            ltl                          ltl
          /  |  \                         |
   TLPAREN  ltl  TRPAREN               formula
             |                            |
          formula                       lexpr
             |                            |
           lexpr                        lterm
                                      /   |   \
                               TLPAREN  lexpr  TRPAREN

如果您想解决此问题，以便无法进行第二次解析，则需要取消语法分解，以便 ltl 无法扩展为扩展为括号表达式的 lterm。这涉及拆分（复制）沿该路径的所有规则：

ltl: formula_no_paren
   |  ..other ltl rules

formula_no_paren: lexpr_no_paren ;

lexpr_no_paren
    : lterm_no_paren
    |  ... all other lterm rules

lterm_no_paren:  ... all lterm rules that don't start with TLPAREN

然后您可以重构其他规则以使用这些 no_paren 规则以避免重复所有操作：

lterm_paren : TLPAREN lexpr TRPAREN ;
lterm : lterm_paren | lterm_no_paren ;

lexpr_paren : lterm_paren ;
lexpr : lexpr_paren | lexpr_no_paren ;

您可以通过首先摆脱无用的formula 规则来简化这一点。

或者，您可以通过为formula: lexpr 规则赋予高于TRPAREN 优先级的显式优先级（使用%prec）来（ab）使用bison 的优先级解析规则。

如果你想更喜欢第二个解析，你不需要做任何事情，因为这是默认的更喜欢 shift 而不是 reduce 冲突解决方案。您可以通过为formula: lexpr 规则指定低于TPAREN 优先级的显式优先级来关闭警告消息

【讨论】：

感谢您的回答。我看到了语法模棱两可的原因，但是我想避免“代码重复”。我在使用 bison 的 %prec 运算符时遇到问题 - 我在文档中研究过它，但我并不真正了解它的作用和使用方法。能给个小提示吗？

【解决方案2】：

我没有用过 Bison，所以我的回答是基于我对解析的一般知识。

移位/减少冲突与ltl 产生式可以通过两种可能的方式匹配TLPAREN 有关。第一个是您尝试添加的规则。另一种是解析器遵循这些非终结符：formula -> lexpr -> lterm。

这与解析器的 lookahead 属性有关。下面的链接指向 Bison 文档，其中涉及前瞻和处理移位/减少冲突。

http://www.gnu.org/software/bison/manual/bison.html#Lookahead

【讨论】：