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

fix mc efficiency issues

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-22 08:55:21 -08:00
parent 107bfb1438
commit 8230cbef4c
4 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -61,6 +61,7 @@ class inc_sat_solver : public solver {
model_converter_ref m_mc;
model_converter_ref m_mc0;
model_converter_ref m_sat_mc;
mutable model_converter_ref m_cached_mc;
svector<double> m_weights;
std::string m_unknown;
// access formulas after they have been pre-processed and handled by the sat solver.
@ -435,10 +436,12 @@ public:
virtual model_converter_ref get_model_converter() const {
const_cast<inc_sat_solver*>(this)->convert_internalized();
if (m_internalized && m_internalized_converted) {
model_converter_ref mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
mc = concat(solver::get_model_converter().get(), mc.get());
mc = concat(mc.get(), m_sat_mc.get());
return mc;
if (m_cached_mc)
return m_cached_mc;
m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
return m_cached_mc;
}
else {
return solver::get_model_converter();
@ -449,6 +452,7 @@ public:
if (!m_internalized || m_internalized_converted) return;
sat2goal s2g;
m_sat_mc = nullptr;
m_cached_mc = nullptr;
goal g(m, false, true, false);
s2g(m_solver, m_map, m_params, g, m_sat_mc);
m_internalized_fmls.reset();

1
src/sat/tactic/goal2sat.cpp
View file

@ -1030,6 +1030,7 @@ struct sat2goal::imp {
void operator()(expr_ref& formula) override {
if (!m_imc) {
std::cout << "create generic\n";
m_imc = alloc(generic_model_converter, m());
sat::literal_vector updates;
m_mc.expand(updates);

4
src/solver/solver.cpp
View file

@ -40,7 +40,7 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum
expr_ref_vector fmls(get_manager());
stopwatch sw;
sw.start();
get_assertions(fmls);
get_assertions(fmls);
ast_pp_util visitor(get_manager());
model_converter_ref mc = get_model_converter();
mc = concat(mc0(), mc.get());
@ -194,7 +194,7 @@ void solver::assert_expr(expr* f, expr* t) {
mc = concat(mc0(), mc.get());
if (mc) {
(*mc)(fml);
// (*mc0())(a);
// (*mc)(a);
}
assert_expr_core(fml, a);
}

1
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -134,6 +134,7 @@ public:
private:
void flush_assertions() const {
if (m_assertions.empty()) return;
m_rewriter.updt_params(get_params());
proof_ref proof(m);
expr_ref fml1(m), fml(m);