mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Improve distinct constraint generation

Browse source 
still many more optimizations possible
This commit is contained in:
Arie Gurfinkel 2018-06-14 22:27:57 -07:00
parent baa96909cc
commit f936c92efc
2 changed files with 23 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/qe/qe_mbi.cpp
View file

@ -315,10 +315,10 @@ namespace qe {
}
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) {
arith_util a(m);
app_ref_vector avars(m);
is_arith_var_proc _proc(avars, m_shared);
for_each_expr(_proc, lits);
arith_util a(m);
app_ref_vector avars(m);
is_arith_var_proc _proc(avars, m_shared);
for_each_expr(_proc, lits);
return avars;
}
@ -358,8 +358,8 @@ namespace qe {
tg.set_vars(m_shared, false);
tg.add_lits(lits);
lits.reset();
//lits.append(tg.project(*mdl));
lits.append(tg.project());
lits.append(tg.project(*mdl));
//lits.append(tg.project());
TRACE("qe", tout << "project: " << lits << "\n";);
return mbi_sat;
}

18
src/qe/qe_term_graph.cpp
View file

@ -28,6 +28,16 @@ Notes:
namespace qe {
static expr_ref mk_neq(ast_manager &m, expr *e1, expr *e2) {
expr *t = nullptr;
// x != !x == true
if ((m.is_not(e1, t) && t == e2) || (m.is_not(e2, t) && t == e1))
return expr_ref(m.mk_true(), m);
else if (m.are_distinct(e1, e2))
return expr_ref(m.mk_true(), m);
return expr_ref(m.mk_not(m.mk_eq(e1, e2)), m);
}
namespace {
struct sort_lt_proc {
bool operator()(const expr* a, const expr *b) const {
@ -791,10 +801,16 @@ namespace qe {
sort* last_sort = get_sort(reps.get(i));
unsigned j = i + 1;
while (j < sz && last_sort == get_sort(reps.get(j))) {++j;}
if (j - i > 1)
if (j - i == 2) {
expr_ref d(m);
d = mk_neq(m, reps.get(i), reps.get(i+1));
if (!m.is_true(d)) res.push_back(d);
}
else if (j - i > 2)
res.push_back(m.mk_distinct(j - i, reps.c_ptr() + i));
i = j;
}
TRACE("qe", tout << "after distinct: " << res << "\n";);
}
public: