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

README.md

@@ -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)
 
 

src/ast/ast.cpp

@@ -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) {

src/ast/bv_decl_plugin.cpp

@@ -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) {

src/ast/datatype_decl_plugin.cpp

@@ -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) {

src/cmd_context/basic_cmds.cpp

@@ -817,9 +817,9 @@ class declare_map_cmd : public cmd {
         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);

src/model/array_factory.cpp

@@ -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;
 }

src/muz/transforms/dl_mk_rule_inliner.cpp

@@ -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;

src/sat/smt/arith_internalize.cpp

@@ -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;
         }
     }
 

src/smt/theory_array_base.cpp

@@ -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);
         }
     };
 

src/smt/theory_lra.cpp

@@ -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;
         }
     }
 

src/util/gparams.cpp

@@ -276,20 +276,20 @@ struct gparams::imp {
                 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 @@ struct gparams::imp {
             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 @@ struct gparams::imp {
                 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 @@ struct gparams::imp {
                 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 @@ struct gparams::imp {
             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 @@ struct gparams::imp {
                 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 @@ struct gparams::imp {
             if (mod_name[0]) {
                 strm << " at module '" << mod_name << "'";            
             }
-            throw exception(strm.str());
+            throw exception(std::move(strm).str());
         }
     }
 
@@ -406,7 +406,7 @@ struct gparams::imp {
             else {
                 std::stringstream strm;
                 strm << "invalid parameter, unknown module '" << m << "'";
-                throw exception(strm.str());
+                throw exception(std::move(strm).str());
             }
         }
     }
@@ -456,7 +456,7 @@ struct gparams::imp {
         }
         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 @@ struct gparams::imp {
         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 @@ struct gparams::imp {
             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))