mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-27 13:35:53 -07:00
parent 24fc19ed58
commit 41deae52c6
3 changed files with 4 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -126,7 +126,7 @@ struct enum2bv_rewriter::imp {
unsigned nc = m_dt.get_datatype_num_constructors(s);
result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size));
f_fresh = to_app(result)->get_decl();
if (!is_power_of_two(nc)) {
if (!is_power_of_two(nc) || nc == 1) {
m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
}
expr_ref f_def(m);
@ -168,7 +168,7 @@ struct enum2bv_rewriter::imp {
unsigned bv_size = get_bv_size(s);
m_sorts.push_back(m_bv.mk_sort(bv_size));
unsigned nc = m_dt.get_datatype_num_constructors(s);
if (!is_power_of_two(nc)) {
if (!is_power_of_two(nc) || nc == 1) {
bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
}
found = true;

4
src/smt/smt_context.cpp
View file

@ -1111,8 +1111,8 @@ namespace smt {
if (r1 == r2) {
TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
return true;
// return false; // context is inconsistent
theory_id t1 = r1->m_th_var_list.get_th_id();
return get_theory(t1)->use_diseqs();
}
// Propagate disequalities to theories

25
src/util/sorting_network.h
View file

@ -251,15 +251,6 @@ Notes:
return result;
}
#if 0
literal mk_and(literal_vector const& lits) {
if (lits.size() == 1) {
return lits[0];
}
}
#endif
void mk_implies_or(literal l, unsigned n, literal const* xs) {
literal_vector lits(n, xs);
lits.push_back(ctx.mk_not(l));
@ -346,28 +337,12 @@ Notes:
ors.push_back(ex);
// result => xs[0] + ... + xs[n-1] <= 1
#if 1
for (unsigned i = 0; i < n; ++i) {
for (unsigned j = i + 1; j < n; ++j) {
add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
}
}
#else
literal_vector atm;
for (unsigned i = 0; i < n; ++i) {
// at => !xs[1] & .. & !xs[i-1] & !xs[i+1] & ... & !xs[n-1]
literal at = fresh();
for (unsigned j = 0; j < n; ++j) {
if (i != j) {
add_clause(ctx.mk_not(at), ctx.mk_not(xs[j]));
}
}
atm.push_back(at);
}
atm.push_back(ctx.mk_not(result));
add_clause(atm);
#endif
// xs[0] + ... + xs[n-1] <= 1 => and_x
if (full) {
literal and_i = fresh();