Merge remote-tracking branch 'upstream/master'

src/api/api_solver.cpp

@@ -61,7 +61,7 @@ extern "C" {
     }
 
     void solver2smt2_pp::push() {
-        m_out << "(push)\n";
+        m_out << "(push 1)\n";
         m_pp_util.push();
         m_tracked_lim.push_back(m_tracked.size());
     }

src/api/dotnet/Context.cs

@@ -2488,12 +2488,12 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieve element at index.
         /// </summary>
-        public SeqExpr MkNth(SeqExpr s, Expr index)
+        public Expr MkNth(SeqExpr s, Expr index)
         {
             Debug.Assert(s != null);
             Debug.Assert(index != null);
             CheckContextMatch(s, index);
-            return new SeqExpr(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
+            return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
         }
 
         /// <summary>

src/api/java/Context.java

@@ -2048,6 +2048,16 @@ public class Context implements AutoCloseable {
         return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
     }
 
+    /**
+     *  Retrieve element at index.
+     */
+    public Expr MkNth(SeqExpr s, Expr index)
+    {
+        checkContextMatch(s, index);
+        return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
+    }
+
+
     /**
      * Extract subsequence.
      */

src/ast/ast.cpp

@@ -218,6 +218,7 @@ unsigned decl_info::hash() const {
 
 bool decl_info::operator==(decl_info const & info) const {
     return m_family_id == info.m_family_id && m_kind == info.m_kind &&
+        m_parameters.size() == info.m_parameters.size() && 
         compare_arrays<parameter>(m_parameters.begin(), info.m_parameters.begin(), m_parameters.size());
 }
 

src/ast/ast.h

@@ -130,7 +130,7 @@ public:
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 
-    parameter(parameter && other) : m_kind(other.m_kind) {
+    parameter(parameter && other) noexcept : m_kind(other.m_kind) {
         switch (other.m_kind) {
         case PARAM_INT: m_int = other.get_int(); break;
         case PARAM_AST: m_ast = other.get_ast(); break;

src/ast/justified_expr.h

@@ -1,6 +1,5 @@
 
-#ifndef JUSTIFIED_EXPR_H_
-#define JUSTIFIED_EXPR_H_
+#pragma once
 
 #include "ast/ast.h"
 
@@ -40,6 +39,15 @@ public:
         m.inc_ref(m_proof);
     }
 
+    justified_expr(justified_expr && other) noexcept :
+        m(other.m),
+        m_fml(nullptr),
+        m_proof(nullptr)
+    {
+        std::swap(m_fml, other.m_fml);
+        std::swap(m_proof, other.m_proof);
+    }
+
     ~justified_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_proof);
@@ -50,5 +58,3 @@ public:
     expr* get_fml() const { return m_fml; }
     proof* get_proof() const { return m_proof; }        
 };
-
-#endif

src/ast/normal_forms/nnf.cpp

@@ -221,16 +221,6 @@ struct nnf::imp {
             m_cache_result(cache_res),
             m_spos(spos) {
         }
-        frame(frame && other):
-            m_curr(std::move(other.m_curr)),
-            m_i(other.m_i),
-            m_pol(other.m_pol),
-            m_in_q(other.m_in_q),
-            m_new_child(other.m_new_child),
-            m_cache_result(other.m_cache_result),
-            m_spos(other.m_spos) {            
-        }
-            
     };
 
     // There are four caches:

src/ast/recfun_decl_plugin.cpp

@@ -131,8 +131,6 @@ namespace recfun {
             path(nullptr), to_split(nullptr), to_unfold(to_unfold) {}
         branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : 
             path(path), to_split(to_split), to_unfold(to_unfold) {}
-        branch(branch const & from) : 
-            path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {}
     };
 
     // state for computing cases from the RHS of a functions' definition

src/ast/rewriter/seq_rewriter.cpp

@@ -2152,6 +2152,7 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
 }
 
 expr_ref seq_rewriter::is_nullable_rec(expr* r) {
+    std::cout << "is_nullable_rec" << std::endl;
     expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr), m());
     if (!result) {
         result = is_nullable(r);
@@ -2161,6 +2162,8 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
 }
 
 expr_ref seq_rewriter::is_nullable(expr* r) {
+    std::cout << "is_nullable" << std::endl;
+    // std::cout << "call to is_nullable(" << expr_ref(r, m()) << ")" << std::endl;
     SASSERT(m_util.is_re(r));
     expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr;
     unsigned lo = 0, hi = 0;
@@ -2312,6 +2315,7 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
     expr* r1 = nullptr, *r2 = nullptr, *p = nullptr;
     unsigned lo = 0, hi = 0;
     if (re().is_concat(r, r1, r2)) {
+        std::cout << "is_nullable -- from concat" << std::endl;
         expr_ref is_n = is_nullable(r1);
         expr_ref dr1(re().mk_derivative(ele, r1), m());
         expr_ref dr2(re().mk_derivative(ele, r2), m());
@@ -2796,6 +2800,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE1;
     }
     if (str().is_empty(a)) {
+        std::cout << "is_nullable -- from str.in_re" << std::endl;
         result = is_nullable(b);
         if (str().is_in_re(result))
             return BR_DONE;

src/math/automata/automaton.h

@@ -54,6 +54,10 @@ public:
             if (m_t) m.inc_ref(m_t);
         }
 
+        move(move &&other) noexcept : m(other.m), m_t(nullptr), m_src(other.m_src), m_dst(other.m_dst) {
+            std::swap(m_t, other.m_t);
+        }
+
         move& operator=(move const& other) {
             SASSERT(&m == &other.m);
             T* t = other.m_t;

src/math/dd/dd_pdd.h

@@ -320,7 +320,7 @@ namespace dd {
     public:
         pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); }
         pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); }
-        pdd(pdd && other): root(0), m(other.m) { std::swap(root, other.root); }
+        pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); }
         pdd& operator=(pdd const& other);
         ~pdd() { m.dec_ref(root); }
         pdd lo() const { return pdd(m.lo(root), m); }

src/math/grobner/pdd_solver.h

@@ -25,6 +25,7 @@
 #include "util/rlimit.h"
 #include "util/statistics.h"
 #include "math/dd/dd_pdd.h"
+#include <cstring>
 
 namespace dd {
 

src/math/hilbert/heap_trie.h

@@ -37,13 +37,13 @@ Notes:
 #ifndef HEAP_TRIE_H_
 #define HEAP_TRIE_H_
 
+#include <cstring>
 #include "util/map.h"
 #include "util/vector.h"
 #include "util/buffer.h"
 #include "util/statistics.h"
 #include "util/small_object_allocator.h"
 
-
 template<typename Key, typename KeyLE, typename KeyHash, typename Value>
 class heap_trie {
 

src/math/hilbert/hilbert_basis.h

@@ -25,14 +25,14 @@ Revision History:
 
 --*/
 
-#ifndef HILBERT_BASIS_H_
-#define HILBERT_BASIS_H_
+#pragma once
 
 #include "util/rational.h"
 #include "util/lbool.h"
 #include "util/statistics.h"
 #include "util/checked_int64.h"
 #include "util/rlimit.h"
+#include <cstring>
 
 typedef vector<rational> rational_vector;
 
@@ -198,6 +198,3 @@ public:
     void reset_statistics();     
 
 };
-
-
-#endif 

src/math/lp/indexed_value.h

@@ -35,19 +35,6 @@ public:
         m_value(v), m_index(i), m_other(other) {
     }
 
-    indexed_value(const indexed_value & iv) {
-        m_value = iv.m_value;
-        m_index = iv.m_index;
-        m_other = iv.m_other;
-    }
-
-    indexed_value & operator=(const indexed_value & right_side) {
-        m_value = right_side.m_value;
-        m_index = right_side.m_index;
-        m_other = right_side.m_other;
-        return *this;
-    }
-
     const T & value() const {
         return m_value;
     }

src/math/lp/lp_settings.h

@@ -24,6 +24,7 @@ Revision History:
 #include <algorithm>
 #include <limits>
 #include <iomanip>
+#include <cstring>
 #include "math/lp/lp_utils.h"
 #include "util/stopwatch.h"
 #include "math/lp/lp_types.h"

src/math/lp/numeric_pair.h

@@ -144,8 +144,6 @@ struct numeric_pair {
     explicit numeric_pair(const X & n) : x(n), y(0) {
     }
 
-    numeric_pair(const numeric_pair<T> & n) : x(n.x), y(n.y) {}
-
     template <typename X, typename Y>
     numeric_pair(X xp, Y yp) : x(convert_struct<T, X>::convert(xp)), y(convert_struct<T, Y>::convert(yp)) {}
 

src/math/simplex/model_based_opt.h

@@ -67,7 +67,6 @@ namespace opt {
         struct def {
             def(): m_div(1) {}
             def(row const& r, unsigned x);
-            def(def const& other): m_vars(other.m_vars), m_coeff(other.m_coeff), m_div(other.m_div) {}
             vector<var> m_vars;
             rational    m_coeff;
             rational    m_div; 

src/math/simplex/sparse_matrix.h

@@ -16,11 +16,11 @@ Notes:
 
 --*/
 
-#ifndef SPARSE_MATRIX_H_
-#define SPARSE_MATRIX_H_
+#pragma once
 
 #include "util/mpq_inf.h"
 #include "util/statistics.h"
+#include <cstring>
 
 namespace simplex {
 
@@ -271,6 +271,3 @@ namespace simplex {
     };
 
 };
-
-
-#endif

src/math/subpaving/subpaving_types.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef SUBPAVING_TYPES_H_
-#define SUBPAVING_TYPES_H_
+#pragma once
 
 namespace subpaving {
 
@@ -34,7 +33,6 @@ class power : public std::pair<var, unsigned> {
 public:
     power():std::pair<var, unsigned>() {}
     power(var v, unsigned d):std::pair<var, unsigned>(v, d) {}
-    power(power const & p):std::pair<var, unsigned>(p) {}
     var x() const { return first; }
     var get_var() const { return first; }
     unsigned degree() const { return second; }
@@ -47,6 +45,4 @@ struct display_var_proc {
     virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
 };
 
-};
-
-#endif
+}

src/muz/base/dl_context.cpp

@@ -1231,14 +1231,14 @@ namespace datalog {
         }
         else {
             for (unsigned i = 0; i < queries.size(); ++i) {
-                if (queries.size() > 1) out << "(push)\n";
+                if (queries.size() > 1) out << "(push 1)\n";
                 out << "(assert ";
                 expr_ref q(m);
                 q = m.mk_not(queries[i].get());
                 PP(q);
                 out << ")\n";
                 out << "(check-sat)\n";
-                if (queries.size() > 1) out << "(pop)\n";
+                if (queries.size() > 1) out << "(pop 1)\n";
             }
         }
     }

src/muz/spacer/spacer_manager.cpp

@@ -141,12 +141,12 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector<datalog::
 
     out << to_string() << "\n";
     for (auto* r : rules) {
-        out << "(push)\n";
+        out << "(push 1)\n";
         out << "(assert (not\n";
         rm.display_smt2(*r, out);
         out << "))\n";
         out << "(check-sat)\n";
-        out << "(pop)\n";
+        out << "(pop 1)\n";
     }
 }
 

src/muz/spacer/spacer_util.cpp

@@ -124,13 +124,13 @@ namespace spacer {
         out << "(define-fun mbp_benchmark_fml () Bool\n  ";
         out << mk_pp(fml, m) << ")\n\n";
 
-        out << "(push)\n"
+        out << "(push 1)\n"
             << "(assert mbp_benchmark_fml)\n"
             << "(check-sat)\n"
             << "(mbp mbp_benchmark_fml (";
         for (auto v : vars) {out << mk_pp(v, m) << " ";}
         out << "))\n"
-            << "(pop)\n"
+            << "(pop 1)\n"
             << "(exit)\n";
     }
 

src/muz/transforms/dl_mk_array_blast.cpp

@@ -322,18 +322,18 @@ namespace datalog {
         if (!m_ctx.array_blast ()) {
             return nullptr;
         }
-        rule_set* rules = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
         rules->inherit_predicates(source);
-        rule_set::iterator it = source.begin(), end = source.end();
         bool change = false;
-        for (; !m_ctx.canceled() && it != end; ++it) {
-            change = blast(**it, *rules) || change;
+        for (rule* r : source) {
+            if (m_ctx.canceled())
+                return nullptr;
+            change = blast(*r, *rules) || change;
         }
         if (!change) {
-            dealloc(rules);
             rules = nullptr;
         }        
-        return rules;        
+        return rules.detach();        
     }
 
 };

src/muz/transforms/dl_mk_array_eq_rewrite.cpp

@@ -38,14 +38,14 @@ namespace datalog {
     rule_set * mk_array_eq_rewrite::operator()(rule_set const & source)
     {
         m_src_set = &source;
-        rule_set * result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
         result->inherit_predicates(source);
-        m_dst = result;
+        m_dst = result.get();
         m_src_manager = &source.get_rule_manager();
         for (rule * rp : source) {
             instantiate_rule(*rp, *result);
         }
-        return result;
+        return result.detach();
     }
 
     void mk_array_eq_rewrite::instantiate_rule(const rule& r, rule_set & dest)

src/muz/transforms/dl_mk_array_instantiation.cpp

@@ -27,7 +27,7 @@ Revision History:
 
 namespace datalog {
 
-  mk_array_instantiation::mk_array_instantiation(
+    mk_array_instantiation::mk_array_instantiation(
         context & ctx, unsigned priority):
         plugin(priority),
         m(ctx.get_manager()),
@@ -35,289 +35,253 @@ namespace datalog {
         m_a(m),
         eq_classes(m),
         ownership(m)
-  {
-  }
-
-  rule_set * mk_array_instantiation::operator()(rule_set const & source)
-  {
-    std::cout<<"Array Instantiation called with parameters :"
-             <<" enforce="<<m_ctx.get_params().xform_instantiate_arrays_enforce()
-             <<" nb_quantifier="<<m_ctx.get_params().xform_instantiate_arrays_nb_quantifier()
-             <<" slice_technique="<<m_ctx.get_params().xform_instantiate_arrays_slice_technique()
-             <<"\n";
-    std::cout<<"Input rules = \n";
-    source.display(std::cout);
-    src_set = &source;
-    rule_set * result = alloc(rule_set, m_ctx);
-    dst=result;
-    unsigned nbrules = source.get_num_rules();
-    src_manager = &source.get_rule_manager();
-    for(unsigned i =0;i<nbrules;i++)
     {
-      rule & r = *source.get_rule(i);
-      instantiate_rule(r, *result);
-    }
-    std::cout<<"\n\nOutput rules = \n";
-    result->display(std::cout);
-    return result;
-  }
-
-  void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest)
-  {
-    //Reset everything
-    selects.reset();
-    eq_classes.reset();
-    cnt = src_manager->get_counter().get_max_rule_var(r)+1;
-    done_selects.reset();
-    ownership.reset();
-
-    expr_ref_vector phi(m);
-    expr_ref_vector preds(m);
-    expr_ref new_head = create_head(to_app(r.get_head()));
-    unsigned nb_predicates = r.get_uninterpreted_tail_size();
-    unsigned tail_size = r.get_tail_size();
-    for(unsigned i=0;i<nb_predicates;i++)
-    {
-      preds.push_back(r.get_tail(i));
-    }
-    for(unsigned i=nb_predicates;i<tail_size;i++)
-    {
-      phi.push_back(r.get_tail(i));
     }
 
-    //Retrieve selects
-    for(unsigned i=0;i<phi.size();i++)
-      retrieve_selects(phi[i].get());
-
-    //Rewrite the predicates
-    expr_ref_vector new_tail(m);
-    for(unsigned i=0;i<preds.size();i++)
-    {
-      new_tail.append(instantiate_pred(to_app(preds[i].get())));
-    }
-    new_tail.append(phi);
-    for(obj_map<expr, var*>::iterator it = done_selects.begin(); it!=done_selects.end(); ++it)
-    {
-      expr_ref tmp(m);
-      tmp = &it->get_key();
-      new_tail.push_back(m.mk_eq(it->get_value(), tmp));
-    }
-    proof_ref pr(m);
-    src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name());
-  }
-
-  expr_ref mk_array_instantiation::create_head(app* old_head)
-  {
-     expr_ref_vector new_args(m);
-     for(unsigned i=0;i<old_head->get_num_args();i++)
-     {
-       expr*arg = old_head->get_arg(i);
-       if(m_a.is_array(get_sort(arg)))
-       {
-         for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++)
-         {
-           expr_ref_vector dummy_args(m);
-           dummy_args.push_back(arg);
-           for(unsigned i=0;i<get_array_arity(get_sort(arg));i++)
-           {
-             dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(arg), i)));
-             cnt++;
-           }
-           expr_ref select(m);
-           select = m_a.mk_select(dummy_args.size(), dummy_args.c_ptr());
-           new_args.push_back(select);
-           selects.insert_if_not_there(arg, ptr_vector<expr>());
-           selects[arg].push_back(select);
-         }
-         if(!m_ctx.get_params().xform_instantiate_arrays_enforce())
-             new_args.push_back(arg);
-       }
-       else
-        new_args.push_back(arg);
-     }
-     return create_pred(old_head, new_args);
-  }
-
-
-  void mk_array_instantiation::retrieve_selects(expr* e)
-  {
-    //If the expression is not a function application, we ignore it
-    if (!is_app(e)) {
-      return;
-    }
-    app*f=to_app(e);
-    //Call the function recursively on all arguments
-    unsigned nbargs = f->get_num_args();
-    for(unsigned i=0;i<nbargs;i++)
-    {
-      retrieve_selects(f->get_arg(i));
-    }
-    //If it is a select, then add it to selects
-    if(m_a.is_select(f))
-    {
-      SASSERT(!m_a.is_array(get_sort(e)));
-      selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>());
-      selects[f->get_arg(0)].push_back(e);
-    }
-    //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes
-    if(m_a.is_store(f))
-    {
-      eq_classes.merge(e, f->get_arg(0));
-    }
-    else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0))))
-    {
-      eq_classes.merge(f->get_arg(0), f->get_arg(1));
-    }
-  }
-
-
-  expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args)
-  {
-    expr_ref_vector res(m);
-    for(unsigned i=0;i<n_args.size(); i++)
-    {
-      if(m_a.is_select(n_args[i]))
-      {
-        app*select = to_app(n_args[i]);
-        for(unsigned j=1;j<select->get_num_args();j++)
-        {
-          res.push_back(select->get_arg(j));
+    rule_set * mk_array_instantiation::operator()(rule_set const & source)  {
+        std::cout<<"Array Instantiation called with parameters :"
+                 <<" enforce="<<m_ctx.get_params().xform_instantiate_arrays_enforce()
+                 <<" nb_quantifier="<<m_ctx.get_params().xform_instantiate_arrays_nb_quantifier()
+                 <<" slice_technique="<<m_ctx.get_params().xform_instantiate_arrays_slice_technique()
+                 <<"\n";
+        std::cout<<"Input rules = \n";
+        source.display(std::cout);
+        src_set = &source;
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
+        dst = result.get();
+        unsigned nbrules = source.get_num_rules();
+        src_manager = &source.get_rule_manager();
+        for(unsigned i = 0; i < nbrules; i++) {
+            rule & r = *source.get_rule(i);
+            instantiate_rule(r, *result);
         }
-      }
+        std::cout<<"\n\nOutput rules = \n";
+        result->display(std::cout);
+        return result.detach();
     }
-    return res;
-  }
 
-  expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args)
-  {
-    expr_ref_vector new_args(m);
-    new_args.append(n_args);
-    new_args.append(getId(old_pred, n_args));
-    for(unsigned i=0;i<new_args.size();i++)
-    {
-      if(m_a.is_select(new_args[i].get()))
-      {
-        new_args[i] = mk_select_var(new_args[i].get());
-      }
-    }
-    sort_ref_vector new_sorts(m);
-    for(unsigned i=0;i<new_args.size();i++)
-      new_sorts.push_back(get_sort(new_args[i].get()));
-    expr_ref res(m);
-    func_decl_ref fun_decl(m);
-    fun_decl = m.mk_func_decl(symbol((old_pred->get_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range());
-    m_ctx.register_predicate(fun_decl, false);
-    if(src_set->is_output_predicate(old_pred->get_decl()))
-      dst->set_output_predicate(fun_decl);
-    res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr());
-    return res;
-  }
+    void mk_array_instantiation::instantiate_rule(const rule& r, rule_set & dest) {
+        //Reset everything
+        selects.reset();
+        eq_classes.reset();
+        cnt = src_manager->get_counter().get_max_rule_var(r)+1;
+        done_selects.reset();
+        ownership.reset();
 
-  var * mk_array_instantiation::mk_select_var(expr* select)
-  {
-    var*result;
-    if(!done_selects.find(select, result))
-    {
-      ownership.push_back(select);
-      result = m.mk_var(cnt, get_sort(select));
-      cnt++;
-      done_selects.insert(select, result);
-    }
-    return result;
-  }
-
-  expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select)
-  {
-    app*s = to_app(select);
-    expr_ref res(m);
-    expr_ref_vector args(m);
-    args.push_back(array);
-    for(unsigned i=1; i<s->get_num_args();i++)
-    {
-      args.push_back(s->get_arg(i));
-    }
-    res = m_a.mk_select(args.size(), args.c_ptr());
-    return res;
-  }
-
-  expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array)
-  {
-    expr_ref_vector all_selects(m);
-    for(expr_equiv_class::iterator it = eq_classes.begin(array);
-        it != eq_classes.end(array); ++it)
-    {
-      selects.insert_if_not_there(*it, ptr_vector<expr>());
-      ptr_vector<expr>& select_ops = selects[*it];
-      for(unsigned i=0;i<select_ops.size();i++)
-      {
-        all_selects.push_back(rewrite_select(array, select_ops[i]));
-      }
-    }
-    if(all_selects.empty())
-    {
-      expr_ref_vector dummy_args(m);
-      dummy_args.push_back(array);
-      for(unsigned i=0;i<get_array_arity(get_sort(array));i++)
-      {
-        dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(array), i)));
-        cnt++;
-      }
-      all_selects.push_back(m_a.mk_select(dummy_args.size(), dummy_args.c_ptr()));
-    }
-    return all_selects;
-  }
-
-
-  expr_ref_vector mk_array_instantiation::instantiate_pred(app*old_pred)
-  {
-
-    unsigned nb_old_args=old_pred->get_num_args();
-    //Stores, for each old position, the list of a new possible arguments
-    vector<expr_ref_vector> arg_correspondance;
-    for(unsigned i=0;i<nb_old_args;i++)
-    {
-      expr_ref arg(old_pred->get_arg(i), m);
-      if(m_a.is_array(get_sort(arg)))
-      {
-        vector<expr_ref_vector> arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg));
-        arg_correspondance.append(arg_possibilities);
-        if(!m_ctx.get_params().xform_instantiate_arrays_enforce())
-        {
-          expr_ref_vector tmp(m);
-          tmp.push_back(arg);
-          arg_correspondance.push_back(tmp);
+        expr_ref_vector phi(m);
+        expr_ref_vector preds(m);
+        expr_ref new_head = create_head(to_app(r.get_head()));
+        unsigned nb_predicates = r.get_uninterpreted_tail_size();
+        unsigned tail_size = r.get_tail_size();
+        for(unsigned i=0;i<nb_predicates;i++) {
+            preds.push_back(r.get_tail(i));
         }
-      }
-      else
-      {
-        expr_ref_vector tmp(m);
-        tmp.push_back(arg);
-        arg_correspondance.push_back(tmp);
-      }
-    }
-    //Now, we need to deal with every combination
-
-    expr_ref_vector res(m);
-
-    svector<unsigned> chosen(arg_correspondance.size(), 0u);
-    while(true)
-    {
-      expr_ref_vector new_args(m);
-      for(unsigned i=0;i<chosen.size();i++)
-      {
-          new_args.push_back(arg_correspondance[i][chosen[i]].get());
-      }
-      res.push_back(create_pred(old_pred, new_args));
-      unsigned pos=-1;
-      do
-      {
-        pos++;
-        if(pos==chosen.size())
-        {
-          return res;
+        for(unsigned i=nb_predicates;i<tail_size;i++) {
+            phi.push_back(r.get_tail(i));
+        }
+
+        //Retrieve selects
+        for(unsigned i=0;i<phi.size();i++)
+            retrieve_selects(phi[i].get());
+
+        //Rewrite the predicates
+        expr_ref_vector new_tail(m);
+        for(unsigned i=0;i<preds.size();i++) {
+            new_tail.append(instantiate_pred(to_app(preds[i].get())));
+        }
+        new_tail.append(phi);
+        for(obj_map<expr, var*>::iterator it = done_selects.begin(); it!=done_selects.end(); ++it)  {
+            expr_ref tmp(m);
+            tmp = &it->get_key();
+            new_tail.push_back(m.mk_eq(it->get_value(), tmp));
+        }
+        proof_ref pr(m);
+        src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.c_ptr()), new_head), pr, dest, r.name());
+    }
+
+    expr_ref mk_array_instantiation::create_head(app* old_head)  {
+        expr_ref_vector new_args(m);
+        for(unsigned i=0;i<old_head->get_num_args();i++) {
+            expr*arg = old_head->get_arg(i);
+            if(m_a.is_array(get_sort(arg))) {
+                for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++)  {
+                    expr_ref_vector dummy_args(m);
+                    dummy_args.push_back(arg);
+                    for(unsigned i=0;i<get_array_arity(get_sort(arg));i++) {
+                        dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(arg), i)));
+                        cnt++;
+                    }
+                    expr_ref select(m);
+                    select = m_a.mk_select(dummy_args.size(), dummy_args.c_ptr());
+                    new_args.push_back(select);
+                    selects.insert_if_not_there(arg, ptr_vector<expr>());
+                    selects[arg].push_back(select);
+                }
+                if(!m_ctx.get_params().xform_instantiate_arrays_enforce())
+                    new_args.push_back(arg);
+            }
+            else
+                new_args.push_back(arg);
+        }
+        return create_pred(old_head, new_args);
+    }
+    
+    
+    void mk_array_instantiation::retrieve_selects(expr* e) {
+        //If the expression is not a function application, we ignore it
+        if (!is_app(e)) {
+            return;
+        }
+        app*f=to_app(e);
+        //Call the function recursively on all arguments
+        unsigned nbargs = f->get_num_args();
+        for(unsigned i=0;i<nbargs;i++) {
+            retrieve_selects(f->get_arg(i));
+        }
+        //If it is a select, then add it to selects
+        if(m_a.is_select(f)) {
+            SASSERT(!m_a.is_array(get_sort(e)));
+            selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>());
+            selects[f->get_arg(0)].push_back(e);
+        }
+        //If it is a condition between arrays, for example the result of a store, then add it to the equiv_classes
+        if(m_a.is_store(f)) {
+            eq_classes.merge(e, f->get_arg(0));
+        }
+        else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) {
+            eq_classes.merge(f->get_arg(0), f->get_arg(1));
+        }
+    }
+
+
+    expr_ref_vector mk_array_instantiation::getId(app*old_pred, const expr_ref_vector& n_args)
+    {
+        expr_ref_vector res(m);
+        for(unsigned i=0;i<n_args.size(); i++) {
+            if(m_a.is_select(n_args[i])) {
+                app*select = to_app(n_args[i]);
+                for(unsigned j=1;j<select->get_num_args();j++) {
+                    res.push_back(select->get_arg(j));
+                }
+            }
+        }
+        return res;
+    }
+
+    expr_ref mk_array_instantiation::create_pred(app*old_pred, expr_ref_vector& n_args)
+    {
+        expr_ref_vector new_args(m);
+        new_args.append(n_args);
+        new_args.append(getId(old_pred, n_args));
+        for(unsigned i=0;i<new_args.size();i++) {
+                if(m_a.is_select(new_args[i].get())) {
+                    new_args[i] = mk_select_var(new_args[i].get());
+                }
+        }
+        sort_ref_vector new_sorts(m);
+        for(unsigned i=0;i<new_args.size();i++)
+            new_sorts.push_back(get_sort(new_args[i].get()));
+        expr_ref res(m);
+        func_decl_ref fun_decl(m);
+        fun_decl = m.mk_func_decl(symbol((old_pred->get_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range());
+        m_ctx.register_predicate(fun_decl, false);
+        if(src_set->is_output_predicate(old_pred->get_decl()))
+            dst->set_output_predicate(fun_decl);
+        res=m.mk_app(fun_decl,new_args.size(), new_args.c_ptr());
+        return res;
+    }
+
+    var * mk_array_instantiation::mk_select_var(expr* select)
+    {
+        var*result;
+        if(!done_selects.find(select, result)) {
+            ownership.push_back(select);
+            result = m.mk_var(cnt, get_sort(select));
+            cnt++;
+            done_selects.insert(select, result);
+        }
+        return result;
+    }
+
+    expr_ref mk_array_instantiation::rewrite_select(expr*array, expr*select)
+    {
+        app*s = to_app(select);
+        expr_ref res(m);
+        expr_ref_vector args(m);
+        args.push_back(array);
+        for(unsigned i=1; i<s->get_num_args();i++)   {
+            args.push_back(s->get_arg(i));
+        }
+        res = m_a.mk_select(args.size(), args.c_ptr());
+        return res;
+    }
+
+    expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array)
+    {
+        expr_ref_vector all_selects(m);
+        for(expr_equiv_class::iterator it = eq_classes.begin(array);
+            it != eq_classes.end(array); ++it) {
+            selects.insert_if_not_there(*it, ptr_vector<expr>());
+            ptr_vector<expr>& select_ops = selects[*it];
+            for(unsigned i=0;i<select_ops.size();i++) {
+                all_selects.push_back(rewrite_select(array, select_ops[i]));
+            }
+        }
+        if(all_selects.empty()) {
+            expr_ref_vector dummy_args(m);
+            dummy_args.push_back(array);
+            for(unsigned i=0;i<get_array_arity(get_sort(array));i++) {
+                dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(array), i)));
+                cnt++;
+            }
+            all_selects.push_back(m_a.mk_select(dummy_args.size(), dummy_args.c_ptr()));
+        }
+        return all_selects;
+    }
+
+
+    expr_ref_vector mk_array_instantiation::instantiate_pred(app*old_pred)
+    {
+        unsigned nb_old_args=old_pred->get_num_args();
+        //Stores, for each old position, the list of a new possible arguments
+        vector<expr_ref_vector> arg_correspondance;
+        for(unsigned i=0;i<nb_old_args;i++) {
+            expr_ref arg(old_pred->get_arg(i), m);
+            if(m_a.is_array(get_sort(arg))) {
+                vector<expr_ref_vector> arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg));
+                arg_correspondance.append(arg_possibilities);
+                if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) {
+                    expr_ref_vector tmp(m);
+                    tmp.push_back(arg);
+                    arg_correspondance.push_back(tmp);
+                }
+            }
+            else {
+                expr_ref_vector tmp(m);
+                tmp.push_back(arg);
+                arg_correspondance.push_back(tmp);
+            }
+        }
+        //Now, we need to deal with every combination
+
+        expr_ref_vector res(m);
+        
+        svector<unsigned> chosen(arg_correspondance.size(), 0u);
+        while(true) {
+            expr_ref_vector new_args(m);
+            for(unsigned i=0;i<chosen.size();i++) {
+                new_args.push_back(arg_correspondance[i][chosen[i]].get());
+            }
+            res.push_back(create_pred(old_pred, new_args));
+            unsigned pos=-1;
+            do {
+                pos++;
+                if(pos==chosen.size()){
+                    return res;
+                }
+            }
+            while(chosen[pos]+1>=arg_correspondance[pos].size());
+            chosen[pos]++;
         }
-      }while(chosen[pos]+1>=arg_correspondance[pos].size());
-      chosen[pos]++;
     }
-  }
 }

src/muz/transforms/dl_mk_backwards.cpp

@@ -33,7 +33,7 @@ namespace datalog {
     rule_set * mk_backwards::operator()(rule_set const & source) {
         context& ctx = source.get_context();
         rule_manager& rm = source.get_rule_manager();
-        rule_set * result = alloc(rule_set, ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, ctx);
         unsigned sz = source.get_num_rules();
         rule_ref new_rule(rm);
         app_ref_vector tail(m);
@@ -72,7 +72,7 @@ namespace datalog {
             }
         }
         TRACE("dl", result->display(tout););
-        return result;
+        return result.detach();
     }
 
 };

src/muz/transforms/dl_mk_coalesce.cpp

@@ -172,7 +172,7 @@ namespace datalog {
     }    
         
     rule_set * mk_coalesce::operator()(rule_set const & source) {
-        rule_set* rules = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
         rules->inherit_predicates(source);
         rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
         for (; it != end; ++it) {
@@ -181,8 +181,8 @@ namespace datalog {
             for (unsigned i = 0; i < d_rules.size(); ++i) {
                 rule_ref r1(d_rules[i].get(), rm);
                 for (unsigned j = i + 1; j < d_rules.size(); ++j) {
-                    if (same_body(*r1.get(), *d_rules[j].get())) {
-                        merge_rules(r1, *d_rules[j].get());
+                    if (same_body(*r1.get(), *d_rules.get(j))) {
+                        merge_rules(r1, *d_rules.get(j));
                         d_rules[j] = d_rules.back();
                         d_rules.pop_back();
                         --j;
@@ -191,7 +191,7 @@ namespace datalog {
                 rules->add_rule(r1.get());
             }
         }
-        return rules;
+        return rules.detach();
     }
 
 };

src/muz/transforms/dl_mk_coi_filter.cpp

@@ -128,7 +128,8 @@ namespace datalog {
             func_decl * pred = r->get_decl();
             if (engine.get_fact(pred).is_reachable()) {
                 res->add_rule(r);
-            } else if (m_context.get_model_converter()) {
+            } 
+            else if (m_context.get_model_converter()) {
                 pruned_preds.insert(pred);
             }
         }

src/muz/transforms/dl_mk_interp_tail_simplifier.cpp

@@ -602,17 +602,17 @@ namespace datalog {
             return nullptr;
         }
 
-        rule_set * res = alloc(rule_set, m_context);
+        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
         if (transform_rules(source, *res)) {
             res->inherit_predicates(source);
             TRACE("dl",
                   source.display(tout);
                   res->display(tout););
-        } else {
-            dealloc(res);
+        } 
+        else {
             res = nullptr;
         }
-        return res;
+        return res.detach();
     }
 
 };

src/muz/transforms/dl_mk_loop_counter.cpp

@@ -68,7 +68,7 @@ namespace datalog {
         m_old2new.reset();
         m_new2old.reset();
         rule_manager& rm = source.get_rule_manager();
-        rule_set * result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
         unsigned sz = source.get_num_rules();
         rule_ref new_rule(rm);
         app_ref_vector tail(m);
@@ -118,7 +118,7 @@ namespace datalog {
         // model converter: remove references to extra argument.
         // proof converter: remove references to extra argument as well.
 
-        return result;
+        return result.detach();
     }
 
     rule_set * mk_loop_counter::revert(rule_set const & source) {

src/muz/transforms/dl_mk_magic_sets.cpp

@@ -345,7 +345,7 @@ namespace datalog {
         var_idx_set empty_var_idx_set;
         adorn_literal(goal_head, empty_var_idx_set);
 
-        rule_set * result = alloc(rule_set, m_context);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_context);
         result->inherit_predicates(source);
 
         while (!m_todo.empty()) {
@@ -373,7 +373,7 @@ namespace datalog {
 
         rule * back_to_goal_rule = m_context.get_rule_manager().mk(goal_head, 1, &adn_goal_head, nullptr);
         result->add_rule(back_to_goal_rule);
-        return result;
+        return result.detach();
     }
 };
 

src/muz/transforms/dl_mk_magic_symbolic.cpp

@@ -72,7 +72,7 @@ namespace datalog {
         }
         context& ctx = source.get_context();
         rule_manager& rm = source.get_rule_manager();
-        rule_set * result = alloc(rule_set, ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, ctx);
         unsigned sz = source.get_num_rules();
         rule_ref new_rule(rm);
         app_ref_vector tail(m);
@@ -109,7 +109,7 @@ namespace datalog {
             
         }
         TRACE("dl", result->display(tout););
-        return result;
+        return result.detach();
     }
 
     app_ref mk_magic_symbolic::mk_query(app* q) {

src/muz/transforms/dl_mk_quantifier_abstraction.cpp

@@ -329,7 +329,7 @@ namespace datalog {
         if (m_ctx.get_model_converter()) {
             m_mc = alloc(qa_model_converter, m);
         }
-        rule_set * result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
 
         for (unsigned i = 0; i < sz; ++i) {
             tail.reset();
@@ -354,7 +354,6 @@ namespace datalog {
         // proof converter: proofs are not necessarily preserved using this transformation.
 
         if (m_old2new.empty()) {
-            dealloc(result);
             dealloc(m_mc);
             result = nullptr;
         }
@@ -363,7 +362,7 @@ namespace datalog {
         }
         m_mc = nullptr;
 
-        return result;
+        return result.detach();
     }
 
 

src/muz/transforms/dl_mk_quantifier_instantiation.cpp

@@ -264,7 +264,7 @@ namespace datalog {
 
         expr_ref_vector conjs(m);
         quantifier_ref_vector qs(m);
-        rule_set * result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
 
         bool instantiated = false;
 
@@ -286,10 +286,9 @@ namespace datalog {
             result->inherit_predicates(source);
         }
         else {
-            dealloc(result);
             result = nullptr;
         }
-        return result;
+        return result.detach();
     }
 
 

src/muz/transforms/dl_mk_scale.cpp

@@ -120,7 +120,7 @@ namespace datalog {
             return nullptr;
         }
         rule_manager& rm = source.get_rule_manager();
-        rule_set * result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
         unsigned sz = source.get_num_rules();
         rule_ref new_rule(rm);
         app_ref_vector tail(m);
@@ -166,7 +166,7 @@ namespace datalog {
         }
         m_trail.reset();
         m_cache.reset();
-        return result;
+        return result.detach();
     }
 
     app_ref mk_scale::mk_pred(unsigned sigma_idx, app* q) {

src/muz/transforms/dl_mk_slice.cpp

@@ -841,11 +841,10 @@ namespace datalog {
         m_mc = smc.get();
         reset();
         saturate(src);
-        rule_set* result = alloc(rule_set, m_ctx);
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
         declare_predicates(src, *result);
         if (m_predicates.empty()) {
             // nothing could be sliced.
-            dealloc(result);
             return nullptr;
         }
         TRACE("dl", display(tout););        
@@ -859,7 +858,7 @@ namespace datalog {
         }
         m_ctx.add_proof_converter(spc.get());
         m_ctx.add_model_converter(smc.get());
-        return result;
+        return result.detach();
     }    
 
 };

src/muz/transforms/dl_mk_subsumption_checker.cpp

@@ -335,7 +335,7 @@ namespace datalog {
     rule_set * mk_subsumption_checker::operator()(rule_set const & source) {
         // TODO mc
         if (!m_context.get_params ().xform_subsumption_checker())
-          return nullptr;
+            return nullptr;
 
         m_have_new_total_rule = false;
         collect_ground_unconditional_rule_heads(source);
@@ -343,11 +343,10 @@ namespace datalog {
         scan_for_total_rules(source);
 
         m_have_new_total_rule = false;
-        rule_set * res = alloc(rule_set, m_context);
+        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
         bool modified = transform_rules(source, *res);
 
         if (!m_have_new_total_rule && !modified) {
-            dealloc(res);
             return nullptr;
         }
 
@@ -357,14 +356,12 @@ namespace datalog {
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
         while (m_have_new_total_rule) {
             m_have_new_total_rule = false;
-
-            rule_set * old = res;
+            scoped_ptr<rule_set> old = res.detach();
             res = alloc(rule_set, m_context);
             transform_rules(*old, *res);
-            dealloc(old);
         }
 
-        return res;
+        return res.detach();
     }
 
 };

src/muz/transforms/dl_mk_unbound_compressor.cpp

@@ -387,7 +387,7 @@ namespace datalog {
             }
         }
 
-        rule_set * result = static_cast<rule_set *>(nullptr);
+        scoped_ptr<rule_set> result;
         if (m_modified) {
             result = alloc(rule_set, m_context);
             unsigned fin_rule_cnt = m_rules.size();
@@ -397,7 +397,7 @@ namespace datalog {
             result->inherit_predicates(source);
         }
         reset();
-        return result;
+        return result.detach();
     }
 
 

src/muz/transforms/dl_mk_unfold.cpp

@@ -51,13 +51,12 @@ namespace datalog {
     }
         
     rule_set * mk_unfold::operator()(rule_set const & source) {
-        rule_set* rules = alloc(rule_set, m_ctx);
-        rule_set::iterator it = source.begin(), end = source.end();
-        for (; it != end; ++it) {
-            expand_tail(**it, 0, source, *rules);
+        scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
+        for (rule* r : source) {
+            expand_tail(*r, 0, source, *rules);
         }
         rules->inherit_predicates(source);
-        return rules;
+        return rules.detach();
     }
 
 };

src/nlsat/nlsat_solver.cpp

@@ -1961,6 +1961,13 @@ namespace nlsat {
             return new_lvl;
         }
 
+        struct scoped_reset_marks {
+            imp& i;
+            scoped_reset_marks(imp& i):i(i) {}
+            ~scoped_reset_marks() { if (i.m_num_marks > 0) { i.m_num_marks = 0; for (char& m : i.m_marks) m = 0; } }
+        };
+
+
         /**
            \brief Return true if the conflict was solved.
         */
@@ -1980,7 +1987,7 @@ namespace nlsat {
             m_num_marks = 0;
             m_lemma.reset();
             m_lemma_assumptions = nullptr;
-
+            scoped_reset_marks _sr(*this);
             resolve_clause(null_bool_var, *conflict_clause);
 
             unsigned top = m_trail.size();

src/opt/maxsmt.h

@@ -64,8 +64,6 @@ namespace opt {
             void set_value(lbool t) { value = t; }
             bool is_true() const { return value == l_true; }
             soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
-            soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {}
-            soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; }            
         };
         ast_manager&     m;
         maxsat_context&  m_c;        

src/opt/pb_sls.cpp

@@ -77,16 +77,6 @@ namespace smt {
                 m_value(m),
                 m_eq(true)
             {}
-            clause(clause const& cls):
-                m_lits(cls.m_lits),
-                m_weights(cls.m_weights.m()),
-                m_k(cls.m_k),
-                m_value(cls.m_value),
-                m_eq(cls.m_eq) {
-                for (unsigned i = 0; i < cls.m_weights.size(); ++i) {
-                    m_weights.push_back(cls.m_weights[i]);
-                }
-            }
         };
 
         struct stats {

src/qe/qe.cpp

@@ -1208,9 +1208,9 @@ namespace qe {
                 fml = mk_not(m, m.mk_iff(q, fml));
                 ast_smt_pp pp(m);
                 out << "; eliminate " << mk_pp(m_var, m) << "\n";
-                out << "(push)\n";
+                out << "(push 1)\n";
                 pp.display_smt2(out, fml);                
-                out << "(pop)\n\n";      
+                out << "(pop 1)\n\n";
 #if 0
                 DEBUG_CODE(
                     smt_params params;

src/qe/qe_arith_plugin.cpp

@@ -2412,24 +2412,21 @@ public:
         }
 
         bool update_bounds(contains_app& contains_x, expr* fml) {
-            bounds_proc* bounds = nullptr;
-            if (m_bounds_cache.find(contains_x.x(), fml, bounds)) {
+            bounds_proc* _bounds = nullptr;
+            if (m_bounds_cache.find(contains_x.x(), fml, _bounds)) {
                 return true;
             }
-            bounds = alloc(bounds_proc, m_util);
-
+            scoped_ptr<bounds_proc> bounds = alloc(bounds_proc, m_util);
             if (!update_bounds(*bounds, contains_x, fml, m_ctx.pos_atoms(), true)) {
-                dealloc(bounds);
                 return false;
             }
             if (!update_bounds(*bounds, contains_x, fml, m_ctx.neg_atoms(), false)) {
-                dealloc(bounds);
                 return false;
             }
             
             m_trail.push_back(contains_x.x());
             m_trail.push_back(fml);
-            m_bounds_cache.insert(contains_x.x(), fml, bounds);
+            m_bounds_cache.insert(contains_x.x(), fml, bounds.detach());
             return true;
         }
     };

src/qe/qe_arrays.cpp

@@ -899,12 +899,8 @@ namespace qe {
             expr_ref_vector idx;
             expr_ref_vector val;
             vector<rational> rval;
-            idx_val(expr_ref_vector & idx, expr_ref_vector & val, vector<rational> const& rval): idx(idx), val(val), rval(rval) {}
-            idx_val& operator=(idx_val const& o) {
-                idx.reset(); val.reset(); rval.reset();
-                idx.append(o.idx); val.append(o.val); rval.append(o.rval);
-                return *this;
-            }
+            idx_val(expr_ref_vector && idx, expr_ref_vector && val, vector<rational> && rval):
+              idx(std::move(idx)), val(std::move(val)), rval(std::move(rval)) {}
         };
         ast_manager&                m;
         array_util                  m_arr_u;
@@ -1049,8 +1045,7 @@ namespace qe {
                 }
                 if (is_new) {
                     // new repr, val, and sel const
-                    vector<rational> rvals = to_num(vals);
-                    m_idxs.push_back(idx_val(idxs, vals, rvals));
+                    m_idxs.push_back(idx_val(std::move(idxs), std::move(vals), to_num(vals)));
                     app_ref c (m.mk_fresh_const ("sel", val_sort), m);
                     m_sel_consts.push_back (c);
                     // substitute sel term with new const

src/qe/qsat.cpp

@@ -166,7 +166,9 @@ namespace qe {
         expr_ref val(m);
         for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
             app* p = m_preds[level - 1][j].get();            
-            eval(p, val);            
+            eval(p, val); 
+            if (!m.inc())
+                return;
             if (m.is_false(val)) {
                 m_asms.push_back(m.mk_not(p));
             }
@@ -179,6 +181,8 @@ namespace qe {
         
         for (unsigned i = level + 1; i < m_preds.size(); i += 2) {
             for (unsigned j = 0; j < m_preds[i].size(); ++j) {
+                if (!m.inc())
+                    return;
                 app* p = m_preds[i][j].get();
                 max_level lvl = m_elevel.find(p);
                 bool use = 

src/sat/sat_model_converter.cpp

@@ -208,7 +208,7 @@ namespace sat {
     }
 
     void model_converter::add_elim_stack(entry & e) {
-        e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv()));
+        e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, std::move(m_elim_stack)));
         // VERIFY(for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var())););
         stackv().reset();
     }

src/sat/sat_model_converter.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef SAT_MODEL_CONVERTER_H_
-#define SAT_MODEL_CONVERTER_H_
+#pragma once
 
 #include "sat/sat_types.h"
 #include "util/ref_vector.h"
@@ -51,12 +50,12 @@ namespace sat {
             unsigned        m_counter;
             unsigned        m_refcount;
             elim_stackv     m_stack;
-            elim_stack(elim_stack const& );
         public:
-            elim_stack(elim_stackv const& stack): 
+            elim_stack(elim_stack const&) = delete;
+            elim_stack(elim_stackv && stack):
                 m_counter(0),
                 m_refcount(0), 
-                m_stack(stack) {
+                m_stack(std::move(stack)) {
                 m_counter = ++counter;
             }
             ~elim_stack() { }
@@ -76,14 +75,6 @@ namespace sat {
             sref_vector<elim_stack> m_elim_stack;
             entry(kind k, bool_var v): m_var(v), m_kind(k) {}
         public:
-            entry(entry const & src):
-                m_var(src.m_var),
-                m_kind(src.m_kind),
-                m_clauses(src.m_clauses),
-                m_clause(src.m_clause)
-            {
-                m_elim_stack.append(src.m_elim_stack);
-            }
             bool_var var() const { return m_var; }
             kind get_kind() const { return m_kind; }
         };
@@ -166,5 +157,3 @@ namespace sat {
     }
 
 };
-
-#endif

src/smt/asserted_formulas.cpp

@@ -665,11 +665,12 @@ proof * asserted_formulas::get_inconsistency_proof() const {
         return nullptr;
     if (!m.proofs_enabled())
         return nullptr;
+    if (!m.inc())
+        return nullptr;
     for (justified_expr const& j : m_formulas) {
         if (m.is_false(j.get_fml()))
             return j.get_proof();
     }
-    UNREACHABLE();
     return nullptr;
 }
 

src/smt/old_interval.cpp

@@ -227,17 +227,8 @@ interval::interval(v_dependency_manager & m, rational const & val, bool open, bo
     }
 }
 
-interval::interval(interval const & other):
-    m_manager(other.m_manager),
-    m_lower(other.m_lower),
-    m_upper(other.m_upper),
-    m_lower_open(other.m_lower_open),
-    m_upper_open(other.m_upper_open),
-    m_lower_dep(other.m_lower_dep),
-    m_upper_dep(other.m_upper_dep) {
-}
-
 interval & interval::operator=(interval const & other) {
+    SASSERT(&m_manager == &other.m_manager);
     m_lower = other.m_lower;
     m_upper = other.m_upper;
     m_lower_open = other.m_lower_open;
@@ -247,6 +238,17 @@ interval & interval::operator=(interval const & other) {
     return *this;
 }
 
+interval & interval::operator=(interval && other) {
+    SASSERT(&m_manager == &other.m_manager);
+    m_lower = std::move(other.m_lower);
+    m_upper = std::move(other.m_upper);
+    m_lower_open = other.m_lower_open;
+    m_upper_open = other.m_upper_open;
+    m_lower_dep  = other.m_lower_dep;
+    m_upper_dep  = other.m_upper_dep;
+    return *this;
+}
+
 interval & interval::operator+=(interval const & other) {
     m_lower      += other.m_lower;
     m_upper      += other.m_upper;

src/smt/old_interval.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef OLD_INTERVAL_H_
-#define OLD_INTERVAL_H_
+#pragma once
 
 #include "util/rational.h"
 #include "util/dependency.h"
@@ -27,14 +26,12 @@ public:
     enum kind { MINUS_INFINITY, FINITE, PLUS_INFINITY };
 private:
     kind     m_kind;
-    rational m_value; 
-    explicit ext_numeral(kind k):m_kind(k) {}
+    rational m_value;
 public:
     ext_numeral():m_kind(FINITE) {} /* zero */
     explicit ext_numeral(bool plus_infinity):m_kind(plus_infinity ? PLUS_INFINITY : MINUS_INFINITY) {}
     explicit ext_numeral(rational const & val):m_kind(FINITE), m_value(val) {}
     explicit ext_numeral(int i):m_kind(FINITE), m_value(i) {}
-    ext_numeral(ext_numeral const & other):m_kind(other.m_kind), m_value(other.m_value) {}
     bool is_infinite() const { return m_kind != FINITE; }
     bool sign() const { return m_kind == MINUS_INFINITY || (m_kind == FINITE && m_value.is_neg()); }
     void neg();
@@ -78,13 +75,14 @@ class old_interval {
     v_dependency * join_opt(v_dependency * d1, v_dependency * d2, v_dependency * opt1, v_dependency * opt2);
 
 public:
-    explicit old_interval(v_dependency_manager & m);  
+    explicit old_interval(v_dependency_manager & m);
     explicit old_interval(v_dependency_manager & m, rational const & lower, bool l_open, v_dependency * l_dep, rational const & upper, bool u_open, v_dependency * u_dep);
     explicit old_interval(v_dependency_manager & m, rational const & val, v_dependency * l_dep = nullptr, v_dependency * u_dep = nullptr);
     explicit old_interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d);
     explicit old_interval(v_dependency_manager & m, ext_numeral const& lower, bool l_open, v_dependency * l_dep, ext_numeral const & upper, bool u_open, v_dependency * u_dep);
-    old_interval(old_interval const & other);
-    
+    old_interval(const old_interval&) = default;
+    old_interval(old_interval&&) = default;
+
     bool minus_infinity() const { return m_lower.is_infinite(); }
     bool plus_infinity() const { return m_upper.is_infinite(); }
     bool is_lower_open() const { return m_lower_open; }
@@ -94,6 +92,7 @@ public:
     rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); }
     rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); }
     old_interval & operator=(old_interval const & other);
+    old_interval & operator=(old_interval && other);
     old_interval & operator+=(old_interval const & other);
     old_interval & operator-=(old_interval const & other);
     old_interval & operator*=(old_interval const & other);
@@ -128,12 +127,5 @@ inline old_interval operator/(old_interval const & i1, old_interval const & i2)
 inline old_interval expt(old_interval const & i, unsigned n) { old_interval tmp(i); tmp.expt(n); return tmp; }
 inline std::ostream & operator<<(std::ostream & out, old_interval const & i) { i.display(out); return out; }
 
-struct interval_detail{};
-inline std::pair<old_interval, interval_detail> wd(old_interval const & i) { interval_detail d; return std::make_pair(i, d); }
-inline std::ostream & operator<<(std::ostream & out, std::pair<old_interval, interval_detail> const & p) { p.first.display_with_dependencies(out); return out; }
-
 // allow "customers" of this file to keep using interval
 #define interval old_interval
-
-#endif /* OLD_INTERVAL_H_ */
-

src/smt/seq_regex.cpp

@@ -101,6 +101,8 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var());
         VERIFY(str().is_in_re(e, s, r));
 
+        std::cout << "SEQ REGEX P_IN_RE" << std::endl;
+
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         // convert negative negative membership literals to positive
@@ -144,11 +146,11 @@ namespace smt {
     }
 
     void seq_regex::propagate_accept(literal lit) {
+        std::cout << "SEQ REGEX P_ACCEPT" << std::endl;
         if (!propagate(lit))
             m_to_propagate.push_back(lit);
     }
 
-       
     // s in R[if(p,R1,R2)] & p => s in R[R1]
     // s in R[if(p,R1,R2)] & ~p => s in R[R2]
 
@@ -195,13 +197,25 @@ namespace smt {
         VERIFY(sk().is_accept(e, s, i, idx, r));
         expr_ref is_nullable(m), d(r, m);
 
+
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
-        // std::cout << "SEQ REGEX PROPOGATE: " << mk_pp(e, m) << std::endl;
+        std::cout << "SEQ REGEX P" << std::endl;
+        // << mk_pp(e, m) << std::endl;
 
         if (block_unfolding(lit, idx))
             return true;
 
+        literal_vector conds;
+        conds.push_back(~lit);
+        if (!unfold_cofactors(d, conds)) 
+            return false;
+
+        if (re().is_empty(d)) {
+            th.add_axiom(conds);
+            return true;
+        }
+
         // s in R & len(s) <= i => nullable(R)
         literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
         switch (ctx.get_assignment(len_s_le_i)) {
@@ -209,17 +223,18 @@ namespace smt {
             ctx.mark_as_relevant(len_s_le_i);
             return false;
         case l_true: 
-            is_nullable = seq_rw().is_nullable(r);
+            std::cout << "is_nullable -- from prop" << std::endl;
+            is_nullable = seq_rw().is_nullable(d);
             rewrite(is_nullable);
-            th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
+            conds.push_back(~len_s_le_i);
+            conds.push_back(th.mk_literal(is_nullable));            
+            th.add_axiom(conds);
             return true;
         case l_false:
             break;
         }
 
-        literal_vector conds;
-        if (!unfold_cofactors(d, conds)) 
-            return false;
+        std::cout << "...MK DERIVATIVE" << std::endl;
 
         // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
         expr_ref head = th.mk_nth(s, i);
@@ -227,7 +242,6 @@ namespace smt {
         rewrite(d);
 
         literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d));
-        conds.push_back(~lit);
         conds.push_back(len_s_le_i);
         conds.push_back(acc_next);
         th.add_axiom(conds);
@@ -336,6 +350,7 @@ namespace smt {
      *
      */
     void seq_regex::propagate_is_non_empty(literal lit) {
+        std::cout << "SEQ REGEX P_NE" << std::endl;
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_non_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);
@@ -377,6 +392,7 @@ namespace smt {
       is_empty(r, u) is true if r is a member of u
      */
     void seq_regex::propagate_is_empty(literal lit) {
+        std::cout << "SEQ REGEX P_E" << std::endl;
         expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
         VERIFY(sk().is_is_empty(e, r, u));
         expr_ref is_nullable = seq_rw().is_nullable(r);

src/smt/smt_model_finder.cpp

@@ -2386,9 +2386,9 @@ namespace smt {
                 expr * e = q->get_expr();
                 reset_cache();
                 if (!m.inc()) return;
-                SASSERT(m_ttodo.empty());
-                SASSERT(m_ftodo.empty());
-
+                m_ttodo.reset();
+                m_ftodo.reset();
+  
                 if (is_clause(m, e)) {
                     process_clause(e);
                 }

src/tactic/core/reduce_invertible_tactic.cpp

@@ -196,7 +196,6 @@ private:
         case OP_BSHL:
         case OP_BASHR:
         case OP_BLSHR:
-        case OP_BOR:
             model = rational::zero();
             return true;
 

src/test/mpff.cpp

@@ -16,7 +16,8 @@ Author:
 Revision History:
 
 --*/
-#include<sstream>
+#include <sstream>
+#include <cstring>
 #include "util/mpff.h"
 #include "util/mpz.h"
 #include "util/mpq.h"

src/test/old_interval.cpp

@@ -140,6 +140,7 @@ class interval_tester {
         std::cerr << l(-10, true) << "\n";
         std::cerr << r(10, true) << "\n";
         std::cerr << b(2, 10) << "\n";
+#if 0
         std::cerr << wd(b(-5, 5, true, false, 1, 2) * b(-5, 5, false, true, 3, 4)) << "\n";
         std::cerr << wd(l(2, false, 1) / b(2, 6, false, false, 2, 3)) << "\n";
         std::cerr << wd(expt(b(-2, 3, true, false, 1, 2), 2)) << "\n";
@@ -148,6 +149,7 @@ class interval_tester {
         std::cerr << wd(expt(b(0, 3, true, false, 1, 2), 2)) << "\n";
         std::cerr << wd(expt(b(-4, -2, true, false, 1, 2), 2)) << "\n";
         std::cerr << b(2, 10, false, false, 1, 2) << " * " << l(10, false, 3).inv() << " = " << wd(b(2, 10, false, false, 1, 2) / l(10, false, 3)) << "\n";
+#endif
         std::cerr << b(-2, -1, false, true) << " * " << b(-3,0) << " = "; std::cerr.flush();
         std::cerr << (b(-2, -1, false, true) * b(-3,0)) << "\n";
         std::cerr << b(1, 2, true, false) << " * " << b(0,3) << " = "; std::cerr.flush();

src/test/theory_pb.cpp

@@ -90,7 +90,7 @@ private:
     void fuzz_round(unsigned& num_rounds, unsigned lvl) {
         unsigned num_rounds2 = 0;
         lbool is_sat = l_true;    
-        std::cout << "(push)\n";
+        std::cout << "(push 1)\n";
         ctx.push();
         unsigned r = 0;
         while (is_sat == l_true && r <= num_rounds + 1) {
@@ -105,7 +105,7 @@ private:
         num_rounds = r;
         std::cout << "; number of rounds: " << num_rounds << " level: " << lvl << "\n";
         ctx.pop(1);
-        std::cout << "(pop)\n";
+        std::cout << "(pop 1)\n";
     }
 
 };

src/util/array_map.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef ARRAY_MAP_H_
-#define ARRAY_MAP_H_
+#pragma once
 
 #include "util/vector.h"
 #include "util/optional.h"
@@ -40,9 +39,9 @@ class array_map {
         entry(Key const & k, Data const & d, unsigned t): m_key(k), m_data(d), m_timestamp(t) {}
     };
 
-    unsigned                 m_timestamp;
-    unsigned                 m_garbage;
-    unsigned                 m_non_garbage;
+    unsigned                 m_timestamp = 0;
+    unsigned                 m_garbage = 0;
+    unsigned                 m_non_garbage = 0;
     static const unsigned    m_gc_threshold = 10000;
     vector<optional<entry>, CallDestructors > m_map;
     Plugin                   m_plugin;
@@ -76,7 +75,10 @@ class array_map {
 
 public:
 
-    array_map(Plugin const & p = Plugin()):m_timestamp(0), m_garbage(0), m_non_garbage(0), m_plugin(p) {}
+    array_map() = default;
+    array_map(array_map&&) noexcept = default;
+    array_map(Plugin const & p) : m_plugin(p) {}
+
     ~array_map() { really_flush(); }
 
     bool contains(Key const & k) const {
@@ -155,5 +157,3 @@ public:
     }
 
 };
-
-#endif /* ARRAY_MAP_H_ */

src/util/buffer.h

@@ -21,7 +21,7 @@ Revision History:
 --*/
 #pragma once
 
-#include<string.h>
+#include <type_traits>
 #include "util/memory_manager.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
@@ -39,10 +39,14 @@ protected:
     }
 
     void expand() {
+        static_assert(std::is_nothrow_move_constructible<T>::value, "");
         unsigned new_capacity = m_capacity << 1;
         T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
         for (unsigned i = 0; i < m_pos; ++i) {
             new (&new_buffer[i]) T(std::move(m_buffer[i]));
+            if (CallDestructors) {
+                m_buffer[i].~T();
+            }
         }
         free_memory();
         m_buffer              = new_buffer;

src/util/checked_int64.h

@@ -21,8 +21,7 @@ Revision History:
 
 --*/
 
-#ifndef CHECKED_INT64_H_
-#define CHECKED_INT64_H_
+#pragma once
 
 #include "util/z3_exception.h"
 #include "util/rational.h"
@@ -38,7 +37,6 @@ public:
 
     checked_int64(): m_value(0) {}
     checked_int64(int64_t v): m_value(v) {}
-    checked_int64(checked_int64 const& other) { m_value = other.m_value; }
 
     class overflow_exception : public z3_exception {
         char const * msg() const override { return "checked_int64 overflow/underflow";}
@@ -217,5 +215,3 @@ inline checked_int64<CHECK> operator*(checked_int64<CHECK> const& a, checked_int
     result *= b;
     return result;
 }
-
-#endif

src/util/hashtable.h

@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef HASHTABLE_H_
-#define HASHTABLE_H_
+#pragma once
+
 #include "util/debug.h"
 #include <ostream>
 #include "util/util.h"
@@ -269,6 +269,19 @@ public:
             m_st_collision = 0;
         });
     }
+
+    core_hashtable(core_hashtable && source) noexcept :
+        HashProc(source),
+        EqProc(source),
+        m_table(nullptr) {
+        m_capacity    = source.m_capacity;
+        std::swap(m_table, source.m_table);
+        m_size        = source.m_size;
+        m_num_deleted = 0;
+        HS_CODE({
+            m_st_collision = 0;
+        });
+    }
     
     ~core_hashtable() {
         delete_table();
@@ -736,6 +749,3 @@ public:
                   EqProc const & e = EqProc()):
         core_hashtable<int_hash_entry<INT_MIN, INT_MIN + 1>, HashProc, EqProc>(initial_capacity, h, e) {}
 };
-
-
-#endif /* HASHTABLE_H_ */

src/util/hwf.h

@@ -16,10 +16,10 @@ Author:
 Revision History:
 
 --*/
-#ifndef HWF_H_
-#define HWF_H_
+#pragma once
 
-#include<string>
+#include <cstring>
+#include <string>
 #include "util/mpz.h"
 #include "util/mpq.h"
 #include "util/mpf.h"
@@ -36,9 +36,6 @@ class hwf {
     }
 
 public:    
-    hwf() {}
-    hwf(hwf const & other) { this->value = other.value; }
-    ~hwf() {}   
     void swap(hwf & other) { double t = value; value = other.value; other.value = t; }
 };
 
@@ -172,5 +169,3 @@ protected:
 
 typedef _scoped_numeral<hwf_manager> scoped_hwf;
 typedef _scoped_numeral_vector<hwf_manager> scoped_hwf_vector;
-
-#endif

src/util/inf_rational.h

@@ -17,8 +17,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef INF_RATIONAL_H_
-#define INF_RATIONAL_H_
+#pragma once
+
 #include<stdlib.h>
 #include<string>
 #include "util/debug.h"
@@ -67,11 +67,6 @@ class inf_rational {
 
     inf_rational() {}
 
-    inf_rational(const inf_rational & r): 
-        m_first(r.m_first),
-        m_second(r.m_second)
-     {}
-
     explicit inf_rational(int n):
         m_first(rational(n)),
         m_second(rational())
@@ -470,5 +465,3 @@ inline inf_rational abs(const inf_rational & r) {
     }
     return result;
 }
-
-#endif /* INF_RATIONAL_H_ */

src/util/inf_s_integer.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef INF_S_INTEGER_H_
-#define INF_S_INTEGER_H_
+#pragma once
 
 #include "util/s_integer.h"
 #include "util/rational.h"
@@ -47,8 +46,6 @@ class inf_s_integer {
 
     inf_s_integer():m_first(0), m_second(0) {}
 
-    inf_s_integer(const inf_s_integer & r):m_first(r.m_first), m_second(r.m_second) {}
-
     explicit inf_s_integer(int n):m_first(n), m_second(0) {}
     explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); }
     explicit inf_s_integer(s_integer const& r, bool pos_inf):m_first(r.get_int()), m_second(pos_inf ? 1 : -1) {}
@@ -345,7 +342,3 @@ inline inf_s_integer abs(const inf_s_integer & r) {
     }
     return result;
 }
-
-
-#endif /* INF_S_INTEGER_H_ */
-

src/util/mpf.cpp

@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include<sstream>
 #include<iomanip>
 #include "util/mpf.h"

src/util/mpf.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPF_H_
-#define MPF_H_
+#pragma once
 
 #include<string>
 #include "util/mpz.h"
@@ -45,18 +44,13 @@ class mpf {
     unsigned sign:1; // counts as one sbit.
     mpz significand;
     mpf_exp_t exponent;
-    mpf & operator=(mpf const & other) { UNREACHABLE(); return *this; }
     void set(unsigned _ebits, unsigned _sbits);
 public:
     mpf();
     mpf(unsigned ebits, unsigned sbits);
-    mpf(mpf && other) :
-        ebits(other.ebits),
-        sbits(other.sbits),
-        sign(other.sign),
-        significand(std::move(other.significand)),
-        exponent(other.exponent) {}
+    mpf(mpf &&) = default;
     ~mpf();
+    mpf & operator=(mpf const & other) = delete;
     unsigned get_ebits() const { return ebits; }
     unsigned get_sbits() const { return sbits; }
     void swap(mpf & other);
@@ -325,5 +319,3 @@ public:
 };
 
 typedef _scoped_numeral_vector<mpf_manager> scoped_mpf_vector;
-
-#endif

src/util/mpfx.cpp

@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include<sstream>
 #include<iomanip>
 #include "util/mpfx.h"

src/util/mpq.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPQ_H_
-#define MPQ_H_
+#pragma once
 
 #include "util/mpz.h"
 #include "util/trace.h"
@@ -27,11 +26,11 @@ class mpq {
     mpz m_den;
     friend class mpq_manager<true>;
     friend class mpq_manager<false>;
-    mpq & operator=(mpq const & other) { UNREACHABLE(); return *this; }
 public:
     mpq(int v):m_num(v), m_den(1) {}
     mpq():m_den(1) {}
-    mpq(mpq && other) : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {}
+    mpq(mpq &&) = default;
+    mpq & operator=(mpq const &) = delete;
     void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
     mpz const & numerator() const { return m_num; }
     mpz const & denominator() const { return m_den; }
@@ -862,6 +861,3 @@ typedef mpq_manager<false> unsynch_mpq_manager;
 typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;
 typedef _scoped_numeral<synch_mpq_manager> scoped_synch_mpq;
 typedef _scoped_numeral_vector<unsynch_mpq_manager> scoped_mpq_vector;
-
-#endif /* MPQ_H_ */
-

src/util/mpz.cpp

@@ -16,6 +16,7 @@ Author:
 Revision History:
 
 --*/
+#include <cstring>
 #include <sstream>
 #include <iomanip>
 #include "util/mpz.h"

src/util/mpz.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef MPZ_H_
-#define MPZ_H_
+#pragma once
 
 #include<string>
 #include "util/mutex.h"
@@ -104,10 +103,10 @@ public:
     mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz():m_val(0), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);}
-    mpz(mpz && other) : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {
+    mpz(mpz && other) noexcept : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {
         std::swap(m_ptr, other.m_ptr);
-        unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o;
-        unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k;
+        m_owner = other.m_owner;
+        m_kind = other.m_kind;
     }
     void swap(mpz & other) { 
         std::swap(m_val, other.m_val);
@@ -734,6 +733,3 @@ typedef mpz_manager<false> unsynch_mpz_manager;
 typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;
 typedef _scoped_numeral<synch_mpz_manager> scoped_synch_mpz;
 typedef _scoped_numeral_vector<unsynch_mpz_manager> scoped_mpz_vector;
-
-#endif /* MPZ_H_ */
-

src/util/obj_ref.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef OBJ_REF_H_
-#define OBJ_REF_H_
+#pragma once
 
 /**
    Smart pointer for T objects.
@@ -53,7 +52,7 @@ public:
         inc_ref();
     }
 
-    obj_ref(obj_ref && other) : m_obj(nullptr), m_manager(other.m_manager) {
+    obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) {
         std::swap(m_obj, other.m_obj);
     }
 
@@ -146,5 +145,3 @@ inline void dec_range_ref(IT const & begin, IT const & end, TManager & m) {
         }
     }
 }
-
-#endif /* OBJ_REF_H_ */

src/util/optional.h

@@ -18,8 +18,7 @@ Revision History:
 
 --*/
 
-#ifndef OPTIONAL_H_
-#define OPTIONAL_H_
+#pragma once
 
 template<class T>
 class optional {
@@ -47,6 +46,11 @@ public:
         construct(val);
     }
 
+    optional(T && val) noexcept : m_obj(nullptr), m_initialized(0) {
+        std::swap(m_obj, val.m_obj);
+        std::swap(m_initialized, val.m_initialized);
+    }
+
     optional(const optional<T> & val):
         m_initialized(0) {
         if (val.m_initialized == 1) {
@@ -160,7 +164,3 @@ public:
     
     T * & operator*() { return m_ptr; }
 };
-
-
-#endif /* OPTIONAL_H_ */
-

src/util/rational.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef RATIONAL_H_
-#define RATIONAL_H_
+#pragma once
 
 #include "util/mpq.h"
 
@@ -41,7 +40,7 @@ public:
     rational() {}
     
     rational(rational const & r) { m().set(m_val, r.m_val); }
-    rational(rational && r) : m_val(std::move(r.m_val)) {}
+    rational(rational&&) = default;
 
     explicit rational(int n) { m().set(m_val, n); }
 
@@ -576,7 +575,3 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati
   rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
   return result;
 }
-
-
-#endif /* RATIONAL_H_ */
-

src/util/ref_vector.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef REF_VECTOR_H_
-#define REF_VECTOR_H_
+#pragma once
 
 #include "util/vector.h"
 #include "util/obj_ref.h"
@@ -49,11 +48,14 @@ protected:
 public:
     typedef T * data;
 
-    ref_vector_core(Ref const & r = Ref()):Ref(r) {}
+    ref_vector_core() = default;
+    ref_vector_core(Ref const & r) : Ref(r) {}
 
-    ref_vector_core(ref_vector_core && other) :
-        Ref(std::move(other)),
-        m_nodes(std::move(other.m_nodes)) {}
+    ref_vector_core(const ref_vector_core & other) {
+        append(other);
+    }
+
+    ref_vector_core(ref_vector_core &&) = default;
     
     ~ref_vector_core() {
         dec_range_ref(m_nodes.begin(), m_nodes.end());
@@ -189,6 +191,13 @@ public:
             push_back(data[i]);
     }
 
+    void operator=(ref_vector_core && other) {
+        if (this != &other) {
+            reset();
+            m_nodes = std::move(other.m_nodes);
+        }
+    }
+
     void swap(unsigned idx1, unsigned idx2) {
         std::swap(m_nodes[idx1], m_nodes[idx2]);
     }
@@ -232,7 +241,7 @@ public:
         this->append(other);
     }
 
-    ref_vector(ref_vector && other) : super(std::move(other)) {}
+    ref_vector(ref_vector &&) = default;
 
     ref_vector(TManager & m, unsigned sz, T * const * data):
         super(ref_manager_wrapper<T, TManager>(m)) {
@@ -318,6 +327,11 @@ public:
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
 
+    ref_vector & operator=(ref_vector && other) {
+        super::operator=(std::move(other));
+        return *this;
+    }
+
     bool operator==(ref_vector const& other) const {
         if (other.size() != this->size()) return false;
         for (unsigned i = this->size(); i-- > 0; ) {
@@ -400,9 +414,8 @@ public:
 /**
    \brief Vector of unmanaged references.
 */
-template<typename T> 
-class sref_vector : public ref_vector_core<T, ref_unmanaged_wrapper<T> > {
-};
+template<typename T>
+using sref_vector = ref_vector_core<T, ref_unmanaged_wrapper<T>>;
 
 /**
    \brief Hash utilities on ref_vector pointers.
@@ -440,6 +453,3 @@ struct ref_vector_ptr_eq {
         return true;
     }
 };
-
-
-#endif /* REF_VECTOR_H_ */

src/util/scoped_numeral.h

@@ -17,8 +17,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef SCOPED_NUMERAL_H_
-#define SCOPED_NUMERAL_H_
+#pragma once
 
 template<typename Manager>
 class _scoped_numeral {
@@ -30,6 +29,7 @@ private:
 public:
     _scoped_numeral(Manager & m):m_manager(m) {}
     _scoped_numeral(_scoped_numeral const & n):m_manager(n.m_manager) { m().set(m_num, n.m_num); }
+    _scoped_numeral(_scoped_numeral &&) = default;
     ~_scoped_numeral() { m_manager.del(m_num); }
 
     Manager & m() const { return m_manager; }
@@ -189,5 +189,3 @@ public:
     }
                                  
 };
-
-#endif

src/util/scoped_numeral_vector.h

@@ -16,17 +16,24 @@ Author:
 Revision History:
 
 --*/
-#ifndef SCOPED_NUMERAL_VECTOR_H_
-#define SCOPED_NUMERAL_VECTOR_H_
+#pragma once
 
 #include "util/vector.h"
 
 template<typename Manager>
 class _scoped_numeral_vector : public svector<typename Manager::numeral> {
     Manager & m_manager;
-    _scoped_numeral_vector(_scoped_numeral_vector const & v);
 public:
     _scoped_numeral_vector(Manager & m):m_manager(m) {}
+
+    _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) {
+        for (unsigned i = 0, e = other.size(); i != e; ++i) {
+            push_back((*this)[i]);
+        }
+    }
+
+    _scoped_numeral_vector(_scoped_numeral_vector&&) = default;
+
     ~_scoped_numeral_vector() {
         reset();
     }
@@ -66,5 +73,3 @@ public:
         svector<typename Manager::numeral>::resize(sz, 0);
     }
 };
-
-#endif

src/util/uint_set.h

@@ -16,8 +16,7 @@ Author:
 Revision History:
 
 --*/
-#ifndef UINT_SET_H_
-#define UINT_SET_H_
+#pragma once
 
 #include "util/util.h"
 #include "util/vector.h"
@@ -29,16 +28,6 @@ public:
     
     typedef unsigned data;
 
-    uint_set() {}
-
-    uint_set(const uint_set & source) {
-        for (unsigned i = 0; i < source.size(); ++i) {
-            push_back(source[i]);
-        }
-    }
-
-    ~uint_set() {}
-
     void swap(uint_set & other) {
         unsigned_vector::swap(other);
     }
@@ -384,6 +373,3 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) {
     for (unsigned i : s) out << i << " ";
     return out;
 }
-
-#endif /* UINT_SET_H_ */
-

src/util/vector.h

@@ -69,6 +69,7 @@ class vector {
             m_data            = reinterpret_cast<T *>(mem);
         }
         else {
+            //static_assert(std::is_nothrow_move_constructible<T>::value, "");
             SASSERT(capacity() > 0);
             SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
             SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
@@ -163,7 +164,7 @@ public:
         SASSERT(size() == source.size());
     }
 
-    vector(vector&& other) : m_data(nullptr) {
+    vector(vector&& other) noexcept : m_data(nullptr) {
         std::swap(m_data, other.m_data);
     }
 
@@ -587,7 +588,7 @@ public:
     ptr_vector(unsigned s):vector<T *, false>(s) {}
     ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
     ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
-    ptr_vector(ptr_vector && other) : vector<T*, false>(std::move(other)) {}
+    ptr_vector(ptr_vector && other) noexcept : vector<T*, false>(std::move(other)) {}
     ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
     ptr_vector & operator=(ptr_vector const & source) {
         vector<T *, false>::operator=(source);
@@ -602,7 +603,7 @@ public:
     svector(SZ s):vector<T, false, SZ>(s) {}
     svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
     svector(svector const & source):vector<T, false, SZ>(source) {}
-    svector(svector && other) : vector<T, false, SZ>(std::move(other)) {}
+    svector(svector && other) noexcept : vector<T, false, SZ>(std::move(other)) {}
     svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
     svector & operator=(svector const & source) {
         vector<T, false, SZ>::operator=(source);