mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

disable buggy clausification in ba_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-15 17:20:19 -08:00
parent 3047d930e1
commit ae728374c8
3 changed files with 25 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/ba_solver.cpp
View file

@ -2649,6 +2649,7 @@ namespace sat {
} }
bool ba_solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) { bool ba_solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) {
return false;
bool is_def = lit != null_literal; bool is_def = lit != null_literal;
if ((!is_def || !s().was_eliminated(lit)) && if ((!is_def || !s().was_eliminated(lit)) &&
!std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) { !std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) {
@ -2667,6 +2668,7 @@ namespace sat {
} }
bool ba_solver::clausify(card& c) { bool ba_solver::clausify(card& c) {
return false;
if (get_config().m_card_solver) if (get_config().m_card_solver)
return false; return false;

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

@ -60,7 +60,8 @@ class inc_sat_solver : public solver {
goal_ref_buffer m_subgoals; goal_ref_buffer m_subgoals;
proof_converter_ref m_pc; proof_converter_ref m_pc;
model_converter_ref m_mc; model_converter_ref m_mc;
model_converter_ref m_mc0; mutable model_converter_ref m_mc0;
mutable obj_hashtable<func_decl> m_inserted_const2bits;
ref<sat2goal::mc> m_sat_mc; ref<sat2goal::mc> m_sat_mc;
mutable model_converter_ref m_cached_mc; mutable model_converter_ref m_cached_mc;
svector<double> m_weights; svector<double> m_weights;
@ -227,6 +228,7 @@ public:
n = m_num_scopes; // take over for another solver. n = m_num_scopes; // take over for another solver.
} }
if (m_bb_rewriter) m_bb_rewriter->pop(n); if (m_bb_rewriter) m_bb_rewriter->pop(n);
m_inserted_const2bits.reset();
m_map.pop(n); m_map.pop(n);
SASSERT(n <= m_num_scopes); SASSERT(n <= m_num_scopes);
m_solver.user_pop(n); m_solver.user_pop(n);
@ -443,7 +445,8 @@ public:
if (m_cached_mc) if (m_cached_mc)
return m_cached_mc; return m_cached_mc;
if (is_internalized() && m_internalized_converted) { if (is_internalized() && m_internalized_converted) {
m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits())); insert_const2bits();
m_cached_mc = m_mc0.get();
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get()); 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()); m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
return m_cached_mc; return m_cached_mc;
@ -500,6 +503,21 @@ public:
private: private:
void insert_const2bits() const {
if (!m_bb_rewriter) return;
obj_map<func_decl, expr*> to_insert;
obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
for (auto const& kv : const2bits) {
if (!m_inserted_const2bits.contains(kv.m_key)) {
m_inserted_const2bits.insert(kv.m_key);
to_insert.insert(kv.m_key, kv.m_value);
}
}
if (!to_insert.empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, to_insert));
}
}
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) { lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
m_mc.reset(); m_mc.reset();
@ -790,9 +808,7 @@ private:
if (m_sat_mc) { if (m_sat_mc) {
(*m_sat_mc)(m_model); (*m_sat_mc)(m_model);
} }
if (m_bb_rewriter.get() && !m_bb_rewriter->const2bits().empty()) { insert_const2bits();
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
}
if (m_mc0) { if (m_mc0) {
(*m_mc0)(m_model); (*m_mc0)(m_model);
} }

2
src/solver/solver.cpp
View file

@ -193,6 +193,8 @@ void solver::assert_expr(expr* f, expr* t) {
expr_ref fml(f, m); expr_ref fml(f, m);
expr_ref a(t, m); expr_ref a(t, m);
if (m_enforce_model_conversion) { if (m_enforce_model_conversion) {
IF_VERBOSE(0, verbose_stream() << "enforce model conversion\n";);
exit(0);
model_converter_ref mc = get_model_converter(); model_converter_ref mc = get_model_converter();
mc = concat(mc0(), mc.get()); mc = concat(mc0(), mc.get());
if (mc) { if (mc) {