From 91e4058cfa9dc255904a8a403b7e476bad1083bc Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Wed, 20 Sep 2017 14:52:23 +0200 Subject: [PATCH] a cleanup on various ways of vampire outputting --- CASC/CASCMode.cpp | 2 - CASC/CASCMultiMode.cpp | 3 -- CASC/CLTBMode.cpp | 4 +- CASC/Schedules.hpp | 6 --- FMB/FiniteModelBuilder.cpp | 9 ++-- Global.cpp | 1 - InstGen/IGAlgorithm.cpp | 16 +++---- Kernel/InferenceStore.cpp | 1 - Kernel/MainLoop.cpp | 1 + Lib/TimeCounter.cpp | 8 +--- Lib/Timer.cpp | 25 ++++++----- SAT/Z3Interfacing.cpp | 2 + Shell/Options.cpp | 12 ++--- Shell/Options.hpp | 16 +++++-- Shell/Statistics.cpp | 32 +++++--------- Shell/Statistics.hpp | 1 - Shell/UIHelper.cpp | 90 +++++++++++++++----------------------- Shell/UIHelper.hpp | 30 +++++-------- vampire.cpp | 19 +++----- 19 files changed, 113 insertions(+), 165 deletions(-) diff --git a/CASC/CASCMode.cpp b/CASC/CASCMode.cpp index 9481b9627b..823373704b 100644 --- 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 index b628474f19..78bc932de5 100644 --- 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 index 5911b84a05..ccaaea7087 100644 --- 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 index 599cf03de5..d53979fe02 100644 --- 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 index 7a10d23d74..b5aa3e832d 100644 --- 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 index 51a5e7f682..2684ae9125 100644 --- 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 index f870feea2f..7dc05f6710 100644 --- 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 index 05ce18f92e..a3c6f2c2f0 100644 --- 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 index c9e00a07ff..092df996ed 100644 --- 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 index 66bde88ea0..36d4b15a8c 100644 --- 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(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 index 4e7f43f0b5..f62785366c 100644 --- 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 index d8b2e3ade3..9a12e00ba9 100644 --- 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 index 3f285d1bca..1da07ce62e 100644 --- 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","p",Proof::ON,{"off","on","proofcheck","tptp","smtcomp","property"}); + _proof = ChoiceOptionValue("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_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 index 2d92ca2532..9c25769257 100644 --- 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 _outputMode; StringOptionValue _thanks; ChoiceOptionValue _theoryAxioms; BoolOptionValue _theoryFlattening; diff --git a/Shell/Statistics.cpp b/Shell/Statistics.cpp index 67c53333ba..0ff207b7a2 100644 --- 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 index 9ce14d63ff..18361dd7a3 100644 --- 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 diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index e4c510b8c2..93a00bda48 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -72,13 +72,10 @@ bool outputAllowed(bool debug) #if VDEBUG if(debug){ return true; } #endif - return !Lib::env.options || (Lib::env.options->mode()!=Shell::Options::Mode::SPIDER - && Lib::env.options->proof()!=Shell::Options::Proof::SMTCOMP ); -} -bool inSpiderMode() -{ - return Lib::env.options && Lib::env.options->mode()==Shell::Options::Mode::SPIDER; + // spider and smtcomp output modes are generally silent + return !Lib::env.options || (Lib::env.options->outputMode()!=Shell::Options::Output::SPIDER + && Lib::env.options->outputMode()!=Shell::Options::Output::SMTCOMP ); } void reportSpiderFail() @@ -90,11 +87,7 @@ void reportSpiderStatus(char status) { using namespace Lib; - static bool headerPrinted=false; - - if(inSpiderMode() && !headerPrinted) { - headerPrinted=true; - + if(Lib::env.options && Lib::env.options->outputMode() == Shell::Options::Output::SPIDER) { env.beginOutput(); env.out() << status << " " << (Lib::env.options ? Lib::env.options->problemName() : "unknown") << " " @@ -104,26 +97,18 @@ void reportSpiderStatus(char status) } } -bool UIHelper::s_haveConjecture=false; - -bool UIHelper::unitNumberComparator(Unit* us1, Unit* us2) -{ - CALL("UIHelper::unitNumberComparator"); - - return us1->number() < us2->number(); +bool szsOutputMode() { + return (Lib::env.options && Lib::env.options->outputMode() == Shell::Options::Output::SZS); } -/** - * In the CASC mode output "% " so that the following line will be considered a comment. - * @author Andrei Voronkov - * @since 03/06/2012 Manchester - */ -void UIHelper::addCommentIfCASC(ostream& out) +void addCommentSignForSZS(ostream& out) { - if (szsOutput) { + if (szsOutputMode()) { out << "% "; } -} // UIHelper::addCommentIfCASC +} + +bool UIHelper::s_haveConjecture=false; void UIHelper::outputAllPremises(ostream& out, UnitList* units, vstring prefix) { @@ -171,7 +156,7 @@ void UIHelper::outputSaturatedSet(ostream& out, UnitIterator uit) { CALL("UIHelper::outputSaturatedSet"); - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "# SZS output start Saturation." << endl; while (uit.hasNext()) { @@ -179,7 +164,7 @@ void UIHelper::outputSaturatedSet(ostream& out, UnitIterator uit) out << TPTPPrinter::toString(cl) << endl; } - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "# SZS output end Saturation." << endl; } // outputSaturatedSet @@ -297,14 +282,13 @@ void UIHelper::outputResult(ostream& out) switch (env.statistics->terminationReason) { case Statistics::REFUTATION: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unsat" << endl; return; } - addCommentIfCASC(out); - out << "Refutation found. Thanks to " - << env.options->thanks() << "!\n"; - if (szsOutput) { + addCommentSignForSZS(out); + out << "Refutation found. Thanks to " << env.options->thanks() << "!\n"; + if (szsOutputMode()) { out << "% SZS status " << ( UIHelper::haveConjecture() ? "Theorem" : "Unsatisfiable" ) << " for " << env.options->problemName() << endl; } @@ -313,12 +297,12 @@ void UIHelper::outputResult(ostream& out) AnswerExtractor::tryOutputAnswer(static_cast(env.statistics->refutation)); } if (env.options->proof() != Options::Proof::OFF) { - if (szsOutput) { - out << "% SZS output start Proof for " << env.options->problemName() << endl; + if (szsOutputMode()) { + out << "% SZS output start Proof for " << env.options->problemName() << endl; } InferenceStore::instance()->outputProof(out, env.statistics->refutation); - if (szsOutput) { - out << "% SZS output end Proof for " << env.options->problemName() << endl << flush; + if (szsOutputMode()) { + out << "% SZS output end Proof for " << env.options->problemName() << endl << flush; } } if (env.options->showInterpolant()==Options::InterpolantMode::ON) { @@ -370,28 +354,26 @@ void UIHelper::outputResult(ostream& out) } break; case Statistics::TIME_LIMIT: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unknown" << endl; return; } - if (szsOutput) { - out << "% (" << getpid() << ')'; - } + addCommentSignForSZS(out); out << "Time limit reached!\n"; break; case Statistics::MEMORY_LIMIT: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unknown" << endl; return; } #if VDEBUG Allocator::reportUsageByClasses(); #endif - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "Memory limit exceeded!\n"; break; case Statistics::ACTIVATION_LIMIT: { - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "Activation limit reached!\n"; // HERE ADD MORE @@ -399,11 +381,11 @@ void UIHelper::outputResult(ostream& out) break; } case Statistics::REFUTATION_NOT_FOUND: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unknown" << endl; return; } - addCommentIfCASC(out); + addCommentSignForSZS(out); if (env.statistics->discardedNonRedundantClauses) { out << "Refutation not found, non-redundant clauses discarded\n"; } @@ -418,7 +400,7 @@ void UIHelper::outputResult(ostream& out) } break; case Statistics::SATISFIABLE: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "sat" << endl; return; } @@ -431,19 +413,19 @@ void UIHelper::outputResult(ostream& out) out<<"good job\n"; break; case Statistics::INAPPROPRIATE: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unknown" << endl; return; } - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "Terminated due to inappropriate strategy.\n"; break; case Statistics::UNKNOWN: - if(env.options->proof() == Options::Proof::SMTCOMP){ + if(env.options->outputMode() == Options::Output::SMTCOMP){ out << "unknown" << endl; return; } - addCommentIfCASC(out); + addCommentSignForSZS(out); out << "Unknown reason of termination!\n"; break; default: @@ -457,16 +439,16 @@ void UIHelper::outputSatisfiableResult(ostream& out) CALL("UIHelper::outputSatisfiableResult"); out << "Satisfiable!\n"; - if (szsOutput && !satisfiableStatusWasAlreadyOutput) { + if (szsOutputMode() && !satisfiableStatusWasAlreadyOutput) { out << "% SZS status " << ( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" ) <<" for " << env.options->problemName() << endl; } if (!env.statistics->model.empty()) { - if (szsOutput) { + if (szsOutputMode()) { out << "% SZS output start FiniteModel for " << env.options->problemName() << endl; } out << env.statistics->model; - if (szsOutput) { + if (szsOutputMode()) { out << "% SZS output end FiniteModel for " << env.options->problemName() << endl; } } diff --git a/Shell/UIHelper.hpp b/Shell/UIHelper.hpp index b87f771fbd..6cc452e483 100644 --- a/Shell/UIHelper.hpp +++ b/Shell/UIHelper.hpp @@ -16,10 +16,11 @@ namespace Shell { using namespace Lib; using namespace Kernel; -bool outputAllowed(bool debug=false); -bool inSpiderMode(); +bool szsOutputMode(); +void addCommentSignForSZS(ostream&); void reportSpiderFail(); void reportSpiderStatus(char status); +bool outputAllowed(bool debug=false); class UIHelper { public: @@ -47,11 +48,6 @@ class UIHelper { static void outputSortDeclarations(ostream& out); - /** - * Hacky global flag indicating that reporting should be done in a Geoff-compliant way. - * (http://www.cs.miami.edu/~tptp/TPTP/TPTPTParty/2007/PositionStatements/GeoffSutcliffe_SZS.html) - */ - static bool szsOutput; /** * A hacky global flag distinguishing the parent and the child in portfolio modes. * Currently affects how things are reported during timeout (see Timer.cpp) @@ -62,7 +58,16 @@ class UIHelper { * IGAlgorithm, before we start generating model) */ static bool satisfiableStatusWasAlreadyOutput; + +private: + + static bool s_haveConjecture; +#if VDEBUG + static bool _inputHasBeenRead; +#endif + #if GNUMP +public: static ConstraintRCList* getInputConstraints(const Options& opts); static ConstraintRCList* getPreprocessedConstraints(const ConstraintRCList* inputConstraints); static ConstraintRCList* getPreprocessedConstraints(const Options& opts); @@ -71,22 +76,11 @@ class UIHelper { static void outputConstraints(ConstraintList* constraints, ostream& out, Options::InputSyntax syntax=Options::IS_HUMAN); static void outputAssignment(Assignment& assignemt, ostream& out, Options::InputSyntax syntax=Options::IS_HUMAN); -#endif //GNUMP private: -#if GNUMP static void outputConstraintInHumanFormat(const Constraint& constraint, ostream& out); static void outputConstraintInSMTFormat(const Constraint& constraint, ostream& out); #endif //GNUMP - - static bool unitNumberComparator(Unit* us1, Unit* us2); - static void addCommentIfCASC(ostream&); - - static bool s_haveConjecture; -#if VDEBUG - static bool _inputHasBeenRead; -#endif - }; } diff --git a/vampire.cpp b/vampire.cpp index 4c2efedffa..1bd3a25df7 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -642,10 +642,7 @@ void vampireMode() env.options->setUnusedPredicateDefinitionRemoval(false); } - if (env.options->szsOutput()) { - UIHelper::szsOutput = true; - UIHelper::portfolioChild = true; // so that we print stats on time-out (see Timer.cpp) - } + UIHelper::portfolioChild = true; // so that we print stats on time-out (see Timer.cpp) doProving(); @@ -662,7 +659,8 @@ void vampireMode() void spiderMode() { CALL("spiderMode()"); - env.options->setBadOptionChoice(Options::BadOption::HARD); + env.options->setBadOptionChoice(Options::BadOption::HARD); + env.options->setOutputMode(Options::Output::SPIDER); Exception* exception = 0; #if VZ3 z3::exception* z3_exception = 0; @@ -927,6 +925,7 @@ int main(int argc, char* argv[]) case Options::Mode::CASC_SAT: CASC::CASCMode::makeSat(); case Options::Mode::CASC: + env.options->setOutputMode(Options::Output::SZS); // If using a single core use old approach if(env.options->multicore()==1){ if (CASC::CASCMode::perform(argc, argv)) { @@ -943,7 +942,7 @@ int main(int argc, char* argv[]) } break; case Options::Mode::SMTCOMP: - env.options->setProof(Options::Proof::SMTCOMP); + env.options->setOutputMode(Options::Output::SMTCOMP); env.options->setInputSyntax(Options::InputSyntax::SMTLIB2); if(SMTCOMP::SMTCOMPMode::perform()){ vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS; @@ -970,14 +969,6 @@ int main(int argc, char* argv[]) vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS; break; } -/* - case Options::Mode::CASC_MZR: { - CASC::CMZRMode::perform(); - //we have processed the ltb batch file, so we can return zero - vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS; - break; - } -*/ case Options::Mode::MODEL_CHECK: modelCheckMode(); break;