add source files

.gitignore

@@ -30,3 +30,34 @@
 *.exe
 *.out
 *.app
+
+*~
+
+*.DS_Store
+*-checkpoint.ipynb
+*.so
+*.pyc
+
+src/GTAGS
+src/GRTAGS
+src/GPATH
+src/tools
+
+/* CMAKE */
+CMakeLists.txt.user
+CMakeCache.txt
+CMakeFiles
+CMakeScripts
+Testing
+Makefile
+cmake_install.cmake
+install_manifest.txt
+compile_commands.json
+CTestTestfile.cmake
+_deps
+/tools/pybind11_2_3_0.tar.gz
+build
+/.idea/
+cmake-build-debug/
+
+tools/

CMakeLists.txt

@@ -0,0 +1,291 @@
+cmake_minimum_required (VERSION 3.12)
+project(Soy)
+
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+
+option(BUILD_STATIC_SOY "Build static Soy binary" OFF)
+option(RUN_UNIT_TEST "run unit tests on build" ON)
+option(RUN_MEMORY_TEST "run cxxtest testing with ASAN ON" ON)
+option(CODE_COVERAGE "add code coverage" OFF)  # Available only in debug mode
+
+set(SOY_LIB SoyHelper)
+set(SOY_TEST_LIB SoyHelperTest)
+set(SOY_EXE Soy${CMAKE_EXECUTABLE_SUFFIX})
+
+set(DEPS_DIR "${PROJECT_SOURCE_DIR}/deps")
+set(TOOLS_DIR "${PROJECT_SOURCE_DIR}/tools")
+set(SRC_DIR "${PROJECT_SOURCE_DIR}/src")
+
+set(ENGINE_DIR "${SRC_DIR}/engine")
+set(PYBIND11_DIR "${TOOLS_DIR}/pybind11-2.3.0")
+set(BOOST_DIR "${TOOLS_DIR}/boost_1_68_0")
+set(CADICAL_DIR "${TOOLS_DIR}/cadical")
+
+set(COMMON_DIR "${SRC_DIR}/common")
+set(CVC4_DIR "${DEPS_DIR}/CVC4")
+
+set(LOCAL_SEARCH_DIR "${SRC_DIR}/local_search")
+set(CONSTRAINTS_DIR "${SRC_DIR}/constraints")
+
+set(CONTEXT_DIR "${CVC4_DIR}/context")
+set(CVC4_BASE_DIR "${CVC4_DIR}/base")
+file(GLOB DEPS_CVC4_CONTEXT "${CONTEXT_DIR}/*.cpp")
+file(GLOB DEPS_CVC4_BASE "${CVC4_BASE_DIR}/*.cpp")
+include_directories(SYSTEM ${CVC4_DIR} ${CVC4_DIR}/include)
+
+set(CADICAL_LIB cadical)
+
+set(BIN_DIR "${CMAKE_BINARY_DIR}/bin")
+
+set(COMMON_REAL "${COMMON_DIR}/real")
+set(COMMON_MOCK "${COMMON_DIR}/mock")
+file(GLOB SRCS_COMMON_REAL "${COMMON_REAL}/*.cpp")
+file(GLOB SRCS_COMMON_MOCK "${COMMON_MOCK}/*.cpp")
+
+set(ENGINE_REAL "${ENGINE_DIR}/real")
+set(ENGINE_MOCK "${ENGINE_DIR}/mock")
+file(GLOB SRCS_ENGINE_REAL "${ENGINE_REAL}/*.cpp")
+file(GLOB SRCS_ENGINE_MOCK "${ENGINE_MOCK}/*.cpp")
+
+set(MPS_PARSER mps)
+set(ACAS_PARSER acas)
+set(BERKELEY_PARSER berkeley)
+set(INPUT_PARSERS_DIR input_parsers)
+
+#-----------------------------------------------------------------------------#
+# Determine number of threads available, used to configure (default) parallel
+# execution of custom test targets (can be overriden with ARGS=-jN).
+
+include(ProcessorCount)
+ProcessorCount(CTEST_NTHREADS)
+if(CTEST_NTHREADS EQUAL 0)
+  set(CTEST_NTHREADS 1)
+endif()
+
+# --------------- set build type ----------------------------
+set(BUILD_TYPES Release Debug MinSizeRel RelWithDebInfo)
+
+# Set the default build type to Production
+if(NOT CMAKE_BUILD_TYPE)
+  set(CMAKE_BUILD_TYPE
+      Release CACHE STRING "Options are: Release Debug MinSizeRel RelWithDebInfo" FORCE)
+  # Provide drop down menu options in cmake-gui
+  set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
+endif()
+message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
+
+#-------------------------set code coverage----------------------------------#
+# Allow coverage only in debug mode only in gcc
+if(CODE_COVERAGE AND CMAKE_CXX_COMPILER_ID MATCHES "GNU" AND CMAKE_BUILD_TYPE MATCHES Debug)
+  message(STATUS "Building with code coverage")
+  set(COVERAGE_COMPILER_FLAGS "-g -O0 --coverage" CACHE INTERNAL "")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${COVERAGE_COMPILER_FLAGS}")
+  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
+endif()
+
+# We build a static library that is the core of the project, the link it to the
+# API's (executable and python at the moment)
+add_library(${SOY_LIB} ${DEPS_CVC4_CONTEXT} ${DEPS_CVC4_BASE} ${SRCS_COMMON_REAL} ${SRCS_ENGINE_REAL})
+target_include_directories(${SOY_LIB} PRIVATE SYSTEM)
+
+add_executable(${SOY_EXE} "${ENGINE_DIR}/main.cpp")
+set(SOY_EXE_PATH "${BIN_DIR}/${SOY_EXE}")
+add_custom_command(TARGET ${SOY_EXE} POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E copy $<TARGET_FILE:${SOY_EXE}> ${SOY_EXE_PATH} )
+
+set(MPS_PARSER_PATH "${BIN_DIR}/${MPS_PARSER}")
+
+if (NOT MSVC)
+    if (CMAKE_CXX_COMPILER_ID MATCHES "Clang")
+       set(COMPILE_FLAGS  -Wall -Wextra  -Werror -MMD -Qunused-arguments ) #-Wno-deprecated 
+     else()
+       set(COMPILE_FLAGS  -Wall -Wextra  -Werror -MMD ) #-Wno-deprecated 
+    endif()
+    set(RELEASE_FLAGS ${COMPILE_FLAGS} -O3) #-Wno-deprecated
+endif()
+
+if (RUN_MEMORY_TEST)
+    if(NOT MSVC)
+        set(MEMORY_FLAGS -fsanitize=address -fno-omit-frame-pointer -O1)
+    endif()
+endif()
+
+if (NOT MSVC)
+    set(DEBUG_FLAGS ${COMPILE_FLAGS} ${MEMORY_FLAGS} -g)
+    set(CXXTEST_FLAGS ${DEBUG_FLAGS}  -Wno-ignored-qualifiers)
+else()
+    set(DEBUG_FLAGS ${COMPILE_FLAGS} ${MEMORY_FLAGS})
+    add_definitions(-DNOMINMAX) # remove min max macros
+endif()
+
+if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
+    set(CXXTEST_FLAGS ${CXXTEST_FLAGS} -Wno-terminate)
+endif()
+
+# Boost
+if (MSVC)
+    set(BOOST_ROOT "${BOOST_DIR}/win_installed")
+elseif (${CMAKE_SIZEOF_VOID_P} EQUAL 4 AND NOT MSVC)
+    set(BOOST_ROOT "${BOOST_DIR}/installed32")
+else()
+    set(BOOST_ROOT "${BOOST_DIR}/installed")
+endif()
+
+if (MSVC)
+    set(SCRIPT_EXTENSION bat)
+    set(Boost_NAMESPACE libboost)
+else()
+    set(SCRIPT_EXTENSION sh)
+endif()
+
+if (MSVC)
+    set(SCRIPT_EXTENSION bat)
+    set(Boost_NAMESPACE libboost)
+else()
+    set(SCRIPT_EXTENSION sh)
+endif()
+find_package(Boost COMPONENTS program_options timer chrono thread)
+# Find boost
+if (NOT ${Boost_FOUND})
+    # bash file that downloads and install boost 1_68_0, the name need to match
+    # BOOST_DIR variable
+    execute_process(COMMAND ${TOOLS_DIR}/download_boost.${SCRIPT_EXTENSION})
+    find_package(Boost REQUIRED COMPONENTS program_options timer chrono thread)
+endif()
+set(LIBS_INCLUDES ${Boost_INCLUDE_DIRS})
+set(LIBS ${Boost_LIBRARIES})
+
+message(STATUS "Looking for Gurobi")
+if (NOT DEFINED GUROBI_DIR)
+  set(GUROBI_DIR $ENV{GUROBI_HOME})
+endif()
+add_compile_definitions(ENABLE_GUROBI)
+
+set(GUROBI_LIB1 "gurobi_c++")
+set(GUROBI_LIB2 "gurobi95")
+
+add_library(${GUROBI_LIB1} SHARED IMPORTED)
+set_target_properties(${GUROBI_LIB1} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi_c++.a)
+list(APPEND LIBS ${GUROBI_LIB1})
+target_include_directories(${GUROBI_LIB1} INTERFACE ${GUROBI_DIR}/include/)
+
+add_library(${GUROBI_LIB2} SHARED IMPORTED)
+
+# MACOSx uses .dylib instead of .so for its Gurobi downloads.
+if (APPLE)
+  set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi95.dylib)
+else()
+  set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi95.so)
+endif ()
+
+list(APPEND LIBS ${GUROBI_LIB2})
+target_include_directories(${GUROBI_LIB2} INTERFACE ${GUROBI_DIR}/include/)
+
+# Cadical
+message(STATUS "Looking for cadical")
+if(NOT EXISTS "${CADICAL_DIR}/build/libcadical.a")
+  message("Can't find cadical, installing.")
+  execute_process(COMMAND ${TOOLS_DIR}/download_cadical.sh)
+endif()
+
+add_library(${CADICAL_LIB} SHARED IMPORTED)
+set_target_properties(${CADICAL_LIB} PROPERTIES IMPORTED_LOCATION ${CADICAL_DIR}/build/libcadical.a)
+list(APPEND LIBS ${CADICAL_LIB})
+target_include_directories(${CADICAL_LIB} INTERFACE ${CADICAL_DIR}/src/)
+
+# pthread
+set(THREADS_PREFER_PTHREAD_FLAG ON)
+find_package(Threads REQUIRED)
+list(APPEND LIBS Threads::Threads)
+
+if (BUILD_STATIC_SOY)
+  # build a static library
+  target_link_libraries(${SOY_LIB} ${LIBS} -static)
+else()
+  target_link_libraries(${SOY_LIB} ${LIBS})
+endif()
+
+target_include_directories(${SOY_LIB} PRIVATE ${LIBS_INCLUDES})
+target_compile_options(${SOY_LIB} PRIVATE ${RELEASE_FLAGS})
+
+# Build Soy executable
+target_link_libraries(${SOY_EXE} ${SOY_LIB})
+target_include_directories(${SOY_EXE} PRIVATE ${LIBS_INCLUDES})
+
+add_library(${SOY_TEST_LIB})
+set (TEST_DIR "${CMAKE_CURRENT_BINARY_DIR}/tests")
+file(MAKE_DIRECTORY ${TEST_DIR})
+
+set(CMAKE_PREFIX_PATH "${TOOLS_DIR}/cxxtest")
+set(CXXTEST_USE_PYTHON FALSE)
+find_package(CxxTest)
+if(CXXTEST_FOUND)
+    include_directories(${CXXTEST_INCLUDE_DIR})
+    enable_testing()
+endif()
+
+target_link_libraries(${SOY_TEST_LIB} ${SOY_LIB} ${LIBS})
+target_include_directories(${SOY_TEST_LIB} PRIVATE ${LIBS_INCLUDES} )
+target_compile_options(${SOY_TEST_LIB} PRIVATE ${CXXTEST_FLAGS})
+
+add_custom_target(build-tests ALL)
+
+add_custom_target(check
+      COMMAND ctest --output-on-failure -j${CTEST_NTHREADS} $$ARGS
+      DEPENDS build-tests build_input_parsers ${SOY_EXE})
+
+# Decide which tests to run and execute
+set(TESTS_TO_RUN "")
+# ctest uses regex, so create the string to look: (unit|system) ...
+macro(append_tests_to_run new_val)
+    if ("${TESTS_TO_RUN}" STREQUAL "")
+        set(TESTS_TO_RUN ${new_val})
+    else()
+        set(TESTS_TO_RUN "${TESTS_TO_RUN}|${new_val}")
+    endif()
+endmacro()
+
+if (${RUN_UNIT_TEST})
+    append_tests_to_run("unit")
+endif()
+if (${RUN_SYSTEM_TEST})
+    append_tests_to_run("system")
+endif()
+if (NOT ${TESTS_TO_RUN} STREQUAL "")
+    # make ctest verbose
+    set(CTEST_OUTPUT_ON_FAILURE 1)
+    add_custom_command(
+        TARGET build-tests
+        POST_BUILD
+        COMMAND ctest --output-on-failure  -L "\"(${TESTS_TO_RUN})\"" -j${CTEST_NTHREADS} $$ARGS
+    )
+endif()
+
+# Add the input parsers
+add_custom_target(build_input_parsers)
+add_dependencies(build_input_parsers ${MPS_PARSER})
+
+add_subdirectory(${SRC_DIR})
+add_subdirectory(${TOOLS_DIR})
+
+
+execute_process(
+  COMMAND git rev-parse --abbrev-ref HEAD
+  WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+  OUTPUT_VARIABLE GIT_BRANCH
+  OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+# Get the latest abbreviated commit hash of the working branch
+execute_process(
+  COMMAND git log -1 --format=%h
+  WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+  OUTPUT_VARIABLE GIT_COMMIT_HASH
+  OUTPUT_STRIP_TRAILING_WHITESPACE
+)
+
+# Soy Version
+set(SOY_VERSION 1.0.+)
+add_definitions("-DGIT_COMMIT_HASH=\"${GIT_COMMIT_HASH}\"")
+add_definitions("-DGIT_BRANCH=\"${GIT_BRANCH}\"")
+add_definitions("-DSOY_VERSION=\"${SOY_VERSION}\"")

COPYING

@@ -0,0 +1,45 @@
+This repo is copyright (C) 2022-2023 by its contributors and their institutional
+affiliations. All rights reserved.
+
+The source code of Soy is open and available to study, to modify, and to
+redistribute original or modified versions; distribution is under the terms of
+the modified BSD license (reproduced below). Soy links against multiple
+third-party libraries, see details below.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+-------------------------------------------------------------------------------
+ Third-Party Software
+-------------------------------------------------------------------------------
+
+The Soy source code includes third-party software which has its own copyright
+and licensing terms, as described below. 
+
+    Boost        Boost Software License     (https://www.boost.org)
+    Cadical      MIT License                (https://github.com/arminbiere/cadical/)
+    Gurobi       Free Academic License      (https://www.gurobi.com)