47 CheckArgument(type.isArray(), type,
"array store-all constants can only be created for array types, not `%s'", type.toString().c_str());
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");
64 return d_type == asa.d_type && d_expr == asa.d_expr;
67 return !(*
this == asa);
71 return d_type < asa.d_type ||
72 (d_type == asa.d_type && d_expr < asa.d_expr);
75 return d_type < asa.d_type ||
76 (d_type == asa.d_type && d_expr <= asa.d_expr);
79 return !(*
this <= asa);
82 return !(*
this < asa);
Class encapsulating CVC4 expressions and methods for constructing new expressions.
ArrayStoreAll(ArrayType type, Expr expr)
size_t operator()(const ArrayStoreAll &asa) const
bool operator<(const ArrayStoreAll &asa) const
std::ostream & operator<<(std::ostream &out, const UninterpretedConstant &uc)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Class encapsulating an array type.
bool operator==(const ArrayStoreAll &asa) const
bool operator>=(const ArrayStoreAll &asa) const
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator>(const ArrayStoreAll &asa) const
bool operator!=(const ArrayStoreAll &asa) const
struct CVC4::options::out__option_t out
Hash function for the ArrayStoreAll constants.
ArrayType getType() const
bool operator<=(const ArrayStoreAll &asa) const
Interface for expression types.