mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 22:57:51 +00:00
Code Activity

control recursion depth for check function

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-27 14:29:53 -07:00
parent 5fe4d88d43
commit 17c6e0729b
2 changed files with 29 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/smt/smt_checker.cpp
View file

@ -22,23 +22,25 @@ Revision History:
namespace smt { namespace smt {
bool checker::all_args(app * a, bool is_true) { bool checker::all_args(app *a, unsigned depth, bool is_true) {
for (expr* arg : *a) { for (expr* arg : *a) {
if (!check(arg, is_true)) if (!check(arg, depth + 1, is_true))
return false; return false;
} }
return true; return true;
} }
bool checker::any_arg(app * a, bool is_true) { bool checker::any_arg(app *a, unsigned depth, bool is_true) {
for (expr* arg : *a) { for (expr* arg : *a) {
if (check(arg, is_true)) if (check(arg, depth + 1, is_true))
return true; return true;
} }
return false; return false;
} }
bool checker::check_core(expr * n, bool is_true) { bool checker::check_core(expr *n, unsigned depth, bool is_true) {
if (depth > 600)
return false;
SASSERT(m_manager.is_bool(n)); SASSERT(m_manager.is_bool(n));
if (m_context.b_internalized(n) && m_context.is_relevant(n)) { if (m_context.b_internalized(n) && m_context.is_relevant(n)) {
lbool val = m_context.get_assignment(n); lbool val = m_context.get_assignment(n);
@ -54,11 +56,11 @@ namespace smt {
case OP_FALSE: case OP_FALSE:
return !is_true; return !is_true;
case OP_NOT: case OP_NOT:
return check(a->get_arg(0), !is_true); return check(a->get_arg(0), depth + 1, !is_true);
case OP_OR: case OP_OR:
return is_true ? any_arg(a, true) : all_args(a, false); return is_true ? any_arg(a, depth, true) : all_args(a, depth, false);
case OP_AND: case OP_AND:
return is_true ? all_args(a, true) : any_arg(a, false); return is_true ? all_args(a, depth, true) : any_arg(a, depth, false);
case OP_EQ: case OP_EQ:
if (!m_manager.is_iff(a)) { if (!m_manager.is_iff(a)) {
enode * lhs = get_enode_eq_to(a->get_arg(0)); enode * lhs = get_enode_eq_to(a->get_arg(0));
@ -74,27 +76,27 @@ namespace smt {
} }
else if (is_true) { else if (is_true) {
return return
(check(a->get_arg(0), true) && (check(a->get_arg(0), depth + 1, true) &&
check(a->get_arg(1), true)) || check(a->get_arg(1), depth + 1, true)) ||
(check(a->get_arg(0), false) && (check(a->get_arg(0), depth + 1, false) &&
check(a->get_arg(1), false)); check(a->get_arg(1), depth + 1, false));
} }
else { else {
return return
(check(a->get_arg(0), true) && (check(a->get_arg(0), depth + 1, true) &&
check(a->get_arg(1), false)) || check(a->get_arg(1), depth + 1, false)) ||
(check(a->get_arg(0), false) && (check(a->get_arg(0), depth + 1, false) &&
check(a->get_arg(1), true)); check(a->get_arg(1), depth + 1, true));
} }
case OP_ITE: { case OP_ITE: {
if (m_context.lit_internalized(a->get_arg(0)) && m_context.is_relevant(a->get_arg(0))) { if (m_context.lit_internalized(a->get_arg(0)) && m_context.is_relevant(a->get_arg(0))) {
switch (m_context.get_assignment(a->get_arg(0))) { switch (m_context.get_assignment(a->get_arg(0))) {
case l_false: return check(a->get_arg(2), is_true); case l_false: return check(a->get_arg(2), depth + 1, is_true);
case l_undef: return false; case l_undef: return false;
case l_true: return check(a->get_arg(1), is_true); case l_true: return check(a->get_arg(1), depth + 1, is_true);
} }
} }
return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true); return check(a->get_arg(1), depth + 1, is_true) && check(a->get_arg(2), depth + 1, is_true);
} }
default: default:
break; break;
@ -108,11 +110,11 @@ namespace smt {
return false; return false;
} }
bool checker::check(expr * n, bool is_true) { bool checker::check(expr *n, unsigned depth, bool is_true) {
bool r; bool r;
if (n->get_ref_count() > 1 && m_is_true_cache[is_true].find(n, r)) if (n->get_ref_count() > 1 && m_is_true_cache[is_true].find(n, r))
return r; return r;
r = check_core(n, is_true); r = check_core(n, depth, is_true);
if (n->get_ref_count() > 1) if (n->get_ref_count() > 1)
m_is_true_cache[is_true].insert(n, r); m_is_true_cache[is_true].insert(n, r);
return r; return r;
@ -156,7 +158,7 @@ namespace smt {
bool checker::is_sat(expr * n, unsigned num_bindings, enode * const * bindings) { bool checker::is_sat(expr * n, unsigned num_bindings, enode * const * bindings) {
flet<unsigned> l1(m_num_bindings, num_bindings); flet<unsigned> l1(m_num_bindings, num_bindings);
flet<enode * const *> l2(m_bindings, bindings); flet<enode * const *> l2(m_bindings, bindings);
bool r = check(n, true); bool r = check(n, 0, true);
m_is_true_cache[0].reset(); m_is_true_cache[0].reset();
m_is_true_cache[1].reset(); m_is_true_cache[1].reset();
m_to_enode_cache.reset(); m_to_enode_cache.reset();
@ -166,7 +168,7 @@ namespace smt {
bool checker::is_unsat(expr * n, unsigned num_bindings, enode * const * bindings) { bool checker::is_unsat(expr * n, unsigned num_bindings, enode * const * bindings) {
flet<unsigned> l1(m_num_bindings, num_bindings); flet<unsigned> l1(m_num_bindings, num_bindings);
flet<enode * const *> l2(m_bindings, bindings); flet<enode * const *> l2(m_bindings, bindings);
bool r = check(n, false); bool r = check(n, 0,false);
m_is_true_cache[0].reset(); m_is_true_cache[0].reset();
m_is_true_cache[1].reset(); m_is_true_cache[1].reset();
m_to_enode_cache.reset(); m_to_enode_cache.reset();

8
src/smt/smt_checker.h
View file

@ -37,10 +37,10 @@ namespace smt {
unsigned m_num_bindings; unsigned m_num_bindings;
enode * const * m_bindings; enode * const * m_bindings;
bool all_args(app * a, bool is_true); bool all_args(app *a, unsigned depth, bool is_true);
bool any_arg(app * a, bool is_true); bool any_arg(app *a, unsigned depth, bool is_true);
bool check_core(expr * n, bool is_true); bool check_core(expr * n, unsigned depth, bool is_true);
bool check(expr * n, bool is_true); bool check(expr *n, unsigned depth, bool is_true);
enode * get_enode_eq_to_core(app * n); enode * get_enode_eq_to_core(app * n);
enode * get_enode_eq_to(expr * n); enode * get_enode_eq_to(expr * n);