mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 07:07:52 +00:00
Code Activity

Use internal AST/cmd_context APIs in TPTP shell frontend

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2a6b01d0-c799-4e44-aa73-ef228cb4402e

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-10 15:17:40 +00:00 • committed by GitHub
parent f8ad15e38a
commit e36d3936cb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 161 additions and 142 deletions
Download patch file Download diff file Expand all files Collapse all files

303
src/shell/tptp_frontend.cpp
View file

@ -2,16 +2,21 @@
#include <cstdlib> #include <cstdlib>
#include <fstream> #include <fstream>
#include <iostream> #include <iostream>
#include <memory>
#include <sstream> #include <sstream>
#include <string> #include <string>
#include <unordered_map> #include <unordered_map>
#include <unordered_set> #include <unordered_set>
#include <memory>
#include <vector> #include <vector>
#include <api/c++/z3++.h> #include "ast/arith_decl_plugin.h"
#include "ast/expr_abstract.h"
#include "ast/ast_util.h"
#include "cmd_context/cmd_context.h"
#include "shell/tptp_frontend.h" #include "shell/tptp_frontend.h"
#include "smt/smt_solver.h"
#include "util/error_codes.h" #include "util/error_codes.h"
#include "util/z3_exception.h"
extern bool g_display_statistics; extern bool g_display_statistics;
extern bool g_display_model; extern bool g_display_model;
@ -50,7 +55,7 @@ enum class token_kind {
struct parse_error : public std::exception { struct parse_error : public std::exception {
std::string m_msg; std::string m_msg;
parse_error(std::string const& msg): m_msg(msg) {} parse_error(std::string const& msg): m_msg(msg) {}
const char* what() const noexcept override { return m_msg.c_str(); } char const* what() const noexcept override { return m_msg.c_str(); }
}; };
struct token { struct token {
@ -227,27 +232,27 @@ public:
}; };
struct parsed_type { struct parsed_type {
std::vector<z3::sort> domain; std::vector<sort*> domain;
z3::sort range; sort* range = nullptr;
parsed_type(z3::sort const& s): range(s) {} parsed_type(sort* s): range(s) {}
parsed_type(std::vector<z3::sort> const& d, z3::sort const& r): domain(d), range(r) {} parsed_type(std::vector<sort*> const& d, sort* r): domain(d), range(r) {}
}; };
class tptp_parser { class tptp_parser {
z3::context& m_ctx; cmd_context& m_cmd;
z3::solver& m_solver; ast_manager& m;
z3::sort m_univ; arith_util m_arith;
sort* m_univ;
bool m_has_conjecture = false; bool m_has_conjecture = false;
std::unordered_map<std::string, z3::sort> m_sorts; std::unordered_map<std::string, sort*> m_sorts;
std::unordered_map<std::string, z3::func_decl> m_decls; std::unordered_map<std::string, func_decl*> m_decls;
std::unordered_map<std::string, std::pair<std::vector<z3::sort>, z3::sort>> m_typed_decls; std::unordered_map<std::string, std::pair<std::vector<sort*>, sort*>> m_typed_decls;
std::vector<std::unordered_map<std::string, z3::expr>> m_bound; std::vector<std::unordered_map<std::string, app*>> m_bound;
std::unordered_set<std::string> m_seen_files; std::unordered_set<std::string> m_seen_files;
std::string m_input; std::string m_input;
std::unique_ptr<lexer> m_lex; std::unique_ptr<lexer> m_lex;
token m_curr; token m_curr;
std::vector<std::string> m_file_stack;
static std::string to_lower(std::string s) { static std::string to_lower(std::string s) {
for (char& c : s) c = static_cast<char>(std::tolower(static_cast<unsigned char>(c))); for (char& c : s) c = static_cast<char>(std::tolower(static_cast<unsigned char>(c)));
@ -305,20 +310,20 @@ class tptp_parser {
throw parse_error(out.str()); throw parse_error(out.str());
} }
z3::sort get_sort(std::string const& n) { sort* get_sort(std::string const& n) {
if (n == "$i") return m_univ; if (n == "$i") return m_univ;
if (n == "$o") return m_ctx.bool_sort(); if (n == "$o") return m.mk_bool_sort();
if (n == "$int") return m_ctx.int_sort(); if (n == "$int") return m_arith.mk_int();
if (n == "$real") return m_ctx.real_sort(); if (n == "$real") return m_arith.mk_real();
auto it = m_sorts.find(n); auto it = m_sorts.find(n);
if (it != m_sorts.end()) return it->second; if (it != m_sorts.end()) return it->second;
z3::sort s = m_ctx.uninterpreted_sort(n.c_str()); sort* s = m.mk_uninterpreted_sort(symbol(n));
m_sorts.emplace(n, s); m_sorts.emplace(n, s);
return s; return s;
} }
bool is_ttype(z3::sort const& s) const { static bool is_ttype(sort* s) {
return std::string(Z3_get_symbol_string(m_ctx, Z3_get_sort_name(m_ctx, s))) == "$tType"; return s->get_name() == symbol("$tType");
} }
static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) { static std::string mk_decl_key(std::string const& name, unsigned arity, char tag) {
@ -329,16 +334,14 @@ class tptp_parser {
return mk_decl_key(name, arity, 't'); return mk_decl_key(name, arity, 't');
} }
z3::func_decl mk_decl(std::string const& name, unsigned arity, bool pred) { func_decl* mk_decl(std::string const& name, unsigned arity, bool pred) {
auto itt = m_typed_decls.find(mk_typed_key(name, arity)); auto itt = m_typed_decls.find(mk_typed_key(name, arity));
if (itt != m_typed_decls.end()) { if (itt != m_typed_decls.end()) {
std::string typed_decl_key = mk_decl_key(name, arity, 'd'); std::string typed_decl_key = mk_decl_key(name, arity, 'd');
auto itd = m_decls.find(typed_decl_key); auto itd = m_decls.find(typed_decl_key);
if (itd != m_decls.end()) return itd->second; if (itd != m_decls.end()) return itd->second;
auto const& sig = itt->second; auto const& sig = itt->second;
z3::sort_vector dom(m_ctx); func_decl* f = m.mk_func_decl(symbol(name), sig.first.size(), sig.first.data(), sig.second);
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(typed_decl_key, f); m_decls.emplace(typed_decl_key, f);
return f; return f;
} }
@ -347,18 +350,13 @@ class tptp_parser {
auto itd = m_decls.find(key); auto itd = m_decls.find(key);
if (itd != m_decls.end()) return itd->second; if (itd != m_decls.end()) return itd->second;
std::vector<z3::sort> dom(arity, m_univ); std::vector<sort*> dom(arity, m_univ);
if (pred) { func_decl* f = m.mk_func_decl(symbol(name), arity, dom.data(), pred ? m.mk_bool_sort() : m_univ);
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); m_decls.emplace(key, f);
return f; return f;
} }
bool find_bound(std::string const& n, z3::expr& e) const { bool find_bound(std::string const& n, expr_ref& e) const {
for (auto it = m_bound.rbegin(); it != m_bound.rend(); ++it) { for (auto it = m_bound.rbegin(); it != m_bound.rend(); ++it) {
auto jt = it->find(n); auto jt = it->find(n);
if (jt != it->end()) { if (jt != it->end()) {
@ -369,12 +367,9 @@ class tptp_parser {
return false; return false;
} }
z3::expr mk_quantifier(bool is_forall, z3::expr_vector const& bound, z3::expr const& body) { expr_ref mk_quantifier(bool is_forall, ptr_vector<app> const& bound, expr* body) {
if (bound.empty()) return body; if (bound.empty()) return expr_ref(body, m);
std::vector<Z3_app> vars(bound.size()); return is_forall ? ::mk_forall(m, bound.size(), bound.data(), body) : ::mk_exists(m, bound.size(), bound.data(), body);
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, 0, bound.size(), vars.data(), 0, nullptr, body);
return z3::expr(m_ctx, q);
} }
parsed_type parse_type_atom() { parsed_type parse_type_atom() {
@ -387,11 +382,11 @@ class tptp_parser {
return parsed_type(get_sort(n)); return parsed_type(get_sort(n));
} }
std::vector<z3::sort> parse_type_product() { std::vector<sort*> parse_type_product() {
parsed_type first = parse_type_atom(); parsed_type first = parse_type_atom();
if (!first.domain.empty()) if (!first.domain.empty())
throw parse_error("higher-order type in product is unsupported"); throw parse_error("higher-order type in product is unsupported");
std::vector<z3::sort> args; std::vector<sort*> args;
args.push_back(first.range); args.push_back(first.range);
while (accept(token_kind::star_tok)) { while (accept(token_kind::star_tok)) {
parsed_type t = parse_type_atom(); parsed_type t = parse_type_atom();
@ -403,7 +398,7 @@ class tptp_parser {
} }
parsed_type parse_type_expr() { parsed_type parse_type_expr() {
std::vector<z3::sort> prod = parse_type_product(); std::vector<sort*> prod = parse_type_product();
if (accept(token_kind::gt_tok)) { if (accept(token_kind::gt_tok)) {
parsed_type rhs = parse_type_expr(); parsed_type rhs = parse_type_expr();
if (!rhs.domain.empty()) if (!rhs.domain.empty())
@ -441,49 +436,48 @@ class tptp_parser {
} }
} }
z3::expr parse_term(); expr_ref parse_term();
z3::expr parse_term_primary() { expr_ref parse_term_primary() {
if (accept(token_kind::lparen)) { if (accept(token_kind::lparen)) {
z3::expr e = parse_term(); expr_ref e = parse_term();
expect(token_kind::rparen, "')'"); expect(token_kind::rparen, "')'");
return e; return e;
} }
std::string n = parse_name(); std::string n = parse_name();
if (n == "$true") return m_ctx.bool_val(true); if (n == "$true") return expr_ref(m.mk_true(), m);
if (n == "$false") return m_ctx.bool_val(false); if (n == "$false") return expr_ref(m.mk_false(), m);
z3::expr b(m_ctx); expr_ref b(m);
if (is_var_name(n) && find_bound(n, b)) if (is_var_name(n) && find_bound(n, b))
return b; return b;
std::vector<z3::expr> args; expr_ref_vector args(m);
if (accept(token_kind::lparen)) { if (accept(token_kind::lparen)) {
if (!accept(token_kind::rparen)) { if (!accept(token_kind::rparen)) {
do { args.push_back(parse_term()); } while (accept(token_kind::comma)); do { args.push_back(parse_term()); } while (accept(token_kind::comma));
expect(token_kind::rparen, "')'"); expect(token_kind::rparen, "')'");
} }
} }
z3::func_decl f = mk_decl(n, static_cast<unsigned>(args.size()), false);
if (args.empty()) return f(); func_decl* f = mk_decl(n, args.size(), false);
std::vector<z3::expr> tmp(args.begin(), args.end()); return expr_ref(args.empty() ? m.mk_const(f) : m.mk_app(f, args.size(), args.data()), m);
return f(static_cast<unsigned>(tmp.size()), tmp.data());
} }
z3::expr parse_formula(); expr_ref parse_formula();
z3::expr parse_atomic_formula() { expr_ref parse_atomic_formula() {
if (accept(token_kind::lparen)) { if (accept(token_kind::lparen)) {
z3::expr e = parse_formula(); expr_ref e = parse_formula();
expect(token_kind::rparen, "')'"); expect(token_kind::rparen, "')'");
return e; return e;
} }
std::string n = parse_name(); std::string n = parse_name();
if (n == "$true") return m_ctx.bool_val(true); if (n == "$true") return expr_ref(m.mk_true(), m);
if (n == "$false") return m_ctx.bool_val(false); if (n == "$false") return expr_ref(m.mk_false(), m);
std::vector<z3::expr> args; expr_ref_vector args(m);
if (accept(token_kind::lparen)) { if (accept(token_kind::lparen)) {
if (!accept(token_kind::rparen)) { if (!accept(token_kind::rparen)) {
do { args.push_back(parse_term()); } while (accept(token_kind::comma)); do { args.push_back(parse_term()); } while (accept(token_kind::comma));
@ -491,110 +485,119 @@ class tptp_parser {
} }
} }
z3::expr lhs(m_ctx); expr_ref lhs(m);
bool has_lhs = false; bool has_lhs = false;
if (args.empty()) { if (args.empty()) {
z3::expr b(m_ctx); expr_ref b(m);
if (is_var_name(n) && find_bound(n, b)) { if (is_var_name(n) && find_bound(n, b)) {
lhs = b; lhs = b;
has_lhs = true; has_lhs = true;
} }
} }
if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) { if (is(token_kind::equal_tok) || is(token_kind::neq_tok)) {
if (!has_lhs) { if (!has_lhs) {
z3::func_decl f = mk_decl(n, static_cast<unsigned>(args.size()), false); func_decl* f = mk_decl(n, args.size(), false);
lhs = args.empty() ? f() : f(static_cast<unsigned>(args.size()), args.data()); lhs = args.empty() ? m.mk_const(f) : m.mk_app(f, args.size(), args.data());
} }
bool neq = accept(token_kind::neq_tok); bool neq = accept(token_kind::neq_tok);
if (!neq) expect(token_kind::equal_tok, "'='"); if (!neq) expect(token_kind::equal_tok, "'='");
z3::expr rhs = parse_term(); expr_ref rhs = parse_term();
return neq ? !(lhs == rhs) : (lhs == rhs); expr_ref eq(m.mk_eq(lhs, rhs), m);
return neq ? expr_ref(m.mk_not(eq), m) : eq;
} }
if (has_lhs) { if (has_lhs) {
if (lhs.is_bool()) return lhs; if (m.is_bool(lhs)) return lhs;
throw parse_error("non-boolean variable used as formula"); throw parse_error("non-boolean variable used as formula");
} }
auto typed = m_typed_decls.find(mk_typed_key(n, static_cast<unsigned>(args.size()))); auto typed = m_typed_decls.find(mk_typed_key(n, args.size()));
if (typed != m_typed_decls.end()) { if (typed != m_typed_decls.end()) {
z3::func_decl f = mk_decl(n, static_cast<unsigned>(args.size()), false); func_decl* f = mk_decl(n, args.size(), false);
z3::expr e = args.empty() ? f() : f(static_cast<unsigned>(args.size()), args.data()); expr_ref e(args.empty() ? m.mk_const(f) : m.mk_app(f, args.size(), args.data()), m);
if (!e.is_bool()) if (!m.is_bool(e))
throw parse_error("typed non-boolean term used as formula"); throw parse_error("typed non-boolean term used as formula");
return e; return e;
} }
z3::func_decl pred = mk_decl(n, static_cast<unsigned>(args.size()), true); func_decl* pred = mk_decl(n, args.size(), true);
if (args.empty()) return pred(); return expr_ref(args.empty() ? m.mk_const(pred) : m.mk_app(pred, args.size(), args.data()), m);
return pred(static_cast<unsigned>(args.size()), args.data());
} }
z3::expr parse_unary_formula() { expr_ref parse_unary_formula() {
if (accept(token_kind::not_tok)) return !parse_unary_formula(); if (accept(token_kind::not_tok)) {
expr_ref e = parse_unary_formula();
return expr_ref(m.mk_not(e), m);
}
if (is(token_kind::forall_tok) || is(token_kind::exists_tok)) { if (is(token_kind::forall_tok) || is(token_kind::exists_tok)) {
bool is_forall = is(token_kind::forall_tok); bool is_forall = is(token_kind::forall_tok);
next(); next();
expect(token_kind::lbrack, "'['"); expect(token_kind::lbrack, "'['");
z3::expr_vector vars(m_ctx); ptr_vector<app> vars;
std::unordered_map<std::string, z3::expr> scope; std::unordered_map<std::string, app*> scope;
if (!accept(token_kind::rbrack)) { if (!accept(token_kind::rbrack)) {
do { do {
std::string v = parse_name(); std::string v = parse_name();
z3::sort s = m_univ; sort* s = m_univ;
if (accept(token_kind::colon)) { if (accept(token_kind::colon)) {
parsed_type t = parse_type_expr(); parsed_type t = parse_type_expr();
if (!t.domain.empty()) if (!t.domain.empty())
throw parse_error("higher-order variable type is unsupported"); throw parse_error("higher-order variable type is unsupported");
s = t.range; s = t.range;
} }
z3::expr c = m_ctx.constant(v.c_str(), s); app* c = m.mk_const(symbol(v), s);
vars.push_back(c); vars.push_back(c);
scope.emplace(v, c); scope.emplace(v, c);
} while (accept(token_kind::comma)); }
while (accept(token_kind::comma));
expect(token_kind::rbrack, "']'"); expect(token_kind::rbrack, "']'");
} }
expect(token_kind::colon, "':'"); expect(token_kind::colon, "':'");
m_bound.push_back(scope); m_bound.push_back(scope);
z3::expr body = parse_formula(); expr_ref body = parse_formula();
m_bound.pop_back(); m_bound.pop_back();
return mk_quantifier(is_forall, vars, body); return mk_quantifier(is_forall, vars, body);
} }
return parse_atomic_formula(); return parse_atomic_formula();
} }
z3::expr parse_and_formula() { expr_ref parse_and_formula() {
z3::expr e = parse_unary_formula(); expr_ref e = parse_unary_formula();
while (is(token_kind::and_tok) || is(token_kind::nand_tok)) { while (is(token_kind::and_tok) || is(token_kind::nand_tok)) {
bool is_nand = accept(token_kind::nand_tok); bool is_nand = accept(token_kind::nand_tok);
if (!is_nand) expect(token_kind::and_tok, "'&'"); if (!is_nand) expect(token_kind::and_tok, "'&'");
z3::expr rhs = parse_unary_formula(); expr_ref rhs = parse_unary_formula();
e = is_nand ? !(e && rhs) : (e && rhs); expr_ref conj(::mk_and(m, e, rhs), m);
e = is_nand ? expr_ref(m.mk_not(conj), m) : conj;
} }
return e; return e;
} }
z3::expr parse_or_formula() { expr_ref parse_or_formula() {
z3::expr e = parse_and_formula(); expr_ref e = parse_and_formula();
while (is(token_kind::or_tok) || is(token_kind::nor_tok)) { while (is(token_kind::or_tok) || is(token_kind::nor_tok)) {
bool is_nor = accept(token_kind::nor_tok); bool is_nor = accept(token_kind::nor_tok);
if (!is_nor) expect(token_kind::or_tok, "'|'"); if (!is_nor) expect(token_kind::or_tok, "'|'");
z3::expr rhs = parse_and_formula(); expr_ref rhs = parse_and_formula();
e = is_nor ? !(e || rhs) : (e || rhs); expr_ref disj(::mk_or(m, e, rhs), m);
e = is_nor ? expr_ref(m.mk_not(disj), m) : disj;
} }
return e; return e;
} }
z3::expr parse_implies_formula() { expr_ref parse_implies_formula() {
z3::expr e = parse_or_formula(); expr_ref e = parse_or_formula();
if (accept(token_kind::implies_tok)) { if (accept(token_kind::implies_tok)) {
z3::expr rhs = parse_implies_formula(); expr_ref rhs = parse_implies_formula();
return implies(e, rhs); return expr_ref(m.mk_implies(e, rhs), m);
} }
if (accept(token_kind::implied_tok)) { if (accept(token_kind::implied_tok)) {
z3::expr rhs = parse_implies_formula(); expr_ref rhs = parse_implies_formula();
return implies(rhs, e); return expr_ref(m.mk_implies(rhs, e), m);
} }
return e; return e;
} }
@ -607,10 +610,11 @@ class tptp_parser {
skip_wrapping_rparens(); skip_wrapping_rparens();
if (t.domain.empty() && is_ttype(t.range)) { if (t.domain.empty() && is_ttype(t.range)) {
m_sorts.insert_or_assign(name, m_ctx.uninterpreted_sort(name.c_str())); m_sorts.insert_or_assign(name, m.mk_uninterpreted_sort(symbol(name)));
return; return;
} }
m_typed_decls.insert_or_assign(mk_typed_key(name, static_cast<unsigned>(t.domain.size())), std::make_pair(t.domain, t.range));
m_typed_decls.insert_or_assign(mk_typed_key(name, t.domain.size()), std::make_pair(t.domain, t.range));
} }
static bool file_exists(std::string const& f) { static bool file_exists(std::string const& f) {
@ -658,7 +662,7 @@ class tptp_parser {
parse_file(resolve_include(curr_file, file)); parse_file(resolve_include(curr_file, file));
} }
void parse_annotated(std::string const& kind) { void parse_annotated() {
expect(token_kind::lparen, "'('"); expect(token_kind::lparen, "'('");
parse_name(); parse_name();
expect(token_kind::comma, "','"); expect(token_kind::comma, "','");
@ -669,12 +673,12 @@ class tptp_parser {
parse_type_decl_formula(); parse_type_decl_formula();
} }
else { else {
z3::expr f = parse_formula(); expr_ref f = parse_formula();
if (role == "conjecture") { if (role == "conjecture") {
m_has_conjecture = true; m_has_conjecture = true;
f = !f; f = m.mk_not(f);
} }
m_solver.add(f); m_cmd.assert_expr(f);
} }
if (accept(token_kind::comma)) { if (accept(token_kind::comma)) {
@ -682,8 +686,6 @@ class tptp_parser {
} }
expect(token_kind::rparen, "')'"); expect(token_kind::rparen, "')'");
expect(token_kind::dot, "'.'"); expect(token_kind::dot, "'.'");
(void)kind;
} }
void parse_toplevel(std::string const& current_file) { void parse_toplevel(std::string const& current_file) {
@ -693,7 +695,7 @@ class tptp_parser {
parse_include(current_file); parse_include(current_file);
} }
else if (kw == "fof" || kw == "cnf" || kw == "tff" || kw == "thf") { else if (kw == "fof" || kw == "cnf" || kw == "tff" || kw == "thf") {
parse_annotated(kw); parse_annotated();
} }
else { else {
std::ostringstream out; std::ostringstream out;
@ -704,15 +706,16 @@ class tptp_parser {
} }
public: public:
tptp_parser(z3::context& ctx, z3::solver& solver): tptp_parser(cmd_context& cmd):
m_ctx(ctx), m_cmd(cmd),
m_solver(solver), m(m_cmd.m()),
m_univ(ctx.uninterpreted_sort("U")) { m_arith(m),
m_sorts.emplace("$tType", ctx.uninterpreted_sort("$tType")); m_univ(m.mk_uninterpreted_sort(symbol("U"))) {
m_sorts.emplace("$tType", m.mk_uninterpreted_sort(symbol("$tType")));
m_sorts.emplace("$i", m_univ); m_sorts.emplace("$i", m_univ);
m_sorts.emplace("$o", m_ctx.bool_sort()); m_sorts.emplace("$o", m.mk_bool_sort());
m_sorts.emplace("$int", m_ctx.int_sort()); m_sorts.emplace("$int", m_arith.mk_int());
m_sorts.emplace("$real", m_ctx.real_sort()); m_sorts.emplace("$real", m_arith.mk_real());
} }
void parse_file(std::string const& filename) { void parse_file(std::string const& filename) {
@ -728,9 +731,7 @@ public:
m_input = buf.str(); m_input = buf.str();
m_lex = std::make_unique<lexer>(m_input); m_lex = std::make_unique<lexer>(m_input);
next(); next();
m_file_stack.push_back(filename);
parse_toplevel(filename); parse_toplevel(filename);
m_file_stack.pop_back();
} }
void parse_stream(std::istream& in) { void parse_stream(std::istream& in) {
@ -745,28 +746,29 @@ public:
bool has_conjecture() const { return m_has_conjecture; } bool has_conjecture() const { return m_has_conjecture; }
}; };
z3::expr tptp_parser::parse_term() { expr_ref tptp_parser::parse_term() {
z3::expr e = parse_term_primary(); expr_ref e = parse_term_primary();
while (accept(token_kind::at_tok)) { while (accept(token_kind::at_tok)) {
z3::expr arg = parse_term_primary(); expr_ref arg = parse_term_primary();
if (!e.is_app() || e.decl().decl_kind() != Z3_OP_UNINTERPRETED) if (!is_app(e) || to_app(e)->get_decl()->get_family_id() != null_family_id)
throw parse_error("application operator (@) requires uninterpreted function on left-hand side"); throw parse_error("application operator (@) requires uninterpreted function on left-hand side");
z3::func_decl f = e.decl(); app* a = to_app(e);
std::vector<z3::expr> args; expr_ref_vector args(m);
for (unsigned i = 0; i < e.num_args(); ++i) args.push_back(e.arg(i)); for (unsigned i = 0; i < a->get_num_args(); ++i) args.push_back(a->get_arg(i));
args.push_back(arg); args.push_back(arg);
e = f(static_cast<unsigned>(args.size()), args.data()); e = m.mk_app(a->get_decl(), args.size(), args.data());
} }
return e; return e;
} }
z3::expr tptp_parser::parse_formula() { expr_ref tptp_parser::parse_formula() {
z3::expr e = parse_implies_formula(); expr_ref e = parse_implies_formula();
while (is(token_kind::iff_tok) || is(token_kind::xor_tok)) { while (is(token_kind::iff_tok) || is(token_kind::xor_tok)) {
bool is_xor = accept(token_kind::xor_tok); bool is_xor = accept(token_kind::xor_tok);
if (!is_xor) expect(token_kind::iff_tok, "'<=>'"); if (!is_xor) expect(token_kind::iff_tok, "'<=>'");
z3::expr rhs = parse_implies_formula(); expr_ref rhs = parse_implies_formula();
e = is_xor ? !(e == rhs) : (e == rhs); expr_ref iff(m.mk_iff(e, rhs), m);
e = is_xor ? expr_ref(m.mk_not(iff), m) : iff;
} }
return e; return e;
} }
@ -775,36 +777,53 @@ z3::expr tptp_parser::parse_formula() {
unsigned read_tptp(char const* file_name) { unsigned read_tptp(char const* file_name) {
try { try {
z3::context ctx; cmd_context ctx;
z3::solver solver(ctx); ctx.set_solver_factory(mk_smt_strategic_solver_factory());
tptp_parser p(ctx, solver);
tptp_parser p(ctx);
if (file_name) p.parse_file(file_name); if (file_name) p.parse_file(file_name);
else p.parse_stream(std::cin); else p.parse_stream(std::cin);
z3::check_result r = solver.check(); std::ostringstream sink;
if (r == z3::unsat) { ctx.set_regular_stream(sink);
ctx.check_sat(0, nullptr);
switch (ctx.cs_state()) {
case cmd_context::css_unsat:
if (p.has_conjecture()) std::cout << "% SZS status Theorem\n"; if (p.has_conjecture()) std::cout << "% SZS status Theorem\n";
else std::cout << "% SZS status Unsatisfiable\n"; else std::cout << "% SZS status Unsatisfiable\n";
} break;
else if (r == z3::sat) { case cmd_context::css_sat:
if (p.has_conjecture()) std::cout << "% SZS status CounterSatisfiable\n"; if (p.has_conjecture()) std::cout << "% SZS status CounterSatisfiable\n";
else std::cout << "% SZS status Satisfiable\n"; else std::cout << "% SZS status Satisfiable\n";
if (g_display_model) std::cout << solver.get_model() << "\n"; if (g_display_model) {
} model_ref mdl;
else { if (ctx.is_model_available(mdl))
ctx.display_model(mdl);
}
break;
case cmd_context::css_unknown:
std::cout << "% SZS status GaveUp\n"; std::cout << "% SZS status GaveUp\n";
std::string reason = solver.reason_unknown(); {
if (!reason.empty()) std::cout << "% SZS reason " << reason << "\n"; std::string reason = ctx.reason_unknown();
if (!reason.empty()) std::cout << "% SZS reason " << reason << "\n";
}
break;
default:
break;
}
if (g_display_statistics) {
ctx.set_regular_stream("stdout");
ctx.display_statistics();
} }
if (g_display_statistics) std::cout << solver.statistics() << "\n";
return 0; return 0;
} }
catch (parse_error const& ex) { catch (parse_error const& ex) {
std::cerr << "TPTP parse error: " << ex.what() << "\n"; std::cerr << "TPTP parse error: " << ex.what() << "\n";
return ERR_PARSER; return ERR_PARSER;
} }
catch (z3::exception const& ex) { catch (z3_exception& ex) {
std::cerr << "TPTP frontend error: " << ex.msg() << "\n"; std::cerr << "TPTP frontend error: " << ex.what() << "\n";
return ERR_INTERNAL_FATAL; return ERR_INTERNAL_FATAL;
} }
} }