also allow imports relative to the _supplied_ input file

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, "<string>");
   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),

Parse/TPTP.hpp

@@ -317,17 +317,17 @@ 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. '<stdin>', '<string>')
    * @param unitBuffer is FIFO of units to which newly parsed Clauses/Formulas
    *   will be added (via pushBack);
    *
    *  if left unspecified, and empty fifo is created and used instead.
    *  (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(); }

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, "<string>");
         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,23 +283,23 @@ 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) {
         addCommentSignForSZS(std::cout);
         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);
       }
     }
     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, "<stdin>", 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;

Shell/UIHelper.hpp

@@ -15,6 +15,7 @@
 #ifndef __UIHelper__
 #define __UIHelper__
 
+#include <filesystem>
 #include <ostream>
 
 #include "Forwards.hpp"
@@ -45,12 +46,12 @@ class UIHelper {
   };
   static Stack<LoadedPiece> _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);