From d8104e0d48a845be7653d1a541c52dea21321aed Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 23 Mar 2021 19:27:39 -0300 Subject: [PATCH] Removing unused build options and deprecated proof compile flag (#6195) --- .github/workflows/ci.yml | 5 +-- CMakeLists.txt | 40 +---------------- COPYING | 2 - INSTALL.md | 42 ++++++++---------- configure.sh | 35 --------------- src/CMakeLists.txt | 8 ---- src/base/configuration.cpp | 18 +------- src/base/configuration.h | 6 --- src/base/configuration_private.h | 18 -------- src/options/options_handler.cpp | 43 +++---------------- src/options/options_handler.h | 2 - src/options/smt_options.toml | 2 - src/smt/smt_engine.cpp | 14 ------ src/smt/smt_engine_scope.cpp | 6 --- test/CMakeLists.txt | 4 -- test/regress/regress0/arrays/issue3814.smt2 | 1 - test/regress/regress0/bv/ackermann2.smt2 | 1 - .../regress0/bv/bv_to_int_5230_binary.smt2 | 1 - .../bv/bv_to_int_5230_missing_op.smt2 | 1 - .../bv/bv_to_int_5230_shift_const.smt2 | 3 +- .../regress0/bv/core/slice-12.smtv1.smt2 | 1 - .../regress0/dump-unsat-core-full.smt2 | 1 - test/regress/regress0/nl/issue3959.smt2 | 1 - .../regress1/quantifiers/dump-inst-proof.smt2 | 1 - .../regress1/sygus-abduct-test-ccore.smt2 | 1 - .../regress1/sygus-abduct-test-user.smt2 | 1 - .../regress1/sygus/abd-simple-conj-4.smt2 | 1 - .../abduction_1255.corecstrs.readable.smt2 | 1 - .../sygus/abduction_streq.readable.smt2 | 1 - test/regress/regress1/sygus/array_search_2.sy | 1 - test/regress/run_regression.py | 11 ----- test/unit/CMakeLists.txt | 4 -- test/unit/api/solver_black.cpp | 14 +----- 33 files changed, 29 insertions(+), 262 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e1ea39011..ad6004251 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,7 +23,7 @@ jobs: include: - name: production - config: production --all-bindings --lfsc --editline --poly --symfpu + config: production --all-bindings --editline --poly --symfpu cache-key: production python-bindings: true check-examples: true @@ -40,7 +40,7 @@ jobs: run_regression_args: --no-check-unsat-cores --no-check-proofs - name: production-dbg - config: production --assertions --tracing --unit-testing --symfpu --lfsc --editline + config: production --assertions --tracing --unit-testing --symfpu --editline cache-key: dbg os: ubuntu-latest exclude_regress: 3-4 @@ -198,4 +198,3 @@ jobs: make -j2 ctest -j2 --output-on-failure working-directory: examples - diff --git a/CMakeLists.txt b/CMakeLists.txt index 1bbe6d288..7d0c98be2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -70,9 +70,6 @@ endif() if(CRYPTOMINISAT_DIR) list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}") endif() -if(DRAT2ER_DIR) - list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}") -endif() if(GLPK_DIR) list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}") endif() @@ -82,9 +79,6 @@ endif() if(KISSAT_DIR) list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}") endif() -if(LFSC_DIR) - list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}") -endif() if(POLY_DIR) list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}") endif() @@ -119,7 +113,6 @@ cvc4_option(ENABLE_COMP_INC_TRACK cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc4_option(ENABLE_DUMPING "Enable dumping") cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") -cvc4_option(ENABLE_PROOFS "Enable proof support") cvc4_option(ENABLE_STATISTICS "Enable statistics") cvc4_option(ENABLE_TRACING "Enable tracing") cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") @@ -148,8 +141,6 @@ cvc4_option(USE_KISSAT "Use Kissat SAT solver") cvc4_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) -option(USE_DRAT2ER "Include drat2er for making eager BV proofs") -option(USE_LFSC "Use LFSC proof checker") option(USE_POLY "Use LibPoly for polynomial arithmetic") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Force Python 2 (deprecated)") @@ -163,11 +154,9 @@ set(ABC_DIR "" CACHE STRING "Set ABC install directory") set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory") set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory") set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory") -set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") set(GMP_DIR "" CACHE STRING "Set GMP install directory") set(KISSAT_DIR "" CACHE STRING "Set Kissat install directory") -set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") set(POLY_DIR "" CACHE STRING "Set LibPoly install directory") set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") @@ -429,10 +418,6 @@ if(ENABLE_PROFILING) add_check_c_cxx_flag("-pg") endif() -if(ENABLE_PROOFS) - add_definitions(-DCVC4_PROOF) -endif() - if(ENABLE_TRACING) add_definitions(-DCVC4_TRACING) endif() @@ -477,11 +462,6 @@ if(USE_CRYPTOMINISAT) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() -if(USE_DRAT2ER) - find_package(Drat2Er REQUIRED) - add_definitions(-DCVC4_USE_DRAT2ER) -endif() - if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") find_package(GLPK REQUIRED) @@ -493,11 +473,6 @@ if(USE_KISSAT) add_definitions(-DCVC4_USE_KISSAT) endif() -if(USE_LFSC) - find_package(LFSC REQUIRED) - add_definitions(-DCVC4_USE_LFSC) -endif() - if(USE_POLY) find_package(Poly REQUIRED) add_definitions(-DCVC4_USE_POLY) @@ -550,11 +525,6 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# # Add subdirectories -# signatures needs to come before src since it adds source files to libcvc4. -if(ENABLE_PROOFS) - add_subdirectory(proofs/signatures) -endif() - add_subdirectory(doc) add_subdirectory(src) add_subdirectory(test) @@ -580,7 +550,7 @@ include(CMakePackageConfigHelpers) # libraries from deps/install/lib, we need to be cautious. Changing these # shared libraries from deps/install/lib most probably breaks the binary. # We only allow such an installation for custom installation prefixes -# (in the assumption that only reasonably experienced users use this and +# (in the assumption that only reasonably experienced users use this and # also that custom installation prefixes are not used for longer periods of # time anyway). Also, we print a big warning with further instructions. if(NOT ENABLE_STATIC_BINARY) @@ -695,10 +665,8 @@ message("") print_config("ABC :" USE_ABC) print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) -print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) print_config("Kissat :" USE_KISSAT) -print_config("LFSC :" USE_LFSC) print_config("LibPoly :" USE_POLY) message("") print_config("Build libcvc4 only :" BUILD_LIB_ONLY) @@ -723,9 +691,6 @@ endif() if(CRYPTOMINISAT_DIR) message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() -if(DRAT2ER_DIR) - message("DRAT2ER dir : ${DRAT2ER_DIR}") -endif() if(GLPK_DIR) message("GLPK dir : ${GLPK_DIR}") endif() @@ -735,9 +700,6 @@ endif() if(KISSAT_DIR) message("KISSAT dir : ${KISSAT_DIR}") endif() -if(LFSC_DIR) - message("LFSC dir : ${LFSC_DIR}") -endif() if(POLY_DIR) message("LibPoly dir : ${POLY_DIR}") endif() diff --git a/COPYING b/COPYING index d6f66b097..b181eb668 100644 --- a/COPYING +++ b/COPYING @@ -78,7 +78,6 @@ CVC4 optionally links against the following libraries: ABC (https://bitbucket.org/alanmi/abc) CaDiCaL (https://github.com/arminbiere/cadical) CryptoMiniSat (https://github.com/msoos/cryptominisat) - LFSC checker (https://github.com/CVC4/LFSC) LibPoly (https://github.com/SRI-CSL/libpoly) libedit (https://thrysoee.dk/editline) @@ -108,4 +107,3 @@ CVC4 can be optionally configured to link against glpk-cut-log, a modified version of GLPK, the GNU Linear Programming Kit, available here: https://github.com/timothy-king/glpk-cut-log - diff --git a/INSTALL.md b/INSTALL.md index 635118f1d..2d124b2af 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -41,7 +41,7 @@ can be found in `/lib`. ## Build dependencies -The following tools and libraries are required to build and run CVC4. +The following tools and libraries are required to build and run CVC4. Versions given are minimum versions; more recent versions should be compatible. @@ -95,7 +95,7 @@ want and should use. is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms of bit-vector operations. It is required for supporting the theory of floating-point numbers and -can be installed using the `contrib/get-symfpu` script. +can be installed using the `contrib/get-symfpu` script. Configure CVC4 with `configure.sh --symfpu` to build with this dependency. ### CaDiCaL (Optional SAT solver) @@ -103,7 +103,7 @@ Configure CVC4 with `configure.sh --symfpu` to build with this dependency. [CaDiCaL](https://github.com/arminbiere/cadical) is a SAT solver that can be used for solving non-incremental bit-vector problems with eager bit-blasting. This dependency may improve performance. -It can be installed using the `contrib/get-cadical script`. +It can be installed using the `contrib/get-cadical script`. Configure CVC4 with `configure.sh --cadical` to build with this dependency. ### CryptoMiniSat (Optional SAT solver) @@ -111,7 +111,7 @@ Configure CVC4 with `configure.sh --cadical` to build with this dependency. [CryptoMinisat](https://github.com/msoos/cryptominisat) is a SAT solver that can be used for solving bit-vector problems with eager bit-blasting. This dependency may improve performance. -It can be installed using the `contrib/get-cryptominisat` script. +It can be installed using the `contrib/get-cryptominisat` script. Configure CVC4 with `configure.sh --cryptominisat` to build with this dependency. @@ -120,16 +120,10 @@ dependency. [Kissat](https://github.com/arminbiere/kissat) is a SAT solver that can be used for solving bit-vector problems with eager bit-blasting. This dependency may improve performance. -It can be installed using the `contrib/get-kissat` script. +It can be installed using the `contrib/get-kissat` script. Configure CVC4 with `configure.sh --kissat` to build with this dependency. -### LFSC (The LFSC Proof Checker) - -[LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally -with --check-proofs. It can be installed using the `contrib/get-lfsc` script. -Configure CVC4 with `configure.sh --lfsc` to build with this dependency. - ### LibPoly (Optional polynomial library) [LibPoly](https://github.com/SRI-CSL/libpoly) is required for CAD-based nonlinear reasoning. @@ -140,7 +134,7 @@ Configure CVC4 with `configure.sh --poly` to build with this dependency. [CLN](http://www.ginac.de/CLN) is an alternative multiprecision arithmetic package that may offer better -performance and memory footprint than GMP. +performance and memory footprint than GMP. Configure CVC4 with `configure.sh --cln` to build with this dependency. Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). @@ -158,7 +152,7 @@ implementation in CVC4. (This is not recommended for most users.) glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script. Note that the only installation option is manual installation via this script. -CVC4 is no longer compatible with the main GLPK library. +CVC4 is no longer compatible with the main GLPK library. Configure CVC4 with `configure.sh --glpk` to build with this dependency. Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). @@ -174,7 +168,7 @@ 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. +ABC can be installed using the `contrib/get-abc` script. Configure CVC4 with `configure.sh --abc` to build with this dependency. ### Editline library (Improved Interactive Experience) @@ -192,7 +186,7 @@ provided with CVC4. ### Google Test Unit Testing Framework (Unit Tests) [Google Test](https://github.com/google/googletest) is required to optionally -run CVC4's unit tests (included with the distribution). +run CVC4's unit tests (included with the distribution). See [Testing CVC4](#Testing-CVC4) below for more details. ## Language bindings @@ -245,7 +239,7 @@ The system tests are not built by default. All system test binaries are built into `/bin/test/system`. We use prefix `api/` + `` (for `` in `test/api`) -as test target name. +as test target name. make ouroborous # build test/api/ouroborous.cpp ctest -R ouroborous # run all tests that match '*ouroborous*' @@ -268,7 +262,7 @@ assertions enabled. All unit test binaries are built into `/bin/test/unit`. We use prefix `unit/` + `/` + `` (for `` in -`test/unit/`) as test target name. +`test/unit/`) as test target name. make map_util_black # build test/unit/base/map_util_black.cpp ctest -R map_util_black # run all tests that match '*map_util_black*' @@ -281,7 +275,7 @@ We use prefix `unit/` + `/` + `` (for `` in ### Testing Regression Tests We use prefix `regressN/` + `/` + `` (for `` -in level `N` in `test/regress/regressN/`) as test target name. +in level `N` in `test/regress/regressN/`) as test target name. ctest -L regress # run all regression tests ctest -L regress0 # run all regression tests in level 0 @@ -295,23 +289,23 @@ in level `N` in `test/regress/regressN/`) as test target name. All custom test targets build and run a preconfigured set of tests. -- `make check [-jN] [ARGS=-jN]` +- `make check [-jN] [ARGS=-jN]` The default build-and-test target for CVC4, builds and runs all examples, all system and unit tests, and regression tests from levels 0 to 2. -- `make systemtests [-jN] [ARGS=-jN]` +- `make systemtests [-jN] [ARGS=-jN]` Build and run all system tests. -- `make units [-jN] [ARGS=-jN]` +- `make units [-jN] [ARGS=-jN]` Build and run all unit tests. -- `make regress [-jN] [ARGS=-jN]` +- `make regress [-jN] [ARGS=-jN]` Build and run regression tests from levels 0 to 2. -- `make runexamples [-jN] [ARGS=-jN]` +- `make runexamples [-jN] [ARGS=-jN]` Build and run all examples. -- `make coverage [-jN] [ARGS=-jN]` +- `make coverage [-jN] [ARGS=-jN]` Build and run all tests (system and unit tests, regression tests level 0-4) with gcov to determine code coverage. diff --git a/configure.sh b/configure.sh index d57bcd5d5..43925a504 100755 --- a/configure.sh +++ b/configure.sh @@ -32,7 +32,6 @@ The following flags enable optional features (disable with --no-