35 CheckArgument(type.isSort(), type,
"uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
36 CheckArgument(index >= 0, index,
"index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
50 return d_type == uc.d_type && d_index == uc.d_index;
53 return !(*
this == uc);
57 return d_type < uc.d_type ||
58 (d_type == uc.d_type && d_index < uc.d_index);
61 return d_type < uc.d_type ||
62 (d_type == uc.d_type && d_index <= uc.d_index);
65 return !(*
this <= uc);
Hash function for the BitVector constants.
bool operator>(const UninterpretedConstant &uc) const
const Integer & getIndex() const
Class encapsulating CVC4 expression types.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
UninterpretedConstant(Type type, Integer index)
bool operator>=(const UninterpretedConstant &uc) const
bool operator<(const UninterpretedConstant &uc) const
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator==(const UninterpretedConstant &uc) const
bool operator<=(const UninterpretedConstant &uc) const
struct CVC4::options::out__option_t out
bool operator!=(const UninterpretedConstant &uc) const
Interface for expression types.
size_t operator()(const UninterpretedConstant &uc) const