fix yyscan_t not defined issue

CMakeLists.txt

@@ -0,0 +1,101 @@
+cmake_minimum_required(VERSION 3.8)
+
+project(smtparser VERSION 1.0 LANGUAGES C)
+
+option(SMT_PARSER_BUILD_DOCS "Build documents." OFF)
+option(SMT_PARSER_EXPORT_PACAKGE "Export package if enabled." OFF)
+option(SMT_PARSER_BUILD_YICES "Build Yices if enabled." OFF)
+
+# ------------------------------------------------------------------------
+set(SMT_PARSER_TARGET_NAME                 ${PROJECT_NAME})
+set(SMT_PARSER_CONFIG_INSTALL_DIR          "lib/cmake/${PROJECT_NAME}" CACHE INTERNAL "")
+set(SMT_PARSER_INCLUDE_INSTALL_DIR         "include")
+set(SMT_PARSER_INCLUDE_BUILD_DIR           "${PROJECT_SOURCE_DIR}/include")
+set(SMT_PARSER_TARGETS_EXPORT_NAME         "${PROJECT_NAME}Targets")
+set(SMT_PARSER_CMAKE_CONFIG_TEMPLATE       "cmake/config.cmake.in")
+set(SMT_PARSER_CMAKE_CONFIG_DIR            "${CMAKE_CURRENT_BINARY_DIR}")
+set(SMT_PARSER_CMAKE_VERSION_CONFIG_FILE   "${SMT_PARSER_CMAKE_CONFIG_DIR}/${PROJECT_NAME}ConfigVersion.camke")
+set(SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE   "${SMT_PARSER_CMAKE_CONFIG_DIR}/${PROJECT_NAME}Config.cmake")
+set(SMT_PARSER_CMAKE_PROJECT_TARGETS_FILE  "${PROJECT_NAME}Targets.cmake")
+
+
+# ------------------------------------------------------------------------
+
+set(LIBRARY_NAME ${PROJECT_NAME}) 
+
+add_subdirectory(./src)
+
+# ------------------------------------------------------------------------
+# Add FindGMP
+
+set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/")
+
+# ------------------------------------------------------------------------
+# install
+
+include(CMakePackageConfigHelpers)
+write_basic_package_version_file(
+  ${SMT_PARSER_CMAKE_VERSION_CONFIG_FILE}
+  COMPATIBILITY AnyNewerVersion
+)
+
+configure_file(
+  ${SMT_PARSER_CMAKE_CONFIG_TEMPLATE}
+  ${SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE}
+  @ONLY
+)
+
+install(
+  FILES ${SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE} ${SMT_PARSER_CMAKE_VERSION_CONFIG_FILE}
+  DESTINATION ${SMT_PARSER_CONFIG_INSTALL_DIR}
+)
+
+
+
+if (SMT_PARSER_BUILD_YICES) 
+
+  install(
+    EXPORT ${SMT_PARSER_TARGETS_EXPORT_NAME}
+    DESTINATION ${SMT_PARSER_CONFIG_INSTALL_DIR}
+    NAMESPACE ${PROJECT_NAME}::
+    FILE ${SMT_PARSER_PROJECT_TARGETS_FILE}
+  )
+
+else ()
+
+  message (STATUS "Not building Yices.")
+
+endif ()
+
+export(
+  TARGETS ${LIBRARY_NAME}
+  NAMESPACE ${PROJECT_NAME}::
+  FILE ${SMT_PARSER_CMAKE_PROJECT_TARGETS_FILE}
+)
+
+if(${SMT_PARSER_EXPORT_PACKAGE})
+  export(PACKAGE ${PROJECT_NAME})
+endif()
+
+
+# ---------------------------------------------------------------------------- #
+# UNINSTALL
+# uninstall files listed in install_manifest.txt
+# ---------------------------------------------------------------------------- #
+if(NOT TARGET uninstall)
+  configure_file(
+    "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
+    "${CMAKE_CURRENT_BINARY_DIR}/cmake/cmake_uninstall.cmake"
+    IMMEDIATE @ONLY
+  )
+
+  add_custom_target(uninstall
+    COMMAND 
+      ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_BINARY_DIR}/cmake/cmake_uninstall.cmake
+  )
+
+endif()
+
+
+# ------------------------------------------------------------------------
+

cmake/Modules/FindGMP.cmake

@@ -0,0 +1,64 @@
+# Tries to find an install of the GNU multiple precision library
+#
+# Once done this will define
+#  GMP_FOUND - BOOL: System has the GMP library installed
+#  GMP_INCLUDE_DIRS - LIST:The GMP include directories
+#  GMP_C_LIBRARIES - LIST:The libraries needed to use GMP via it's C interface
+#  GMP_CXX_LIBRARIES - LIST:The libraries needed to use GMP via it's C++ interface
+
+include(FindPackageHandleStandardArgs)
+
+# Try to find libraries
+find_library(GMP_C_LIBRARIES
+  NAMES gmp
+  DOC "GMP C libraries"
+)
+if (GMP_C_LIBRARIES)
+  message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C library")
+endif()
+find_library(GMP_CXX_LIBRARIES
+  NAMES gmpxx
+  DOC "GMP C++ libraries"
+)
+if (GMP_CXX_LIBRARIES)
+  message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C++ library")
+endif()
+
+# Try to find headers
+find_path(GMP_C_INCLUDES
+  NAMES gmp.h
+  DOC "GMP C header"
+)
+if (GMP_C_INCLUDES)
+  message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C include path")
+endif()
+
+find_path(GMP_CXX_INCLUDES
+  NAMES gmpxx.h
+  DOC "GMP C++ header"
+)
+if (GMP_CXX_INCLUDES)
+  message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C++ include path")
+endif()
+
+if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES)
+  set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
+  list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
+  message(STATUS "Found GMP")
+else()
+  message(STATUS "Could not find GMP")
+endif()
+
+# TODO: We should check we can link some simple code against libgmp and libgmpxx
+
+# Handle QUIET and REQUIRED and check the necessary variables were set and if so
+# set ``GMP_FOUND``
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES)

cmake/cmake_uninstall.cmake.in

@@ -0,0 +1,23 @@
+# uninstall targets
+if(NOT EXISTS "@CMAKE_BINARY_DIR@/install_manifest.txt")
+  message(FATAL_ERROR "Cannot find install manifest: @CMAKE_BINARY_DIR@/install_manifest.txt")
+endif(NOT EXISTS "@CMAKE_BINARY_DIR@/install_manifest.txt")
+
+file(READ "@CMAKE_BINARY_DIR@/install_manifest.txt" files)
+string(REGEX REPLACE "\n" ";" files "${files}")
+foreach(file ${files})
+  message(STATUS "Uninstalling $ENV{DESTDIR}${file}")
+  if(IS_SYMLINK "$ENV{DESTDIR}${file}" OR EXISTS "$ENV{DESTDIR}${file}")
+    exec_program(
+      "@CMAKE_COMMAND@" ARGS "-E remove \"$ENV{DESTDIR}${file}\""
+      OUTPUT_VARIABLE rm_out
+      RETURN_VALUE rm_retval
+      )
+    if(NOT "${rm_retval}" STREQUAL 0)
+      message(FATAL_ERROR "Problem when removing $ENV{DESTDIR}${file}")
+    endif(NOT "${rm_retval}" STREQUAL 0)
+  else(IS_SYMLINK "$ENV{DESTDIR}${file}" OR EXISTS "$ENV{DESTDIR}${file}")
+    message(STATUS "File $ENV{DESTDIR}${file} does not exist.")
+  endif(IS_SYMLINK "$ENV{DESTDIR}${file}" OR EXISTS "$ENV{DESTDIR}${file}")
+endforeach(file)
+

cmake/config.cmake.in

@@ -0,0 +1,23 @@
+# ---------------------------------------------------------------------------- #
+
+include(FindPackageHandleStandardArgs)
+
+set(${CMAKE_FIND_PACKAGE_NAME}_CONFIG ${CMAKE_CURRENT_LIST_FILE})
+
+find_package_handle_standard_args(@PROJECT_NAME@ CONFIG_MODE)
+
+if(NOT TARGET @PROJECT_NAME@::@VCD_PARSER_TARGET_NAME@) 
+
+  include("${CMAKE_CURRENT_LIST_DIR}/@VCD_PARSER_TARGETS_EXPORT_NAME@.cmake")
+
+  if((NOT TARGET @VCD_PARSER_TARGET_NAME@) AND 
+     (NOT @PROJECT_NAME@_FIND_VERSION OR @PROJECT_NAME@_FIND_VERSION VERSION_LESS 1.0.0))
+
+    add_library(@VCD_PARSER_TARGET_NAME@ INTERFACE IMPORTED)
+    set_target_properties(@VCD_PARSER_TARGET_NAME@ PROPERTIES
+      INTERFACE_LINK_LIBRARIES @PROJECT_NAME@::@VCD_PARSER_TARGET_NAME@
+    )
+
+  endif()
+
+endif()

src/CMakeLists.txt

@@ -0,0 +1,139 @@
+message(STATUS "Build Type: ${CMAKE_BUILD_TYPE}")
+
+#set(LIBRARY_NAME    smtparser)
+
+FIND_PACKAGE(BISON 3.0.4 REQUIRED)
+FIND_PACKAGE(FLEX 2.5.35 REQUIRED)
+
+set(SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR})
+set(BINARY_DIR ${CMAKE_CURRENT_BINARY_DIR})
+
+set(FLEX_INPUT  smtlib2flexlexer.l)
+set(FLEX_OUTPUT smtlib2flexlexer.c)
+set(FLEX_HEADER smtlib2flexlexer.h)
+
+set(BISON_INPUT  smtlib2bisonparser.y)
+set(BISON_OUTPUT smtlib2bisonparser.c)
+set(BISON_HEADER smtlib2bisonparser.h)
+
+# ------------------------------------------------------------------------
+
+option(WITH_COVERAGE "If YES, build the debug executable with coverage." NO)
+
+SET(COV_FLAGS_C     "-fprofile-arcs -ftest-coverage")
+SET(COV_FLAGS_LINK  "-fprofile-arcs -ftest-coverage")
+
+# ------------------------------------------------------------------------
+
+if(${WITH_COVERAGE})
+
+  message(STATUS "Building with coverage flags set.")
+  SET(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} ${COV_FLAGS_C} -DVERILOG_PARSER_COVERAGE_ON")
+  SET(CMAKE_EXE_LINKER_FLAGS_DEBUG "${CMAKE_C_FLAGS_RELEASE} ${COV_FLAGS_LINK}")
+
+else()
+
+  message(STATUS "NOT building with coverage.")
+
+endif()
+
+# ------------------------------------------------------------------------
+
+
+message(STATUS "Parser Build Flags Debug:   ${CMAKE_C_FLAGS_DEBUG}")
+message(STATUS "Parser Link Flags Debug:   ${CMAKE_EXE_LINKER_FLAGS_DEBUG}")
+message(STATUS "Parser Build Flags Release: ${CMAKE_C_FLAGS_RELEASE}")
+message(STATUS "Parser Link Flags Release: ${CMAKE_EXE_LINKER_FLAGS_RELEASE}")
+
+# ------------------------------------------------------------------------
+
+add_custom_command(
+  COMMAND ${BISON_EXECUTABLE}
+  ARGS ${SOURCE_DIR}/${BISON_INPUT} -o ${BINARY_DIR}/${BISON_OUTPUT}
+  OUTPUT ${BINARY_DIR}/${BISON_OUTPUT} ${BINARY_DIR}/${BISON_HEADER}
+  WORKING_DIRECTORY ${SOURCE_DIR} #/${BISON_INPUT}
+  DEPENDS ${BINARY_DIR}/${FLEX_OUTPUT} ${SOURCE_DIR}/${BISON_INPUT}
+)
+
+add_custom_command(
+  COMMAND ${FLEX_EXECUTABLE}
+  ARGS --header-file=${BINARY_DIR}/${FLEX_HEADER} -o ${BINARY_DIR}/${FLEX_OUTPUT} ${SOURCE_DIR}/${FLEX_INPUT}
+  OUTPUT ${BINARY_DIR}/${FLEX_OUTPUT} ${BINARY_DIR}/${FLEX_HEADER}
+  WORKING_DIRECTORY ${SOURCE_DIR} #/${FLEX_INPUT}
+  DEPENDS ${SOURCE_DIR}/${FLEX_INPUT}
+)
+
+SET_SOURCE_FILES_PROPERTIES(${BINARY_DIR}/${FLEX_OUTPUT} ${BINARY_DIR}/${FLEX_HEADER} GENERATED)
+SET_SOURCE_FILES_PROPERTIES(${BINARY_DIR}/${BISON_OUTPUT} ${BINARY_DIR}/${BISON_HEADER} GENERATED)
+
+# ------------------------------------------------------------------------
+
+set(PARSER_LIB_SRC ${BINARY_DIR}/${FLEX_OUTPUT}
+                   ${BINARY_DIR}/${BISON_OUTPUT}
+                   ${SOURCE_DIR}/smtlib2hashtable.c
+                   ${SOURCE_DIR}/smtlib2abstractparser.c
+                   ${SOURCE_DIR}/smtlib2termparser.c
+                   ${SOURCE_DIR}/smtlib2utils.c
+                   ${SOURCE_DIR}/smtlib2vector.c
+                   ${SOURCE_DIR}/smtlib2charbuf.c
+                   ${SOURCE_DIR}/smtlib2stream.c
+                   ${SOURCE_DIR}/smtlib2scanner.c
+)
+
+add_library(${LIBRARY_NAME} ${PARSER_LIB_SRC})
+add_library(${LIBRARY_NAME}::${LIBRARY_NAME} ALIAS ${LIBRARY_NAME})
+
+target_compile_options(${LIBRARY_NAME} PRIVATE -Wall)
+target_compile_options(${LIBRARY_NAME} PRIVATE -W)
+
+set_target_properties(${LIBRARY_NAME} PROPERTIES C_EXTENSIONS OFF)
+
+target_include_directories(${LIBRARY_NAME}
+  PUBLIC
+    $<INSTALL_INTERFACE:include>
+    $<BUILD_INTERFACE:${PROJECT_SOURCE_DIR}/include>
+    $<BUILD_INTERFACE:${BINARY_DIR}>
+)
+
+# ------------------------------------------------------------------------
+
+if (SMT_PARSER_BUILD_YICES) 
+
+  set(EXECUTABLE_NAME parser)
+
+  find_package(GMP REQUIRED)
+
+  add_executable(${EXECUTABLE_NAME} smtlib2yices.c yicesmain.c)
+
+  target_compile_options(${EXECUTABLE_NAME} PRIVATE -Wall)
+  target_compile_options(${EXECUTABLE_NAME} PRIVATE -W)
+
+  target_link_libraries(${EXECUTABLE_NAME} ${LIBRARY_NAME})
+  target_link_libraries(${EXECUTABLE_NAME} ${GMP_C_LIBRARIES})
+
+  target_include_directories(${EXECUTABLE_NAME} 
+      PRIVATE ${PROJECT_SOURCE_DIR}/include
+      $<BUILD_INTERFACE:${GMP_C_INCLUDES}>
+  )
+
+  install(TARGETS ${LIBRARY_NAME} ${EXECUTABLE_NAME}
+    EXPORT ${SMT_PARSER_TARGETS_EXPORT_NAME}
+    LIBRARY DESTINATION lib
+    ARCHIVE DESTINATION lib
+    RUNTIME DESTINATION bin
+    INCLUDES DESTINATION ${SMT_PARSER_INCLUDE_INSTALL_DIR}
+  )
+
+
+endif()
+
+# ------------------------------------------------------------------------
+
+
+install(
+  DIRECTORY ${SMT_PARSER_INCLUDE_BUILD_DIR}/smtparser
+  DESTINATION ${SMT_PARSER_INCLUDE_INSTALL_DIR}
+)
+
+
+# ------------------------------------------------------------------------

src/smtlib2bisonparser.y

@@ -66,9 +66,9 @@ smtlib2_term smtlib2_make_term_from_identifier(
 %debug
 %verbose
 
-%parse-param {yyscan_t scanner}
+%parse-param {void * scanner}
 %parse-param {smtlib2_parser_interface *parser}
-%lex-param {yyscan_t scanner}
+%lex-param {void * scanner}
 
 %union {
     char *string;