Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minor refactor in strings rewriter #3387

Merged
merged 6 commits into from Oct 14, 2019
Merged

Conversation

ajreynol
Copy link
Member

No description provided.

@ajreynol ajreynol added minor Priority simple Complexity labels Oct 11, 2019
@ajreynol ajreynol requested a review from 4tXJ7f October 11, 2019 19:00
Copy link
Member

@4tXJ7f 4tXJ7f left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, just two minor suggestions.

}
preNode = Node::null();
++j;
for (const Node& nc : node)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could just do for (Node tmp : node), then we don't need the next line.

}
for (; j < tmpNode.getNumChildren() - 1; ++j)
{
node_vec.push_back(tmpNode[j]);
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could do: node_vec.insert(node_vec.end(), tmpNode.begin() + j, tmpNode.end() - 1); (untested)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There were a few issues with doing this, but I've now refactored so there isn't a for loop.

@4tXJ7f 4tXJ7f added the do not merge Do not merge this PR if you are not the author label Oct 11, 2019
@ajreynol ajreynol removed the do not merge Do not merge this PR if you are not the author label Oct 14, 2019
@ajreynol ajreynol merged commit 04d6ede into cvc5:master Oct 14, 2019
@ajreynol ajreynol deleted the strRewrite092019 branch October 14, 2019 17:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
minor Priority simple Complexity
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants