/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

PARSER FOR SMT-LIB 2.0

We don't care about the logic and theory part of SMT LIB 2.0.
We just need to parse SMT-LIB 2.0 scripts.


Tokens
------

They are defined in smt2_lexer.h:

enum smt2_token {
  // open/close par
  SMT2_TK_LP,
  SMT2_TK_RP,

  // end of stream
  SMT2_TK_EOS,

  // atomic tokens
  SMT2_TK_NUMERAL,
  SMT2_TK_DECIMAL,
  SMT2_TK_HEXADECIMAL,
  SMT2_TK_BINARY,
  SMT2_TK_STRING,
  SMT2_TK_SYMBOL,
  SMT2_TK_QSYMBOL,
  SMT2_TK_KEYWORD,

  // Reserved words
  SMT2_TK_PAR,
  SMT2_TK_NUM,
  SMT2_TK_DEC,
  SMT2_TK_STR,
  SMT2_TK_UNDERSCORE,
  SMT2_TK_BANG,
  SMT2_TK_AS,
  SMT2_TK_LET,
  SMT2_TK_EXISTS,
  SMT2_TK_FORALL,

  // Commands
  SMT2_TK_ASSERT,
  SMT2_TK_CHECK_SAT,
  SMT2_TK_CHECK_SAT_ASSUMING,
  SMT2_TK_CHECK_SAT_ASSUMING_MODEL,
  SMT2_TK_DECLARE_SORT,
  SMT2_TK_DECLARE_CONST,
  SMT2_TK_DECLARE_FUN,
  SMT2_TK_DEFINE_SORT,
  SMT2_TK_DEFINE_CONST,
  SMT2_TK_DEFINE_FUN,
  SMT2_TK_EXIT,
  SMT2_TK_GET_ASSERTIONS,
  SMT2_TK_GET_ASSIGNMENT,
  SMT2_TK_GET_INFO,
  SMT2_TK_GET_MODEL,
  SMT2_TK_GET_OPTION,
  SMT2_TK_GET_PROOF,
  SMT2_TK_GET_UNSAT_CORE,
  SMT2_TK_GET_MODEL_INTERPOLANT,
  SMT2_TK_GET_VALUE,
  SMT2_TK_POP,
  SMT2_TK_PUSH,
  SMT2_TK_SET_LOGIC,
  SMT2_TK_SET_INFO,
  SMT2_TK_SET_OPTION,
  SMT2_TK_ECHO,
  SMT2_TK_RESET,
  SMT2_TK_RESET_ASSERTIONS,

  // Errors
  SMT2_TK_INVALID_STRING,
  SMT2_TK_INVALID_NUMERAL,
  SMT2_TK_INVALID_DECIMAL,
  SMT2_TK_INVALID_HEXADECIMAL,
  SMT2_TK_INVALID_BINARY,
  SMT2_TK_INVALID_SYMBOL,
  SMT2_TK_INVALID_KEYWORD,
  SMT2_TK_ERROR,
}


Grammar (SMT-LIB 2.5, June 28 2015)
----------------------------------------

   <command> ::= 
              ( set-logic <symbol> )
            | ( set-option <option> )
            | ( get-option <keyword> )
            | ( set-info <attribute> )
            | ( get-info <info-flag> )      
            | ( push <numeral> )
            | ( pop <numeral> )
            | ( check-sat )
            | ( check-sat-assuming ( <literal>* ) )
            | ( get-assertions )
            | ( get-assignment )
            | ( get-proof )
            | ( get-unsat-assumptions )
            | ( get-unsat-core )
            | ( get-unsat-model-interpolant )
            | ( exit )
            | ( get-value ( <term>+ ) )
            | ( declare-sort <symbol> <numeral> )
            | ( define-sort <symbol> ( <symbol>* ) <sort> )
            | ( declare-const <symbol> <sort> )
            | ( define-const <symbol> <sotr> <term> )
            | ( declare-fun <symbol> ( <sort>* ) <sort> )
            | ( define-fun <symbol> ( <sorted-var>* ) <sort> <term> )
            | ( assert <term> )
            | ( echo <string> )
            | ( reset )
            | ( reset-assertions )
            | ( check-sat-assuming-model ( <variables>* ) ( <terms>* ))
            | EOS


   <option> ::=
              :diagnostic-output-channel <string>
            | :global-declarations <bool-value>
            | :interactive-mode <bool-value>
            | :print-success <bool-value>
            | :produce-assertions <bool-value>
            | :produce-assignments <bool-value>
            | :produce-models <bool-value>
            | :produce-proofs <bool-value>
            | :produce-unsat-assumptions <bool-value>
            | :produce-unsat-core <bool-value>
            | :produce-unsat-model-interpolants <bool-value>
            | :random-seed <numeral>
            | :regular-output-channel <string>
            | :repoducible-resource-limit <numeral>
            | :verbosity <numeral>
            | <attribute>


   <bool-value> ::= true | false


   <attribute> ::=
              <keyword> 
            | <keyword> <attribute-value>


   <attribute-value> ::=
              <numeral>
            | <decimal>
            | <hexadecimal>
            | <binary>
            | <string>
            | <symbol>
            | ( <s-expr>+ )


   <s-expr> ::=
              <numeral>
            | <decimal>
            | <hexadecimal>
            | <binary>
            | <string>
            | <symbol>
            | <keyword>
            | ( <s-expr>+ )


   <info-flag> :=
              :all-statistics
            | :assertion-stack-levels
            | :authors
            | :error-behavior
            | :name
            | :reason-unknown
            | :version
            | :status
            | <keyword>


   <identifier> ::=
              <symbol>
            | ( _ <symbol> <numeral>+ )

   <sort> ::=
              <identifier>
            | ( <identifier> <sort>+ )


   <sorted-var> ::=   ( <symbol> <sort> )

   <var-binding> :=   ( <symbol> <term> ) 

   <qual-identifier> ::=
              <identifier>
            | (as <identifier> <sort> )

   <term> ::=
              <numeral>
            | <decimal>
            | <hexadecimal>
            | <binary>
            | <string>
            | <qual-identifier>
            | ( <qual-identifier> <term>+ )
            | ( let ( <var-binding>+ ) <term> )
            | ( forall ( <sorted-var>+ ) <term> )
            | ( exists ( <sorted-var>+ ) <term> )
            | ( ! <term> <term-attribute>+ )

   <term-attribute> ::= 
             :named <symbol>
           | :pattern ( <term>+ )
           | <attribute>            

   <literal> ::=
            <symbol>
          | ( not <symbol> )


The EOS part in <command> is non standard but it makes sense to allow it.



We rewrite  the rules  for <term> and  <sort> to remove  the ambiguity
caused by <identifiers>. For example, when we parse a <sort>, we can't
tell whether an opening '(' is for an indexed identifier '( _ <symbol>
...)'  or for a sort constructor '( F ... )'.

Also,  to simplify  term  construction, we  unroll  the definition  of
<identifier> in (as <identifier> <sort>) because <sort> is interpreted
in a different way depending on the context (i.e., whether it's in 

   (as <identifier> <sort>) 
or 

   ((as <identifier> <sort>) <arg1> ... <arg_n>).




The new rules are as follows:

   <sort> ::=
             <symbol>
           | ( _ <symbol> <numeral>+ )
           | ( <symbol> <sort>+ )
           | ( (_ <symbol> <numeral>+ ) <sort>+ )


   <terms> ::=
              <numeral>
            | <decimal>
            | <hexadecimal>
            | <binary>
            | <string>
            | <symbol>
            | (_ <symbol> <numeral>+ )
            | ( as <symbol> <sort> )
            | ( as (_ <symbol> <numeral>+ ) <sort> )
            | ( <symbol> <term>+ )
            | ( ( _ <symbol> <numeral>+ ) <term>+ )
            | ( ( as <symbol> <sort> ) <term>+ )
            | ( ( as (_ <symbol> <numeral>+ ) <sort> ) <term>+ )
            | ( let ( <var-binding>+ ) <term> )
            | ( forall ( <sorted-var>+ ) <term> )
            | ( exists ( <sorted-var>+ ) <term> )
            | ( ! <term> <attribute>+ )


We also rewrite the rules for set-info and set-option to make them consistent:

   <command> ::=
             ...
           | (set-option <keyword> )
           | (set-option <keyword> <attribute-value> )
           | (set-info <keyword> )
           | (set-info <keyword> <attribute-value> )
             ...



Recursive-descent parser
------------------------

See yices_parser.txt for more explanations on this stuff.

NOTE: the non-standard commands get-model, echo, reset are treated
like ordinary symbols, unless thay occur when parsing a command (i.e.,
in state c1).

parse-command:
- initial state = c0
- transition table

c0           (                  c1
             EOS                DONE

c1           assert             c7
             check-sat          c2
             check-sat-assuming c16
             check-sat-assuming-model c17
             declare-sort       c8
             declare-const    c14
             declare-fun        c10
             define-sort        c9
             define-const       c15
             define-fun         c11
             echo               c13
             exit               c2
             get-assertions     c2
             get-assignment     c2
             get-info           c4
             get-model          c2
             get-option         c4
             get-proof          c2
             get-unsat-assumptions   c2
             get-unsat-core     c2
             get-unsat-model-interpolant c2
             get-value          c12
             pop                c3
             push               c3
             set-logic          c5
             set-info           c6
             set-option         c6
             reset              c2
             reset-assertions   c2

c2           )                  DONE

; push/pop
c3           <numeral>          c2

; get-info/get-option
c4           <keyword>          c2

; set-logic
c5           <symbol>           c2

; set-info/set-option
c6           <keyword>          c6a
c6a          )                  DONE
             [attribute-value]  c2

; assert
c7           [term]             c2

; declare-sort
c8           <symbol>           c3

; define-sort
c9           <symbol>           c9a
c9a          (                  c9b
c9b          )                  c9c
             <symbol>           c9b
c9c          [sort]             c2

; declare-fun
c10          <symbol>           c10a
c10a         (                  c10b
c10b         )                  c9c
             [sort]             c10b

; define-fun
c11          <symbol>           c11a
c11a         (                  c11b
c11b         )                  c11c
             (                  c11d
c11c         [sort]             c7
c11d         <symbol>           c11e
c11e         [sort]             c11f
c11f         )                  c11b

; get-value
c12          (                  c12a
c12a         [term]             c12b
c12b         )                  c2
             [term]             c12b

; echo
c13          <string>           c2

; declare-const
c14          <symbol>           c9c

; define-const
c15          <symbol>           c11c

; check-sat-assuming
c16          (                  c16a
c16a         <symbol>           c16a
             (                  c16b
             )                  c2
c16b         not                c16c
c16c         <symbol>           c16d
c16d         )                  c16a

; check-sat-assuming-model
c17          (                  c17a
c17a         <symbol>           c17a
             )                  c17b
c17b         (                  c17c
c17c         [term]             c17c
             )                  c2


parse attribute-value:
- initial state a0
- all built-in symbols must be treated like symbols here

a0           <numeral>          DONE
             <decimal>          DONE
             <hexadecimal>      DONE
             <binary>           DONE
             <string>           DONE
             <symbol>           DONE
             (                  a1

a1           [s-expr]           a1
             )                  DONE


parse s-expression:
- initial state v0
- as above, all built-in symbols must be allowed here

v0           <numeral>          DONE
             <decimal>          DONE
             <hexadecimal>      DONE
             <binary>           DONE
             <string>           DONE
             <symbol>           DONE
             <keyword>          DONE
             (                  v1

v1           [s-expr]           v1
             )                  DONE



parse sort:
- initial state s0

s0           <symbol>           DONE
             (                  s1

s1           _                  s2
             (                  s5
             <symbol>           s9

// after '(_'
s2           <symbol>           s3
s3           <numeral>          s4
s4           )                  DONE
             <numeral>          s4

// after '(('
s5           _                  s6
s6           <symbol>           s7
s7           <numeral>          s8
s8           )                  s9
             <numeral>          s8

// arguments in ( F <sort> ... <sort> )
s9           [sort]             s10
s10          )                  DONE
             [sort]             s10


parse term
- initial state t0

t0           <numeral>          DONE
             <decimal>          DONE
             <hexadecimal>      DONE
             <binary>           DONE
             <string>           DONE
             <symbol>           DONE
             (                  t1

t1           let                t2
             forall             t3
             exists             t3
             !                  t4
             as                 t5           
             (                  t6
             _                  t7
             <symbol>           t8

// after '(let'
t2           (                  t2a
t2a          (                  t2b
t2b          <symbol>           t2c
t2c          [term]             t2d
t2d          )                  t2e
t2e          (                  t2b
             )                  t9

// after '(forall' or '(exists'
t3           (                  t3a
t3a          (                  t3b
t3b          <symbol>           t3c
t3c          [sort]             t3d
t3d          )                  t3e
t3e          (                  t3b
             )                  t9

// after '(!'
t4           [term]             t4a

t4a          <keyword>          t4d      if keyword is :named
             <keyword>          t4e      if keyword is :pattern
             <keyword>          t4b      for all other keywords

t4b          )                  DONE

t4b          <keyword>          t4d      if keyword is :named
             <keyword>          t4e      if keyword is :pattern
             <keyword>          t4b          
             [attribute-value]  t4c

t4c          )                  DONE
             <keyword>          t4d      if keyword is :named
             <keyword>          t4e      if keyword is :pattern
             <keyword>          t4b

// after :named
t4d          <symbol>           t4c

// after :pattern
t4e          (                  t4f
t4f          [term]             t4g
t4g          )                  t4c
             [term]             t4g



// t5: after '(as'
             (                  t5a
             <symbol>           t5e
t5e          _                  t5b
t5b          <symbol>           t5c
t5c          <numeral>          t5d
t5d          <numeral>          t5d
             )                  t5e
t5e          [sort]             t10


// after '(('
t6           as                 t6a
             _                  t6h

// after '((as'
t6a          (                  t6b
             <symbol>           t6f
t6b          _                  t6c
t6c          <numeral>          t6d
t6d          <numeral>          t6e
t6e          <numeral>          t6e
             )                  t6f
t6f          [sort]             t6g
t6g          )                  t8

// after '((_'
t6h          <symbol>           t6i
t6i          <numeral>          t6j
t6j          )                  t8
             <numeral>          t6j

// after '(_'
t7           <symbol>           t7a
t7a          <numeral>          t7b
t7b          )                  DONE
             <numeral>          t7b

// list of arguments in '( F <term> ... <term> )'
// after '( F' has been parsed
t8           [term]             t8a
t8a          )                  DONE
             [term]             t8a

// <term> in '(let (...) <term> )'
//        or '(forall (...) <term> )'
//        or '(exists (...) <term. )'
t9           [term]             t10
t10          )                  DONE




Full table
----------

state        token              action

c0           (                  next; goto c1
             EOS                return

c1           assert         next; push r0; goto t0
             check-sat          next; goto r0
             check-sat-assuming next; goto c16
             check-sat-assuming-model   next; goto c17
             declare-sort       next; goto c8
             declare-const      next; goto c14
             declare-fun        next; goto c10
             define-sort        next; goto c9
             define-const       next; goto c15
             define-fun         next; goto c11
             echo               next; goto c13
             exit               next; goto r0
             get-assertions     next; goto r0
             get-assignment     next; goto r0
             get-info           next; goto c4
             get-model          next; goto r0
             get-option         next; goto c4
             get-proof          next; goto r0
             get-unsat-assumptions     next; goto r0
             get-unsat-core     next; goto r0
             get-unsat-model-interpolant     next; goto r0
             get-value          next; goto c12
             pop                next; goto c3
             push               next; goto c3
             set-logic          next; goto c5
             set-info           next; goto c6
             set-option         next; goto c6
             reset              next; goto r0
             reset-assertions   next; goto r0

// after '(push' or '(pop' or '(declare-sort <symnbl>'
c3           <numeral>          next; goto r0

// after '(get-info' or '(get-option'
c4           <keyword>          next; goto r0

// after '(set-logic'
c5           <symbol>           next; goto r0

// after '(set-info' or '(set-option'
c6           <keyword>          next; goto c6a
c6a          )                  next; return
             ...                push r0; goto a0

// after '(declare-sort'
c8           <symbol>           next; goto c3

// after '(define-sort'
c9           <symbol>           next; goto c9a
c9a          (                  next; goto c9b
c9b          )                  next; push r0; goto s0
             <symbol>           next; goto c9b

// after '(declare-fun'
c10          <symbol>           next; goto c10a
c10a         (                  next; goto c10b
c10b         )                  next; push r0; goto s0
             ...                push c10b; goto s0

// after '(define-fun'
c11          <symbol>           next; goto c11a
c11a         (                  next; goto c11b
c11b         )                  next; push r0; push t0; goto s0
             (                  next; goto c11d
c11d         <symbol>           next; push c11f; goto s0
c11f         )                  eval; next; goto c11b      (evaluate the variable declaration here)

// after '(get-value'
c12          (                  next; push c12b; goto t0
c12b         )                  next; goto r0
             ...                push c12b; goto t0

// after '(echo'
c13          <string>           next; goto r0

// after '(declare-const'
c14          <symbol>           next; push r0; goto s0

// after '(define-const'
c15          <symbol>           next; push r0; push t0; goto s0

// after '(check-sat-assuming'
c16          (                  next; goto c16a
c16a         <symbol>           next; goto c16a
             (                  next; goto c16b
         )                  next; goto r0
c16b         not        next; goto c16c
c16c         <symbol>           next; goto c16d
c61d         )                  next; goto c16a

// after '(check-sat-assuming-model'
c17         (            next; goto c17a
c17a         <symbol>           next; goto c17a
         )            next; goto c17b
c17b         (                  next; push c17c; goto t0
c17c         )                  next; goto r0
                                push c17c; goto t0


// attribute value
a0           <numeral>          next; return
             <decimal>          next; return
             <hexadecimal>      next; return
             <binary>           next; return
             <string>           next; return
             <symbol>           next; return         
             (                  next; goto a1

a1           )                  next; return
             ...                push a1; goto v0

v0           <numeral>          next; return
             <decimal>          next; return
             <hexadecimal>      next; return
             <binary>           next; return
             <string>           next; return
             <symbol>           next; return
             <keyword>          next; return
             (                  next; goto a1

// sorts
s0           <symbol>           next; return
             (                  next; goto s1

s1           _                  next; goto s2
             (                  next; goto s5
             <symbol>           next; push s10; goto s0

// after '(_'
s2           <symbol>           next; goto s3

s3           <numeral>          next; goto s4

s4           )                  next; return
             <numeral>          next; goto s4

// after '(('
s5           _                  next; goto s6

s6           <symbol>           next; goto s7

s7           <numeral>          next; goto s8

s8           )                  next; push s10; goto s0
             <numeral>          next; goto s8

// arguments to ( F <sort> ... <sort> )
s10          )                  next; return
             ...                push s10; goto s0


t0           <numeral>          next; return
             <decimal>          next; return
             <hexadecimal>      next; return
             <binary>           next; return
             <string>           next; return
             <symbol>           next; return
             (                  next; goto t1

t1           let                next; goto t2
             forall             next; goto t3
             exists             next; goto t3
             !                  next; push t4a; goto t0
             as                 next; goto t5
             (                  next; goto t6
             _                  next; goto t7
             <symbol>           next; push t8a; goto t0

// after '(let'
t2           (                  next; goto t2a // start bind

t2a          (                  next; goto t2b

t2b          <symbol>           next; push t2d; goto t0

t2d          )                  next; goto t2e

t2e          (                  next; goto t2b
             )                  next; push r0; goto t0 // end bind

// after '(exists' or '(forall'
t3           (                  next; goto t3a

t3a          (                  next; goto t3b

t3b          <symbol>           next; push t3d; goto s0

t3d          )                  next; goto t3e

t3e          (                  next; goto t3b
             )                  next; push r0; goto t0

// after '(! <term>'
t4a          <keyword>          check_keyword_then_branch 

t4b          )                  next; return
             <keyword>          check_keyword_then_branch
             ...                push t4c; goto a0

t4c          )                  next; return
             <keyword>          check_keyword_then_branch

t4d          <symbol>           next; goto t4c

t4e          (                  next; push t4g; goto t0
t4g          )                  next; goto t4c
             ...                push t4g; goto t0


We need a special action 'check_keyword_then_branch' to 
parse the  :named  and  :pattern  attributes.

if (keyword == ':named') then  
  next; goto t4d
elsif (keyword == ':pattern') then
  next; goto t4e
else
  next; goto t4b
endif


// after '(as'
t5           (                  next; goto t5a
             <symbol>           next; push r0; goto s0

t5a          _                  next; goto t5b

t5b          <symbol>           next; goto t5c

t5c          <numeral>          next; goto t5d

t5d          <numeral>          next; goto t5d
             )                  next; push r0; goto s0


// after '(('
t6           as                 next; goto t6a
             _                  next; goto t6h

// after '((as'
t6a          (                  next; goto t6b
             <symbol>           next; push t6g; goto s0

t6b          _                  next; goto t6c

t6c          <symbol>           next; goto t6d

t6d          <numeral>          next; goto t6e

t6e          <numeral>          next; goto t6e
             )                  next; push t6g; goto s0

t6g          )                  next; push t8a; goto t0

// after '((_'
t6h          <symbol>           next; goto t6i

t6i          <numeral>          next; goto t6j

t6j          <numeral>          next; goto t6j
             )                  next; push t8a; goto t0


// after '(_'
t7           <symbol>           next; goto t7a

t7a          <numeral>          next; goto t7b

t7b          )                  next; return
             <numeral>          next; goto t7b


// arguments
t8a          )                  next; return
             ...                push t8a; goto t0




r0           )                  next; return