From 9cae42243a4c0be14fd72f5379ee4eb9f4bc88e9 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Nov 2021 13:59:47 -0700 Subject: [PATCH] bv: Remove layered solver. (#7455) This commit removes the old bit-vector solver code. --- CMakeLists.txt | 14 - INSTALL.rst | 13 - cmake/FindABC.cmake | 40 - configure.sh | 15 - contrib/get-abc | 42 - src/CMakeLists.txt | 52 - src/base/configuration.cpp | 12 +- src/base/configuration.h | 2 - src/base/configuration_private.h | 6 - src/options/bv_options.toml | 98 +- src/options/didyoumean_test.cpp | 760 +++++++++ src/options/options_handler.cpp | 28 - src/preprocessing/passes/bv_abstraction.cpp | 64 - src/preprocessing/passes/bv_abstraction.h | 50 - .../preprocessing_pass_registry.cpp | 2 - src/prop/bv_sat_solver_notify.h | 51 - src/prop/bvminisat/LICENSE | 21 - src/prop/bvminisat/README | 24 - src/prop/bvminisat/bvminisat.cpp | 299 ---- src/prop/bvminisat/bvminisat.h | 151 -- src/prop/bvminisat/core/Dimacs.h | 91 -- src/prop/bvminisat/core/Solver.cc | 1421 ----------------- src/prop/bvminisat/core/Solver.h | 539 ------- src/prop/bvminisat/core/SolverTypes.h | 435 ----- src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt | 79 - src/prop/bvminisat/mtl/Alg.h | 87 - src/prop/bvminisat/mtl/Alloc.h | 154 -- src/prop/bvminisat/mtl/Heap.h | 161 -- src/prop/bvminisat/mtl/IntTypes.h | 50 - src/prop/bvminisat/mtl/Map.h | 196 --- src/prop/bvminisat/mtl/Queue.h | 91 -- src/prop/bvminisat/mtl/Sort.h | 99 -- src/prop/bvminisat/mtl/Vec.h | 152 -- src/prop/bvminisat/mtl/XAlloc.h | 47 - src/prop/bvminisat/simp/SimpSolver.cc | 812 ---------- src/prop/bvminisat/simp/SimpSolver.h | 243 --- src/prop/bvminisat/utils/Options.cc | 94 -- src/prop/bvminisat/utils/Options.h | 437 ----- src/prop/bvminisat/utils/ParseUtils.h | 125 -- src/prop/bvminisat/utils/System.cc | 99 -- src/prop/bvminisat/utils/System.h | 67 - src/prop/sat_solver.h | 25 - src/prop/sat_solver_factory.cpp | 9 - src/prop/sat_solver_factory.h | 4 - src/smt/process_assertions.cpp | 5 - src/smt/set_defaults.cpp | 36 +- src/theory/bv/abstraction.cpp | 1100 ------------- src/theory/bv/abstraction.h | 248 --- src/theory/bv/bitblast/aig_bitblaster.cpp | 492 ------ src/theory/bv/bitblast/aig_bitblaster.h | 124 -- src/theory/bv/bitblast/bitblaster.h | 15 - src/theory/bv/bitblast/eager_bitblaster.cpp | 294 ---- src/theory/bv/bitblast/eager_bitblaster.h | 88 - src/theory/bv/bitblast/lazy_bitblaster.cpp | 581 ------- src/theory/bv/bitblast/lazy_bitblaster.h | 180 --- src/theory/bv/bv_eager_solver.cpp | 129 -- src/theory/bv/bv_eager_solver.h | 64 - src/theory/bv/bv_inequality_graph.cpp | 480 ------ src/theory/bv/bv_inequality_graph.h | 297 ---- src/theory/bv/bv_quick_check.cpp | 373 ----- src/theory/bv/bv_quick_check.h | 182 --- src/theory/bv/bv_solver.h | 9 - src/theory/bv/bv_solver_layered.cpp | 553 ------- src/theory/bv/bv_solver_layered.h | 228 --- src/theory/bv/bv_subtheory.h | 111 -- src/theory/bv/bv_subtheory_algebraic.cpp | 984 ------------ src/theory/bv/bv_subtheory_algebraic.h | 244 --- src/theory/bv/bv_subtheory_bitblast.cpp | 276 ---- src/theory/bv/bv_subtheory_bitblast.h | 84 - src/theory/bv/bv_subtheory_core.cpp | 418 ----- src/theory/bv/bv_subtheory_core.h | 108 -- src/theory/bv/bv_subtheory_inequality.cpp | 254 --- src/theory/bv/bv_subtheory_inequality.h | 94 -- src/theory/bv/slicer.cpp | 85 - src/theory/bv/slicer.h | 55 - src/theory/bv/theory_bv.cpp | 13 +- src/theory/bv/theory_bv.h | 4 - test/regress/CMakeLists.txt | 2 - test/regress/regress0/bv/bv-abstr-bug.smt2 | 16 - .../regress0/bv/test-bv_intro_pow2.smt2 | 2 +- .../issue5729-rewritten-assertions.smt2 | 3 +- .../regress1/bv/test-bv-abstraction.smt2 | 24 - test/unit/theory/theory_bv_white.cpp | 35 +- 83 files changed, 769 insertions(+), 14782 deletions(-) delete mode 100644 cmake/FindABC.cmake delete mode 100755 contrib/get-abc create mode 100644 src/options/didyoumean_test.cpp delete mode 100644 src/preprocessing/passes/bv_abstraction.cpp delete mode 100644 src/preprocessing/passes/bv_abstraction.h delete mode 100644 src/prop/bv_sat_solver_notify.h delete mode 100644 src/prop/bvminisat/LICENSE delete mode 100644 src/prop/bvminisat/README delete mode 100644 src/prop/bvminisat/bvminisat.cpp delete mode 100644 src/prop/bvminisat/bvminisat.h delete mode 100644 src/prop/bvminisat/core/Dimacs.h delete mode 100644 src/prop/bvminisat/core/Solver.cc delete mode 100644 src/prop/bvminisat/core/Solver.h delete mode 100644 src/prop/bvminisat/core/SolverTypes.h delete mode 100644 src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt delete mode 100644 src/prop/bvminisat/mtl/Alg.h delete mode 100644 src/prop/bvminisat/mtl/Alloc.h delete mode 100644 src/prop/bvminisat/mtl/Heap.h delete mode 100644 src/prop/bvminisat/mtl/IntTypes.h delete mode 100644 src/prop/bvminisat/mtl/Map.h delete mode 100644 src/prop/bvminisat/mtl/Queue.h delete mode 100644 src/prop/bvminisat/mtl/Sort.h delete mode 100644 src/prop/bvminisat/mtl/Vec.h delete mode 100644 src/prop/bvminisat/mtl/XAlloc.h delete mode 100644 src/prop/bvminisat/simp/SimpSolver.cc delete mode 100644 src/prop/bvminisat/simp/SimpSolver.h delete mode 100644 src/prop/bvminisat/utils/Options.cc delete mode 100644 src/prop/bvminisat/utils/Options.h delete mode 100644 src/prop/bvminisat/utils/ParseUtils.h delete mode 100644 src/prop/bvminisat/utils/System.cc delete mode 100644 src/prop/bvminisat/utils/System.h delete mode 100644 src/theory/bv/abstraction.cpp delete mode 100644 src/theory/bv/abstraction.h delete mode 100644 src/theory/bv/bitblast/aig_bitblaster.cpp delete mode 100644 src/theory/bv/bitblast/aig_bitblaster.h delete mode 100644 src/theory/bv/bitblast/eager_bitblaster.cpp delete mode 100644 src/theory/bv/bitblast/eager_bitblaster.h delete mode 100644 src/theory/bv/bitblast/lazy_bitblaster.cpp delete mode 100644 src/theory/bv/bitblast/lazy_bitblaster.h delete mode 100644 src/theory/bv/bv_eager_solver.cpp delete mode 100644 src/theory/bv/bv_eager_solver.h delete mode 100644 src/theory/bv/bv_inequality_graph.cpp delete mode 100644 src/theory/bv/bv_inequality_graph.h delete mode 100644 src/theory/bv/bv_quick_check.cpp delete mode 100644 src/theory/bv/bv_quick_check.h delete mode 100644 src/theory/bv/bv_solver_layered.cpp delete mode 100644 src/theory/bv/bv_solver_layered.h delete mode 100644 src/theory/bv/bv_subtheory.h delete mode 100644 src/theory/bv/bv_subtheory_algebraic.cpp delete mode 100644 src/theory/bv/bv_subtheory_algebraic.h delete mode 100644 src/theory/bv/bv_subtheory_bitblast.cpp delete mode 100644 src/theory/bv/bv_subtheory_bitblast.h delete mode 100644 src/theory/bv/bv_subtheory_core.cpp delete mode 100644 src/theory/bv/bv_subtheory_core.h delete mode 100644 src/theory/bv/bv_subtheory_inequality.cpp delete mode 100644 src/theory/bv/bv_subtheory_inequality.h delete mode 100644 src/theory/bv/slicer.cpp delete mode 100644 src/theory/bv/slicer.h delete mode 100644 test/regress/regress0/bv/bv-abstr-bug.smt2 delete mode 100644 test/regress/regress1/bv/test-bv-abstraction.smt2 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-