Address review feedback and clean up TPTP/frontend readability

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ba80bc5a-d80f-4d9f-8ed4-a962f697697c

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

scripts/mk_project.py

@@ -98,7 +98,7 @@ def init_project_def():
     API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_fpa.h', 'z3_spacer.h']
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('api', ['portfolio',  'realclosure', 'opt', 'extra_cmds'],
-            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h', 'c++/z3++.h'] + API_files)
+            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing', 'simplex', 'sat_smt'], exe_name='test-z3', install=False)
     _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',

src/shell/main.cpp

@@ -132,6 +132,15 @@ static bool validate_is_ulong(char const* s) {
             return false;
     return true;
 }
+
+static bool is_tptp_extension(char const* ext) {
+    static char const* exts[] = {"p", "tptp", "fof", "cnf", "tff", "thf"};
+    for (char const* e : exts) {
+        if (strcmp(ext, e) == 0)
+            return true;
+    }
+    return false;
+}
    
 static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) {
     long timeout = 0;
@@ -392,7 +401,7 @@ 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) {
+                else if (is_tptp_extension(ext)) {
                     g_input_kind = IN_TPTP;
                 }
             }

src/shell/tptp_frontend.cpp

@@ -83,8 +83,8 @@ class lexer {
         return c;
     }
 
-    static bool is_id_start(char c) {
+    static bool is_symbol_start(char c) {
-        return std::isalpha(static_cast<unsigned char>(c)) || c == '$' || c == '_' || std::isdigit(static_cast<unsigned char>(c));
+        return std::isalnum(static_cast<unsigned char>(c)) || c == '$' || c == '_';
     }
 
     static bool is_id_char(char c) {
@@ -212,7 +212,7 @@ public:
             break;
         }
 
-        if (is_id_start(c)) {
+        if (is_symbol_start(c)) {
             t.kind = token_kind::id;
             t.text.push_back(c);
             while (!eof() && is_id_char(peek()))
@@ -266,6 +266,14 @@ class tptp_parser {
         return out.str();
     }
 
+    void skip_wrapping_lparens() {
+        while (accept(token_kind::lparen)) {}
+    }
+
+    void skip_wrapping_rparens() {
+        while (accept(token_kind::rparen)) {}
+    }
+
     void next() { m_curr = m_lex->next(); }
 
     bool is(token_kind k) const { return m_curr.kind == k; }
@@ -310,7 +318,7 @@ class tptp_parser {
     }
 
     bool is_ttype(z3::sort const& s) const {
-        return std::string(s.name().str()) == "$tType";
+        return std::string(Z3_get_symbol_string(m_ctx, Z3_get_sort_name(m_ctx, s))) == "$tType";
     }
 
     z3::func_decl mk_decl(std::string const& name, unsigned arity, bool pred) {
@@ -473,7 +481,8 @@ class tptp_parser {
             }
         }
         if (!has_lhs) {
-            lhs = args.empty() ? mk_decl(n, 0, false)() : mk_decl(n, static_cast<unsigned>(args.size()), false)(static_cast<unsigned>(args.size()), args.data());
+            z3::func_decl f = mk_decl(n, static_cast<unsigned>(args.size()), false);
+            lhs = args.empty() ? f() : f(static_cast<unsigned>(args.size()), args.data());
         }
 
         if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) {
@@ -560,11 +569,11 @@ class tptp_parser {
     }
 
     void parse_type_decl_formula() {
-        while (accept(token_kind::lparen)) {}
+        skip_wrapping_lparens();
         std::string name = parse_name();
         expect(token_kind::colon, "':'");
         parsed_type t = parse_type_expr();
-        while (accept(token_kind::rparen)) {}
+        skip_wrapping_rparens();
 
         if (t.domain.empty() && is_ttype(t.range)) {
             m_sorts.insert_or_assign(name, m_ctx.uninterpreted_sort(name.c_str()));
@@ -578,13 +587,19 @@ class tptp_parser {
         return !in.fail();
     }
 
+    static bool is_absolute_path(std::string const& name) {
+        return !name.empty() &&
+            (name[0] == '/' ||
+             (name.size() > 2 && std::isalpha(static_cast<unsigned char>(name[0])) && name[1] == ':'));
+    }
+
     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<unsigned char>(name[0])) && name[1] == ':')))
+        if (is_absolute_path(name))
             return name;
         std::string local = dirname(curr_file) + "/" + name;
         if (file_exists(local)) return local;