mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
0169417c64
|
@ -65,6 +65,15 @@ void throw_z3_error(Z3_context c, Z3_error_code e)
|
|||
longjmp(g_catch_buffer, e);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Error handling that depends on checking an error code on the context.
|
||||
|
||||
*/
|
||||
|
||||
void nothrow_z3_error(Z3_context c, Z3_error_code e) {
|
||||
// no-op
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a logical context.
|
||||
|
||||
|
@ -1592,18 +1601,16 @@ void error_code_example1()
|
|||
void error_code_example2() {
|
||||
Z3_config cfg;
|
||||
Z3_context ctx = NULL;
|
||||
int r;
|
||||
Z3_error_code e;
|
||||
|
||||
printf("\nerror_code_example2\n");
|
||||
LOG_MSG("error_code_example2");
|
||||
|
||||
/* low tech try&catch */
|
||||
r = setjmp(g_catch_buffer);
|
||||
if (r == 0) {
|
||||
if (1) {
|
||||
Z3_ast x, y, app;
|
||||
|
||||
cfg = Z3_mk_config();
|
||||
ctx = mk_context_custom(cfg, throw_z3_error);
|
||||
ctx = mk_context_custom(cfg, nothrow_z3_error);
|
||||
Z3_del_config(cfg);
|
||||
|
||||
x = mk_int_var(ctx, "x");
|
||||
|
@ -1611,11 +1618,14 @@ void error_code_example2() {
|
|||
printf("before Z3_mk_iff\n");
|
||||
/* the next call will produce an error */
|
||||
app = Z3_mk_iff(ctx, x, y);
|
||||
e = Z3_get_error_code(ctx);
|
||||
if (e != Z3_OK) goto err;
|
||||
unreachable();
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
else {
|
||||
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r));
|
||||
err:
|
||||
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e));
|
||||
if (ctx != NULL) {
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
@ -1781,15 +1791,14 @@ void parser_example5() {
|
|||
Z3_config cfg;
|
||||
Z3_context ctx = NULL;
|
||||
Z3_solver s = NULL;
|
||||
int r;
|
||||
Z3_error_code e;
|
||||
|
||||
printf("\nparser_example5\n");
|
||||
LOG_MSG("parser_example5");
|
||||
|
||||
r = setjmp(g_catch_buffer);
|
||||
if (r == 0) {
|
||||
if (1) {
|
||||
cfg = Z3_mk_config();
|
||||
ctx = mk_context_custom(cfg, throw_z3_error);
|
||||
ctx = mk_context_custom(cfg, nothrow_z3_error);
|
||||
s = mk_solver(ctx);
|
||||
Z3_del_config(cfg);
|
||||
|
||||
|
@ -1798,12 +1807,15 @@ void parser_example5() {
|
|||
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
|
||||
0, 0, 0,
|
||||
0, 0, 0);
|
||||
e = Z3_get_error_code(ctx);
|
||||
if (e != Z3_OK) goto err;
|
||||
unreachable();
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
else {
|
||||
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r));
|
||||
err:
|
||||
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e));
|
||||
if (ctx != NULL) {
|
||||
printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx));
|
||||
del_solver(ctx, s);
|
||||
|
@ -2639,6 +2651,7 @@ void smt2parser_example() {
|
|||
ctx = mk_context();
|
||||
fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0);
|
||||
printf("formulas: %s\n", Z3_ast_to_string(ctx, fs));
|
||||
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
|
|
|
@ -283,15 +283,16 @@ extern "C" {
|
|||
Z3_optimize opt,
|
||||
std::istream& s) {
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
cmd_context ctx(false, &m);
|
||||
install_opt_cmds(ctx, to_optimize_ptr(opt));
|
||||
ctx.set_ignore_check(true);
|
||||
if (!parse_smt2_commands(ctx, s)) {
|
||||
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
|
||||
install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
|
||||
ctx->set_ignore_check(true);
|
||||
if (!parse_smt2_commands(*ctx.get(), s)) {
|
||||
ctx = nullptr;
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
return;
|
||||
}
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
|
||||
for (; it != end; ++it) {
|
||||
to_optimize_ptr(opt)->add_hard_constraint(*it);
|
||||
}
|
||||
|
@ -320,9 +321,6 @@ extern "C" {
|
|||
std::ostringstream strm;
|
||||
strm << "Could not open file " << s;
|
||||
throw default_exception(strm.str());
|
||||
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
return;
|
||||
}
|
||||
Z3_optimize_from_stream(c, d, is);
|
||||
Z3_CATCH;
|
||||
|
|
|
@ -56,19 +56,20 @@ extern "C" {
|
|||
Z3_func_decl const decls[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
|
||||
std::ostringstream outs;
|
||||
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
|
||||
bool ok = false;
|
||||
|
||||
RESET_ERROR_CODE();
|
||||
init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
|
||||
mk_c(c)->m_smtlib_parser->set_error_stream(outs);
|
||||
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
|
||||
try {
|
||||
ok = mk_c(c)->m_smtlib_parser->parse_string(str);
|
||||
}
|
||||
catch (...) {
|
||||
ok = false;
|
||||
}
|
||||
mk_c(c)->m_smtlib_error_buffer = outs.str();
|
||||
mk_c(c)->m_smtlib_error_buffer = outs->str();
|
||||
outs = nullptr;
|
||||
if (!ok) {
|
||||
mk_c(c)->reset_parser();
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
|
@ -88,16 +89,17 @@ extern "C" {
|
|||
LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
|
||||
bool ok = false;
|
||||
RESET_ERROR_CODE();
|
||||
std::ostringstream outs;
|
||||
scoped_ptr<std::ostringstream> outs = alloc(std::ostringstream);
|
||||
init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
|
||||
mk_c(c)->m_smtlib_parser->set_error_stream(outs);
|
||||
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
|
||||
try {
|
||||
ok = mk_c(c)->m_smtlib_parser->parse_file(file_name);
|
||||
}
|
||||
catch(...) {
|
||||
ok = false;
|
||||
}
|
||||
mk_c(c)->m_smtlib_error_buffer = outs.str();
|
||||
mk_c(c)->m_smtlib_error_buffer = outs->str();
|
||||
outs = nullptr;
|
||||
if (!ok) {
|
||||
mk_c(c)->reset_parser();
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
|
@ -260,21 +262,22 @@ extern "C" {
|
|||
Z3_symbol const decl_names[],
|
||||
Z3_func_decl const decls[]) {
|
||||
Z3_TRY;
|
||||
cmd_context ctx(false, &(mk_c(c)->m()));
|
||||
ctx.set_ignore_check(true);
|
||||
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
|
||||
ctx->set_ignore_check(true);
|
||||
for (unsigned i = 0; i < num_decls; ++i) {
|
||||
ctx.insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
|
||||
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
|
||||
}
|
||||
for (unsigned i = 0; i < num_sorts; ++i) {
|
||||
psort* ps = ctx.pm().mk_psort_cnst(to_sort(sorts[i]));
|
||||
ctx.insert(ctx.pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
|
||||
psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
|
||||
ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
|
||||
}
|
||||
if (!parse_smt2_commands(ctx, is)) {
|
||||
if (!parse_smt2_commands(*ctx.get(), is)) {
|
||||
ctx = nullptr;
|
||||
SET_ERROR_CODE(Z3_PARSER_ERROR);
|
||||
return of_ast(mk_c(c)->m().mk_true());
|
||||
}
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
|
||||
unsigned size = static_cast<unsigned>(end - it);
|
||||
return of_ast(mk_c(c)->mk_and(size, it));
|
||||
Z3_CATCH_RETURN(0);
|
||||
|
|
|
@ -63,9 +63,11 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
if (!mk_c(c)->m().is_bool(to_expr(body))) {
|
||||
SET_ERROR_CODE(Z3_SORT_ERROR);
|
||||
return nullptr;
|
||||
}
|
||||
if (num_patterns > 0 && num_no_patterns > 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_USAGE);
|
||||
return nullptr;
|
||||
}
|
||||
expr * const* ps = reinterpret_cast<expr * const*>(patterns);
|
||||
expr * const* no_ps = reinterpret_cast<expr * const*>(no_patterns);
|
||||
|
@ -76,7 +78,7 @@ extern "C" {
|
|||
for (unsigned i = 0; i < num_patterns; i++) {
|
||||
if (!v(num_decls, ps[i], 0, 0)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_PATTERN);
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -442,6 +442,7 @@ extern "C" {
|
|||
unsigned sz = __assumptions.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (!is_expr(__assumptions[i])) {
|
||||
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
|
||||
SET_ERROR_CODE(Z3_INVALID_USAGE);
|
||||
return Z3_L_UNDEF;
|
||||
}
|
||||
|
@ -451,6 +452,7 @@ extern "C" {
|
|||
sz = __variables.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (!is_expr(__variables[i])) {
|
||||
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
|
||||
SET_ERROR_CODE(Z3_INVALID_USAGE);
|
||||
return Z3_L_UNDEF;
|
||||
}
|
||||
|
@ -471,6 +473,7 @@ extern "C" {
|
|||
}
|
||||
catch (z3_exception & ex) {
|
||||
to_solver_ref(s)->set_reason_unknown(eh);
|
||||
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
|
||||
mk_c(c)->handle_exception(ex);
|
||||
return Z3_L_UNDEF;
|
||||
}
|
||||
|
|
|
@ -140,18 +140,17 @@ namespace z3 {
|
|||
class context {
|
||||
bool m_enable_exceptions;
|
||||
Z3_context m_ctx;
|
||||
static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
|
||||
void init(config & c) {
|
||||
m_ctx = Z3_mk_context_rc(c);
|
||||
m_enable_exceptions = true;
|
||||
Z3_set_error_handler(m_ctx, error_handler);
|
||||
Z3_set_error_handler(m_ctx, 0);
|
||||
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
|
||||
}
|
||||
|
||||
void init_interp(config & c) {
|
||||
m_ctx = Z3_mk_interpolation_context(c);
|
||||
m_enable_exceptions = true;
|
||||
Z3_set_error_handler(m_ctx, error_handler);
|
||||
Z3_set_error_handler(m_ctx, 0);
|
||||
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
|
||||
}
|
||||
|
||||
|
|
|
@ -768,7 +768,7 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic
|
|||
|
||||
func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
|
||||
if (num_parents >= cache.size()) {
|
||||
cache.resize(num_parents+1, 0);
|
||||
cache.resize(num_parents+1);
|
||||
}
|
||||
if (cache[num_parents] == 0) {
|
||||
cache[num_parents] = mk_proof_decl(name, k, num_parents);
|
||||
|
|
|
@ -121,6 +121,20 @@ 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) {
|
||||
switch (other.m_kind) {
|
||||
case PARAM_INT: m_int = other.get_int(); break;
|
||||
case PARAM_AST: m_ast = other.get_ast(); break;
|
||||
case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
|
||||
case PARAM_RATIONAL: m_rational = 0; std::swap(m_rational, other.m_rational); break;
|
||||
case PARAM_DOUBLE: m_dval = other.m_dval; break;
|
||||
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
~parameter();
|
||||
|
||||
parameter& operator=(parameter const& other);
|
||||
|
|
|
@ -863,8 +863,7 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const {
|
|||
}
|
||||
|
||||
app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
|
||||
parameter p1(val);
|
||||
parameter p[2] = { p1, parameter(static_cast<int>(bv_size)) };
|
||||
parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
|
||||
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
|
||||
}
|
||||
|
||||
|
|
|
@ -207,8 +207,8 @@ struct nnf::imp {
|
|||
unsigned m_new_child:1;
|
||||
unsigned m_cache_result:1;
|
||||
unsigned m_spos; // top of the result stack, when the frame was created.
|
||||
frame(expr_ref& n, bool pol, bool in_q, bool cache_res, unsigned spos):
|
||||
m_curr(n),
|
||||
frame(expr_ref&& n, bool pol, bool in_q, bool cache_res, unsigned spos):
|
||||
m_curr(std::move(n)),
|
||||
m_i(0),
|
||||
m_pol(pol),
|
||||
m_in_q(in_q),
|
||||
|
@ -324,8 +324,7 @@ struct nnf::imp {
|
|||
}
|
||||
|
||||
void push_frame(expr * t, bool pol, bool in_q, bool cache_res) {
|
||||
expr_ref tr(t, m());
|
||||
m_frame_stack.push_back(frame(tr, pol, in_q, cache_res, m_result_stack.size()));
|
||||
m_frame_stack.push_back(frame({ t, m() }, pol, in_q, cache_res, m_result_stack.size()));
|
||||
}
|
||||
|
||||
static unsigned get_cache_idx(bool pol, bool in_q) {
|
||||
|
|
|
@ -179,11 +179,11 @@ expr_pattern_match::compile(expr* q)
|
|||
}
|
||||
|
||||
if (m_regs.size() <= max_reg) {
|
||||
m_regs.resize(max_reg+1, 0);
|
||||
m_regs.resize(max_reg+1);
|
||||
}
|
||||
if (m_bound_dom.size() <= num_bound) {
|
||||
m_bound_dom.resize(num_bound+1, 0);
|
||||
m_bound_rng.resize(num_bound+1, 0);
|
||||
m_bound_dom.resize(num_bound+1);
|
||||
m_bound_rng.resize(num_bound+1);
|
||||
}
|
||||
|
||||
instr.m_kind = YIELD;
|
||||
|
|
|
@ -272,7 +272,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
|
|||
zero = m().mk_false();
|
||||
|
||||
vector< expr_ref_vector > pps;
|
||||
pps.resize(sz, m());
|
||||
pps.resize(sz, expr_ref_vector(m()));
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
checkpoint();
|
||||
|
|
|
@ -125,11 +125,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
const mpz & sm1 = m_fm.m_powers2(sbits - 1);
|
||||
const mpz & em1 = m_fm.m_powers2(ebits);
|
||||
|
||||
scoped_mpq q(mpqm);
|
||||
mpqm.set(q, r1.to_mpq());
|
||||
SASSERT(mpzm.is_one(q.get().denominator()));
|
||||
const mpq & q = r1.to_mpq();
|
||||
SASSERT(mpzm.is_one(q.denominator()));
|
||||
scoped_mpz z(mpzm);
|
||||
z = q.get().numerator();
|
||||
z = q.numerator();
|
||||
|
||||
mpzm.rem(z, sm1, sig);
|
||||
mpzm.div(z, sm1, z);
|
||||
|
|
|
@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
|
|||
TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";);
|
||||
try_to_reuse:
|
||||
if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) {
|
||||
for (unsigned i = 0; i < num_args - 1; i++) {
|
||||
for (unsigned i = 0; i + 1 < num_args; i++) {
|
||||
for (unsigned j = i + 1; j < num_args; j++) {
|
||||
if (contains(f, _args[i], _args[j])) {
|
||||
TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";);
|
||||
_args[i] = m.mk_app(f, _args[i], _args[j]);
|
||||
SASSERT(num_args > 1);
|
||||
for (unsigned w = j; w < num_args - 1; w++) {
|
||||
for (unsigned w = j; w + 1 < num_args; w++) {
|
||||
_args[w] = _args[w+1];
|
||||
}
|
||||
num_args--;
|
||||
|
@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) {
|
|||
while (i != old_lim) {
|
||||
--i;
|
||||
entry * e = m_entries[i];
|
||||
m_cache.remove(e);
|
||||
m.dec_ref(e->m_arg1);
|
||||
m.dec_ref(e->m_arg2);
|
||||
}
|
||||
|
|
|
@ -256,7 +256,7 @@ void substitution_tree::insert(expr * new_expr) {
|
|||
sort * s = to_var(new_expr)->get_sort();
|
||||
unsigned id = s->get_decl_id();
|
||||
if (id >= m_vars.size())
|
||||
m_vars.resize(id+1, 0);
|
||||
m_vars.resize(id+1);
|
||||
if (m_vars[id] == 0)
|
||||
m_vars[id] = alloc(var_ref_vector, m_manager);
|
||||
var_ref_vector * v = m_vars[id];
|
||||
|
@ -277,7 +277,7 @@ void substitution_tree::insert(app * new_expr) {
|
|||
unsigned id = d->get_decl_id();
|
||||
|
||||
if (id >= m_roots.size())
|
||||
m_roots.resize(id+1, 0);
|
||||
m_roots.resize(id+1);
|
||||
|
||||
if (!m_roots[id]) {
|
||||
// there is no tree for the function symbol heading new_expr
|
||||
|
|
|
@ -58,7 +58,7 @@ void used_vars::process(expr * n, unsigned delta) {
|
|||
if (idx >= delta) {
|
||||
idx = idx - delta;
|
||||
if (idx >= m_found_vars.size())
|
||||
m_found_vars.resize(idx + 1, 0);
|
||||
m_found_vars.resize(idx + 1);
|
||||
m_found_vars[idx] = to_var(n)->get_sort();
|
||||
}
|
||||
break;
|
||||
|
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
|
||||
#include "math/automata/symbolic_automata.h"
|
||||
#include "util/hashtable.h"
|
||||
#include "util/vector.h"
|
||||
|
||||
|
||||
|
||||
|
@ -311,7 +312,7 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
|
|||
s2id.insert(set, p_state_id++); // the index to the initial state is 0
|
||||
id2s.push_back(set);
|
||||
|
||||
svector<uint_set> todo; //States to visit
|
||||
::vector<uint_set> todo; //States to visit
|
||||
todo.push_back(set);
|
||||
|
||||
uint_set state;
|
||||
|
|
|
@ -162,7 +162,7 @@ private:
|
|||
void checkpoint();
|
||||
|
||||
public:
|
||||
interval_manager(reslimit& lim, C const & c);
|
||||
interval_manager(reslimit& lim, C && c);
|
||||
~interval_manager();
|
||||
|
||||
numeral_manager & m() const { return m_c.m(); }
|
||||
|
|
|
@ -31,7 +31,7 @@ Revision History:
|
|||
// #define TRACE_NTH_ROOT
|
||||
|
||||
template<typename C>
|
||||
interval_manager<C>::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) {
|
||||
interval_manager<C>::interval_manager(reslimit& lim, C && c): m_limit(lim), m_c(std::move(c)) {
|
||||
m().set(m_minus_one, -1);
|
||||
m().set(m_one, 1);
|
||||
m_pi_n = 0;
|
||||
|
|
|
@ -2632,10 +2632,14 @@ namespace algebraic_numbers {
|
|||
scoped_mpz neg_n(qm());
|
||||
qm().set(neg_n, v.numerator());
|
||||
qm().neg(neg_n);
|
||||
mpz const coeffs[2] = { neg_n.get(), v.denominator() };
|
||||
unsynch_mpz_manager zmgr;
|
||||
// FIXME: remove these copies
|
||||
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
|
||||
out << "(";
|
||||
upm().display(out, 2, coeffs, "#");
|
||||
out << ", 1)"; // first root of the polynomial d*# - n
|
||||
zmgr.del(coeffs[0]);
|
||||
zmgr.del(coeffs[1]);
|
||||
}
|
||||
else {
|
||||
algebraic_cell * c = a.to_algebraic();
|
||||
|
@ -2678,10 +2682,14 @@ namespace algebraic_numbers {
|
|||
scoped_mpz neg_n(qm());
|
||||
qm().set(neg_n, v.numerator());
|
||||
qm().neg(neg_n);
|
||||
mpz const coeffs[2] = { neg_n.get(), v.denominator() };
|
||||
unsynch_mpz_manager zmgr;
|
||||
// FIXME: remove these copies
|
||||
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
|
||||
out << "(root-obj ";
|
||||
upm().display_smt2(out, 2, coeffs, "x");
|
||||
out << " 1)"; // first root of the polynomial d*# - n
|
||||
zmgr.del(coeffs[0]);
|
||||
zmgr.del(coeffs[1]);
|
||||
}
|
||||
else {
|
||||
algebraic_cell * c = a.to_algebraic();
|
||||
|
|
|
@ -3536,10 +3536,11 @@ namespace polynomial {
|
|||
iccp(p, max_var(p), i, c, pp);
|
||||
}
|
||||
|
||||
void pp(polynomial const * p, var x, polynomial_ref & pp) {
|
||||
polynomial_ref pp(polynomial const * p, var x) {
|
||||
scoped_numeral i(m_manager);
|
||||
polynomial_ref c(pm());
|
||||
iccp(p, x, i, c, pp);
|
||||
polynomial_ref c(pm()), result(pm());
|
||||
iccp(p, x, i, c, result);
|
||||
return result;
|
||||
}
|
||||
|
||||
bool is_primitive(polynomial const * p, var x) {
|
||||
|
@ -3598,7 +3599,7 @@ namespace polynomial {
|
|||
if (is_zero(rem)) {
|
||||
TRACE("polynomial", tout << "rem is zero...\npp_v: " << pp_v << "\n";);
|
||||
flip_sign_if_lm_neg(pp_v);
|
||||
pp(pp_v, x, r);
|
||||
r = pp(pp_v, x);
|
||||
r = mul(d_a, d_r, r);
|
||||
return;
|
||||
}
|
||||
|
@ -3849,7 +3850,7 @@ namespace polynomial {
|
|||
TRACE("mgcd", tout << "new combined:\n" << C_star << "\n";);
|
||||
}
|
||||
}
|
||||
pp(C_star, x, candidate);
|
||||
candidate = pp(C_star, x);
|
||||
TRACE("mgcd", tout << "candidate:\n" << candidate << "\n";);
|
||||
scoped_numeral lc_candidate(m());
|
||||
lc_candidate = univ_coeff(candidate, degree(candidate, x));
|
||||
|
@ -4821,10 +4822,9 @@ namespace polynomial {
|
|||
|
||||
polynomial * mk_x_minus_y(var x, var y) {
|
||||
numeral zero(0);
|
||||
numeral one(1);
|
||||
numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2
|
||||
m_manager.set(minus_one, -1);
|
||||
numeral as[2] = { one, minus_one };
|
||||
numeral as[2] = { numeral(1), std::move(minus_one) };
|
||||
var xs[2] = { x, y };
|
||||
return mk_linear(2, as, xs, zero);
|
||||
}
|
||||
|
@ -4844,8 +4844,7 @@ namespace polynomial {
|
|||
|
||||
polynomial * mk_x_plus_y(var x, var y) {
|
||||
numeral zero(0);
|
||||
numeral one(1);
|
||||
numeral as[2] = { one, one };
|
||||
numeral as[2] = { numeral(1), numeral(1) };
|
||||
var xs[2] = { x, y };
|
||||
return mk_linear(2, as, xs, zero);
|
||||
}
|
||||
|
@ -6619,8 +6618,8 @@ namespace polynomial {
|
|||
polynomial_ref cf1(pm()); m_wrapper.content(f1, x, cf1);
|
||||
polynomial_ref cf2(pm()); m_wrapper.content(f2, x, cf2);
|
||||
tout << "content(f1): " << cf1 << "\ncontent(f2): " << cf2 << "\n";);
|
||||
pp(f1, x, f1);
|
||||
pp(f2, x, f2);
|
||||
f1 = pp(f1, x);
|
||||
f2 = pp(f2, x);
|
||||
TRACE("factor", tout << "f1: " << f1 << "\nf2: " << f2 << "\n";);
|
||||
DEBUG_CODE({
|
||||
polynomial_ref f1f2(pm());
|
||||
|
@ -7150,7 +7149,7 @@ namespace polynomial {
|
|||
}
|
||||
|
||||
void manager::primitive(polynomial const * p, var x, polynomial_ref & pp) {
|
||||
m_imp->pp(p, x, pp);
|
||||
pp = m_imp->pp(p, x);
|
||||
}
|
||||
|
||||
void manager::icpp(polynomial const * p, var x, numeral & i, polynomial_ref & c, polynomial_ref & pp) {
|
||||
|
|
|
@ -45,7 +45,7 @@ namespace upolynomial {
|
|||
for (unsigned i = 0; i < p.size(); ++ i) {
|
||||
numeral p_i; // no need to delete, we keep it pushed in zp_p
|
||||
zp_nm.set(p_i, p[i]);
|
||||
zp_p.push_back(p_i);
|
||||
zp_p.push_back(std::move(p_i));
|
||||
}
|
||||
zp_upm.trim(zp_p);
|
||||
}
|
||||
|
|
|
@ -35,7 +35,7 @@ namespace simplex {
|
|||
struct row_entry {
|
||||
numeral m_coeff;
|
||||
var_t m_var;
|
||||
row_entry(numeral const& c, var_t v): m_coeff(c), m_var(v) {}
|
||||
row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {}
|
||||
};
|
||||
|
||||
private:
|
||||
|
@ -61,7 +61,7 @@ namespace simplex {
|
|||
int m_col_idx;
|
||||
int m_next_free_row_entry_idx;
|
||||
};
|
||||
_row_entry(numeral const & c, var_t v): row_entry(c, v), m_col_idx(0) {}
|
||||
_row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {}
|
||||
_row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {}
|
||||
bool is_dead() const { return row_entry::m_var == dead_id; }
|
||||
};
|
||||
|
|
|
@ -739,7 +739,7 @@ void context_t<C>::del_sum(polynomial * p) {
|
|||
|
||||
template<typename C>
|
||||
var context_t<C>::mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs) {
|
||||
m_num_buffer.reserve(num_vars(), numeral());
|
||||
m_num_buffer.reserve(num_vars());
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
SASSERT(xs[i] < num_vars());
|
||||
nm().set(m_num_buffer[xs[i]], as[i]);
|
||||
|
|
|
@ -117,7 +117,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
|
|||
(m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
|
||||
return false;
|
||||
|
||||
args.resize(m_arity, 0);
|
||||
args.resize(m_arity);
|
||||
for (unsigned i = 0; i < m_arity; i++) {
|
||||
expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);
|
||||
|
||||
|
|
|
@ -128,7 +128,7 @@ namespace datalog {
|
|||
void set_reg(reg_idx i, reg_type val) {
|
||||
if (i >= m_registers.size()) {
|
||||
check_overflow(i);
|
||||
m_registers.resize(i+1,0);
|
||||
m_registers.resize(i+1);
|
||||
}
|
||||
if (m_registers[i]) {
|
||||
m_registers[i]->deallocate();
|
||||
|
|
|
@ -465,7 +465,7 @@ namespace datalog {
|
|||
|
||||
unsigned sz = r.get_signature().size();
|
||||
ptr_vector<expr> subst_arg;
|
||||
subst_arg.resize(sz, 0);
|
||||
subst_arg.resize(sz);
|
||||
unsigned ofs = sz-1;
|
||||
for (unsigned i=0; i<sz; i++) {
|
||||
SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));
|
||||
|
|
|
@ -1272,7 +1272,7 @@ namespace qe {
|
|||
family_id fid = p->get_family_id();
|
||||
SASSERT(fid != null_family_id);
|
||||
if (static_cast<int>(m_plugins.size()) <= fid) {
|
||||
m_plugins.resize(fid+1,0);
|
||||
m_plugins.resize(fid+1);
|
||||
}
|
||||
SASSERT(!m_plugins[fid]);
|
||||
m_plugins[fid] = p;
|
||||
|
|
|
@ -105,10 +105,10 @@ namespace qe {
|
|||
rational r;
|
||||
app* alit = to_app(lit);
|
||||
vector<std::pair<expr*,rational> > nums;
|
||||
for (unsigned i = 0; i < alit->get_num_args(); ++i) {
|
||||
val = eval(alit->get_arg(i));
|
||||
for (expr* arg : *alit) {
|
||||
val = eval(arg);
|
||||
if (!a.is_numeral(val, r)) return false;
|
||||
nums.push_back(std::make_pair(alit->get_arg(i), r));
|
||||
nums.push_back(std::make_pair(arg, r));
|
||||
}
|
||||
std::sort(nums.begin(), nums.end(), compare_second());
|
||||
for (unsigned i = 0; i + 1 < nums.size(); ++i) {
|
||||
|
@ -168,8 +168,8 @@ namespace qe {
|
|||
}
|
||||
else if (a.is_add(t)) {
|
||||
app* ap = to_app(t);
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
linearize(mbo, eval, mul, ap->get_arg(i), c, fmls, ts, tids);
|
||||
for (expr* arg : *ap) {
|
||||
linearize(mbo, eval, mul, arg, c, fmls, ts, tids);
|
||||
}
|
||||
}
|
||||
else if (a.is_sub(t, t1, t2)) {
|
||||
|
@ -226,16 +226,16 @@ namespace qe {
|
|||
else if (a.is_mul(t)) {
|
||||
app* ap = to_app(t);
|
||||
r = rational(1);
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
if (!is_numeral(ap->get_arg(i), r1)) return false;
|
||||
for (expr * arg : *ap) {
|
||||
if (!is_numeral(arg, r1)) return false;
|
||||
r *= r1;
|
||||
}
|
||||
}
|
||||
else if (a.is_add(t)) {
|
||||
app* ap = to_app(t);
|
||||
r = rational(0);
|
||||
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
|
||||
if (!is_numeral(ap->get_arg(i), r1)) return false;
|
||||
for (expr * arg : *ap) {
|
||||
if (!is_numeral(arg, r1)) return false;
|
||||
r += r1;
|
||||
}
|
||||
}
|
||||
|
@ -297,6 +297,7 @@ namespace qe {
|
|||
|
||||
opt::model_based_opt mbo;
|
||||
obj_map<expr, unsigned> tids;
|
||||
expr_ref_vector pinned(m);
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
expr* fml = fmls[i].get();
|
||||
|
@ -308,6 +309,7 @@ namespace qe {
|
|||
}
|
||||
else {
|
||||
TRACE("qe", tout << mk_pp(fml, m) << "\n";);
|
||||
pinned.push_back(fml);
|
||||
}
|
||||
}
|
||||
fmls.resize(j);
|
||||
|
@ -321,8 +323,7 @@ namespace qe {
|
|||
// return those to fmls.
|
||||
|
||||
expr_mark var_mark, fmls_mark;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
app* v = vars[i].get();
|
||||
for (app * v : vars) {
|
||||
var_mark.mark(v);
|
||||
if (is_arith(v) && !tids.contains(v)) {
|
||||
rational r;
|
||||
|
@ -332,17 +333,16 @@ namespace qe {
|
|||
tids.insert(v, mbo.add_var(r, a.is_int(v)));
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
fmls_mark.mark(fmls[i].get());
|
||||
for (expr* fml : fmls) {
|
||||
fmls_mark.mark(fml);
|
||||
}
|
||||
obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
|
||||
ptr_vector<expr> index2expr;
|
||||
for (; it != end; ++it) {
|
||||
expr* e = it->m_key;
|
||||
for (auto& kv : tids) {
|
||||
expr* e = kv.m_key;
|
||||
if (!var_mark.is_marked(e)) {
|
||||
mark_rec(fmls_mark, e);
|
||||
}
|
||||
index2expr.setx(it->m_value, e, 0);
|
||||
index2expr.setx(kv.m_value, e, 0);
|
||||
}
|
||||
j = 0;
|
||||
unsigned_vector real_vars;
|
||||
|
@ -360,8 +360,7 @@ namespace qe {
|
|||
}
|
||||
vars.resize(j);
|
||||
TRACE("qe", tout << "remaining vars: " << vars << "\n";
|
||||
for (unsigned i = 0; i < real_vars.size(); ++i) {
|
||||
unsigned v = real_vars[i];
|
||||
for (unsigned v : real_vars) {
|
||||
tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
|
||||
}
|
||||
mbo.display(tout););
|
||||
|
@ -449,8 +448,8 @@ namespace qe {
|
|||
|
||||
// extract linear constraints
|
||||
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
linearize(mbo, eval, fmls[i].get(), fmls, tids);
|
||||
for (expr * fml : fmls) {
|
||||
linearize(mbo, eval, fml, fmls, tids);
|
||||
}
|
||||
|
||||
// find optimal value
|
||||
|
@ -459,11 +458,10 @@ namespace qe {
|
|||
|
||||
// update model to use new values that satisfy optimality
|
||||
ptr_vector<expr> vars;
|
||||
obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = it->m_key;
|
||||
for (auto& kv : tids) {
|
||||
expr* e = kv.m_key;
|
||||
if (is_uninterp_const(e)) {
|
||||
unsigned id = it->m_value;
|
||||
unsigned id = kv.m_value;
|
||||
func_decl* f = to_app(e)->get_decl();
|
||||
expr_ref val(a.mk_numeral(mbo.get_value(id), false), m);
|
||||
mdl.register_decl(f, val);
|
||||
|
@ -509,10 +507,9 @@ namespace qe {
|
|||
void extract_coefficients(opt::model_based_opt& mbo, model_evaluator& eval, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
|
||||
coeffs.reset();
|
||||
eval.set_model_completion(true);
|
||||
obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
|
||||
for (; it != end; ++it) {
|
||||
for (auto& kv : ts) {
|
||||
unsigned id;
|
||||
expr* v = it->m_key;
|
||||
expr* v = kv.m_key;
|
||||
if (!tids.find(v, id)) {
|
||||
rational r;
|
||||
expr_ref val = eval(v);
|
||||
|
@ -520,9 +517,9 @@ namespace qe {
|
|||
id = mbo.add_var(r, a.is_int(v));
|
||||
tids.insert(v, id);
|
||||
}
|
||||
CTRACE("qe", it->m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";);
|
||||
if (!it->m_value.is_zero()) {
|
||||
coeffs.push_back(var(id, it->m_value));
|
||||
CTRACE("qe", kv.m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";);
|
||||
if (!kv.m_value.is_zero()) {
|
||||
coeffs.push_back(var(id, kv.m_value));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1311,7 +1311,6 @@ namespace sat {
|
|||
clause_use_list & neg_occs = m_use_list.get(neg_l);
|
||||
unsigned num_pos = pos_occs.size() + num_bin_pos;
|
||||
unsigned num_neg = neg_occs.size() + num_bin_neg;
|
||||
m_elim_counter -= num_pos + num_neg;
|
||||
|
||||
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
|
||||
|
||||
|
@ -1352,8 +1351,6 @@ namespace sat {
|
|||
collect_clauses(pos_l, m_pos_cls);
|
||||
collect_clauses(neg_l, m_neg_cls);
|
||||
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
|
||||
unsigned before_clauses = num_pos + num_neg;
|
||||
unsigned after_clauses = 0;
|
||||
|
@ -1376,7 +1373,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
|
||||
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
// eliminate variable
|
||||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
|
|
|
@ -726,7 +726,7 @@ namespace sat {
|
|||
SASSERT(scope_lvl() == 0);
|
||||
if (m_config.m_dimacs_display) {
|
||||
display_dimacs(std::cout);
|
||||
for (unsigned i = 0; i < num_lits; ++lits) {
|
||||
for (unsigned i = 0; i < num_lits; ++i) {
|
||||
std::cout << dimacs_lit(lits[i]) << " 0\n";
|
||||
}
|
||||
return l_undef;
|
||||
|
|
|
@ -109,10 +109,10 @@ namespace sat {
|
|||
bool operator!=(watched const & w) const { return !operator==(w); }
|
||||
};
|
||||
|
||||
COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3);
|
||||
COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3);
|
||||
COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3);
|
||||
COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3);
|
||||
static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
|
||||
static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
|
||||
static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
|
||||
static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
|
||||
|
||||
struct watched_lt {
|
||||
bool operator()(watched const & w1, watched const & w2) const {
|
||||
|
|
|
@ -1999,7 +1999,7 @@ namespace smt {
|
|||
m_ast_manager(ctx.get_manager()),
|
||||
m_mam(m),
|
||||
m_use_filters(use_filters) {
|
||||
m_args.resize(INIT_ARGS_SIZE, 0);
|
||||
m_args.resize(INIT_ARGS_SIZE);
|
||||
}
|
||||
|
||||
~interpreter() {
|
||||
|
|
|
@ -1286,7 +1286,7 @@ namespace smt {
|
|||
else {
|
||||
if (depth >= m_almost_cg_tables.size()) {
|
||||
unsigned old_sz = m_almost_cg_tables.size();
|
||||
m_almost_cg_tables.resize(depth+1, 0);
|
||||
m_almost_cg_tables.resize(depth+1);
|
||||
for (unsigned i = old_sz; i < depth + 1; i++)
|
||||
m_almost_cg_tables[i] = alloc(almost_cg_table);
|
||||
}
|
||||
|
|
|
@ -67,9 +67,9 @@ namespace smt {
|
|||
};
|
||||
|
||||
// 32 bit machine
|
||||
COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int));
|
||||
static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit");
|
||||
// 64 bit machine
|
||||
COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int));
|
||||
static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit");
|
||||
};
|
||||
|
||||
#endif /* SMT_THEORY_VAR_LIST_H_ */
|
||||
|
|
|
@ -617,8 +617,8 @@ namespace smt {
|
|||
m_else_values.reset();
|
||||
m_parents.reset();
|
||||
m_parents.resize(num_vars, -1);
|
||||
m_defaults.resize(num_vars, 0);
|
||||
m_else_values.resize(num_vars, 0);
|
||||
m_defaults.resize(num_vars);
|
||||
m_else_values.resize(num_vars);
|
||||
|
||||
if (m_use_unspecified_default)
|
||||
return;
|
||||
|
|
|
@ -620,7 +620,7 @@ namespace smt {
|
|||
sort * s = recognizer->get_decl()->get_domain(0);
|
||||
if (d->m_recognizers.empty()) {
|
||||
SASSERT(m_util.is_datatype(s));
|
||||
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), 0);
|
||||
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
|
||||
}
|
||||
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
|
||||
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
|
||||
|
|
|
@ -914,6 +914,8 @@ namespace smt {
|
|||
}
|
||||
verbose_stream() << " + " << m_objective_consts[v] << "\n";);
|
||||
|
||||
unsynch_mpq_manager mgr;
|
||||
unsynch_mpq_inf_manager inf_mgr;
|
||||
unsigned num_nodes = get_num_vars();
|
||||
unsigned num_edges = m_edges.size();
|
||||
S.ensure_var(num_nodes + num_edges + m_objectives.size());
|
||||
|
@ -921,8 +923,9 @@ namespace smt {
|
|||
numeral const& a = m_assignment[i];
|
||||
rational fin = a.get_rational().to_rational();
|
||||
rational inf = a.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(), inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_value(i, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
enode * n = get_enode(i);
|
||||
|
@ -933,7 +936,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
svector<unsigned> vars;
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_mpq_vector coeffs(mgr);
|
||||
coeffs.push_back(mpq(1));
|
||||
coeffs.push_back(mpq(-1));
|
||||
|
@ -954,8 +956,9 @@ namespace smt {
|
|||
numeral const& w = e.m_offset;
|
||||
rational fin = w.get_rational().to_rational();
|
||||
rational inf = w.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(),inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_upper(base_var, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
unsigned w = num_nodes + num_edges + v;
|
||||
|
||||
|
|
|
@ -1107,6 +1107,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
|
|||
|
||||
template<typename Ext>
|
||||
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
||||
unsynch_mpq_manager mgr;
|
||||
unsynch_mpq_inf_manager inf_mgr;
|
||||
unsigned num_nodes = m_graph.get_num_nodes();
|
||||
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
|
||||
S.ensure_var(num_simplex_vars());
|
||||
|
@ -1114,13 +1116,13 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
|||
numeral const& a = m_graph.get_assignment(i);
|
||||
rational fin = a.get_rational().to_rational();
|
||||
rational inf = a.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(), inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_value(node2simplex(i), q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
|
||||
S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
|
||||
svector<unsigned> vars;
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_mpq_vector coeffs(mgr);
|
||||
coeffs.push_back(mpq(1));
|
||||
coeffs.push_back(mpq(-1));
|
||||
|
@ -1145,8 +1147,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
|||
numeral const& w = e.get_weight();
|
||||
rational fin = w.get_rational().to_rational();
|
||||
rational inf = w.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(),inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_upper(base_var, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
else {
|
||||
S.unset_upper(base_var);
|
||||
|
|
|
@ -806,8 +806,9 @@ namespace smt {
|
|||
if (c != 0) {
|
||||
if (m_enable_simplex) {
|
||||
row_info const& info = m_ineq_row_info.find(v);
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_eps_numeral coeff(m_mpq_inf_mgr);
|
||||
coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0));
|
||||
coeff = std::make_pair(mgr.dup(info.m_bound.to_mpq()), mpq(0));
|
||||
unsigned slack = info.m_slack;
|
||||
if (is_true) {
|
||||
update_bound(slack, literal(v), true, coeff);
|
||||
|
|
|
@ -279,7 +279,6 @@ namespace smt {
|
|||
//
|
||||
void compile_ineq(ineq& c);
|
||||
void inc_propagations(ineq& c);
|
||||
unsigned get_compilation_threshold(ineq& c);
|
||||
|
||||
//
|
||||
// Conflict resolution, cutting plane derivation.
|
||||
|
|
|
@ -315,6 +315,7 @@ namespace smt {
|
|||
m_trail.push_back(node);
|
||||
if (!cut_var_map.contains(baseNode)) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map.insert(baseNode, std::stack<T_cut*>());
|
||||
|
@ -323,6 +324,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[baseNode].empty()) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
|
@ -330,6 +332,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[baseNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
|
||||
varInfo->vars[node] = 1;
|
||||
|
@ -359,6 +362,7 @@ namespace smt {
|
|||
|
||||
if (!cut_var_map.contains(destNode)) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
cut_var_map.insert(destNode, std::stack<T_cut*>());
|
||||
|
@ -367,6 +371,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
|
|
|
@ -18,9 +18,12 @@
|
|||
#define _THEORY_STR_H_
|
||||
|
||||
#include "util/trail.h"
|
||||
#include "util/union_find.h"
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/params/theory_str_params.h"
|
||||
#include "smt/proto_model/value_factory.h"
|
||||
|
@ -29,8 +32,6 @@
|
|||
#include<stack>
|
||||
#include<vector>
|
||||
#include<map>
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "util/union_find.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -292,6 +293,7 @@ protected:
|
|||
bool avoidLoopCut;
|
||||
bool loopDetected;
|
||||
obj_map<expr, std::stack<T_cut*> > cut_var_map;
|
||||
scoped_ptr_vector<T_cut> m_cut_allocs;
|
||||
expr_ref m_theoryStrOverlapAssumption_term;
|
||||
|
||||
obj_hashtable<expr> variable_set;
|
||||
|
|
|
@ -85,6 +85,10 @@ namespace smt {
|
|||
watch_list():
|
||||
m_data(0) {
|
||||
}
|
||||
|
||||
watch_list(watch_list && other) : m_data(0) {
|
||||
std::swap(m_data, other.m_data);
|
||||
}
|
||||
|
||||
~watch_list() {
|
||||
destroy();
|
||||
|
|
|
@ -238,7 +238,7 @@ bool bvsls_opt_engine::what_if(
|
|||
|
||||
mpz bvsls_opt_engine::find_best_move(
|
||||
ptr_vector<func_decl> & to_evaluate,
|
||||
mpz score,
|
||||
mpz & score,
|
||||
unsigned & best_const,
|
||||
mpz & best_value,
|
||||
unsigned & new_bit,
|
||||
|
|
|
@ -61,7 +61,7 @@ protected:
|
|||
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
|
||||
mpz & best_score, unsigned & best_const, mpz & best_value);
|
||||
|
||||
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz score,
|
||||
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
|
||||
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
|
||||
mpz const & max_score, expr * objective);
|
||||
|
||||
|
|
|
@ -41,7 +41,24 @@ class sls_tracker {
|
|||
|
||||
struct value_score {
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {};
|
||||
value_score(value_score && other) :
|
||||
m(other.m),
|
||||
value(std::move(other.value)),
|
||||
score(other.score),
|
||||
score_prune(other.score_prune),
|
||||
has_pos_occ(other.has_pos_occ),
|
||||
has_neg_occ(other.has_neg_occ),
|
||||
distance(other.distance),
|
||||
touched(other.touched) {}
|
||||
~value_score() { if (m) m->del(value); }
|
||||
void operator=(value_score && other) {
|
||||
this->~value_score();
|
||||
new (this) value_score(std::move(other));
|
||||
}
|
||||
value_score& operator=(value_score& other) {
|
||||
UNREACHABLE();
|
||||
return *this;
|
||||
}
|
||||
unsynch_mpz_manager * m;
|
||||
mpz value;
|
||||
double score;
|
||||
|
@ -50,15 +67,6 @@ class sls_tracker {
|
|||
unsigned has_neg_occ;
|
||||
unsigned distance; // max distance from any root
|
||||
unsigned touched;
|
||||
value_score & operator=(const value_score & other) {
|
||||
SASSERT(m == 0 || m == other.m);
|
||||
if (m) m->set(value, 0); else m = other.m;
|
||||
m->set(value, other.value);
|
||||
score = other.score;
|
||||
distance = other.distance;
|
||||
touched = other.touched;
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
public:
|
||||
|
@ -294,7 +302,7 @@ public:
|
|||
if (!m_scores.contains(n)) {
|
||||
value_score vs;
|
||||
vs.m = & m_mpz_manager;
|
||||
m_scores.insert(n, vs);
|
||||
m_scores.insert(n, std::move(vs));
|
||||
}
|
||||
|
||||
// Update uplinks
|
||||
|
@ -539,7 +547,7 @@ public:
|
|||
rational r_val;
|
||||
unsigned bv_sz;
|
||||
m_bv_util.is_numeral(val, r_val, bv_sz);
|
||||
mpq q = r_val.to_mpq();
|
||||
const mpq& q = r_val.to_mpq();
|
||||
SASSERT(m_mpz_manager.is_one(q.denominator()));
|
||||
set_value(fd, q.numerator());
|
||||
}
|
||||
|
@ -630,7 +638,7 @@ public:
|
|||
if (m_bv_util.is_bv_sort(s))
|
||||
return get_random_bv(s);
|
||||
else if (m_manager.is_bool(s))
|
||||
return get_random_bool();
|
||||
return m_mpz_manager.dup(get_random_bool());
|
||||
else
|
||||
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
|
||||
}
|
||||
|
@ -653,9 +661,7 @@ public:
|
|||
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
|
||||
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
|
||||
mpz temp = m_zero;
|
||||
set_value(it->m_value, temp);
|
||||
m_mpz_manager.del(temp);
|
||||
set_value(it->m_value, m_zero);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -931,7 +937,7 @@ public:
|
|||
rational q;
|
||||
if (!m_bv_util.is_numeral(n, q, bv_sz))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
mpq temp = q.to_mpq();
|
||||
const mpq& temp = q.to_mpq();
|
||||
SASSERT(m_mpz_manager.is_one(temp.denominator()));
|
||||
m_mpz_manager.set(result, temp.numerator());
|
||||
}
|
||||
|
@ -1039,7 +1045,6 @@ public:
|
|||
unsigned pos = -1;
|
||||
if (m_ucb)
|
||||
{
|
||||
value_score vscore;
|
||||
double max = -1.0;
|
||||
// Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit.
|
||||
/* for (unsigned i = 0; i < m_where_false.size(); i++) {
|
||||
|
@ -1048,7 +1053,7 @@ public:
|
|||
expr * e = as[i];
|
||||
if (m_mpz_manager.neq(get_value(e), m_one))
|
||||
{
|
||||
vscore = m_scores.find(e);
|
||||
value_score & vscore = m_scores.find(e);
|
||||
// Andreas: Select the assertion with the greatest ucb score. Potentially add some noise.
|
||||
// double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
|
||||
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8);
|
||||
|
|
|
@ -63,10 +63,4 @@ public:
|
|||
numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); }
|
||||
};
|
||||
|
||||
template<typename fmanager>
|
||||
inline void del_f_interval(im_float_config<fmanager> & cfg, typename im_float_config<fmanager>::interval & a) {
|
||||
cfg.m().del(a.m_lower);
|
||||
cfg.m().del(a.m_upper);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
@ -125,7 +125,8 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
|
|||
}
|
||||
#endif
|
||||
|
||||
static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) {
|
||||
template <typename T>
|
||||
static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
|
||||
switch (rand()%3) {
|
||||
case 0:
|
||||
// Neg, Neg
|
||||
|
@ -195,11 +196,6 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
|
|||
}
|
||||
}
|
||||
|
||||
static void del_interval(im_default_config & cfg, interval & a) {
|
||||
cfg.m().del(a.m_lower);
|
||||
cfg.m().del(a.m_upper);
|
||||
}
|
||||
|
||||
#define BUFFER_SZ 256
|
||||
static int g_problem_id = 0;
|
||||
static char g_buffer[BUFFER_SZ];
|
||||
|
@ -238,19 +234,18 @@ static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,
|
|||
static void tst_ ## NAME(unsigned N, unsigned magnitude) { \
|
||||
reslimit rl; \
|
||||
unsynch_mpq_manager nm; \
|
||||
im_default_config imc(nm); \
|
||||
interval_manager<im_default_config> im(rl, imc); \
|
||||
interval_manager<im_default_config> im(rl, nm); \
|
||||
interval a, b, r; \
|
||||
\
|
||||
for (unsigned i = 0; i < N; i++) { \
|
||||
mk_random_interval(imc, a, magnitude); \
|
||||
mk_random_interval(imc, b, magnitude); \
|
||||
mk_random_interval(im, a, magnitude); \
|
||||
mk_random_interval(im, b, magnitude); \
|
||||
interval_deps deps; \
|
||||
im.NAME(a, b, r, deps); \
|
||||
\
|
||||
display_lemmas(nm, RES_TERM, a, b, r, deps); \
|
||||
} \
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); \
|
||||
im.del(a); im.del(b); im.del(r); \
|
||||
}
|
||||
|
||||
MK_BINARY(mul, "(* a b)");
|
||||
|
@ -260,56 +255,52 @@ MK_BINARY(sub, "(- a b)");
|
|||
static void tst_neg(unsigned N, unsigned magnitude) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
|
||||
for (unsigned i = 0; i < N; i++) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
interval_deps deps;
|
||||
im.neg(a, r, deps);
|
||||
display_lemmas(nm, "(- a)", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_pw_2(unsigned N, unsigned magnitude) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
|
||||
for (unsigned i = 0; i < N; i++) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
interval_deps deps;
|
||||
im.power(a, 2, r, deps);
|
||||
display_lemmas(nm, "(* a a)", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_pw_3(unsigned N, unsigned magnitude) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
|
||||
for (unsigned i = 0; i < N; i++) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
interval_deps deps;
|
||||
im.power(a, 3, r, deps);
|
||||
display_lemmas(nm, "(* a a a)", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
scoped_mpq p(nm);
|
||||
p = precision;
|
||||
|
@ -317,7 +308,7 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
|
|||
|
||||
unsigned i = 0;
|
||||
while (i < N) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
if (!im.lower_is_neg(a)) {
|
||||
i++;
|
||||
interval_deps deps;
|
||||
|
@ -325,14 +316,13 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
|
|||
display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps);
|
||||
}
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
scoped_mpq p(nm);
|
||||
p = precision;
|
||||
|
@ -340,25 +330,24 @@ static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
|
|||
|
||||
unsigned i = 0;
|
||||
while (i < N) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
i++;
|
||||
interval_deps deps;
|
||||
im.nth_root(a, 3, p, r, deps);
|
||||
display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_inv(unsigned N, unsigned magnitude) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
|
||||
for (unsigned i = 0; i < N; i++) {
|
||||
while (true) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
if (!im.contains_zero(a))
|
||||
break;
|
||||
}
|
||||
|
@ -366,20 +355,19 @@ static void tst_inv(unsigned N, unsigned magnitude) {
|
|||
im.inv(a, r, deps);
|
||||
display_lemmas(nm, "(/ 1 a)", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
static void tst_div(unsigned N, unsigned magnitude) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval a, b, r;
|
||||
|
||||
for (unsigned i = 0; i < N; i++) {
|
||||
mk_random_interval(imc, a, magnitude);
|
||||
mk_random_interval(im, a, magnitude);
|
||||
while (true) {
|
||||
mk_random_interval(imc, b, magnitude);
|
||||
mk_random_interval(im, b, magnitude);
|
||||
if (!im.contains_zero(b))
|
||||
break;
|
||||
}
|
||||
|
@ -387,7 +375,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
|
|||
im.div(a, b, r, deps);
|
||||
display_lemmas(nm, "(/ a b)", a, b, r, deps);
|
||||
}
|
||||
del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
|
||||
#include "test/im_float_config.h"
|
||||
|
@ -396,8 +384,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
|
|||
static void tst_float() {
|
||||
unsynch_mpq_manager qm;
|
||||
mpf_manager fm;
|
||||
im_float_config<mpf_manager> ifc(fm);
|
||||
interval_manager<im_float_config<mpf_manager> > im(ifc);
|
||||
interval_manager<im_float_config<mpf_manager> > im(fm);
|
||||
im_float_config<mpf_manager>::interval a, b, c;
|
||||
scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm);
|
||||
qm.set(minus_one_third, -1, 3);
|
||||
|
@ -424,15 +411,14 @@ static void tst_float() {
|
|||
im.display(std::cout, c);
|
||||
std::cout << "\n";
|
||||
|
||||
del_f_interval(ifc, a); del_f_interval(ifc, b); del_f_interval(ifc, c);
|
||||
im.del(a); im.del(b); im.del(r);
|
||||
}
|
||||
#endif
|
||||
|
||||
void tst_pi() {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
interval r;
|
||||
for (unsigned i = 0; i < 8; i++) {
|
||||
im.pi(i, r);
|
||||
|
@ -440,7 +426,7 @@ void tst_pi() {
|
|||
nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n";
|
||||
ENSURE(nm.lt(im.lower(r), im.upper(r)));
|
||||
}
|
||||
del_interval(imc, r);
|
||||
im.del(r);
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
|
|
@ -10,27 +10,28 @@
|
|||
#include "util/memory_manager.h"
|
||||
#include "util/gparams.h"
|
||||
|
||||
|
||||
//
|
||||
// Unit tests fail by asserting.
|
||||
// If they return, we assume the unit test succeeds
|
||||
// and print "PASS" to indicate success.
|
||||
//
|
||||
|
||||
#define TST(MODULE) { \
|
||||
std::string s("test "); \
|
||||
s += #MODULE; \
|
||||
void tst_##MODULE(); \
|
||||
if (do_display_usage) \
|
||||
std::cout << #MODULE << "\n"; \
|
||||
for (int i = 0; i < argc; i++) \
|
||||
if (test_all || strcmp(argv[i], #MODULE) == 0) { \
|
||||
enable_trace(#MODULE); \
|
||||
enable_debug(#MODULE); \
|
||||
timeit timeit(true, s.c_str()); \
|
||||
tst_##MODULE(); \
|
||||
std::cout << "PASS" << std::endl; \
|
||||
} \
|
||||
}
|
||||
#define TST(MODULE) { \
|
||||
std::string s("test "); \
|
||||
s += #MODULE; \
|
||||
void tst_##MODULE(); \
|
||||
if (do_display_usage) \
|
||||
std::cout << #MODULE << "\n"; \
|
||||
for (int i = 0; i < argc; i++) \
|
||||
if (test_all || strcmp(argv[i], #MODULE) == 0) { \
|
||||
enable_trace(#MODULE); \
|
||||
enable_debug(#MODULE); \
|
||||
timeit timeit(true, s.c_str()); \
|
||||
tst_##MODULE(); \
|
||||
std::cout << "PASS" << std::endl; \
|
||||
} \
|
||||
}
|
||||
|
||||
#define TST_ARGV(MODULE) { \
|
||||
std::string s("test "); \
|
||||
|
@ -207,6 +208,7 @@ int main(int argc, char ** argv) {
|
|||
TST(prime_generator);
|
||||
TST(permutation);
|
||||
TST(nlsat);
|
||||
if (test_all) return 0;
|
||||
TST(ext_numeral);
|
||||
TST(interval);
|
||||
TST(f2n);
|
||||
|
@ -222,7 +224,7 @@ int main(int argc, char ** argv) {
|
|||
TST(heap_trie);
|
||||
TST(karr);
|
||||
TST(no_overflow);
|
||||
TST(memory);
|
||||
// TST(memory);
|
||||
TST(datalog_parser);
|
||||
TST_ARGV(datalog_parser_file);
|
||||
TST(dl_query);
|
||||
|
|
|
@ -698,10 +698,8 @@ static void tst10() {
|
|||
void tst_nlsat() {
|
||||
tst10();
|
||||
std::cout << "------------------\n";
|
||||
exit(0);
|
||||
tst9();
|
||||
std::cout << "------------------\n";
|
||||
exit(0);
|
||||
tst8();
|
||||
std::cout << "------------------\n";
|
||||
tst7();
|
||||
|
|
|
@ -18,8 +18,11 @@ void tst_small_object_allocator() {
|
|||
TRACE("small_object_allocator",
|
||||
tout << "p1: " << (void*)p1 << " q1: " << (void*)q1 << " p2: " << (void*)p2 << "\n";);
|
||||
soa.deallocate(13,p1);
|
||||
soa.deallocate(14,q1);
|
||||
soa.deallocate(13,p2);
|
||||
char * p3 = new (soa) char[13];
|
||||
TRACE("small_object_allocator", tout << "p3: " << (void*)p3 << "\n";);
|
||||
soa.deallocate(13,p3);
|
||||
|
||||
char * r1 = new (soa) char[1];
|
||||
char * r2 = new (soa) char[1];
|
||||
|
@ -36,6 +39,10 @@ void tst_small_object_allocator() {
|
|||
r3 = new (soa) char[1];
|
||||
TRACE("small_object_allocator",
|
||||
tout << "r1: " << (void*)r1 << " r2: " << (void*)r2 << " r3: " << (void*)r3 << " r4: " << (void*)r4 << "\n";);
|
||||
soa.deallocate(1,r1);
|
||||
soa.deallocate(1,r2);
|
||||
soa.deallocate(1,r3);
|
||||
soa.deallocate(1,r4);
|
||||
(void)r1;
|
||||
(void)r2;
|
||||
(void)r3;
|
||||
|
|
|
@ -39,9 +39,8 @@ static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval
|
|||
|
||||
static void tst_sine(std::ostream & out, unsigned N, unsigned k) {
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
reslimit rl;
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
scoped_mpq a(nm);
|
||||
nm.set(a, 0);
|
||||
tst_sine_core(out, nm, im, a, 1);
|
||||
|
@ -67,8 +66,7 @@ static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interv
|
|||
static void tst_cosine(std::ostream & out, unsigned N, unsigned k) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
scoped_mpq a(nm);
|
||||
nm.set(a, 0);
|
||||
tst_cosine_core(out, nm, im, a, 1);
|
||||
|
@ -100,8 +98,7 @@ template<typename fmanager>
|
|||
static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) {
|
||||
reslimit rl;
|
||||
fmanager fm;
|
||||
im_float_config<fmanager> ifc(fm, EBITS, SBITS);
|
||||
interval_manager<im_float_config<fmanager> > im(rl, ifc);
|
||||
interval_manager<im_float_config<fmanager> > im(rl, { fm, EBITS, SBITS });
|
||||
_scoped_numeral<fmanager> a(fm);
|
||||
fm.set(a, EBITS, SBITS, static_cast<int>(0));
|
||||
tst_float_sine_core(out, fm, im, a, 1);
|
||||
|
@ -136,8 +133,7 @@ static void tst_mpf_bug() {
|
|||
static void tst_e(std::ostream & out) {
|
||||
reslimit rl;
|
||||
unsynch_mpq_manager nm;
|
||||
im_default_config imc(nm);
|
||||
interval_manager<im_default_config> im(rl, imc);
|
||||
interval_manager<im_default_config> im(rl, nm);
|
||||
im_default_config::interval r;
|
||||
for (unsigned i = 0; i < 64; i++) {
|
||||
im.e(i, r);
|
||||
|
@ -152,8 +148,7 @@ static void tst_e_float(std::ostream & out) {
|
|||
reslimit rl;
|
||||
unsynch_mpq_manager qm;
|
||||
mpf_manager fm;
|
||||
im_float_config<mpf_manager> ifc(fm);
|
||||
interval_manager<im_float_config<mpf_manager> > im(rl, ifc);
|
||||
interval_manager<im_float_config<mpf_manager> > im(rl, fm);
|
||||
scoped_mpq q(qm);
|
||||
im_float_config<mpf_manager>::interval r;
|
||||
for (unsigned i = 0; i < 64; i++) {
|
||||
|
@ -161,7 +156,7 @@ static void tst_e_float(std::ostream & out) {
|
|||
out << fm.to_rational_string(im.lower(r)) << " <= E\n";
|
||||
out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n";
|
||||
}
|
||||
del_f_interval(ifc, r);
|
||||
im.del(r);
|
||||
}
|
||||
|
||||
void tst_trigo() {
|
||||
|
|
|
@ -29,7 +29,7 @@ public:
|
|||
static const unsigned long long zero = 0ull;
|
||||
static const unsigned long long one = 1ull;
|
||||
};
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8);
|
||||
static_assert(sizeof(unsigned long long) == 8, "");
|
||||
|
||||
template <> class approx_set_traits<unsigned> {
|
||||
public:
|
||||
|
@ -37,7 +37,7 @@ public:
|
|||
static const unsigned zero = 0;
|
||||
static const unsigned one = 1;
|
||||
};
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
|
||||
static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
|
||||
|
||||
template<typename T, typename T2U_Proc, typename R=unsigned long long>
|
||||
class approx_set_tpl : private T2U_Proc {
|
||||
|
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
#include "util/vector.h"
|
||||
#include "util/memory_manager.h"
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
|
||||
static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
|
||||
#define BV_DEFAULT_CAPACITY 2
|
||||
|
||||
class bit_vector {
|
||||
|
|
|
@ -149,6 +149,13 @@ public:
|
|||
new (m_buffer + m_pos) T(elem);
|
||||
m_pos++;
|
||||
}
|
||||
|
||||
void push_back(T && elem) {
|
||||
if (m_pos >= m_capacity)
|
||||
expand();
|
||||
new (m_buffer + m_pos) T(std::move(elem));
|
||||
m_pos++;
|
||||
}
|
||||
|
||||
void pop_back() {
|
||||
if (CallDestructors) {
|
||||
|
|
|
@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag);
|
|||
exit(-1); \
|
||||
}
|
||||
|
||||
#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "")
|
||||
|
||||
void finalize_debug();
|
||||
/*
|
||||
|
|
|
@ -97,7 +97,7 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double));
|
||||
static_assert(sizeof(uint64) == sizeof(double), "");
|
||||
|
||||
#endif /* DOUBLE_MANAGER_H_ */
|
||||
|
||||
|
|
|
@ -46,6 +46,9 @@ public:
|
|||
m_manager.set(m_one, ebits, sbits, 1);
|
||||
}
|
||||
|
||||
f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits),
|
||||
m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {}
|
||||
|
||||
~f2n() {
|
||||
m().del(m_tmp1);
|
||||
m().del(m_one);
|
||||
|
|
|
@ -54,7 +54,7 @@ public:
|
|||
bool is_used() const { return m_state == HT_USED; }
|
||||
T & get_data() { return m_data; }
|
||||
const T & get_data() const { return m_data; }
|
||||
void set_data(const T & d) { m_data = d; m_state = HT_USED; }
|
||||
void set_data(T && d) { m_data = std::move(d); m_state = HT_USED; }
|
||||
void set_hash(unsigned h) { m_hash = h; }
|
||||
void mark_as_deleted() { m_state = HT_DELETED; }
|
||||
void mark_as_free() { m_state = HT_FREE; }
|
||||
|
@ -187,10 +187,42 @@ protected:
|
|||
}
|
||||
}
|
||||
|
||||
static void move_table(entry * source, unsigned source_capacity, entry * target, unsigned target_capacity) {
|
||||
SASSERT(target_capacity >= source_capacity);
|
||||
unsigned target_mask = target_capacity - 1;
|
||||
entry * source_end = source + source_capacity;
|
||||
entry * target_end = target + target_capacity;
|
||||
for (entry * source_curr = source; source_curr != source_end; ++source_curr) {
|
||||
if (source_curr->is_used()) {
|
||||
unsigned hash = source_curr->get_hash();
|
||||
unsigned idx = hash & target_mask;
|
||||
entry * target_begin = target + idx;
|
||||
entry * target_curr = target_begin;
|
||||
for (; target_curr != target_end; ++target_curr) {
|
||||
SASSERT(!target_curr->is_deleted());
|
||||
if (target_curr->is_free()) {
|
||||
*target_curr = std::move(*source_curr);
|
||||
goto end;
|
||||
}
|
||||
}
|
||||
for (target_curr = target; target_curr != target_begin; ++target_curr) {
|
||||
SASSERT(!target_curr->is_deleted());
|
||||
if (target_curr->is_free()) {
|
||||
*target_curr = std::move(*source_curr);
|
||||
goto end;
|
||||
}
|
||||
}
|
||||
UNREACHABLE();
|
||||
end:
|
||||
;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void expand_table() {
|
||||
unsigned new_capacity = m_capacity << 1;
|
||||
entry * new_table = alloc_table(new_capacity);
|
||||
copy_table(m_table, m_capacity, new_table, new_capacity);
|
||||
move_table(m_table, m_capacity, new_table, new_capacity);
|
||||
delete_table();
|
||||
m_table = new_table;
|
||||
m_capacity = new_capacity;
|
||||
|
@ -202,7 +234,7 @@ protected:
|
|||
if (memory::is_out_of_memory())
|
||||
return;
|
||||
entry * new_table = alloc_table(m_capacity);
|
||||
copy_table(m_table, m_capacity, new_table, m_capacity);
|
||||
move_table(m_table, m_capacity, new_table, m_capacity);
|
||||
delete_table();
|
||||
m_table = new_table;
|
||||
m_num_deleted = 0;
|
||||
|
@ -321,7 +353,7 @@ public:
|
|||
#define INSERT_LOOP_BODY() { \
|
||||
if (curr->is_used()) { \
|
||||
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
|
||||
curr->set_data(e); \
|
||||
curr->set_data(std::move(e)); \
|
||||
return; \
|
||||
} \
|
||||
HS_CODE(m_st_collision++;); \
|
||||
|
@ -330,7 +362,7 @@ public:
|
|||
entry * new_entry; \
|
||||
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
|
||||
else { new_entry = curr; } \
|
||||
new_entry->set_data(e); \
|
||||
new_entry->set_data(std::move(e)); \
|
||||
new_entry->set_hash(hash); \
|
||||
m_size++; \
|
||||
return; \
|
||||
|
@ -342,7 +374,7 @@ public:
|
|||
} \
|
||||
} ((void) 0)
|
||||
|
||||
void insert(data const & e) {
|
||||
void insert(data && e) {
|
||||
if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
|
||||
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
|
||||
expand_table();
|
||||
|
@ -363,6 +395,11 @@ public:
|
|||
UNREACHABLE();
|
||||
}
|
||||
|
||||
void insert(const data & e) {
|
||||
data tmp(e);
|
||||
insert(std::move(tmp));
|
||||
}
|
||||
|
||||
#define INSERT_LOOP_CORE_BODY() { \
|
||||
if (curr->is_used()) { \
|
||||
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
|
||||
|
@ -375,7 +412,7 @@ public:
|
|||
entry * new_entry; \
|
||||
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
|
||||
else { new_entry = curr; } \
|
||||
new_entry->set_data(e); \
|
||||
new_entry->set_data(std::move(e)); \
|
||||
new_entry->set_hash(hash); \
|
||||
m_size++; \
|
||||
et = new_entry; \
|
||||
|
@ -393,7 +430,7 @@ public:
|
|||
Return true if it is a new element, and false otherwise.
|
||||
Store the entry/slot of the table in et.
|
||||
*/
|
||||
bool insert_if_not_there_core(data const & e, entry * & et) {
|
||||
bool insert_if_not_there_core(data && e, entry * & et) {
|
||||
if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
|
||||
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
|
||||
expand_table();
|
||||
|
@ -415,6 +452,11 @@ public:
|
|||
return 0;
|
||||
}
|
||||
|
||||
bool insert_if_not_there_core(const data & e, entry * & et) {
|
||||
data temp(e);
|
||||
return insert_if_not_there_core(std::move(temp), et);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Insert the element e if it is not in the table.
|
||||
Return a reference to e or to an object identical to e
|
||||
|
|
|
@ -40,12 +40,6 @@ mpf::mpf(unsigned _ebits, unsigned _sbits):
|
|||
set(ebits, sbits);
|
||||
}
|
||||
|
||||
mpf::mpf(mpf const & other) {
|
||||
// It is safe if the mpz numbers are small.
|
||||
// I need it for resize method in vector.
|
||||
// UNREACHABLE();
|
||||
}
|
||||
|
||||
mpf::~mpf() {
|
||||
}
|
||||
|
||||
|
@ -73,7 +67,7 @@ mpf_manager::~mpf_manager() {
|
|||
}
|
||||
|
||||
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) {
|
||||
COMPILE_TIME_ASSERT(sizeof(int) == 4);
|
||||
static_assert(sizeof(int) == 4, "assume integers are 4 bytes");
|
||||
|
||||
o.sign = false;
|
||||
o.ebits = ebits;
|
||||
|
@ -119,7 +113,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
|
|||
|
||||
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
|
||||
// double === mpf(11, 53)
|
||||
COMPILE_TIME_ASSERT(sizeof(double) == 8);
|
||||
static_assert(sizeof(double) == 8, "doubles are 8 bytes");
|
||||
|
||||
uint64 raw;
|
||||
memcpy(&raw, &value, sizeof(double));
|
||||
|
@ -155,7 +149,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
|
|||
|
||||
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) {
|
||||
// single === mpf(8, 24)
|
||||
COMPILE_TIME_ASSERT(sizeof(float) == 4);
|
||||
static_assert(sizeof(float) == 4, "floats are 4 bytes");
|
||||
|
||||
unsigned int raw;
|
||||
memcpy(&raw, &value, sizeof(float));
|
||||
|
|
|
@ -50,7 +50,12 @@ class mpf {
|
|||
public:
|
||||
mpf();
|
||||
mpf(unsigned ebits, unsigned sbits);
|
||||
mpf(mpf const & other);
|
||||
mpf(mpf && other) :
|
||||
ebits(other.ebits),
|
||||
sbits(other.sbits),
|
||||
sign(other.sign),
|
||||
significand(std::move(other.significand)),
|
||||
exponent(other.exponent) {}
|
||||
~mpf();
|
||||
unsigned get_ebits() const { return ebits; }
|
||||
unsigned get_sbits() const { return sbits; }
|
||||
|
|
|
@ -27,8 +27,8 @@ Revision History:
|
|||
#include "util/bit_util.h"
|
||||
#include "util/trace.h"
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned));
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
|
||||
static_assert(sizeof(mpn_digit) == sizeof(unsigned), "");
|
||||
static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while");
|
||||
|
||||
// MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word.
|
||||
#define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1))
|
||||
|
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
#define max(a,b) (((a) > (b)) ? (a) : (b))
|
||||
|
||||
typedef uint64 mpn_double_digit;
|
||||
COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit));
|
||||
static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment");
|
||||
|
||||
const mpn_digit mpn_manager::zero = 0;
|
||||
|
||||
|
|
|
@ -31,11 +31,10 @@ class mpq {
|
|||
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)) {}
|
||||
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; }
|
||||
|
||||
double get_double() const;
|
||||
};
|
||||
|
||||
inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
|
||||
|
@ -745,6 +744,12 @@ public:
|
|||
reset_denominator(a);
|
||||
}
|
||||
|
||||
mpq dup(const mpq & source) {
|
||||
mpq temp;
|
||||
set(temp, source);
|
||||
return temp;
|
||||
}
|
||||
|
||||
void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
|
||||
|
||||
void swap(mpq & a, mpq & b) {
|
||||
|
|
|
@ -558,7 +558,7 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
|
|||
|
||||
template<bool SYNCH>
|
||||
void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
|
||||
COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
|
||||
static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch");
|
||||
if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
|
||||
int _a = a.m_val;
|
||||
int _b = b.m_val;
|
||||
|
@ -724,7 +724,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
|
|||
|
||||
#ifdef LEHMER_GCD
|
||||
// For now, it only works if sizeof(digit_t) == sizeof(unsigned)
|
||||
COMPILE_TIME_ASSERT(sizeof(digit_t) == sizeof(unsigned));
|
||||
static_assert(sizeof(digit_t) == sizeof(unsigned), "");
|
||||
|
||||
int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz;
|
||||
mpz a1, b1, t, r, tmp;
|
||||
|
@ -1754,7 +1754,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
|
|||
}
|
||||
|
||||
#ifndef _MP_GMP
|
||||
COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8);
|
||||
static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, "");
|
||||
#endif
|
||||
|
||||
template<bool SYNCH>
|
||||
|
@ -1821,7 +1821,7 @@ unsigned mpz_manager<SYNCH>::log2(mpz const & a) {
|
|||
if (is_small(a))
|
||||
return ::log2((unsigned)a.m_val);
|
||||
#ifndef _MP_GMP
|
||||
COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
|
||||
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
|
||||
mpz_cell * c = a.m_ptr;
|
||||
unsigned sz = c->m_size;
|
||||
digit_t * ds = c->m_digits;
|
||||
|
@ -1843,7 +1843,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
|
|||
if (is_small(a))
|
||||
return ::log2((unsigned)-a.m_val);
|
||||
#ifndef _MP_GMP
|
||||
COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
|
||||
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
|
||||
mpz_cell * c = a.m_ptr;
|
||||
unsigned sz = c->m_size;
|
||||
digit_t * ds = c->m_digits;
|
||||
|
|
|
@ -94,6 +94,9 @@ class mpz {
|
|||
public:
|
||||
mpz(int v):m_val(v), m_ptr(0) {}
|
||||
mpz():m_val(0), m_ptr(0) {}
|
||||
mpz(mpz && other) : m_val(other.m_val), m_ptr(0) {
|
||||
std::swap(m_ptr, other.m_ptr);
|
||||
}
|
||||
void swap(mpz & other) {
|
||||
std::swap(m_val, other.m_val);
|
||||
std::swap(m_ptr, other.m_ptr);
|
||||
|
@ -668,6 +671,12 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void set(mpz & target, mpz && source) {
|
||||
del(target);
|
||||
target.m_val = source.m_val;
|
||||
std::swap(target.m_ptr, source.m_ptr);
|
||||
}
|
||||
|
||||
void set(mpz & a, int val) {
|
||||
del(a);
|
||||
a.m_val = val;
|
||||
|
@ -700,6 +709,12 @@ public:
|
|||
|
||||
void set(mpz & target, unsigned sz, digit_t const * digits);
|
||||
|
||||
mpz dup(const mpz & source) {
|
||||
mpz temp;
|
||||
set(temp, source);
|
||||
return temp;
|
||||
}
|
||||
|
||||
void reset(mpz & a) {
|
||||
del(a);
|
||||
a.m_val = 0;
|
||||
|
|
|
@ -69,6 +69,10 @@ public:
|
|||
m_key(k),
|
||||
m_value(v) {
|
||||
}
|
||||
key_data(Key * k, Value && v) :
|
||||
m_key(k),
|
||||
m_value(std::move(v)) {
|
||||
}
|
||||
Value const & get_value() const { return m_value; }
|
||||
Key & get_key () const { return *m_key; }
|
||||
unsigned hash() const { return m_key->hash(); }
|
||||
|
@ -86,7 +90,7 @@ public:
|
|||
bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
|
||||
key_data const & get_data() const { return m_data; }
|
||||
key_data & get_data() { return m_data; }
|
||||
void set_data(key_data const & d) { m_data = d; }
|
||||
void set_data(key_data && d) { m_data = std::move(d); }
|
||||
void set_hash(unsigned h) { SASSERT(h == m_data.hash()); }
|
||||
void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
|
||||
void mark_as_free() { m_data.m_key = 0; }
|
||||
|
@ -137,6 +141,10 @@ public:
|
|||
void insert(Key * const k, Value const & v) {
|
||||
m_table.insert(key_data(k, v));
|
||||
}
|
||||
|
||||
void insert(Key * const k, Value && v) {
|
||||
m_table.insert(key_data(k, std::move(v)));
|
||||
}
|
||||
|
||||
key_data const & insert_if_not_there(Key * k, Value const & v) {
|
||||
return m_table.insert_if_not_there(key_data(k, v));
|
||||
|
|
|
@ -53,6 +53,10 @@ public:
|
|||
inc_ref();
|
||||
}
|
||||
|
||||
obj_ref(obj_ref && other) : m_obj(0), m_manager(other.m_manager) {
|
||||
std::swap(m_obj, other.m_obj);
|
||||
}
|
||||
|
||||
~obj_ref() { dec_ref(); }
|
||||
|
||||
TManager & get_manager() const { return m_manager; }
|
||||
|
|
|
@ -41,6 +41,7 @@ public:
|
|||
rational() {}
|
||||
|
||||
rational(rational const & r) { m().set(m_val, r.m_val); }
|
||||
rational(rational && r) : m_val(std::move(r.m_val)) {}
|
||||
|
||||
explicit rational(int n) { m().set(m_val, n); }
|
||||
|
||||
|
|
|
@ -45,6 +45,10 @@ public:
|
|||
typedef T * data;
|
||||
|
||||
ref_vector_core(Ref const & r = Ref()):Ref(r) {}
|
||||
|
||||
ref_vector_core(ref_vector_core && other) :
|
||||
Ref(std::move(other)),
|
||||
m_nodes(std::move(other.m_nodes)) {}
|
||||
|
||||
~ref_vector_core() {
|
||||
dec_range_ref(m_nodes.begin(), m_nodes.end());
|
||||
|
@ -63,7 +67,7 @@ public:
|
|||
void resize(unsigned sz) {
|
||||
if (sz < m_nodes.size())
|
||||
dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
|
||||
m_nodes.resize(sz, 0);
|
||||
m_nodes.resize(sz);
|
||||
}
|
||||
|
||||
void resize(unsigned sz, T * d) {
|
||||
|
@ -80,7 +84,7 @@ public:
|
|||
void reserve(unsigned sz) {
|
||||
if (sz <= m_nodes.size())
|
||||
return;
|
||||
m_nodes.resize(sz, 0);
|
||||
m_nodes.resize(sz);
|
||||
}
|
||||
|
||||
void shrink(unsigned sz) {
|
||||
|
@ -207,6 +211,8 @@ public:
|
|||
this->append(other);
|
||||
}
|
||||
|
||||
ref_vector(ref_vector && other) : super(std::move(other)) {}
|
||||
|
||||
ref_vector(TManager & m, unsigned sz, T * const * data):
|
||||
super(ref_manager_wrapper<T, TManager>(m)) {
|
||||
this->append(sz, data);
|
||||
|
|
|
@ -63,8 +63,7 @@ public:
|
|||
unsigned old_sz = this->size();
|
||||
if (sz <= old_sz)
|
||||
shrink(sz);
|
||||
typename Manager::numeral zero(0);
|
||||
svector<typename Manager::numeral>::resize(sz, zero);
|
||||
svector<typename Manager::numeral>::resize(sz, 0);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -42,7 +42,7 @@ public:
|
|||
bool empty() const { return m_vector.empty(); }
|
||||
void resize(unsigned sz) {
|
||||
if (sz < m_vector.size()) {
|
||||
for (unsigned i = m_vector.size(); i < sz; i++)
|
||||
for (unsigned i = m_vector.size(); i-- > sz; )
|
||||
dealloc(m_vector[i]);
|
||||
m_vector.shrink(sz);
|
||||
}
|
||||
|
|
|
@ -22,7 +22,6 @@ Revision History:
|
|||
#include "util/util.h"
|
||||
#include "util/vector.h"
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
|
||||
|
||||
class uint_set : unsigned_vector {
|
||||
|
||||
|
|
|
@ -33,13 +33,13 @@ Revision History:
|
|||
typedef unsigned long long uint64;
|
||||
#endif
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(uint64) == 8);
|
||||
static_assert(sizeof(uint64) == 8, "64 bits please");
|
||||
|
||||
#ifndef int64
|
||||
typedef long long int64;
|
||||
#endif
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(int64) == 8);
|
||||
static_assert(sizeof(int64) == 8, "64 bits");
|
||||
|
||||
#ifndef INT64_MIN
|
||||
#define INT64_MIN static_cast<int64>(0x8000000000000000ull)
|
||||
|
@ -111,7 +111,7 @@ inline unsigned next_power_of_two(unsigned v) {
|
|||
unsigned log2(unsigned v);
|
||||
unsigned uint64_log2(uint64 v);
|
||||
|
||||
COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
|
||||
static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");
|
||||
|
||||
// Return the number of 1 bits in v.
|
||||
static inline unsigned get_num_1bits(unsigned v) {
|
||||
|
@ -322,7 +322,7 @@ bool compare_arrays(const T * array1, const T * array2, unsigned size) {
|
|||
template<typename T>
|
||||
void force_ptr_array_size(T & v, unsigned sz) {
|
||||
if (sz > v.size()) {
|
||||
v.resize(sz, 0);
|
||||
v.resize(sz);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -26,6 +26,7 @@ Revision History:
|
|||
|
||||
#include "util/debug.h"
|
||||
#include<algorithm>
|
||||
#include<type_traits>
|
||||
#include<memory.h>
|
||||
#include "util/memory_manager.h"
|
||||
#include "util/hash.h"
|
||||
|
@ -74,9 +75,27 @@ class vector {
|
|||
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
|
||||
throw default_exception("Overflow encountered when expanding vector");
|
||||
}
|
||||
SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
|
||||
*mem = new_capacity;
|
||||
m_data = reinterpret_cast<T *>(mem + 2);
|
||||
SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
|
||||
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
|
||||
if (__has_trivial_copy(T)) {
|
||||
#else
|
||||
if (std::is_trivially_copyable<T>::value) {
|
||||
#endif
|
||||
mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
|
||||
m_data = reinterpret_cast<T *>(mem + 2);
|
||||
} else {
|
||||
mem = (SZ*)memory::allocate(new_capacity_T);
|
||||
auto old_data = m_data;
|
||||
auto old_size = size();
|
||||
mem[1] = old_size;
|
||||
m_data = reinterpret_cast<T *>(mem + 2);
|
||||
for (unsigned i = 0; i < old_size; ++i) {
|
||||
new (&m_data[i]) T(std::move(old_data[i]));
|
||||
old_data[i].~T();
|
||||
}
|
||||
memory::deallocate(old_mem);
|
||||
}
|
||||
*mem = new_capacity;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -148,6 +167,10 @@ public:
|
|||
SASSERT(size() == source.size());
|
||||
}
|
||||
|
||||
vector(vector&& other) : m_data(0) {
|
||||
std::swap(m_data, other.m_data);
|
||||
}
|
||||
|
||||
vector(SZ s, T const * data):
|
||||
m_data(0) {
|
||||
for (SZ i = 0; i < s; i++) {
|
||||
|
@ -179,6 +202,16 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
vector & operator=(vector && source) {
|
||||
if (this == &source) {
|
||||
return *this;
|
||||
}
|
||||
destroy();
|
||||
m_data = 0;
|
||||
std::swap(m_data, source.m_data);
|
||||
return *this;
|
||||
}
|
||||
|
||||
void reset() {
|
||||
if (m_data) {
|
||||
if (CallDestructors) {
|
||||
|
@ -292,6 +325,11 @@ public:
|
|||
m_data[idx] = val;
|
||||
}
|
||||
|
||||
void set(SZ idx, T && val) {
|
||||
SASSERT(idx < size());
|
||||
m_data[idx] = std::move(val);
|
||||
}
|
||||
|
||||
T & back() {
|
||||
SASSERT(!empty());
|
||||
return operator[](size() - 1);
|
||||
|
@ -318,6 +356,14 @@ public:
|
|||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
}
|
||||
|
||||
void push_back(T && elem) {
|
||||
if (m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
|
||||
expand_vector();
|
||||
}
|
||||
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
}
|
||||
|
||||
void insert(T const & elem) {
|
||||
push_back(elem);
|
||||
}
|
||||
|
@ -357,7 +403,8 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void resize(SZ s, T const & elem=T()) {
|
||||
template<typename Args>
|
||||
void resize(SZ s, Args args...) {
|
||||
SZ sz = size();
|
||||
if (s <= sz) { shrink(s); return; }
|
||||
while (s > capacity()) {
|
||||
|
@ -367,8 +414,23 @@ public:
|
|||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
|
||||
iterator it = m_data + sz;
|
||||
iterator end = m_data + s;
|
||||
for(; it != end; ++it) {
|
||||
new (it) T(elem);
|
||||
for (; it != end; ++it) {
|
||||
new (it) T(std::forward<Args>(args));
|
||||
}
|
||||
}
|
||||
|
||||
void resize(SZ s) {
|
||||
SZ sz = size();
|
||||
if (s <= sz) { shrink(s); return; }
|
||||
while (s > capacity()) {
|
||||
expand_vector();
|
||||
}
|
||||
SASSERT(m_data != 0);
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
|
||||
iterator it = m_data + sz;
|
||||
iterator end = m_data + s;
|
||||
for (; it != end; ++it) {
|
||||
new (it) T();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -439,10 +501,15 @@ public:
|
|||
return m_data[idx];
|
||||
}
|
||||
|
||||
void reserve(SZ s, T const & d = T()) {
|
||||
void reserve(SZ s, T const & d) {
|
||||
if (s > size())
|
||||
resize(s, d);
|
||||
}
|
||||
|
||||
void reserve(SZ s) {
|
||||
if (s > size())
|
||||
resize(s);
|
||||
}
|
||||
};
|
||||
|
||||
template<typename T>
|
||||
|
@ -452,7 +519,12 @@ 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(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);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
template<typename T, typename SZ = unsigned>
|
||||
|
@ -462,7 +534,12 @@ 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(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
|
||||
svector & operator=(svector const & source) {
|
||||
vector<T, false, SZ>::operator=(source);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
typedef svector<int> int_vector;
|
||||
|
@ -494,23 +571,4 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
|
|||
template<typename Hash>
|
||||
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
|
||||
|
||||
#include <vector>
|
||||
// Specialize vector<std::string> to be an instance of std::vector instead.
|
||||
// This will catch any regression of issue #564 and #420.
|
||||
|
||||
template <>
|
||||
class vector<std::string, true, unsigned> : public std::vector<std::string> {
|
||||
public:
|
||||
vector(vector<std::string, true, unsigned> const& other): std::vector<std::string>(other) {}
|
||||
vector(size_t sz, char const* s): std::vector<std::string>(sz, s) {}
|
||||
vector() {}
|
||||
|
||||
void reset() { clear(); }
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif /* VECTOR_H_ */
|
||||
|
||||
|
|
Loading…
Reference in a new issue