[SMT-LIB] OCaml parser for SMT-LIB 2.0

[Cesare Tinelli]

On 30 Aug 2010, at 11:35, Aaron Stump wrote:

> Dear SMT-LIB community,
> 
> We are contributing an OCaml parser for SMT-LIB 2.0, which Kyle implemented
> as part of an undergraduate research project this summer at Iowa with Aaron.
> The parser builds ASTs, and is generated from a high-level declarative
> specification, included below and in the distribution.  You can download the
> parser from:
> 
> http://www.cs.uiowa.edu/~astump/software/ocaml-smt2.zip
> 
A link to this parser has also been added in the Utilities section of 
www.smtlib.org


Cesare



> Cesare has looked through our grammar, and at this point, we believe it is
> conformant to the SMT-LIB 2.0 standard.  That said, please let us know if
> you find any bugs.
> 
> Thanks,
> Aaron Stump and Kyle Krchak
> The University of Iowa
> -------------------------------------------------------------------------------------------------------
> smtlib
> 
> line_comment = ";"
> 
> Commands : commands -> { command }*
> 
> CommandSetLogic : command -> LPAREN SETLOGIC symbol RPAREN
> CommandSetOption : command -> LPAREN SETOPTION an_option RPAREN
> CommandSetInfo : command -> LPAREN SETINFO attribute RPAREN
> CommandDeclareSort : command -> LPAREN DECLARESORT symbol NUMERAL RPAREN
> CommandDefineSort : command -> LPAREN DEFINESORT symbol LPAREN { symbol }*
> RPAREN sort RPAREN
> CommandDeclareFun : command -> LPAREN DECLAREFUN symbol LPAREN { sort }*
> RPAREN sort RPAREN
> CommandDefineFun : command -> LPAREN DEFINEFUN symbol LPAREN { sortedvar }*
> RPAREN sort term RPAREN
> CommandPush : command -> LPAREN PUSH NUMERAL RPAREN
> CommandPop : command -> LPAREN POP NUMERAL RPAREN
> CommandAssert : command -> LPAREN ASSERT term RPAREN
> CommandCheckSat : command -> LPAREN CHECKSAT RPAREN
> CommandGetAssert : command -> LPAREN GETASSERT RPAREN
> CommandGetProof : command -> LPAREN GETPROOF RPAREN
> CommandGetUnsatCore : command -> LPAREN GETUNSATCORE RPAREN
> CommandGetValue : command -> LPAREN GETVALUE LPAREN { term }+ RPAREN RPAREN
> CommandGetAssign : command -> LPAREN GETASSIGN RPAREN
> CommandGetOption : command -> LPAREN GETOPTION KEYWORD RPAREN
> CommandGetInfo : command -> LPAREN GETINFO infoflag RPAREN
> CommandExit : command -> LPAREN EXIT RPAREN
> 
> Symbol : symbol -> SYMBOL
> SymbolWithOr : symbol -> ASCIIWOR
> 
> VarBindingSymTerm : varbinding -> LPAREN symbol term RPAREN
> 
> SortIdentifier : sort -> identifier
> SortIdSortMulti : sort -> LPAREN identifier { sort }+ RPAREN
> 
> SortedVarSymSort : sortedvar -> LPAREN symbol sort RPAREN
> 
> TermSpecConst : term -> specconstant
> TermQualIdentifier : term -> qualidentifier
> TermQualIdTerm : term -> LPAREN qualidentifier { term }+ RPAREN
> TermLetTerm : term -> LPAREN LET LPAREN { varbinding }+ RPAREN term RPAREN
> TermForAllTerm : term -> LPAREN FORALL LPAREN { sortedvar }+ RPAREN term
> RPAREN
> TermExistsTerm : term -> LPAREN EXISTS LPAREN { sortedvar }+ RPAREN term
> RPAREN
> TermExclimationPt : term -> LPAREN EXCLIMATIONPT term { attribute }+ RPAREN
> 
> QualIdentifierId : qualidentifier -> identifier
> QualIdentifierAs : qualidentifier -> LPAREN AS identifier sort RPAREN
> 
> IdSymbol : identifier -> symbol
> IdUnderscoreSymNum : identifier -> LPAREN UNDERSCORE symbol { NUMERAL }+
> RPAREN
> 
> InfoFlagKeyword : infoflag -> KEYWORD
> AnOptionAttribute : an_option -> attribute
> 
> AttributeKeyword : attribute -> KEYWORD
> AttributeKeywordValue : attribute -> KEYWORD attributevalue
> AttributeValSpecConst : attributevalue -> specconstant
> AttributeValSymbol : attributevalue -> symbol
> AttributeValSexpr : attributevalue -> LPAREN { sexpr }* RPAREN
> 
> SexprSpecConst : sexpr -> specconstant
> SexprSymbol : sexpr -> symbol
> SexprKeyword : sexpr -> KEYWORD
> SexprInParen : sexpr -> LPAREN { sexpr }* RPAREN
> 
> SpecConstsDec : specconstant -> DECIMAL
> SpecConstNum : specconstant -> NUMERAL
> SpecConstString : specconstant -> STRINGLIT
> SpecConstsHex : specconstant -> HEXADECIMAL
> SpecConstsBinary : specconstant -> BINARY
> 
> 
> 
> UNDERSCORE = "_"
> LPAREN = "("
> RPAREN = ")"
> AS = "as"
> LET = "let"
> FORALL = "forall"
> EXISTS = "exists"
> EXCLIMATIONPT = "!"
> SETLOGIC = "set-logic"
> SETOPTION = "set-option"
> SETINFO = "set-info"
> DECLARESORT = "declare-sort"
> DEFINESORT = "define-sort"
> DECLAREFUN = "declare-fun"
> DEFINEFUN = "define-fun"
> PUSH = "push"
> POP = "pop"
> ASSERT = "assert"
> CHECKSAT = "check-sat"
> GETASSERT = "get-assertions"
> GETPROOF = "get-proof"
> GETUNSATCORE = "get-unsat-core"
> GETVALUE = "get-value"
> GETASSIGN = "get-assignment"
> GETOPTION = "get-option"
> GETINFO = "get-info"
> EXIT = "exit"
> 
> 
> HEXADECIMAL = {{ '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+ }}
> 
> BINARY = {{ '#' 'b' ['0'-'1']+ }}
> 
> ASCIIWOR = {{ '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|' }}
> 
> KEYWORD = {{ ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!'
> '.' '$' '_' '~' '&' '^' '<' '>' '@']+ }}
> 
> SYMBOL = {{ ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~'
> '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!'
> '.' '$' '_' '~' '&' '^' '<' '>' '@']* }}
> 
> STRINGLIT = {{ '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\'
> ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"'}}
> 
> NUMERAL = {{ ( '0' | ['1'-'9'] ['0'-'9']* ) }}
> 
> DECIMAL = {{ ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+}}
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib