mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

fix #3004

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-17 19:37:47 -10:00
parent 1959b7c48a
commit f810f25d8d
4 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/macros/quasi_macros.cpp
View file

@ -157,10 +157,8 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
if (is_forall(e)) { if (is_forall(e)) {
quantifier * q = to_quantifier(e); quantifier * q = to_quantifier(e);
expr * qe = q->get_expr(); expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
if ((m_manager.is_eq(qe))) { if ((m_manager.is_eq(qe, lhs, rhs))) {
expr * lhs = to_app(qe)->get_arg(0);
expr * rhs = to_app(qe)->get_arg(1);
if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
!depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) { !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
@ -173,9 +171,9 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
t = lhs; t = lhs;
return true; return true;
} }
} else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) && } else if (m_manager.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
a = to_app(to_app(qe)->get_arg(0)); a = to_app(lhs);
t = m_manager.mk_false(); t = m_manager.mk_false();
return true; return true;
} else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true

2
src/muz/rel/rel_context.cpp
View file

@ -74,7 +74,7 @@ namespace datalog {
} }
~scoped_query() { ~scoped_query() {
m_ctx.reopen(); m_ctx.ensure_opened();
m_ctx.restrict_predicates(m_preds); m_ctx.restrict_predicates(m_preds);
m_ctx.replace_rules(m_rules); m_ctx.replace_rules(m_rules);
if (m_was_closed) { if (m_was_closed) {

3
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -58,7 +58,7 @@ class quasi_macros_tactic : public tactic {
deps.push_back(g->dep(i)); deps.push_back(g->dep(i));
} }
while (more) { // CMW: use repeat(...) ? do {
if (m().canceled()) if (m().canceled())
throw tactic_exception(m().limit().get_cancel_msg()); throw tactic_exception(m().limit().get_cancel_msg());
@ -70,6 +70,7 @@ class quasi_macros_tactic : public tactic {
proofs.swap(new_proofs); proofs.swap(new_proofs);
deps.swap(new_deps); deps.swap(new_deps);
} }
while (more);
g->reset(); g->reset();
for (unsigned i = 0; i < new_forms.size(); i++) for (unsigned i = 0; i < new_forms.size(); i++)