diff options
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: |