diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-09 20:09:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-09 20:09:51 -0500 |
| commit | fc9e113c5f9ea99a1308d0f36b1aad778747870c (patch) | |
| tree | 1bc632ebe9d2c28a6ffaac4dc90d7b5203647624 /src/theory/uf | |
| parent | 51824dbdc2a8c19cbae7c76826732ae2f319111d (diff) | |
Fix higher-order term indexing. (#1754)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index c45dd4833..fe9247ae8 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -148,7 +148,11 @@ public: //conversion between HO_APPLY AND APPLY_UF // cannot construct APPLY_UF if operator is partially applied or is not standard return Node::null(); } - // collects arguments into args, returns operator of a curried HO_APPLY node + /** + * Given a curried HO_APPLY term n, this method adds its arguments into args + * and returns its operator. If the argument opInArgs is true, then we add + * its operator to args. + */ static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) { TNode curr = n; while( curr.getKind() == kind::HO_APPLY ){ |