Merge pull request #535 from vprover/michael-cleanup-system

remove unused functions in `Lib::System`
vprover · Mar 14, 2024 · 69aa640 · 69aa640
2 parents a16758b + e0b0d7a
commit 69aa640
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 93 deletions.
diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp
@@ -638,16 +638,8 @@ void PortfolioMode::runSlice(Options& strategyOpt)
   if (env.statistics->terminationReason == Statistics::REFUTATION ||
       env.statistics->terminationReason == Statistics::SATISFIABLE) {
     resultValue=0;
-
-    /*
-     env.beginOutput();
-     lineOutput() << " found solution " << endl;
-     env.endOutput();
-    */
   }
 
-  System::ignoreSIGHUP(); // don't interrupt now, we need to finish printing the proof !
-
   bool outputResult = false;
   if (!resultValue) {
     // only successfull vampires get here

diff --git a/Lib/System.cpp b/Lib/System.cpp
@@ -22,9 +22,6 @@
 // TODO these should probably be guarded
 // for getpid, _exit
 #include <unistd.h>
-// for listing directory items
-// C++17: use std::filesystem
-#include <dirent.h>
 
 #ifdef __linux__
 #include <sys/prctl.h>
@@ -49,8 +46,6 @@ namespace Lib {
 
 using namespace std;
 
-bool System::s_shouldIgnoreSIGINT = false;
-bool System::s_shouldIgnoreSIGHUP = false;
 const char* System::s_argv0 = 0;
 
 const char* signalToString (int sigNum)
@@ -132,18 +127,12 @@ void handleSignal (int sigNum)
 # endif
 
     case SIGINT:
-      if(System::shouldIgnoreSIGINT()) {
-	return;
-      }
       haveSigInt=true;
       System::terminateImmediately(VAMP_RESULT_STATUS_SIGINT);
 //      exit(0);
 //      return;
 
     case SIGHUP:
-      if(System::shouldIgnoreSIGHUP()) {
-  return;
-      }
     case SIGILL:
     case SIGFPE:
     case SIGSEGV:
@@ -274,15 +263,6 @@ void System::registerForSIGHUPOnParentDeath()
 #endif
 }
 
-vstring System::extractFileNameFromPath(vstring str)
-{
-  size_t index=str.find_last_of("\\/")+1;
-  if(index==vstring::npos) {
-    return str;
-  }
-  return vstring(str, index);
-}
-
 /**
  * If directory name can be extracted from @c path, assign it into
  * @c dir and return true; otherwise return false.
@@ -305,51 +285,4 @@ bool System::fileExists(vstring fname)
   return ifile.good();
 }
 
-// C++17: use std::filesystem
-void System::readDir(vstring dirName, Stack<vstring>& filenames)
-{
-  DIR *dirp;
-  struct dirent *dp;
-
-  static Stack<vstring> todo;
-  ASS(todo.isEmpty());
-  todo.push(dirName);
-
-  while (todo.isNonEmpty()) {
-    vstring dir = todo.pop();
-
-    dirp = opendir(dir.c_str());
-
-    if (!dirp) {
-      // cout << "Cannot open dir " << dir << endl;
-      continue;
-    }
-
-    while ((dp = readdir(dirp)) != NULL) {
-      if (strncmp(dp->d_name, ".", 1) == 0) {
-        continue;
-      }
-      if (strncmp(dp->d_name, "..", 2) == 0) {
-        continue;
-      }
-
-      switch (dp->d_type) {
-        case DT_REG:
-          filenames.push(dir+"/"+dp->d_name);
-          break;
-        case DT_DIR:
-          // cout << "seen dir " << dp->d_name << endl;
-          todo.push(dir+"/"+dp->d_name);
-          break;
-        default:
-          ;
-          // cout << "weird file type" << endl;
-      }
-    }
-    (void)closedir(dirp);
-  }
-
-  todo.reset();
-}
-
 };
diff --git a/Lib/System.hpp b/Lib/System.hpp
@@ -31,29 +31,14 @@ namespace Lib {
 class System {
 public:
   static void setSignalHandlers();
-  static vstring extractFileNameFromPath(vstring str);
   static bool extractDirNameFromPath(vstring path, vstring& dir);
 
-  static void ignoreSIGINT() { s_shouldIgnoreSIGINT=true; }
-  static void heedSIGINT() { s_shouldIgnoreSIGINT=false; }
-  static bool shouldIgnoreSIGINT() { return s_shouldIgnoreSIGINT; }
-
-  static void ignoreSIGHUP() { s_shouldIgnoreSIGHUP=true; }
-  static void heedSIGHUP() { s_shouldIgnoreSIGHUP=false; }
-  static bool shouldIgnoreSIGHUP() { return s_shouldIgnoreSIGHUP; }
-
   static void addTerminationHandler(VoidFunc proc, unsigned priority=0);
   static void onTermination();
   [[noreturn]] static void terminateImmediately(int resultStatus);
 
   static void registerForSIGHUPOnParentDeath();
 
-  /**
-   * Collect filenames of all the files occurring in the given directory.
-   * Recursive traverse subdirs.
-   */
-  static void readDir(vstring dirName, Stack<vstring>& filenames);
-
   /**
    * Register the value of the argv[0] argument of the main function, so that
    * it can be later used to determine the executable directory
@@ -76,9 +61,6 @@ class System {
    */
   static ZIArray<List<VoidFunc>*>& terminationHandlersArray();
 
-  static bool s_shouldIgnoreSIGINT;
-  static bool s_shouldIgnoreSIGHUP;
-
   static const char* s_argv0;
 };
 

diff --git a/Shell/Options.cpp b/Shell/Options.cpp
@@ -2409,6 +2409,13 @@ Options::OptionProblemConstraintUP Options::isRandSat(){
  * @since 16/10/2003 Manchester, relativeName changed to string from char*
  * @since 07/08/2014 Manchester, relativeName changed to vstring
  */
+// TODO this behaviour isn't quite right, at least:
+// 1. we use the *root* file to resolve relative paths, which won't work if we have an axiom file that includes another
+// 2. checks current directory, which spec doesn't ask for
+// 3. checks our "-include" option, which isn't in the spec either (OK if someone relies on it, I guess)
+// cf https://tptp.org/TPTP/TR/TPTPTR.shtml#IncludeSection
+// probable solution: move all this logic into TPTP parser and do it properly there
+
 vstring Options::includeFileName (const vstring& relativeName)
 {
   if (relativeName[0] == '/') { // absolute name