diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-03-23 19:27:39 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-23 19:27:39 -0300 |
commit | d8104e0d48a845be7653d1a541c52dea21321aed (patch) | |
tree | e2ae24c92d7959bb3d877372e562a5701a113db6 | |
parent | d5d526730d11d08c65aa17ea53d0dffb0a72e692 (diff) |
Removing unused build options and deprecated proof compile flag (#6195)
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() @@ -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 `<build_dir>/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 `<build_dir>/bin/test/system`. We use prefix `api/` + `<api_test>` (for `<api_test>` 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 `<build_dir>/bin/test/unit`. We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in -`test/unit/<subdir>`) as test target name. +`test/unit/<subdir>`) 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/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in ### Testing Regression Tests We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>` -in level `N` in `test/regress/regressN/<subdir>`) as test target name. +in level `N` in `test/regress/regressN/<subdir>`) 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/<subdir>`) 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-<option name>). --static build static libraries and binaries [default=no] --static-binary statically link against system libraries (must be disabled for static macOS builds) [default=yes] - --proofs support for proof generation --debug-symbols include debug symbols --valgrind Valgrind instrumentation --debug-context-mm use the debug context memory manager @@ -60,9 +59,7 @@ The following flags enable optional packages (disable with --no-<option name>). --abc use the ABC AIG library --cadical use the CaDiCaL SAT solver --cryptominisat use the CryptoMiniSat SAT solver - --drat2er use drat2er (required for eager BV proofs) --kissat use the Kissat SAT solver - --lfsc use the LFSC proof checker --poly use the LibPoly library --symfpu use SymFPU for floating point solver --editline support the editline library @@ -72,11 +69,9 @@ Optional Path to Optional Packages: --antlr-dir=PATH path to ANTLR C headers and libraries --cadical-dir=PATH path to top level of CaDiCaL source tree --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree - --drat2er-dir=PATH path to the top level of the drat2er installation --glpk-dir=PATH path to top level of GLPK installation --gmp-dir=PATH path to top level of GMP installation --kissat-dir=PATH path to top level of Kissat source tree - --lfsc-dir=PATH path to top level of LFSC source tree --poly-dir=PATH path to top level of LibPoly source tree --symfpu-dir=PATH path to top level of SymFPU source tree @@ -123,17 +118,14 @@ coverage=default cryptominisat=default debug_context_mm=default debug_symbols=default -drat2er=default dumping=default glpk=default gpl=default kissat=default -lfsc=default poly=default muzzle=default ninja=default profiling=default -proofs=default python2=default python_bindings=default java_bindings=default @@ -155,11 +147,9 @@ abc_dir=default antlr_dir=default cadical_dir=default cryptominisat_dir=default -drat2er_dir=default glpk_dir=default gmp_dir=default kissat_dir=default -lfsc_dir=default poly_dir=default symfpu_dir=default @@ -235,9 +225,6 @@ do --debug-context-mm) debug_context_mm=ON;; --no-debug-context-mm) debug_context_mm=OFF;; - --drat2er) drat2er=ON;; - --no-drat2er) drat2er=OFF;; - --dumping) dumping=ON;; --no-dumping) dumping=OFF;; @@ -256,18 +243,12 @@ do --glpk) glpk=ON;; --no-glpk) glpk=OFF;; - --lfsc) lfsc=ON;; - --no-lfsc) lfsc=OFF;; - --poly) poly=ON;; --no-poly) poly=OFF;; --muzzle) muzzle=ON;; --no-muzzle) muzzle=OFF;; - --proofs) proofs=ON;; - --no-proofs) proofs=OFF;; - --static) shared=OFF; static_binary=ON;; --no-static) shared=ON;; @@ -320,9 +301,6 @@ do --cryptominisat-dir) die "missing argument to $1 (try -h)" ;; --cryptominisat-dir=*) cryptominisat_dir=${1##*=} ;; - --drat2er-dir) die "missing argument to $1 (try -h)" ;; - --drat2er-dir=*) drat2er_dir=${1##*=} ;; - --glpk-dir) die "missing argument to $1 (try -h)" ;; --glpk-dir=*) glpk_dir=${1##*=} ;; @@ -332,9 +310,6 @@ do --kissat-dir) die "missing argument to $1 (try -h)" ;; --kissat-dir=*) kissat_dir=${1##*=} ;; - --lfsc-dir) die "missing argument to $1 (try -h)" ;; - --lfsc-dir=*) lfsc_dir=${1##*=} ;; - --poly-dir) die "missing argument to $1 (try -h)" ;; --poly-dir=*) poly_dir=${1##*=} ;; @@ -411,8 +386,6 @@ cmake_opts="" [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja" [ $muzzle != default ] \ && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" -[ $proofs != default ] \ - && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" [ $shared != default ] \ && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared" [ $static_binary != default ] \ @@ -443,14 +416,10 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_CLN=$cln" [ $cryptominisat != default ] \ && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat" -[ $drat2er != default ] \ - && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er" [ $glpk != default ] \ && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk" [ $kissat != default ] \ && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat" -[ $lfsc != default ] \ - && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc" [ $poly != default ] \ && cmake_opts="$cmake_opts -DUSE_POLY=$poly" [ $symfpu != default ] \ @@ -463,16 +432,12 @@ cmake_opts="" && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir" [ "$cryptominisat_dir" != default ] \ && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir" -[ "$drat2er_dir" != default ] \ - && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir" [ "$glpk_dir" != default ] \ && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir" [ "$gmp_dir" != default ] \ && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir" [ "$kissat_dir" != default ] \ && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir" -[ "$lfsc_dir" != default ] \ - && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir" [ "$poly_dir" != default ] \ && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir" [ "$symfpu_dir" != default ] \ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5b7c1d8f8..44ba4e261 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1139,18 +1139,10 @@ if(USE_KISSAT) target_link_libraries(cvc4 ${Kissat_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR}) endif() -if(USE_DRAT2ER) - target_link_libraries(cvc4 ${Drat2Er_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR}) -endif() if(USE_GLPK) target_link_libraries(cvc4 ${GLPK_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR}) endif() -if(USE_LFSC) - target_link_libraries(cvc4 ${LFSC_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR}) -endif() if(USE_POLY) target_link_libraries(cvc4 ${POLY_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR}) diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index f452c7a5c..39284227a 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -66,10 +66,6 @@ bool Configuration::isAssertionBuild() { return IS_ASSERTIONS_BUILD; } -bool Configuration::isProofBuild() { - return IS_PROOFS_BUILD; -} - bool Configuration::isCoverageBuild() { return IS_COVERAGE_BUILD; } @@ -144,8 +140,7 @@ std::string Configuration::copyright() { << "See licenses/antlr3-LICENSE for copyright and licensing information." << "\n\n"; - if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc() - || Configuration::isBuiltWithCadical() + if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical() || Configuration::isBuiltWithCryptominisat() || Configuration::isBuiltWithKissat() || Configuration::isBuiltWithSymFPU() @@ -158,11 +153,6 @@ std::string Configuration::copyright() { << " See http://bitbucket.org/alanmi/abc for copyright and\n" << " licensing information.\n\n"; } - if (Configuration::isBuiltWithLfsc()) { - ss << " LFSC Proof Checker\n" - << " See http://github.com/CVC4/LFSC for copyright and\n" - << " licensing information.\n\n"; - } if (Configuration::isBuiltWithCadical()) { ss << " CaDiCaL - Simplified Satisfiability Solver\n" @@ -282,14 +272,8 @@ bool Configuration::isBuiltWithCryptominisat() { bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; } -bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; } - bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; } -bool Configuration::isBuiltWithLfsc() { - return IS_LFSC_BUILD; -} - bool Configuration::isBuiltWithPoly() { return IS_POLY_BUILD; diff --git a/src/base/configuration.h b/src/base/configuration.h index aab136374..ec8cc879b 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -58,8 +58,6 @@ public: static bool isAssertionBuild(); - static bool isProofBuild(); - static bool isCoverageBuild(); static bool isProfilingBuild(); @@ -106,12 +104,8 @@ public: static bool isBuiltWithKissat(); - static bool isBuiltWithDrat2Er(); - static bool isBuiltWithEditline(); - static bool isBuiltWithLfsc(); - static bool isBuiltWithPoly(); static bool isBuiltWithSymFPU(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 835a02a44..cc1983734 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -60,12 +60,6 @@ namespace CVC4 { # define IS_ASSERTIONS_BUILD false #endif /* CVC4_ASSERTIONS */ -#ifdef CVC4_PROOF -# define IS_PROOFS_BUILD true -#else /* CVC4_PROOF */ -# define IS_PROOFS_BUILD false -#endif /* CVC4_PROOF */ - #ifdef CVC4_COVERAGE # define IS_COVERAGE_BUILD true #else /* CVC4_COVERAGE */ @@ -120,24 +114,12 @@ namespace CVC4 { # define IS_CRYPTOMINISAT_BUILD false #endif /* CVC4_USE_CRYPTOMINISAT */ -#if CVC4_USE_DRAT2ER -# define IS_DRAT2ER_BUILD true -#else /* CVC4_USE_DRAT2ER */ -# define IS_DRAT2ER_BUILD false -#endif /* CVC4_USE_DRAT2ER */ - #if CVC4_USE_KISSAT #define IS_KISSAT_BUILD true #else /* CVC4_USE_KISSAT */ #define IS_KISSAT_BUILD false #endif /* CVC4_USE_KISSAT */ -#if CVC4_USE_LFSC -#define IS_LFSC_BUILD true -#else /* CVC4_USE_LFSC */ -#define IS_LFSC_BUILD false -#endif /* CVC4_USE_LFSC */ - #if CVC4_USE_POLY #define IS_POLY_BUILD true #else /* CVC4_USE_POLY */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b1cbca05b..ee3242067 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -253,36 +253,6 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) options::interactiveMode.set(value); } -void OptionsHandler::proofEnabledBuild(std::string option, bool value) -{ -#ifdef CVC4_PROOF - if (value && options::bitblastMode() == options::BitblastMode::EAGER - && options::bvSatSolver() != options::SatSolverMode::MINISAT - && options::bvSatSolver() != options::SatSolverMode::CRYPTOMINISAT) - { - throw OptionException( - "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used"); - } -#else - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_PROOF */ -} - -void OptionsHandler::LFSCEnabledBuild(std::string option, bool value) { -#ifndef CVC4_USE_LFSC - if (value) { - std::stringstream ss; - ss << "option `" << option << "' requires a build of CVC4 with integrated " - "LFSC; this binary was not built with LFSC"; - throw OptionException(ss.str()); - } -#endif /* CVC4_USE_LFSC */ -} - void OptionsHandler::statsEnabledBuild(std::string option, bool value) { #ifndef CVC4_STATISTICS_ON @@ -347,7 +317,7 @@ void OptionsHandler::showConfiguration(std::string option) { } else { print_config_cond("scm", false); } - + std::cout << std::endl; std::stringstream ss; @@ -355,7 +325,7 @@ void OptionsHandler::showConfiguration(std::string option) { << Configuration::getVersionMinor() << "." << Configuration::getVersionRelease(); print_config("library", ss.str()); - + std::cout << std::endl; print_config_cond("debug code", Configuration::isDebugBuild()); @@ -364,29 +334,26 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("dumping", Configuration::isDumpingBuild()); print_config_cond("muzzled", Configuration::isMuzzledBuild()); print_config_cond("assertions", Configuration::isAssertionBuild()); - print_config_cond("proof", Configuration::isProofBuild()); print_config_cond("coverage", Configuration::isCoverageBuild()); print_config_cond("profiling", Configuration::isProfilingBuild()); print_config_cond("asan", Configuration::isAsanBuild()); print_config_cond("ubsan", Configuration::isUbsanBuild()); print_config_cond("tsan", Configuration::isTsanBuild()); print_config_cond("competition", Configuration::isCompetitionBuild()); - + std::cout << std::endl; - + print_config_cond("abc", Configuration::isBuiltWithAbc()); print_config_cond("cln", Configuration::isBuiltWithCln()); print_config_cond("glpk", Configuration::isBuiltWithGlpk()); print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); - print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("kissat", Configuration::isBuiltWithKissat()); - print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("poly", Configuration::isBuiltWithPoly()); print_config_cond("editline", Configuration::isBuiltWithEditline()); print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); - + exit(0); } diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 18e8a917a..b24fb032f 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -86,8 +86,6 @@ public: * initialization. */ void setProduceAssertions(std::string option, bool value); - void proofEnabledBuild(std::string option, bool value); - void LFSCEnabledBuild(std::string option, bool value); void statsEnabledBuild(std::string option, bool value); diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 787a60e78..2d678ec2b 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -198,7 +198,6 @@ header = "options/smt_options.h" category = "regular" long = "produce-unsat-cores" type = "bool" - predicates = ["proofEnabledBuild"] help = "turn on unsat core generation" [[option]] @@ -238,7 +237,6 @@ header = "options/smt_options.h" long = "produce-unsat-assumptions" type = "bool" default = "false" - predicates = ["proofEnabledBuild"] read_only = true help = "turn on unsat assumptions generation" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4f4d983c5..f10439156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -150,9 +150,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // d_proofManager must be created before Options has been finished // being parsed from the input file. Because of this, we cannot trust // that options::unsatCores() is set correctly yet. -#ifdef CVC4_PROOF d_proofManager.reset(new ProofManager(getUserContext())); -#endif d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); } @@ -331,9 +329,7 @@ SmtEngine::~SmtEngine() // Note: the proof manager must be destroyed before the theory engine. // Because the destruction of the proofs depends on contexts owned be the // theory solvers. -#ifdef CVC4_PROOF d_proofManager.reset(nullptr); -#endif d_pfManager.reset(nullptr); d_ucManager.reset(nullptr); @@ -1406,7 +1402,6 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() UnsatCore SmtEngine::getUnsatCoreInternal() { -#if IS_PROOFS_BUILD if (!options::unsatCores()) { throw ModalException( @@ -1433,11 +1428,6 @@ UnsatCore SmtEngine::getUnsatCoreInternal() std::vector<Node> core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); return UnsatCore(core); -#else /* IS_PROOFS_BUILD */ - throw ModalException( - "This build of CVC4 doesn't have proof support (required for unsat " - "cores)."); -#endif /* IS_PROOFS_BUILD */ } void SmtEngine::checkUnsatCore() { @@ -1539,7 +1529,6 @@ std::string SmtEngine::getProof() { getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); } -#if IS_PROOFS_BUILD if (!options::produceProofs()) { throw ModalException("Cannot get a proof when proof option is off."); @@ -1558,9 +1547,6 @@ std::string SmtEngine::getProof() std::ostringstream ss; d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions); return ss.str(); -#else /* IS_PROOFS_BUILD */ - throw ModalException("This build of CVC4 doesn't have proof support."); -#endif /* IS_PROOFS_BUILD */ } void SmtEngine::printInstantiations( std::ostream& out ) { diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index cc528f89c..2aa96dfbb 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -35,14 +35,8 @@ SmtEngine* currentSmtEngine() { bool smtEngineInScope() { return s_smtEngine_current != NULL; } ProofManager* currentProofManager() { -#if IS_PROOFS_BUILD Assert(s_smtEngine_current != NULL); return s_smtEngine_current->getProofManager(); -#else /* IS_PROOFS_BUILD */ - InternalError() - << "proofs/unsat cores are not on, but ProofManager requested"; - return NULL; -#endif /* IS_PROOFS_BUILD */ } ResourceManager* currentResourceManager() diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3caa1250e..35d640869 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -43,7 +43,3 @@ if(ENABLE_UNIT_TESTING) add_subdirectory(java) endif() endif() - -if(LFSC_BINARY) - add_subdirectory(signatures) -endif() diff --git a/test/regress/regress0/arrays/issue3814.smt2 b/test/regress/regress0/arrays/issue3814.smt2 index 6c557d99d..6e4a41338 100644 --- a/test/regress/regress0/arrays/issue3814.smt2 +++ b/test/regress/regress0/arrays/issue3814.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-unsat-cores ; EXPECT: sat (set-logic QF_AX) diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2 index 80b8126a0..9bba5f141 100644 --- a/test/regress/regress0/bv/ackermann2.smt2 +++ b/test/regress/regress0/bv/ackermann2.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores ; REQUIRES: cryptominisat -; REQUIRES: drat2er ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_UFBV) diff --git a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 index 32680d862..406041937 100644 --- a/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 +++ b/test/regress/regress0/bv/bv_to_int_5230_binary.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; EXPECT: sat (set-logic QF_UFBV) (set-option :produce-unsat-cores true) diff --git a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 index 757b00e5f..497fbaab1 100644 --- a/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 +++ b/test/regress/regress0/bv/bv_to_int_5230_missing_op.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; EXPECT: sat (set-logic ABV) (set-option :check-unsat-cores true) diff --git a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 index e94e0cae5..a8d0144f1 100644 --- a/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 +++ b/test/regress/regress0/bv/bv_to_int_5230_shift_const.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; EXPECT: sat (set-logic QF_UFBV) (set-option :check-unsat-cores true) @@ -7,6 +6,6 @@ (declare-const v5 Bool) (declare-const v8 Bool) (declare-const v9 Bool) -(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110))) +(assert (or (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110) v9 (= #b1001110 ((_ sign_extend 0) #b1001110) #b1001110 #b1001110 ((_ sign_extend 0) #b1001110)) v5 (distinct ((_ sign_extend 0) #b1001110) (bvlshr #b1001110 #b1001110) ((_ sign_extend 0) #b1001110) #b1001110))) (assert (or v0 v8)) (check-sat) diff --git a/test/regress/regress0/bv/core/slice-12.smtv1.smt2 b/test/regress/regress0/bv/core/slice-12.smtv1.smt2 index d66b27caa..f370c0f0f 100644 --- a/test/regress/regress0/bv/core/slice-12.smtv1.smt2 +++ b/test/regress/regress0/bv/core/slice-12.smtv1.smt2 @@ -1,5 +1,4 @@ ; REQUIRES: cryptominisat -; REQUIRES: drat2er ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores ; EXPECT: unsat (set-option :incremental false) diff --git a/test/regress/regress0/dump-unsat-core-full.smt2 b/test/regress/regress0/dump-unsat-core-full.smt2 index 3c68501f9..a21508efb 100644 --- a/test/regress/regress0/dump-unsat-core-full.smt2 +++ b/test/regress/regress0/dump-unsat-core-full.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --dump-unsat-cores-full ; EXPECT: unsat ; EXPECT: ( diff --git a/test/regress/regress0/nl/issue3959.smt2 b/test/regress/regress0/nl/issue3959.smt2 index cce64a848..eccd6b301 100644 --- a/test/regress/regress0/nl/issue3959.smt2 +++ b/test/regress/regress0/nl/issue3959.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-unsat-cores --incremental ; EXPECT: sat diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 index 274fc213f..0c8c21f01 100644 --- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full ; EXPECT: unsat ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x))) diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2 index adb38add0..86f5fe133 100644 --- a/test/regress/regress1/sygus-abduct-test-ccore.smt2 +++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 index ed1d5c862..bb02ebce2 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-abducts ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2 index dda5e9751..98bf70fd7 100644 --- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 +++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 index 691cf6d9a..1595b0865 100644 --- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 +++ b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2 index b6a422035..b466ab33e 100644 --- a/test/regress/regress1/sygus/abduction_streq.readable.smt2 +++ b/test/regress/regress1/sygus/abduction_streq.readable.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: proof ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy index c2404a12c..9009c8260 100644 --- a/test/regress/regress1/sygus/array_search_2.sy +++ b/test/regress/regress1/sygus/array_search_2.sy @@ -1,4 +1,3 @@ -; REQUIRES: proof ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index fb4786331..01924559a 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -10,12 +10,6 @@ ## directory for licensing information. ## """ -Usage: - - run_regression.py [--enable-proof] [--with-lfsc] [--dump] - [--use-skip-return-code] [wrapper] cvc4-binary - [benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p] - Runs benchmark and checks for correct exit status and output. """ @@ -193,11 +187,6 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary) - # Disable proof and unsat core checks if CVC4 was not compiled with proofs. - if 'proof' not in cvc4_features: - check_unsat_cores = False - check_proofs = False - basic_command_line_args = [] benchmark_basename = os.path.basename(benchmark_path) diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 71568e337..f63f3f315 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -40,10 +40,6 @@ macro(cvc4_add_unit_test is_white name output_dir) target_link_libraries(${name} main-test) target_link_libraries(${name} GTest::GTest) target_link_libraries(${name} GTest::Main) - if(USE_LFSC) - # We don't link against LFSC, because CVC4 is already linked against it. - target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) - endif() if(USE_POLY) # We don't link against libpoly, because CVC4 is already linked against it. target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 18a8f9cc8..6b6a0fa0f 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1346,59 +1346,48 @@ TEST_F(TestApiBlackSolver, getOption) TEST_F(TestApiBlackSolver, getUnsatAssumptions1) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "false"); d_solver.checkSatAssuming(d_solver.mkFalse()); ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); -#endif } TEST_F(TestApiBlackSolver, getUnsatAssumptions2) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-assumptions", "false"); d_solver.checkSatAssuming(d_solver.mkFalse()); ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); -#endif } TEST_F(TestApiBlackSolver, getUnsatAssumptions3) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-assumptions", "true"); d_solver.checkSatAssuming(d_solver.mkFalse()); ASSERT_NO_THROW(d_solver.getUnsatAssumptions()); d_solver.checkSatAssuming(d_solver.mkTrue()); ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException); -#endif } TEST_F(TestApiBlackSolver, getUnsatCore1) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "false"); d_solver.assertFormula(d_solver.mkFalse()); d_solver.checkSat(); ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException); -#endif } TEST_F(TestApiBlackSolver, getUnsatCore2) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "false"); d_solver.setOption("produce-unsat-cores", "false"); d_solver.assertFormula(d_solver.mkFalse()); d_solver.checkSat(); ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException); -#endif } TEST_F(TestApiBlackSolver, getUnsatCore3) { -#if IS_PROOFS_BUILD d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-cores", "true"); @@ -1434,9 +1423,8 @@ TEST_F(TestApiBlackSolver, getUnsatCore3) { d_solver.assertFormula(t); } - Result res = d_solver.checkSat(); + CVC4::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isUnsat()); -#endif } TEST_F(TestApiBlackSolver, getValue1) |