Move tptp frontend to cmd_context and add string API

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1be7cf7e-2747-43ba-9a33-2e71dad2d14d

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/cmd_context/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(cmd_context
     simplifier_cmds.cpp
     tactic_cmds.cpp
     tactic_manager.cpp
+    tptp_frontend.cpp
   COMPONENT_DEPENDENCIES
     rewriter
     solver

src/cmd_context/tptp_frontend.cpp

@@ -13,7 +13,7 @@
 #include "ast/expr_abstract.h"
 #include "ast/ast_util.h"
 #include "cmd_context/cmd_context.h"
-#include "shell/tptp_frontend.h"
+#include "cmd_context/tptp_frontend.h"
 #include "smt/smt_solver.h"
 #include "util/error_codes.h"
 #include "util/z3_exception.h"
@@ -727,6 +727,15 @@ public:
         m_sorts.emplace("$real", m_arith.mk_real());
     }
 
+    void parse_stream(std::istream& in, std::string const& current_file) {
+        std::ostringstream buf;
+        buf << in.rdbuf();
+        m_input = buf.str();
+        m_lex = std::make_unique<lexer>(m_input);
+        next();
+        parse_toplevel(current_file);
+    }
+
     void parse_file(std::string const& filename) {
         if (!m_seen_files.insert(filename).second) return;
         std::ifstream in(filename);
@@ -735,21 +744,11 @@ public:
             out << "failed to open file '" << filename << "'";
             throw parse_error(out.str());
         }
-        std::ostringstream buf;
-        buf << in.rdbuf();
-        m_input = buf.str();
-        m_lex = std::make_unique<lexer>(m_input);
-        next();
-        parse_toplevel(filename);
+        parse_stream(in, filename);
     }
 
     void parse_stream(std::istream& in) {
-        std::ostringstream buf;
-        buf << in.rdbuf();
-        m_input = buf.str();
-        m_lex = std::make_unique<lexer>(m_input);
-        next();
-        parse_toplevel(".");
+        parse_stream(in, ".");
     }
 
     bool has_conjecture() const { return m_has_conjecture; }
@@ -787,14 +786,13 @@ expr_ref tptp_parser::parse_formula() {
 
 }
 
-unsigned read_tptp(char const* file_name) {
+static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
     try {
         cmd_context ctx;
         ctx.set_solver_factory(mk_smt_strategic_solver_factory());
 
         tptp_parser p(ctx);
-        if (file_name) p.parse_file(file_name);
-        else p.parse_stream(std::cin);
+        p.parse_stream(in, current_file ? current_file : ".");
 
         // Suppress default check-sat output; TPTP frontend reports SZS status explicitly.
         std::ostringstream sink;
@@ -840,3 +838,19 @@ unsigned read_tptp(char const* file_name) {
         return ERR_INTERNAL_FATAL;
     }
 }
+
+unsigned read_tptp(char const* file_name) {
+    if (!file_name)
+        return read_tptp_stream(std::cin, ".");
+    std::ifstream in(file_name);
+    if (in.fail()) {
+        std::cerr << "TPTP parse error: failed to open file '" << file_name << "'\n";
+        return ERR_PARSER;
+    }
+    return read_tptp_stream(in, file_name);
+}
+
+unsigned read_tptp_string(char const* input) {
+    std::istringstream in(input ? input : "");
+    return read_tptp_stream(in, "<string>");
+}

src/cmd_context/tptp_frontend.h

@@ -1,3 +1,4 @@
 #pragma once
 
 unsigned read_tptp(char const* file_name);
+unsigned read_tptp_string(char const* input);

src/shell/CMakeLists.txt

@@ -27,7 +27,6 @@ add_executable(shell
   "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
   opt_frontend.cpp
   smtlib_frontend.cpp
-  tptp_frontend.cpp
   z3_log_frontend.cpp
 # FIXME: shell should really link against libz3 but it can't due to requiring
 # use of some hidden symbols. Also libz3 has the ``api_dll`` component which

src/shell/main.cpp

@@ -30,7 +30,7 @@ Revision History:
 #include "shell/dimacs_frontend.h"
 #include "shell/datalog_frontend.h"
 #include "shell/opt_frontend.h"
-#include "shell/tptp_frontend.h"
+#include "cmd_context/tptp_frontend.h"
 #include "util/timeout.h"
 #include "util/z3_exception.h"
 #include "util/error_codes.h"

src/test/CMakeLists.txt

@@ -146,7 +146,6 @@ add_executable(test-z3
   theory_pb.cpp
   timeout.cpp
   tptp.cpp
-  ../shell/tptp_frontend.cpp
   total_order.cpp
   totalizer.cpp
   trigo.cpp
@@ -167,7 +166,6 @@ z3_add_memory_initializer_rule(${z3_test_deps})
 z3_add_gparams_register_modules_rule(${z3_test_deps})
 target_compile_definitions(test-z3 PRIVATE
   ${Z3_COMPONENT_CXX_DEFINES}
-  Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}"
 )
 target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
 target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})

src/test/tptp.cpp

@@ -3,19 +3,19 @@
 #include <iostream>
 #include <sstream>
 #include "util/debug.h"
-#include "shell/tptp_frontend.h"
+#include "cmd_context/tptp_frontend.h"
 
 struct tptp_case {
-    char const* file;
+    char const* name;
+    char const* input;
     char const* expected_status;
 };
 
-static std::string run_tptp(char const* file) {
-    std::string path = std::string(Z3_TEST_SRC_DIR) + "/tptp/" + file;
+static std::string run_tptp(char const* input) {
     std::streambuf* old_out = std::cout.rdbuf();
     std::ostringstream out;
     std::cout.rdbuf(out.rdbuf());
-    unsigned code = read_tptp(path.c_str());
+    unsigned code = read_tptp_string(input);
     std::cout.rdbuf(old_out);
     ENSURE(code == 0);
     return out.str();
@@ -27,12 +27,35 @@ bool g_display_model = false;
 
 void tst_tptp() {
     std::vector<tptp_case> cases = {
-        {"agatha-butler.p", "% SZS status Theorem"},
-        {"socrates-theorem.p", "% SZS status Theorem"},
-        {"simple-sat.p", "% SZS status Satisfiable"}
+        {"agatha-butler",
+R"(fof(ax1,axiom, lives(agatha)).
+fof(ax2,axiom, lives(butler)).
+fof(ax3,axiom, lives(charles)).
+fof(ax4,axiom, ! [X] : (lives(X) => (X = agatha | X = butler | X = charles))).
+fof(ax5,axiom, ! [X,Y] : (killed(X,Y) => hates(X,Y))).
+fof(ax6,axiom, ! [X,Y] : (killed(X,Y) => ~ richer(X,Y))).
+fof(ax7,axiom, ! [X] : (hates(agatha,X) => ~ hates(charles,X))).
+fof(ax8,axiom, ! [X] : (X != butler => hates(agatha,X))).
+fof(ax9,axiom, ! [X] : (~ richer(X,agatha) => hates(butler,X))).
+fof(ax10,axiom, ! [X] : (hates(agatha,X) => hates(butler,X))).
+fof(ax11,axiom, ! [X] : (? [Y] : ~ hates(X,Y))).
+fof(ax12,axiom, agatha != butler).
+fof(ax13,axiom, ? [X] : killed(X,agatha)).
+fof(conj,conjecture, ~ killed(butler,agatha)).)",
+         "% SZS status Theorem"},
+        {"socrates-theorem",
+R"(fof(a1,axiom, ! [X] : (human(X) => mortal(X))).
+fof(a2,axiom, human(socrates)).
+fof(c1,conjecture, mortal(socrates)).)",
+         "% SZS status Theorem"},
+        {"simple-sat",
+R"(fof(a1,axiom, p(a)).)",
+         "% SZS status Satisfiable"}
     };
     for (auto const& c : cases) {
-        std::string out = run_tptp(c.file);
+        std::string out = run_tptp(c.input);
+        if (out.find(c.expected_status) == std::string::npos)
+            std::cerr << "Unexpected TPTP status for case: " << c.name << "\n" << out << "\n";
         ENSURE(out.find(c.expected_status) != std::string::npos);
     }
 }

src/test/tptp/agatha-butler.p

@@ -1,18 +0,0 @@
-fof(ax1,axiom, lives(agatha)).
-fof(ax2,axiom, lives(butler)).
-fof(ax3,axiom, lives(charles)).
-
-fof(ax4,axiom, ! [X] : (lives(X) => (X = agatha | X = butler | X = charles))).
-fof(ax5,axiom, ! [X,Y] : (killed(X,Y) => hates(X,Y))).
-fof(ax6,axiom, ! [X,Y] : (killed(X,Y) => ~ richer(X,Y))).
-
-fof(ax7,axiom, ! [X] : (hates(agatha,X) => ~ hates(charles,X))).
-fof(ax8,axiom, ! [X] : (X != butler => hates(agatha,X))).
-fof(ax9,axiom, ! [X] : (~ richer(X,agatha) => hates(butler,X))).
-fof(ax10,axiom, ! [X] : (hates(agatha,X) => hates(butler,X))).
-fof(ax11,axiom, ! [X] : (? [Y] : ~ hates(X,Y))).
-
-fof(ax12,axiom, agatha != butler).
-fof(ax13,axiom, ? [X] : killed(X,agatha)).
-
-fof(conj,conjecture, ~ killed(butler,agatha)).

src/test/tptp/simple-sat.p

@@ -1,2 +0,0 @@
-fof(a1,axiom, p(a)).
-

src/test/tptp/socrates-theorem.p

@@ -1,4 +0,0 @@
-fof(a1,axiom, ! [X] : (human(X) => mortal(X))).
-fof(a2,axiom, human(socrates)).
-fof(c1,conjecture, mortal(socrates)).
-