From 50fb4d5ac61a98ff47bb0c4d22ed6a64e35e47c0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 8 May 2026 17:09:18 +0000 Subject: [PATCH] Add shell-integrated self-contained TPTP frontend and CLI wiring Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ba80bc5a-d80f-4d9f-8ed4-a962f697697c Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/shell/CMakeLists.txt | 1 + src/shell/main.cpp | 14 +- src/shell/tptp_frontend.cpp | 771 ++++++++++++++++++++++++++++++++++++ src/shell/tptp_frontend.h | 3 + 4 files changed, 787 insertions(+), 2 deletions(-) create mode 100644 src/shell/tptp_frontend.cpp create mode 100644 src/shell/tptp_frontend.h diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c0e9c8505..30d10f0ab 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -27,6 +27,7 @@ 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 diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 19e617e55..2125c3bcf 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -30,6 +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 "util/timeout.h" #include "util/z3_exception.h" #include "util/error_codes.h" @@ -43,7 +44,7 @@ Revision History: #include #endif -typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_DRAT } input_kind; +typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_DRAT, IN_TPTP } input_kind; static char const * g_input_file = nullptr; static char const * g_drat_input_file = nullptr; @@ -84,6 +85,7 @@ void display_usage() { std::cout << " -opb use parser for PB optimization input format.\n"; std::cout << " -lp use parser for a modest subset of CPLEX LP input format.\n"; std::cout << " -log use parser for Z3 log input format.\n"; + std::cout << " -tptp use parser for TPTP input format (fof/cnf/tff/thf fragments).\n"; std::cout << " -in read formula from standard input.\n"; std::cout << " -model display model for satisfiable SMT.\n"; std::cout << "\nMiscellaneous:\n"; @@ -214,6 +216,9 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) else if (strcmp(opt_name, "log") == 0) { g_input_kind = IN_Z3_LOG; } + else if (strcmp(opt_name, "tptp") == 0) { + g_input_kind = IN_TPTP; + } else if (strcmp(opt_name, "st") == 0) { g_display_statistics = true; gparams::set("stats", "true"); @@ -387,6 +392,9 @@ int STD_CALL main(int argc, char ** argv) { else if (strcmp(ext, "smt2") == 0) { g_input_kind = IN_SMTLIB_2; } + else if (strcmp(ext, "p") == 0 || strcmp(ext, "tptp") == 0 || strcmp(ext, "fof") == 0 || strcmp(ext, "cnf") == 0 || strcmp(ext, "tff") == 0 || strcmp(ext, "thf") == 0) { + g_input_kind = IN_TPTP; + } } } switch (g_input_kind) { @@ -415,6 +423,9 @@ int STD_CALL main(int argc, char ** argv) { case IN_DRAT: return_value = read_drat(g_drat_input_file); break; + case IN_TPTP: + return_value = read_tptp(g_input_file); + break; default: UNREACHABLE(); } @@ -434,4 +445,3 @@ int STD_CALL main(int argc, char ** argv) { return ERR_INTERNAL_FATAL; } } - diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp new file mode 100644 index 000000000..b7dab46fa --- /dev/null +++ b/src/shell/tptp_frontend.cpp @@ -0,0 +1,771 @@ +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "api/c++/z3++.h" +#include "shell/tptp_frontend.h" +#include "util/error_codes.h" + +extern bool g_display_statistics; +extern bool g_display_model; + +namespace { + +enum class token_kind { + eof_tok, + id, + str, + lparen, + rparen, + lbrack, + rbrack, + comma, + dot, + colon, + and_tok, + or_tok, + not_tok, + forall_tok, + exists_tok, + equal_tok, + neq_tok, + iff_tok, + implies_tok, + implied_tok, + xor_tok, + nor_tok, + nand_tok, + gt_tok, + star_tok, + at_tok +}; + +struct parse_error : public std::exception { + std::string m_msg; + parse_error(std::string const& msg): m_msg(msg) {} + const char* what() const noexcept override { return m_msg.c_str(); } +}; + +struct token { + token_kind kind = token_kind::eof_tok; + std::string text; + unsigned line = 1; + unsigned col = 1; +}; + +class lexer { + std::string const& m_input; + size_t m_pos = 0; + unsigned m_line = 1; + unsigned m_col = 1; + + bool eof() const { return m_pos >= m_input.size(); } + char peek(unsigned k = 0) const { return m_pos + k < m_input.size() ? m_input[m_pos + k] : '\0'; } + char get() { + char c = peek(); + if (!eof()) { + ++m_pos; + if (c == '\n') { + ++m_line; + m_col = 1; + } + else { + ++m_col; + } + } + return c; + } + + static bool is_id_start(char c) { + return std::isalpha(static_cast(c)) || c == '$' || c == '_' || std::isdigit(static_cast(c)); + } + + static bool is_id_char(char c) { + return std::isalnum(static_cast(c)) || c == '$' || c == '_' || c == '\'' || c == '-'; + } + + void skip_ws_comments() { + while (!eof()) { + if (std::isspace(static_cast(peek()))) { + get(); + continue; + } + if (peek() == '%') { + while (!eof() && get() != '\n') {} + continue; + } + if (peek() == '/' && peek(1) == '*') { + get(); + get(); + while (!eof()) { + if (peek() == '*' && peek(1) == '/') { + get(); + get(); + break; + } + get(); + } + continue; + } + break; + } + } + +public: + lexer(std::string const& input): m_input(input) {} + + token next() { + skip_ws_comments(); + token t; + t.line = m_line; + t.col = m_col; + if (eof()) { + t.kind = token_kind::eof_tok; + return t; + } + + if (peek() == '\'' || peek() == '"') { + char q = get(); + t.kind = token_kind::str; + while (!eof()) { + char c = get(); + if (c == '\\' && !eof()) { + t.text.push_back(c); + t.text.push_back(get()); + continue; + } + if (c == q) return t; + t.text.push_back(c); + } + throw parse_error("unterminated string literal"); + } + + if (peek() == '<' && peek(1) == '=' && peek(2) == '>') { + get(); get(); get(); + t.kind = token_kind::iff_tok; + t.text = "<=>"; + return t; + } + if (peek() == '<' && peek(1) == '~' && peek(2) == '>') { + get(); get(); get(); + t.kind = token_kind::xor_tok; + t.text = "<~>"; + return t; + } + if (peek() == '=' && peek(1) == '>') { + get(); get(); + t.kind = token_kind::implies_tok; + t.text = "=>"; + return t; + } + if (peek() == '<' && peek(1) == '=') { + get(); get(); + t.kind = token_kind::implied_tok; + t.text = "<="; + return t; + } + if (peek() == '~' && peek(1) == '|') { + get(); get(); + t.kind = token_kind::nor_tok; + t.text = "~|"; + return t; + } + if (peek() == '~' && peek(1) == '&') { + get(); get(); + t.kind = token_kind::nand_tok; + t.text = "~&"; + return t; + } + if (peek() == '!' && peek(1) == '=') { + get(); get(); + t.kind = token_kind::neq_tok; + t.text = "!="; + return t; + } + + char c = get(); + switch (c) { + case '(': t.kind = token_kind::lparen; return t; + case ')': t.kind = token_kind::rparen; return t; + case '[': t.kind = token_kind::lbrack; return t; + case ']': t.kind = token_kind::rbrack; return t; + case ',': t.kind = token_kind::comma; return t; + case '.': t.kind = token_kind::dot; return t; + case ':': t.kind = token_kind::colon; return t; + case '&': t.kind = token_kind::and_tok; return t; + case '|': t.kind = token_kind::or_tok; return t; + case '~': t.kind = token_kind::not_tok; return t; + case '!': t.kind = token_kind::forall_tok; return t; + case '?': t.kind = token_kind::exists_tok; return t; + case '=': t.kind = token_kind::equal_tok; return t; + case '>': t.kind = token_kind::gt_tok; return t; + case '*': t.kind = token_kind::star_tok; return t; + case '@': t.kind = token_kind::at_tok; return t; + default: + break; + } + + if (is_id_start(c)) { + t.kind = token_kind::id; + t.text.push_back(c); + while (!eof() && is_id_char(peek())) + t.text.push_back(get()); + return t; + } + + std::ostringstream out; + out << "unexpected character '" << c << "' at " << t.line << ":" << t.col; + throw parse_error(out.str()); + } +}; + +struct parsed_type { + std::vector domain; + z3::sort range; + parsed_type(z3::sort const& s): range(s) {} + parsed_type(std::vector const& d, z3::sort const& r): domain(d), range(r) {} +}; + +class tptp_parser { + z3::context& m_ctx; + z3::solver& m_solver; + z3::sort m_univ; + bool m_has_conjecture = false; + std::unordered_map m_sorts; + std::unordered_map m_decls; + std::unordered_map, z3::sort>> m_typed_decls; + std::vector> m_bound; + std::unordered_set m_seen_files; + + std::string m_input; + std::unique_ptr m_lex; + token m_curr; + std::vector m_file_stack; + + static std::string to_lower(std::string s) { + for (char& c : s) c = static_cast(std::tolower(static_cast(c))); + return s; + } + + static bool is_var_name(std::string const& s) { + if (s.empty()) return false; + unsigned char c = static_cast(s[0]); + return std::isupper(c) || s[0] == '_'; + } + + std::string loc() const { + std::ostringstream out; + out << m_curr.line << ":" << m_curr.col; + return out.str(); + } + + void next() { m_curr = m_lex->next(); } + + bool is(token_kind k) const { return m_curr.kind == k; } + + bool accept(token_kind k) { + if (is(k)) { + next(); + return true; + } + return false; + } + + void expect(token_kind k, char const* msg) { + if (!accept(k)) { + std::ostringstream out; + out << "expected " << msg << " at " << loc(); + throw parse_error(out.str()); + } + } + + std::string parse_name() { + if (is(token_kind::id) || is(token_kind::str)) { + std::string r = m_curr.text; + next(); + return r; + } + std::ostringstream out; + out << "expected identifier at " << loc(); + throw parse_error(out.str()); + } + + z3::sort get_sort(std::string const& n) { + if (n == "$i") return m_univ; + if (n == "$o") return m_ctx.bool_sort(); + if (n == "$int") return m_ctx.int_sort(); + if (n == "$real") return m_ctx.real_sort(); + auto it = m_sorts.find(n); + if (it != m_sorts.end()) return it->second; + z3::sort s = m_ctx.uninterpreted_sort(n.c_str()); + m_sorts.emplace(n, s); + return s; + } + + bool is_ttype(z3::sort const& s) const { + return std::string(s.name().str()) == "$tType"; + } + + z3::func_decl mk_decl(std::string const& name, unsigned arity, bool pred) { + std::string key = name + "/" + std::to_string(arity) + "/" + (pred ? "p" : "f"); + auto itd = m_decls.find(key); + if (itd != m_decls.end()) return itd->second; + + auto itt = m_typed_decls.find(name + "/" + std::to_string(arity)); + if (itt != m_typed_decls.end()) { + auto const& sig = itt->second; + z3::sort_vector dom(m_ctx); + for (z3::sort const& s : sig.first) dom.push_back(s); + z3::func_decl f = m_ctx.function(name.c_str(), dom, sig.second); + m_decls.emplace(key, f); + return f; + } + + std::vector dom(arity, m_univ); + if (pred) { + z3::func_decl f = m_ctx.function(name.c_str(), arity, dom.data(), m_ctx.bool_sort()); + m_decls.emplace(key, f); + return f; + } + z3::func_decl f = m_ctx.function(name.c_str(), arity, dom.data(), m_univ); + m_decls.emplace(key, f); + return f; + } + + bool find_bound(std::string const& n, z3::expr& e) const { + for (auto it = m_bound.rbegin(); it != m_bound.rend(); ++it) { + auto jt = it->find(n); + if (jt != it->end()) { + e = jt->second; + return true; + } + } + return false; + } + + z3::expr mk_quantifier(bool is_forall, z3::expr_vector const& bound, z3::expr const& body) { + if (bound.empty()) return body; + std::vector vars(bound.size()); + for (unsigned i = 0; i < bound.size(); ++i) vars[i] = (Z3_app)(Z3_ast)bound[i]; + Z3_ast q = Z3_mk_quantifier_const(m_ctx, is_forall, 1, bound.size(), vars.data(), 0, nullptr, body); + return z3::expr(m_ctx, q); + } + + parsed_type parse_type_atom() { + if (accept(token_kind::lparen)) { + parsed_type t = parse_type_expr(); + expect(token_kind::rparen, "')'"); + return t; + } + std::string n = parse_name(); + return parsed_type(get_sort(n)); + } + + std::vector parse_type_product() { + parsed_type first = parse_type_atom(); + if (!first.domain.empty()) + throw parse_error("higher-order type in product is unsupported"); + std::vector args; + args.push_back(first.range); + while (accept(token_kind::star_tok)) { + parsed_type t = parse_type_atom(); + if (!t.domain.empty()) + throw parse_error("higher-order type in product is unsupported"); + args.push_back(t.range); + } + return args; + } + + parsed_type parse_type_expr() { + std::vector prod = parse_type_product(); + if (accept(token_kind::gt_tok)) { + parsed_type rhs = parse_type_expr(); + if (!rhs.domain.empty()) + throw parse_error("higher-order result type is unsupported"); + return parsed_type(prod, rhs.range); + } + if (prod.size() != 1) + throw parse_error("type product must be followed by '>'"); + return parsed_type(prod[0]); + } + + void skip_annotations_until_rparen() { + int depth = 0; + while (!is(token_kind::eof_tok)) { + if (accept(token_kind::lparen) || accept(token_kind::lbrack)) { + ++depth; + continue; + } + if (is(token_kind::rparen) || is(token_kind::rbrack)) { + if (depth == 0) return; + --depth; + next(); + continue; + } + next(); + } + } + + z3::expr parse_term(); + + z3::expr parse_term_primary() { + if (accept(token_kind::lparen)) { + z3::expr e = parse_term(); + expect(token_kind::rparen, "')'"); + return e; + } + std::string n = parse_name(); + if (n == "$true") return m_ctx.bool_val(true); + if (n == "$false") return m_ctx.bool_val(false); + + z3::expr b(m_ctx); + if (is_var_name(n) && find_bound(n, b)) + return b; + + std::vector args; + if (accept(token_kind::lparen)) { + if (!accept(token_kind::rparen)) { + do { args.push_back(parse_term()); } while (accept(token_kind::comma)); + expect(token_kind::rparen, "')'"); + } + } + z3::func_decl f = mk_decl(n, static_cast(args.size()), false); + if (args.empty()) return f(); + std::vector tmp(args.begin(), args.end()); + return f(static_cast(tmp.size()), tmp.data()); + } + + z3::expr parse_term() { + z3::expr e = parse_term_primary(); + while (accept(token_kind::at_tok)) { + z3::expr arg = parse_term_primary(); + if (!e.is_app() || e.decl().decl_kind() != Z3_OP_UNINTERPRETED) + throw parse_error("higher-order application is unsupported"); + z3::func_decl f = e.decl(); + std::vector args; + for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i)); + args.push_back(arg); + e = f(static_cast(args.size()), args.data()); + } + return e; + } + + z3::expr parse_formula(); + + z3::expr parse_atomic_formula() { + if (accept(token_kind::lparen)) { + z3::expr e = parse_formula(); + expect(token_kind::rparen, "')'"); + return e; + } + + std::string n = parse_name(); + if (n == "$true") return m_ctx.bool_val(true); + if (n == "$false") return m_ctx.bool_val(false); + + std::vector args; + if (accept(token_kind::lparen)) { + if (!accept(token_kind::rparen)) { + do { args.push_back(parse_term()); } while (accept(token_kind::comma)); + expect(token_kind::rparen, "')'"); + } + } + + z3::expr lhs(m_ctx); + bool has_lhs = false; + if (args.empty()) { + z3::expr b(m_ctx); + if (is_var_name(n) && find_bound(n, b)) { + lhs = b; + has_lhs = true; + } + } + if (!has_lhs) { + lhs = args.empty() ? mk_decl(n, 0, false)() : mk_decl(n, static_cast(args.size()), false)(static_cast(args.size()), args.data()); + } + + if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) { + bool neq = accept(token_kind::neq_tok); + if (!neq) expect(token_kind::equal_tok, "'='"); + z3::expr rhs = parse_term(); + return neq ? !(lhs == rhs) : (lhs == rhs); + } + + if (lhs.is_bool()) return lhs; + + z3::func_decl p = mk_decl(n, static_cast(args.size()), true); + if (args.empty()) return p(); + return p(static_cast(args.size()), args.data()); + } + + z3::expr parse_unary_formula() { + if (accept(token_kind::not_tok)) return !parse_unary_formula(); + if (is(token_kind::forall_tok) || is(token_kind::exists_tok)) { + bool is_forall = is(token_kind::forall_tok); + next(); + expect(token_kind::lbrack, "'['"); + + z3::expr_vector vars(m_ctx); + std::unordered_map scope; + if (!accept(token_kind::rbrack)) { + do { + std::string v = parse_name(); + z3::sort s = m_univ; + if (accept(token_kind::colon)) { + parsed_type t = parse_type_expr(); + if (!t.domain.empty()) + throw parse_error("higher-order variable type is unsupported"); + s = t.range; + } + z3::expr c = m_ctx.constant(v.c_str(), s); + vars.push_back(c); + scope.emplace(v, c); + } while (accept(token_kind::comma)); + expect(token_kind::rbrack, "']'"); + } + expect(token_kind::colon, "':'"); + m_bound.push_back(scope); + z3::expr body = parse_formula(); + m_bound.pop_back(); + return mk_quantifier(is_forall, vars, body); + } + return parse_atomic_formula(); + } + + z3::expr parse_and_formula() { + z3::expr e = parse_unary_formula(); + while (is(token_kind::and_tok) || is(token_kind::nand_tok)) { + bool is_nand = accept(token_kind::nand_tok); + if (!is_nand) expect(token_kind::and_tok, "'&'"); + z3::expr rhs = parse_unary_formula(); + e = is_nand ? !(e && rhs) : (e && rhs); + } + return e; + } + + z3::expr parse_or_formula() { + z3::expr e = parse_and_formula(); + while (is(token_kind::or_tok) || is(token_kind::nor_tok)) { + bool is_nor = accept(token_kind::nor_tok); + if (!is_nor) expect(token_kind::or_tok, "'|'"); + z3::expr rhs = parse_and_formula(); + e = is_nor ? !(e || rhs) : (e || rhs); + } + return e; + } + + z3::expr parse_implies_formula() { + z3::expr e = parse_or_formula(); + if (accept(token_kind::implies_tok)) { + z3::expr rhs = parse_implies_formula(); + return implies(e, rhs); + } + if (accept(token_kind::implied_tok)) { + z3::expr rhs = parse_implies_formula(); + return implies(rhs, e); + } + return e; + } + + z3::expr parse_formula() { + z3::expr e = parse_implies_formula(); + while (is(token_kind::iff_tok) || is(token_kind::xor_tok)) { + bool is_xor = accept(token_kind::xor_tok); + if (!is_xor) expect(token_kind::iff_tok, "'<=>'"); + z3::expr rhs = parse_implies_formula(); + e = is_xor ? !(e == rhs) : (e == rhs); + } + return e; + } + + void parse_type_decl_formula() { + while (accept(token_kind::lparen)) {} + std::string name = parse_name(); + expect(token_kind::colon, "':'"); + parsed_type t = parse_type_expr(); + while (accept(token_kind::rparen)) {} + + if (t.domain.empty() && is_ttype(t.range)) { + m_sorts.insert_or_assign(name, m_ctx.uninterpreted_sort(name.c_str())); + return; + } + m_typed_decls.insert_or_assign(name + "/" + std::to_string(t.domain.size()), std::make_pair(t.domain, t.range)); + } + + static bool file_exists(std::string const& f) { + std::ifstream in(f); + return !in.fail(); + } + + std::string dirname(std::string const& f) const { + size_t idx = f.find_last_of("/\\"); + return idx == std::string::npos ? "." : f.substr(0, idx); + } + + std::string resolve_include(std::string const& curr_file, std::string const& name) const { + if (!name.empty() && (name[0] == '/' || (name.size() > 2 && std::isalpha(static_cast(name[0])) && name[1] == ':'))) + return name; + std::string local = dirname(curr_file) + "/" + name; + if (file_exists(local)) return local; + char const* root = std::getenv("TPTP"); + if (root) { + std::string env = std::string(root) + "/" + name; + if (file_exists(env)) return env; + } + return local; + } + + void parse_include(std::string const& curr_file) { + expect(token_kind::lparen, "'('"); + std::string file = parse_name(); + if (accept(token_kind::comma)) { + if (accept(token_kind::lbrack)) { + int depth = 1; + while (depth > 0 && !is(token_kind::eof_tok)) { + if (accept(token_kind::lbrack)) ++depth; + else if (accept(token_kind::rbrack)) --depth; + else next(); + } + } + else { + skip_annotations_until_rparen(); + } + } + expect(token_kind::rparen, "')'"); + expect(token_kind::dot, "'.'"); + parse_file(resolve_include(curr_file, file)); + } + + void parse_annotated(std::string const& kind) { + expect(token_kind::lparen, "'('"); + parse_name(); + expect(token_kind::comma, "','"); + std::string role = to_lower(parse_name()); + expect(token_kind::comma, "','"); + + if (role == "type") { + parse_type_decl_formula(); + } + else { + z3::expr f = parse_formula(); + if (role == "conjecture") { + m_has_conjecture = true; + f = !f; + } + m_solver.add(f); + } + + if (accept(token_kind::comma)) { + skip_annotations_until_rparen(); + } + expect(token_kind::rparen, "')'"); + expect(token_kind::dot, "'.'"); + + if (kind == "thf") { + // THF parsing is supported for first-order compatible fragments only. + } + } + + void parse_toplevel(std::string const& current_file) { + while (!is(token_kind::eof_tok)) { + std::string kw = to_lower(parse_name()); + if (kw == "include") { + parse_include(current_file); + } + else if (kw == "fof" || kw == "cnf" || kw == "tff" || kw == "thf") { + parse_annotated(kw); + } + else { + std::ostringstream out; + out << "unsupported TPTP unit '" << kw << "' at " << loc(); + throw parse_error(out.str()); + } + } + } + +public: + tptp_parser(z3::context& ctx, z3::solver& solver): + m_ctx(ctx), + m_solver(solver), + m_univ(ctx.uninterpreted_sort("U")) { + m_sorts.emplace("$tType", ctx.uninterpreted_sort("$tType")); + m_sorts.emplace("$i", m_univ); + m_sorts.emplace("$o", m_ctx.bool_sort()); + m_sorts.emplace("$int", m_ctx.int_sort()); + m_sorts.emplace("$real", m_ctx.real_sort()); + } + + void parse_file(std::string const& filename) { + if (!m_seen_files.insert(filename).second) return; + std::ifstream in(filename); + if (in.fail()) { + std::ostringstream out; + 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(m_input); + next(); + m_file_stack.push_back(filename); + parse_toplevel(filename); + m_file_stack.pop_back(); + } + + void parse_stream(std::istream& in) { + std::ostringstream buf; + buf << in.rdbuf(); + m_input = buf.str(); + m_lex = std::make_unique(m_input); + next(); + parse_toplevel("."); + } + + bool has_conjecture() const { return m_has_conjecture; } +}; + +} + +unsigned read_tptp(char const* file_name) { + try { + z3::context ctx; + z3::solver solver(ctx); + tptp_parser p(ctx, solver); + if (file_name) p.parse_file(file_name); + else p.parse_stream(std::cin); + + z3::check_result r = solver.check(); + if (r == z3::unsat) { + if (p.has_conjecture()) std::cout << "% SZS status Theorem\n"; + else std::cout << "% SZS status Unsatisfiable\n"; + } + else if (r == z3::sat) { + if (p.has_conjecture()) std::cout << "% SZS status CounterSatisfiable\n"; + else std::cout << "% SZS status Satisfiable\n"; + if (g_display_model) std::cout << solver.get_model() << "\n"; + } + else { + std::cout << "% SZS status GaveUp\n"; + std::string reason = solver.reason_unknown(); + if (!reason.empty()) std::cout << "% SZS reason " << reason << "\n"; + } + if (g_display_statistics) std::cout << solver.statistics() << "\n"; + return 0; + } + catch (parse_error const& ex) { + std::cerr << "TPTP parse error: " << ex.what() << "\n"; + return ERR_PARSER; + } + catch (z3::exception const& ex) { + std::cerr << "TPTP frontend error: " << ex.msg() << "\n"; + return ERR_INTERNAL_FATAL; + } +} diff --git a/src/shell/tptp_frontend.h b/src/shell/tptp_frontend.h new file mode 100644 index 000000000..7600b37e7 --- /dev/null +++ b/src/shell/tptp_frontend.h @@ -0,0 +1,3 @@ +#pragma once + +unsigned read_tptp(char const* file_name);