mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-10 17:09:36 -08:00
parent 081c62d006 580012e19f
commit 8f2ea90db1
11 changed files with 36 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
README.md
View file

@ -199,6 +199,11 @@ The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C++ A
A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](src/api/js).
### Smalltalk (``Pharo`` / ``Smalltalk/X``)
Project [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) provides Smalltalk interface
to Z3's C API. For more information, see [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md)
## System Overview
![System Diagram](https://github.com/Z3Prover/doc/blob/master/programmingz3/images/Z3Overall.jpg)
@ -215,5 +220,6 @@ A WebAssembly build with associated TypeScript typings is published on npm as [z
* C
* OCaml
* [Julia](https://github.com/ahumenberger/Z3.jl)
* [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X)

5
src/ast/ast.cpp
View file

@ -234,8 +234,7 @@ std::ostream& operator<<(std::ostream& out, sort_size const & ss) {
// -----------------------------------
std::ostream & operator<<(std::ostream & out, sort_info const & info) {
operator<<(out, static_cast<decl_info const&>(info));
out << " :size " << info.get_num_elements();
return out;
return out << " :size " << info.get_num_elements();
}
// -----------------------------------
@ -2237,7 +2236,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
std::ostringstream buffer;
buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this);
throw ast_exception(buffer.str());
throw ast_exception(std::move(buffer).str());
}
app * r = nullptr;
if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {

4
src/ast/bv_decl_plugin.cpp
View file

@ -886,8 +886,8 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
}
sort * bv_util::mk_sort(unsigned bv_size) {
parameter p[1] = { parameter(bv_size) };
return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
parameter p(bv_size);
return m_manager.mk_sort(get_fid(), BV_SORT, 1, &p);
}
unsigned bv_util::get_int2bv_size(parameter const& p) {

8
src/ast/datatype_decl_plugin.cpp
View file

@ -69,8 +69,8 @@ namespace datatype {
domain.push_back(a->instantiate(ps)->get_range());
}
sort_ref range = get_def().instantiate(ps);
parameter pas[1] = { parameter(name()) };
return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, pas, domain.size(), domain.data(), range), m);
parameter pas(name());
return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, &pas, domain.size(), domain.data(), range), m);
}
func_decl_ref constructor::instantiate(sort* dt) const {
@ -1052,8 +1052,8 @@ namespace datatype {
func_decl * util::get_constructor_is(func_decl * con) {
SASSERT(is_constructor(con));
sort * datatype = con->get_range();
parameter ps[1] = { parameter(con)};
return m.mk_func_decl(fid(), OP_DT_IS, 1, ps, 1, &datatype);
parameter ps(con);
return m.mk_func_decl(fid(), OP_DT_IS, 1, &ps, 1, &datatype);
}
func_decl * util::get_constructor_recognizer(func_decl * con) {

4
src/cmd_context/basic_cmds.cpp
View file

@ -817,9 +817,9 @@ public:
sort_ref range(ctx.m());
array_sort_args.push_back(m_f->get_range());
range = array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data());
parameter p[1] = { parameter(m_f) };
parameter p(m_f);
func_decl_ref new_map(ctx.m());
new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, p, domain.size(), domain.data(), range.get());
new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, &p, domain.size(), domain.data(), range.get());
if (new_map == 0)
throw cmd_exception("invalid array map operator");
ctx.insert(m_name, new_map);

4
src/model/array_factory.cpp
View file

@ -45,8 +45,8 @@ expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {
func_decl * f = mk_aux_decl_for_array_sort(m_manager, s);
fi = alloc(func_interp, m_manager, get_array_arity(s));
m_model.register_decl(f, fi);
parameter p[1] = { parameter(f) };
expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, p);
parameter p(f);
expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, &p);
register_value(val);
return val;
}

2
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -449,7 +449,7 @@ namespace datalog {
}
}
if (modified) {
datalog::del_rule(m_mc, *r0, l_false);
datalog::del_rule(m_mc, *r0, l_true);
}
return modified;

2
src/sat/smt/arith_internalize.cpp
View file

@ -85,7 +85,7 @@ namespace arith {
m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching() = prms.arith_nl_expp();
m_nla->settings().expensive_patching() = false;
}
}

4
src/smt/theory_array_base.cpp
View file

@ -958,8 +958,8 @@ namespace smt {
fi->insert_entry(args.data(), result);
}
parameter p[1] = { parameter(f) };
return m.mk_app(m_fid, OP_AS_ARRAY, 1, p);
parameter p(f);
return m.mk_app(m_fid, OP_AS_ARRAY, 1, &p);
}
};

2
src/smt/theory_lra.cpp
View file

@ -292,7 +292,7 @@ class theory_lra::imp {
m_nla->settings().grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->settings().grobner_quota() = prms.arith_nl_gr_q();
m_nla->settings().grobner_frequency() = prms.arith_nl_grobner_frequency();
m_nla->settings().expensive_patching() = prms.arith_nl_expp();
m_nla->settings().expensive_patching() = false;
}
}

26
src/util/gparams.cpp
View file

@ -276,20 +276,20 @@ public:
strm << "the parameter '" << param_name
<< "', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:" << new_name
<< "' for the full description of the parameter";
throw exception(strm.str());
throw exception(std::move(strm).str());
}
else if (is_old_param_name(param_name)) {
std::stringstream strm;
strm << "unknown parameter '" << param_name
<< "', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list";
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
else {
std::stringstream strm;
strm << "unknown parameter '" << param_name << "'\n";
strm << "Legal parameters are:\n";
d.display(strm, 2, false, false);
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
}
else {
@ -298,7 +298,7 @@ public:
strm << "at module '" << mod_name << "'\n";
strm << "Legal parameters are:\n";
d.display(strm, 2, false, false);
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
}
@ -312,7 +312,7 @@ public:
if (!('0' <= *value && *value <= '9')) {
strm << "Expected values for parameter " << name
<< " is an unsigned integer. It was given argument '" << _value << "'";
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
}
break;
@ -321,7 +321,7 @@ public:
if (!('0' <= *value && *value <= '9') && *value != '.' && *value != '-' && *value != '/') {
strm << "Expected values for parameter " << name
<< " is a double. It was given argument '" << _value << "'";
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
}
break;
@ -330,7 +330,7 @@ public:
if (strcmp(value, "true") != 0 && strcmp(value, "false") != 0) {
strm << "Expected values for parameter " << name
<< " are 'true' or 'false'. It was given argument '" << value << "'";
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
break;
default:
@ -368,7 +368,7 @@ public:
if (mod_name[0]) {
strm << " at module '" << mod_name << "'";
}
throw default_exception(strm.str());
throw default_exception(std::move(strm).str());
}
}
else if (k == CPK_SYMBOL) {
@ -385,7 +385,7 @@ public:
if (mod_name[0]) {
strm << " at module '" << mod_name << "'";
}
throw exception(strm.str());
throw exception(std::move(strm).str());
}
}
@ -406,7 +406,7 @@ public:
else {
std::stringstream strm;
strm << "invalid parameter, unknown module '" << m << "'";
throw exception(strm.str());
throw exception(std::move(strm).str());
}
}
}
@ -456,7 +456,7 @@ public:
}
std::stringstream strm;
strm << "unknown module '" << m << "'";
throw exception(strm.str());
throw exception(std::move(strm).str());
}
// unfortunately, params_ref is not thread safe
@ -523,7 +523,7 @@ public:
if (!get_module_param_descr(module_name, d)) {
std::stringstream strm;
strm << "unknown module '" << module_name << "'";
throw exception(strm.str());
throw exception(std::move(strm).str());
}
out << "[module] " << module_name;
char const * descr = nullptr;
@ -548,7 +548,7 @@ public:
if (!get_module_param_descr(m, d)) {
std::stringstream strm;
strm << "unknown module '" << m << "'";
throw exception(strm.str());
throw exception(std::move(strm).str());
}
}
if (!d->contains(sp))