diff options
Diffstat (limited to 'src/theory/sets/theory_sets_rewriter.h')
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 693731862..1d2f36255 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -74,6 +74,15 @@ private: * Returns true if elementTerm is in setTerm, where both terms are constants. */ bool checkConstantMembership(TNode elementTerm, TNode setTerm); + /** + * rewrites for n include: + * - (set.map f (as set.empty (Set T1)) = (as set.empty (Set T2)) + * - (set.map f (set.singleton x)) = (set.singleton (apply f x)) + * - (set.map f (set.union A B)) = + * (set.union (set.map f A) (set.map f B)) + * where f: T1 -> T2 + */ + RewriteResponse postRewriteMap(TNode n); }; /* class TheorySetsRewriter */ } // namespace sets |