mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fix #2974 by using same code path as qe. It now diverges, but this is due to the use of an uninterpreted predicate which the use of mbp doesn't handle

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-12 13:40:23 -10:00
parent 85fd139c7f
commit 1ce0d7512a
2 changed files with 29 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/qe/qsat.cpp
View file

@ -1013,11 +1013,14 @@ namespace qe {
if (is_fa) {
tmp = ::push_not(tmp);
}
TRACE("qe", tout << "elim-rec " << tmp << "\n";);
tmp = elim(vars, tmp);
if (is_fa) {
tmp = ::push_not(tmp);
}
trail.push_back(tmp);
TRACE("qe", tout << vars << ": " << tmp << "\n";);
visited.insert(e, tmp);
todo.pop_back();
break;
@ -1031,16 +1034,24 @@ namespace qe {
return expr_ref(e, m);
}
/*
* Solve ex (x) phi(x)
*/
expr_ref elim(app_ref_vector const& vars, expr* _fml) {
expr_ref save(_fml, m);
expr_ref fml(_fml, m);
reset();
m_vars.push_back(app_ref_vector(m));
m_vars.push_back(vars);
initialize_levels();
fml = push_not(fml);
TRACE("qe", tout << vars << " " << fml << "\n";);
expr_ref_vector defs(m);
if (has_quantifiers(fml)) {
return fml;
}
flet<qsat_mode> _mode(m_mode, qsat_qe);
reset();
fml = ::mk_exists(m, vars.size(), vars.c_ptr(), fml);
fml = ::push_not(fml);
hoist(fml);
if (!is_ground(fml)) {
throw tactic_exception("formula is not hoistable");
}
m_pred_abs.abstract_atoms(fml, defs);
fml = m_pred_abs.mk_abstract(fml);
m_ex.assert_expr(mk_and(defs));
@ -1049,27 +1060,13 @@ namespace qe {
m_fa.assert_expr(m.mk_not(fml));
TRACE("qe", tout << "ex: " << fml << "\n";);
lbool is_sat = check_sat();
fml = ::mk_and(m_answer);
TRACE("qe", tout << "ans: " << fml << "\n";
tout << "Free vars: " << m_free_vars << "\n";);
if (is_sat == l_false) {
obj_hashtable<app> vars;
for (unsigned i = 0; i < m_free_vars.size(); ++i) {
app* v = m_free_vars[i].get();
if (vars.contains(v)) {
m_free_vars[i] = m_free_vars.back();
m_free_vars.pop_back();
--i;
}
else {
vars.insert(v);
}
}
fml = mk_exists(m, m_free_vars.size(), m_free_vars.c_ptr(), fml);
switch (is_sat) {
case l_false:
fml = ::mk_and(m_answer);
return fml;
}
else {
return expr_ref(_fml, m);
default:
return save;
}
}
@ -1223,7 +1220,6 @@ namespace qe {
void collect_param_descrs(param_descrs & r) override {
}
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result) override {

7
src/sat/sat_aig_cuts.cpp
View file

@ -43,11 +43,11 @@ namespace sat {
if (m_aig[id].empty()) {
continue;
}
IF_VERBOSE(10, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "augment " << id << "\nbefore\n"));
for (node const& n : m_aig[id]) {
augment(id, n);
}
IF_VERBOSE(10, m_cuts[id].display(verbose_stream() << "after\n"));
IF_VERBOSE(20, m_cuts[id].display(verbose_stream() << "after\n"));
}
}
@ -432,6 +432,9 @@ namespace sat {
if (eq(n, n2)) return false;
else if (n.size() < n2.size()) num_gt++;
else if (n.size() == n2.size()) num_eq++;
// avoid inserting LUTs that are likely to collide
if (n.is_lut() && !n2.is_lut() && n.size() == n2.size())
return false;
}
if (m_aig[v].size() < m_config.m_max_aux) {
on_node_add(v, n);