a cleanup on various ways of vampire outputting

ModelWriter · Sep 20, 2017 · 91e4058 · 91e4058
1 parent 5591427
commit 91e4058
Show file tree

Hide file tree

Showing 19 changed files with 113 additions and 165 deletions.
diff --git a/CASC/CASCMode.cpp b/CASC/CASCMode.cpp
@@ -30,8 +30,6 @@ bool CASCMode::perform(int argc, char* argv [])
 {
   CALL("CASCMode::perform/2");
 
-  UIHelper::szsOutput=true;
-
   env.timer->makeChildrenIncluded();
 
   ForkingCM cm;

diff --git a/CASC/CASCMultiMode.cpp b/CASC/CASCMultiMode.cpp
@@ -55,7 +55,6 @@ bool CASCMultiMode::perform()
   // to prevent from terminating by time limit
   env.options->setTimeLimitInSeconds(100000);
 
-  UIHelper::szsOutput = true;
   env.options->setProof(Options::Proof::TPTP);
   env.options->setStatistics(Options::Statistics::NONE);
 
@@ -147,8 +146,6 @@ bool CASCMultiMode::searchForProof()
   // now all the cpu usage will be in children, we'll just be waiting for them
   Timer::setTimeLimitEnforcement(false);
 
-  UIHelper::szsOutput=true;
-
   return performStrategy(property);
 } // CASCMultiMode::perform
 

diff --git a/CASC/CLTBMode.cpp b/CASC/CLTBMode.cpp
@@ -62,7 +62,7 @@ void CLTBMode::perform()
   // to prevent from terminating by time limit
   env.options->setTimeLimitInSeconds(100000);
 
-  UIHelper::szsOutput = true;
+  env.options->setOutputMode(Options::Output::SZS);
   env.options->setProof(Options::Proof::TPTP);
   env.options->setStatistics(Options::Statistics::NONE);
 
@@ -749,7 +749,7 @@ void CLTBProblem::searchForProof(int terminationTime,int timeLimit,const Categor
   // now all the cpu usage will be in children, we'll just be waiting for them
   Timer::setTimeLimitEnforcement(false);
 
-  UIHelper::szsOutput=true;
+  env.options->setOutputMode(Options::Output::SZS);
 
   performStrategy(terminationTime,timeLimit,category,property);
   exitOnNoSuccess();

diff --git a/CASC/Schedules.hpp b/CASC/Schedules.hpp
@@ -26,12 +26,6 @@ class Schedules
   static void getLtb2017MzrSchedule(const Shell::Property& property, Schedule& sched);
   static void getLtb2017DefaultSchedule(const Shell::Property& property, Schedule& sched);
 
-  // veci soutezni (szs, ...) oddel od veci portfoliovych
-
-  // from file, bude specialni value --schedule
-
-  // "casc" je posledni casc, "casc2017" je navzdy zadratovany historicky
-
   // ignore missing should be on in porfolio mode and only give a warning (error in vampire mode - in combination with --decode)
 
   // vsechny souteze 1 kod (az na LTB)

diff --git a/FMB/FiniteModelBuilder.cpp b/FMB/FiniteModelBuilder.cpp
@@ -1560,7 +1560,7 @@ MainLoopResult FiniteModelBuilder::runImpl()
 
   if (reset()) {
   while(true){
-    if(outputAllowed()) { 
+    if(outputAllowed()) {
       cout << "TRYING " << "["; 
       for(unsigned i=0;i<_distinctSortSizes.size();i++){
         cout << _distinctSortSizes[i];
@@ -1821,15 +1821,14 @@ void FiniteModelBuilder::onModelFound()
  if(_opt.proof()==Options::Proof::OFF){ 
    return; 
  }
- if(_opt.mode()==Options::Mode::SPIDER){
-   reportSpiderStatus('-');
- }
+
+ reportSpiderStatus('-');
  if(outputAllowed()){
    cout << "Finite Model Found!" << endl;
  }
 
  //we need to print this early because model generating can take some time
- if(UIHelper::szsOutput) {
+ if(szsOutputMode()) {
    env.beginOutput();
    env.out() << "% SZS status "<<( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" )
        << " for " << _opt.problemName() << endl << flush;

diff --git a/Global.cpp b/Global.cpp
@@ -27,7 +27,6 @@
 // any objects
 Lib::Enumerator Lib::Enumerator::unitEnumerator;
 unsigned Kernel::Unit::_lastNumber = 0;
-bool Shell::UIHelper::szsOutput=false;
 bool Shell::UIHelper::portfolioChild=false;
 bool Shell::UIHelper::satisfiableStatusWasAlreadyOutput=false;
 

diff --git a/InstGen/IGAlgorithm.cpp b/InstGen/IGAlgorithm.cpp
@@ -895,15 +895,13 @@ MainLoopResult IGAlgorithm::onModelFound()
     MainLoopResult res(Statistics::SATISFIABLE);
     if(_opt.proof()!=Options::Proof::OFF) {
       //we need to print this early because model generating can take some time
-      if(UIHelper::szsOutput) {
-	env.beginOutput();
-	env.out() << "% SZS status "<<( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" )
-	    << " for " << _opt.problemName() << endl << flush;
-	env.endOutput();
-	UIHelper::satisfiableStatusWasAlreadyOutput = true;
-      }
-      if(_opt.mode()==Options::Mode::SPIDER){
-        reportSpiderStatus('-');
+      reportSpiderStatus('-');
+      if(szsOutputMode()) {
+        env.beginOutput();
+        env.out() << "% SZS status "<<( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" )
+            << " for " << _opt.problemName() << endl << flush;
+        env.endOutput();
+        UIHelper::satisfiableStatusWasAlreadyOutput = true;
       }
 
       // Prevent timing out whilst the model is being printed

diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp
@@ -940,7 +940,6 @@ InferenceStore::ProofPrinter* InferenceStore::createProofPrinter(ostream& out)
   case Options::Proof::PROPERTY:
     return new ProofPropertyPrinter(out,this);
   case Options::Proof::OFF:
-  case Options::Proof::SMTCOMP:
     return 0;
   }
   ASSERTION_VIOLATION;

diff --git a/Kernel/MainLoop.cpp b/Kernel/MainLoop.cpp
@@ -27,6 +27,7 @@
 
 #include "Shell/BFNTMainLoop.hpp"
 #include "Shell/Options.hpp"
+#include "Shell/UIHelper.hpp"
 
 #include "Signature.hpp"
 #include "Clause.hpp"

diff --git a/Lib/TimeCounter.cpp b/Lib/TimeCounter.cpp
@@ -155,9 +155,7 @@ void TimeCounter::printReport(ostream& out)
 
   snapShot();
 
-  if (UIHelper::szsOutput) {
-    out << "% ";
-  }
+  addCommentSignForSZS(out);
   out << "Time measurement results:" << endl;
   for (int i=0; i<__TC_ELEMENT_COUNT; i++) {
     outputSingleStat(static_cast<TimeCounterUnit>(i), out);
@@ -171,9 +169,7 @@ void TimeCounter::outputSingleStat(TimeCounterUnit tcu, ostream& out)
     return;
   }
 
-  if (UIHelper::szsOutput) {
-    out << "% ";
-  }
+  addCommentSignForSZS(out);
   switch(tcu) {
   case TC_RAND_OPT:
     out << "random option generation";

diff --git a/Lib/Timer.cpp b/Lib/Timer.cpp
@@ -54,24 +54,25 @@ void timeLimitReached()
 
   env.beginOutput();
   reportSpiderStatus('t');
-  if (!inSpiderMode() && env.options->proof()!=Shell::Options::Proof::SMTCOMP) {
-    if (Shell::UIHelper::szsOutput) {
-      env.out() << "% (" << getpid() << ')';
-    }
+  if (outputAllowed()) {
+    addCommentSignForSZS(env.out());
     env.out() << "Time limit reached!\n";
-    if (Shell::UIHelper::szsOutput && !Shell::UIHelper::portfolioChild) {
-      env.out() << "% Proof not found in time ";
+
+    if (!UIHelper::portfolioChild) { // the boss
+      addCommentSignForSZS(env.out());
+      env.out() << "Proof not found in time ";
       Timer::printMSString(env.out(),env.timer->elapsedMilliseconds());
       env.out() << endl;
 
-      env.out() << "% SZS status Timeout for "
-                << (env.options ? env.options->problemName() : "unknown") << endl;
+      if (szsOutputMode()) {
+        env.out() << "% SZS status Timeout for "
+                        << (env.options ? env.options->problemName() : "unknown") << endl;
+      }
+    } else // the actual child
+      if (env.statistics) {
+        env.statistics->print(env.out());
     }
   }
-  if(env.statistics && (!Shell::UIHelper::szsOutput || Shell::UIHelper::portfolioChild) &&
-     env.options->mode() != Shell::Options::Mode::SPIDER && env.options->proof() != Shell::Options::Proof::SMTCOMP) {
-    env.statistics->print(env.out());
-  }
   env.endOutput();
 
   System::terminateImmediately(1);

diff --git a/SAT/Z3Interfacing.cpp b/SAT/Z3Interfacing.cpp
@@ -18,6 +18,8 @@
 #include "Kernel/Sorts.hpp"
 #include "Kernel/SortHelper.hpp"
 
+#include "Shell/UIHelper.hpp"
+
 #include "Indexing/TermSharing.hpp"
 
 #include "Z3Interfacing.hpp"

diff --git a/Shell/Options.cpp b/Shell/Options.cpp
@@ -27,6 +27,8 @@
 #include "Lib/Set.hpp"
 #include "Lib/System.hpp"
 
+#include "Shell/UIHelper.hpp"
+
 #include "Kernel/Problem.hpp"
 #include "Kernel/Signature.hpp"
 
@@ -235,7 +237,7 @@ void Options::Options::init()
     _problemName.description="";
     //_lookup.insert(&_problemName);
 
-    _proof = ChoiceOptionValue<Proof>("proof","p",Proof::ON,{"off","on","proofcheck","tptp","smtcomp","property"});
+    _proof = ChoiceOptionValue<Proof>("proof","p",Proof::ON,{"off","on","proofcheck","tptp","property"});
     _proof.description=
     "Specifies whether proof will be output. 'proofcheck' will output proof as a sequence of TPTP problems to allow for proof-checking.";
     _lookup.insert(&_proof);
@@ -270,10 +272,10 @@ void Options::Options::init()
     _lookup.insert(&_testId);
     _testId.setExperimental();
 
-    _szsOutput = BoolOptionValue("szs_output","szs",false);
-    _szsOutput.description="";
-    _lookup.insert(&_szsOutput);
-    _szsOutput.setExperimental();
+    _outputMode = ChoiceOptionValue<Output>("output_mode","",Output::VAMPIRE,{"smtcomp","spider","szs","vampire"});
+    _outputMode.description="";
+    _lookup.insert(&_outputMode);
+    _outputMode.setExperimental();
 
     _thanks = StringOptionValue("thanks","","Tanya");
     _thanks.description="";

diff --git a/Shell/Options.hpp b/Shell/Options.hpp
@@ -413,6 +413,14 @@ class Options
     NONE = 2
   };
 
+  /** how much we want vampire talking and in what language */
+  enum class Output : unsigned int {
+    SMTCOMP,
+    SPIDER,
+    SZS,
+    VAMPIRE
+  };
+
   /** Possible values for sat_solver */
   enum class SatSolver : unsigned int {
      MINISAT = 0,
@@ -510,8 +518,7 @@ class Options
     ON = 1,
     PROOFCHECK = 2,
     TPTP = 3,
-    SMTCOMP = 4,
-    PROPERTY = 5
+    PROPERTY = 4
   };
 
   /** Values for --equality_proxy */
@@ -1871,7 +1878,8 @@ class Options
   void setOutputAxiomNames(bool newVal) { _outputAxiomNames.actualValue = newVal; }
   QuestionAnsweringMode questionAnswering() const { return _questionAnswering.actualValue; }
   vstring xmlOutput() const { return _xmlOutput.actualValue; }
-  bool szsOutput() const { return _szsOutput.actualValue; }
+  Output outputMode() const { return _outputMode.actualValue; }
+  void setOutputMode(Output newVal) { _outputMode.actualValue = newVal; }
   vstring thanks() const { return _thanks.actualValue; }
   void setQuestionAnswering(QuestionAnsweringMode newVal) { _questionAnswering.actualValue = newVal; }
   bool globalSubsumption() const { return _globalSubsumption.actualValue; }
@@ -2306,7 +2314,7 @@ class Options
   StringOptionValue _predicatePrecedence;
 
   StringOptionValue _testId;
-  BoolOptionValue _szsOutput;
+  ChoiceOptionValue<Output> _outputMode;
   StringOptionValue _thanks;
   ChoiceOptionValue<TheoryAxiomLevel> _theoryAxioms;
   BoolOptionValue _theoryFlattening;

diff --git a/Shell/Statistics.cpp b/Shell/Statistics.cpp
@@ -141,18 +141,6 @@ Statistics::Statistics()
 {
 } // Statistics::Statistics
 
-/**
- * In the CASC mode output "% " so that the following line will be considered a comment.
- * @author Andrei Voronkov
- * @since 03/06/2012 Manchester
- */
-void Statistics::addCommentIfCASC(ostream& out)
-{
-  if (UIHelper::szsOutput) {
-    out << "% ";
-  }
-} // Statistics::addCommentIfCASC
-
 void Statistics::print(ostream& out)
 {
   if (env.options->statistics()==Options::Statistics::NONE) {
@@ -162,16 +150,16 @@ void Statistics::print(ostream& out)
   SaturationAlgorithm::tryUpdateFinalClauseCount();
 
   bool separable=false;
-#define HEADING(text,num) if (num) { addCommentIfCASC(out); out << ">>> " << (text) << endl;}
-#define COND_OUT(text, num) if (num) { addCommentIfCASC(out); out << (text) << ": " << (num) << endl; separable = true; }
-#define SEPARATOR if (separable) {   addCommentIfCASC(out); out << endl; separable = false; }
+#define HEADING(text,num) if (num) { addCommentSignForSZS(out); out << ">>> " << (text) << endl;}
+#define COND_OUT(text, num) if (num) { addCommentSignForSZS(out); out << (text) << ": " << (num) << endl; separable = true; }
+#define SEPARATOR if (separable) { addCommentSignForSZS(out); out << endl; separable = false; }
 
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "------------------------------\n";
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "Version: " << VERSION_STRING << endl;
 
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "Termination reason: ";
   switch(terminationReason) {
   case Statistics::REFUTATION:
@@ -220,7 +208,7 @@ void Statistics::print(ostream& out)
   }
   out << endl;
   if (phase!=FINALIZATION) {
-    addCommentIfCASC(out);
+    addCommentSignForSZS(out);
     out << "Termination phase: " << phaseToString(phase) << endl;
   }
   out << endl;
@@ -378,15 +366,15 @@ void Statistics::print(ostream& out)
 
   COND_OUT("Memory used [KB]", Allocator::getUsedMemory()/1024);
 
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "Time elapsed: ";
   Timer::printMSString(out,env.timer->elapsedMilliseconds());
   out << endl;
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "------------------------------\n";
 
   RSTAT_PRINT(out);
-  addCommentIfCASC(out);
+  addCommentSignForSZS(out);
   out << "------------------------------\n";
 
 #undef SEPARATOR

diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp
@@ -400,7 +400,6 @@ class Statistics
   ExecutionPhase phase;
 
 private:
-  static void addCommentIfCASC(ostream&); 
   static const char* phaseToString(ExecutionPhase p);
 }; // class Statistics