<commit_before>%{
  /********************************************************************
   * AUTHORS:  <NAME>
   *
   * BEGIN DATE: May, 2010
   *
   * This file is modified version of the STP's smtlib.lex file. Please
   * see CVCL license below
   ********************************************************************/

  /********************************************************************
   * AUTHORS: <NAME>, <NAME>, <NAME>
   *
   * BEGIN DATE: July, 2006
   *
   * This file is modified version of the CVCL's smtlib.lex file. Please
   * see CVCL license below
   ********************************************************************/
   
  /********************************************************************
   * \file smtlib.lex
   * 
   * Author: <NAME>, <NAME>
   * 
   * Created: Apr 30 2005
   *
   * <hr>
   * Copyright (C) 2004 by the Board of Trustees of Leland Stanford
   * Junior University and by New York University. 
   *
   * License to use, copy, modify, sell and/or distribute this software
   * and its documentation for any purpose is hereby granted without
   * royalty, subject to the terms and conditions defined in the \ref
   * LICENSE file provided with this distribution.  In particular:
   *
   * - The above copyright notice and this permission notice must appear
   * in all copies of the software and related documentation.
   *
   * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
   * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
   * 
   * <hr>
   ********************************************************************/
  // -*- c++ -*-L
#include "parser.h"
#include "parse2SMT_defs.h"
#include "ParserInterface.h"

  extern char *smt2text;
  extern int smt2error (const char *msg);

  // File-static (local to this file) variables and functions
  static std::string _string_lit;  
  static char escapeChar(char c) {
    switch(c) {
    case 'n': return '\n';
    case 't': return '\t';
    default: return c;
    }
  }    
   
  static int lookup(const char* s)
  {
    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(s); 

  // Check valuesize to see if it's a prop var.  I don't like doing
  // type determination in the lexer, but it's easier than rewriting
  // the whole grammar to eliminate the term/formula distinction.  
  smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
  if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
    return FORMID_TOK;
  else 
    return TERMID_TOK;
   }
   
%}

%option noyywrap
%option nounput
%option noreject
%option noyymore
%option yylineno

%x	COMMENT
%x	STRING_LITERAL
%x  SYMBOL

LETTER	([a-zA-Z])
DIGIT	([0-9])
OPCHAR	([~!@$%^&*\_\-+=<>\.?/]) 

ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})

%%<commit_msg>Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol name.<commit_after>%{
  /********************************************************************
   * AUTHORS:  <NAME>
   *
   * BEGIN DATE: May, 2010
   *
   * This file is modified version of the STP's smtlib.lex file. Please
   * see CVCL license below
   ********************************************************************/

  /********************************************************************
   * AUTHORS: <NAME>, <NAME>, <NAME>
   *
   * BEGIN DATE: July, 2006
   *
   * This file is modified version of the CVCL's smtlib.lex file. Please
   * see CVCL license below
   ********************************************************************/
   
  /********************************************************************
   * \file smtlib.lex
   * 
   * Author: <NAME>, <NAME>
   * 
   * Created: Apr 30 2005
   *
   * <hr>
   * Copyright (C) 2004 by the Board of Trustees of Leland Stanford
   * Junior University and by New York University. 
   *
   * License to use, copy, modify, sell and/or distribute this software
   * and its documentation for any purpose is hereby granted without
   * royalty, subject to the terms and conditions defined in the \ref
   * LICENSE file provided with this distribution.  In particular:
   *
   * - The above copyright notice and this permission notice must appear
   * in all copies of the software and related documentation.
   *
   * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
   * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
   * 
   * <hr>
   ********************************************************************/
  // -*- c++ -*-L
#include "parser.h"
#include "parse2SMT_defs.h"
#include "ParserInterface.h"

  extern char *smt2text;
  extern int smt2error (const char *msg);

  // File-static (local to this file) variables and functions
  static std::string _string_lit;  
  static char escapeChar(char c) {
    switch(c) {
    case 'n': return '\n';
    case 't': return '\t';
    default: return c;
    }
  }    
   
  static int lookup(const char* s)
  {
    string str(s);
  
    // The SMTLIB2 specifications sez that the outter bars aren't part of the
    // name. This means that we can create an empty string symbol name.
    if (s[0] == '|' && s[str.size()-1] == '|')
    	str = str.substr(1,str.length()-2);
    
    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(str.c_str()); 

  // Check valuesize to see if it's a prop var.  I don't like doing
  // type determination in the lexer, but it's easier than rewriting
  // the whole grammar to eliminate the term/formula distinction.  
  smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr));
  if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE)
    return FORMID_TOK;
  else 
    return TERMID_TOK;
   }
   
%}

%option noyywrap
%option nounput
%option noreject
%option noyymore
%option yylineno

%x	COMMENT
%x	STRING_LITERAL
%x  SYMBOL

LETTER	([a-zA-Z])
DIGIT	([0-9])
OPCHAR	([~!@$%^&*\_\-+=<>\.?/]) 

ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})

%%
{'fraction_non_alphanumeric': 0.24153846153846154, 'fraction_numerical': 0.009572649572649573, 'mean_word_length': 3.442672741078208, 'pattern_counts': {'":': 0, '<': 21, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4190300', 'n_tokens_mistral': 1882, 'n_tokens_neox': 1754, 'n_words': 579}