如何在 bison 中为 LTL 公式编写无歧义语法

Question

我正在为LTL公式写一个CFG语法，其中原子命题直接用逻辑公式表达。然而，当我尝试为逻辑和 LTL 公式实现括号时，我的语法变得模糊（逻辑公式的括号应该具有更高的优先级）。这是我的语法；当我取消注释 ltl 非终结符中的括号规则时，我遇到了 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...
  ;

Answer 1

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

shift/reduce 冲突与 ltl 生产可以通过两种可能的方式匹配 TLPAREN 有关。第一个是您要添加的规则。另一种是解析器遵循这些非终端：formula -> lexpr -> lterm.

这与解析器的 lookahead 属性有关。下面的 link 是关于前瞻和处理 shift/reduce 冲突的 Bison 文档。

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

Answer 2

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

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

如果您想修复此问题以便无法进行第二次解析，则需要取消分解语法，这样 ltl 就无法扩展为 lterm，而 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）来（滥用）使用 bison 的优先级解析规则。

如果你想更喜欢第二个解析，你不需要做任何事情，因为这是默认更喜欢 shift over reduce 冲突解决会做的。您可以通过为 formula: lexpr 规则指定一个低于 TPAREN

规则的显式优先级来关闭警告消息

如何在 bison 中为 LTL 公式编写无歧义语法

How to write non-ambiguous grammar for LTL formula in bison

parsing

grammar

bison

context-free-grammar