ANTLR4 Ошибка синтаксического анализатора для мини-грамматики SMTLIB v2 - PullRequest
Новая
       8

ANTLR4 Ошибка синтаксического анализатора для мини-грамматики SMTLIB v2

0 голосов
/ 05 декабря 2018

Моя грамматика SMTLib v2 выглядит следующим образом: 

/**
* Author : Sourav DAS
* Group : Rigorous System Design
* Lab : VERIMAG, IMAG Building, UGA
* Date : 23/11/2018
* A Grammar for syntax, defined for test cases, to be run in Parametric Dead-lock Finder
* Inspired from the complete SMTLibV2 grammar present at 
* https://github.com/antlr/grammars-v4/tree/master/smtlibv2
**/

grammar SyntaxGrammarSMTLibV2;

Colon
    : ':'
    ;

generalReservedWord
    : GenResWrd_Exclamation
    | GenResWrd_Underscore
    | GenResWrd_As
    | GenResWrd_Exists
    | GenResWrd_Forall
    | GenResWrd_Numeral
    | GenResWrd_String
    ;

fragment Digit
    : [0-9]
    ;

fragment Sym
    : 'a'..'z'
    | 'A' .. 'Z'
    | '+'
    | '='
    | '/'
    | '*'
    | '%'
    | '?'
    | '!'
    | '$'
    | '-'
    | '_'
    | '~'
    | '&'
    | '^'
    | '<'
    | '>'
    | '@'
    | '.'
    ;

fragment PrintCharNoDQuote
    : '\u0020' .. '\u0021'
    | '\u0023' .. '\u007E'
    | '\u0080' .. '\uffff'
    | EscapedSpace
    ;

Numeral
    : '0'
    | [1-9] Digit*
    ;

UndefinedSymbol:
    Sym (Digit | Sym)*
    ;

QuotedSymbol:
    '|' (PrintableCharNoBackslash | WhiteSpaceChar)+ '|'
    ;

simpleSymbol
    : UndefinedSymbol
    ;

quotedSymbol
    : QuotedSymbol
    ;

symbol
    : simpleSymbol
    | quotedSymbol
    ;

index
    : Numeral
    | symbol
    ;

ParenthesisOpen
    : '('
    ;

ParenthesisClose
    : ')'
    ;

identifier
    : symbol
    | ParenthesisOpen GenResWrd_Underscore symbol index+ ParenthesisClose
    ;

sort_expr
    : symbol
    | ParenthesisOpen symbol sort_expr+ ParenthesisClose
    ;

// Command names    

CMD_DeclareFun
    : 'declare-fun'
    ;

CMD_DeclareSort
    : 'declare-sort'
    ;

CMD_DefineFun
    : 'define-fun'
    ;

CMD_DefineSort
    : 'define-sort'
    ;

cmd_declareFun
    : CMD_DeclareFun
    ;

cmd_declareSort
    : CMD_DeclareSort
    ;

cmd_defineSort
    : CMD_DefineSort
    ;

cmd_defineFun
    : CMD_DefineFun
    ;

// General reserved words

GenResWrd_Exclamation
    : '!'
    ;

GenResWrd_Underscore
    : '_'
    ;

GenResWrd_As
    : 'as'
    ;

GenResWrd_Numeral
    : 'Numeral'
    ;

GenResWrd_String
    : 'string'
    ;

GenResWrd_Exists
    : 'exists'
    ;

GenResWrd_Forall
    : 'forall'
    ;

fragment EscapedSpace
    : '""'
    ;

fragment PrintableCharNoBackslash
    : '\u0020' .. '\u005B'
    | '\u005D' .. '\u007B'
    | '\u007D' .. '\u007E'
    | '\u0080' .. '\uffff'
    | EscapedSpace
    ;

fragment WhiteSpaceChar
    : '\u0009'
    | '\u000A'
    | '\u000D'
    | '\u0020'
    ;

// Sorts

sort
    : identifier
    | ParenthesisOpen identifier sort+ ParenthesisClose
    ;

sorted_var
    : ParenthesisOpen symbol sort ParenthesisClose
    ;

qualified_identifier
    : identifier
    | ParenthesisOpen GenResWrd_As identifier sort ParenthesisClose
    ;

String
    : '"' (PrintCharNoDQuote | WhiteSpaceChar)+ '"'
    ;

string
    : String
    ;

spec_constant
    : Numeral
    | string
    ;

function_dec
    : ParenthesisOpen symbol ParenthesisOpen sort_expr* ParenthesisClose sort_expr ParenthesisClose
    ;

function_def
    : symbol ParenthesisOpen ParenthesisOpen symbol sort_expr ParenthesisClose* ParenthesisClose sort_expr expr
    ;

s_expr
    : spec_constant
    | symbol
    | keyword
    | ParenthesisOpen s_expr* ParenthesisClose
    ;

keyword
    : Colon simpleSymbol
    ;

// Attributes

attribute_value
    : spec_constant
    | symbol
    | ParenthesisOpen s_expr* ParenthesisClose
    ;

attribute
    : keyword
    | keyword attribute_value
    ;

attributed_expr
    : ParenthesisOpen GenResWrd_Exclamation expr attribute+ ParenthesisClose 
    ;

expr
    : spec_constant
    | identifier
    | qualified_identifier
    | ParenthesisOpen qualified_identifier expr+ ParenthesisClose
    | ParenthesisOpen GenResWrd_Forall ParenthesisOpen ParenthesisOpen symbol sort ParenthesisClose+ ParenthesisClose expr ParenthesisClose
    | ParenthesisOpen GenResWrd_Exists ParenthesisOpen ParenthesisOpen symbol sort ParenthesisClose+ ParenthesisClose expr ParenthesisClose
    | ParenthesisOpen GenResWrd_Exclamation expr attribute+ ParenthesisClose
    ;

model_response
    : ParenthesisOpen CMD_DefineFun function_def ParenthesisClose
    // cardinalities for function_dec and expr have to be n+1
    ParenthesisClose ParenthesisClose
    ;

command
    : ParenthesisOpen cmd_declareFun symbol ParenthesisOpen sort* ParenthesisClose sort ParenthesisClose
    | ParenthesisOpen cmd_declareSort symbol Numeral ParenthesisClose
    | ParenthesisOpen cmd_defineFun function_def ParenthesisClose
    | ParenthesisOpen cmd_defineSort symbol ParenthesisOpen symbol* ParenthesisClose sort ParenthesisClose
    ;

// Parser Rules End

WS  :  [ \t\r\n]+ -> skip
    ;

И мой тестовый пример: 

(declare-fun s0 (Int ) Bool)
(declare-fun s1 (Int ) Bool)
(declare-fun s2 (Int ) Bool)
(declare-fun s3 (Int ) Bool)
(declare-fun s4 (Int ) Bool)
(implies (forall ((i Int)) (and (>= i 0) (<= i 3))) (and (implies (and (s4 i) (s0 (% (+ i 1) 4)) (and (s0 i) (s1 (% (+ i 1) 4)))) (implies (s1 i) (s2 i)) (implies (s1 i) (s4 i)) (implies (s3 i) (s4 i)) (implies (s2 i) (s3 i)))))

Когда я запускаю его с grun, я получаю следующую ошибку: 

> grun SyntaxGrammarSMTLibV2 expr Examples/example6_Mutual_Exclusion_Protocol.smt2 -gui
line 1:21 extraneous input ')' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', String}
line 2:21 extraneous input ')' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', String}
line 3:21 extraneous input ')' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', String}
line 4:21 extraneous input ')' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', String}
line 5:21 extraneous input ')' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', String}
line 6:19 no viable alternative at input '(i'
line 7:0 extraneous input '<EOF>' expecting {Numeral, UndefinedSymbol, QuotedSymbol, '(', ')', String}

Кто-нибудь может мне помочь разобраться с дефектами в моей грамматике?

1 Ответ

0 голосов
/ 05 декабря 2018

Ваше правило expr определено для соответствия одному выражению.Но вводимые вами данные это список команд, за которыми следует выражение.Вы должны либо передать ему одно выражение, либо определить правило, которое соответствует списку команд и выражений, и использовать это правило вместо expr.

. Также обратите внимание, что declare-fun интерпретируется как UndefinedSymbol s.вместо CMD_DeclareFun, потому что UndefinedSymbol стоит первым в грамматике и, таким образом, имеет прецедент.В противном случае вы уже получили бы ошибку в начале строки, сообщающую, что declare-fun не ожидается в начале выражения.

Также, поэтому использование forall или exists isnне сработает, потому что не распознает forall или exists как зарезервированные слова.

Чтобы устранить обе эти проблемы, переместите определение UndefinedSymbol в конец токена.определения (которые, с точки зрения читабельности, должны быть все в одном месте, не смешанные с правилами синтаксического анализатора).

...