src/theory/bags/rewrites.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mudathir Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Type for rewrites for bags.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__BAGS__REWRITES_H
  19 #define CVC5__THEORY__BAGS__REWRITES_H
  20
  21 #include <iosfwd>
  22
  23 namespace cvc5 {
  24 namespace theory {
  25 namespace bags {
  26
  27 /** Types of rewrites used by bags
  28  *
  29  * This rewrites are documented where they are used in the rewriter.
  30  */
  31 enum class Rewrite : uint32_t
  32 {
  33   NONE,  // no rewrite happened
  34   BAG_MAKE_COUNT_NEGATIVE,
  35   CARD_DISJOINT,
  36   CARD_BAG_MAKE,
  37   CHOOSE_BAG_MAKE,
  38   CONSTANT_EVALUATION,
  39   COUNT_EMPTY,
  40   COUNT_BAG_MAKE,
  41   DUPLICATE_REMOVAL_BAG_MAKE,
  42   EQ_CONST_FALSE,
  43   EQ_REFL,
  44   EQ_SYM,
  45   FILTER_CONST,
  46   FILTER_BAG_MAKE,
  47   FILTER_UNION_DISJOINT,
  48   FROM_SINGLETON,
  49   FOLD_BAG,
  50   FOLD_CONST,
  51   FOLD_UNION_DISJOINT,
  52   IDENTICAL_NODES,
  53   INTERSECTION_EMPTY_LEFT,
  54   INTERSECTION_EMPTY_RIGHT,
  55   INTERSECTION_SAME,
  56   INTERSECTION_SHARED_LEFT,
  57   INTERSECTION_SHARED_RIGHT,
  58   IS_SINGLETON_BAG_MAKE,
  59   MAP_CONST,
  60   MAP_BAG_MAKE,
  61   MAP_UNION_DISJOINT,
  62   MEMBER,
  63   REMOVE_FROM_UNION,
  64   REMOVE_MIN,
  65   REMOVE_RETURN_LEFT,
  66   REMOVE_SAME,
  67   SUB_BAG,
  68   SUBTRACT_DISJOINT_SHARED_LEFT,
  69   SUBTRACT_DISJOINT_SHARED_RIGHT,
  70   SUBTRACT_FROM_UNION,
  71   SUBTRACT_MIN,
  72   SUBTRACT_RETURN_LEFT,
  73   SUBTRACT_SAME,
  74   TO_SINGLETON,
  75   UNION_DISJOINT_EMPTY_LEFT,
  76   UNION_DISJOINT_EMPTY_RIGHT,
  77   UNION_DISJOINT_MAX_MIN,
  78   UNION_MAX_EMPTY,
  79   UNION_MAX_SAME_OR_EMPTY,
  80   UNION_MAX_UNION_LEFT,
  81   UNION_MAX_UNION_RIGHT
  82 };
  83
  84 /**
  85  * Converts an rewrite to a string. Note: This function is also used in
  86  * `safe_print()`. Changing this functions name or signature will result in
  87  * `safe_print()` printing "<unsupported>" instead of the proper strings for
  88  * the enum values.
  89  *
  90  * @param r The rewrite
  91  * @return The name of the rewrite
  92  */
  93 const char* toString(Rewrite r);
  94
  95 /**
  96  * Writes an rewrite name to a stream.
  97  *
  98  * @param out The stream to write to
  99  * @param r The rewrite to write to the stream
 100  * @return The stream
 101  */
 102 std::ostream& operator<<(std::ostream& out, Rewrite r);
 103
 104 }  // namespace bags
 105 }  // namespace theory
 106 }  // namespace cvc5
 107
 108 #endif /* CVC5__THEORY__BAGS__REWRITES_H */