mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Lev Nachmanson 2023-12-20 12:56:55 -10:00
parent 4317d134bf c4fa719751
commit a00eb08ddd
22 changed files with 53 additions and 127 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_ast.cpp
View file

@ -146,8 +146,7 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
if (!p.has_def(d)) {
std::string msg = "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl";
SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " needs to be declared using rec_func_decl");
return;
}
expr_ref abs_body(m);
@ -168,8 +167,7 @@ extern "C" {
return;
}
if (!pd.get_def()->get_cases().empty()) {
std::string msg = "function " + mk_pp(d, m) + " has already been given a definition";
SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
SET_ERROR_CODE(Z3_INVALID_ARG, "function " + mk_pp(d, m) + " has already been given a definition");
return;
}

4
src/api/api_ast_map.cpp
View file

@ -160,8 +160,8 @@ extern "C" {
for (; it != end; ++it) {
buffer << "\n (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n " << mk_ismt2_pp(it->m_value, mng, 3) << ")";
}
buffer << ")";
return mk_c(c)->mk_external_string(buffer.str());
buffer << ')';
return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN(nullptr);
}

6
src/api/api_context.cpp
View file

@ -338,12 +338,12 @@ namespace api {
std::ostringstream buffer;
app * a = to_app(n);
buffer << mk_pp(a->get_decl(), m()) << " applied to: ";
if (a->get_num_args() > 1) buffer << "\n";
if (a->get_num_args() > 1) buffer << '\n';
for (unsigned i = 0; i < a->get_num_args(); ++i) {
buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort ";
buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << "\n";
buffer << mk_pp(a->get_arg(i)->get_sort(), m()) << '\n';
}
auto str = buffer.str();
auto str = std::move(buffer).str();
warning_msg("%s", str.c_str());
break;
}

4
src/api/api_fpa.cpp
View file

@ -1022,7 +1022,7 @@ extern "C" {
if (mpfm.is_inf(val)) mpqm.set(q, 0);
std::stringstream ss;
mpqm.display_decimal(ss, q, sbits);
return mk_c(c)->mk_external_string(ss.str());
return mk_c(c)->mk_external_string(std::move(ss).str());
Z3_CATCH_RETURN("");
}
@ -1100,7 +1100,7 @@ extern "C" {
}
std::stringstream ss;
ss << exp;
return mk_c(c)->mk_external_string(ss.str());
return mk_c(c)->mk_external_string(std::move(ss).str());
Z3_CATCH_RETURN("");
}

4
src/api/api_goal.cpp
View file

@ -185,7 +185,7 @@ extern "C" {
std::ostringstream buffer;
to_goal_ref(g)->display(buffer);
// Hack for removing the trailing '\n'
std::string result = buffer.str();
std::string result = std::move(buffer).str();
SASSERT(result.size() > 0);
result.resize(result.size()-1);
return mk_c(c)->mk_external_string(std::move(result));
@ -203,7 +203,7 @@ extern "C" {
}
to_goal_ref(g)->display_dimacs(buffer, include_names);
// Hack for removing the trailing '\n'
std::string result = buffer.str();
std::string result = std::move(buffer).str();
SASSERT(result.size() > 0);
result.resize(result.size()-1);
return mk_c(c)->mk_external_string(std::move(result));

4
src/api/api_model.cpp
View file

@ -432,14 +432,14 @@ extern "C" {
if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) {
model_smt2_pp(buffer, mk_c(c)->m(), *(to_model_ref(m)), 0);
// Hack for removing the trailing '\n'
result = buffer.str();
result = std::move(buffer).str();
if (!result.empty())
result.resize(result.size()-1);
}
else {
model_params p;
model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
result = buffer.str();
result = std::move(buffer).str();
}
return mk_c(c)->mk_external_string(std::move(result));
Z3_CATCH_RETURN(nullptr);

10
src/api/api_numeral.cpp
View file

@ -189,7 +189,7 @@ extern "C" {
if (ok && r.is_int() && !r.is_neg()) {
std::stringstream strm;
r.display_bin(strm, r.get_num_bits());
return mk_c(c)->mk_external_string(strm.str());
return mk_c(c)->mk_external_string(std::move(strm).str());
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@ -237,7 +237,7 @@ extern "C" {
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
std::ostringstream buffer;
fu.fm().display_smt2(buffer, tmp, false);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
@ -288,21 +288,21 @@ extern "C" {
if (u.is_numeral(e, r) && !r.is_int()) {
std::ostringstream buffer;
r.display_decimal(buffer, precision);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
}
if (u.is_irrational_algebraic_numeral(e)) {
algebraic_numbers::anum const & n = u.to_irrational_algebraic_numeral(e);
algebraic_numbers::manager & am = u.am();
std::ostringstream buffer;
am.display_decimal(buffer, n, precision);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm))
return Z3_get_numeral_string(c, a);
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), ftmp)) {
std::ostringstream buffer;
fu.fm().display_decimal(buffer, ftmp, 12);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
}
else if (Z3_get_numeral_rational(c, a, r)) {
return mk_c(c)->mk_external_string(r.to_string());

16
src/api/api_solver.cpp
View file

@ -170,8 +170,8 @@ extern "C" {
if (g_is_threaded || g_thread_id != std::this_thread::get_id()) {
g_is_threaded = true;
std::ostringstream strm;
strm << smt2log << "-" << std::this_thread::get_id();
smt2log = symbol(strm.str());
strm << smt2log << '-' << std::this_thread::get_id();
smt2log = symbol(std::move(strm).str());
}
to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str());
}
@ -208,7 +208,7 @@ extern "C" {
if (!smt_logics::supported_logic(to_symbol(logic))) {
std::ostringstream strm;
strm << "logic '" << to_symbol(logic) << "' is not recognized";
SET_ERROR_CODE(Z3_INVALID_ARG, strm.str());
SET_ERROR_CODE(Z3_INVALID_ARG, std::move(strm).str());
RETURN_Z3(nullptr);
}
else {
@ -306,7 +306,7 @@ extern "C" {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(errstrm).str());
return;
}
@ -333,7 +333,7 @@ extern "C" {
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
if (!parse_dimacs(is, err, solver)) {
SET_ERROR_CODE(Z3_PARSER_ERROR, err.str());
SET_ERROR_CODE(Z3_PARSER_ERROR, std::move(err).str());
return;
}
sat2goal s2g;
@ -400,7 +400,7 @@ extern "C" {
if (!initialized)
to_solver(s)->m_solver = nullptr;
descrs.display(buffer);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN("");
}
@ -799,7 +799,7 @@ extern "C" {
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->display(buffer);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN("");
}
@ -810,7 +810,7 @@ extern "C" {
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->display_dimacs(buffer, include_names);
return mk_c(c)->mk_external_string(buffer.str());
return mk_c(c)->mk_external_string(std::move(buffer).str());
Z3_CATCH_RETURN("");
}

33
src/ast/ast.cpp
View file

@ -319,26 +319,6 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain,
//
// -----------------------------------
static app_flags mk_const_flags() {
app_flags r;
r.m_depth = 1;
r.m_ground = true;
r.m_has_quantifiers = false;
r.m_has_labels = false;
return r;
}
static app_flags mk_default_app_flags() {
app_flags r;
r.m_depth = 1;
r.m_ground = true;
r.m_has_quantifiers = false;
r.m_has_labels = false;
return r;
}
app_flags app::g_constant_flags = mk_const_flags();
app::app(func_decl * decl, unsigned num_args, expr * const * args):
expr(AST_APP),
m_decl(decl),
@ -1762,8 +1742,7 @@ ast * ast_manager::register_node_core(ast * n) {
inc_ref(t->get_decl());
unsigned num_args = t->get_num_args();
if (num_args > 0) {
app_flags * f = t->flags();
*f = mk_default_app_flags();
app_flags * f = &t->m_flags;
SASSERT(t->is_ground());
SASSERT(!t->has_quantifiers());
SASSERT(!t->has_labels());
@ -1776,13 +1755,13 @@ ast * ast_manager::register_node_core(ast * n) {
unsigned arg_depth = 0;
switch (arg->get_kind()) {
case AST_APP: {
app_flags * arg_flags = to_app(arg)->flags();
arg_depth = arg_flags->m_depth;
if (arg_flags->m_has_quantifiers)
app *app = to_app(arg);
arg_depth = app->get_depth();
if (app->has_quantifiers())
f->m_has_quantifiers = true;
if (arg_flags->m_has_labels)
if (app->has_labels())
f->m_has_labels = true;
if (!arg_flags->m_ground)
if (!app->is_ground())
f->m_ground = false;
break;
}

17
src/ast/ast.h
View file

@ -704,6 +704,7 @@ struct app_flags {
unsigned m_ground:1; // application does not have free variables or nested quantifiers.
unsigned m_has_quantifiers:1; // application has nested quantifiers.
unsigned m_has_labels:1; // application has nested labels.
app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {}
};
class app : public expr {
@ -711,19 +712,15 @@ class app : public expr {
func_decl * m_decl;
unsigned m_num_args;
app_flags m_flags;
expr * m_args[0];
static app_flags g_constant_flags;
// remark: store term depth in the end of the app. the depth is only stored if the num_args > 0
static unsigned get_obj_size(unsigned num_args) {
return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags);
return sizeof(app) + num_args * sizeof(expr *);
}
friend class tmp_app;
app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast<app_flags*>(const_cast<expr**>(m_args + m_num_args)); }
app(func_decl * decl, unsigned num_args, expr * const * args);
public:
func_decl * get_decl() const { return m_decl; }
@ -744,10 +741,10 @@ public:
expr * const * end() const { return m_args + m_num_args; }
sort * _get_sort() const { return get_decl()->get_range(); }
unsigned get_depth() const { return flags()->m_depth; }
bool is_ground() const { return flags()->m_ground; }
bool has_quantifiers() const { return flags()->m_has_quantifiers; }
bool has_labels() const { return flags()->m_has_labels; }
unsigned get_depth() const { return m_flags.m_depth; }
bool is_ground() const { return m_flags.m_ground; }
bool has_quantifiers() const { return m_flags.m_has_quantifiers; }
bool has_labels() const { return m_flags.m_has_labels; }
};
// -----------------------------------

4
src/ast/ast_pp.h
View file

@ -58,13 +58,13 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
inline std::string operator+(char const* s, mk_pp const& pp) {
std::ostringstream strm;
strm << s << pp;
return strm.str();
return std::move(strm).str();
}
inline std::string operator+(std::string const& s, mk_pp const& pp) {
std::ostringstream strm;
strm << s << pp;
return strm.str();
return std::move(strm).str();
}
inline std::string& operator+=(std::string& s, mk_pp const& pp) {

8
src/ast/rewriter/pb_rewriter.cpp
View file

@ -157,9 +157,7 @@ expr_ref pb_rewriter::mk_validate_rewrite(app_ref& e1, app_ref& e2) {
continue;
}
std::ostringstream strm;
strm << 'x' << i;
name = symbol(strm.str());
name = symbol('x' + std::to_string(i));
trail.push_back(m.mk_const(name, a.mk_int()));
expr* x = trail.back();
m.is_not(e,e);
@ -188,9 +186,7 @@ void pb_rewriter::validate_rewrite(func_decl* f, unsigned sz, expr*const* args,
}
void pb_rewriter::dump_pb_rewrite(expr* fml) {
std::ostringstream strm;
strm << "pb_rewrite_" << (s_lemma++) << ".smt2";
std::ofstream out(strm.str());
std::ofstream out("pb_rewrite_" + std::to_string(s_lemma++) + ".smt2");
ast_smt_pp pp(m());
pp.display_smt2(out, fml);
out.close();

3
src/ast/well_sorted.cpp
View file

@ -70,8 +70,7 @@ struct well_sorted_proc {
strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << '\n';
strm << "Actual sort: " << mk_pp(actual_sort, m_manager) << '\n';
strm << "Function sort: " << mk_pp(decl, m_manager) << '.';
auto str = strm.str();
warning_msg("%s", str.c_str());
warning_msg("%s", std::move(strm).str().c_str());
m_error = true;
return;
}

1
src/math/lp/numeric_pair.h
View file

@ -24,7 +24,6 @@
#include <algorithm>
#ifdef lp_for_z3
#include "util/rational.h"
#include "util/sstream.h"
#include "util/z3_exception.h"
#else
// include "util/numerics/mpq.h"

6
src/model/model_smt2_pp.cpp
View file

@ -68,7 +68,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
buffer << " ";
}
buffer << "\n-----------";
std::string buffer_str = buffer.str();
std::string buffer_str = std::move(buffer).str();
unsigned len = static_cast<unsigned>(buffer_str.length());
pp_indent(out, indent);
out << ";; ";
@ -206,9 +206,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
if (f_i->is_partial()) {
body = mk_string(m, "#unspecified");
for (unsigned j = 0; j < f->get_arity(); j++) {
std::stringstream strm;
strm << "x!" << (j+1);
var_names.push_back(symbol(strm.str()));
var_names.push_back(symbol("x!" + std::to_string(j+1)));
}
}
else {

2
src/sat/sat_cutset.cpp
View file

@ -273,7 +273,7 @@ namespace sat {
std::string cut::table2string(unsigned num_input, uint64_t table) {
std::ostringstream strm;
display_table(strm, num_input, table);
return strm.str();
return std::move(strm).str();
}

2
src/sat/sat_solver.cpp
View file

@ -2280,7 +2280,7 @@ namespace sat {
<< std::setw(4) << m_stats.m_restart
<< mk_stat(*this)
<< " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
std::string str(strm.str());
std::string str = std::move(strm).str();
svector<size_t> nums;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;

4
src/smt/smt_context_pp.cpp
View file

@ -510,7 +510,7 @@ namespace smt {
#else
strm << "lemma_" << (++m_lemma_id) << ".smt2";
#endif
return strm.str();
return std::move(strm).str();
}
@ -722,7 +722,7 @@ namespace smt {
<< std::setw(4) << m_stats.m_num_del_clauses << " "
<< std::setw(7) << mem_stat() << ")\n";
std::string str(strm.str());
std::string str = std::move(strm).str();
svector<size_t> offsets;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;

10
src/smt/smt_enode.cpp
View file

@ -340,8 +340,7 @@ namespace smt {
void tmp_enode::set_capacity(unsigned new_capacity) {
SASSERT(new_capacity > m_capacity);
if (m_enode_data)
dealloc_svect(m_enode_data);
dealloc_svect(m_enode_data);
m_capacity = new_capacity;
unsigned sz = sizeof(enode) + m_capacity * sizeof(enode*);
m_enode_data = alloc_svect(char, sz);
@ -359,9 +358,6 @@ namespace smt {
if (num_args > m_capacity)
set_capacity(num_args * 2);
enode * r = get_enode();
if (m_app.get_app()->get_decl() != f) {
r->m_func_decl_id = UINT_MAX;
}
m_app.set_decl(f);
m_app.set_num_args(num_args);
r->m_commutative = num_args == 2 && f->is_commutative();
@ -369,9 +365,5 @@ namespace smt {
return r;
}
void tmp_enode::reset() {
get_enode()->m_func_decl_id = UINT_MAX;
}
};

1
src/smt/smt_enode.h
View file

@ -465,7 +465,6 @@ namespace smt {
tmp_enode();
~tmp_enode();
enode * set(func_decl * f, unsigned num_args, enode * const * args);
void reset();
};
inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); }

31
src/util/sstream.h
View file

@ -1,31 +0,0 @@
/*
Copyright (c) 2018 Microsoft Corporation
Module Name:
nat_set.h
Abstract:
Wrapper for sstream.
Author:
Leonardo de Moura (leonardo) 2013
Revision History:
*/
#pragma once
#include <sstream>
#include <string>
namespace lean {
/** \brief Wrapper for std::ostringstream */
class sstream {
std::ostringstream m_strm;
public:
std::string str() const { return m_strm.str(); }
template<typename T> sstream & operator<<(T const & t) { m_strm << t; return *this; }
};
}

4
src/util/zstring.cpp
View file

@ -152,7 +152,7 @@ std::string zstring::encode() const {
unsigned ch = m_buffer[i];
if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) {
_flush();
strm << "\\u{" << std::hex << ch << std::dec << "}";
strm << "\\u{" << std::hex << ch << std::dec << '}';
}
else {
if (offset == 99)
@ -161,7 +161,7 @@ std::string zstring::encode() const {
}
}
_flush();
return strm.str();
return std::move(strm).str();
}
bool zstring::suffixof(zstring const& other) const {