SMT公式的Antlr语法

Question

我正在尝试为SMT公式制作语法，这就是我到目前为止的

grammar Z3input;
startRule : formulaList? EOF;
LEFT_PAREN : '(';
RIGHT_PAREN : ')';
COMMA : ',';
SEMICOLON : ';';
PLUS : '+';
MINUS : '-';
TIMES : '*';
DIVIDE : '/';
DIGIT : [0-9];
INTEGER : '0' | [1-9] DIGIT*;
FLOAT : DIGIT+ '.' DIGIT+;
NUMERICAL_LITERAL : FLOAT | INTEGER;
BOOLEAN_LITERAL : 'True' | 'False';
LITERAL : MINUS? NUMERICAL_LITERAL | BOOLEAN_LITERAL;
COMPARISON_OPERATOR : '>' | '<' | '>=' | '<=' | '!=' | '==';
WHITESPACE: [ tnr]+ -> skip;
IDENTIFIER : [a-uw-zB-DF-Z]+ ([a-zA-Z0-9]? [a-uw-zB-DF-Z])*; // omits 'v', 'A', 'E' and cannot end in those characters
IMPLIES : '->' | '-->' | 'implies';
AND : '&' | 'and' | '^';
OR : 'or' | 'v' | '|';
NOT : '~' | '!' | 'not';
QUANTIFIER : 'A' | 'E' | 'forall' | 'exists';
formulaList : formula ( SEMICOLON formula )*; 
argumentList : expression ( COMMA expression )*; 
formula : formulaConjunction 
        | LEFT_PAREN formula RIGHT_PAREN OR LEFT_PAREN formulaConjunction RIGHT_PAREN
        | formula IMPLIES LEFT_PAREN formulaConjunction RIGHT_PAREN;
formulaConjunction : formulaNegation | formulaConjunction AND         formulaNegation;
formulaNegation : formulaAtom | NOT formulaNegation;
formulaAtom : BOOLEAN_LITERAL 
        | IDENTIFIER ( LEFT_PAREN argumentList? RIGHT_PAREN )?
        | QUANTIFIER '.' LEFT_PAREN formulaAtom RIGHT_PAREN
        | compareExpn;
expression : boolConjunction | expression OR boolConjunction;
boolConjunction : boolNegation | boolConjunction AND boolNegation;
boolNegation : compareExpn | NOT boolNegation;
compareExpn : arithExpn COMPARISON_OPERATOR arithExpn;
arithExpn : term | arithExpn PLUS term | arithExpn MINUS term;
term : factor | term TIMES factor | term DIVIDE factor;
factor : primary | MINUS factor;
primary : LITERAL 
        | IDENTIFIER ( LEFT_PAREN argumentList? RIGHT_PAREN )? 
        | LEFT_PAREN expression RIGHT_PAREN;

smt公式是具有函数符号（可以用多个参数调用的标识符），变量，布尔文字（即'true''或'false'或数字文字）的比较）的一阶逻辑公式或变量，与操作员' '，'*'，' - '和'/'的算术。本质上，这些公式在某些签名上是一阶逻辑，出于我的目的，我选择了这个签名作为理论的理论。

我可以正确解释诸如'True ^ True'之类的东西，但包括'True | True'在内的任何更复杂的东西似乎总是会导致

的线

... mismatched input '|' expecting {<EOF>, ';', IMPLIES, AND}

所以我希望在纠正语法方面提供一些帮助。为了记录，我希望将语法运行时独立保持。

Answer 1

您的formula规则似乎在此引起问题：LEFT_PAREN formula RIGHT_PAREN OR LEFT_PAREN formulaConjunction RIGHT_PAREN。

也就是说，只有(FORMULA)|(CONJUNCTIVE)表格的公式将被语言接受。

相反，为每个操作员指定优先规则，并为每个优先级使用非终端。例如，您的语法可能看起来如下：

formula            : (QUANTIFIER IDENTIFIER '.')? formulaImplication;
formulaImplication : formulaConjunction (IMPLIES formula)?;
formulaConjunction : formulaDisjunction (AND formulaConjunction)?;
formulaDisjunction : formulaNegation (OR formulaDisjunction)?;
formulaNegation    : formulaAtom | NOT formulaNegation;
formulaAtom        : BOOLEAN_LITERAL | IDENTIFIER ( LEFT_PAREN argumentList? RIGHT_PAREN )? | LEFT_PAREN formula RIGHT_PAREN | compareExpn;
expression : boolConjunction | expression OR boolConjunction;
boolConjunction : boolNegation | boolConjunction AND boolNegation;
boolNegation : compareExpn | NOT boolNegation;
compareExpn : arithExpn COMPARISON_OPERATOR arithExpn;
arithExpn : term | arithExpn PLUS term | arithExpn MINUS term;
term : factor ((TIMES | DIVIDE) term)?;
factor : primary | MINUS factor;
primary : LITERAL | IDENTIFIER ( LEFT_PAREN argumentList? RIGHT_PAREN )? | LEFT_PAREN expression RIGHT_PAREN;