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: [ \t\n\r]+ -> 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 ^ 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;