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

style(datatype): use modern iteration

Browse source
This commit is contained in:
Simon Cruanes 2018-04-06 17:19:06 -05:00
parent 8fd2d8a636
commit ac881d949d
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_datatype.cpp
View file

@ -429,9 +429,7 @@ namespace smt {
// first: explain that root=v, given that app=cstor(…,v,…) // first: explain that root=v, given that app=cstor(…,v,…)
{ {
enode * app_cstor = oc_get_cstor(app); enode * app_cstor = oc_get_cstor(app);
unsigned n_args_app = app_cstor->get_num_args(); for (enode * arg : enode::args(app_cstor)) {
for (unsigned i=0; i < n_args_app; ++i) {
enode * arg = app_cstor->get_arg(i);
// found an argument which is equal to root // found an argument which is equal to root
if (arg->get_root() == root->get_root()) { if (arg->get_root() == root->get_root()) {
if (arg != root) if (arg != root)
@ -463,9 +461,7 @@ namespace smt {
v = m_find.find(v); v = m_find.find(v);
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
if (d->m_constructor) { if (d->m_constructor) {
unsigned num_args = d->m_constructor->get_num_args(); for (enode * arg : enode::args(d->m_constructor)) {
for (unsigned i = 0; i < num_args; i++) {
enode * arg = d->m_constructor->get_arg(i);
if (oc_cycle_free(arg)) { if (oc_cycle_free(arg)) {
return false; return false;
} }