Casc2023

CASC/PortfolioMode.cpp

@@ -369,13 +369,21 @@ void PortfolioMode::getSchedules(const Property& prop, Schedule& quick, Schedule
     Schedules::getSnakeTptpSatSchedule(prop,quick);
     break;
 
-  case Options::Schedule::CASC_2019:
+  case Options::Schedule::CASC_2023:
   case Options::Schedule::CASC:
+    Schedules::getCasc2023Schedule(prop,quick,fallback);
+    break;
+
+  case Options::Schedule::CASC_2019:
     Schedules::getCasc2019Schedule(prop,quick,fallback);
     break;
 
-  case Options::Schedule::CASC_SAT_2019:
+  case Options::Schedule::CASC_SAT_2023:
   case Options::Schedule::CASC_SAT:
+    Schedules::getCascSat2023Schedule(prop,quick,fallback);
+    break;
+
+  case Options::Schedule::CASC_SAT_2019:
     Schedules::getCascSat2019Schedule(prop,quick,fallback);
     break;
 
@@ -483,7 +491,7 @@ bool PortfolioMode::runSchedule(Schedule schedule) {
   // kill all running processes first
   decltype(processes)::Iterator killIt(processes);
   while(killIt.hasNext())
-    Multiprocessing::instance()->killNoCheck(killIt.next(), SIGKILL);
+    Multiprocessing::instance()->killNoCheck(killIt.next(), SIGINT);
 
   return success;
 }

CASC/Schedules.hpp

@@ -26,10 +26,13 @@ class Schedules
 {
 public:
   static void getScheduleFromFile(const vstring& filename, Schedule& quick);
-
+  
   static void getHigherOrderSchedule2020(Schedule& quick, Schedule& fallback);
-  static void getCasc2019Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
 
+  static void getCasc2023Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
+  static void getCascSat2023Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
+
+  static void getCasc2019Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
   static void getCascSat2019Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
 
   static void getSmtcomp2018Schedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);

CMakeLists.txt

@@ -914,7 +914,7 @@ endif() # COMPILE_TESTS
 #################################################################
 # automated generation of Vampire revision information from git #
 #################################################################
-set(VAMPIRE_VERSION_NUMBER 4.7)
+set(VAMPIRE_VERSION_NUMBER 4.8)
 
 execute_process(
     COMMAND git rev-parse --is-inside-work-tree

Lib/System.cpp

@@ -104,6 +104,7 @@ void handleSignal (int sigNum)
   switch (sigNum)
     {
     case SIGTERM:
+
 # ifndef _MSC_VER
     case SIGQUIT:
       if (handled) {
@@ -139,6 +140,7 @@ void handleSignal (int sigNum)
 	return;
       }
       haveSigInt=true;
+      System::terminateImmediately(VAMP_RESULT_STATUS_SIGINT);
 //      exit(0);
 //      return;
 

Lib/Timer.cpp

@@ -125,13 +125,13 @@ timer_sigalrm_handler (int sig)
   }
 
 #ifdef __linux__
-  if(Timer::s_limitEnforcement && env.options->instructionLimit()) {
+  if(Timer::s_limitEnforcement && (env.options->instructionLimit() || env.options->simulatedInstructionLimit())) {
     if (perf_fd >= 0) {
       // we could also decide not to guard this read by env.options->instructionLimit(),
       // to get info about instructions burned even when not instruction limiting
       read(perf_fd, &last_instruction_count_read, sizeof(long long));
 
-      if (last_instruction_count_read >= MEGA*(long long)env.options->instructionLimit()) {
+      if (env.options->instructionLimit() && last_instruction_count_read >= MEGA*(long long)env.options->instructionLimit()) {
         Timer::setLimitEnforcement(false);
         if (TimeoutProtector::protectingTimeout) {
           TimeoutProtector::callLimitReachedLater = 2; // 2 for an instr limit

Makefile

@@ -507,7 +507,7 @@ all: #default make disabled
 ################################################################
 # automated generation of Vampire revision information
 
-VERSION_NUMBER = 4.7
+VERSION_NUMBER = 4.8
 
 # We extract the revision number from svn every time the svn meta-data are modified
 # (that's why there is the dependency on .svn/entries) 

Saturation/LRS.cpp

@@ -110,12 +110,14 @@ long long LRS::estimatedReachableCount()
   float correction_coef = _opt.lrsEstimateCorrectionCoef();
   int firstCheck=_opt.lrsFirstTimeCheck(); // (in percent)!
 
-  unsigned opt_instruction_limit = 0; // (in mega-instructions)
+  long int opt_instruction_limit = 0; // (in mega-instructions)
 #ifdef __linux__
-  opt_instruction_limit = _opt.instructionLimit();
+  opt_instruction_limit = _opt.simulatedInstructionLimit()
+    ? _opt.simulatedInstructionLimit()
+    : _opt.instructionLimit();
 #endif
 
-  unsigned instrsBurned = env.timer->elapsedMegaInstructions();
+  long int instrsBurned = env.timer->elapsedMegaInstructions();
 
   long long result = -1;
 
@@ -140,7 +142,7 @@ long long LRS::estimatedReachableCount()
       timeLeft=opt_timeLimitDeci*100 - currTime;
     }
 
-    long long instrsLeft = opt_instruction_limit - instrsBurned;
+    long int instrsLeft = opt_instruction_limit - instrsBurned;
 
     // note that result is -1 here already
 

Shell/Options.cpp

@@ -93,6 +93,13 @@ void Options::init()
   _instructionLimit.description="Limit the number (in millions) of executed instructions (excluding the kernel ones).";
   _lookup.insert(&_instructionLimit);
 
+  _simulatedInstructionLimit = UnsignedOptionValue("simulated_instruction_limit","sil",0);
+  _simulatedInstructionLimit.description=
+    "Instruction limit (in millions) of executed instructions for the purpose of reachability estimations of the LRS saturation algorithm (if 0, the actual instruction limit is used)";
+  _simulatedInstructionLimit.onlyUsefulWith(_saturationAlgorithm.is(equal(SaturationAlgorithm::LRS)));
+  _lookup.insert(&_simulatedInstructionLimit);
+  _simulatedInstructionLimit.tag(OptionTag::LRS);
+
   _parsingDoesNotCount = BoolOptionValue("parsing_does_not_count","",false);
   _parsingDoesNotCount.description= "Extend the instruction limit by the amount of instructions it took to parse the input problem.";
   _lookup.insert(&_parsingDoesNotCount);
@@ -145,8 +152,10 @@ void Options::init()
 
     _schedule = ChoiceOptionValue<Schedule>("schedule","sched",Schedule::CASC,
         {"casc",
+         "casc_2023",
          "casc_2019",
          "casc_sat",
+         "casc_hol_2023",
          "casc_sat_2019",
          "casc_hol_2020",
          "file",
@@ -2825,7 +2834,7 @@ bool Options::OptionValue<T>::checkConstraints(){
        const OptionValueConstraintUP<T>& con = it.next();
        if(!con->check(*this)){
 
-         if(env.options->mode()==Mode::SPIDER){
+         if (env.options->mode() == Mode::SPIDER){
            reportSpiderFail();
            USER_ERROR("\nBroken Constraint: "+con->msg(*this));
          }
@@ -2867,7 +2876,7 @@ bool Options::OptionValue<T>::checkProblemConstraints(Property* prop){
       // Constraint should hold whenever the option is set
       if(is_set && !con->check(prop)){
 
-         if(env.options->mode()==Mode::SPIDER){
+         if (env.options->mode() == Mode::SPIDER){
            reportSpiderFail();
            USER_ERROR("WARNING: " + longName + con->msg());
          }

Shell/Options.hpp

@@ -405,8 +405,10 @@ class Options
 
   enum class Schedule : unsigned int {
     CASC,
+    CASC_2023,
     CASC_2019,
     CASC_SAT,
+    CASC_SAT_2023,
     CASC_SAT_2019,
     CASC_HOL_2020,
     FILE,
@@ -2240,6 +2242,8 @@ bool _hard;
 #ifdef __linux__
   unsigned instructionLimit() const { return _instructionLimit.actualValue; }
   void setInstructionLimit(unsigned newVal) { _instructionLimit.actualValue = newVal; }
+  unsigned simulatedInstructionLimit() const { return _simulatedInstructionLimit.actualValue; }
+  unsigned setSimulatedInstructionLimit() const { return _simulatedInstructionLimit.actualValue; }
   bool parsingDoesNotCount() const { return _parsingDoesNotCount.actualValue; }
 #endif
   int inequalitySplitting() const { return _inequalitySplitting.actualValue; }
@@ -2678,7 +2682,8 @@ bool _hard;
   StringOptionValue _ltbDirectory;
 
 #ifdef __linux__
-  UnsignedOptionValue _instructionLimit; 
+  UnsignedOptionValue _instructionLimit;
+  UnsignedOptionValue _simulatedInstructionLimit;
   BoolOptionValue _parsingDoesNotCount;
 #endif
 

Shell/UIHelper.cpp

@@ -25,6 +25,7 @@
 #include "Debug/TimeProfiling.hpp"
 #include "Lib/VString.hpp"
 #include "Lib/Timer.hpp"
+#include "Lib/Allocator.hpp"
 
 #include "Kernel/InferenceStore.hpp"
 #include "Kernel/Problem.hpp"
@@ -100,12 +101,15 @@ void reportSpiderStatus(char status)
   }
 
   vstring problemName = Lib::env.options->problemName();
+  Timer* timer = Lib::env.timer;
 
   env.beginOutput();
   env.out()
     << status << " "
     << (problemName.length() == 0 ? "unknown" : problemName) << " "
-    << (Lib::env.timer ? Lib::env.timer->elapsedDeciseconds() : 0) << " "
+    << (timer ? timer->elapsedDeciseconds() : 0) << " "
+    << (timer ? timer->elapsedMegaInstructions() : 0) << " "
+    << Allocator::getUsedMemory()/1048576 << " "
     << (Lib::env.options ? Lib::env.options->testId() : "unknown") << " "
     << commitNumber << ':' << z3Version << endl;
   env.endOutput();

starexec/bin/starexec_run_casc

@@ -0,0 +1,9 @@
+#!/bin/sh
+
+input_language=`egrep -om1 "^(thf|tff|tcf|fof|cnf)" $1`
+if test "$input_language" = "thf"
+then
+	exec ./vampire-hol --cores 8 --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_tptp_hol $1 -m 12000  -t $STAREXEC_WALLCLOCK_LIMIT
+else
+	exec ./vampire --mode casc -m 16384 --cores 7 -t $STAREXEC_WALLCLOCK_LIMIT $1
+fi

starexec/bin/starexec_run_casc_sat

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec ./vampire --mode casc_sat -m 16384 --cores 7 -t $STAREXEC_WALLCLOCK_LIMIT $1

starexec/bin/starexec_run_slh

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec ./vampire_hol --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_slh $1 -m 12000  -t $STAREXEC_CPU_LIMIT

vampire.cpp

@@ -478,6 +478,12 @@ void spiderMode()
   CALL("spiderMode()");
   env.options->setBadOptionChoice(Options::BadOption::HARD);
   env.options->setOutputMode(Options::Output::SPIDER);
+  env.options->setNormalize(true);
+  // to start counting instructions
+#ifdef __linux__
+  Timer::ensureTimerInitialized();
+#endif
+
   Exception* exception = 0;
 #if VZ3
   z3::exception* z3_exception = 0;