mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
1ce0d7512a
commit
8ad939a10f
|
@ -1761,7 +1761,7 @@ namespace qe {
|
|||
// unless the current state is unsatisfiable.
|
||||
//
|
||||
if (m.is_true(fml_mixed)) {
|
||||
SASSERT(l_true == m_solver.check());
|
||||
SASSERT(l_false != m_solver.check());
|
||||
m_current = m_current->add_child(fml_closed);
|
||||
for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
|
||||
expr_ref val(m);
|
||||
|
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
|
||||
#include "ast/expr_abstract.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/occurs.h"
|
||||
#include "ast/rewriter/quant_hoist.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
|
@ -919,9 +920,6 @@ namespace qe {
|
|||
if (level.max() == UINT_MAX) {
|
||||
num_scopes = 2*(m_level/2);
|
||||
}
|
||||
else if (m_mode == qsat_qe_rec) {
|
||||
num_scopes = 2;
|
||||
}
|
||||
else {
|
||||
if (level.max() + 2 > m_level) return false;
|
||||
SASSERT(level.max() + 2 <= m_level);
|
||||
|
@ -1016,11 +1014,16 @@ namespace qe {
|
|||
|
||||
TRACE("qe", tout << "elim-rec " << tmp << "\n";);
|
||||
tmp = elim(vars, tmp);
|
||||
if (!tmp) {
|
||||
visited.insert(e, e);
|
||||
todo.pop_back();
|
||||
break;
|
||||
}
|
||||
if (is_fa) {
|
||||
tmp = ::push_not(tmp);
|
||||
}
|
||||
trail.push_back(tmp);
|
||||
TRACE("qe", tout << vars << ": " << tmp << "\n";);
|
||||
TRACE("qe", tout << tmp << "\n";);
|
||||
visited.insert(e, tmp);
|
||||
todo.pop_back();
|
||||
break;
|
||||
|
@ -1037,14 +1040,12 @@ namespace qe {
|
|||
/*
|
||||
* Solve ex (x) phi(x)
|
||||
*/
|
||||
expr_ref elim(app_ref_vector const& vars, expr* _fml) {
|
||||
expr_ref save(_fml, m);
|
||||
expr_ref elim(app_ref_vector& vars, expr* _fml) {
|
||||
expr_ref fml(_fml, m);
|
||||
expr_ref_vector defs(m);
|
||||
if (has_quantifiers(fml)) {
|
||||
return fml;
|
||||
return expr_ref(m);
|
||||
}
|
||||
flet<qsat_mode> _mode(m_mode, qsat_qe);
|
||||
reset();
|
||||
fml = ::mk_exists(m, vars.size(), vars.c_ptr(), fml);
|
||||
fml = ::push_not(fml);
|
||||
|
@ -1061,12 +1062,20 @@ namespace qe {
|
|||
TRACE("qe", tout << "ex: " << fml << "\n";);
|
||||
lbool is_sat = check_sat();
|
||||
|
||||
unsigned j = 0;
|
||||
switch (is_sat) {
|
||||
case l_false:
|
||||
fml = ::mk_and(m_answer);
|
||||
for (app* v : m_free_vars) {
|
||||
if (occurs(v, fml)) m_free_vars[j++] = v;
|
||||
}
|
||||
m_free_vars.shrink(j);
|
||||
if (!m_free_vars.empty()) {
|
||||
fml = ::mk_exists(m, m_free_vars.size(), m_free_vars.c_ptr(), fml);
|
||||
}
|
||||
return fml;
|
||||
default:
|
||||
return save;
|
||||
return expr_ref(m);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue