src/expr/array_store_all.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Andres Noetzli, Mathias Preiner
   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  * Representation of a constant array (an array in which the element is the
  14  * same for all indices).
  15  */
  16
  17 #include "cvc5_public.h"
  18
  19 #ifndef CVC5__ARRAY_STORE_ALL_H
  20 #define CVC5__ARRAY_STORE_ALL_H
  21
  22 #include <iosfwd>
  23 #include <memory>
  24
  25 namespace cvc5 {
  26
  27 template <bool ref_count>
  28 class NodeTemplate;
  29 typedef NodeTemplate<true> Node;
  30 class TypeNode;
  31
  32 class ArrayStoreAll
  33 {
  34  public:
  35   /**
  36    * @throws IllegalArgumentException if `type` is not an array or if `expr` is
  37    * not a constant of type `type`.
  38    */
  39   ArrayStoreAll(const TypeNode& type, const Node& value);
  40   ~ArrayStoreAll();
  41
  42   ArrayStoreAll(const ArrayStoreAll& other);
  43   ArrayStoreAll& operator=(const ArrayStoreAll& other);
  44
  45   const TypeNode& getType() const;
  46   const Node& getValue() const;
  47
  48   bool operator==(const ArrayStoreAll& asa) const;
  49   bool operator!=(const ArrayStoreAll& asa) const;
  50   bool operator<(const ArrayStoreAll& asa) const;
  51   bool operator<=(const ArrayStoreAll& asa) const;
  52   bool operator>(const ArrayStoreAll& asa) const;
  53   bool operator>=(const ArrayStoreAll& asa) const;
  54
  55  private:
  56   std::unique_ptr<TypeNode> d_type;
  57   std::unique_ptr<Node> d_value;
  58 }; /* class ArrayStoreAll */
  59
  60 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa);
  61
  62 /**
  63  * Hash function for the ArrayStoreAll constants.
  64  */
  65 struct ArrayStoreAllHashFunction
  66 {
  67   size_t operator()(const ArrayStoreAll& asa) const;
  68 }; /* struct ArrayStoreAllHashFunction */
  69
  70 }  // namespace cvc5
  71
  72 #endif /* CVC5__ARRAY_STORE_ALL_H */