From 42396f246d99ce85c26d4d1a4408cec211b94f11 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Wed, 6 Mar 2024 18:15:24 +0000 Subject: [PATCH 1/3] put LTB and dependencies on hiatus --- CASC/CLTBMode.cpp | 1027 ------------------------------- CASC/CLTBMode.hpp | 186 ------ CASC/CLTBModeLearning.cpp | 1202 ------------------------------------- CASC/CLTBModeLearning.hpp | 192 ------ CASC/PortfolioMode.cpp | 1 + CASC/PortfolioMode.hpp | 2 +- CMakeLists.txt | 8 - Lib/Environment.cpp | 44 +- Lib/Environment.hpp | 16 - Lib/FreshnessGuard.hpp | 57 -- Lib/Sys/SyncPipe.cpp | 249 -------- Lib/Sys/SyncPipe.hpp | 122 ---- Lib/fdstream.hpp | 173 ------ Shell/Options.cpp | 11 - Shell/Options.hpp | 11 - vampire.cpp | 33 +- 16 files changed, 8 insertions(+), 3326 deletions(-) delete mode 100644 CASC/CLTBMode.cpp delete mode 100644 CASC/CLTBMode.hpp delete mode 100644 CASC/CLTBModeLearning.cpp delete mode 100644 CASC/CLTBModeLearning.hpp delete mode 100644 Lib/FreshnessGuard.hpp delete mode 100644 Lib/Sys/SyncPipe.cpp delete mode 100644 Lib/Sys/SyncPipe.hpp delete mode 100644 Lib/fdstream.hpp diff --git a/CASC/CLTBMode.cpp b/CASC/CLTBMode.cpp deleted file mode 100644 index 3dacfe20ff..0000000000 --- a/CASC/CLTBMode.cpp +++ /dev/null @@ -1,1027 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file CLTBMode.cpp - * Implements class CLTBMode. - * @since 03/06/2013 updated to conform to the CASC-J6 specification - * @author Andrei Voronkov - */ -#include -#include -#include -#include -#include - -#include "Lib/Portability.hpp" - -#include "Lib/DHSet.hpp" -#include "Lib/Environment.hpp" -#include "Lib/Exception.hpp" -#include "Lib/Int.hpp" -#include "Lib/StringUtils.hpp" -#include "Lib/System.hpp" -#include "Debug/TimeProfiling.hpp" -#include "Lib/Timer.hpp" -#include "Lib/ScopedPtr.hpp" - -#include "Lib/Sys/Multiprocessing.hpp" -#include "Lib/Sys/SyncPipe.hpp" - -#include "Shell/Options.hpp" -#include "Shell/Normalisation.hpp" -#include "Saturation/ProvingHelper.hpp" -#include "Shell/Statistics.hpp" -#include "Shell/UIHelper.hpp" - -#include "Parse/TPTP.hpp" - -#include "Schedules.hpp" - -#include "CLTBMode.hpp" - -// #define SLOWNESS 1.15 - -using namespace CASC; -using namespace std; -using namespace Lib; -using namespace Lib::Sys; -using namespace Saturation; - -/** - * The function that does all the job: reads the input files and runs - * Vampires to solve problems. - * @since 05/06/2013 Vienna, adapted for CASC-J6 - * @author Andrei Voronkov - */ -void CLTBMode::perform() -{ - if (env.options->inputFile() == "") { - USER_ERROR("Input file must be specified for ltb mode"); - } - // to prevent from terminating by time limit - env.options->setTimeLimitInSeconds(1000000); - - env.options->setOutputMode(Options::Output::SZS); - env.options->setProof(Options::Proof::TPTP); - env.options->setStatistics(Options::Statistics::NONE); - - vstring line; - vstring inputFile = env.options->inputFile(); - std::size_t found = inputFile.find_last_of("/"); - vstring inputDirectory = "."; - if(found != vstring::npos){ - inputDirectory = inputFile.substr(0,found); - } - - ifstream in(inputFile.c_str()); - if (in.fail()) { - USER_ERROR("Cannot open input file: " + env.options->inputFile()); - } - - //support several batches in one file - bool firstBatch=true; - while (!in.eof()) { - vostringstream singleInst; - bool ready = false; - while (!in.eof()) { - getline(in, line); - singleInst << line << endl; - if (line == "% SZS end BatchProblems") { - ready = true; - break; - } - } - if (!ready) { - break; - } - CLTBMode ltbm; - vistringstream childInp(singleInst.str()); - ltbm.solveBatch(childInp,firstBatch,inputDirectory); - firstBatch=false; - } -} // CLTBMode::perform - -/** - * This function processes a single batch in a batch file. It makes the following - * steps: - *
  1. read the batch file
    2. - *
  2. load the common axioms and put them into a SInE selector
    3. - *
  3. spawn child processes that try to prove a problem by calling - * CLTBProblem::searchForProof(). These processes are run sequentially and the time - * limit for each one is computed depending on the per-problem time limit, - * batch time limit, and time spent on this batch so far. The termination - * time for the proof search for a problem will be passed to - * CLTBProblem::searchForProof() as an argument.
- * @author Andrei Voronkov - * @since 04/06/2013 flight Manchester-Frankfurt - */ -void CLTBMode::solveBatch(istream& batchFile, bool first,vstring inputDirectory) -{ - // this is the time in milliseconds since the start when this batch file should terminate - _timeUsedByPreviousBatches = env.timer->elapsedMilliseconds(); - coutLineOutput() << "Starting Vampire on the batch file " << "\n"; - int terminationTime = readInput(batchFile,first); - loadIncludes(); - - _biasedLearning = false; - if (env.options->ltbLearning() != Options::LTBLearning::OFF){ - _learnedFormulasMaxCount = 1; - _biasedLearning = (env.options->ltbLearning() == Options::LTBLearning::BIASED); - doTraining(); - } - - int solvedProblems = 0; - int remainingProblems = _problemFiles.size(); - StringPairStack::BottomFirstIterator probs(_problemFiles); - while (probs.hasNext()) { - StringPair res=probs.next(); - - vstring probFile= inputDirectory+"/"+res.first; - vstring outFile= res.second; - vstring outDir = env.options->ltbDirectory(); - if(!outDir.empty()){ - std::size_t found = outFile.find_last_of("/"); - if(found != vstring::npos){ - outFile = outFile.substr(found); - } - outFile= outDir+"/"+outFile; - } - - // calculate the next problem time limit in milliseconds - int elapsedTime = env.timer->elapsedMilliseconds(); - int timeRemainingForThisBatch = terminationTime - elapsedTime; - coutLineOutput() << "time remaining for this batch " << timeRemainingForThisBatch << endl; - int remainingBatchTimeForThisProblem = timeRemainingForThisBatch / remainingProblems; - coutLineOutput() << "remaining batch time for this problem " << remainingBatchTimeForThisProblem << endl; - int nextProblemTimeLimit; - if (!_problemTimeLimit) { - nextProblemTimeLimit = remainingBatchTimeForThisProblem; - } - else if (remainingBatchTimeForThisProblem > _problemTimeLimit) { - nextProblemTimeLimit = _problemTimeLimit; - } - else { - nextProblemTimeLimit = remainingBatchTimeForThisProblem; - } - // time in milliseconds when the current problem should terminate - int problemTerminationTime = elapsedTime + nextProblemTimeLimit; - coutLineOutput() << "problem termination time " << problemTerminationTime << endl; - - env.beginOutput(); - env.out() << flush << "%" << endl; - lineOutput() << "SZS status Started for " << probFile << endl << flush; - env.endOutput(); - - pid_t child = Multiprocessing::instance()->fork(); - if (!child) { - // child process - TIME_TRACE_NEW_ROOT("child process") - CLTBProblem prob(this, probFile, outFile); - try { - prob.searchForProof(problemTerminationTime,nextProblemTimeLimit,_category); - } catch (Exception& exc) { - cerr << "% Exception at proof search level" << endl; - exc.cry(cerr); - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code - } - // searchForProof() function should never return - ASSERTION_VIOLATION; - } - - env.beginOutput(); - lineOutput() << "solver pid " << child << endl; - env.endOutput(); - int resValue; - // wait until the child terminates - try { - ALWAYS( - Multiprocessing::instance()->waitForChildTermination(resValue) == child - ); - } - catch(SystemFailException& ex) { - cerr << "% SystemFailException at batch level" << endl; - ex.cry(cerr); - } - - // output the result depending on the termination code - env.beginOutput(); - if (!resValue) { - lineOutput() << "SZS status Theorem for " << probFile << endl; - solvedProblems++; - - if (env.options->ltbLearning() != Options::LTBLearning::OFF){ - // As we solved it we can learn from the proof - learnFromSolutionFile(outFile); - } - } - else { - lineOutput() << "SZS status GaveUp for " << probFile << endl; - } - env.out() << flush << '%' << endl; - lineOutput() << "% SZS status Ended for " << probFile << endl << flush; - env.endOutput(); - - Timer::syncClock(); - - remainingProblems--; - } - env.beginOutput(); - lineOutput() << "Solved " << solvedProblems << " out of " << _problemFiles.size() << endl; - env.endOutput(); -} // CLTBMode::solveBatch(batchFile) - -void CLTBMode::loadIncludes() -{ - UnitList* theoryAxioms=0; - { - TIME_TRACE(TimeTrace::PARSING); - env.statistics->phase=Statistics::PARSING; - - StringList::Iterator iit(_theoryIncludes); - while (iit.hasNext()) { - vstring fname=env.options->includeFileName(iit.next()); - - ifstream inp(fname.c_str()); - if (inp.fail()) { - USER_ERROR("Cannot open included file: "+fname); - } - Parse::TPTP parser(inp); - parser.parse(); - UnitList* funits = parser.units(); - if (parser.containsConjecture()) { - USER_ERROR("Axiom file " + fname + " contains a conjecture."); - } - - UnitList::Iterator fuit(funits); - while (fuit.hasNext()) { - fuit.next()->inference().markIncluded(); - } - theoryAxioms=UnitList::concat(funits,theoryAxioms); - } - } - - _baseProblem = new Problem(theoryAxioms); - //ensure we scan the theory axioms for property here, so we don't need to - //do it afterward in each problem - _baseProblem->getProperty(); - env.setMainProblem(_baseProblem.ptr()); - env.statistics->phase=Statistics::UNKNOWN_PHASE; -} // CLTBMode::loadIncludes - - -void CLTBMode::learnFromSolutionFile(vstring& solnFileName) -{ - ifstream soln(solnFileName.c_str()); - if (soln.fail()) { - return; // ignore if we cannot get the solution file - //USER_ERROR("Cannot open problem file: " + solnFileName); - } - cout << "Reading solutions " << solnFileName << endl; - - ScopedPtr > sources; - sources = new DHMap(); - - Parse::TPTP parser(soln); - parser.setUnitSourceMap(sources.ptr()); - parser.setFilterReserved(); - UnitList* solnUnits = 0; - try { - bool outputAxiomValue = env.options->outputAxiomNames(); - env.options->setOutputAxiomNames(true); - parser.parse(); - env.options->setOutputAxiomNames(outputAxiomValue); - solnUnits = parser.units(); - } catch (Lib::Exception& ex) { - cout << "Couldn't parse " << "solnFileName" << endl; - ex.cry(cout); - - //save memory by deleting the already loaded units: - UnitList* units = parser.units(); - UnitList::Iterator it(units); - while (it.hasNext()) { - it.next()->destroy(); - } - UnitList::destroy(units); - } - - UnitList::DelIterator it(solnUnits); - while (it.hasNext()) { - Unit* unit = it.next(); - if (unit->inputType()==UnitInputType::AXIOM){ - if (sources->find(unit)){ - if (sources->get(unit)->isFile()){ - vstring name = static_cast(sources->get(unit))->nameInFile; - if (_learnedFormulas.insert(name)){ - // new name - if (_biasedLearning){ - _learnedFormulasCount.insert(name,1); - } - }else{ - if (_biasedLearning){ - ASS_REP(_learnedFormulas.contains(name),name); - ASS_REP(_learnedFormulasCount.find(name),name); - // not new - _learnedFormulasCount.get(name)++; - if (_learnedFormulasCount.get(name) > _learnedFormulasMaxCount){ - _learnedFormulasMaxCount = _learnedFormulasCount.get(name); - } - //cout << name << "," << _learnedFormulasCount.get(name) << endl; - } - } - - } - } - else{ - // The Der outputs seem to not do the file thing for input axioms - // I think it is safe to include the names of these axioms as learned - // If not I expect we will be unsound - vstring name; - if (Parse::TPTP::findAxiomName(unit,name)){ - if (_learnedFormulas.insert(name)){ - // new name - if (_biasedLearning){ - _learnedFormulasCount.insert(name,1); - } - }else{ - if (_biasedLearning){ - ASS_REP(_learnedFormulas.contains(name),name); - ASS_REP(_learnedFormulasCount.find(name),name); - // not new - _learnedFormulasCount.get(name)++; - if (_learnedFormulasCount.get(name) > _learnedFormulasMaxCount){ - _learnedFormulasMaxCount = _learnedFormulasCount.get(name); - } - //cout << name << "," << _learnedFormulasCount.get(name) << endl; - } - } - } - } - } - it.del(); - } - -} - - -void CLTBMode::doTraining() -{ - env.beginOutput(); - env.out() << "Training in LTB currently unsupported" << endl; - env.endOutput(); - return; - - Stack solutions; - System::readDir(_trainingDirectory+"/Solutions",solutions); - - - Stack::RefIterator it(solutions); - while (it.hasNext()) { - TIME_TRACE(TimeTrace::PARSING); - env.statistics->phase=Statistics::PARSING; - - vstring& solnFileName = it.next(); - learnFromSolutionFile(solnFileName); - - } - - // Idea is to solve training problems and look in proofs for common clauses derived from axioms - // these can then be loaded into later proof attempts with weight zero to ensure they are processed quickly - // - // training could insert these axioms directly into the base problem object and mark their input type such that - // they get weight zero in Vampire - // - // do to training let's - // prove the training problems in the same way as the real problems - this will write output to a file per problem - // this output should contain the proofs - // read in these files and parse the proofs, building up the clauses to add to the base problem - // add clauses to the base problem - -} // CLTBMode::doTraining - -/** - * Read a single batch file from @b in. Return the time in milliseconds since - * the start, when the process should terminate. If the batch contains no overall - * time limit, return a very large integer value. - * Set _problemTimeLimit to the per-problem time limit from - * the batch file. - * @since 04/06/2013 flight Manchester-Frankfurt - * @author Andrei Voronkov - */ -int CLTBMode::readInput(istream& in, bool first) -{ - vstring line, word; - - if(first){ - getline(in,line); - if (line.find("division.category") != vstring::npos){ - StringStack ls; - StringUtils::splitStr(line.c_str(),' ',ls); - _category = getCategory(ls[1]); - coutLineOutput() << "read category " << ls[1] << endl; - } - else{ USER_ERROR("division category not found"); } - - // Get training directory - getline(in,line); - if (line.find("training_data") != vstring::npos){ - StringStack ls; - StringUtils::splitStr(line.c_str(),' ',ls); - _trainingDirectory = ls[1]; - } - else{ USER_ERROR("training_directory not found"); } - - } - - getline(in,line); - if (line!="% SZS start BatchConfiguration") { - USER_ERROR("\"% SZS start BatchConfiguration\" expected, \""+line+"\" found."); - } - - getline(in, line); - - _questionAnswering = false; - _problemTimeLimit = -1; - int batchTimeLimit = -1; - - StringStack lineSegments; - while (!in.eof() && line!="% SZS end BatchConfiguration") { - lineSegments.reset(); - StringUtils::splitStr(line.c_str(), ' ', lineSegments); - vstring param = lineSegments[0]; - // not used here now -/* - if (param == "division.category") { - if (lineSegments.size()!=2) { - USER_ERROR("unexpected \""+param+"\" specification: \""+line+"\""); - } - _category = lineSegments[1]; - } - else -*/ - if (param == "output.required" || param == "output.desired") { - if (lineSegments.find("Answer")) { - _questionAnswering = true; - } - } - else if (param == "execution.order") { - // we ignore this for now and always execute in order - } - else - if (param == "limit.time.problem.wc") { - - if (lineSegments.size() != 2 || - !Int::stringToInt(lineSegments[1], _problemTimeLimit)) { - USER_ERROR("unexpected \""+param+"\" specification: \""+line+"\""); - } - _problemTimeLimit = 1000 * _problemTimeLimit; - } - else if (param == "limit.time.overall.wc") { - if (lineSegments.size() != 2 || - !Int::stringToInt(lineSegments[1], batchTimeLimit)) { - USER_ERROR("unexpected \"" + param + "\" specification: \""+ line +"\""); - } - batchTimeLimit = 1000 * batchTimeLimit; - } - else { - USER_ERROR("unknown batch configuration parameter: \""+line+"\""); - } - - getline(in, line); - } - - if (line != "% SZS end BatchConfiguration") { - USER_ERROR("\"% SZS end BatchConfiguration\" expected, \"" + line + "\" found."); - } - if (_questionAnswering) { - env.options->setQuestionAnswering(Options::QuestionAnsweringMode::ANSWER_LITERAL); - } - - getline(in, line); - if (line!="% SZS start BatchIncludes") { - USER_ERROR("\"% SZS start BatchIncludes\" expected, \""+line+"\" found."); - } - - _theoryIncludes=0; - for (getline(in, line); line[0]!='%' && !in.eof(); getline(in, line)) { - size_t first=line.find_first_of('\''); - size_t last=line.find_last_of('\''); - if (first == vstring::npos || first == last) { - USER_ERROR("Include specification must contain the file name enclosed in the ' characters:\""+line+"\"."); - } - ASS_G(last,first); - vstring fname=line.substr(first+1, last-first-1); - StringList::push(fname, _theoryIncludes); - } - - while (!in.eof() && line == "") { getline(in, line); } - if (line!="% SZS end BatchIncludes") { - USER_ERROR("\"% SZS end BatchIncludes\" expected, \""+line+"\" found."); - } - getline(in, line); - if (line!="% SZS start BatchProblems") { - USER_ERROR("\"% SZS start BatchProblems\" expected, \""+line+"\" found."); - } - - for (getline(in, line); line[0]!='%' && !in.eof(); getline(in, line)) { - size_t spc=line.find(' '); - size_t lastSpc=line.find(' ', spc+1); - if (spc == vstring::npos || spc == 0 || spc == line.length()-1) { - USER_ERROR("Two file names separated by a single space expected:\""+line+"\"."); - } - vstring inp=line.substr(0,spc); - vstring outp=line.substr(spc+1, lastSpc-spc-1); - _problemFiles.push(make_pair(inp, outp)); - } - - while (!in.eof() && line == "") { - getline(in, line); - } - if (line!="% SZS end BatchProblems") { - USER_ERROR("\"% SZS end BatchProblems\" expected, \""+line+"\" found."); - } - - if (batchTimeLimit == -1) { // batch time limit is undefined - if (_problemTimeLimit == -1) { - USER_ERROR("either the problem time limit or the batch time limit must be specified"); - } - // to avoid overflows when added to the current elapsed time, make it less than INT_MAX - return INT_MAX / 8; - } - - // batch time limit is defined - if (_problemTimeLimit == -1) { - _problemTimeLimit = 0; - } - return _timeUsedByPreviousBatches + batchTimeLimit; -} // CLTBMode::readInput - -vstring CLTBProblem::problemFinishedString = "##Problem finished##vn;3-d-ca-12=1;'"; - -CLTBProblem::CLTBProblem(CLTBMode* parent, vstring problemFile, vstring outFile) - : parent(parent), problemFile(problemFile), outFile(outFile), - prb(*parent->_baseProblem), _syncSemaphore(1) -{ - //add the privileges into the semaphore - _syncSemaphore.set(0,1); -} - -void CLTBProblem::fillSchedule(Schedule& sched,const Shell::Property* property,int timeLimit,Category category) -{ - switch (category) { - case HH4: - Schedules::getLtb2017Hh4Schedule(*property,sched); - return; - case HLL: - Schedules::getLtb2017HllSchedule(*property,sched); - return; - case ISA: - Schedules::getLtb2017IsaSchedule(*property,sched); - return; - case MZR: - Schedules::getLtb2017MzrSchedule(*property,sched); - return; - default: - Schedules::getLtb2017DefaultSchedule(*property,sched); - return; - } -} // fillSchedule - -/** - * This function solves a single problem. It makes the following steps: - *
  1. find the main and the fallback schedules depending on the problem - * properties
    2. - *
  2. run the main schedule using runSchedule()
    3. - *
  3. if the proof is not found, checks if all the remaining time - * was used: if not, it runs the fallback strategy using - * runSchedule() with the updated time limit
- * Once the problem is proved, the runSchedule() function does not return - * and the process terminates. - * - * If a slice contains sine_selection value different from off, theory axioms - * will be selected using SInE from the common axioms included in the batch file - * (all problem axioms, including the included ones, will be used as a base - * for this selection). - * - * If the sine_selection is off, all the common axioms will be just added to the - * problem axioms. All this is done in the @b runSlice(Options&) function. - * @param terminationTime the time in milliseconds since the prover starts when - * the strategy should terminate - * @param timeLimit in milliseconds - * @param category - * @param property - * @author Krystof Hoder - * @since 04/06/2013 flight Frankfurt-Vienna, updated for CASC-J6 - * @author Andrei Voronkov - */ -void CLTBProblem::performStrategy(int terminationTime,int timeLimit,Category category,const Shell::Property* property) -{ - cout << "% Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!\n"; - - Schedule quick; - - fillSchedule(quick,property,timeLimit,category); - - StrategySet usedSlices; - if (runSchedule(quick,usedSlices,terminationTime)) { - return; - } - if (env.timer->elapsedMilliseconds() >= terminationTime) { - return; - } - Schedule fallback; - Schedule fallback2; - Schedules::getCasc2019Schedule(*property,fallback,fallback2); - runSchedule(fallback,usedSlices,terminationTime); - runSchedule(fallback2,usedSlices,terminationTime); -} // CLTBProblem::performStrategy - -/** - * This function solves a single problem. It parses the problem, spawns a - * writer process for output and creates a pipe to communicate with it. - * Then it calls performStrategy(terminationTime) that performs the - * actual proof search. - * @param terminationTime the time in milliseconds since the prover start - * @param timeLimit time limit in milliseconds - * @param category - * @since 04/06/2013 flight Manchester-Frankfurt - * @author Andrei Voronkov - */ -void CLTBProblem::searchForProof(int terminationTime,int timeLimit,const Category category) -{ - TIME_TRACE("search for proof") - - System::registerForSIGHUPOnParentDeath(); - - // special reporting in Timer.cpp - UIHelper::portfolioParent = true; - env.options->setInputFile(problemFile); - - Stack cutoffs; - if (env.options->ltbLearning() != Options::LTBLearning::OFF){ - - if (parent->_biasedLearning){ - unsigned cutoff = parent->_learnedFormulasMaxCount/2; - while (cutoff>0){ - cutoffs.push(cutoff); - //cout << "create cutoff " << cutoff << endl; - cutoff /= 2; - } - } - } - - // this local scope will delete a potentially large parser - { - TIME_TRACE(TimeTrace::PARSING); - env.statistics->phase=Statistics::PARSING; - - // Ensure the parser is recording axiom names - bool outputAxiomValue = env.options->outputAxiomNames(); - env.options->setOutputAxiomNames(true); - - ifstream inp(problemFile.c_str()); - if (inp.fail()) { - USER_ERROR("Cannot open problem file: " + problemFile); - } - Parse::TPTP parser(inp); - List::Iterator iit(parent->_theoryIncludes); - while (iit.hasNext()) { - parser.addForbiddenInclude(iit.next()); - } - parser.parse(); - UnitList* probUnits = parser.units(); - UIHelper::setConjecturePresence(parser.containsConjecture()); - prb.addUnits(probUnits); - - env.options->setOutputAxiomNames(outputAxiomValue); - } - - Shell::Property* property = prb.getProperty(); - if (property->atoms()<=1000000) { - TIME_TRACE(TimeTrace::PREPROCESSING); - env.statistics->phase=Statistics::NORMALIZATION; - Normalisation norm; - norm.normalise(prb); - } - - env.statistics->phase=Statistics::UNKNOWN_PHASE; - - // now all the cpu usage will be in children, we'll just be waiting for them - Timer::setLimitEnforcement(false); - - env.options->setOutputMode(Options::Output::SZS); - - performStrategy(terminationTime,timeLimit,category,property); - exitOnNoSuccess(); - ASSERTION_VIOLATION; // the exitOnNoSuccess() function should never return -} // CLTBProblem::perform - -/** - * This function exits the problem master process if the problem - * was not solved - * - * The unsuccessful problem master process does not have to - * necessarily call this function to exit. - */ -void CLTBProblem::exitOnNoSuccess() -{ - env.beginOutput(); - CLTBMode::lineOutput() << "Proof not found in time " << Timer::msToSecondsString(env.timer->elapsedMilliseconds()) << endl; - if (env.remainingTime()/100>0) { - CLTBMode::lineOutput() << "SZS status GaveUp for " << env.options->problemName() << endl; - } - else { - //From time to time we may also be terminating in the timeLimitReached() - //function in Lib/Timer.cpp in case the time runs out. We, however, output - //the same string there as well. - CLTBMode::lineOutput() << "SZS status Timeout for " << env.options->problemName() << endl; - } - env.endOutput(); - - CLTBMode::coutLineOutput() << "problem proof search terminated (fail)" << endl << flush; - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code -} // CLTBProblem::exitOnNoSuccess - -static unsigned milliToDeci(unsigned timeInMiliseconds) { - return timeInMiliseconds/100; -} - -/** - * Run a schedule. Terminate the process with 0 exit status - * if a proof was found, otherwise return false. This function available cores: - * If the total number of cores @b n is 8 or more, then @b n-2, otherwise @b n-1. - * It spawns processes by calling runSlice() - * @author Andrei Voronkov - * @since 04/06/2013 flight Frankfurt-Vienna, updated for CASC-J6 - */ -bool CLTBProblem::runSchedule(Schedule& schedule,StrategySet& used,int terminationTime) -{ - // compute the number of parallel processes depending on the - // number of available cores - int parallelProcesses; - unsigned coreNumber = System::getNumberOfCores(); - if (coreNumber <= 1) { - parallelProcesses = 1; - } - else if (coreNumber>=8) { - parallelProcesses = coreNumber-2; - } - else { - parallelProcesses = coreNumber; - } - - int processesLeft = parallelProcesses; - Schedule::BottomFirstIterator it(schedule); - - int slices = schedule.length(); - while (it.hasNext()) { - while (processesLeft) { - CLTBMode::coutLineOutput() << "Slices left: " << slices-- << endl; - CLTBMode::coutLineOutput() << "Processes available: " << processesLeft << endl << flush; - ASS_G(processesLeft,0); - - int elapsedTime = env.timer->elapsedMilliseconds(); - if (elapsedTime >= terminationTime) { - // time limit reached - goto finish_up; - } - - vstring sliceCode = it.next(); - vstring chopped; - - // slice time in milliseconds - // int sliceTime = SLOWNESS * getSliceTime(sliceCode,chopped); - int sliceTime = getSliceTime(sliceCode,chopped); - if (used.contains(chopped)) { - // this slice was already used - continue; - } - used.insert(chopped); - int remainingTime = terminationTime - elapsedTime; - if (sliceTime > remainingTime) { - sliceTime = remainingTime; - } - - ASS_GE(sliceTime,0); - if (milliToDeci((unsigned)sliceTime) == 0) { - // can be still zero, due to rounding - // and zero time limit means no time limit -> the child might never return! - - // time limit reached - goto finish_up; - } - - pid_t childId=Multiprocessing::instance()->fork(); - ASS_NEQ(childId,-1); - if (!childId) { - //we're in a proving child - try { - runSlice(sliceCode,sliceTime); //start proving - } catch (Exception& exc) { - cerr << "% Exception at run slice level" << endl; - exc.cry(cerr); - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code - } - ASSERTION_VIOLATION; //the runSlice function should never return - } - Timer::syncClock(); - ASS(childIds.insert(childId)); - CLTBMode::coutLineOutput() << "slice pid "<< childId << " slice: " << sliceCode - << " time: " << (sliceTime/100)/10.0 << endl << flush; - processesLeft--; - if (!it.hasNext()) { - break; - } - } - - CLTBMode::coutLineOutput() << "No processes available: " << endl << flush; - if (processesLeft==0) { - waitForChildAndExitWhenProofFound(); - // proof search failed - processesLeft++; - } - } - - finish_up: - - while (parallelProcesses!=processesLeft) { - ASS_L(processesLeft, parallelProcesses); - waitForChildAndExitWhenProofFound(); - // proof search failed - processesLeft++; - Timer::syncClock(); - } - return false; -} // CLTBProblem::runSchedule - -/** - * Wait for termination of a child and terminate the process with a zero status - * if a proof was found. If the child didn't find the proof, just return. - */ -void CLTBProblem::waitForChildAndExitWhenProofFound() -{ - ASS(!childIds.isEmpty()); - - int resValue; - pid_t finishedChild = Multiprocessing::instance()->waitForChildTermination(resValue); -#if VDEBUG - ALWAYS(childIds.remove(finishedChild)); -#endif - if (!resValue) { - // we have found the proof. It has been already written down by the writter child, - // so we can just terminate - CLTBMode::coutLineOutput() << "terminated slice pid " << finishedChild << " (success)" << endl << flush; - System::terminateImmediately(0); - } - // proof not found - CLTBMode::coutLineOutput() << "terminated slice pid " << finishedChild << " (fail)" << endl << flush; -} // waitForChildAndExitWhenProofFound - -ofstream* CLTBProblem::writerFileStream = 0; - -void CLTBProblem::terminatingSignalHandler(int sigNum) -{ - try { - if (writerFileStream) { - writerFileStream->close(); - } - } catch (Lib::SystemFailException& ex) { - cerr << "Process " << getpid() << " received SystemFailException in terminatingSignalHandler" << endl; - ex.cry(cerr); - cerr << " and will now die" << endl; - } - System::terminateImmediately(0); -} - -/** - * Run a slice given by its code using the specified time limit. - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -void CLTBProblem::runSlice(vstring sliceCode, unsigned timeLimitInMilliseconds) -{ - Options opt = *env.options; - opt.readFromEncodedOptions(sliceCode); - opt.setTimeLimitInDeciseconds(milliToDeci(timeLimitInMilliseconds)); - // int stl = opt.simulatedTimeLimit(); - // if (stl) { - // opt.setSimulatedTimeLimit(int(stl * SLOWNESS)); - // } - runSlice(opt); -} // runSlice - -/** - * Run a slice given by its options - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -void CLTBProblem::runSlice(Options& strategyOpt) -{ - TIME_TRACE_NEW_ROOT("run slice") - - System::registerForSIGHUPOnParentDeath(); - UIHelper::portfolioParent = false; - - int resultValue=1; - env.timer->reset(); - env.timer->start(); - Timer::setLimitEnforcement(true); - - Options opt = strategyOpt; - //we have already performed the normalization - opt.setNormalize(false); - opt.setForcedOptionValues(); - opt.checkGlobalOptionConstraints(); - opt.setProblemName(problemFile); - *env.options = opt; //just temporarily until we get rid of dependencies on env.options in solving - -// if (env.options->sineSelection()!=Options::SS_OFF) { -// //add selected axioms from the theory -// parent->theorySelector.perform(probUnits); -// -// env.options->setSineSelection(Options::SS_OFF); -// env.options->forceIncompleteness(); -// } -// else { -// //if there wasn't any sine selection, just put in all theory axioms -// probUnits=UnitList::concat(probUnits, parent->theoryAxioms); -// } - - env.beginOutput(); - CLTBMode::lineOutput() << opt.testId() << " on " << opt.problemName() << endl; - env.endOutput(); - - ProvingHelper::runVampire(prb, opt); - - //set return value to zero if we were successful - if (env.statistics->terminationReason == Statistics::REFUTATION) { - resultValue=0; - } - - System::ignoreSIGHUP(); // don't interrupt now, we need to finish printing the proof ! - - if (!resultValue) { // write the proof to a file - ScopedSemaphoreLocker locker(_syncSemaphore); - locker.lock(); - ofstream out(outFile.c_str()); - UIHelper::outputResult(out); - out.close(); - } else { // write other result to output - env.beginOutput(); - UIHelper::outputResult(env.out()); - env.endOutput(); - } - - exit(resultValue); -} // CLTBProblem::runSlice - -/** - * Return the intended slice time in milliseconds and assign the slice - * vstring with chopped time limit to @b chopped. - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -unsigned CLTBProblem::getSliceTime(vstring sliceCode,vstring& chopped) -{ - unsigned pos = sliceCode.find_last_of('_'); - vstring sliceTimeStr = sliceCode.substr(pos+1); - chopped.assign(sliceCode.substr(0,pos)); - unsigned sliceTime; - ALWAYS(Int::stringToUnsignedInt(sliceTimeStr,sliceTime)); - ASS_G(sliceTime,0); //strategies with zero time don't make sense - - unsigned time = sliceTime + 1; - if (time < 10) { - time++; - } - // convert deciseconds to milliseconds - return time * 100; -} // getSliceTime - -/** - * Start line output by writing the TPTP comment sign and the current - * elapsed time in milliseconds to env.out(). Returns env.out() - * @since 05/06/2013 Vienna - * @author Andrei Voronkov - */ -ostream& CLTBMode::lineOutput() -{ - return env.out() << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") "; -} // CLTBMode::lineOutput - -/** - * Start line output by writing the TPTP comment sign and the current - * elapsed time in milliseconds to cout. Returns cout - * @since 05/06/2013 Vienna - * @author Andrei Voronkov - */ -ostream& CLTBMode::coutLineOutput() -{ - return cout << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") "; -} // CLTBMode::coutLineOutput diff --git a/CASC/CLTBMode.hpp b/CASC/CLTBMode.hpp deleted file mode 100644 index ceabd52a54..0000000000 --- a/CASC/CLTBMode.hpp +++ /dev/null @@ -1,186 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file CLTBMode.hpp - * Defines class CLTBMode. - */ - -#ifndef __CLTBMode__ -#define __CLTBMode__ - -#include - -#include "Forwards.hpp" - -#include "Lib/DHSet.hpp" -#include "Lib/Portability.hpp" -#include "Lib/ScopedPtr.hpp" -#include "Lib/Stack.hpp" - -#include "Lib/VString.hpp" - -#include "Lib/Sys/SyncPipe.hpp" - -#include "Kernel/Problem.hpp" - -#include "Shell/Property.hpp" -#include "Shell/SineUtils.hpp" - -#include "Schedules.hpp" - -namespace CASC { - -using namespace Lib; -using namespace Kernel; - -enum Category { - HH4, - ISA, - HLL, - MZR, - UNKNOWN -}; - -class CLTBProblem; - -class CLTBMode -{ -public: - static void perform(); -private: - void solveBatch(std::istream& batchFile, bool first,vstring inputDirectory); - int readInput(std::istream& batchFile, bool first); - static std::ostream& lineOutput(); - static std::ostream& coutLineOutput(); - void loadIncludes(); - void doTraining(); - void learnFromSolutionFile(vstring& solnFileName); - - typedef List StringList; - typedef Stack StringStack; - typedef std::pair StringPair; - typedef Stack StringPairStack; - - Category getCategory(vstring& categoryStr) { - if (categoryStr == "LTB.HH4" || categoryStr == "LTB.HL4") { - return HH4; - } else if (categoryStr == "LTB.ISA") { - return ISA; - } else if (categoryStr == "LTB.HLL" || categoryStr == "LTB.HOL") { - return HLL; - } else if (categoryStr == "LTB.MZR") { - return MZR; - } else { - return UNKNOWN; - } - } - - Category _category; - vstring _trainingDirectory; - /** per-problem time limit, in milliseconds */ - int _problemTimeLimit; - /** true if question answers should be given */ - bool _questionAnswering; - /** total time used by batches before this one, in milliseconds */ - int _timeUsedByPreviousBatches; - - /** files to be included */ - StringList* _theoryIncludes; - - /** The first vstring in the pair is problem file, the second - * one is output file. The problemFiles[0] is the first - * problem that should be attempted. */ - StringPairStack _problemFiles; - - ScopedPtr _baseProblem; - - // This contains formulas 'learned' in the sense that they were input - // formulas used in proofs of previous problems - // Note: this relies on the assurance that formulas are consistently named - DHSet _learnedFormulas; - DHMap _learnedFormulasCount; - unsigned _learnedFormulasMaxCount; - bool _biasedLearning; - - friend class CLTBProblem; -}; - - -class CLTBProblem -{ -public: - CLTBProblem(CLTBMode* parent, vstring problemFile, vstring outFile); - - [[noreturn]] void searchForProof(int terminationTime,int timeLimit,const Category category); - typedef Set StrategySet; -private: - bool runSchedule(Schedule&,StrategySet& remember,int terminationTime); - unsigned getSliceTime(vstring sliceCode,vstring& chopped); - - void performStrategy(int terminationTime,int timeLimit,Category category,const Shell::Property* property); - static void fillSchedule(Schedule& sched,const Shell::Property* property,int timeLimit,Category category); - - void waitForChildAndExitWhenProofFound(); - [[noreturn]] void exitOnNoSuccess(); - - static std::ofstream* writerFileStream; - [[noreturn]] static void terminatingSignalHandler(int sigNum); - [[noreturn]] void runSlice(vstring slice, unsigned milliseconds); - [[noreturn]] void runSlice(Options& strategyOpt); - - static vstring problemFinishedString; - -#if VDEBUG - DHSet childIds; -#endif - - CLTBMode* parent; - vstring problemFile; - vstring outFile; - - /** - * Problem that is being solved. - * - * This is just a reference to parent's @c baseProblem object into which we - * add problem-specific axioms in the @c searchForProof() function. We can do this, - * because in the current process this child object is the only one that - * will be using the problem object. - */ - Problem& prb; - - Semaphore _syncSemaphore; // semaphore for synchronizing writing if the solution - - /** - * Assumes semaphore object with 1 semaphores (at index 0). - * Locks on demand (once) and releases the lock on destruction. - */ - struct ScopedSemaphoreLocker { // - Semaphore& _sem; - bool locked; - ScopedSemaphoreLocker(Semaphore& sem) : _sem(sem), locked(false) {} - - void lock() { - if (!locked) { - _sem.dec(0); - locked = true; - } - } - - ~ScopedSemaphoreLocker() { - if (locked) { - _sem.inc(0); - } - } - }; -}; - -} - -#endif // __CLTBMode__ diff --git a/CASC/CLTBModeLearning.cpp b/CASC/CLTBModeLearning.cpp deleted file mode 100644 index 2301e60c22..0000000000 --- a/CASC/CLTBModeLearning.cpp +++ /dev/null @@ -1,1202 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file CLTBModeLearning.cpp - * Implements class CLTBModeLearning. - * @since 03/06/2013 updated to conform to the CASC-J6 specification - * @author Andrei Voronkov - */ -#include -#include -#include -#include -#include - -#include "Lib/Portability.hpp" - -#include "Lib/DHSet.hpp" -#include "Lib/Environment.hpp" -#include "Lib/Exception.hpp" -#include "Lib/Int.hpp" -#include "Lib/StringUtils.hpp" -#include "Lib/System.hpp" -#include "Debug/TimeProfiling.hpp" -#include "Lib/Timer.hpp" -#include "Lib/ScopedPtr.hpp" -#include "Lib/Sort.hpp" - -#include "Lib/Sys/Multiprocessing.hpp" -#include "Lib/Sys/SyncPipe.hpp" - -#include "Shell/Options.hpp" -#include "Shell/Normalisation.hpp" -#include "Saturation/ProvingHelper.hpp" -#include "Shell/Statistics.hpp" -#include "Shell/UIHelper.hpp" - -#include "Parse/TPTP.hpp" - -#include "CLTBModeLearning.hpp" - -#define SLOWNESS 1.15 - -using namespace CASC; -using namespace std; -using namespace Lib; -using namespace Lib::Sys; -using namespace Saturation; - -DHMap CLTBModeLearning::probRecords; -DHMap*> CLTBModeLearning::stratWins; - -/** - * The function that does all the job: reads the input files and runs - * Vampires to solve problems. - * @since 05/06/2013 Vienna, adapted for CASC-J6 - * @author Andrei Voronkov - */ -void CLTBModeLearning::perform() -{ - TIME_TRACE("cltb learning"); - - if (env.options->inputFile() == "") { - USER_ERROR("Input file must be specified for ltb mode"); - } - // to prevent from terminating by time limit - env.options->setTimeLimitInSeconds(1000000); - - //UIHelper::szsOutput = true; - env.options->setProof(Options::Proof::TPTP); - env.options->setStatistics(Options::Statistics::NONE); - - vstring line; - vstring inputFile = env.options->inputFile(); - std::size_t found = inputFile.find_last_of("/"); - vstring inputDirectory = "."; - if(found != vstring::npos){ - inputDirectory = inputFile.substr(0,found); - } - - ifstream in(inputFile.c_str()); - if (in.fail()) { - USER_ERROR("Cannot open input file: " + env.options->inputFile()); - } - - //support several batches in one file - bool firstBatch=true; - while (!in.eof()) { - vostringstream singleInst; - bool ready = false; - while (!in.eof()) { - getline(in, line); - singleInst << line << endl; - if (line == "% SZS end BatchProblems") { - ready = true; - break; - } - } - if (!ready) { - break; - } - CLTBModeLearning ltbm; - vistringstream childInp(singleInst.str()); - ltbm.solveBatch(childInp,firstBatch,inputDirectory); - firstBatch=false; - } -} // CLTBModeLearning::perform - -/** - * This function processes a single batch in a batch file. It makes the following - * steps: - *
  1. read the batch file
    2. - *
  2. load the common axioms and put them into a SInE selector
    3. - *
  3. spawn child processes that try to prove a problem by calling - * CLTBProblemLearning::searchForProof(). These processes are run sequentially and the time - * limit for each one is computed depending on the per-problem time limit, - * batch time limit, and time spent on this batch so far. The termination - * time for the proof search for a problem will be passed to - * CLTBProblemLearning::searchForProof() as an argument.
- * @author Andrei Voronkov - * @since 04/06/2013 flight Manchester-Frankfurt - */ -void CLTBModeLearning::solveBatch(istream& batchFile, bool first,vstring inputDirectory) -{ - // fill the global strats up - fillSchedule(strats); - - // this is the time in milliseconds since the start when this batch file should terminate - _timeUsedByPreviousBatches = env.timer->elapsedMilliseconds(); - coutLineOutput() << "Starting Vampire on the batch file " << "\n"; - int terminationTime = readInput(batchFile,first); - loadIncludes(); - - int surplus = 0; - { // do some startup training - coutLineOutput() << "Performing startup training " << endl; - coutLineOutput() << "Loading problems from " << (_trainingDirectory+"/Problems") << endl; - System::readDir(_trainingDirectory+"/Problems",problems); - - int elapsedTime = env.timer->elapsedMilliseconds(); - int doTrainingFor = 2*_problemTimeLimit; - doTraining(doTrainingFor,true); - int trainingElapsed = env.timer->elapsedMilliseconds(); - int trainingTime = trainingElapsed-elapsedTime; - // we begin with negative surplus - surplus = -trainingTime; - coutLineOutput() << "training took " << trainingTime << endl; - } - - int solvedProblems = 0; - int remainingProblems = _problemFiles.size(); - StringPairStack::BottomFirstIterator probs(_problemFiles); - while (probs.hasNext()) { - StringPair res=probs.next(); - - vstring probFile= inputDirectory+"/"+res.first; - new_problems.push(probFile); - vstring outFile= res.second; - vstring outDir = env.options->ltbDirectory(); - if(!outDir.empty()){ - std::size_t found = outFile.find_last_of("/"); - if(found != vstring::npos){ - outFile = outFile.substr(found); - } - outFile= outDir+"/"+outFile; - } - - // calculate the next problem time limit in milliseconds - int elapsedTime = env.timer->elapsedMilliseconds(); - int timeRemainingForThisBatch = terminationTime - elapsedTime; - coutLineOutput() << "time remaining for this batch " << timeRemainingForThisBatch << endl; - int remainingBatchTimeForThisProblem = timeRemainingForThisBatch / remainingProblems; - coutLineOutput() << "remaining batch time for this problem " << remainingBatchTimeForThisProblem << endl; - int nextProblemTimeLimit; - if (!_problemTimeLimit) { - nextProblemTimeLimit = remainingBatchTimeForThisProblem; - } - else if (remainingBatchTimeForThisProblem > _problemTimeLimit) { - nextProblemTimeLimit = _problemTimeLimit; - } - else { - nextProblemTimeLimit = remainingBatchTimeForThisProblem; - } - // time in milliseconds when the current problem should terminate - int problemTerminationTime = elapsedTime + nextProblemTimeLimit; - coutLineOutput() << "problem termination time " << problemTerminationTime << endl; - - env.beginOutput(); - env.out() << flush << "%" << endl; - lineOutput() << "SZS status Started for " << probFile << endl << flush; - env.endOutput(); - - pid_t child = Multiprocessing::instance()->fork(); - if (!child) { - TIME_TRACE_NEW_ROOT("child process") - // child process - CLTBProblemLearning prob(this, probFile, outFile); - try { - prob.searchForProof(problemTerminationTime,nextProblemTimeLimit,strats,true); - } catch (Exception& exc) { - cerr << "% Exception at proof search level" << endl; - exc.cry(cerr); - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code - } - // searchForProof() function should never return - ASSERTION_VIOLATION; - } - - env.beginOutput(); - lineOutput() << "solver pid " << child << endl; - env.endOutput(); - int resValue; - // wait until the child terminates - try { - ALWAYS( - Multiprocessing::instance()->waitForChildTermination(resValue) == child - ); - } - catch(SystemFailException& ex) { - cerr << "% SystemFailException at batch level" << endl; - ex.cry(cerr); - } - - // output the result depending on the termination code - env.beginOutput(); - if (!resValue) { - lineOutput() << "SZS status Theorem for " << probFile << endl; - solvedProblems++; - } - else { - lineOutput() << "SZS status GaveUp for " << probFile << endl; - } - env.out() << flush << '%' << endl; - lineOutput() << "% SZS status Ended for " << probFile << endl << flush; - env.endOutput(); - - Timer::syncClock(); - - remainingProblems--; - - // If we used less than the time limit to solve this problem then do some more training - int timeNow = env.timer->elapsedMilliseconds(); - int timeTaken = timeNow - elapsedTime; - int timeLeft = nextProblemTimeLimit - timeTaken; - // update running surplus (which might be negative to start with due to startup training) - surplus = surplus+timeLeft; - // only do training if we have at least 5 seconds surplus - coutLineOutput() << "Have " << surplus << " surplus time for training" << endl; - if(surplus>5000){ - doTraining(surplus,false); - // update surplus with actual time taken - int trainingElapsed = env.timer->elapsedMilliseconds(); - int trainingTime = trainingElapsed-timeNow; - surplus = surplus-trainingTime; - coutLineOutput() << "training time " << trainingTime << endl; - } - - } - env.beginOutput(); - lineOutput() << "Solved " << solvedProblems << " out of " << _problemFiles.size() << endl; - env.endOutput(); -} // CLTBModeLearning::solveBatch(batchFile) - -void CLTBModeLearning::loadIncludes() -{ - UnitList* theoryAxioms=0; - { - TIME_TRACE(TimeTrace::PARSING); - env.statistics->phase=Statistics::PARSING; - - StringList::Iterator iit(_theoryIncludes); - while (iit.hasNext()) { - vstring fname=env.options->includeFileName(iit.next()); - - ifstream inp(fname.c_str()); - if (inp.fail()) { - USER_ERROR("Cannot open included file: "+fname); - } - Parse::TPTP parser(inp); - parser.parse(); - UnitList* funits = parser.units(); - if (parser.containsConjecture()) { - USER_ERROR("Axiom file " + fname + " contains a conjecture."); - } - - UnitList::Iterator fuit(funits); - while (fuit.hasNext()) { - fuit.next()->inference().markIncluded(); - } - theoryAxioms=UnitList::concat(funits,theoryAxioms); - } - } - - _baseProblem = new Problem(theoryAxioms); - //ensure we scan the theory axioms for property here, so we don't need to - //do it afterward in each problem - _baseProblem->getProperty(); - env.setMainProblem(_baseProblem.ptr()); - env.statistics->phase=Statistics::UNKNOWN_PHASE; -} // CLTBModeLearning::loadIncludes - -void CLTBModeLearning::doTraining(int time, bool startup) -{ - static Stack::Iterator* prob_iter = 0; - - if(startup || (prob_iter && !prob_iter->hasNext())){ - problems.loadFromIterator(Stack::BottomFirstIterator(new_problems)); - while(!new_problems.isEmpty()){new_problems.pop();} - prob_iter = new Stack::Iterator(problems); - } - ASS(prob_iter); - - vstring outFile = "temp"; - // try and solve the next problem(s) - while(prob_iter->hasNext()){ - - // randomise strategies - Stack randStrats; - while(!strats.isEmpty()){ - int index = Lib::Random::getInteger(strats.length()); - vstring strat = strats[index]; - strats.remove(strat); - randStrats.push(strat); - } - strats.loadFromIterator(Stack::Iterator(randStrats)); - - vstring probFile = prob_iter->next(); - coutLineOutput() << "Training on " << probFile << endl; - - // spend 5s on this problem - - int elapsedTime = env.timer->elapsedMilliseconds(); - int problemTerminationTime = elapsedTime + 5000; - - pid_t child = Multiprocessing::instance()->fork(); - if (!child) { - CLTBProblemLearning prob(this, probFile, outFile); - try { - prob.searchForProof(problemTerminationTime,5000,strats,false); - } catch (Exception& exc) { - } - ASSERTION_VIOLATION; - } - int resValue; - try { - ALWAYS( - Multiprocessing::instance()->waitForChildTermination(resValue) == child - ); - } - catch(SystemFailException& ex) { - cerr << "% SystemFailException at batch level" << endl; - ex.cry(cerr); - } - if(!resValue){ - coutLineOutput() << "solved in training" << endl; - } - int timeNow = env.timer->elapsedMilliseconds(); - int timeTaken = timeNow - elapsedTime; - time = time-timeTaken; - if(time<5000) break; // we want at least 5 seconds - coutLineOutput() << "time left for training " << time << endl; - } - coutLineOutput() << "Collect feedback" << endl; - - // it is important that we know that nobody will be using the semaphores etc - if(stratSem.get(0)){ - strategies->acquireRead(); - istream& sin = strategies->in(); - while(stratSem.get(0)){ - stratSem.dec(0); - vstring strat; - getline(sin,strat); - vstring prob; - getline(sin,prob); - vstring result; - getline(sin,result); - unsigned resValue; - if(!Lib::Int::stringToUnsignedInt(result,resValue)){ resValue=1;} // if we cannot read say it failed - coutLineOutput() << "feedback: " << strat << " on " << prob << " with " << resValue << endl; - ProbRecord* rec = 0; - if(!probRecords.find(prob,rec)){ - rec = new ProbRecord(); - probRecords.insert(prob,rec); - } - if(!resValue){ - rec->suc.insert(strat); - Stack* probs = 0; - if(!stratWins.find(strat,probs)){ - probs = new Stack(); - stratWins.insert(strat,probs); - } - probs->push(prob); - } - else{ rec->fail.insert(strat); } - } - strategies->releaseRead(); - } - coutLineOutput() << "computing scores" << endl; - // Compute the scores - Stack nextStrats; - DHMap scores; - Stack::Iterator sit(strats); - while(sit.hasNext()){ scores.insert(sit.next(),0); } - - // find first strategy and load up scores - float highest = 0; - vstring first_strat = strats[0]; - DHMap::Iterator pit(probRecords); - while(pit.hasNext()){ - vstring prob; - ProbRecord* rec; - pit.next(prob,rec); - unsigned suc = rec->suc.size(); - if(suc==0) continue; - unsigned fail = rec->fail.size(); - unsigned total = suc+fail; - float avg = total / ((float) suc); - rec->avg=avg; - Stack::Iterator sit(strats); - while(sit.hasNext()){ - vstring strat = sit.next(); - if(rec->fail.contains(strat)) continue; - float& sc = scores.get(strat); - if(rec->suc.contains(strat)){sc=sc+1;} - else{ sc=sc+avg; } - if(sc>highest){ highest=sc;first_strat=strat; } - } - } - nextStrats.push(first_strat); - strats.remove(first_strat); - vstring next_strat=first_strat; - unsigned c=1; - coutLineOutput() << (c++) << ":" << next_strat << " (" << highest <<")" << endl; - while(!strats.isEmpty()){ - // decrease for last added - Stack* wins; - if(stratWins.find(next_strat,wins)){ - Stack::Iterator wit(*wins); - while(wit.hasNext()){ - vstring prb = wit.next(); - ProbRecord* rec = probRecords.get(prb); - if(rec->suc.size()==0) continue; - Stack::Iterator sit(strats); - while(sit.hasNext()){ - vstring s = sit.next(); - if(rec->fail.contains(s)) continue; - float& sc = scores.get(s); - if(rec->suc.contains(s)){sc=sc-1;} - else{sc=sc-rec->avg;} - } - } - } - // now recompute best - float highest = 0; - next_strat = strats.top(); - Stack::Iterator sit(strats); - while(sit.hasNext()){ - vstring strat = sit.next(); - float sc = scores.get(strat); - if(sc>highest){ - highest=sc; - next_strat=strat; - } - } - nextStrats.push(next_strat); - strats.remove(next_strat); - coutLineOutput() << (c++) << ":" << next_strat << " (" << highest <<")" << endl; - } - - //TODO check that this loads them in the right order!! - strats.loadFromIterator(Stack::BottomFirstIterator(nextStrats)); - -} // CLTBModeLearning::doTraining - -/** - * Read a single batch file from @b in. Return the time in milliseconds since - * the start, when the process should terminate. If the batch contains no overall - * time limit, return a very large integer value. - * Set _problemTimeLimit to the per-problem time limit from - * the batch file. - * @since 04/06/2013 flight Manchester-Frankfurt - * @author Andrei Voronkov - */ -int CLTBModeLearning::readInput(istream& in, bool first) -{ - vstring line, word; - - if(first){ - getline(in,line); - if (line.find("division.category") != vstring::npos){ - StringStack ls; - StringUtils::splitStr(line.c_str(),' ',ls); - coutLineOutput() << "read category " << ls[1] << endl; - - } - else{ USER_ERROR("division category not found"); } - - // Get training directory - getline(in,line); - if (line.find("training_directory") != vstring::npos){ - StringStack ls; - StringUtils::splitStr(line.c_str(),' ',ls); - _trainingDirectory = ls[1]; - } - else{ USER_ERROR("training_directory not found"); } - - } - - getline(in,line); - if (line!="% SZS start BatchConfiguration") { - USER_ERROR("\"% SZS start BatchConfiguration\" expected, \""+line+"\" found."); - } - - getline(in, line); - - _questionAnswering = false; - _problemTimeLimit = -1; - int batchTimeLimit = -1; - - StringStack lineSegments; - while (!in.eof() && line!="% SZS end BatchConfiguration") { - lineSegments.reset(); - StringUtils::splitStr(line.c_str(), ' ', lineSegments); - vstring param = lineSegments[0]; - if (param == "output.required" || param == "output.desired") { - if (lineSegments.find("Answer")) { - _questionAnswering = true; - } - } - else if (param == "execution.order") { - // we ignore this for now and always execute in order - } - else - if (param == "limit.time.problem.wc") { - - if (lineSegments.size() != 2 || - !Int::stringToInt(lineSegments[1], _problemTimeLimit)) { - USER_ERROR("unexpected \""+param+"\" specification: \""+line+"\""); - } - _problemTimeLimit = 1000 * _problemTimeLimit; - } - else if (param == "limit.time.overall.wc") { - if (lineSegments.size() != 2 || - !Int::stringToInt(lineSegments[1], batchTimeLimit)) { - USER_ERROR("unexpected \"" + param + "\" specification: \""+ line +"\""); - } - batchTimeLimit = 1000 * batchTimeLimit; - } - else { - USER_ERROR("unknown batch configuration parameter: \""+line+"\""); - } - - getline(in, line); - } - - if (line != "% SZS end BatchConfiguration") { - USER_ERROR("\"% SZS end BatchConfiguration\" expected, \"" + line + "\" found."); - } - if (_questionAnswering) { - env.options->setQuestionAnswering(Options::QuestionAnsweringMode::ANSWER_LITERAL); - } - - getline(in, line); - if (line!="% SZS start BatchIncludes") { - USER_ERROR("\"% SZS start BatchIncludes\" expected, \""+line+"\" found."); - } - - _theoryIncludes=0; - for (getline(in, line); line[0]!='%' && !in.eof(); getline(in, line)) { - size_t first=line.find_first_of('\''); - size_t last=line.find_last_of('\''); - if (first == vstring::npos || first == last) { - USER_ERROR("Include specification must contain the file name enclosed in the ' characters:\""+line+"\"."); - } - ASS_G(last,first); - vstring fname=line.substr(first+1, last-first-1); - StringList::push(fname, _theoryIncludes); - } - - while (!in.eof() && line == "") { getline(in, line); } - if (line!="% SZS end BatchIncludes") { - USER_ERROR("\"% SZS end BatchIncludes\" expected, \""+line+"\" found."); - } - getline(in, line); - if (line!="% SZS start BatchProblems") { - USER_ERROR("\"% SZS start BatchProblems\" expected, \""+line+"\" found."); - } - - for (getline(in, line); line[0]!='%' && !in.eof(); getline(in, line)) { - size_t spc=line.find(' '); - size_t lastSpc=line.find(' ', spc+1); - if (spc == vstring::npos || spc == 0 || spc == line.length()-1) { - USER_ERROR("Two file names separated by a single space expected:\""+line+"\"."); - } - vstring inp=line.substr(0,spc); - vstring outp=line.substr(spc+1, lastSpc-spc-1); - _problemFiles.push(make_pair(inp, outp)); - } - - while (!in.eof() && line == "") { - getline(in, line); - } - if (line!="% SZS end BatchProblems") { - USER_ERROR("\"% SZS end BatchProblems\" expected, \""+line+"\" found."); - } - - if (batchTimeLimit == -1) { // batch time limit is undefined - if (_problemTimeLimit == -1) { - USER_ERROR("either the problem time limit or the batch time limit must be specified"); - } - // to avoid overflows when added to the current elapsed time, make it less than INT_MAX - return INT_MAX / 8; - } - - // batch time limit is defined - if (_problemTimeLimit == -1) { - _problemTimeLimit = 0; - } - return _timeUsedByPreviousBatches + batchTimeLimit; -} // CLTBModeLearning::readInput - -vstring CLTBProblemLearning::problemFinishedString = "##Problem finished##vn;3-d-ca-12=1;'"; - -CLTBProblemLearning::CLTBProblemLearning(CLTBModeLearning* parent, vstring problemFile, vstring outFile) - : parent(parent), problemFile(problemFile), outFile(outFile), - prb(*parent->_baseProblem), _syncSemaphore(1) -{ - //add the privileges into the semaphore - _syncSemaphore.set(0,1); -} - -void CLTBModeLearning::fillSchedule(CLTBModeLearning::Schedule& sched) { - sched.push("ins+11_3_ep=RST:fde=unused:gsp=input_only:igbrr=0.4:igrr=1/8:igrpq=1.5:igs=1:igwr=on:lcm=predicate:nwc=1:sd=2:ss=axioms:st=3.0:sos=all:spl=off:updr=off:dm=on:uhcvi=on_60"); // HLL 1 (1373) - sched.push("lrs-4_5:4_bd=off:bs=unit_only:bsr=on:cond=on:fde=none:gs=on:gsaa=full_model:gsem=off:nm=0:nwc=1.1:nicw=on:stl=300:sd=1:ss=axioms:st=2.0:sos=on:sac=on:sfr=on:ssfp=10000:ssfq=1.0:smm=off:ssnc=none:sp=reverse_arity:urr=on:updr=off_60"); // HLL 2 (382) - sched.push("dis+1002_1_ep=RST:gs=on:gsaa=full_model:gsem=on:nm=64:nwc=1:sd=7:ss=axioms:st=1.2:sos=on:sser=off:ssfp=40000:ssfq=1.2:ssnc=none:updr=off:uhcvi=on_60"); // HLL 3 (170) - sched.push("dis+1002_1_gs=on:gsem=off:nwc=1:sd=3:ss=axioms:sos=on:sac=on:ssfp=1000:ssfq=1.4:smm=sco:ssnc=none:sp=reverse_arity:urr=on_60"); // HLL 4 (148) - sched.push("lrs+1011_4:1_bd=off:bsr=unit_only:ccuc=small_ones:fsr=off:fde=unused:gs=on:gsssp=full:nm=64:nwc=4:stl=300:sd=1:ss=priority:sac=on:sscc=model:sdd=large:sser=off:sfr=on:ssfp=100000:ssfq=1.2:ssnc=all:uhcvi=on_60"); // HLL 5 (68) - sched.push("ins+11_5_br=off:ep=RST:fde=none:gsp=input_only:gs=on:gsem=on:igbrr=0.5:igpr=on:igrp=1400:igrpq=1.3:igs=1:igwr=on:nm=0:nwc=1:sd=1:ss=axioms:st=2.0:sos=all:spl=off:urr=on:updr=off:dm=on_60"); // HLL 6 (64) - sched.push("lrs+10_1_bsr=unit_only:cond=fast:gs=on:gsem=off:gsssp=full:lcm=reverse:nwc=1:stl=300:sd=2:ss=axioms:st=5.0:sos=on:sac=on:sfr=on:ssfp=1000:ssfq=2.0:smm=sco:ssnc=none:sp=reverse_arity:urr=on:updr=off_60"); // HLL 7 (62) - sched.push("dis+10_3:1_ep=RST:gsp=input_only:gs=on:gsem=on:lcm=reverse:nwc=1.1:sd=2:ss=priority:st=2.0:sos=on:sac=on:sdd=large:sser=off:ssfp=10000:ssfq=1.1:ssnc=none:sp=reverse_arity_60"); // HLL 8 (42) - sched.push("lrs+1011_3:1_bd=off:bsr=on:cond=fast:gs=on:gsem=on:lwlo=on:nwc=10:stl=300:sd=1:ss=axioms:st=3.0:spl=off:sp=occurrence:updr=off:uhcvi=on_60"); // HLL 9 (35) - sched.push("lrs+1011_5:1_fde=none:gs=on:gsem=on:nwc=4:stl=300:sd=1:ss=axioms:st=5.0:spl=off:sp=occurrence:urr=on:uhcvi=on_60"); // HLL 10 (25) - sched.push("ins+11_4_fsr=off:fde=unused:gsp=input_only:gs=on:igbrr=0.3:igrr=1/4:igrp=700:igrpq=1.3:igs=1:igwr=on:lcm=reverse:nwc=1:sd=2:ss=axioms:st=1.2:sos=on:spl=off:sp=reverse_arity:updr=off:uhcvi=on_60"); // HLL 11 (22) - sched.push("ott+11_2:3_cond=on:ep=RST:fsr=off:fde=none:gsp=input_only:lcm=predicate:nwc=1:sd=3:ss=priority:sos=all:sac=on:ssac=none:sser=off:ssfp=100000:ssfq=1.2:ssnc=all_dependent:urr=ec_only_60"); // HLL 12 (21) - sched.push("dis+1011_5:1_ep=RSTC:fde=unused:gs=on:gsssp=full:lwlo=on:nm=0:nwc=1:sd=1:ss=axioms:st=3.0:sos=on:spl=off:sp=occurrence:updr=off:uhcvi=on_60"); // HLL 13 (16) - sched.push("dis+1011_5:1_cond=fast:fsr=off:fde=none:gs=on:gsaa=from_current:nwc=3:sd=2:ss=axioms:sac=on:ssfp=100000:ssfq=1.0:smm=sco:ssnc=none:sp=reverse_arity:urr=on:updr=off_60"); // HLL 14 (14) - sched.push("lrs+11_3_cond=fast:gsp=input_only:gs=on:gsem=on:gsssp=full:lcm=predicate:nwc=1:stl=300:sd=2:ss=axioms:sos=on:sac=on:sdd=large:sfr=on:ssfp=100000:ssfq=1.0:smm=sco:ssnc=none:updr=off:uhcvi=on_60"); // HLL 15 (14) - sched.push("dis+1011_2:1_cond=fast:ep=RST:fsr=off:gs=on:gsem=off:gsssp=full:nwc=1:sd=1:ss=axioms:sos=on:sdd=large:sser=off:sfr=on:ssfp=4000:ssfq=1.1:ssnc=none:sp=reverse_arity_60"); // HLL 16 (13) - sched.push("dis+1011_1_cond=fast:ep=RST:gs=on:nwc=1:sd=2:ss=axioms:st=1.5:sos=on:sac=on:smm=sco:ssnc=none:urr=ec_only_60"); // HLL 17 (12) - sched.push("lrs+10_4_bd=off:bsr=unit_only:fde=none:gs=on:lcm=reverse:nwc=1:stl=300:sd=3:ss=axioms:st=3.0:sos=on:spl=off:uhcvi=on_60"); // HLL 18 (11) - sched.push("dis+1002_7_bsr=unit_only:cond=fast:nm=64:nwc=1:sd=1:ss=axioms:sos=on:sac=on:sfr=on:ssfp=100000:ssfq=1.4:ssnc=none:uhcvi=on_60"); // HLL 19 (11) - sched.push("lrs+10_5_bd=off:cond=fast:fde=unused:gsp=input_only:gs=on:gsem=on:gsssp=full:nwc=1:stl=300:sd=2:ss=axioms:sos=on:spl=off:urr=on:updr=off:uhcvi=on_60"); // HLL 20 (10) - sched.push("dis+2_4_bd=off:cond=fast:fsr=off:fde=none:gs=on:gsem=on:lcm=reverse:lwlo=on:nwc=1:sd=3:ss=axioms:st=1.5:sos=on:spl=off:sp=occurrence:uhcvi=on_60"); // HLL 21 (9) - sched.push("lrs+1010_5:1_bs=unit_only:bsr=on:fde=none:gs=on:gsem=off:gsssp=full:lcm=reverse:nm=0:nwc=4:stl=300:sd=3:ss=priority:st=1.2:sos=on:ssac=none:sscc=model:sfr=on:ssfp=1000:ssfq=1.0:smm=off:urr=on:uhcvi=on_60"); // HLL 22 (8) - sched.push("lrs-11_8:1_bsr=on:cond=on:fde=none:lcm=reverse:nm=0:nwc=1.5:stl=300:sd=2:ss=priority:spl=off:sp=occurrence_60"); // HLL 23 (7) - sched.push("dis+1002_3_cond=on:ep=RS:fsr=off:gs=on:gsaa=full_model:gsem=off:nm=0:nwc=1:sd=5:ss=axioms:st=2.0:sos=on:ssfp=4000:ssfq=1.4:smm=off:ssnc=none:updr=off_60"); // HLL 24 (7) - sched.push("dis+1003_5_cond=on:fsr=off:fde=none:gs=on:gsem=off:nwc=1:sos=on:sdd=large:sser=off:sfr=on:ssfp=100000:ssfq=1.0:ssnc=all_dependent:sp=reverse_arity:urr=ec_only:uhcvi=on_60"); // HLL 25 (6) - sched.push("lrs+10_5:4_bd=off:gs=on:gsssp=full:lcm=reverse:nwc=1:stl=300:sd=1:ss=axioms:sos=on:sac=on:sdd=off:sfr=on:ssfp=10000:ssfq=1.4:smm=sco:ssnc=none:sp=reverse_arity:updr=off:uhcvi=on_60"); // HLL 26 (6) - sched.push("lrs+11_4:1_br=off:cond=on:fsr=off:fde=unused:gsp=input_only:gs=on:gsssp=full:lcm=predicate:nm=0:nwc=1:stl=300:sd=1:ss=axioms:spl=off:sp=occurrence:urr=on_60"); // HLL 27 (6) - sched.push("lrs+1010_5_cond=fast:ep=RST:gs=on:gsaa=from_current:gsem=on:nwc=1:stl=300:sd=4:ss=axioms:st=1.5:sos=on:sac=on:sdd=off:ssfp=4000:ssfq=2.0:smm=sco:ssnc=none:sp=reverse_arity:uhcvi=on_60"); // HLL 28 (6) - sched.push("lrs+11_3_bd=off:cond=fast:fde=none:gsp=input_only:gs=on:gsaa=from_current:gsem=on:gsssp=full:nwc=1:stl=300:sd=1:ss=axioms:sos=all:sdd=large:sser=off:sfr=on:ssfp=4000:ssfq=2.0:ssnc=none:sp=occurrence:urr=on:updr=off_60"); // HLL 29 (5) - sched.push("lrs+4_5:4_bd=off:bs=on:bsr=unit_only:cond=fast:fde=unused:gs=on:gsem=off:nwc=1:stl=300:sd=2:ss=axioms:st=2.0:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // HLL 30 (5) - sched.push("lrs+11_5:1_bd=off:br=off:cond=fast:gsp=input_only:gs=on:gsem=on:gsssp=full:lcm=predicate:nwc=1.1:stl=300:sd=2:ss=priority:st=3.0:spl=off:sp=occurrence:urr=on:uhcvi=on_60"); // HLL 31 (5) - sched.push("dis+1011_3:2_cond=fast:ep=RST:fsr=off:fde=unused:gsp=input_only:gs=on:gsem=off:nm=0:nwc=1:sd=1:ss=priority:sos=all:sdd=large:ssnc=all:sp=occurrence_60"); // HLL 32 (5) - sched.push("lrs+11_3:1_br=off:cond=fast:ep=R:fsr=off:gs=on:nwc=1:stl=300:sd=2:ss=priority:st=2.0:sos=all:spl=off:sp=occurrence:urr=on:updr=off:uhcvi=on_60"); // HLL 33 (4) - sched.push("lrs+11_3_bsr=unit_only:cond=on:ep=RST:gsp=input_only:nwc=1.7:stl=300:sd=3:ss=axioms:st=5.0:sos=all:sac=on:sfr=on:ssfp=100000:ssfq=1.1:ssnc=all_dependent:sp=reverse_arity:updr=off:uhcvi=on_60"); // HLL 34 (4) - sched.push("ins+11_5_ep=RS:fsr=off:gs=on:igbrr=0.4:igpr=on:igrr=1/2:igrp=4000:igrpq=1.2:igs=1010:igwr=on:nwc=1:sd=1:ss=axioms:st=3.0:sos=all:spl=off:sp=reverse_arity:urr=on:updr=off_60"); // HLL 35 (3) - sched.push("dis+1010_2:3_bs=unit_only:bsr=unit_only:cond=fast:fsr=off:fde=unused:gs=on:gsem=on:gsssp=full:nm=0:nwc=3:sd=4:ss=priority:st=1.5:sos=on:sscc=on:sdd=off:sser=off:sfr=on:ssfp=100000:ssfq=1.0:sp=reverse_arity:uhcvi=on_60"); // HLL 36 (3) - sched.push("dis+1010_5:4_bd=off:fsr=off:fde=unused:gs=on:nm=64:nwc=1:sd=4:ss=axioms:st=1.2:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // HLL 37 (3) - sched.push("lrs+1011_8:1_bd=off:bsr=unit_only:fde=none:gs=on:lwlo=on:nm=0:nwc=1.5:stl=300:sd=1:ss=axioms:st=1.2:spl=off:sp=occurrence:updr=off_60"); // HLL 38 (3) - sched.push("dis+4_5:4_bd=off:fsr=off:fde=unused:gs=on:nwc=1:sd=5:ss=axioms:st=1.5:sos=all:spl=off:sp=occurrence:uhcvi=on_60"); // HLL 39 (3) - sched.push("dis+1011_3_cond=fast:ep=R:gs=on:gsem=off:lwlo=on:nm=0:nwc=1:sd=5:ss=axioms:st=1.5:sos=on:sac=on:sdd=large:sfr=on:ssfp=1000:ssfq=1.1:ssnc=none:uhcvi=on_60"); // HLL 40 (2) - sched.push("dis+1002_3_gs=on:gsem=off:nwc=1.2:sd=2:ss=axioms:st=3.0:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // ISA 1 (1149) - sched.push("dis+1011_3:2_bsr=unit_only:cond=fast:nwc=3:nicw=on:sd=3:ss=priority:sdd=off:sfr=on:ssfp=10000:ssfq=1.2:uhcvi=on_60"); // ISA 2 (347) - sched.push("lrs+1010_1_cond=on:fde=none:gs=on:gsem=off:nwc=1:stl=300:sd=1:ss=axioms:st=3.0:sos=on:sac=on:ssfp=10000:ssfq=1.1:smm=sco:ssnc=none:urr=on:updr=off_60"); // ISA 3 (174) - sched.push("lrs-2_3_ep=RS:gs=on:gsaa=from_current:nwc=1:stl=300:sd=2:ss=axioms:sos=on:sac=on:sfr=on:ssfp=40000:ssfq=1.0:smm=off:ssnc=none:sp=reverse_arity:uhcvi=on_60"); // ISA 4 (93) - sched.push("dis+1011_5_fsr=off:fde=unused:nm=64:nwc=3:sd=2:ss=priority:spl=off:sp=occurrence:uhcvi=on_60"); // ISA 5 (58) - sched.push("dis+1002_4_cond=on:gs=on:gsem=off:nwc=1:sd=1:ss=axioms:sos=on:sac=on:sfr=on:ssfp=1000:ssfq=1.2:smm=sco:ssnc=none:sp=occurrence:uhcvi=on_60"); // ISA 6 (52) - sched.push("dis+1002_4_ep=RST:fsr=off:gs=on:gsem=off:lwlo=on:nwc=1:sd=4:ss=axioms:st=1.5:sos=on:sser=off:sfr=on:ssfp=40000:ssfq=1.2:ssnc=none_60"); // ISA 7 (39) - sched.push("lrs+1011_3:2_bd=off:cond=on:gsp=input_only:gs=on:gsem=on:nm=0:nwc=4:stl=300:sd=1:ss=axioms:sser=off:sfr=on:ssfp=40000:ssfq=1.1:ssnc=all_dependent:sp=reverse_arity:updr=off_60"); // ISA 8 (34) - sched.push("dis+1011_1_bsr=on:ccuc=first:nm=0:nwc=4:sd=2:ss=priority:sscc=model:sdd=large:sfr=on:smm=off:ssnc=none:updr=off:uhcvi=on_60"); // ISA 9 (32) - sched.push("lrs+1002_4_bd=off:fde=none:gs=on:gsaa=from_current:gsem=off:gsssp=full:nwc=1:stl=300:sd=3:ss=axioms:st=5.0:sos=on:sser=off:ssfp=100000:ssfq=1.1:ssnc=none:sp=reverse_arity_60"); // ISA 10 (29) - sched.push("dis+1002_5_cond=fast:fsr=off:fde=none:gs=on:gsaa=full_model:gsem=off:gsssp=full:nwc=1:sd=1:ss=axioms:st=5.0:sos=on:sac=on:sdd=large:ssfp=40000:ssfq=1.1:smm=off:ssnc=none:sp=reverse_arity:updr=off_60"); // ISA 11 (25) - sched.push("dis+1011_3_fde=unused:nm=64:nwc=1:sd=2:ss=axioms:st=5.0:sdd=off:sser=off:ssfp=10000:ssfq=1.0:sp=occurrence_60"); // ISA 12 (20) - sched.push("dis+1011_3:1_cond=fast:ep=RS:nm=0:nwc=1.7:sd=2:ss=priority:st=1.2:sdd=off:ssfp=10000:ssfq=1.2:smm=sco:ssnc=all:sp=occurrence:updr=off:uhcvi=on_60"); // ISA 13 (16) - sched.push("dis+1002_5_cond=on:ep=RST:fsr=off:fde=unused:gs=on:gsem=on:nwc=1:sd=2:ss=axioms:st=1.2:sos=on:sac=on:sdd=off:sfr=on:smm=sco:ssnc=none:updr=off:uhcvi=on_60"); // ISA 14 (16) - sched.push("dis+1011_5_cond=on:er=filter:fde=none:nm=64:nwc=3:sd=2:ss=priority:st=2.0:spl=off:sp=occurrence:updr=off:uhcvi=on_60"); // ISA 15 (12) - sched.push("lrs+10_3:1_cond=on:fde=none:gs=on:gsem=off:gsssp=full:nwc=1.2:stl=300:sd=1:ss=priority:sos=on:sac=on:sdd=off:ssfp=1000:ssfq=1.4:smm=sco:ssnc=all:sp=reverse_arity:urr=on:updr=off:uhcvi=on_60"); // ISA 16 (12) - sched.push("lrs+11_5_br=off:cond=on:fde=none:gs=on:nwc=1:stl=300:sd=2:ss=axioms:st=3.0:sos=all:sdd=off:sfr=on:ssfp=40000:ssfq=1.4:ssnc=none:sp=reverse_arity:urr=on_60"); // ISA 17 (10) - sched.push("dis+1002_3_bd=off:fde=unused:gs=on:gsaa=from_current:gsem=off:nwc=1:sd=2:ss=axioms:st=1.2:sos=on:sfr=on:smm=sco:ssnc=none:sp=occurrence_60"); // ISA 18 (10) - sched.push("ins+11_4_cond=fast:fde=none:igbrr=0.4:igrr=1/32:igrp=200:igrpq=1.2:igs=1003:igwr=on:nwc=10:sd=1:ss=axioms:st=5.0:spl=off_60"); // ISA 19 (10) - sched.push("lrs+1011_4:1_fsr=off:fde=unused:gs=on:gsem=on:gsssp=full:nm=64:nwc=4:stl=300:sd=1:ss=priority:st=3.0:ssac=none:sscc=on:sfr=on:ssfp=40000:ssfq=1.2:smm=sco:ssnc=all:sp=reverse_arity:updr=off:uhcvi=on_60"); // ISA 20 (9) - sched.push("dis+1002_50_fde=unused:nwc=1:sd=2:ss=axioms:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // ISA 21 (8) - sched.push("ott+11_4_cond=fast:fde=none:gs=on:gsem=on:gsssp=full:nwc=1:sd=2:ss=axioms:sos=on:spl=off:sp=occurrence:urr=on:updr=off:uhcvi=on_60"); // ISA 22 (8) - sched.push("dis-3_3_ep=RST:fde=none:nm=64:nwc=1:sd=4:ss=axioms:sos=on:spl=off:sp=occurrence:uhcvi=on_60"); // ISA 23 (7) - sched.push("dis+1010_7_fsr=off:fde=unused:nm=0:nwc=1.3:nicw=on:sd=3:ss=priority:sfr=on:ssfp=100000:ssfq=1.0:smm=sco:ssnc=none:updr=off:uhcvi=on_60"); // ISA 24 (7) - sched.push("dis+1002_4_cond=fast:ep=RST:fsr=off:nwc=1:sd=3:ss=axioms:st=2.0:sos=on:ssfp=10000:ssfq=1.1:smm=sco:sp=occurrence:uhcvi=on_60"); // ISA 25 (6) - sched.push("ott+1011_2_bd=off:ccuc=first:cond=on:fsr=off:fde=unused:gs=on:gsaa=from_current:gsem=on:nm=64:nwc=1.3:sd=3:ss=priority:st=1.2:sac=on:sscc=on:sdd=off:ssfp=4000:ssfq=1.4:smm=sco:ssnc=none:urr=ec_only:updr=off:uhcvi=on_60"); // ISA 26 (6) - sched.push("dis+1002_3_bd=off:gs=on:gsem=on:nwc=1.1:sd=7:ss=axioms:st=1.2:sos=on:spl=off:sp=reverse_arity:updr=off_60"); // ISA 27 (5) - sched.push("dis+11_2:3_cond=on:gs=on:gsem=off:gsssp=full:lcm=reverse:nwc=1:sd=1:ss=axioms:st=1.5:sdd=off:sser=off:sfr=on:ssfp=1000:ssfq=2.0:ssnc=all_dependent:sp=reverse_arity:updr=off:uhcvi=on_60"); // ISA 28 (5) - sched.push("ins+11_10_cond=on:gs=on:igbrr=0.3:igpr=on:igrr=1/32:igrp=100:igrpq=1.1:igs=1010:igwr=on:lcm=reverse:nwc=1.3:sd=1:ss=axioms:st=1.2:sos=on:spl=off:sp=reverse_arity:urr=on:updr=off:dm=on:uhcvi=on_60"); // ISA 29 (5) - sched.push("dis+1002_3_cond=fast:ep=RSTC:fsr=off:gs=on:gsem=off:lwlo=on:nwc=1:sd=3:ss=axioms:st=1.2:sos=on:spl=off:sp=occurrence:uhcvi=on_60"); // ISA 30 (4) - sched.push("lrs+10_3_ep=RS:gs=on:gsem=off:nm=1024:nwc=1:stl=300:sd=2:ss=priority:sos=all:spl=off_60"); // HH4 1 (4899) - sched.push("dis+11_4_cond=on:gsp=input_only:gs=on:nm=0:nwc=1:sd=2:ss=axioms:st=1.5:sos=on:spl=off:urr=on:updr=off:uhcvi=on_60"); // HH4 2 (1018) - sched.push("lrs+11_2:3_br=off:cond=on:fde=none:gs=on:gsem=on:lwlo=on:nm=64:nwc=1:stl=300:sd=1:ss=axioms:st=2.0:sos=all:spl=off:sp=occurrence:urr=on:updr=off_60"); // HH4 3 (356) - sched.push("dis+1002_4_cond=fast:ep=RST:fde=unused:gs=on:gsaa=from_current:gsem=off:nm=0:nwc=1:sd=3:ss=axioms:st=1.2:sos=on:sac=on:sdd=large:ssfp=100000:ssfq=1.0:smm=sco:ssnc=none:updr=off:uhcvi=on_60"); // HH4 4 (230) - sched.push("lrs+1011_1_cond=fast:fsr=off:fde=unused:gsp=input_only:gs=on:gsem=off:gsssp=full:nm=0:nwc=10:stl=300:sd=1:ss=axioms:st=5.0:spl=off:sp=occurrence:urr=on_60"); // HH4 5 (179) - sched.push("ott+2_2:1_bd=off:bsr=unit_only:cond=on:gs=on:nwc=1:sd=3:ss=priority:st=1.5:sos=on:spl=off:sp=occurrence:updr=off_60"); // HH4 6 (138) - sched.push("lrs+11_5:4_bd=off:bsr=unit_only:br=off:fsr=off:fde=none:gsp=input_only:gs=on:gsem=on:nm=0:nwc=1:stl=300:sd=1:ss=axioms:sos=on:sdd=off:ssfp=40000:ssfq=1.4:smm=sco:urr=on:updr=off:uhcvi=on_60"); // HH4 7 (120) - sched.push("ott+1011_1_bd=preordered:cond=on:gsp=input_only:nm=64:nwc=1:sd=3:ss=priority:spl=off:sp=reverse_arity:urr=on_60"); // HH4 8 (90) - sched.push("ins+11_5_cond=fast:ep=RST:gs=on:gsem=on:igbrr=0.4:igpr=on:igrr=1/64:igrp=4000:igrpq=1.3:igwr=on:lcm=reverse:nwc=1:sd=2:ss=axioms:st=1.2:sos=on:spl=off:sp=occurrence:dm=on:uhcvi=on_60"); // HH4 9 (81) - sched.push("lrs+11_5_cond=on:ep=RST:fde=none:gsp=input_only:gs=on:gsem=off:nm=0:nwc=1:stl=300:sd=2:ss=axioms:st=3.0:sos=all:sac=on:sdd=large:ssfp=40000:ssfq=1.4:smm=off:ssnc=none:urr=ec_only:uhcvi=on_60"); // HH4 10 (70) - sched.push("lrs+1011_3_bd=off:bsr=on:cond=fast:fde=none:gs=on:gsssp=full:nm=0:nwc=1:stl=300:sd=2:ss=axioms:sos=all:spl=off:sp=occurrence_60"); // HH4 11 (58) - sched.push("lrs-4_5:4_cond=on:gs=on:gsem=on:gsssp=full:nm=64:nwc=1:stl=300:sd=2:ss=axioms:st=2.0:sos=on:sac=on:ssfp=100000:ssfq=1.1:smm=sco:ssnc=none:urr=on_60"); // HH4 12 (44) - sched.push("dis+1011_3:1_br=off:nm=0:nwc=5:sd=1:ss=axioms:sac=on:ssfp=40000:ssfq=1.4:smm=sco:ssnc=none:urr=on:uhcvi=on_60"); // HH4 13 (38) - sched.push("lrs+11_3:1_bd=off:bsr=unit_only:fsr=off:gs=on:gsaa=from_current:gsem=off:nm=64:nwc=1:stl=300:sd=2:ss=priority:sac=on:smm=sco:ssnc=none:sp=reverse_arity:updr=off:uhcvi=on_60"); // HH4 14 (36) - sched.push("dis+4_3_bd=off:cond=on:fde=unused:gs=on:gsaa=full_model:gsem=off:gsssp=full:nwc=1:sd=3:ss=axioms:st=3.0:sos=on:sdd=off:sfr=on:ssfp=10000:ssfq=1.0:smm=off:ssnc=none:urr=ec_only:updr=off:uhcvi=on_60"); // HH4 15 (32) - sched.push("dis+1010_5_cond=fast:nm=0:nwc=1:sd=1:ss=axioms:st=1.5:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // HH4 16 (32) - sched.push("lrs+11_4:1_bd=off:bsr=unit_only:br=off:fsr=off:fde=unused:gsp=input_only:gs=on:nm=0:nwc=1:stl=300:sd=1:ss=axioms:sos=on:spl=off:sp=reverse_arity:urr=on_60"); // HH4 17 (29) - sched.push("dis+1002_4_cond=on:gs=on:gsem=off:nwc=1:sd=2:ss=axioms:sos=on:spl=off:sp=reverse_arity:urr=ec_only:updr=off:uhcvi=on_60"); // HH4 18 (28) - sched.push("lrs+11_2:3_cond=on:fde=unused:gs=on:gsaa=full_model:nwc=4:stl=300:sd=2:ss=priority:st=5.0:sac=on:sdd=off:sfr=on:smm=off:ssnc=none:sp=occurrence:urr=on:updr=off:uhcvi=on_60"); // HH4 19 (24) - sched.push("ott-11_8:1_bsr=unit_only:cond=on:gs=on:gsem=off:gsssp=full:nwc=1.1:sd=2:ss=axioms:sos=on:sac=on:sscc=model:sdd=large:sser=off:ssfp=40000:ssfq=2.0:ssnc=none:sp=reverse_arity:urr=on_60"); // HH4 20 (23) - sched.push("lrs+1010_2:1_gs=on:lwlo=on:nm=0:nwc=3:stl=300:sd=4:ss=axioms:spl=off_60"); // HH4 21 (22) - sched.push("lrs+1010_4_bsr=unit_only:cond=fast:fsr=off:gs=on:gsaa=from_current:gsem=on:gsssp=full:nm=0:nwc=1:stl=300:sd=1:ss=axioms:st=1.5:sos=on:sdd=off:sser=off:sfr=on:ssfp=10000:ssfq=1.0:ssnc=none:sp=occurrence:urr=on_60"); // HH4 22 (20) - sched.push("dis+2_1_fsr=off:nwc=1:sd=2:ss=axioms:sos=on:spl=off:sp=reverse_arity:updr=off:uhcvi=on_60"); // HH4 23 (17) - sched.push("ott+2_2:1_cond=fast:fsr=off:fde=unused:gs=on:gsem=off:nm=0:nwc=1:sd=1:ss=axioms:st=5.0:sos=all:spl=off:sp=occurrence:updr=off:uhcvi=on_60"); // HH4 24 (17) - sched.push("lrs+1003_8:1_br=off:cond=on:fde=none:gs=on:gsem=off:nm=0:nwc=1:stl=300:sd=1:ss=axioms:sos=on:sdd=off:sfr=on:ssfp=40000:ssfq=1.1:smm=off:ssnc=none:sp=occurrence:urr=on_60"); // HH4 25 (14) - sched.push("ott-11_8:1_bsr=unit_only:lcm=predicate:nwc=1:sd=2:ss=axioms:st=1.2:sos=all:spl=off:sp=reverse_arity_60"); // MZR 1 (828) - sched.push("ott+1010_3:1_bs=unit_only:bsr=unit_only:br=off:ccuc=first:cond=fast:fde=unused:gs=on:gsem=on:nwc=1:sd=2:ss=axioms:sos=on:sac=on:ssac=none:sscc=on:sser=off:ssfp=1000:ssfq=2.0:ssnc=all_dependent:sp=reverse_arity:urr=on:updr=off_60"); // MZR 2 (112) - sched.push("ins+11_3_cond=fast:igbrr=0.7:igpr=on:igrr=1/32:igrp=700:igrpq=1.5:igs=1003:igwr=on:nwc=1:sd=1:ss=axioms:st=3.0:sos=all:spl=off:sp=occurrence:uhcvi=on_60"); // MZR 3 (81) - sched.push("lrs+1004_2_bd=off:ccuc=small_ones:gs=on:gsem=off:gsssp=full:lwlo=on:nm=0:nwc=1:stl=300:sd=4:ss=priority:st=5.0:sos=all:sac=on:sscc=on:sdd=off:sser=off:ssfp=100000:ssfq=1.2:ssnc=none:sp=occurrence:updr=off:uhcvi=on_60"); // MZR 4 (47) - sched.push("dis+10_5_bsr=unit_only:cond=on:ep=RS:fde=unused:nm=0:nwc=1:sd=1:ss=axioms:sos=all:spl=off_60"); // MZR 5 (37) - sched.push("lrs+11_5:1_br=off:cond=fast:fde=unused:gsp=input_only:gs=on:gsem=on:gsssp=full:lcm=predicate:nm=0:nwc=1:nicw=on:stl=300:sd=1:ss=axioms:st=1.2:sac=on:sdd=large:sfr=on:ssfp=40000:ssfq=1.4:smm=sco:ssnc=all:urr=on_60"); // MZR 6 (32) - sched.push("lrs+1011_8:1_cond=on:fde=none:gsp=input_only:lwlo=on:nwc=1:stl=300:sd=2:ss=axioms:sos=all:spl=off:sp=reverse_arity:urr=ec_only:updr=off:uhcvi=on_60"); // MZR 7 (22) - sched.push("lrs+11_3_br=off:cond=fast:gs=on:gsem=off:nwc=1:stl=300:sd=3:ss=priority:st=1.5:sos=all:sac=on:sfr=on:ssfp=1000:ssfq=2.0:smm=sco:ssnc=none:sp=occurrence:urr=on:uhcvi=on_60"); // MZR 8 (21) - sched.push("dis+10_2:1_cond=fast:ep=RST:fsr=off:fde=unused:gsp=input_only:gs=on:gsaa=full_model:gsem=off:nm=0:nwc=1:sd=1:ss=axioms:st=5.0:sos=on:sac=on:sdd=off:sfr=on:ssfp=100000:ssfq=1.4:smm=sco:ssnc=none:urr=on:updr=off:uhcvi=on_60"); // MZR 9 (19) - sched.push("lrs+1002_1_bsr=unit_only:nwc=1:stl=300:sd=1:ss=axioms:st=1.5:sos=all:spl=off:updr=off:uhcvi=on_60"); // MZR 10 (14) - sched.push("lrs+1_1_bs=on:bsr=on:br=off:cond=fast:fsr=off:gs=on:gsem=off:lwlo=on:nwc=3:stl=300:sd=3:ss=priority:sdd=large:sfr=on:ssfp=40000:ssfq=1.4:smm=off:ssnc=none:sp=occurrence:urr=on:updr=off_60"); // MZR 11 (11) - sched.push("lrs-2_1_cond=on:fde=unused:gs=on:gsaa=from_current:gsssp=full:lcm=predicate:nwc=1:stl=300:sd=4:ss=axioms:st=3.0:sos=on:sac=on:sfr=on:ssfp=10000:ssfq=1.1:ssnc=none:updr=off_60"); // MZR 12 (11) - sched.push("lrs+10_8:1_bsr=unit_only:br=off:cond=on:fsr=off:gsp=input_only:gs=on:gsaa=from_current:nm=0:nwc=1:stl=300:sd=2:ss=axioms:st=1.2:sos=on:sac=on:sdd=large:sfr=on:ssfp=1000:ssfq=1.1:smm=sco:ssnc=none:sp=reverse_arity:urr=on:updr=off:uhcvi=on_60"); // MZR 13 (10) - sched.push("dis+11_12_cond=fast:nwc=1:sd=1:ss=axioms:st=1.5:sos=on:spl=off:sp=reverse_arity:uhcvi=on_60"); // MZR 14 (8) - sched.push("dis+1010_3_bsr=unit_only:cond=fast:fde=none:nwc=1:sd=2:ss=axioms:st=1.5:sos=all:spl=off:sp=occurrence:uhcvi=on_60"); // MZR 15 (8) - sched.push("dis+1002_2:3_fde=none:gsp=input_only:nm=0:nwc=1:sd=3:ss=axioms:sos=on:sac=on:ssfp=100000:ssfq=1.0:smm=sco:ssnc=none:sp=occurrence:updr=off_60"); // MZR 16 (7) - sched.push("lrs+10_3:1_fde=unused:lcm=reverse:nwc=1:stl=300:sd=3:ss=priority:st=2.0:sos=all:spl=off:sp=occurrence:uhcvi=on_60"); // MZR 17 (6) - sched.push("lrs+10_2:3_bsr=unit_only:cond=on:fde=none:gs=on:nwc=1:stl=300:sd=2:ss=axioms:sos=on:spl=off:sp=reverse_arity_60"); // MZR 18 (6) - sched.push("dis+1004_3:1_bsr=unit_only:ep=R:fde=unused:gs=on:gsssp=full:nm=0:nwc=1:sos=all:sac=on:sfr=on:ssfp=10000:ssfq=2.0:ssnc=all:sp=reverse_arity:urr=on:updr=off_60"); // MZR 19 (5) - sched.push("ott+4_5:1_br=off:cond=fast:fsr=off:nwc=1.3:spl=off:sp=occurrence:urr=on:uhcvi=on_60"); // MZR 20 (5) - sched.push("dis+1010_1_cond=fast:fsr=off:nwc=1.3:sd=2:ss=axioms:st=1.5:sos=on:sscc=model:sdd=off:ssfp=4000:ssfq=2.0:uhcvi=on_60"); // MZR 21 (5) - sched.push("lrs+11_2_bd=off:bsr=unit_only:cond=on:lcm=predicate:lwlo=on:nm=64:nwc=1.1:stl=300:sd=1:ss=axioms:st=2.0:sos=all:spl=off_60"); // MZR 22 (5) - sched.push("lrs+10_4:1_bd=off:cond=fast:fde=unused:lcm=reverse:nm=0:nwc=1.2:stl=300:sd=2:ss=axioms:sos=all:spl=off_60"); // MZR 23 (5) - sched.push("dis+10_5_ep=RST:fsr=off:gs=on:gsssp=full:lwlo=on:nm=0:nwc=1:sd=4:ss=axioms:sos=on:sfr=on:ssfp=40000:ssfq=1.1:smm=off:ssnc=none:uhcvi=on_60"); // MZR 24 (4) - sched.push("dis+1002_3_ep=RST:fde=unused:gs=on:gsaa=full_model:gsem=off:nwc=1:sd=1:ss=axioms:st=2.0:sos=on:ssfp=100000:ssfq=1.1:ssnc=none:sp=occurrence:uhcvi=on_60"); // MZR 25 (4) -} // fillSchedule - -/** - * This function solves a single problem. It makes the following steps: - *
  1. find the main and the fallback schedules depending on the problem - * properties
    2. - *
  2. run the main schedule using runSchedule()
    3. - *
  3. if the proof is not found, checks if all the remaining time - * was used: if not, it runs the fallback strategy using - * runSchedule() with the updated time limit
- * Once the problem is proved, the runSchedule() function does not return - * and the process terminates. - * - * If a slice contains sine_selection value different from off, theory axioms - * will be selected using SInE from the common axioms included in the batch file - * (all problem axioms, including the included ones, will be used as a base - * for this selection). - * - * If the sine_selection is off, all the common axioms will be just added to the - * problem axioms. All this is done in the @b runSlice(Options&) function. - * @param terminationTime the time in milliseconds since the prover starts when - * the strategy should terminate - * @param timeLimit in milliseconds - * @param property - * @param quick - * @param stopOnProof - * @author Krystof Hoder - * @since 04/06/2013 flight Frankfurt-Vienna, updated for CASC-J6 - * @author Andrei Voronkov - */ -void CLTBProblemLearning::performStrategy(int terminationTime,int timeLimit, Shell::Property* property,Schedule& quick, bool stopOnProof) -{ - cout << "% Hi Geoff, go and have some cold beer while I am trying to solve this very hard problem!\n"; - - Schedule fallback; - //CASC::CASCMode::getSchedules(*property,fallback,fallback); - - StrategySet usedSlices; - if (runSchedule(quick,usedSlices,false,terminationTime,stopOnProof)) { - return; - } - if (env.timer->elapsedMilliseconds() >= terminationTime) { - return; - } - //runSchedule(fallback,usedSlices,true,terminationTime,stopOnProof); -} // CLTBProblemLearning::performStrategy - -/** - * This function solves a single problem. It parses the problem, spawns a - * writer process for output and creates a pipe to communicate with it. - * Then it calls performStrategy(terminationTime) that performs the - * actual proof search. - * @param terminationTime the time in milliseconds since the prover start - * @param timeLimit time limit in milliseconds - * @param strats - * @param stopOnProof - * @since 04/06/2013 flight Manchester-Frankfurt - * @author Andrei Voronkov - */ -void CLTBProblemLearning::searchForProof(int terminationTime,int timeLimit, Schedule& strats, bool stopOnProof) -{ - System::registerForSIGHUPOnParentDeath(); - - env.options->setInputFile(problemFile); - - // this local scope will delete a potentially large parser - { - TIME_TRACE(TimeTrace::PARSING); - env.statistics->phase=Statistics::PARSING; - - ifstream inp(problemFile.c_str()); - if (inp.fail()) { - USER_ERROR("Cannot open problem file: " + problemFile); - } - Parse::TPTP parser(inp); - List::Iterator iit(parent->_theoryIncludes); - while (iit.hasNext()) { - parser.addForbiddenInclude(iit.next()); - } - parser.parse(); - UnitList* probUnits = parser.units(); - UIHelper::setConjecturePresence(parser.containsConjecture()); - prb.addUnits(probUnits); - - - - } - - Shell::Property* property = prb.getProperty(); - if (property->atoms()<=1000000) { - TIME_TRACE(TimeTrace::PREPROCESSING); - env.statistics->phase=Statistics::NORMALIZATION; - Normalisation norm; - norm.normalise(prb); - } - - env.statistics->phase=Statistics::UNKNOWN_PHASE; - - // now all the cpu usage will be in children, we'll just be waiting for them - Timer::setLimitEnforcement(false); - - //UIHelper::szsOutput=true; - - performStrategy(terminationTime,timeLimit,property,strats,stopOnProof); - exitOnNoSuccess(); - ASSERTION_VIOLATION; // the exitOnNoSuccess() function should never return -} // CLTBProblemLearning::perform - -/** - * This function exits the problem master process if the problem - * was not solved - * - * The unsuccessful problem master process does not have to - * necessarily call this function to exit. - */ -void CLTBProblemLearning::exitOnNoSuccess() -{ - env.beginOutput(); - CLTBModeLearning::lineOutput() << "Proof not found in time " << Timer::msToSecondsString(env.timer->elapsedMilliseconds()) << endl; - if (env.remainingTime()/100>0) { - CLTBModeLearning::lineOutput() << "SZS status GaveUp for " << env.options->problemName() << endl; - } - else { - //From time to time we may also be terminating in the timeLimitReached() - //function in Lib/Timer.cpp in case the time runs out. We, however, output - //the same string there as well. - CLTBModeLearning::lineOutput() << "SZS status Timeout for " << env.options->problemName() << endl; - } - env.endOutput(); - - CLTBModeLearning::coutLineOutput() << "problem proof search terminated (fail)" << endl << flush; - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code -} // CLTBProblemLearning::exitOnNoSuccess - -static unsigned milliToDeci(unsigned timeInMiliseconds) { - return timeInMiliseconds/100; -} - -/** - * Run a schedule. Terminate the process with 0 exit status - * if a proof was found, otherwise return false. This function available cores: - * If the total number of cores @b n is 8 or more, then @b n-2, otherwise @b n-1. - * It spawns processes by calling runSlice() - * @author Andrei Voronkov - * @since 04/06/2013 flight Frankfurt-Vienna, updated for CASC-J6 - */ -bool CLTBProblemLearning::runSchedule(Schedule& schedule,StrategySet& used,bool fallback,int terminationTime, bool stopOnProof) -{ - // compute the number of parallel processes depending on the - // number of available cores - int parallelProcesses; - unsigned coreNumber = System::getNumberOfCores(); - if (coreNumber <= 1) { - parallelProcesses = 1; - } - else if (coreNumber>=8) { - parallelProcesses = coreNumber-2; - } - else { - parallelProcesses = coreNumber; - } - - int processesLeft = parallelProcesses; - Schedule::BottomFirstIterator it(schedule); - - int slices = schedule.length(); - while (it.hasNext()) { - while (processesLeft) { - CLTBModeLearning::coutLineOutput() << "Slices left: " << slices-- << endl; - CLTBModeLearning::coutLineOutput() << "Processes available: " << processesLeft << endl << flush; - ASS_G(processesLeft,0); - - int elapsedTime = env.timer->elapsedMilliseconds(); - if (elapsedTime >= terminationTime) { - // time limit reached - goto finish_up; - } - - vstring sliceCode = it.next(); - vstring chopped; - - // slice time in milliseconds - int sliceTime = SLOWNESS * getSliceTime(sliceCode,chopped); - if (used.contains(chopped)) { - // this slice was already used - continue; - } - used.insert(chopped); - int remainingTime = terminationTime - elapsedTime; - if (sliceTime > remainingTime) { - sliceTime = remainingTime; - } - - ASS_GE(sliceTime,0); - if (milliToDeci((unsigned)sliceTime) == 0) { - // can be still zero, due to rounding - // and zero time limit means no time limit -> the child might never return! - - // time limit reached - goto finish_up; - } - - pid_t childId=Multiprocessing::instance()->fork(); - ASS_NEQ(childId,-1); - if (!childId) { - //we're in a proving child - try { - runSlice(sliceCode,sliceTime,stopOnProof); //start proving - } catch (Exception& exc) { - cerr << "% Exception at run slice level" << endl; - exc.cry(cerr); - System::terminateImmediately(1); //we didn't find the proof, so we return nonzero status code - } - ASSERTION_VIOLATION; //the runSlice function should never return - } - Timer::syncClock(); - ASS(childIds.insert(childId)); - CLTBModeLearning::coutLineOutput() << "slice pid "<< childId << " slice: " << sliceCode - << " time: " << (sliceTime/100)/10.0 << endl << flush; - processesLeft--; - if (!it.hasNext()) { - break; - } - } - - CLTBModeLearning::coutLineOutput() << "No processes available: " << endl << flush; - if (processesLeft==0) { - waitForChildAndExitWhenProofFound(stopOnProof); - // proof search failed - processesLeft++; - } - } - - finish_up: - - while (parallelProcesses!=processesLeft) { - ASS_L(processesLeft, parallelProcesses); - waitForChildAndExitWhenProofFound(stopOnProof); - // proof search failed - processesLeft++; - Timer::syncClock(); - } - return false; -} // CLTBProblemLearning::runSchedule - -/** - * Wait for termination of a child and terminate the process with a zero status - * if a proof was found. If the child didn't find the proof, just return. - */ -void CLTBProblemLearning::waitForChildAndExitWhenProofFound(bool stopOnProof) -{ - ASS(!childIds.isEmpty()); - - int resValue; - pid_t finishedChild = Multiprocessing::instance()->waitForChildTermination(resValue); -#if VDEBUG - ALWAYS(childIds.remove(finishedChild)); -#endif - if (!resValue) { - // we have found the proof. It has been already written down by the writter child, - // so we can just terminate - CLTBModeLearning::coutLineOutput() << "terminated slice pid " << finishedChild << " (success)" << endl << flush; - if(stopOnProof){ System::terminateImmediately(0);} - } - // proof not found - CLTBModeLearning::coutLineOutput() << "terminated slice pid " << finishedChild << " (fail)" << endl << flush; -} // waitForChildAndExitWhenProofFound - -ofstream* CLTBProblemLearning::writerFileStream = 0; - -void CLTBProblemLearning::terminatingSignalHandler(int sigNum) -{ - try { - if (writerFileStream) { - writerFileStream->close(); - } - } catch (Lib::SystemFailException& ex) { - cerr << "Process " << getpid() << " received SystemFailException in terminatingSignalHandler" << endl; - ex.cry(cerr); - cerr << " and will now die" << endl; - } - System::terminateImmediately(0); -} - -/** - * Run a slice given by its code using the specified time limit. - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -void CLTBProblemLearning::runSlice(vstring sliceCode, unsigned timeLimitInMilliseconds,bool printProof) -{ - if(!printProof){ - // We're learning, don't run again if already run - ProbRecord* rec; - if(parent->probRecords.find(env.options->problemName(),rec)){ - if(rec->suc.contains(sliceCode) || rec->fail.contains(sliceCode)){ - CLTBModeLearning::coutLineOutput() << " GaveUp as tried before (in learning)" << endl; - exit(1); // GaveUp - } - rec->fail.insert(sliceCode); // insert this here in child in case the same slice is in the schedule multiple times - } - } - - Options opt = *env.options; - opt.readFromEncodedOptions(sliceCode); - opt.setTimeLimitInDeciseconds(milliToDeci(timeLimitInMilliseconds)); - int stl = opt.simulatedTimeLimit(); - if (stl) { - opt.setSimulatedTimeLimit(int(stl * SLOWNESS)); - } - runSlice(opt,printProof); -} // runSlice - -/** - * Run a slice given by its options - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -void CLTBProblemLearning::runSlice(Options& strategyOpt, bool printProof) -{ - System::registerForSIGHUPOnParentDeath(); - //UIHelper::cascModeChild=true; - //UIHelper::cascMode=true; - - int resultValue=1; - env.timer->reset(); - env.timer->start(); - Timer::setLimitEnforcement(true); - - Options opt = strategyOpt; - //we have already performed the normalization - opt.setNormalize(false); - opt.setForcedOptionValues(); - opt.checkGlobalOptionConstraints(); - opt.setProblemName(problemFile); - *env.options = opt; //just temporarily until we get rid of dependencies on env.options in solving - -// if (env.options->sineSelection()!=Options::SS_OFF) { -// //add selected axioms from the theory -// parent->theorySelector.perform(probUnits); -// -// env.options->setSineSelection(Options::SS_OFF); -// env.options->forceIncompleteness(); -// } -// else { -// //if there wasn't any sine selection, just put in all theory axioms -// probUnits=UnitList::concat(probUnits, parent->theoryAxioms); -// } - - env.beginOutput(); - CLTBModeLearning::lineOutput() << opt.testId() << " on " << opt.problemName() << endl; - env.endOutput(); - - ProvingHelper::runVampire(prb, opt); - - //set return value to zero if we were successful - if (env.statistics->terminationReason == Statistics::REFUTATION) { - resultValue=0; - } - CLTBModeLearning::lineOutput() << "result " << resultValue << endl; - - System::ignoreSIGHUP(); // don't interrupt now, we need to finish printing the proof ! - - if (!resultValue) { // write the proof to a file - - if(printProof){ - CLTBModeLearning::lineOutput() << "printing" << endl; - ScopedSemaphoreLocker locker(_syncSemaphore); - locker.lock(); - ofstream out(outFile.c_str()); - UIHelper::outputResult(out); - out.close(); - } - - } else { // write other result to output - env.beginOutput(); - UIHelper::outputResult(env.out()); - env.endOutput(); - } - - CLTBModeLearning::lineOutput() << "sending feedback" << endl; - { - ScopedSemaphoreLocker locker(_syncSemaphore); - locker.lock(); - ScopedSyncPipe pipe = ScopedSyncPipe(parent->strategies); - ostream& pout = pipe.pipe->out(); - pout << opt.testId() << endl; - CLTBModeLearning::lineOutput() << "sent " << opt.testId() << endl; - pout << opt.problemName() << endl; - CLTBModeLearning::lineOutput() << "sent " << opt.problemName() << endl; - pout << resultValue << endl; - CLTBModeLearning::lineOutput() << "sent " << resultValue << endl; - } - parent->stratSem.incp(0); - CLTBModeLearning::lineOutput() << "sent" << endl; - - exit(resultValue); -} // CLTBProblemLearning::runSlice - -/** - * Return the intended slice time in milliseconds and assign the slice - * vstring with chopped time limit to @b chopped. - * @since 04/06/2013 flight Frankfurt-Vienna - * @author Andrei Voronkov - */ -unsigned CLTBProblemLearning::getSliceTime(vstring sliceCode,vstring& chopped) -{ - unsigned pos = sliceCode.find_last_of('_'); - vstring sliceTimeStr = sliceCode.substr(pos+1); - chopped.assign(sliceCode.substr(0,pos)); - unsigned sliceTime; - ALWAYS(Int::stringToUnsignedInt(sliceTimeStr,sliceTime)); - ASS_G(sliceTime,0); //strategies with zero time don't make sense - - unsigned time = sliceTime + 1; - if (time < 10) { - time++; - } - // convert deciseconds to milliseconds - return time * 100; -} // getSliceTime - -/** - * Start line output by writing the TPTP comment sign and the current - * elapsed time in milliseconds to env.out(). Returns env.out() - * @since 05/06/2013 Vienna - * @author Andrei Voronkov - */ -ostream& CLTBModeLearning::lineOutput() -{ - return env.out() << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") "; -} // CLTBModeLearning::lineOutput - -/** - * Start line output by writing the TPTP comment sign and the current - * elapsed time in milliseconds to cout. Returns cout - * @since 05/06/2013 Vienna - * @author Andrei Voronkov - */ -ostream& CLTBModeLearning::coutLineOutput() -{ - return cout << "% (" << getpid() << ',' << (env.timer->elapsedMilliseconds()/100)/10.0 << ") "; -} // CLTBModeLearning::coutLineOutput - diff --git a/CASC/CLTBModeLearning.hpp b/CASC/CLTBModeLearning.hpp deleted file mode 100644 index fe716c3f62..0000000000 --- a/CASC/CLTBModeLearning.hpp +++ /dev/null @@ -1,192 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file CLTBModeLearning.hpp - * Defines class CLTBModeLearning. - */ - -#ifndef __CLTBModeLearning__ -#define __CLTBModeLearning__ - -#include - -#include "Forwards.hpp" - -#include "Lib/DHSet.hpp" -#include "Lib/Portability.hpp" -#include "Lib/ScopedPtr.hpp" -#include "Lib/Stack.hpp" -#include "Lib/Set.hpp" - -#include "Lib/VString.hpp" - -#include "Lib/Sys/SyncPipe.hpp" - -#include "Kernel/Problem.hpp" - -#include "Shell/Property.hpp" -#include "Shell/SineUtils.hpp" - -namespace CASC { - -using namespace Lib; -using namespace Kernel; - -class CLTBProblemLearning; - - struct ProbRecord{ - Set suc; - Set fail; - float avg; - }; - -class CLTBModeLearning -{ -public: - CLTBModeLearning() : stratSem(1) { - strategies = new SyncPipe();; - stratSem.set(0,0); - } - - static void perform(); -private: - void solveBatch(std::istream& batchFile, bool first, vstring inputDirectory); - int readInput(std::istream& batchFile, bool first); - static std::ostream& lineOutput(); - static std::ostream& coutLineOutput(); - void loadIncludes(); - void doTraining(int time,bool startup); - - typedef List StringList; - typedef Stack StringStack; - typedef std::pair StringPair; - typedef Stack StringPairStack; - typedef Stack Schedule; - static void fillSchedule(Schedule& strats); - - vstring _trainingDirectory; - /** per-problem time limit, in milliseconds */ - int _problemTimeLimit; - /** true if question answers should be given */ - bool _questionAnswering; - /** total time used by batches before this one, in milliseconds */ - int _timeUsedByPreviousBatches; - - /** files to be included */ - StringList* _theoryIncludes; - - /** The first vstring in the pair is problem file, the second - * one is output file. The problemFiles[0] is the first - * problem that should be attempted. */ - StringPairStack _problemFiles; - - ScopedPtr _baseProblem; - - Semaphore stratSem; - SyncPipe* strategies; - - static DHMap probRecords; - static DHMap*> stratWins; - - Stack problems; - Stack new_problems; - Schedule strats; - - friend class CLTBProblemLearning; -}; - - -class CLTBProblemLearning -{ -public: - CLTBProblemLearning(CLTBModeLearning* parent, vstring problemFile, vstring outFile); - - typedef Set StrategySet; - typedef Stack Schedule; - - [[noreturn]] void searchForProof(int terminationTime,int timeLimit,Schedule& strats,bool stopOnProof); -private: - bool runSchedule(Schedule&,StrategySet& remember,bool fallback,int terminationTime, bool stopOnProof); - unsigned getSliceTime(vstring sliceCode,vstring& chopped); - - void performStrategy(int terminationTime,int timeLimit, Shell::Property* property, Schedule& quick, bool stopOnProof); - void waitForChildAndExitWhenProofFound(bool stopOnProof); - [[noreturn]] void exitOnNoSuccess(); - - static std::ofstream* writerFileStream; - [[noreturn]] static void terminatingSignalHandler(int sigNum); - [[noreturn]] void runSlice(vstring slice, unsigned milliseconds,bool printProof); - [[noreturn]] void runSlice(Options& strategyOpt, bool printProof); - - static vstring problemFinishedString; - -#if VDEBUG - DHSet childIds; -#endif - - CLTBModeLearning* parent; - vstring problemFile; - vstring outFile; - - /** - * Problem that is being solved. - * - * This is just a reference to parent's @c baseProblem object into which we - * add problem-specific axioms in the @c searchForProof() function. We can do this, - * because in the current process this child object is the only one that - * will be using the problem object. - */ - Problem& prb; - - Semaphore _syncSemaphore; // semaphore for synchronizing writing if the solution - - /** - * Assumes semaphore object with 1 semaphores (at index 0). - * Locks on demand (once) and releases the lock on destruction. - */ - struct ScopedSemaphoreLocker { // - Semaphore& _sem; - bool locked; - ScopedSemaphoreLocker(Semaphore& sem) : _sem(sem), locked(false) {} - - void lock() { - if (!locked) { - _sem.dec(0); - locked = true; - } - } - - ~ScopedSemaphoreLocker() { - if (locked) { - _sem.inc(0); - } - } - }; - - struct ScopedSyncPipe { - SyncPipe* pipe; - // Probably dangerous to acquire in constructor - ScopedSyncPipe(SyncPipe* p) : pipe(p) - { - std::cout << "getting pipe" << std::endl; - pipe->acquireWrite(); - std::cout << "got pipe" << std::endl; - } - ~ScopedSyncPipe(){ - std::cout << "release pipe" << std::endl; - pipe->releaseWrite(); - } - }; - -}; - -} - -#endif // __CLTBModeLearning__ diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp index edb1a932fb..a7575db6a6 100644 --- a/CASC/PortfolioMode.cpp +++ b/CASC/PortfolioMode.cpp @@ -48,6 +48,7 @@ using namespace std; using namespace Lib; using namespace CASC; +using Lib::Sys::Multiprocessing; PortfolioMode::PortfolioMode(Problem* problem) : _prb(problem), _slowness(env.options->slowness()), _syncSemaphore(2) { unsigned cores = System::getNumberOfCores(); diff --git a/CASC/PortfolioMode.hpp b/CASC/PortfolioMode.hpp index 41086c8989..01113992a7 100644 --- a/CASC/PortfolioMode.hpp +++ b/CASC/PortfolioMode.hpp @@ -74,7 +74,7 @@ class PortfolioMode { ScopedPtr _prb; float _slowness; - Semaphore _syncSemaphore; // semaphore for synchronizing proof printing + Sys::Semaphore _syncSemaphore; // semaphore for synchronizing proof printing }; } diff --git a/CMakeLists.txt b/CMakeLists.txt index 8dc9133eb4..31a7b82a2d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -157,8 +157,6 @@ set(VAMPIRE_LIB_SOURCES Lib/Environment.hpp Lib/Event.hpp Lib/Exception.hpp - Lib/fdstream.hpp - Lib/FreshnessGuard.hpp Lib/Hash.hpp Lib/Int.hpp Lib/IntNameTable.hpp @@ -202,10 +200,8 @@ source_group(lib_source_files FILES ${VAMPIRE_LIB_SOURCES}) set(VAMPIRE_LIB_SYS_SOURCES Lib/Sys/Multiprocessing.cpp Lib/Sys/Semaphore.cpp - Lib/Sys/SyncPipe.cpp Lib/Sys/Multiprocessing.hpp Lib/Sys/Semaphore.hpp - Lib/Sys/SyncPipe.hpp ) source_group(lib_sys_source_files FILES ${VAMPIRE_LIB_SYS_SOURCES}) @@ -686,12 +682,8 @@ source_group(smt_comp_source_files FILES ${VAMPIRE_SMTCOMP_SOURCES}) set(VAMPIRE_CASC_SOURCES CASC/PortfolioMode.cpp CASC/Schedules.cpp - CASC/CLTBMode.cpp - CASC/CLTBModeLearning.cpp CASC/PortfolioMode.hpp CASC/Schedules.hpp - CASC/CLTBMode.hpp - CASC/CLTBModeLearning.hpp ) source_group(casc_source_files FILES ${VAMPIRE_CASC_SOURCES}) diff --git a/Lib/Environment.cpp b/Lib/Environment.cpp index 4fd83eb802..bbbc49acaa 100644 --- a/Lib/Environment.cpp +++ b/Lib/Environment.cpp @@ -47,8 +47,6 @@ Environment::Environment() predicateSineLevels(nullptr), colorUsed(false), _outputDepth(0), - _priorityOutput(0), - _pipe(0), _problem(0) { options = new Options; @@ -133,9 +131,6 @@ void Environment::beginOutput() ASS_GE(_outputDepth,0); _outputDepth++; - if(_outputDepth==1 && _pipe) { - _pipe->acquireWrite(); - } } /** @@ -147,13 +142,7 @@ void Environment::endOutput() _outputDepth--; if(_outputDepth==0) { - if(_pipe) { - cout.flush(); - _pipe->releaseWrite(); - } - else { - cout.flush(); - } + cout.flush(); } } @@ -174,36 +163,7 @@ bool Environment::haveOutput() ostream& Environment::out() { ASS(_outputDepth); - - if(_priorityOutput) { - return *_priorityOutput; - } - else if(_pipe) { - return _pipe->out(); - } - else { - return cout; - } -} - -/** - * Direct @b env.out() into @b pipe or to @b cout if @b pipe is zero - * - * This function cannot be called when an output is in progress. - */ -void Environment::setPipeOutput(SyncPipe* pipe) -{ - ASS(!haveOutput()); - - _pipe=pipe; -} - -void Environment::setPriorityOutput(ostream* stm) -{ - ASS(!_priorityOutput || !stm); - - _priorityOutput=stm; - + return cout; } // global environment object, constructed before main() and used everywhere diff --git a/Lib/Environment.hpp b/Lib/Environment.hpp index 68c5dad4d2..64d9749bc0 100644 --- a/Lib/Environment.hpp +++ b/Lib/Environment.hpp @@ -26,12 +26,6 @@ namespace Lib { -namespace Sys { - class SyncPipe; -} - -using namespace Sys; - /** * Class Environment. * Implements environment used by the top-level run procedures. @@ -66,12 +60,6 @@ class Environment void endOutput(); std::ostream& out(); - void setPipeOutput(SyncPipe* pipe); - SyncPipe* getOutputPipe() { return _pipe; } - - void setPriorityOutput(std::ostream* stm); - std::ostream* getPriorityOutput() { return _priorityOutput; } - bool timeLimitReached() const; template @@ -104,10 +92,6 @@ class Environment private: int _outputDepth; - /** if non-zero, all output will go here */ - std::ostream* _priorityOutput; - SyncPipe* _pipe; - Kernel::Problem* _problem; }; // class Environment diff --git a/Lib/FreshnessGuard.hpp b/Lib/FreshnessGuard.hpp deleted file mode 100644 index cc3a84bbf8..0000000000 --- a/Lib/FreshnessGuard.hpp +++ /dev/null @@ -1,57 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file FreshnessGuard.hpp - * Defines class FreshnessGuard. - */ - -#ifndef __FreshnessGuard__ -#define __FreshnessGuard__ - -#include "Forwards.hpp" - -#include "Debug/Assertion.hpp" - -#include "Exception.hpp" - -namespace Lib { - -/** - * Some objects can be used only once. This auxiliary object - * can be used to enforce this constraint. - */ -class FreshnessGuard { -public: - FreshnessGuard() : _fresh(true) {} - - bool isFresh() const { return _fresh; } - /** - * This function can be called only when the object is fresh. - * It makes the object non-fresh. - */ - void use() { - ASS(isFresh()); - if(!isFresh()) { - INVALID_OPERATION("using non-fresh object"); - } - _fresh = false; - } - - void refresh() { - _fresh = true; - } - -private: - bool _fresh; -}; - -} - -#endif // __FreshnessGuard__ diff --git a/Lib/Sys/SyncPipe.cpp b/Lib/Sys/SyncPipe.cpp deleted file mode 100644 index ef85b7d06e..0000000000 --- a/Lib/Sys/SyncPipe.cpp +++ /dev/null @@ -1,249 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file SyncPipe.cpp - * Implements class SyncPipe. - */ - -#include "Lib/Portability.hpp" - -#include -#include - -#include "Lib/Environment.hpp" -#include "Lib/Exception.hpp" -#include "Lib/fdstream.hpp" -#include "Lib/List.hpp" -#include "Lib/System.hpp" - -#include "Multiprocessing.hpp" - -#include "SyncPipe.hpp" - -namespace Lib -{ -namespace Sys -{ - -SyncPipe::PipeList* SyncPipe::s_instances = 0; - -SyncPipe::SyncPipe() -: _isReading(false), _isWriting(false), _syncSemaphore(3) -{ - ensureEventHandlersInstalled(); - - int fd[2]; - errno=0; - int res=pipe(fd); - if(res==-1) { - SYSTEM_FAIL("Pipe creation.", errno); - } - - _readDescriptor=fd[0]; - _writeDescriptor=fd[1]; - - _istream=new fdstream(_readDescriptor); - _ostream=new fdstream(_writeDescriptor); - - _istream->rdbuf()->pubsetbuf(0,0); - - //add the privileges into the semaphore - _syncSemaphore.set(0,1); - _syncSemaphore.set(1,1); - //set the read-ahead byte to empty values - _syncSemaphore.set(2,256); - - PipeList::push(this, s_instances); -} - -SyncPipe::~SyncPipe() -{ - releasePrivileges(); - ASS(PipeList::member(this, s_instances)); - s_instances = PipeList::remove(this, s_instances); - - if(canRead()) { - neverRead(); - } - if(canWrite()) { - neverWrite(); - } -} - -/** - * Acquire a privilege for this process to read from the pipe - */ -void SyncPipe::acquireRead() -{ - ASS(canRead()); - ASS(!isReading()); - ASS(!isWriting()); //it does not make sense if one process would both reads and writes into a pipe - - _syncSemaphore.dec(0); - - //restore the preread character - int preRead=_syncSemaphore.get(2); - if(preRead==256) { - preRead=-1; - } - ASS_LE(preRead,255); - _istream->setPreReadChar(preRead); - - _isReading=true; -} - -/** - * Give up the privilege of this process to read from the pipe - */ -void SyncPipe::releaseRead() -{ - ASS(isReading()); - - _isReading=false; - - int preRead=_istream->getPreReadChar(); - if(preRead==-1) { - preRead=256; - } - ASS_GE(preRead,0); - ASS_LE(preRead,256); - _syncSemaphore.set(2,preRead); - - _syncSemaphore.inc(0); -} - -/** - * Release the reading end of the pipe from this object. This - * means that it will not be possible to call @b acquireRead on it. - */ -void SyncPipe::neverRead() -{ - ASS(canRead()); //@b neverRead() can only be called once - ASS(!isReading()); - - int res=close(_readDescriptor); - if(res==-1) { - SYSTEM_FAIL("Closing read descriptor of a pipe.", errno); - } - ASS_EQ(res,0); - delete _istream; - _istream=0; -} - - -/** - * Acquire a privilege for this process to write into the pipe - */ -void SyncPipe::acquireWrite() -{ - ASS(canWrite()); - ASS(!isWriting()); - ASS(!isReading()); //it does not make sense if one process would both reads and writes into a pipe - - _syncSemaphore.dec(1); - _isWriting=true; -} - -/** - * Give up the privilege of this process to write into the pipe - */ -void SyncPipe::releaseWrite() -{ - ASS(isWriting()); - - _ostream->flush(); - _isWriting=false; - _syncSemaphore.inc(1); -} - -/** - * Release the writing end of the pipe from this object. This - * means that it will not be possible to call @b acquireWrite on it. - */ -void SyncPipe::neverWrite() -{ - ASS(canWrite()); //@b neverWrite() can only be called once - ASS(!isWriting()); - ASS(env.getOutputPipe()!=this); //we cannot forbid writing to pipe that we use as output - - int res=close(_writeDescriptor); - if(res==-1) { - SYSTEM_FAIL("Closing write descriptor of a pipe.", errno); - } - ASS_EQ(res,0); - - delete _ostream; - _ostream=0; -} -/** - * Give up all the privileges of this object - */ -void SyncPipe::releasePrivileges() -{ - ASS(_syncSemaphore.hasSemaphore()); - - if(isReading()) { - releaseRead(); - } - if(isWriting()) { - releaseWrite(); - } -} - -/** - * Give up privileges of all the object in this process - * - * This function is called in the beginning of a forked child process. - */ -void SyncPipe::postForkChildHadler() -{ - PipeList::Iterator pit(s_instances); - while(pit.hasNext()) { - SyncPipe* p=pit.next(); - p->releasePrivileges(); - } -} - -/** - * Give up privileges of all the object in this process and destroy - * the list of all pipe objects - * - * This function is called before the process termination. - */ -void SyncPipe::terminationHadler() -{ - PipeList* listIter=s_instances; - while(listIter) { - if(listIter->head()) { - SyncPipe* p=listIter->head(); - p->releasePrivileges(); - listIter->setHead(0); - } - listIter=listIter->tail(); - } -} - -void SyncPipe::ensureEventHandlersInstalled() -{ - static bool installed=false; - if(installed) { - return; - } - Multiprocessing::instance()->registerForkHandlers(0,0,postForkChildHadler); - //this termination handler must be called before the termination handler - //of the Semaphore class - System::addTerminationHandler(terminationHadler,0); - installed=true; -} - - -} -} - diff --git a/Lib/Sys/SyncPipe.hpp b/Lib/Sys/SyncPipe.hpp deleted file mode 100644 index 3d0fdb011c..0000000000 --- a/Lib/Sys/SyncPipe.hpp +++ /dev/null @@ -1,122 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file SyncPipe.hpp - * Defines class SyncPipe. - */ - -#ifndef __SyncPipe__ -#define __SyncPipe__ - -#include - -#include "Forwards.hpp" - -#include "Lib/fdstream.hpp" -#include "Lib/Exception.hpp" -#include "Lib/Portability.hpp" - -#include "Semaphore.hpp" - -namespace Lib { -namespace Sys { - -class SyncPipe { -public: - SyncPipe(); - ~SyncPipe(); - - /** Return true iff the current object has acquired the read privilege */ - bool isReading() const { return _isReading; } - /** Return true iff the current object can acquire read privileges */ - bool canRead() const { return _istream; } - - void acquireRead(); - void releaseRead(); - void neverRead(); - - /** Return true iff the current object has acquired the write privilege */ - bool isWriting() const { return _isWriting; } - /** Return true iff the current object can acquire write privileges */ - bool canWrite() const { return _ostream; } - - void acquireWrite(); - void releaseWrite(); - void neverWrite(); - - void releasePrivileges(); - - /** - * If we have read privileges, return reference to an std::istream object - */ - std::istream& in() - { - ASS(_istream); - ASS(isReading()); - if(!isReading()) { - INVALID_OPERATION("Unallowed read from pipe."); - } - return *_istream; - } - - /** - * If we have write privileges, return reference to an std::ostream object - */ - std::ostream& out() - { - ASS(_ostream); - ASS(isWriting()); - if(!isWriting()) { - INVALID_OPERATION("Unallowed write to pipe."); - } - return *_ostream; - } - -private: - SyncPipe(const SyncPipe&); //private and undefined - const SyncPipe& operator=(const SyncPipe&); //private and undefined - - /** Contains pointer to input stream reading from the pipe, or 0 if - * @b neverRead has been called */ - fdstream *_istream; - /** Contains pointer to output stream writing to the pipe, or 0 if - * @b neverWrite has been called */ - fdstream *_ostream; - - int _readDescriptor; - int _writeDescriptor; - bool _isReading; - bool _isWriting; - - /** - * Semaphore object with three semaphores. The first (number 0) - * controls reading, the second one controls writing, and the third - * one contains the value of the read-ahead byte from the pipe, or - * 256 if there is not any. - * - * When the semaphore value is one, anyone can acquire a privilege, - * when it is zero, the acquire function will wait until it - * increases. - */ - Semaphore _syncSemaphore; - - static void postForkChildHadler(); - static void terminationHadler(); - static void ensureEventHandlersInstalled(); - - typedef List PipeList; - - static PipeList* s_instances; -}; - -} -} - -#endif // __SyncPipe__ diff --git a/Lib/fdstream.hpp b/Lib/fdstream.hpp deleted file mode 100644 index c8681c69d7..0000000000 --- a/Lib/fdstream.hpp +++ /dev/null @@ -1,173 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file fdstream.hpp - * Defines class fdstream. - */ - -#ifndef __fdstream__ -#define __fdstream__ - -#include "Portability.hpp" - -#include -#include -#include -#include - -#include "Forwards.hpp" - -#include "Exception.hpp" - -namespace Lib { - -template < - typename CharType, - typename CharTraits = std::char_traits - > -class basic_fdbuf: public std::basic_streambuf -{ -public: - typedef CharType char_type; - typedef CharTraits traits_type; - typedef typename traits_type::int_type int_type; - typedef typename traits_type::pos_type pos_type; - typedef typename traits_type::off_type off_type; - - typedef basic_fdbuf this_type; - - basic_fdbuf( int fd ) : _fd( fd ), _preRead(-1) - { } - - ~basic_fdbuf() - { - } - - int_type getPreReadChar() const { return _preRead; } - void setPreReadChar(int_type val) { _preRead=val; } -protected: -// /** -// * Get the CURRENT character without advancing the file pointer -// */ - virtual int_type underflow() - { - if(_preRead!=-1) { - return _preRead; - } - int_type ch=uflow(); - if(ch!=traits_type::eof()) { - _preRead=ch; - } - return ch; - } - - virtual std::streamsize xsgetn ( char_type * s0, std::streamsize n0 ) - { - char_type * s=s0; - std::streamsize n=n0; - if(_preRead!=-1) { - *(s++)=_preRead; - n--; - _preRead=-1; - } - if(n==0) { - return n0-n; - } - errno=0; - ssize_t res=read(_fd, s, n*sizeof(char_type)); - if(res<0) { - SYSTEM_FAIL("read in xsgetn", errno); - return n0-n; - } - return (n0-n)+res/sizeof(char_type); - } - - /** - * Get the CURRENT character AND advance the file pointer - */ - virtual int_type uflow() - { - if(_preRead!=-1) { - int_type res=_preRead; - _preRead=-1; - return res; - } - - char_type ch; - errno=0; - ssize_t res=read(_fd, &ch, sizeof(char_type)); - if(res<0) { - SYSTEM_FAIL("read in uflow", errno); - return traits_type::eof(); - } - - return (res==sizeof(char_type)) ? ch : traits_type::eof(); - } - - virtual int_type sync() - { - _preRead=-1; //we throw away the preread char - return 0; - } - - virtual std::streamsize xsputn (const char_type * s, std::streamsize n) - { - ssize_t res=write(_fd, s, n*sizeof(char_type)); - if(res<0) { - return 0; - } - return res/sizeof(char_type); - } - - virtual int_type overflow( int_type c = traits_type::eof() ) - { - char_type ch=c; - ssize_t res=write(_fd, &ch, sizeof(char_type)); - return (res==sizeof(char_type)) ? 0 : traits_type::eof(); - } - -private: - int _fd; - int_type _preRead; -}; - - -template < -typename CharType, -typename CharTraits = std::char_traits -> -struct basic_fdstream: public std::basic_iostream -{ - typedef CharType char_type; - typedef CharTraits traits_type; - - typedef basic_fdbuf sbuf_type; - typedef basic_fdstream this_type; - typedef std::basic_iostream base_type; - - basic_fdstream( int fd ): - base_type( new sbuf_type( fd ) ) - { } - - ~basic_fdstream() - { delete static_cast(this->rdbuf()); } - - typename traits_type::int_type getPreReadChar() const - { return static_cast(this->rdbuf())->getPreReadChar(); } - void setPreReadChar(typename traits_type::int_type val) - { return static_cast(this->rdbuf())->setPreReadChar(val); } -}; - -typedef basic_fdbuf fdbuf; -typedef basic_fdstream fdstream; - -} - -#endif // __fdstream__ diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 7f26f5abf7..2d98c26dc7 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -115,7 +115,6 @@ void Options::init() "casc", "casc_hol", "casc_sat", - "casc_ltb", "clausify", "consequence_elimination", "model_check", @@ -197,16 +196,6 @@ void Options::init() _lookup.insert(&_randomizSeedForPortfolioWorkers); _randomizSeedForPortfolioWorkers.onlyUsefulWith(UsingPortfolioTechnology()); - _ltbLearning = ChoiceOptionValue("ltb_learning","ltbl",LTBLearning::OFF,{"on","off","biased"}); - _ltbLearning.description = "Perform learning in LTB mode"; - _lookup.insert(&_ltbLearning); - _ltbLearning.setExperimental(); - - _ltbDirectory = StringOptionValue("ltb_directory","",""); - _ltbDirectory.description = "Directory for output from LTB mode. Default is to put output next to problem."; - _lookup.insert(&_ltbDirectory); - _ltbDirectory.setExperimental(); - _decode = DecodeOptionValue("decode","",this); _decode.description="Decodes an encoded strategy. Can be used to replay a strategy. To make Vampire output an encoded version of the strategy use the encode option."; _lookup.insert(&_decode); diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 1a9897cc04..de7b0c771f 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -337,12 +337,6 @@ class Options SOFT }; - enum class LTBLearning : unsigned int { - ON, - OFF, - BIASED - }; - enum class IgnoreMissing : unsigned int { ON, OFF, @@ -392,7 +386,6 @@ class Options CASC, CASC_HOL, CASC_SAT, - CASC_LTB, CLAUSIFY, CONSEQUENCE_ELIMINATION, MODEL_CHECK, @@ -1979,8 +1972,6 @@ bool _hard; bool keepSbeamGenerators() const { return _fmbKeepSbeamGenerators.actualValue; } bool flattenTopLevelConjunctions() const { return _flattenTopLevelConjunctions.actualValue; } - LTBLearning ltbLearning() const { return _ltbLearning.actualValue; } - vstring ltbDirectory() const { return _ltbDirectory.actualValue; } Mode mode() const { return _mode.actualValue; } void setMode(Mode mode) { _mode.actualValue = mode; } Schedule schedule() const { return _schedule.actualValue; } @@ -2540,8 +2531,6 @@ bool _hard; IntOptionValue _lookaheadDelay; IntOptionValue _lrsFirstTimeCheck; BoolOptionValue _lrsWeightLimitOnly; - ChoiceOptionValue _ltbLearning; - StringOptionValue _ltbDirectory; #if VAMPIRE_PERF_EXISTS UnsignedOptionValue _instructionLimit; diff --git a/vampire.cpp b/vampire.cpp index c3e2edaefd..e7607e41ea 100644 --- a/vampire.cpp +++ b/vampire.cpp @@ -58,6 +58,7 @@ #include "Shell/Statistics.hpp" #include "Shell/UIHelper.hpp" #include "Shell/LaTeX.hpp" +#include "Shell/SineUtils.hpp" #include "Saturation/SaturationAlgorithm.hpp" @@ -560,7 +561,7 @@ void axiomSelectionMode(Problem* problem) } env.statistics->phase = Statistics::SINE_SELECTION; - SineSelector(*env.options).perform(*prb); + Shell::SineSelector(*env.options).perform(*prb); env.statistics->phase = Statistics::FINALIZATION; @@ -694,10 +695,6 @@ void dispatchByMode(Problem* problem) case Options::Mode::TPREPROCESS: preprocessMode(problem,true); break; - - case Options::Mode::CASC_LTB: - // handled elsewhere! - ASSERTION_VIOLATION; } } @@ -720,7 +717,7 @@ void interactiveMetamode() break; } else if (line.rfind("run",0) == 0) { // the whole running happens in a child (don't modify our options, don't crash here when parsing option rubbish, etc.) - pid_t process = Multiprocessing::instance()->fork(); + pid_t process = Lib::Sys::Multiprocessing::instance()->fork(); ASS_NEQ(process, -1); if(process == 0) { // probably garbage at this point @@ -735,10 +732,6 @@ void interactiveMetamode() } Shell::CommandLine cl(argv.size(), argv.begin()); cl.interpret(opts); - if (opts.mode() == Options::Mode::CASC_LTB) { - cout << "casc_ltb incompatible with interactive mode. Switching to vampire mode instead" << endl; - opts.setMode(Options::Mode::VAMPIRE); - } if (!opts.inputFile().empty()) { UIHelper::parseFile(opts.inputFile(),opts.inputSyntax(),true); prb = UIHelper::getInputProblem(); @@ -826,25 +819,7 @@ int main(int argc, char* argv[]) Lib::setMemoryLimit(env.options->memoryLimit() * 1048576ul); - // CASC_LTB is treated specially, all other modes are happy to receive a Problem* as input and take it from there - if (opts.mode() == Options::Mode::CASC_LTB) { - Timer::instance()->start(); - bool learning = opts.ltbLearning()!=Options::LTBLearning::OFF; - try { - if(learning){ - CASC::CLTBModeLearning::perform(); - } - else{ - CASC::CLTBMode::perform(); - } - } catch (Lib::SystemFailException& ex) { - cerr << "Process " << getpid() << " received SystemFailException" << endl; - ex.cry(cerr); - cerr << " and will now die" << endl; - } - //we have processed the ltb batch file, so we can return zero - vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS; - } else if (opts.interactive()) { + if (opts.interactive()) { interactiveMetamode(); } else { if (opts.inputFile().empty()) { From 124e51fff62518d43bb02b46538b0cc8c78cc3f5 Mon Sep 17 00:00:00 2001 From: Michael Rawson Date: Wed, 6 Mar 2024 20:27:55 +0000 Subject: [PATCH 2/3] also delete TwoVampires --- CMakeLists.txt | 1 - Lib/Environment.cpp | 2 - UnitTests/tTwoVampires.cpp | 175 ------------------------------------- vampire.cpp | 2 - 4 files changed, 180 deletions(-) delete mode 100644 UnitTests/tTwoVampires.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 31a7b82a2d..1a7ef97e7c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -720,7 +720,6 @@ set(UNIT_TESTS UnitTests/tSKIKBO.cpp UnitTests/tLPO.cpp UnitTests/tRatioKeeper.cpp - UnitTests/tTwoVampires.cpp UnitTests/tOptionConstraints.cpp UnitTests/tDHMultiset.cpp UnitTests/tList.cpp diff --git a/Lib/Environment.cpp b/Lib/Environment.cpp index bbbc49acaa..56738e8278 100644 --- a/Lib/Environment.cpp +++ b/Lib/Environment.cpp @@ -15,8 +15,6 @@ */ -#include "Lib/Sys/SyncPipe.hpp" - #include "Indexing/TermSharing.hpp" #include "Kernel/Signature.hpp" diff --git a/UnitTests/tTwoVampires.cpp b/UnitTests/tTwoVampires.cpp deleted file mode 100644 index e856043505..0000000000 --- a/UnitTests/tTwoVampires.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/* - * This file is part of the source code of the software program - * Vampire. It is protected by applicable - * copyright laws. - * - * This source code is distributed under the licence found here - * https://vprover.github.io/license.html - * and in the source directory - */ -/** - * @file tTwoVampires.cpp - * Unit test checking it is possible to work two child Vampires at once - */ - -#include "Lib/Portability.hpp" - -#include "Test/UnitTesting.hpp" - -#include -#include - -#include "Lib/Environment.hpp" -#include "Lib/Timer.hpp" -#include "Lib/Sys/Multiprocessing.hpp" -#include "Lib/Sys/SyncPipe.hpp" -#include "Lib/VString.hpp" - -#include "Kernel/Problem.hpp" - -#include "Shell/Options.hpp" -#include "Shell/Statistics.hpp" -#include "Shell/UIHelper.hpp" - -#include "Saturation/ProvingHelper.hpp" - -#include "Parse/TPTP.hpp" - -using namespace std; -using namespace Lib; -using namespace Lib::Sys; -using namespace Kernel; -using namespace Saturation; -using namespace Shell; - -//[[noreturn]] void runChild(UnitList* units, vstring slice); - -void runChild(UnitList* units, vstring slice) -{ - int resultValue=1; - try { - env.timer->reset(); - env.timer->start(); - - env.options->readFromEncodedOptions(slice); - - //To make sure the outputs of the two child Vampires don't interfere, - //the pipe allows only one process at a time to possess the output for - //writing (any other process that needs to output will wait). - - //However, not to block other processes from running, we claim the output - //only when we actually need it -- this we announce it by calling the - //functions env.beginOutput() and env.endOutput(). - - //As outputs can happen all over the Vampire, every (non-debugging) output - //is now encapsulated by a call to these two functions. - - //Also, to allow easy switching between cout and the pipe, the env.out - //member has now become a function env.out(). - env.beginOutput(); - env.out()<testId()<<" on "<problemName()<terminationReason==Statistics::REFUTATION) { - resultValue=0; - } - - env.beginOutput(); - UIHelper::outputResult(env.out()); - env.endOutput(); - } - catch (Exception& exception) { - env.beginOutput(); - exception.cry(env.out()); - env.endOutput(); - } catch (std::bad_alloc& _) { - env.beginOutput(); - env.out() << "Insufficient system memory" << '\n'; - env.endOutput(); - } - - - _exit(resultValue); -} - -TEST_FUN(two_vampires1) -{ - //a non-trivial satisfiable problem (LCL354+1) - vstring prob="fof(m1,axiom,( ! [P,Q,R,S] :( ( meets(P,Q) & meets(P,S) & meets(R,Q) ) => meets(R,S) ) ))." - "fof(m2,axiom, ( ! [P,Q,R,S] : ( ( meets(P,Q) & meets(R,S) ) => ( ( meets(P,S) <~> ? [T] : " - " ( meets(P,T) & meets(T,S) ) ) <~> ? [T] : ( meets(R,T) & meets(T,Q) ) ) ) ))." - "fof(m3,axiom, ( ! [P] : ? [Q,R] : ( meets(Q,P) & meets(P,R) ) ))." - "fof(not_m5,axiom, ( ~ ( ! [P,Q] : ( meets(P,Q) => ? [R,S,T] : ( meets(R,P) & meets(Q,S) & meets(R,T) & meets(T,S) ) ) ) ))."; - - //get the problem we'll be solving - vistringstream inp(prob); - UnitList* units=Parse::TPTP::parse(inp); - - //pipe for collecting the output from children - SyncPipe childOutputPipe; - - //create the first child - pid_t child1=Multiprocessing::instance()->fork(); - ASS_NEQ(child1,-1); - if(!child1) { - //we're in child1 - childOutputPipe.neverRead(); //we won't be reading from the pipe in children - env.setPipeOutput(&childOutputPipe); //direct output into the pipe - runChild(units, "dis+10_32_nwc=2.0:sac=on:spl=backtracking_20"); //start proving - } - - pid_t child2=Multiprocessing::instance()->fork(); - ASS_NEQ(child2,-1); - if(!child2) { - //we're in child2 - childOutputPipe.neverRead(); - env.setPipeOutput(&childOutputPipe); - runChild(units, "dis+4_8_30"); - } - - //We won't be writing anything into the pipe in the parent. - //(We cannot call this function before the forks, as then - //the children wouldn't be able to write either.) - childOutputPipe.neverWrite(); - - cout< Date: Mon, 11 Mar 2024 16:38:56 +0100 Subject: [PATCH 3/3] cleanup also in the Makefile --- Makefile | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 14823721ce..a71c945c68 100644 --- a/Makefile +++ b/Makefile @@ -167,8 +167,7 @@ VL_OBJ= Lib/Allocator.o\ Lib/Timer.o VLS_OBJ= Lib/Sys/Multiprocessing.o\ - Lib/Sys/Semaphore.o\ - Lib/Sys/SyncPipe.o + Lib/Sys/Semaphore.o VK_OBJ= Kernel/Clause.o\ Kernel/ClauseQueue.o\ @@ -388,9 +387,7 @@ DP_OBJ = DP/ShortConflictMetaDP.o\ DP/SimpleCongruenceClosure.o CASC_OBJ = CASC/PortfolioMode.o\ - CASC/Schedules.o\ - CASC/CLTBMode.o\ - CASC/CLTBModeLearning.o + CASC/Schedules.o VFMB_OBJ = FMB/ClauseFlattening.o\ FMB/SortInference.o\