/*
 * 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/>.
 */

/*
 * Lexer for Yices language with support for EF-solver
 * - separators are ( ) : and spaces
 *
 * - strings are delimited by " with escaped char \n, \t, etc. allowed
 *
 * - two kinds of numeric literals are recognized
 *     TK_NUM_RATIONAL:  <optional_sign><digits>/<digits>
 *                    or <optional_sign><digits>
 *     TK_NUM_FLOAT:
 *       <optional_sign> <digits> . <digits>
 *       <optional_sign> <digits> <exp> <optional_sign> <digits>
 *       <optional_sign> <digits> . <digits> <exp> <optional_sign> <digits>
 *
 *   (the two formats recognized by string-to-rational conversions in rational.c)
 *
 * - bit-vector literals are written 0b<binary digits> (cf. bv_constants.c)
 *   or 0x<hexa digits>
 *
 * - comments start with ; and extend to the end of the line
 *
 * 2013/12/12: added ef-solve token
 * 2014/03: added export-to-dimancs and show-implicants
 */

#ifndef __YICES_LEXER_H
#define __YICES_LEXER_H

#include "parser_utils/lexer.h"


/*
 * Tokens
 */
enum yices_token {
  // commands
  TK_DEFINE_TYPE, TK_DEFINE, TK_ASSERT, TK_CHECK, TK_CHECK_ASSUMING,
  TK_PUSH, TK_POP, TK_RESET, TK_DUMP_CONTEXT, TK_EXIT,
  TK_ECHO, TK_INCLUDE, TK_SHOW_MODEL, TK_EVAL, TK_SET_PARAM,
  TK_SHOW_PARAM, TK_SHOW_PARAMS, TK_SHOW_STATS, TK_RESET_STATS,
  TK_SET_TIMEOUT, TK_SHOW_TIMEOUT, TK_HELP, TK_EF_SOLVE,
  TK_EXPORT_TO_DIMACS, TK_SHOW_IMPLICANT,
  TK_SHOW_UNSAT_CORE, TK_SHOW_UNSAT_ASSUMPTIONS,
  TK_SHOW_REDUCED_MODEL,

  // term constructors
  TK_UPDATE, TK_FORALL, TK_EXISTS, TK_LAMBDA, TK_LET,

  // separators and end-of-stream
  TK_LP, TK_RP, TK_COLON_COLON, TK_EOS,

  // literals
  TK_STRING, TK_NUM_RATIONAL, TK_NUM_FLOAT, TK_BV_CONSTANT, TK_HEX_CONSTANT,

  // any symbol that's not a keyword
  TK_SYMBOL,

  // type keywords
  TK_BOOL, TK_INT, TK_REAL, TK_BITVECTOR, TK_SCALAR, TK_TUPLE, TK_ARROW,

  // term keywords
  TK_TRUE, TK_FALSE, TK_IF, TK_ITE, TK_EQ, TK_DISEQ, TK_DISTINCT,
  TK_OR, TK_AND, TK_NOT, TK_XOR, TK_IFF, TK_IMPLIES, TK_MK_TUPLE,
  TK_SELECT, TK_UPDATE_TUPLE,

  // arithmetic keywords
  TK_ADD, TK_SUB, TK_MUL, TK_DIV, TK_POW, TK_LT, TK_LE, TK_GT, TK_GE,

  // bitvector keywords
  TK_MK_BV, TK_BV_ADD, TK_BV_SUB, TK_BV_MUL, TK_BV_NEG, TK_BV_POW,
  TK_BV_NOT, TK_BV_AND, TK_BV_OR, TK_BV_XOR, TK_BV_NAND, TK_BV_NOR, TK_BV_XNOR,

  TK_BV_SHIFT_LEFT0, TK_BV_SHIFT_LEFT1, TK_BV_SHIFT_RIGHT0,
  TK_BV_SHIFT_RIGHT1, TK_BV_ASHIFT_RIGHT, TK_BV_ROTATE_LEFT, TK_BV_ROTATE_RIGHT,
  TK_BV_EXTRACT, TK_BV_CONCAT, TK_BV_REPEAT,
  TK_BV_SIGN_EXTEND, TK_BV_ZERO_EXTEND,
  TK_BV_GE, TK_BV_GT, TK_BV_LE, TK_BV_LT,
  TK_BV_SGE, TK_BV_SGT, TK_BV_SLE, TK_BV_SLT,

  // more bitvector operators
  TK_BV_SHL, TK_BV_LSHR, TK_BV_ASHR,
  TK_BV_DIV, TK_BV_REM, TK_BV_SDIV, TK_BV_SREM, TK_BV_SMOD,
  TK_BV_REDOR, TK_BV_REDAND, TK_BV_COMP,

  // conversions between bitvectors and Booleans
  TK_BOOL_TO_BV, TK_BIT,

  // more arithmetic functions (inherited from SMT-LIB2 Ints theory)
  TK_FLOOR, TK_CEIL, TK_ABS, TK_IDIV, TK_MOD, TK_DIVIDES, TK_IS_INT, 

  // unrecognized tokens or other errors
  TK_OPEN_STRING, TK_EMPTY_BVCONST, TK_EMPTY_HEXCONST,
  TK_INVALID_NUM, TK_ZERO_DIVISOR, TK_ERROR,
};

#define NUM_YICES_TOKENS (TK_ERROR+1)

typedef enum yices_token yices_token_t;


/*
 * Lexer initialization:
 * - for file_lexer, return code 0 means OK, negative code means error
 *   (can't open the file).
 */
extern int32_t init_yices_file_lexer(lexer_t *lex, char *filename);

extern void init_yices_stream_lexer(lexer_t *lex, FILE *f, char *name);

static inline void init_yices_stdin_lexer(lexer_t *lex) {
  init_yices_stream_lexer(lex, stdin, "stdin");
}

extern void init_yices_string_lexer(lexer_t *lex, char *data, char *name);



/*
 * Conversion from a token type to a string.
 * The internal table is initialized by one of the
 * init_yices_lexer functions. This function should not be
 * called before the init function.
 */
extern char *yices_token_to_string(yices_token_t tk);


/*
 * Read next token and return its type tk
 * - set lex->token to tk
 * - set lex->tk_pos, etc.
 * - if token is TK_STRING, TK_NUM_RATIONAL, TK_NUM_FLOAT,
 *   TK_BV_CONSTANT, TK_SYMBOL, or TK_ERROR,
 * the token value is set in lex->buffer.
 */
extern yices_token_t next_yices_token(lexer_t *lex);




#endif /* __YICE_LEXER_H */