cmake_minimum_required(VERSION 3.5)
project(ic3ia)

set(MATHSAT_DIR "" CACHE PATH "directory of MathSAT")
set(MSAT_INCLUDE_DIR "" CACHE PATH "include dir for mathsat")
set(MSAT_LIB_DIR "" CACHE PATH "library dir for mathsat")
option(BUILD_STATIC "Build a static executable" OFF)

if(MATHSAT_DIR)
    set(MSAT_LIB_DIR "${MATHSAT_DIR}/lib" CACHE INTERNAL "")
    set(MSAT_INCLUDE_DIR "${MATHSAT_DIR}/include" CACHE INTERNAL "")
endif()

if(BUILD_STATIC)
    set(CMAKE_EXE_LINKER_FLAGS -static)
    set(CMAKE_EXE_LINK_DYNAMIC_C_FLAGS "")       # remove -Wl,-Bdynamic
    set(CMAKE_EXE_LINK_DYNAMIC_CXX_FLAGS "")
    set(CMAKE_SHARED_LIBRARY_C_FLAGS "")         # remove -fPIC
    set(CMAKE_SHARED_LIBRARY_CXX_FLAGS "")
    set(CMAKE_SHARED_LIBRARY_LINK_C_FLAGS "")    # remove -rdynamic
    set(CMAKE_SHARED_LIBRARY_LINK_CXX_FLAGS "")
    set(CMAKE_FIND_LIBRARY_SUFFIXES ${CMAKE_STATIC_LIBRARY_SUFFIX})
endif()

find_library(mathsat mathsat PATHS "${MSAT_LIB_DIR}")
if(NOT mathsat)
    message(FATAL_ERROR "mathsat not found in ${MSAT_LIB_DIR}")
endif()

find_library(gmp gmp)
find_library(gmpxx gmpxx)

set(SRCS
    utils.cpp
    ia.cpp
    ic3.cpp
    solver.cpp
    ts.cpp
    unroll.cpp
    live.cpp
    bmc.cpp
    ltl.cpp
    proof.cpp
    api.cpp
    ic3ia.cpp
    invred.cpp
    rlive.cpp
    )

include_directories(. ${MSAT_INCLUDE_DIR})

add_definitions(-std=c++11)
if(NOT BUILD_STATIC)
    add_definitions(-fPIC)
endif()
add_library(ic3ia ${SRCS})
add_executable(ic3ia_main main.cpp)
set_target_properties(ic3ia_main PROPERTIES OUTPUT_NAME ic3ia)
target_link_libraries(ic3ia_main ic3ia ${mathsat} ${gmpxx} ${gmp})

add_executable(horn2vmt horn2vmt.cpp)
target_link_libraries(horn2vmt ic3ia ${mathsat} ${gmpxx} ${gmp})

add_custom_target(proofchecker ALL
    COMMAND ${CMAKE_COMMAND} -E copy_if_different
            "${PROJECT_SOURCE_DIR}/proofchecker.py" proofchecker.py
    WORKING_DIRECTORY "${PROJECT_BINARY_DIR}"
    )


find_package(PythonInterp)
find_package(SWIG)
find_package(PythonLibs)

if(SWIG_FOUND AND PYTHONLIBS_FOUND)
    add_custom_target(py
      COMMAND "${PYTHON_EXECUTABLE}"
          "${PROJECT_SOURCE_DIR}/python_api_setup.py"
		--msat-lib-dir="${MSAT_LIB_DIR}"
		--msat-include-dir="${MSAT_INCLUDE_DIR}"
                --swig-tool="${SWIG_EXECUTABLE}"
                --build-dir="${PROJECT_BINARY_DIR}"
      COMMENT "Building Python bindings"
      DEPENDS ic3ia
      WORKING_DIRECTORY "${PROJECT_BINARY_DIR}"
      )
endif()
