Searched refs:pattern_fds (Results 1 – 2 of 2) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_solver.cpp | 398 bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) { in fds_intersect() argument
399 for (func_decl * fd : pattern_fds) { in fds_intersect()
410 func_decl_set pattern_fds; in add_pattern_literals_to_core() local
421 collect_pattern_fds(assrtn, pattern_fds); in add_pattern_literals_to_core()
425 if (!pattern_fds.empty()) { in add_pattern_literals_to_core()
432 fds_intersect(pattern_fds, assrtn_fds[i])) in add_pattern_literals_to_core()
474 func_decl_set pattern_fds, body_fds; in add_nonlocal_pattern_literals_to_core() local
475 collect_pattern_fds(assrtn, pattern_fds); in add_nonlocal_pattern_literals_to_core()
478 for (func_decl *fd : pattern_fds) { in add_nonlocal_pattern_literals_to_core()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_solver.cpp | 394 bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) { in fds_intersect() argument
395 for (func_decl * fd : pattern_fds) { in fds_intersect()
406 func_decl_set pattern_fds; in add_pattern_literals_to_core() local
417 collect_pattern_fds(assrtn, pattern_fds); in add_pattern_literals_to_core()
421 if (!pattern_fds.empty()) { in add_pattern_literals_to_core()
428 fds_intersect(pattern_fds, assrtn_fds[i])) in add_pattern_literals_to_core()
470 func_decl_set pattern_fds, body_fds; in add_nonlocal_pattern_literals_to_core() local
471 collect_pattern_fds(assrtn, pattern_fds); in add_nonlocal_pattern_literals_to_core()
474 for (func_decl *fd : pattern_fds) { in add_nonlocal_pattern_literals_to_core()
|