From: Mathias Preiner Date: Mon, 1 Nov 2021 20:59:47 +0000 (-0700) Subject: bv: Remove layered solver. (#7455) X-Git-Tag: cvc5-1.0.0~915 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9cae42243a4c0be14fd72f5379ee4eb9f4bc88e9;p=cvc5.git bv: Remove layered solver. (#7455) This commit removes the old bit-vector solver code. --- diff --git a/CMakeLists.txt b/CMakeLists.txt index f5184b2df..ef3b7636e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -48,9 +48,6 @@ endif() #-----------------------------------------------------------------------------# # Tell CMake where to find our dependencies -if(ABC_DIR) - list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}") -endif() if(GLPK_DIR) list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}") endif() @@ -101,7 +98,6 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") # >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for ENABLE_BEST -cvc5_option(USE_ABC "Use ABC for AIG bit-blasting") cvc5_option(USE_CLN "Use CLN instead of GMP") cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") cvc5_option(USE_GLPK "Use GLPK simplex solver") @@ -118,7 +114,6 @@ option(USE_PYTHON2 "Force Python 2 (deprecated)") # installed via the corresponding contrib/get-* script and if not found, we # check the intalled system version. If the user provides a directory we # immediately fail if the dependency was not found at the specified location. -set(ABC_DIR "" CACHE STRING "Set ABC install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") # Prepend binaries with prefix on make install @@ -370,11 +365,6 @@ if(ENABLE_VALGRIND) add_definitions(-DCVC5_VALGRIND) endif() -if(USE_ABC) - find_package(ABC REQUIRED) - add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS}) -endif() - find_package(CaDiCaL REQUIRED) if(USE_CLN) @@ -608,7 +598,6 @@ print_config("Java bindings " ${BUILD_BINDINGS_JAVA}) print_config("Python2 " ${USE_PYTHON2}) print_config("Interprocedural opt. " ${ENABLE_IPO}) message("") -print_config("ABC " ${USE_ABC}) print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM}) print_config("GLPK " ${USE_GLPK}) print_config("Kissat " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM}) @@ -624,9 +613,6 @@ print_config("Editline " ${USE_EDITLINE}) message("") print_config("Api docs " ${BUILD_DOCS}) message("") -if(ABC_DIR) - print_config("ABC dir " ${ABC_DIR}) -endif() if(GLPK_DIR) print_config("GLPK dir " ${GLPK_DIR}) endif() diff --git a/INSTALL.rst b/INSTALL.rst index 8c2b67315..106948969 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -174,19 +174,6 @@ cvc5 with GLPK support, you are licensing cvc5 under that same license. (Usually cvc5's license is more permissive; see above discussion.) -ABC library (Improved Bit-Vector Support) -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -`ABC `_ (A System for Sequential -Synthesis and Verification) is a library for synthesis and verification of logic -circuits. This dependency may improve performance of the eager bit-vector -solver. When enabled, the bit-blasted formula is encoded into -and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. - -ABC can be installed using the ``contrib/get-abc`` script. Configure cvc5 with -``configure.sh --abc`` to build with this dependency. - - Editline library (Improved Interactive Experience) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake deleted file mode 100644 index 4e3b7a397..000000000 --- a/cmake/FindABC.cmake +++ /dev/null @@ -1,40 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Mathias Preiner -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# Find ABC -# ABC_FOUND - system has ABC lib -# ABC_INCLUDE_DIR - the ABC include directory -# ABC_LIBRARIES - Libraries needed to use ABC -# ABC_ARCH_FLAGS - Platform specific compile flags -## - -# Note: contrib/get-abc copies header files to deps/install/include/abc. -# However, includes in ABC headers are not prefixed with "abc/" and therefore -# we have to look for headers in include/abc instead of include/. -find_path(ABC_INCLUDE_DIR NAMES base/abc/abc.h PATH_SUFFIXES abc) -find_library(ABC_LIBRARIES NAMES abc) -find_program(ABC_ARCH_FLAGS_PROG NAMES arch_flags) - -if(ABC_ARCH_FLAGS_PROG) - execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG} - OUTPUT_VARIABLE ABC_ARCH_FLAGS) -endif() - -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(ABC - DEFAULT_MSG - ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) - -mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) -if(ABC_LIBRARIES) - message(STATUS "Found ABC libs: ${ABC_LIBRARIES}") -endif() diff --git a/configure.sh b/configure.sh index 641be5c18..b7a2ca280 100755 --- a/configure.sh +++ b/configure.sh @@ -57,7 +57,6 @@ Optional Packages: The following flags enable optional packages (disable with --no-