mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-03-13 12:09:25 -04:00
commit 3dfc0a93f6
29 changed files with 920 additions and 801 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -38,6 +38,7 @@ public:
tactic_report report("ackermannize", *g);
fail_if_unsat_core_generation("ackermannize", g);
fail_if_proof_generation("ackermannize", g);
TRACE("ackermannize", g->display(tout << "in\n"););
expr_ref_vector flas(m);
const unsigned sz = g->size();
@ -48,6 +49,7 @@ public:
goal_ref resg(alloc(goal, *g, true));
const bool success = lackr.mk_ackermann(resg, m_lemma_limit);
if (!success) { // Just pass on the input unchanged
TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;);
result.reset();
result.push_back(g.get());
mc = 0;
@ -62,7 +64,7 @@ public:
}
resg->inc_depth();
TRACE("ackermannize", resg->display(tout););
TRACE("ackermannize", resg->display(tout << "out\n"););
SASSERT(resg->is_well_sorted());
}

45
src/ackermannization/lackr_model_constructor.cpp
View file

@ -34,11 +34,13 @@ struct lackr_model_constructor::imp {
, m_conflicts(conflicts)
, m_b_rw(m)
, m_bv_rw(m)
, m_evaluator(NULL)
, m_empty_model(m)
, m_ackr_helper(m)
{}
~imp() {
if (m_evaluator) dealloc(m_evaluator);
{
values2val_t::iterator i = m_values2val.begin();
const values2val_t::iterator e = m_values2val.end();
@ -60,15 +62,17 @@ struct lackr_model_constructor::imp {
//
// Returns true iff model was successfully constructed.
// Conflicts are saved as a side effect.
//
bool check() {
bool retv = true;
for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
func_decl * const c = m_abstr_model->get_constant(i);
app * const term = m_info->find_term(c);
if (term) m_stack.push_back(term);
else m_stack.push_back(m_m.mk_const(c));
app * const _term = m_info->find_term(c);
expr * const term = _term ? _term : m_m.mk_const(c);
if (!check_term(term)) retv = false;
}
return run();
return retv;
}
@ -134,7 +138,7 @@ struct lackr_model_constructor::imp {
conflict_list& m_conflicts;
bool_rewriter m_b_rw;
bv_rewriter m_bv_rw;
scoped_ptr<model_evaluator> m_evaluator;
model_evaluator * m_evaluator;
model m_empty_model;
private:
struct val_info { expr * value; app * source_term; };
@ -144,6 +148,7 @@ struct lackr_model_constructor::imp {
app2val_t m_app2val;
ptr_vector<expr> m_stack;
ackr_helper m_ackr_helper;
expr_mark m_visited;
static inline val_info mk_val_info(expr* value, app* source_term) {
val_info rv;
@ -152,17 +157,23 @@ struct lackr_model_constructor::imp {
return rv;
}
//
// Performs congruence check on a given term.
bool check_term(expr * term) {
m_stack.push_back(term);
const bool rv = _check_stack();
m_stack.reset();
return rv;
}
// Performs congruence check on terms on the stack.
// (Currently stops upon the first failure).
// Returns true if and only if congruence check succeeded.
bool run() {
m_evaluator = alloc(model_evaluator, m_empty_model);
expr_mark visited;
// Stops upon the first failure.
// Returns true if and only if all congruence checks succeeded.
bool _check_stack() {
if (m_evaluator == NULL) m_evaluator = alloc(model_evaluator, m_empty_model);
expr * curr;
while (!m_stack.empty()) {
curr = m_stack.back();
if (visited.is_marked(curr)) {
if (m_visited.is_marked(curr)) {
m_stack.pop_back();
continue;
}
@ -173,8 +184,8 @@ struct lackr_model_constructor::imp {
return false;
case AST_APP: {
app * a = to_app(curr);
if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) {
visited.mark(a, true);
if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) {
m_visited.mark(a, true);
m_stack.pop_back();
if (!mk_value(a)) return false;
}
@ -212,7 +223,11 @@ struct lackr_model_constructor::imp {
for (unsigned i = 0; i < num; ++i) {
expr * val;
const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); );
CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; );
if (!b) {
// bailing out because args eval failed previously
return false;
}
TRACE("model_constructor", tout <<
"arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
<< " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );

108
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1155,38 +1155,34 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
expr_ref res(m);
// The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0.
// There is no "hardware interpretation" for fp.min.
if (m_hi_fp_unspecified)
// The hardware interpretation is -0.0.
mk_nzero(f, res);
else {
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;
}
@ -1244,38 +1240,34 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
expr_ref res(m);
// The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0.
// There is no "hardware interpretation" for fp.max.
if (m_hi_fp_unspecified)
// The hardware interpretation is +0.0.
mk_pzero(f, res);
else {
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
std::pair<app*, app*> decls(0, 0);
if (!m_specials.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
m_specials.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
m.inc_ref(decls.second);
}
expr_ref pn(m), np(m);
mk_fp(decls.first,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
pn);
mk_fp(decls.second,
m_bv_util.mk_numeral(0, ebits),
m_bv_util.mk_numeral(0, sbits - 1),
np);
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;
}

72
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -28,7 +28,7 @@ fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c,
m_manager(m),
m_out(m),
m_conv(c),
m_bindings(m)
m_bindings(m)
{
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
@ -49,7 +49,7 @@ void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) {
updt_local_params(p);
}
bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
return num_steps > m_max_steps;
}
@ -57,22 +57,22 @@ bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const {
br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " <<
mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
@ -100,7 +100,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
@ -108,7 +108,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_POSITIVE:
case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
@ -120,7 +120,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
@ -129,7 +129,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
@ -143,20 +143,20 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE;
case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
@ -167,27 +167,27 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
else {
SASSERT(!m_conv.is_float_family(f));
bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
for (unsigned i = 0; i < f->get_arity(); i++) {
sort * di = f->get_domain()[i];
is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
}
if (is_float_uf) {
m_conv.mk_uninterpreted_function(f, num, args, result);
return BR_DONE;
}
}
return BR_FAILED;
}
bool fpa2bv_rewriter_cfg::pre_visit(expr * t)
{
TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
sort_ref_vector new_bindings(m_manager);
for (unsigned i = 0 ; i < q->get_num_decls(); i++)
@ -199,9 +199,9 @@ bool fpa2bv_rewriter_cfg::pre_visit(expr * t)
}
bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
@ -221,7 +221,7 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
name_buffer.reset();
name_buffer << n << ".bv";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits));
}
else {
new_decl_sorts.push_back(s);
@ -232,19 +232,19 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
m_bindings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
m_bindings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
expr_ref new_exp(m());
sort * s = t->get_sort();
if (m_conv.is_float(s))
@ -255,14 +255,14 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits));
m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var),
m_conv.bu().mk_extract(ebits - 1, 0, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var),
new_exp);
}
else
new_exp = m().mk_var(t->get_idx(), s);
result = new_exp;
result_pr = 0;
result_pr = 0;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}

10
src/ast/fpa_decl_plugin.cpp
View file

@ -593,7 +593,7 @@ func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_paramet
}
func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
if (arity != 3)
m_manager->raise_exception("invalid number of arguments to fp");
if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
@ -610,7 +610,7 @@ func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, paramet
}
func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
SASSERT(m_bv_plugin);
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to fp.to_ubv");
@ -631,7 +631,7 @@ func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, par
}
func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
SASSERT(m_bv_plugin);
if (arity != 2)
m_manager->raise_exception("invalid number of arguments to fp.to_sbv");
@ -671,9 +671,9 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters,
unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
parameter ps[] = { parameter(float_sz) };
sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
sort * bv_srt = m_bv_plugin->mk_sort(BV_SORT, 1, ps);
symbol name("to_ieee_bv");
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));
return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k));
}
func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters,

6
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -150,11 +150,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
}
br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_int());
unsigned bv_sz = f->get_parameter(0).get_int();
bv_util bu(m());
unsigned bv_sz = bu.get_bv_size(f->get_range());
if (m_hi_fp_unspecified)
// The "hardware interpretation" is 0.
result = bu.mk_numeral(0, bv_sz);

2
src/muz/pdr/pdr_sym_mux.cpp
View file

@ -32,7 +32,7 @@ sym_mux::sym_mux(ast_manager & m)
: m(m), m_ref_holder(m),
m_next_sym_suffix_idx(0) {
m_suffixes.push_back("_n");
unsigned suf_sz = m_suffixes.size();
size_t suf_sz = m_suffixes.size();
for(unsigned i = 0; i < suf_sz; ++i) {
symbol suff_sym = symbol(m_suffixes[i].c_str());
m_used_suffixes.insert(suff_sym);

6
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -72,7 +72,7 @@ public:
m_asmsf(m),
m_fmls_head(0),
m_core(m),
m_map(m),
m_map(m),
m_num_scopes(0),
m_dep_core(m),
m_unknown("no reason given") {
@ -214,7 +214,7 @@ public:
m_optimize_model = m_params.get_bool("optimize_model", false);
}
virtual void collect_statistics(statistics & st) const {
m_preprocess->collect_statistics(st);
if (m_preprocess) m_preprocess->collect_statistics(st);
m_solver.collect_statistics(st);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
@ -440,7 +440,7 @@ private:
DEBUG_CODE(
for (unsigned i = 0; i < m_fmls.size(); ++i) {
expr_ref tmp(m);
if (m_model->eval(m_fmls[i].get(), tmp, true)) {
if (m_model->eval(m_fmls[i].get(), tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";

159
src/tactic/core/reduce_args_tactic.cpp
View file

@ -83,14 +83,34 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
struct reduce_args_tactic::imp {
ast_manager & m_manager;
bool m_produce_models;
bv_util m_bv;
ast_manager & m() const { return m_manager; }
imp(ast_manager & m):
m_manager(m) {
m_manager(m),
m_bv(m) {
}
static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
expr *lhs, *rhs;
if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) {
base = rhs;
} else {
base = e;
}
return true;
}
static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {
base = 0;
return m.is_unique_value(e) || is_var_plus_offset(m, bv, e, base);
}
static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e) {
expr* base;
return may_be_unique(m, bv, e, base);
}
void checkpoint() {
if (m_manager.canceled())
@ -100,10 +120,12 @@ struct reduce_args_tactic::imp {
struct find_non_candidates_proc {
ast_manager & m_manager;
bv_util & m_bv;
obj_hashtable<func_decl> & m_non_cadidates;
find_non_candidates_proc(ast_manager & m, obj_hashtable<func_decl> & non_cadidates):
find_non_candidates_proc(ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & non_cadidates):
m_manager(m),
m_bv(bv),
m_non_cadidates(non_cadidates) {
}
@ -122,7 +144,7 @@ struct reduce_args_tactic::imp {
unsigned j = n->get_num_args();
while (j > 0) {
--j;
if (m_manager.is_unique_value(n->get_arg(j)))
if (may_be_unique(m_manager, m_bv, n->get_arg(j)))
return;
}
m_non_cadidates.insert(d);
@ -135,7 +157,7 @@ struct reduce_args_tactic::imp {
*/
void find_non_candidates(goal const & g, obj_hashtable<func_decl> & non_candidates) {
non_candidates.reset();
find_non_candidates_proc proc(m_manager, non_candidates);
find_non_candidates_proc proc(m_manager, m_bv, non_candidates);
expr_fast_mark1 visited;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
@ -154,11 +176,13 @@ struct reduce_args_tactic::imp {
struct populate_decl2args_proc {
ast_manager & m_manager;
bv_util & m_bv;
obj_hashtable<func_decl> & m_non_cadidates;
obj_map<func_decl, bit_vector> & m_decl2args;
populate_decl2args_proc(ast_manager & m, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
m_manager(m), m_non_cadidates(nc), m_decl2args(d) {}
obj_map<func_decl, svector<expr*> > m_decl2base; // for args = base + offset
populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
m_manager(m), m_bv(bv), m_non_cadidates(nc), m_decl2args(d) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
@ -172,20 +196,25 @@ struct reduce_args_tactic::imp {
return; // declaration is not a candidate
unsigned j = n->get_num_args();
obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
expr* base;
if (it == m_decl2args.end()) {
m_decl2args.insert(d, bit_vector());
svector<expr*>& bases = m_decl2base.insert_if_not_there2(d, svector<expr*>())->get_data().m_value;
bases.resize(j);
it = m_decl2args.find_iterator(d);
SASSERT(it != m_decl2args.end());
it->m_value.reserve(j);
while (j > 0) {
--j;
it->m_value.set(j, m_manager.is_unique_value(n->get_arg(j)));
it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base));
bases[j] = base;
}
} else {
svector<expr*>& bases = m_decl2base[d];
SASSERT(j == it->m_value.size());
while (j > 0) {
--j;
it->m_value.set(j, it->m_value.get(j) && m_manager.is_unique_value(n->get_arg(j)));
it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base);
}
}
}
@ -196,7 +225,7 @@ struct reduce_args_tactic::imp {
obj_map<func_decl, bit_vector> & decl2args) {
expr_fast_mark1 visited;
decl2args.reset();
populate_decl2args_proc proc(m_manager, non_candidates, decl2args);
populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
@ -291,67 +320,6 @@ struct reduce_args_tactic::imp {
}
}
};
struct populate_decl2arg_set_proc {
ast_manager & m_manager;
obj_map<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs;
populate_decl2arg_set_proc(ast_manager & m,
obj_map<func_decl, bit_vector> & d,
decl2arg2func_map & ds):
m_manager(m), m_decl2args(d), m_decl2arg2funcs(ds) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (n->get_num_args() == 0)
return; // ignore constants
func_decl * d = n->get_decl();
if (d->get_family_id() != null_family_id)
return; // ignore interpreted symbols
obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
if (it == m_decl2args.end())
return; // not reducing the arguments of this declaration
bit_vector & bv = it->m_value;
arg2func * map = 0;
decl2arg2func_map::iterator it2 = m_decl2arg2funcs.find_iterator(d);
if (it2 == m_decl2arg2funcs.end()) {
map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
m_decl2arg2funcs.insert(d, map);
}
else {
map = it2->m_value;
}
if (!map->contains(n)) {
// create fresh symbol...
ptr_buffer<sort> domain;
unsigned arity = d->get_arity();
for (unsigned i = 0; i < arity; i++) {
if (!bv.get(i))
domain.push_back(d->get_domain(i));
}
func_decl * new_d = m_manager.mk_fresh_func_decl(d->get_name(), symbol::null, domain.size(), domain.c_ptr(), d->get_range());
map->insert(n, new_d);
m_manager.inc_ref(n);
m_manager.inc_ref(new_d);
}
}
};
void populate_decl2arg_set(goal const & g,
obj_map<func_decl, bit_vector> & decl2args,
decl2arg2func_map & decl2arg2funcs) {
expr_fast_mark1 visited;
populate_decl2arg_set_proc proc(m_manager, decl2args, decl2arg2funcs);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
quick_for_each_expr(proc, visited, g.form(i));
}
}
struct reduce_args_rw_cfg : public default_rewriter_cfg {
ast_manager & m;
@ -377,24 +345,31 @@ struct reduce_args_tactic::imp {
return BR_FAILED; // ignore constants
if (f->get_family_id() != null_family_id)
return BR_FAILED; // ignore interpreted symbols
decl2arg2func_map::iterator it = m_decl2arg2funcs.find_iterator(f);
if (it == m_decl2arg2funcs.end())
obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(f);
if (it == m_decl2args.end())
return BR_FAILED;
SASSERT(m_decl2args.contains(f));
bit_vector & bv = m_decl2args.find(f);
arg2func * map = it->m_value;
app_ref tmp(m);
tmp = m.mk_app(f, num, args);
CTRACE("reduce_args", !map->contains(tmp),
tout << "map does not contain tmp f: " << f->get_name() << "\n";
tout << mk_ismt2_pp(tmp, m) << "\n";
arg2func::iterator it = map->begin();
arg2func::iterator end = map->end();
for (; it != end; ++it) {
tout << mk_ismt2_pp(it->m_key, m) << "\n---> " << it->m_value->get_name() << "\n";
});
SASSERT(map->contains(tmp));
func_decl * new_f = map->find(tmp);
bit_vector & bv = it->m_value;
arg2func *& map = m_decl2arg2funcs.insert_if_not_there2(f, 0)->get_data().m_value;
if (!map) {
map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
}
app_ref tmp(m.mk_app(f, num, args), m);
func_decl *& new_f = map->insert_if_not_there2(tmp, 0)->get_data().m_value;
if (!new_f) {
// create fresh symbol
ptr_buffer<sort> domain;
unsigned arity = f->get_arity();
for (unsigned i = 0; i < arity; ++i) {
if (!bv.get(i))
domain.push_back(f->get_domain(i));
}
new_f = m.mk_fresh_func_decl(f->get_name(), symbol::null, domain.size(), domain.c_ptr(), f->get_range());
m.inc_ref(tmp);
m.inc_ref(new_f);
}
ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num; i++) {
if (!bv.get(i))
@ -470,7 +445,6 @@ struct reduce_args_tactic::imp {
void operator()(goal & g, model_converter_ref & mc) {
if (g.inconsistent())
return;
m_produce_models = g.models_enabled();
TRACE("reduce_args", g.display(tout););
tactic_report report("reduce-args", g);
obj_hashtable<func_decl> non_candidates;
@ -481,10 +455,7 @@ struct reduce_args_tactic::imp {
if (decl2args.empty())
return;
ptr_vector<arg2func> arg2funcs;
reduce_args_ctx ctx(m_manager);
populate_decl2arg_set(g, decl2args, ctx.m_decl2arg2funcs);
reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
unsigned sz = g.size();
@ -499,7 +470,7 @@ struct reduce_args_tactic::imp {
report_tactic_progress(":reduced-funcs", decl2args.size());
if (m_produce_models)
if (g.models_enabled())
mc = mk_mc(decl2args, ctx.m_decl2arg2funcs);
TRACE("reduce_args", g.display(tout); if (mc) mc->display(tout););

12
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -47,6 +47,7 @@ public:
: m_m(m)
, m_p(p)
, m_use_sat(false)
, m_inc_use_sat(false)
{}
virtual ~qfufbv_ackr_tactic() { }
@ -85,6 +86,7 @@ public:
void updt_params(params_ref const & _p) {
qfufbv_tactic_params p(_p);
m_use_sat = p.sat_backend();
m_inc_use_sat = p.inc_sat_backend();
}
virtual void collect_statistics(statistics & st) const {
@ -105,12 +107,18 @@ private:
params_ref m_p;
lackr_stats m_st;
bool m_use_sat;
bool m_inc_use_sat;
solver* setup_sat() {
solver * sat(NULL);
if (m_use_sat) {
tactic_ref t = mk_qfbv_tactic(m_m, m_p);
sat = mk_tactic2solver(m_m, t.get(), m_p);
if (m_inc_use_sat) {
sat = mk_inc_sat_solver(m_m, m_p);
}
else {
tactic_ref t = mk_qfbv_tactic(m_m, m_p);
sat = mk_tactic2solver(m_m, t.get(), m_p);
}
}
else {
tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);

1
src/tactic/smtlogics/qfufbv_tactic_params.pyg
View file

@ -4,5 +4,6 @@ def_module_params('ackermannization',
export=True,
params=(
('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'),
('inc_sat_backend', BOOL, False, 'use incremental SAT'),
))