使用Python Yacc\Lex作为公式解析器

0 投票
2 回答
3173 浏览
提问于 2025-04-15 16:46

目前我正在使用Python的Yacc/Lex来构建一个公式解析器,目的是把公式字符串转换成一组定义好的操作数。到目前为止,我的进展还算顺利,但在定义解析规则时遇到了一些麻烦,主要是因为括号的模糊性和一些移位/归约错误。

我正在处理的公式的巴科斯-诺尔形式(Backus Naur Form)是

phi ::= p ; !p ; phi_0 & phi_1 ; phi_0 | phi_1 ; AX phi ; AF phi ; AG phi ; AU phi_0 U phi_1.

此外,我还试图允许任意匹配的括号,但这也是导致很多混乱的地方,我在想这些移位/归约错误的来源。对于我正在处理的任务来说,括号的存在是很必要的,因为它们可以强制特定的公式计算,所以我必须解决这个问题。

目前我的解析器是在一个类里面定义的,它通过以下方式构建词法分析器

            tokens = (
            'NEGATION',
            'FUTURE',
            'GLOBAL',
            'NEXT',
            'CONJUNCTION',
            'DISJUNCTION',
            'EQUIVALENCE',
            'IMPLICATION',
            'PROPOSITION',             
            'LPAREN',
            'RPAREN',
            'TRUE',
            'FALSE',
            )

        # regex in order of parsing precedence
        t_NEGATION    = r'[\s]*\![\s]*'
        t_FUTURE      = r'[\s]*AF[\s]*'
        t_GLOBAL      = r'[\s]*AG[\s]*'
        t_NEXT        = r'[\s]*AX[\s]*'
        t_CONJUNCTION = r'[\s]*\&[\s]*'
        t_DISJUNCTION = r'[\s]*\|[\s]*'
        t_EQUIVALENCE = r'[\s]*\<\-\>[\s]*'
        t_IMPLICATION = r'[\s]*[^<]\-\>[\s]*'
        t_LPAREN      = r'[\s]*\([\s]*'
        t_RPAREN      = r'[\s]*\)[\s]*'
        t_PROPOSITION = r'[\s]*[a-z]+[-\w\._]*[\s]*'
        t_TRUE        = r'[\s]*TRUE[\s]*'
        t_FALSE       = r'[\s]*FALSE[\s]*'

        precedence = (
        ('left', 'ASSIGNMENT'),
        ('left', 'NEGATION'),
        ('left', 'GLOBAL','NEXT','FUTURE'),
        ('left', 'CONJUNCTION'), 
        ('left', 'DISJUNCTION'), 
        ('left', 'EQUIVALENCE'),
        ('left', 'IMPLICATION'),   
        ('left', 'AUB', 'AUM'),
        ('left', 'LPAREN', 'RPAREN', 'TRUE', 'FALSE'),
        )            

        lexer = lex.lex()
        lexer.input(formula)

解析规则是

        def p_double_neg_paren(p):
            '''formula : NEGATION LPAREN NEGATION LPAREN PROPOSITION RPAREN RPAREN
            '''
            stack.append(p[5].strip())

        def p_double_neg(p):
            '''formula : NEGATION NEGATION PROPOSITION
            '''
            stack.append(p[3].strip())

        def p_double_neg_inner_paren(p):
            '''formula : NEGATION NEGATION LPAREN PROPOSITION RPAREN
            '''
            stack.append(p[4].strip())

        def p_double_neg_mid_paren(p):
            '''formula : NEGATION LPAREN NEGATION PROPOSITION RPAREN
            '''
            stack.append(p[4].strip())

        def p_groupAssignment(p):
            '''formula : PROPOSITION ASSIGNMENT ASSIGNVAL
            '''
            stack.append(p[1].strip() + p[2].strip() + p[3].strip())

        def p_neg_paren_take_outer_token(p):
            '''formula : NEGATION LPAREN PROPOSITION RPAREN
                       | NEGATION LPAREN TRUE RPAREN
                       | NEGATION LPAREN FALSE RPAREN
            '''
            stack.append(Neg(p[3]))

        def p_neg_take_outer_token(p):
            '''formula : NEGATION PROPOSITION
                       | NEGATION TRUE
                       | NEGATION FALSE
            '''

            stack.append(Neg(p[2].strip()))

        def p_neg_take_outer_token_paren(p):
            '''formula : LPAREN NEGATION PROPOSITION RPAREN
                       | LPAREN NEGATION TRUE RPAREN
                       | LPAREN NEGATION FALSE RPAREN
            '''
            stack.append(Neg(p[3].strip()))

        def p_unary_paren_nest_take_outer_token(p):
            '''formula : GLOBAL LPAREN LPAREN NEGATION formula RPAREN RPAREN
                       | NEXT LPAREN LPAREN NEGATION formula RPAREN RPAREN
                       | FUTURE LPAREN LPAREN NEGATION formula RPAREN RPAREN
            '''
            if len(stack) >= 1:
                if p[1].strip() == 'AG':
                    stack.append(['AG', ['!', stack.pop()]])
                elif p[1].strip() == 'AF':
                    stack.append(['AF', ['!', stack.pop()]])
                elif p[1].strip() == 'AX':    
                    stack.append(['AX', ['!', stack.pop()]])


        def p_unary_paren_take_outer_token(p):
            '''formula : GLOBAL LPAREN formula RPAREN
                       | NEXT LPAREN formula RPAREN
                       | FUTURE LPAREN formula RPAREN
            '''
            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_unary_take_outer_token(p):
            '''formula : GLOBAL formula
                       | NEXT formula
                       | FUTURE formula
            '''

            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_unary_take_outer_token_prop(p):
            '''formula : GLOBAL PROPOSITION
                       | NEXT PROPOSITION
                       | FUTURE PROPOSITION
            '''

            if len(stack) >= 1:
                if p[1].strip() == "AG":
                    stack.append(AG(stack.pop()))
                elif p[1].strip() == "AF":
                    stack.append(AF(stack.pop()))
                elif p[1].strip() == "AX":
                    stack.append(AX(stack.pop()))

        def p_binary_take_outer_token(p):
            '''formula : formula CONJUNCTION formula 
                       | formula DISJUNCTION formula 
                       | formula EQUIVALENCE formula
                       | formula IMPLICATION formula
            '''

            if len(stack) >= 2:
                a, b = stack.pop(), stack.pop()
                if self.IMPLICATION.search(p[2].strip()) and not self.EQUIVALENCE.search(p[2].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[2].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[2].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[2].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_paren_take_outer_token(p):
            '''formula : LPAREN formula RPAREN CONJUNCTION LPAREN formula RPAREN 
                       | LPAREN formula RPAREN DISJUNCTION LPAREN formula RPAREN
                       | LPAREN formula RPAREN EQUIVALENCE LPAREN formula RPAREN 
                       | LPAREN formula RPAREN IMPLICATION LPAREN formula RPAREN
            '''
            if len(stack) >= 2:
                a, b = stack.pop(), stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_lparen_take_outer_token(p):
            '''formula : LPAREN formula RPAREN CONJUNCTION formula 
                       | LPAREN formula RPAREN DISJUNCTION formula
                       | LPAREN formula RPAREN EQUIVALENCE formula 
                       | LPAREN formula RPAREN IMPLICATION formula
            '''
            if len(stack) >= 2:
                a = stack.pop()
                b = stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_binary_rparen_take_outer_token(p):
            '''formula : formula CONJUNCTION LPAREN formula RPAREN 
                       | formula DISJUNCTION LPAREN formula RPAREN
                       | formula EQUIVALENCE LPAREN formula RPAREN 
                       | formula IMPLICATION LPAREN formula RPAREN
            '''
            if len(stack) >= 2:
                a = stack.pop()
                b = stack.pop()
                if self.IMPLICATION.search(p[4].strip()) and not self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(Or(a, Neg(b)))
                elif self.EQUIVALENCE.search(p[4].strip()):
                    stack.append(And(Or(Neg(a), b), Or(Neg(b), a)))
                else:
                    if p[4].strip() == "|":
                        stack.append(Or(b, a))
                    elif p[4].strip() == "&":
                        stack.append(And(b, a))

        def p_proposition_take_token_paren(p):
            '''formula : LPAREN formula RPAREN
            '''
            stack.append(p[2].strip())

        def p_proposition_take_token_atom(p):
            '''formula : LPAREN PROPOSITION RPAREN
            '''
            stack.append(p[2].strip())

        def p_proposition_take_token(p):
            '''formula : PROPOSITION
            '''
            stack.append(p[1].strip())

        def p_true_take_token(p):
            '''formula : TRUE
                       '''
            stack.append(p[1].strip())

        def p_false_take_token(p):
            '''formula : FALSE
                       '''
            stack.append(p[1].strip())

        # Error rule for syntax errors
        def p_error(p):
            print "Syntax error in input!: " + str(p)
            os.system("pause")
            return 0

我发现我的lex/yacc规则有点乱,我为了简洁和整洁去掉了很多调试代码,但有没有人能看出我哪里出错了?我应该把括号的处理移到另一个方法吗,还是可以用我现在的代码来处理?有没有其他方法可以把这些公式字符串处理成预定义的类操作,而不出现所有的移位/归约错误?

抱歉把我的代码问题放到网上,但我真的很需要帮助,因为这个问题困扰了我几个月。谢谢。

2 个回答

2

解析器确实让人头疼,而你的表示法也不简单。要为中缀表示法创建一个解析器,需要一些特定的思维方式。不过,如果这是你系统的核心部分,你总得让它正常工作。我不太清楚你在使用lepl时遇到的困惑,我觉得它的概念和pyparsing挺相似的。为了帮助你,也许我可以给你提供一个pyparsing的入门示例。

你的BNF(巴科斯-诺尔范式)和你的词法分析代码并不完全匹配,因为你的代码中提到了'<->'和'->'这些操作符,还有一个赋值语句,以及一个我猜是小写标识符的命题。我在网上找了找这个语言的参考资料,但没有找到。此外,你也没有提供任何测试用例。所以我只能根据我的理解来猜测你的语言BNF应该是什么样的。

"""
phi ::= p 
        !p 
        phi_0 & phi_1 
        phi_0 | phi_1 
        AX phi 
        AF phi 
        AG phi 
        AU phi_0 U phi_1
"""

from pyparsing import *

LPAR,RPAR = map(Suppress,"()")
NOT = Literal("!")
TRUE = Keyword("TRUE")
FALSE = Keyword("FALSE")
AX, AF, AG, AU, U = map(Keyword, "AX AF AG AU U".split())
AND_OP = "&"
OR_OP = "|"
ident = Word(alphas.lower())

phi = Forward()
p = Optional(NOT) + (TRUE | FALSE | ident | Group(LPAR + phi + RPAR) )
binand = p + ZeroOrMore(AND_OP + p)
binor = binand + ZeroOrMore(OR_OP + binand)
phi << (
    Group(AX + phi) |
    Group(AF + phi) |
    Group(AG + phi) |
    Group(AU + phi + U + phi) |
    binor)

assign = ident + "=" + Group(phi)
equiv = Group(phi) + "<->" + Group(phi)
implicate = Group(phi) + "->" + Group(phi)

statement = assign | equiv | implicate

tests = """\
a=TRUE
b = FALSE
c = !TRUE
d <-> b & !c
AG b & d -> !e""".splitlines()

for t in tests:
    print statement.parseString(t).asList()

输出结果:

['a', '=', ['TRUE']]
['b', '=', ['FALSE']]
['c', '=', ['!', 'TRUE']]
[['d'], '<->', ['b', '&', '!', 'c']]
[[['AG', 'b', '&', 'd']], '->', ['!', 'e']]

Group类帮助将结果结构化成一个类似抽象语法树(AST)的东西。在pyparsing的维基上有很多示例,可以帮助你继续进行。我建议你看看simpleBool.py这个示例,了解如何让解析器生成一个求值器。

2

从小开始!!!无论你最后选择哪个解析库,先尝试做一个简单的二元运算,比如 expr & expr,确保这个能正常工作。然后再添加对 '|' 的支持。这样你就有了两个不同的运算符,足以表示运算的优先级,括号也开始发挥作用了。这个BNF(巴科斯-诺尔范式)看起来大概是这样的:

atom := TRUE | FALSE | '(' expr ')'
and_op := atom '&' atom
or_op := and_op '|' and_op
expr = or_op

你明白这是怎么回事吗?没有明确的“取左括号”、“弹出右括号”之类的操作。先弄清楚你其他运算的优先级,然后再扩展这个递归的中缀表示法解析器来反映这些优先级。但在你把这个最基本的部分搞定之前,千万不要做其他事情。否则,你只是在试图一次解决太多问题。

撰写回答