diff --git a/Parse/TPTP.cpp b/Parse/TPTP.cpp index 4cc6c0139..c825f3e31 100644 --- a/Parse/TPTP.cpp +++ b/Parse/TPTP.cpp @@ -74,21 +74,10 @@ const int TPTP::PI = 102u; /** Sigma function for existential quantification */ const int TPTP::SIGMA = 103u; -/** - * Create a parser, parse the input and return the parsed list of units. - * @since 13/07/2011 Manchester - */ -UnitList* TPTP::parse(istream& input) -{ - Parse::TPTP parser(input); - parser.parse(); - return parser.units(); -} - Unit* TPTP::parseFormulaFromString(const std::string& str) { std::stringstream input(str+")."); // to fake endFOF, which creates the clause - Parse::TPTP parser(input); + Parse::TPTP parser(input, ""); parser._lastInputType = UnitInputType::AXIOM; parser._bools.push(true); // true is what fof/tff normally pushes (but we start "from the middle") parser._strings.push("dummy_name"); @@ -101,9 +90,9 @@ Unit* TPTP::parseFormulaFromString(const std::string& str) * Initialise a lexer. * @since 27/07/2004 Torrevieja */ -TPTP::TPTP(std::istream &in, UnitList::FIFO unitBuffer) +TPTP::TPTP(std::istream &in, std::filesystem::path path, UnitList::FIFO unitBuffer) : _containsConjecture(false), - currentFile { &in, {}, {}, 1 }, + currentFile { &in, {}, path, 1 }, _units(unitBuffer), _isThf(false), _containsPolymorphism(false), diff --git a/Parse/TPTP.hpp b/Parse/TPTP.hpp index d9cd255ac..9475c8ec0 100644 --- a/Parse/TPTP.hpp +++ b/Parse/TPTP.hpp @@ -317,6 +317,7 @@ class TPTP * @brief Construct a new TPTP parser. * * @param in is the stream with the raw input to read + * @param path is the path to the file backing the stream (or e.g. '', '') * @param unitBuffer is FIFO of units to which newly parsed Clauses/Formulas * will be added (via pushBack); * @@ -324,10 +325,9 @@ class TPTP * (use this default behaviour if you do not want to collect formulas * from multiple parser calls) */ - TPTP(std::istream &in, UnitList::FIFO unitBuffer = UnitList::FIFO()); + TPTP(std::istream &in, std::filesystem::path path, UnitList::FIFO unitBuffer = UnitList::FIFO()); ~TPTP(); void parse(); - static UnitList* parse(std::istream& str); static Unit* parseFormulaFromString(const std::string& str); /** Return the list of parsed units */ UnitList* units() const { return _units.list(); } diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index e67db5671..4d4718e8e 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -189,10 +189,10 @@ static bool hasEnding (std::string const &fullString, std::string const &ending) } } -void UIHelper::tryParseTPTP(istream& input) +void UIHelper::tryParseTPTP(istream& input, std::filesystem::path path) { LoadedPiece& curPiece = _loadedPieces.top(); - Parse::TPTP parser(input,curPiece._units); + Parse::TPTP parser(input,path,curPiece._units); try { parser.parse(); curPiece._units = parser.unitBuffer(); @@ -239,7 +239,7 @@ void UIHelper::parseSingleLine(const std::string& lineToParse, Options::InputSyn try { switch (inputSyntax) { case Options::InputSyntax::TPTP: - tryParseTPTP(stream); + tryParseTPTP(stream, ""); break; case Options::InputSyntax::SMTLIB2: tryParseSMTLIB2(stream); @@ -270,7 +270,7 @@ void resetParsing(ParsingRelatedException& exception, istream& input, std::strin input.seekg(0); } -void UIHelper::parseStream(std::istream& input, Options::InputSyntax inputSyntax, bool verbose, bool preferSMTonAuto) +void UIHelper::parseStream(std::istream& input, std::filesystem::path path, Options::InputSyntax inputSyntax, bool verbose, bool preferSMTonAuto) { switch (inputSyntax) { case Options::InputSyntax::AUTO: @@ -283,7 +283,7 @@ void UIHelper::parseStream(std::istream& input, Options::InputSyntax inputSyntax tryParseSMTLIB2(input); } catch (ParsingRelatedException& exception) { resetParsing(exception,input,"TPTP"); - tryParseTPTP(input); + tryParseTPTP(input, path); } } else { if (verbose) { @@ -291,7 +291,7 @@ void UIHelper::parseStream(std::istream& input, Options::InputSyntax inputSyntax std::cout << "Running in auto input_syntax mode. Trying TPTP\n"; } try { - tryParseTPTP(input); + tryParseTPTP(input, path); } catch (ParsingRelatedException& exception) { resetParsing(exception,input,"SMTLIB2"); tryParseSMTLIB2(input); @@ -299,7 +299,7 @@ void UIHelper::parseStream(std::istream& input, Options::InputSyntax inputSyntax } break; case Options::InputSyntax::TPTP: - tryParseTPTP(input); + tryParseTPTP(input, path); break; case Options::InputSyntax::SMTLIB2: tryParseSMTLIB2(input); @@ -320,7 +320,7 @@ void UIHelper::parseStandardInput(Options::InputSyntax inputSyntax) inputSyntax = Options::InputSyntax::TPTP; } try { - parseStream(cin,inputSyntax,false,false); + parseStream(cin, "", inputSyntax,false,false); } catch (ParsingRelatedException& exception) { _loadedPieces.pop(); throw; @@ -342,7 +342,7 @@ void UIHelper::parseFile(const std::string& inputFile, Options::InputSyntax inpu } try { - parseStream(input,inputSyntax,verbose,hasEnding(inputFile,"smt") || hasEnding(inputFile,"smt2")); + parseStream(input,inputFile,inputSyntax,verbose,hasEnding(inputFile,"smt") || hasEnding(inputFile,"smt2")); } catch (ParsingRelatedException& exception) { _loadedPieces.pop(); throw; diff --git a/Shell/UIHelper.hpp b/Shell/UIHelper.hpp index 2553119cb..71dbd9e2d 100644 --- a/Shell/UIHelper.hpp +++ b/Shell/UIHelper.hpp @@ -15,6 +15,7 @@ #ifndef __UIHelper__ #define __UIHelper__ +#include #include #include "Forwards.hpp" @@ -45,12 +46,12 @@ class UIHelper { }; static Stack _loadedPieces; - static void tryParseTPTP(std::istream& input); + static void tryParseTPTP(std::istream& input, std::filesystem::path path); static void tryParseSMTLIB2(std::istream& input); public: static void parseSingleLine(const std::string& lineToParse, Options::InputSyntax inputSyntax); - static void parseStream(std::istream& input, Options::InputSyntax inputSyntax, bool verbose, bool preferSMTonAuto); + static void parseStream(std::istream& input, std::filesystem::path path, Options::InputSyntax inputSyntax, bool verbose, bool preferSMTonAuto); static void parseStandardInput(Options::InputSyntax inputSyntax); static void parseFile(const std::string& inputFile, Options::InputSyntax inputSyntax, bool verbose);