diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index de4d3732f..596ba011d 100644
--- a/src/api/api_solver.cpp
+++ b/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());
}
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 3987004ef..0293fc76a 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2488,12 +2488,12 @@ namespace Microsoft.Z3
///
/// Retrieve element at index.
///
- 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));
}
///
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ef1f6bb07..06fe6061a 100644
--- a/src/api/java/Context.java
+++ b/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.
*/
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 641c01285..8bd125dd7 100644
--- a/src/ast/ast.cpp
+++ b/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(m_parameters.begin(), info.m_parameters.begin(), m_parameters.size());
}
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 0410a4edd..611c07eec 100644
--- a/src/ast/ast.h
+++ b/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;
diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
index d9a6fc629..786061065 100644
--- a/src/ast/justified_expr.h
+++ b/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
diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index db9f5eb66..7bf9de2e0 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/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:
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 99e0da198..87a09afb0 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/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
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 8277fa703..e466249a3 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/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;
diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h
index 4903b2067..3d42f13a0 100644
--- a/src/math/automata/automaton.h
+++ b/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;
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index b24f95c6d..d12af2585 100644
--- a/src/math/dd/dd_pdd.h
+++ b/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); }
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index b8fc04b0a..cceb34b0b 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/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
namespace dd {
diff --git a/src/math/hilbert/heap_trie.h b/src/math/hilbert/heap_trie.h
index 3c6ecd1cb..add64d2a0 100644
--- a/src/math/hilbert/heap_trie.h
+++ b/src/math/hilbert/heap_trie.h
@@ -37,13 +37,13 @@ Notes:
#ifndef HEAP_TRIE_H_
#define HEAP_TRIE_H_
+#include
#include "util/map.h"
#include "util/vector.h"
#include "util/buffer.h"
#include "util/statistics.h"
#include "util/small_object_allocator.h"
-
template
class heap_trie {
diff --git a/src/math/hilbert/hilbert_basis.h b/src/math/hilbert/hilbert_basis.h
index cb4dd146e..46563195c 100644
--- a/src/math/hilbert/hilbert_basis.h
+++ b/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
typedef vector rational_vector;
@@ -198,6 +198,3 @@ public:
void reset_statistics();
};
-
-
-#endif
diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h
index 38e48f4aa..c48376470 100644
--- a/src/math/lp/indexed_value.h
+++ b/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;
}
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index a7d7e9b86..0cd0305fc 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -24,6 +24,7 @@ Revision History:
#include
#include
#include
+#include
#include "math/lp/lp_utils.h"
#include "util/stopwatch.h"
#include "math/lp/lp_types.h"
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index cd992ccb2..e7586cf5a 100644
--- a/src/math/lp/numeric_pair.h
+++ b/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 & n) : x(n.x), y(n.y) {}
-
template
numeric_pair(X xp, Y yp) : x(convert_struct::convert(xp)), y(convert_struct::convert(yp)) {}
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index 7311850ab..4740a4899 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/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 m_vars;
rational m_coeff;
rational m_div;
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 96b2dd03c..f18bb6f87 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/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
namespace simplex {
@@ -271,6 +271,3 @@ namespace simplex {
};
};
-
-
-#endif
diff --git a/src/math/subpaving/subpaving_types.h b/src/math/subpaving/subpaving_types.h
index e81b86e09..28150cc04 100644
--- a/src/math/subpaving/subpaving_types.h
+++ b/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 {
public:
power():std::pair() {}
power(var v, unsigned d):std::pair(v, d) {}
- power(power const & p):std::pair(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
+}
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index c9252eece..707167e17 100644
--- a/src/muz/base/dl_context.cpp
+++ b/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";
}
}
}
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 61fd9447d..f560ef4dd 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -141,12 +141,12 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector 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();
}
};
diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp b/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
index c8a3d4357..c37370d14 100644
--- a/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
+++ b/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 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)
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index a94383453..9c962d774 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/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="<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::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;iget_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());
- 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;iget_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());
- 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;iget_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="< 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;iget_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; iget_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());
- ptr_vector& select_ops = selects[*it];
- for(unsigned i=0;iget_num_args();
- //Stores, for each old position, the list of a new possible arguments
- vector arg_correspondance;
- for(unsigned i=0;iget_arg(i), m);
- if(m_a.is_array(get_sort(arg)))
- {
- 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 chosen(arg_correspondance.size(), 0u);
- while(true)
- {
- expr_ref_vector new_args(m);
- for(unsigned i=0;i::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;iget_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());
+ 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;iget_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());
+ 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;iget_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;iget_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; iget_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());
+ ptr_vector& select_ops = selects[*it];
+ for(unsigned i=0;iget_num_args();
+ //Stores, for each old position, the list of a new possible arguments
+ vector arg_correspondance;
+ for(unsigned i=0;iget_arg(i), m);
+ if(m_a.is_array(get_sort(arg))) {
+ 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 chosen(arg_correspondance.size(), 0u);
+ while(true) {
+ expr_ref_vector new_args(m);
+ for(unsigned i=0;i=arg_correspondance[pos].size());
+ chosen[pos]++;
}
- }while(chosen[pos]+1>=arg_correspondance[pos].size());
- chosen[pos]++;
}
- }
}
diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp
index 0aa3c4d9a..4899ed126 100644
--- a/src/muz/transforms/dl_mk_backwards.cpp
+++ b/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 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();
}
};
diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp
index 6613b6551..2ff4372c4 100644
--- a/src/muz/transforms/dl_mk_coalesce.cpp
+++ b/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 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();
}
};
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 8c34325a4..79959d9bf 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/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);
}
}
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index 5ad3f67d2..fe9dee45e 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/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 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();
}
};
diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp
index e0895981f..b22d9fa3b 100644
--- a/src/muz/transforms/dl_mk_loop_counter.cpp
+++ b/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 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) {
diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp
index b951cfd28..85c88716c 100644
--- a/src/muz/transforms/dl_mk_magic_sets.cpp
+++ b/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 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();
}
};
diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp
index acdf0bff0..ac4efd448 100644
--- a/src/muz/transforms/dl_mk_magic_symbolic.cpp
+++ b/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 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) {
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index dacb32d1b..f956ca429 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/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 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();
}
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 0a183b923..032b4b19c 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/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 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();
}
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index 95397fa67..84e48d514 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/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 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) {
diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp
index b2f464931..b4b64de24 100644
--- a/src/muz/transforms/dl_mk_slice.cpp
+++ b/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 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();
}
};
diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp
index 4c5a08eb5..d75ae0b46 100644
--- a/src/muz/transforms/dl_mk_subsumption_checker.cpp
+++ b/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 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 old = res.detach();
res = alloc(rule_set, m_context);
transform_rules(*old, *res);
- dealloc(old);
}
- return res;
+ return res.detach();
}
};
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 6be75fc2c..c9d4fd3c6 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -387,7 +387,7 @@ namespace datalog {
}
}
- rule_set * result = static_cast(nullptr);
+ scoped_ptr 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();
}
diff --git a/src/muz/transforms/dl_mk_unfold.cpp b/src/muz/transforms/dl_mk_unfold.cpp
index c9b8becde..6a1ae1535 100644
--- a/src/muz/transforms/dl_mk_unfold.cpp
+++ b/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 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();
}
};
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index a7dbedca4..65c2a8795 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/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();
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 291ec26d8..02fc16e02 100644
--- a/src/opt/maxsmt.h
+++ b/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;
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index c433f56d3..315b6f22a 100644
--- a/src/opt/pb_sls.cpp
+++ b/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 {
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index b033e6767..88009358d 100644
--- a/src/qe/qe.cpp
+++ b/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;
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 6b7eb2897..30b09a381 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/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 = 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;
}
};
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index cee6e3e8e..cec3a7726 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -899,12 +899,8 @@ namespace qe {
expr_ref_vector idx;
expr_ref_vector val;
vector rval;
- idx_val(expr_ref_vector & idx, expr_ref_vector & val, vector 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 && 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 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
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 248344c21..8f78a9106 100644
--- a/src/qe/qsat.cpp
+++ b/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 =
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 0abb38eae..062b6904d 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/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();
}
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index 93a078818..e453bcaa1 100644
--- a/src/sat/sat_model_converter.h
+++ b/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 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
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index cba9832d2..576a85a87 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/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;
}
diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp
index 48fd7d69a..efdb78754 100644
--- a/src/smt/old_interval.cpp
+++ b/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;
diff --git a/src/smt/old_interval.h b/src/smt/old_interval.h
index a666908e4..7a6f41e26 100644
--- a/src/smt/old_interval.h
+++ b/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 wd(old_interval const & i) { interval_detail d; return std::make_pair(i, d); }
-inline std::ostream & operator<<(std::ostream & out, std::pair 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_ */
-
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 269bd6fb6..5ed4b2631 100644
--- a/src/smt/seq_regex.cpp
+++ b/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);
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 6ba4868cb..5b6e4638a 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/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);
}
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index ea427145d..80b561d08 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/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;
diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp
index c78489f21..83c500b49 100644
--- a/src/test/mpff.cpp
+++ b/src/test/mpff.cpp
@@ -16,7 +16,8 @@ Author:
Revision History:
--*/
-#include
+#include
+#include
#include "util/mpff.h"
#include "util/mpz.h"
#include "util/mpq.h"
diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp
index 7ef9cdc87..751f6fdbe 100644
--- a/src/test/old_interval.cpp
+++ b/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();
diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp
index bff5c3809..3188b1a6a 100644
--- a/src/test/theory_pb.cpp
+++ b/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";
}
};
diff --git a/src/util/array_map.h b/src/util/array_map.h
index f3f99d015..91d226dab 100644
--- a/src/util/array_map.h
+++ b/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, 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_ */
diff --git a/src/util/buffer.h b/src/util/buffer.h
index aec826a55..22cf17ada 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -21,7 +21,7 @@ Revision History:
--*/
#pragma once
-#include
+#include
#include "util/memory_manager.h"
template
@@ -39,10 +39,14 @@ protected:
}
void expand() {
+ static_assert(std::is_nothrow_move_constructible::value, "");
unsigned new_capacity = m_capacity << 1;
T * new_buffer = reinterpret_cast(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;
diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h
index 507564a2e..06b957fcf 100644
--- a/src/util/checked_int64.h
+++ b/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 operator*(checked_int64 const& a, checked_int
result *= b;
return result;
}
-
-#endif
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 55866065e..78abd3c87 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -16,8 +16,8 @@ Author:
Revision History:
--*/
-#ifndef HASHTABLE_H_
-#define HASHTABLE_H_
+#pragma once
+
#include "util/debug.h"
#include
#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, HashProc, EqProc>(initial_capacity, h, e) {}
};
-
-
-#endif /* HASHTABLE_H_ */
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 21e7655ea..f2afbee63 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -16,10 +16,10 @@ Author:
Revision History:
--*/
-#ifndef HWF_H_
-#define HWF_H_
+#pragma once
-#include
+#include
+#include
#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 scoped_hwf;
typedef _scoped_numeral_vector scoped_hwf_vector;
-
-#endif
diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h
index c3f4160ba..86e04543c 100644
--- a/src/util/inf_rational.h
+++ b/src/util/inf_rational.h
@@ -17,8 +17,8 @@ Author:
Revision History:
--*/
-#ifndef INF_RATIONAL_H_
-#define INF_RATIONAL_H_
+#pragma once
+
#include
#include
#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_ */
diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h
index dd136d1b9..b99167b32 100644
--- a/src/util/inf_s_integer.h
+++ b/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_ */
-
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index cdd8f5f3e..1e93d0d3d 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -16,6 +16,7 @@ Author:
Revision History:
--*/
+#include
#include
#include
#include "util/mpf.h"
diff --git a/src/util/mpf.h b/src/util/mpf.h
index 107ada0bd..fb5f2a022 100644
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@@ -16,8 +16,7 @@ Author:
Revision History:
--*/
-#ifndef MPF_H_
-#define MPF_H_
+#pragma once
#include
#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 scoped_mpf_vector;
-
-#endif
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index 4769ab24a..8595e0185 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -16,6 +16,7 @@ Author:
Revision History:
--*/
+#include
#include
#include
#include "util/mpfx.h"
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 4cc15229f..a9e6063a3 100644
--- a/src/util/mpq.h
+++ b/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;
friend class mpq_manager;
- 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 unsynch_mpq_manager;
typedef _scoped_numeral scoped_mpq;
typedef _scoped_numeral scoped_synch_mpq;
typedef _scoped_numeral_vector scoped_mpq_vector;
-
-#endif /* MPQ_H_ */
-
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index eb6754654..3a7922e13 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -16,6 +16,7 @@ Author:
Revision History:
--*/
+#include
#include
#include
#include "util/mpz.h"
diff --git a/src/util/mpz.h b/src/util/mpz.h
index dee54b1c8..248048888 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -16,8 +16,7 @@ Author:
Revision History:
--*/
-#ifndef MPZ_H_
-#define MPZ_H_
+#pragma once
#include
#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 unsynch_mpz_manager;
typedef _scoped_numeral scoped_mpz;
typedef _scoped_numeral scoped_synch_mpz;
typedef _scoped_numeral_vector scoped_mpz_vector;
-
-#endif /* MPZ_H_ */
-
diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h
index e3b0d0710..6b00f894f 100644
--- a/src/util/obj_ref.h
+++ b/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_ */
diff --git a/src/util/optional.h b/src/util/optional.h
index d496fd322..b9687df8c 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -18,8 +18,7 @@ Revision History:
--*/
-#ifndef OPTIONAL_H_
-#define OPTIONAL_H_
+#pragma once
template
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 & val):
m_initialized(0) {
if (val.m_initialized == 1) {
@@ -160,7 +164,3 @@ public:
T * & operator*() { return m_ptr; }
};
-
-
-#endif /* OPTIONAL_H_ */
-
diff --git a/src/util/rational.h b/src/util/rational.h
index c7f0358dd..0f2a2a1b7 100644
--- a/src/util/rational.h
+++ b/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_ */
-
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index 5b5d9ac34..40c01b012 100644
--- a/src/util/ref_vector.h
+++ b/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(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
-class sref_vector : public ref_vector_core > {
-};
+template
+using sref_vector = ref_vector_core>;
/**
\brief Hash utilities on ref_vector pointers.
@@ -440,6 +453,3 @@ struct ref_vector_ptr_eq {
return true;
}
};
-
-
-#endif /* REF_VECTOR_H_ */
diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h
index 2c80c4703..3b35a1bd8 100644
--- a/src/util/scoped_numeral.h
+++ b/src/util/scoped_numeral.h
@@ -17,8 +17,7 @@ Author:
Revision History:
--*/
-#ifndef SCOPED_NUMERAL_H_
-#define SCOPED_NUMERAL_H_
+#pragma once
template
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
diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h
index cb9a6b4fd..f53d93470 100644
--- a/src/util/scoped_numeral_vector.h
+++ b/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
class _scoped_numeral_vector : public svector {
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::resize(sz, 0);
}
};
-
-#endif
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index ebef623aa..46a606e8f 100644
--- a/src/util/uint_set.h
+++ b/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_ */
-
diff --git a/src/util/vector.h b/src/util/vector.h
index 9de2b2a86..588be7ae8 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -69,6 +69,7 @@ class vector {
m_data = reinterpret_cast(mem);
}
else {
+ //static_assert(std::is_nothrow_move_constructible::value, "");
SASSERT(capacity() > 0);
SZ old_capacity = reinterpret_cast(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(s) {}
ptr_vector(unsigned s, T * elem):vector(s, elem) {}
ptr_vector(ptr_vector const & source):vector(source) {}
- ptr_vector(ptr_vector && other) : vector(std::move(other)) {}
+ ptr_vector(ptr_vector && other) noexcept : vector(std::move(other)) {}
ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {}
ptr_vector & operator=(ptr_vector const & source) {
vector::operator=(source);
@@ -602,7 +603,7 @@ public:
svector(SZ s):vector(s) {}
svector(SZ s, T const & elem):vector(s, elem) {}
svector(svector const & source):vector(source) {}
- svector(svector && other) : vector(std::move(other)) {}
+ svector(svector && other) noexcept : vector(std::move(other)) {}
svector(SZ s, T const * data):vector(s, data) {}
svector & operator=(svector const & source) {
vector::operator=(source);