mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c4d168205a
commit
8b720a0d66
|
@ -35,7 +35,7 @@ public:
|
|||
tactic_report report("ackermannize_bv", *g);
|
||||
fail_if_unsat_core_generation("ackermannize", g);
|
||||
fail_if_proof_generation("ackermannize", g);
|
||||
TRACE("ackermannize", g->display(tout << "in\n"););
|
||||
TRACE("goal", g->display(tout << "in\n"););
|
||||
|
||||
ptr_vector<expr> flas;
|
||||
const unsigned sz = g->size();
|
||||
|
@ -58,7 +58,7 @@ public:
|
|||
}
|
||||
|
||||
resg->inc_depth();
|
||||
TRACE("ackermannize", resg->display(tout << "out\n"););
|
||||
TRACE("goal", resg->display(tout << "out\n"););
|
||||
SASSERT(resg->is_well_sorted());
|
||||
}
|
||||
|
||||
|
|
|
@ -30,7 +30,8 @@ public:
|
|||
info(info),
|
||||
abstr_model(abstr_model),
|
||||
fixed_model(true)
|
||||
{ }
|
||||
{
|
||||
}
|
||||
|
||||
ackr_model_converter(ast_manager & m,
|
||||
const ackr_info_ref& info)
|
||||
|
@ -44,6 +45,7 @@ public:
|
|||
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
|
||||
|
||||
void operator()(model_ref & md) override {
|
||||
TRACE("ackermannize", tout << (fixed_model? "fixed" : "nonfixed") << "\n";);
|
||||
SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
|
||||
model_ref& old_model = fixed_model ? abstr_model : md;
|
||||
SASSERT(old_model.get());
|
||||
|
@ -100,6 +102,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
|
|||
func_decl * const c = source->get_constant(i);
|
||||
app * const term = info->find_term(c);
|
||||
expr * value = source->get_const_interp(c);
|
||||
TRACE("ackermannize", tout << mk_ismt2_pp(c, m) << " " << term << "\n";);
|
||||
if (!term) {
|
||||
destination->register_decl(c, value);
|
||||
}
|
||||
|
|
|
@ -189,10 +189,17 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
|
|||
break;
|
||||
}
|
||||
if (m_mc && md) {
|
||||
(*m_mc)(md);
|
||||
// (*m_mc)(md);
|
||||
|
||||
}
|
||||
TRACE("tactic",
|
||||
if (m_mc) m_mc->display(tout << "mc:");
|
||||
if (g->mc()) g->mc()->display(tout << "g:");
|
||||
if (md) tout << *md.get() << "\n";
|
||||
);
|
||||
|
||||
m_mc = concat(g->mc(), m_mc.get());
|
||||
TRACE("tactic", if (m_mc) m_mc->display(tout););
|
||||
|
||||
}
|
||||
catch (z3_error & ex) {
|
||||
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);
|
||||
|
|
|
@ -375,6 +375,7 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
|
|||
SASSERT(g->is_well_sorted());
|
||||
fail_if_proof_generation("bv-size-reduction", g);
|
||||
fail_if_unsat_core_generation("bv-size-reduction", g);
|
||||
TRACE("goal", g->display(tout););
|
||||
result.reset();
|
||||
model_converter_ref mc;
|
||||
run(*(g.get()), mc);
|
||||
|
|
|
@ -779,7 +779,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
void run(goal_ref const & g, goal_ref_buffer & result) {
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
|
||||
TRACE("elim_uncnstr_bug", g->display(tout););
|
||||
TRACE("goal", g->display(tout););
|
||||
tactic_report report("elim-uncnstr", *g);
|
||||
m_vars.reset();
|
||||
collect_occs p;
|
||||
|
@ -826,7 +826,7 @@ class elim_uncnstr_tactic : public tactic {
|
|||
m_rw = nullptr;
|
||||
result.push_back(g.get());
|
||||
g->inc_depth();
|
||||
TRACE("elim_uncnstr_bug", g->display(tout););
|
||||
TRACE("goal", g->display(tout););
|
||||
return;
|
||||
}
|
||||
modified = false;
|
||||
|
|
|
@ -1007,7 +1007,7 @@ class solve_eqs_tactic : public tactic {
|
|||
SASSERT(g->is_well_sorted());
|
||||
model_converter_ref mc;
|
||||
tactic_report report("solve_eqs", *g);
|
||||
TRACE("solve_eqs", g->display(tout););
|
||||
TRACE("goal", g->display(tout););
|
||||
m_produce_models = g->models_enabled();
|
||||
m_produce_proofs = g->proofs_enabled();
|
||||
m_produce_unsat_cores = g->unsat_core_enabled();
|
||||
|
@ -1043,7 +1043,7 @@ class solve_eqs_tactic : public tactic {
|
|||
g->inc_depth();
|
||||
g->add(mc.get());
|
||||
result.push_back(g.get());
|
||||
TRACE("solve_eqs", g->display(tout););
|
||||
TRACE("goal", g->display(tout););
|
||||
SASSERT(g->is_well_sorted());
|
||||
}
|
||||
};
|
||||
|
|
|
@ -337,6 +337,9 @@ void goal::display(ast_printer & prn, std::ostream & out) const {
|
|||
prn.display(out, form(i), 2);
|
||||
}
|
||||
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
|
||||
if (m_mc) {
|
||||
m_mc->display(out);
|
||||
}
|
||||
}
|
||||
|
||||
void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) const {
|
||||
|
@ -370,6 +373,9 @@ void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) cons
|
|||
out << ")";
|
||||
}
|
||||
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
|
||||
if (m_mc) {
|
||||
m_mc->display(out);
|
||||
}
|
||||
}
|
||||
|
||||
void goal::display_with_dependencies(std::ostream & out) const {
|
||||
|
@ -391,6 +397,9 @@ void goal::display_with_dependencies(std::ostream & out) const {
|
|||
out << "\n " << mk_ismt2_pp(form(i), m(), 2);
|
||||
}
|
||||
out << "\n :precision " << prec() << " :depth " << depth() << ")" << std::endl;
|
||||
if (m_mc) {
|
||||
m_mc->display(out);
|
||||
}
|
||||
}
|
||||
|
||||
void goal::display(ast_printer_context & ctx) const {
|
||||
|
@ -409,6 +418,9 @@ void goal::display(std::ostream & out) const {
|
|||
out << mk_ismt2_pp(form(i), m(), 2);
|
||||
}
|
||||
out << ")" << std::endl;
|
||||
if (m_mc) {
|
||||
m_mc->display(out);
|
||||
}
|
||||
}
|
||||
|
||||
void goal::display_as_and(std::ostream & out) const {
|
||||
|
|
|
@ -59,7 +59,7 @@ public:
|
|||
fail_if_unsat_core_generation("qfufbv_ackr", g);
|
||||
fail_if_proof_generation("qfufbv_ackr", g);
|
||||
|
||||
TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
|
||||
TRACE("goal", g->display(tout););
|
||||
// running implementation
|
||||
ptr_vector<expr> flas;
|
||||
const unsigned sz = g->size();
|
||||
|
@ -106,7 +106,7 @@ private:
|
|||
bool m_inc_use_sat;
|
||||
|
||||
solver* setup_sat() {
|
||||
solver * sat(nullptr);
|
||||
solver * sat = nullptr;
|
||||
if (m_use_sat) {
|
||||
if (m_inc_use_sat) {
|
||||
sat = mk_inc_sat_solver(m_m, m_p);
|
||||
|
|
Loading…
Reference in a new issue