Merge pull request #577 from vprover/michael-timer

replace signal-based Timer with a ticking thread

CASC/PortfolioMode.cpp

@@ -109,11 +109,11 @@ bool PortfolioMode::perform(Problem* problem)
   if (outputAllowed()) {
     if (resValue) {
       addCommentSignForSZS(cout);
-      cout<<"Success in time "<<Timer::msToSecondsString(env.timer->elapsedMilliseconds())<<endl;
+      cout<<"Success in time "<<Timer::msToSecondsString(Timer::elapsedMilliseconds())<<endl;
     }
     else {
       addCommentSignForSZS(cout);
-      cout<<"Proof not found in time "<<Timer::msToSecondsString(env.timer->elapsedMilliseconds())<<endl;
+      cout<<"Proof not found in time "<<Timer::msToSecondsString(Timer::elapsedMilliseconds())<<endl;
       if (env.remainingTime()/100>0) {
         addCommentSignForSZS(cout);
         cout<<"SZS status GaveUp for "<<env.options->problemName()<<endl;
@@ -166,7 +166,7 @@ bool PortfolioMode::searchForProof()
   }
 
   // now all the cpu usage will be in children, we'll just be waiting for them
-  Timer::setLimitEnforcement(false);
+  Timer::disableLimitEnforcement();
 
   return prepareScheduleAndPerform(*property);
 }
@@ -439,7 +439,7 @@ bool PortfolioMode::runSchedule(Schedule schedule) {
   Set<pid_t> processes;
   bool success = false;
   int remainingTime;
-  while(Timer::syncClock(), remainingTime = env.remainingTime() / 100, remainingTime > 0)
+  while(remainingTime = env.remainingTime() / 100, remainingTime > 0)
   {
     // running under capacity, wake up more tasks
     while(processes.size() < _numWorkers)
@@ -633,12 +633,6 @@ void PortfolioMode::runSlice(Options& strategyOpt)
   System::registerForSIGHUPOnParentDeath();
   UIHelper::portfolioParent=false;
 
-  env.timer->reset();
-  env.timer->start();
-
-  Timer::resetInstructionMeasuring();
-  Timer::setLimitEnforcement(true);
-
   Options opt = strategyOpt;
   //we have already performed the normalization (or don't care about it)
   opt.setNormalize(false);
@@ -655,6 +649,8 @@ void PortfolioMode::runSlice(Options& strategyOpt)
       ")" << endl;
   }
 
+  Timer::reinitialise(); // timer only when done talking (otherwise output may get mangled)
+
   Saturation::ProvingHelper::runVampire(*_prb, opt);
 
   bool succeeded =

FMB/FiniteModelBuilder.cpp

@@ -1601,9 +1601,6 @@ MainLoopResult FiniteModelBuilder::runImpl()
       }
       cout << "]" << endl;
     }
-    Timer::syncClock();
-    if(env.timeLimitReached()){ return MainLoopResult(Statistics::TIME_LIMIT); }
-
     {
     TIME_TRACE("fmb constraint creation");
 
@@ -1900,7 +1897,7 @@ void FiniteModelBuilder::onModelFound()
    UIHelper::satisfiableStatusWasAlreadyOutput = true;
  }
   // Prevent timing out whilst the model is being printed
-  Timer::setLimitEnforcement(false);
+  Timer::disableLimitEnforcement();
 
 
  DHMap<unsigned,unsigned> vampireSortSizes;

FMB/FunctionRelationshipInference.cpp

@@ -17,7 +17,6 @@
 #include "Lib/DHSet.hpp"
 #include "Lib/Stack.hpp"
 #include "Lib/Environment.hpp"
-#include "Lib/Timer.hpp"
 #include "Lib/IntUnionFind.hpp"
 
 #include "Kernel/Problem.hpp"
@@ -64,28 +63,22 @@ void FunctionRelationshipInference::findFunctionRelationships(ClauseIterator cla
   Problem prb(cit,false);
   Options opt; // default saturation algorithm options
 
-  // because of bad things the time limit is actually taken from env!
-  int oldTimeLimit = env.options->timeLimitInDeciseconds();
   Problem* inputProblem = env.getMainProblem();
   env.setMainProblem(&prb);
   unsigned useTimeLimit = env.options->fmbDetectSortBoundsTimeLimit();
-  env.options->setTimeLimitInSeconds(useTimeLimit);
   opt.setSplitting(false);
-  Timer::setLimitEnforcement(false);
 
   LabelFinder* labelFinder = new LabelFinder();
 
   try{
     SaturationAlgorithm* salg = SaturationAlgorithm::createFromOptions(prb,opt);
     salg->setLabelFinder(labelFinder);
-    MainLoopResult sres(salg->run());
-    (void)sres; //TODO do we even care about sres?
+    salg->setSoftTimeLimit(useTimeLimit);
+    salg->run();
   }catch (TimeLimitExceededException&){
     // This is expected behaviour
   }
 
-  Timer::setLimitEnforcement(true);
-  env.options->setTimeLimitInDeciseconds(oldTimeLimit);
   env.setMainProblem(inputProblem);
 
   Stack<unsigned> foundLabels = labelFinder->getFoundLabels();

Forwards.hpp

@@ -20,7 +20,6 @@
 namespace Lib
 {
 struct EmptyStruct {};
-typedef void (*VoidFunc)();
 
 template<typename T> class VirtualIterator;
 
@@ -37,7 +36,6 @@ template<typename T> class SharedSet;
 
 typedef List<int> IntList;
 typedef Stack<std::string> StringStack;
-typedef List<VoidFunc> VoidFuncList;
 
 class DefaultHash;
 class DefaultHash2;
@@ -47,8 +45,6 @@ template <typename Key, typename Val, class Hash1=DefaultHash, class Hash2=Defau
 template <typename Val, class Hash1=DefaultHash, class Hash2=DefaultHash2> class DHSet;
 template <typename Val, class Hash1=DefaultHash, class Hash2=DefaultHash2> class DHMultiset;
 template <typename Val, class Hash=DefaultHash> class Set;
-
-class Timer;
 };
 
 namespace Kernel

Kernel/MLMatcher.cpp

@@ -399,7 +399,6 @@ class MLMatcher::Impl final
     // For backtracking support
     DArray<unsigned> s_matchRecord;
     unsigned s_currBLit;
-    int s_counter;
     bool s_multiset;
 
     MLMatchStats stats;
@@ -560,7 +559,6 @@ void MLMatcher::Impl::init(Literal** baseLits, unsigned baseLen, Clause* instanc
 
   s_matchingData.nextAlts[0] = 0;
   s_currBLit = 0;
-  s_counter = 0;
   s_multiset = multiset;
 
   stats = MLMatchStats{};
@@ -646,15 +644,6 @@ bool MLMatcher::Impl::nextMatch()
       if(s_currBLit==0) { return false; }
       s_currBLit--;
     }
-
-    s_counter++;
-    if(s_counter==50000) {
-      s_counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
-
   } // while (true)
 
   ASSERTION_VIOLATION; // unreachable

Kernel/MLMatcherSD.cpp

@@ -741,8 +741,6 @@ class MLMatcherSD::Impl final
     DArray<pair<int,int> > s_intersectionData;
 
     MatchingData s_matchingData;
-
-    int s_counter;
 };
 
 
@@ -889,8 +887,6 @@ void MLMatcherSD::Impl::init(Literal** baseLits, unsigned baseLen, Clause* insta
     std::cerr << "\tinstance: " << instance->toString() << std::endl;
 #endif
   initMatchingData(baseLits, baseLen, instance, alts);
-
-  s_counter = 0;
 }
 
 
@@ -1060,16 +1056,6 @@ bool MLMatcherSD::Impl::nextMatch()
         return false;
       }
     }
-
-    // Ensure vampire exits timely in pathological cases instead of appearing to be stuck
-    s_counter++;
-    if(s_counter==50000) {
-      // std::cerr << "counter reached 50k" << std::endl;
-      s_counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
   } // while (true)
 
   // We found a complete match

Kernel/MLVariant.cpp

@@ -410,8 +410,6 @@ bool MLVariant::isVariant(Literal* const * cl1Lits, Clause* cl2, LiteralList** a
   md->nextAlts[0]=0;
   unsigned currBLit=0;
 
-  int counter=0;
-
   while(true) {
     MatchingData::InitResult ires=md->ensureInit(currBLit);
     if(ires!=MatchingData::OK) {
@@ -448,14 +446,6 @@ bool MLVariant::isVariant(Literal* const * cl1Lits, Clause* cl2, LiteralList** a
       if(currBLit==0) { return false; }
       currBLit--;
     }
-
-    counter++;
-    if(counter==50000) {
-      counter=0;
-      if(env.timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
   }
   return true;
 }

Kernel/MainLoop.hpp

@@ -17,13 +17,10 @@
 
 #include "Forwards.hpp"
 
-#include "Lib/Environment.hpp"
 #include "Lib/Exception.hpp"
 
 #include "Shell/Statistics.hpp"
 
-#include "Lib/Allocator.hpp"
-
 namespace Shell {
   class Property;
 };
@@ -100,6 +97,7 @@ class MainLoop {
   const Options& getOptions() const { return _opt; }
 
   static bool isRefutation(Clause* cl);
+
 protected:
 
   /**

Lib/Allocator.cpp

@@ -16,8 +16,10 @@
  * @since 24/07/2023, mostly replaced by a small-object allocator
  */
 
+#include <cstdlib>
+#include <limits>
+
 #include "Allocator.hpp"
-#include "Lib/Timer.hpp"
 
 #include <cstdlib>
 #include <limits>
@@ -45,7 +47,6 @@ void *operator new(size_t size, std::align_val_t align_val) {
     throw std::bad_alloc();
   ALLOCATED += size;
   {
-    Lib::TimeoutProtector tp;
     if(void *ptr = std::aligned_alloc(align, size))
       return ptr;
 
@@ -65,7 +66,6 @@ void *operator new(size_t size) {
     throw std::bad_alloc();
   ALLOCATED += size;
   {
-    Lib::TimeoutProtector tp;
     if(void *ptr = std::malloc(size))
       return ptr;
   }
@@ -76,7 +76,6 @@ void *operator new(size_t size) {
 void operator delete(void *ptr, size_t size) noexcept {
   ASS_GE(ALLOCATED, size)
   ALLOCATED -= size;
-  Lib::TimeoutProtector tp;
   std::free(ptr);
 }
 
@@ -91,6 +90,5 @@ void operator delete(void *ptr, size_t size, std::align_val_t align) noexcept {
 // occurs very rarely and usually from deep in the bowels of the standard library
 // TODO does cause us to slightly over-report allocated memory
 void operator delete(void *ptr) noexcept {
-  Lib::TimeoutProtector tp;
   std::free(ptr);
 }

Lib/Environment.cpp

@@ -48,9 +48,6 @@ Environment::Environment()
 {
   options = new Options;
 
-  // statistics calls the timer
-  timer = Timer::instance();
-
   statistics = new Statistics;
   signature = new Signature;
   sharing = new TermSharing;
@@ -71,31 +68,13 @@ Environment::Environment()
 
 Environment::~Environment()
 {
-  Timer::setLimitEnforcement(false);
-
   delete sharing;
   delete signature;
   delete statistics;
   if (predicateSineLevels) delete predicateSineLevels;
   delete options;
 }
 
-/**
- * If the global time limit reached set Statistics::terminationReason
- * to TIME_LIMIT and return true, otherwise return false.
- * @since 25/03/2008 Torrevieja
- */
-bool Environment::timeLimitReached() const
-{
-  if (options->timeLimitInDeciseconds() &&
-      timer->elapsedDeciseconds() > options->timeLimitInDeciseconds()) {
-    statistics->terminationReason = Shell::Statistics::TIME_LIMIT;
-    Timer::setLimitEnforcement(false);
-    return true;
-  }
-  return false;
-} // Environment::timeLimitReached
-
 /**
  * Return remaining time in miliseconds.
  */
@@ -105,7 +84,7 @@ int Environment::remainingTime() const
   if(options->timeLimitInDeciseconds() == 0){
     return 3600000;
   }
-  return options->timeLimitInDeciseconds()*100 - timer->elapsedMilliseconds();
+  return options->timeLimitInDeciseconds()*100 - Timer::elapsedMilliseconds();
 }
 
 // global environment object, constructed before main() and used everywhere

Lib/Environment.hpp

@@ -46,29 +46,13 @@ class Environment
   Indexing::TermSharing* sharing;
   /** Currently used statistics */
   Shell::Statistics* statistics;
-  /** Currently used timer, this is used by all timers as a global clock */
-  Timer* timer;
 
   unsigned char maxSineLevel;
 
   DHMap<unsigned, unsigned>* predicateSineLevels;
 
   DHMap<const Kernel::Unit*,std::string>* proofExtra; // maps Unit* pointers to the associated proof extra string, if available
 
-  bool timeLimitReached() const;
-
-  template<int Period>
-  void checkTimeSometime() const
-  {
-    static int counter=0;
-    counter++;
-    if(counter==Period) {
-      counter=0;
-      if(timeLimitReached()) {
-        throw TimeLimitExceededException();
-      }
-    }
-  }
   /** Time remaining until the end of the time-limit in miliseconds */
   int remainingTime() const;
   /** set to true when coloring is used for symbol elimination or interpolation */

Lib/Portability.hpp

@@ -19,4 +19,12 @@ static_assert(
     "Vampire assumes that there are 8 bits in a `char`"
 );
 
+#define VAMPIRE_PERF_EXISTS 0
+#ifdef __linux__
+#if __has_include(<linux/perf_event.h>)
+#undef VAMPIRE_PERF_EXISTS
+#define VAMPIRE_PERF_EXISTS 1
+#endif
+#endif
+
 #endif /*__Portability__*/