diff --git a/vltb.cpp b/vltb.cpp deleted file mode 100644 index 1f23bc12b0..0000000000 --- a/vltb.cpp +++ /dev/null @@ -1,352 +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 vampire.cpp. Implements the top-level procedures of Vampire. - */ - -#include -#include -#include -#include - -#include "Debug/Tracer.hpp" - -#include "Lib/Exception.hpp" -#include "Lib/Environment.hpp" -#include "Lib/Int.hpp" -#include "Lib/Random.hpp" -#include "Lib/Set.hpp" -#include "Lib/Stack.hpp" -#include "Lib/TimeCounter.hpp" -#include "Lib/Timer.hpp" -#include "Lib/VString.hpp" -#include "Lib/List.hpp" -#include "Lib/Vector.hpp" -#include "Lib/System.hpp" -#include "Lib/Metaiterators.hpp" - -#include "Kernel/Clause.hpp" -#include "Kernel/Formula.hpp" -#include "Kernel/FormulaUnit.hpp" -#include "Kernel/InferenceStore.hpp" -#include "Kernel/Term.hpp" - -#include "Indexing/SubstitutionTree.hpp" -#include "Indexing/LiteralMiniIndex.hpp" - -#include "Shell/CommandLine.hpp" -#include "Shell/Grounding.hpp" -#include "Shell/Interpolants.hpp" -#include "Shell/LaTeX.hpp" -#include "Shell/LispLexer.hpp" -#include "Shell/LispParser.hpp" -#include "Shell/Options.hpp" -#include "Shell/Property.hpp" -#include "Shell/Preprocess.hpp" -#include "Shell/Refutation.hpp" -#include "Shell/TheoryFinder.hpp" -#include "Shell/SimplifyProver.hpp" -#include "Shell/Statistics.hpp" -#include "Shell/TPTP.hpp" - -#include "Shell/LTB/Builder.hpp" -#include "Shell/LTB/Selector.hpp" - -#include "Parse/TPTP.hpp" - -#include "Saturation/SaturationAlgorithm.hpp" - -#include "SAT/DIMACS.hpp" -#include "SAT/SATClause.hpp" - - -#if CHECK_LEAKS -#include "Lib/MemoryLeak.hpp" -#endif - -#define SPIDER 0 -#define SAVE_SPIDER_PROPERTIES 0 - -using namespace Shell; -using namespace SAT; -using namespace Saturation; -using namespace Inferences; - -UnitList* globUnitList=0; - -ClauseIterator getProblemClauses() -{ - CALL("getProblemClauses"); - - Shell::LTB::Selector selector; - Property property; - - UnitList* units; - { - TimeCounter tc1(TC_PARSING); - - vstring inputFile = env.options->inputFile(); - - istream* input; - if(inputFile=="") { - input=&cin; - } else { - input=new ifstream(inputFile.c_str()); - if(input->fail()) { - USER_ERROR("Cannot open input file: "+inputFile); - } - } - - env.statistics->phase=Statistics::PARSING; - if(env.options->inputSyntax()!=Options::IS_TPTP) { - USER_ERROR("Unsupported input syntax"); - } - - { - Parse::TPTP parser(*input); - StringList::Iterator names(selector.theoryFileNames()); - while (names.hasNext()) { - parser.addForbiddenInclude(names.next()); - } - parser.parse() - units = parser.units(); - } - - if(inputFile!="") { - delete static_cast(input); - input=0; - } - } - - selector.selectForProblem(units); - - TimeCounter tc2(TC_PREPROCESSING); - - env.statistics->phase=Statistics::PROPERTY_SCANNING; - property.scan(units); - Preprocess prepro(property,*env.options); - //phases for preprocessing are being set inside the proprocess method - prepro.preprocess(units); - - globUnitList=units; - - return pvi( getStaticCastIterator(UnitList::Iterator(units)) ); -} - -void outputResult() -{ - CALL("outputResult()"); - - switch (env.statistics->terminationReason) { - case Statistics::REFUTATION: - env.out << "Refutation found. Thanks to " - << env.options->thanks() << "!\n"; - if (env.options->proof() != Options::PROOF_OFF) { -// Shell::Refutation refutation(env.statistics->refutation, -// env.options->proof() == Options::PROOF_ON); -// refutation.output(env.out); - InferenceStore::instance()->outputProof(env.out, env.statistics->refutation); - } - if(env.options->showInterpolant()!=Options::INTERP_OFF) { - ASS(env.statistics->refutation->isClause()); - Formula* interpolant=Interpolants::getInterpolant(static_cast(env.statistics->refutation)); - env.out << "Interpolant: " << interpolant->toString() << endl; - } - if(env.options->latexOutput()!="off") { - ofstream latexOut(env.options->latexOutput().c_str()); - - LaTeX formatter; - latexOut<refutation); - } - break; - case Statistics::TIME_LIMIT: - env.out << "Time limit reached!\n"; - break; - case Statistics::MEMORY_LIMIT: -#if VDEBUG - Allocator::reportUsageByClasses(); -#endif - env.out << "Memory limit exceeded!\n"; - break; - case Statistics::REFUTATION_NOT_FOUND: - if(env.options->complete()) { - ASS_EQ(env.options->saturationAlgorithm(), Options::LRS); - env.out << "Refutation not found, LRS age and weight limit was active for some time!\n"; - } else { - env.out << "Refutation not found with incomplete strategy!\n"; - } - break; - case Statistics::SATISFIABLE: - env.out << "Refutation not found!\n"; - break; - case Statistics::UNKNOWN: - env.out << "Unknown reason of termination!\n"; - break; - default: - ASSERTION_VIOLATION; - } - env.statistics->print(); -} - -void explainException (Exception& exception) -{ - exception.cry(env.out); -} // explainException - -void ltbBuildMode() -{ - CALL("ltbBuildMode"); - - vstring inputFile = env.options->inputFile(); - - istream* input0; - if(inputFile=="") { - input0=&cin; - } else { - input0=new ifstream(inputFile.c_str()); - if(input0->fail()) { - USER_ERROR("Cannot open input file: "+inputFile); - } - } - istream& input=*input0; - - Stack nameStack; - char lineBuf[1024]; - - while(!input.eof()) { - input.getline(lineBuf, 1024); - vstring line(lineBuf); - if(line.length()<12 || line.substr(0,9)!="include('" || line.substr(line.length()-3,3)!="').") { - continue; - } - vstring fname(line, 9, line.length()-3-9); - - nameStack.push(fname); - } - - Shell::LTB::Builder builder; - builder.build(pvi( Stack::Iterator(nameStack) )); - - if(inputFile!="") { - delete static_cast(&input); - } -} - -void ltbSolveMode() -{ - CALL("ltbSolveMode"); - - env.beginOutput(); - env.out()<testId()<<" on "<problemName()<phase=Statistics::SATURATION; - MainLoopSP salg=MainLoop::createFromOptions(); - salg->addInputClauses(clauses); - - MainLoopResult sres(salg->saturate()); - env.statistics->phase=Statistics::FINALIZATION; - sres.updateStatistics(); - } - catch(MemoryLimitExceededException) { - env.statistics->terminationReason=Statistics::MEMORY_LIMIT; - env.statistics->refutation=0; - size_t limit=Allocator::getMemoryLimit(); - //add extra 1 MB to allow proper termination - Allocator::setMemoryLimit(limit+1000000); - } - catch(TimeLimitExceededException) { - env.statistics->terminationReason=Statistics::TIME_LIMIT; - env.statistics->refutation=0; - } - outputResult(); -} - -/** - * The main function. - * @since 03/12/2003 many changes related to logging - * and exception handling. - * @since 10/09/2004, Manchester changed to use knowledge bases - */ -int main(int argc, char* argv []) -{ - CALL ("main"); - - System::setSignalHandlers(); - // create random seed for the random number generation - Lib::Random::setSeed(123456); - - try { - // read the command line and interpret it - Shell::CommandLine cl(argc,argv); - cl.interpret(*env.options); - - Allocator::setMemoryLimit(env.options->memoryLimit()*1048576ul); - Lib::Random::setSeed(env.options->randomSeed()); - - switch (env.options->mode()) - { - case Options::MODE_LTB_BUILD: - ltbBuildMode(); - break; - case Options::MODE_LTB_SOLVE: - ltbSolveMode(); - break; - default: - USER_ERROR("Specified mode is not supported by the vltb executable (use '--mode ltb_build' or '--mode ltb_solve')"); - break; - } -#if CHECK_LEAKS - if (globUnitList) { - MemoryLeak leak; - leak.release(globUnitList); - } - delete env.signature; - env.signature = 0; -#endif - } -#if VDEBUG - catch (Debug::AssertionViolationException& exception) { - reportSpiderFail(); -#if CHECK_LEAKS - MemoryLeak::cancelReport(); -#endif - } -#endif - catch (UserErrorException& exception) { - reportSpiderFail(); -#if CHECK_LEAKS - MemoryLeak::cancelReport(); -#endif - explainException(exception); - } - catch (Exception& exception) { - reportSpiderFail(); -#if CHECK_LEAKS - MemoryLeak::cancelReport(); -#endif - explainException(exception); - env.statistics->print(); - } - catch (std::bad_alloc& _) { - reportSpiderFail(); -#if CHECK_LEAKS - MemoryLeak::cancelReport(); -#endif - env.out << "Insufficient system memory" << '\n'; - } -// delete env.allocator; - - return EXIT_SUCCESS; -} // main -