mirror of
https://github.com/Z3Prover/z3
synced 2026-02-19 15:04:42 +00:00
parent
cea0f7c427
commit
b2db2c8b23
4 changed files with 14 additions and 6 deletions
|
|
@ -27,9 +27,9 @@ bool uses_theory(expr * n, family_id fid) {
|
|||
|
||||
namespace {
|
||||
struct found {};
|
||||
struct proc {
|
||||
struct proc_z3 {
|
||||
family_id m_fid;
|
||||
proc(family_id fid):m_fid(fid) {}
|
||||
proc_z3(family_id fid):m_fid(fid) {}
|
||||
void operator()(var * n) {}
|
||||
void operator()(app * n) { if (n->get_family_id() == m_fid) throw found(); }
|
||||
void operator()(quantifier * n) {}
|
||||
|
|
@ -37,7 +37,7 @@ namespace {
|
|||
}
|
||||
|
||||
bool uses_theory(expr * n, family_id fid, expr_mark & visited) {
|
||||
proc p(fid);
|
||||
proc_z3 p(fid);
|
||||
try {
|
||||
for_each_expr(p, visited, n);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue