bool LogicInfo::isDifferenceLogic() const {
  PrettyCheckArgument(d_locked, *this,
                      "This LogicInfo isn't locked yet, and cannot be queried");
  PrettyCheckArgument(
      isTheoryEnabled(theory::THEORY_ARITH), *this,
      "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
  return d_differenceLogic;
}

Type SymbolTable::lookupType(const std::string& name,
                             const std::vector<Type>& params) const throw() {
  pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
  PrettyCheckArgument(p.first.size() == params.size(), params,
                "type constructor arity is wrong: "
                "`%s' requires %u parameters but was provided %u",
         name.c_str(), p.first.size(), params.size());
  if(p.first.size() == 0) {
    PrettyCheckArgument(p.second.isSort(), name.c_str());
    return p.second;
  }
  if(p.second.isSortConstructor()) {
    if(Debug.isOn("sort")) {
      Debug("sort") << "instantiating using a sort constructor" << endl;
      Debug("sort") << "have formals [";
      copy( p.first.begin(), p.first.end() - 1,
            ostream_iterator<Type>(Debug("sort"), ", ") );
      Debug("sort") << p.first.back() << "]" << endl
                    << "parameters   [";
      copy( params.begin(), params.end() - 1,
            ostream_iterator<Type>(Debug("sort"), ", ") );
      Debug("sort") << params.back() << "]" << endl
                    << "type ctor    " << name << endl
                    << "type is      " << p.second << endl;
    }

    Type instantiation =
      SortConstructorType(p.second).instantiate(params);

    Debug("sort") << "instance is  " << instantiation << endl;

    return instantiation;
  } else if(p.second.isDatatype()) {
    PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
    return DatatypeType(p.second).instantiate(params);
  } else {
    if(Debug.isOn("sort")) {
      Debug("sort") << "instantiating using a sort substitution" << endl;
      Debug("sort") << "have formals [";
      copy( p.first.begin(), p.first.end() - 1,
            ostream_iterator<Type>(Debug("sort"), ", ") );
      Debug("sort") << p.first.back() << "]" << endl
                    << "parameters   [";
      copy( params.begin(), params.end() - 1,
            ostream_iterator<Type>(Debug("sort"), ", ") );
      Debug("sort") << params.back() << "]" << endl
                    << "type ctor    " << name << endl
                    << "type is      " << p.second << endl;
    }

    Type instantiation = p.second.substitute(p.first, params);

    Debug("sort") << "instance is  " << instantiation << endl;

    return instantiation;
  }
}

size_t Record::getIndex(std::string name) const {
  FieldVector::const_iterator i = find(*d_fields, name);
  PrettyCheckArgument(i != d_fields->end(), name,
                      "requested field `%s' does not exist in record",
                      name.c_str());
  return i - d_fields->begin();
}

Result::Result(enum Sat s, std::string inputName)
    : d_sat(s),
      d_validity(VALIDITY_UNKNOWN),
      d_which(TYPE_SAT),
      d_unknownExplanation(UNKNOWN_REASON),
      d_inputName(inputName) {
  PrettyCheckArgument(s != SAT_UNKNOWN,
                      "Must provide a reason for satisfiability being unknown");
}

const Datatype& DatatypeType::getDatatype() const {
  NodeManagerScope nms(d_nodeManager);
  if( d_typeNode->isParametricDatatype() ) {
    PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
    const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
    return dt;
  } else {
    return d_typeNode->getDatatype();
  }
}

ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr)
    : d_type(), d_expr() {
  // this check is stronger than the assertion check in the expr manager that
  // ArrayTypes are actually array types
  // because this check is done in production builds too
  PrettyCheckArgument(
      type.isArray(), type,
      "array store-all constants can only be created for array types, not `%s'",
      type.toString().c_str());

  PrettyCheckArgument(
      expr.getType().isComparableTo(type.getConstituentType()), expr,
      "expr type `%s' does not match constituent type of array type `%s'",
      expr.getType().toString().c_str(), type.toString().c_str());

  PrettyCheckArgument(expr.isConst(), expr,
                      "ArrayStoreAll requires a constant expression");

  // Delay allocation until the checks above have been performed. If these fail,
  // the memory for d_type and d_expr should not leak. The alternative is catch,
  // delete and re-throw.
  d_type.reset(new ArrayType(type));
  d_expr.reset(new Expr(expr));
}

Type& Type::operator=(const Type& t) {
  PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
  PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");

  if(this != &t) {
    if(d_nodeManager == t.d_nodeManager) {
      NodeManagerScope nms(d_nodeManager);
      *d_typeNode = *t.d_typeNode;
    } else {
      // This happens more than you think---every time you set to or
      // from the null Type.  It's tricky because each node manager
      // must be in play at the right time.

      NodeManagerScope nms1(d_nodeManager);
      *d_typeNode = TypeNode::null();

      NodeManagerScope nms2(t.d_nodeManager);
      *d_typeNode = *t.d_typeNode;

      d_nodeManager = t.d_nodeManager;
    }
  }
  return *this;
}

std::string SExpr::getValue() const {
  PrettyCheckArgument(isAtom(), this);
  switch (d_sexprType) {
    case SEXPR_INTEGER:
      return d_integerValue.toString();
    case SEXPR_RATIONAL: {
      // We choose to represent rationals as decimal strings rather than
      // "numerator/denominator."  Perhaps an additional SEXPR_DECIMAL
      // could be added if we need both styles, even if it's backed by
      // the same Rational object.
      std::stringstream ss;
      ss << std::fixed << d_rationalValue.getDouble();
      return ss.str();
    }
    case SEXPR_STRING:
    case SEXPR_KEYWORD:
      return d_stringValue;
    case SEXPR_NOT_ATOM:
      return std::string();
  }
  return std::string();
}

SubrangeType::SubrangeType(const Type& t)
  throw(IllegalArgumentException) :
  Type(t) {
  PrettyCheckArgument(isNull() || isSubrange(), this);
}