cvc4-1.4
array_store_all.h
Go to the documentation of this file.
1 /********************* */
19 #include "cvc4_public.h"
20 
21 #pragma once
22 
23 namespace CVC4 {
24  // messy; Expr needs ArrayStoreAll (because it's the payload of a
25  // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
26  class CVC4_PUBLIC ArrayStoreAll;
27 }/* CVC4 namespace */
28 
29 #include "expr/expr.h"
30 #include "expr/type.h"
31 #include <iostream>
32 
33 namespace CVC4 {
34 
36  const ArrayType d_type;
37  const Expr d_expr;
38 
39 public:
40 
42  d_type(type),
43  d_expr(expr) {
44 
45  // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
46  // because this check is done in production builds too
47  CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str());
48 
49  CheckArgument(expr.getType().isSubtypeOf(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str());
50  CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression");
51  }
52 
53  ~ArrayStoreAll() throw() {
54  }
55 
56  ArrayType getType() const throw() {
57  return d_type;
58  }
59  Expr getExpr() const throw() {
60  return d_expr;
61  }
62 
63  bool operator==(const ArrayStoreAll& asa) const throw() {
64  return d_type == asa.d_type && d_expr == asa.d_expr;
65  }
66  bool operator!=(const ArrayStoreAll& asa) const throw() {
67  return !(*this == asa);
68  }
69 
70  bool operator<(const ArrayStoreAll& asa) const throw() {
71  return d_type < asa.d_type ||
72  (d_type == asa.d_type && d_expr < asa.d_expr);
73  }
74  bool operator<=(const ArrayStoreAll& asa) const throw() {
75  return d_type < asa.d_type ||
76  (d_type == asa.d_type && d_expr <= asa.d_expr);
77  }
78  bool operator>(const ArrayStoreAll& asa) const throw() {
79  return !(*this <= asa);
80  }
81  bool operator>=(const ArrayStoreAll& asa) const throw() {
82  return !(*this < asa);
83  }
84 
85 };/* class ArrayStoreAll */
86 
87 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
88 
92 struct CVC4_PUBLIC ArrayStoreAllHashFunction {
93  inline size_t operator()(const ArrayStoreAll& asa) const {
94  return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
95  }
96 };/* struct ArrayStoreAllHashFunction */
97 
98 }/* CVC4 namespace */
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
ArrayStoreAll(ArrayType type, Expr expr)
Hash function for Types.
Definition: type.h:69
bool operator>=(const ArrayStoreAll &asa) const
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
bool operator<(const ArrayStoreAll &asa) const
ArrayType getType() const
Expr getExpr() const
bool operator>(const ArrayStoreAll &asa) const
Class encapsulating an array type.
Definition: type.h:484
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator==(const ArrayStoreAll &asa) const
size_t operator()(const ArrayStoreAll &asa) const
struct CVC4::options::out__option_t out
Hash function for the ArrayStoreAll constants.
expr.h
bool operator<=(const ArrayStoreAll &asa) const
bool operator!=(const ArrayStoreAll &asa) const
Interface for expression types.