removed COMPILER_MSVC

ModelWriter · Sep 18, 2017 · d89459b · d89459b
1 parent acd1748
commit d89459b
Show file tree

Hide file tree

Showing 27 changed files with 2 additions and 318 deletions.
diff --git a/CASC/CASCMode.cpp b/CASC/CASCMode.cpp
@@ -36,11 +36,7 @@ bool CASCMode::perform(int argc, char* argv [])
 
   env.timer->makeChildrenIncluded();
 
-#if COMPILER_MSVC
-  SpawningCM cm(argv[0]);
-#else
   ForkingCM cm;
-#endif
 
   bool res=cm.perform();
 

diff --git a/CASC/CASCMultiMode.cpp b/CASC/CASCMultiMode.cpp
@@ -9,8 +9,6 @@
 
 #include "Lib/Portability.hpp"
 
-#if !COMPILER_MSVC
-
 #include "Lib/DHSet.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Exception.hpp"
@@ -415,5 +413,3 @@ ostream& CASCMultiMode::coutLineOutput()
   CALL("CASCMultiMode::lineOutput");
   return cout << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") ";
 } // CASCMultiMode::coutLineOutput
-
-#endif //!COMPILER_MSVC
diff --git a/CASC/CASCMultiMode.hpp b/CASC/CASCMultiMode.hpp
@@ -31,17 +31,6 @@ using namespace Lib;
 using namespace Kernel;
 
 
-
-#if COMPILER_MSVC
-
-class CASCMultiMode
-{
-public:
-  static bool perform() { USER_ERROR("multi-core casc  mode is not supported on Windows"); }
-};
-
-#else
-
 class CASCMultiMode
 {
     enum {
@@ -96,8 +85,6 @@ class CASCMultiMode
   Semaphore _syncSemaphore; // semaphore for synchronizing proof printing
 };
 
-#endif //!COMPILER_MSVC
-
 }
 
 #endif // __CASCMultiMode__
diff --git a/CASC/CLTBMode.cpp b/CASC/CLTBMode.cpp
@@ -11,8 +11,6 @@
 
 #include "Lib/Portability.hpp"
 
-#if !COMPILER_MSVC
-
 #include "Lib/DHSet.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Exception.hpp"
@@ -1567,5 +1565,3 @@ ostream& CLTBMode::coutLineOutput()
   CALL("CLTBMode::lineOutput");
   return cout << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") ";
 } // CLTBMode::coutLineOutput
-
-#endif //!COMPILER_MSVC
diff --git a/CASC/CLTBMode.hpp b/CASC/CLTBMode.hpp
@@ -31,17 +31,6 @@ using namespace Lib;
 using namespace Kernel;
 
 
-
-#if COMPILER_MSVC
-
-class CLTBMode
-{
-public:
-  static void perform() { USER_ERROR("casc_ltb mode is not supported on Windows"); }
-};
-
-#else
-
 enum Category {
   HH4,
   ISA,
@@ -184,8 +173,6 @@ class CLTBProblem
   };
 };
 
-#endif //!COMPILER_MSVC
-
 }
 
 #endif // __CLTBMode__
diff --git a/CASC/CLTBModeLearning.cpp b/CASC/CLTBModeLearning.cpp
@@ -11,8 +11,6 @@
 
 #include "Lib/Portability.hpp"
 
-#if !COMPILER_MSVC
-
 #include "Lib/DHSet.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Exception.hpp"
@@ -1213,4 +1211,3 @@ ostream& CLTBModeLearning::coutLineOutput()
   return cout << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") ";
 } // CLTBModeLearning::coutLineOutput
 
-#endif //!COMPILER_MSVC
diff --git a/CASC/CLTBModeLearning.hpp b/CASC/CLTBModeLearning.hpp
@@ -31,18 +31,6 @@ using namespace std;
 using namespace Lib;
 using namespace Kernel;
 
-
-
-#if COMPILER_MSVC
-
-class CLTBModeLearning
-{
-public:
-  static void perform() { USER_ERROR("casc_ltb mode is not supported on Windows"); }
-};
-
-#else
-
 class CLTBProblemLearning;
 
   struct ProbRecord{
@@ -191,8 +179,6 @@ class CLTBProblemLearning
 
 };
 
-#endif //!COMPILER_MSVC
-
 }
 
 #endif // __CLTBModeLearning__
diff --git a/CASC/CMZRMode.cpp b/CASC/CMZRMode.cpp
@@ -10,8 +10,6 @@
 
 #include "Lib/Portability.hpp"
 
-#if !COMPILER_MSVC
-
 #include "Lib/DHSet.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Exception.hpp"
@@ -1654,6 +1652,3 @@ void CMZRMode::getStrategy(Property& property, StringStack& res)
   res.loadFromIterator(StringStack::TopFirstIterator(fallback));
   res.loadFromIterator(StringStack::TopFirstIterator(quick));
 }
-
-
-#endif //!COMPILER_MSVC
diff --git a/CASC/CMZRMode.hpp b/CASC/CMZRMode.hpp
@@ -30,16 +30,6 @@ using namespace std;
 using namespace Lib;
 using namespace Kernel;
 
-#if COMPILER_MSVC
-
-class CMZRMode
-{
-public:
-  static void perform() { USER_ERROR("casc_mzr mode is not supported on Windows"); }
-};
-
-#else
-
 class CMZRProblem;
 
 class CMZRMode
@@ -127,9 +117,6 @@ class CMZRMode
   friend class CMZRProblem;
 };
 
-
-#endif //!COMPILER_MSVC
-
 }
 
 #endif // __CMZRMode__
diff --git a/CASC/ForkingCM.cpp b/CASC/ForkingCM.cpp
@@ -5,8 +5,6 @@
 
 #include "Lib/Portability.hpp"
 
-#if !COMPILER_MSVC
-
 #include <cerrno>
 #include <ctime>
 #include <stdlib.h>
@@ -145,12 +143,8 @@ void ForkingCM::childRun(Options& strategyOpt)
   ProvingHelper::runVampire(*_prb,opt);
 
   //set return value to zero if we were successful
-#if SATISFIABLE_IS_SUCCESS
   if(env.statistics->terminationReason==Statistics::REFUTATION ||
       env.statistics->terminationReason==Statistics::SATISFIABLE) {
-#else
-  if(env.statistics->terminationReason==Statistics::REFUTATION) {
-#endif
     resultValue=0;
   }
 
@@ -162,5 +156,3 @@ void ForkingCM::childRun(Options& strategyOpt)
 }
 
 }
-
-#endif // !COMPILER_MSVC
diff --git a/CASC/ForkingCM.hpp b/CASC/ForkingCM.hpp
@@ -21,17 +21,6 @@ namespace CASC
 using namespace Lib;
 using namespace Kernel;
 
-#if COMPILER_MSVC
-
-class ForkingCM
-: public CASCMode
-{
-  ForkingCM() { INVALID_OPERATION("Forking CASC mode is not supported on the Windows platform."); }
-  bool runSlice(Options& opt) { ASSERTION_VIOLATION; }
-};
-
-#else
-
 class ForkingCM
 : public CASCMode
 {
@@ -46,8 +35,6 @@ class ForkingCM
   ScopedPtr<Problem> _prb;
 };
 
-#endif
-
 }
 
 #endif // __ForkingCM__
diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp
@@ -40,12 +40,10 @@ using namespace std;
 using namespace Lib;
 using namespace Kernel;
 
-#if !COMPILER_MSVC 
 const unsigned Term::SF_ITE;
 const unsigned Term::SF_LET;
 const unsigned Term::SF_FORMULA;
 const unsigned Term::SPECIAL_FUNCTOR_LOWER_BOUND;
-#endif
 
 /**
  * Allocate enough bytes to fit a term of a given arity.

diff --git a/Lib/Portability.hpp b/Lib/Portability.hpp
@@ -6,12 +6,6 @@
 //////////////////////////////////////////////////////
 // Detect compiler
 
-#ifdef _MSC_VER
-# define COMPILER_MSVC 1
-#else
-# define COMPILER_MSVC 0
-#endif
-
 #ifndef __APPLE__
 # define __APPLE__ 0
 #endif
@@ -80,29 +74,9 @@ ASS_STATIC(sizeof(char)==1);
 # endif
 #endif
 
-
-//////////////////////////////////////////////////////
-// Fix compiler-specific problems
-
-#if COMPILER_MSVC
-
-#define int32_t __int32
-#define pid_t __int32
-
-#endif
-
-
 //////////////////////////////////////////////////////
 // Attempt to detect endianness
 
-#if COMPILER_MSVC
-
-//is this always true??
-#define HASH_LITTLE_ENDIAN 1
-#define HASH_BIG_ENDIAN 0
-
-#else
-
 #include <sys/param.h>  
 #ifdef linux
 # include <endian.h>    
@@ -128,6 +102,4 @@ ASS_STATIC(sizeof(char)==1);
 # define HASH_BIG_ENDIAN 0
 #endif
 
-#endif
-
 #endif /*__Portability__*/