mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

refine test for non-fd to be more inclusive while addressing #1092

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-21 08:01:03 -07:00
parent a3ee785923
commit b516f22549
2 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include "var_subst.h"
#include "ast_util.h"
#include "enum2bv_rewriter.h"
#include "ast_pp.h"
class dt2bv_tactic : public tactic {
@ -53,36 +54,38 @@ class dt2bv_tactic : public tactic {
void operator()(app* a) {
if (m.is_eq(a)) {
return;
// no-op
}
if (m.is_distinct(a)) {
return;
else if (m.is_distinct(a)) {
// no-op
}
if (m_t.m_dt.is_recognizer(a->get_decl()) &&
else if (m_t.m_dt.is_recognizer(a->get_decl()) &&
m_t.is_fd(a->get_arg(0))) {
m_t.m_fd_sorts.insert(get_sort(a->get_arg(0)));
return;
}
if (m_t.is_fd(a) && a->get_num_args() > 0) {
else if (m_t.is_fd(a) && a->get_num_args() > 0) {
m_t.m_non_fd_sorts.insert(get_sort(a));
args_cannot_be_fd(a);
}
else if (m_t.is_fd(a)) {
m_t.m_fd_sorts.insert(get_sort(a));
}
else {
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
if (m_t.is_fd(a->get_arg(i))) {
m_t.m_non_fd_sorts.insert(get_sort(a->get_arg(i)));
}
}
args_cannot_be_fd(a);
}
}
void args_cannot_be_fd(app* a) {
for (expr* arg : *a) {
if (m_t.is_fd(arg)) {
m_t.m_non_fd_sorts.insert(get_sort(arg));
}
}
}
void operator()(var * v) {
if (m_t.is_fd(v)) {
m_t.m_non_fd_sorts.insert(get_sort(v));
m_t.m_fd_sorts.insert(get_sort(v));
}
}