From d8104e0d48a845be7653d1a541c52dea21321aed Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 23 Mar 2021 19:27:39 -0300 Subject: Removing unused build options and deprecated proof compile flag (#6195) --- 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 ------ 9 files changed, 6 insertions(+), 111 deletions(-) (limited to 'src') 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 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() -- cgit v1.2.3