Removing unused build options and deprecated proof compile flag (#6195)

9 files changed, 6 insertions, 111 deletions

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()