mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

disable macro finder tactic if there are recursive functions fix #5574

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-29 09:33:46 -07:00
parent 137e5c5263
commit 62fd22f555
3 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/array_model.cpp
View file

@ -120,7 +120,6 @@ namespace array {
bool solver::must_have_different_model_values(theory_var v1, theory_var v2) { bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
euf::enode* else1 = nullptr, * else2 = nullptr; euf::enode* else1 = nullptr, * else2 = nullptr;
euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2); euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
euf::enode* r1 = n1->get_root(), * r2 = n2->get_root();
expr* e1 = n1->get_expr(); expr* e1 = n1->get_expr();
if (!a.is_array(e1)) if (!a.is_array(e1))
return true; return true;

1
src/sat/smt/q_mam.cpp
View file

@ -2070,7 +2070,6 @@ namespace q {
enode * n = m_registers[j2->m_reg]->get_root(); enode * n = m_registers[j2->m_reg]->get_root();
if (n->num_parents() == 0) if (n->num_parents() == 0)
return nullptr; return nullptr;
unsigned num_args = n->num_args();
enode_vector * v = mk_enode_vector(); enode_vector * v = mk_enode_vector();
for (enode* p : euf::enode_parents(n)) { for (enode* p : euf::enode_parents(n)) {
if (p->get_decl() == j2->m_decl && if (p->get_decl() == j2->m_decl &&

7
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/ --*/
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/macros/macro_manager.h" #include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h" #include "ast/macros/macro_finder.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
@ -42,6 +43,12 @@ class macro_finder_tactic : public tactic {
tactic_report report("macro-finder", *g); tactic_report report("macro-finder", *g);
TRACE("macro-finder", g->display(tout);); TRACE("macro-finder", g->display(tout););
recfun::util rec(m());
if (!rec.get_rec_funs().empty()) {
result.push_back(g.get());
return;
}
bool produce_proofs = g->proofs_enabled(); bool produce_proofs = g->proofs_enabled();
bool unsat_core_enabled = g->unsat_core_enabled(); bool unsat_core_enabled = g->unsat_core_enabled();
macro_manager mm(m_manager); macro_manager mm(m_manager);