mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-21 09:29:35 +00:00
Code Activity

Fix TPTP frontend build integration and validate with tests

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-08 17:22:02 +00:00 • committed by GitHub
parent 50fb4d5ac6
commit fce83df3fc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 28 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_project.py
View file

@ -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'] 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('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'euf', 'arith_tactics'], 'cmd_context/extra_cmds')
add_lib('api', ['portfolio', 'realclosure', 'opt', 'extra_cmds'], add_lib('api', ['portfolio', 'realclosure', 'opt', 'extra_cmds'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h', 'c++/z3++.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds', 'opt'], exe_name='z3') 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) 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', _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
@ -125,5 +125,3 @@ def init_project_def():
add_ml_example('ml_example', 'ml') add_ml_example('ml_example', 'ml')
add_z3py_example('py_example', 'python') add_z3py_example('py_example', 'python')
return API_files return API_files

54
src/shell/tptp_frontend.cpp
View file

@ -9,7 +9,7 @@
#include <memory> #include <memory>
#include <vector> #include <vector>
#include "api/c++/z3++.h" #include <api/c++/z3++.h>
#include "shell/tptp_frontend.h" #include "shell/tptp_frontend.h"
#include "util/error_codes.h" #include "util/error_codes.h"
@ -442,21 +442,6 @@ class tptp_parser {
return f(static_cast<unsigned>(tmp.size()), tmp.data()); return f(static_cast<unsigned>(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<z3::expr> args;
for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i));
args.push_back(arg);
e = f(static_cast<unsigned>(args.size()), args.data());
}
return e;
}
z3::expr parse_formula(); z3::expr parse_formula();
z3::expr parse_atomic_formula() { z3::expr parse_atomic_formula() {
@ -574,17 +559,6 @@ class tptp_parser {
return 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() { void parse_type_decl_formula() {
while (accept(token_kind::lparen)) {} while (accept(token_kind::lparen)) {}
std::string name = parse_name(); std::string name = parse_name();
@ -732,6 +706,32 @@ public:
bool has_conjecture() const { return m_has_conjecture; } bool has_conjecture() const { return m_has_conjecture; }
}; };
z3::expr tptp_parser::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<z3::expr> args;
for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i));
args.push_back(arg);
e = f(static_cast<unsigned>(args.size()), args.data());
}
return e;
}
z3::expr tptp_parser::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;
}
} }
unsigned read_tptp(char const* file_name) { unsigned read_tptp(char const* file_name) {