mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

extra flags to control quant_hoist

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 14:13:08 -04:00
parent be1df279ec
commit 15451ae858
2 changed files with 50 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

80
src/ast/rewriter/quant_hoist.cpp
View file

@ -41,9 +41,9 @@ public:
m_rewriter(m) m_rewriter(m)
{} {}
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = Q_none_pos; quantifier_type qt = Q_none_pos;
pull_quantifier(fml, qt, vars, result); pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose", TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n"; tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";); tout << mk_pp(result, m) << "\n";);
@ -51,36 +51,38 @@ public:
is_fa = (Q_forall_pos == qt); is_fa = (Q_forall_pos == qt);
} }
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = Q_exists_pos; quantifier_type qt = Q_exists_pos;
pull_quantifier(fml, qt, vars, result); pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose", TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n"; tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";); tout << mk_pp(result, m) << "\n";);
} }
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos; quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
expr_ref result(m); expr_ref result(m);
pull_quantifier(fml, qt, vars, result); pull_quantifier(fml, qt, vars, result, use_fresh, rewrite_ok);
TRACE("qe_verbose", TRACE("qe_verbose",
tout << mk_pp(fml, m) << "\n"; tout << mk_pp(fml, m) << "\n";
tout << mk_pp(result, m) << "\n";); tout << mk_pp(result, m) << "\n";);
fml = result; fml = result;
} }
void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result) { void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) {
unsigned nd = q->get_num_decls(); unsigned nd = q->get_num_decls();
for (unsigned i = 0; i < nd; ++i) { for (unsigned i = 0; i < nd; ++i) {
sort* s = q->get_decl_sort(i); sort* s = q->get_decl_sort(i);
app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s); symbol const& sym = q->get_decl_name (i);
app* a = use_fresh ? m.mk_fresh_const(sym.str ().c_str (), s)
: m.mk_const (sym, s);
vars.push_back(a); vars.push_back(a);
} }
expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd); expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
instantiate(m, q, exprs, result); instantiate(m, q, exprs, result);
} }
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) { unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
unsigned index = var_counter().get_next_var(fml); unsigned index = var_counter().get_next_var(fml);
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) { while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
quantifier* q = to_quantifier(fml); quantifier* q = to_quantifier(fml);
@ -97,7 +99,7 @@ public:
return index; return index;
} }
app_ref_vector vars(m); app_ref_vector vars(m);
pull_quantifier(is_forall, fml, vars); pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
if (vars.empty()) { if (vars.empty()) {
return index; return index;
} }
@ -192,7 +194,7 @@ private:
} }
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) { void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
if (!has_quantifiers(fml)) { if (!has_quantifiers(fml)) {
result = fml; result = fml;
@ -209,38 +211,48 @@ private:
if (m.is_and(fml)) { if (m.is_and(fml)) {
num_args = a->get_num_args(); num_args = a->get_num_args();
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
pull_quantifier(a->get_arg(i), qt, vars, tmp); pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
args.push_back(tmp); args.push_back(tmp);
} }
if (rewrite_ok) {
m_rewriter.mk_and(args.size(), args.c_ptr(), result); m_rewriter.mk_and(args.size(), args.c_ptr(), result);
}
else {
result = m.mk_and (args.size (), args.c_ptr ());
}
} }
else if (m.is_or(fml)) { else if (m.is_or(fml)) {
num_args = to_app(fml)->get_num_args(); num_args = to_app(fml)->get_num_args();
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp); pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
args.push_back(tmp); args.push_back(tmp);
} }
if (rewrite_ok) {
m_rewriter.mk_or(args.size(), args.c_ptr(), result); m_rewriter.mk_or(args.size(), args.c_ptr(), result);
}
else {
result = m.mk_or (args.size (), args.c_ptr ());
}
} }
else if (m.is_not(fml)) { else if (m.is_not(fml)) {
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp); pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok);
negate(qt); negate(qt);
result = m.mk_not(tmp); result = m.mk_not(tmp);
} }
else if (m.is_implies(fml, t1, t2)) { else if (m.is_implies(fml, t1, t2)) {
pull_quantifier(t1, negate(qt), vars, tmp); pull_quantifier(t1, negate(qt), vars, tmp, use_fresh, rewrite_ok);
negate(qt); negate(qt);
pull_quantifier(t2, qt, vars, result); pull_quantifier(t2, qt, vars, result, use_fresh, rewrite_ok);
result = m.mk_implies(tmp, result); result = m.mk_implies(tmp, result);
} }
else if (m.is_ite(fml, t1, t2, t3)) { else if (m.is_ite(fml, t1, t2, t3)) {
expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m); expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
pull_quantifier(t2, qt, vars, tt2); pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
pull_quantifier(t3, qt, vars, tt3); pull_quantifier(t3, qt, vars, tt3, use_fresh, rewrite_ok);
if (has_quantifiers(t1)) { if (has_quantifiers(t1)) {
pull_quantifier(t1, qt, vars, tt1); pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
nt1 = m.mk_not(t1); nt1 = m.mk_not(t1);
pull_quantifier(nt1, qt, vars, ntt1); pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3)); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
} }
else { else {
@ -249,12 +261,12 @@ private:
} }
else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) { else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m); expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
pull_quantifier(t1, qt, vars, tt1); pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
pull_quantifier(t2, qt, vars, tt2); pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);
nt1 = m.mk_not(t1); nt1 = m.mk_not(t1);
nt2 = m.mk_not(t2); nt2 = m.mk_not(t2);
pull_quantifier(nt1, qt, vars, ntt1); pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok);
pull_quantifier(nt2, qt, vars, ntt2); pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok);
result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1)); result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
} }
else { else {
@ -271,8 +283,8 @@ private:
break; break;
} }
set_quantifier_type(qt, q->is_forall()); set_quantifier_type(qt, q->is_forall());
extract_quantifier(q, vars, tmp); extract_quantifier(q, vars, tmp, use_fresh);
pull_quantifier(tmp, qt, vars, result); pull_quantifier(tmp, qt, vars, result, use_fresh, rewrite_ok);
break; break;
} }
case AST_VAR: case AST_VAR:
@ -295,18 +307,18 @@ quantifier_hoister::~quantifier_hoister() {
dealloc(m_impl); dealloc(m_impl);
} }
void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) { void quantifier_hoister::operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh, bool rewrite_ok) {
(*m_impl)(fml, vars, is_fa, result); (*m_impl)(fml, vars, is_fa, result, use_fresh, rewrite_ok);
} }
void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) { void quantifier_hoister::pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh, bool rewrite_ok) {
m_impl->pull_exists(fml, vars, result); m_impl->pull_exists(fml, vars, result, use_fresh, rewrite_ok);
} }
void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) { void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh, bool rewrite_ok) {
m_impl->pull_quantifier(is_forall, fml, vars); m_impl->pull_quantifier(is_forall, fml, vars, use_fresh, rewrite_ok);
} }
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) { unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh, bool rewrite_ok) {
return m_impl->pull_quantifier(is_forall, fml, sorts, names); return m_impl->pull_quantifier(is_forall, fml, sorts, names, use_fresh, rewrite_ok);
} }

8
src/ast/rewriter/quant_hoist.h
View file

@ -43,14 +43,14 @@ public:
or, and, implies, ite (then and else branch only). or, and, implies, ite (then and else branch only).
*/ */
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result); void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/** /**
\brief Pull top-most existential quantifier up. \brief Pull top-most existential quantifier up.
The list of variables is empty if there are no top-level existential quantifier. The list of variables is empty if there are no top-level existential quantifier.
*/ */
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result); void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/** /**
@ -58,7 +58,7 @@ public:
The list of variables is empty if there are no top-level universal/existential quantifier. The list of variables is empty if there are no top-level universal/existential quantifier.
*/ */
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars); void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true);
/** /**
\brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up. \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
@ -66,7 +66,7 @@ public:
Return index of maximal variable. Return index of maximal variable.
*/ */
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names); unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true);
}; };