mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-02 18:16:07 -08:00
parent f736f7e83e ba79700096
commit 4028ffa995
6 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -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());
}

5
src/ackermannization/ackr_model_converter.cpp
View file

@ -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);
}

13
src/solver/tactic2solver.cpp
View file

@ -188,11 +188,14 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
}
break;
}
m_mc = concat(m_mc.get(), g->mc());
if (m_mc && md) {
(*m_mc)(md);
}
TRACE("tactic", if (m_mc) m_mc->display(tout););
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());
}
catch (z3_error & ex) {
TRACE("tactic2solver", tout << "exception: " << ex.msg() << "\n";);

1
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -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);

4
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -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());
}
};

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

@ -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);