diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-27 13:55:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-27 13:55:08 -0500 |
| commit | dc6e0f9c0489e733a70e6715b8dfba4e7fa4f0bd (patch) | |
| tree | f9a52b7fb2054a0c1a31e5433e8e1c507d21e9a6 /src/theory/quantifiers/extended_rewrite.h | |
| parent | 68a994dbb7527b6f98975bbb776687413f23d451 (diff) | |
Core improvements to extended rewriter (#1820)
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.h')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index bfae55730..937f522b2 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -66,6 +66,13 @@ class ExtendedRewriter bool d_aggr; /** cache that the extended rewritten form of n is ret */ void setCache(Node n, Node ret); + /** add to children + * + * Adds nc to the vector of children, if dropDup is true, we do not add + * nc if it already occurs in children. This method returns false in this + * case, otherwise it returns true. + */ + bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup); //--------------------------------------generic utilities /** Rewrite ITE, for example: |