Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/type_node.cpp	Lines:	288	334	86.2 %
Date:	2021-09-29	Branches:	388	1026	37.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Tim King
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Reference-counted encapsulation of a pointer to node information.
 */
#include "expr/type_node.h"

#include <vector>

#include "expr/datatype_index.h"
#include "expr/dtype_cons.h"
#include "expr/node_manager_attributes.h"
#include "expr/type_properties.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "theory/type_enumerator.h"
#include "util/bitvector.h"
#include "util/cardinality.h"

using namespace std;

namespace cvc5 {

TypeNode TypeNode::s_null( &expr::NodeValue::null() );

TypeNode TypeNode::substitute(
    const TypeNode& type,
    const TypeNode& replacement,
    std::unordered_map<TypeNode, TypeNode>& cache) const
{
  // in cache?
  std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
  if(i != cache.end()) {
    return (*i).second;
  }

  // otherwise compute
  NodeBuilder nb(getKind());
  if(getMetaKind() == kind::metakind::PARAMETERIZED) {
    // push the operator
    nb << TypeNode(d_nv->d_children[0]);
  }
  for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j)
  {
    if (*j == type)
    {
      nb << replacement;
    }
    else
    {
      (*j).substitute(type, replacement);
    }
  }

  // put in cache
  TypeNode tn = nb.constructTypeNode();
  cache[*this] = tn;
  return tn;
}

Cardinality TypeNode::getCardinality() const {
  return kind::getCardinality(*this);
}

/** Attribute true for types that have cardinality one */
struct TypeCardinalityClassTag
{
};
typedef expr::Attribute<TypeCardinalityClassTag, uint64_t>
    TypeCardinalityClassAttr;

CardinalityClass TypeNode::getCardinalityClass()
{
  // check it is already cached
  if (hasAttribute(TypeCardinalityClassAttr()))
  {
    return static_cast<CardinalityClass>(
        getAttribute(TypeCardinalityClassAttr()));
  }
  CardinalityClass ret = CardinalityClass::INFINITE;
  if (isSort())
  {
    ret = CardinalityClass::INTERPRETED_ONE;
  }
  else if (isBoolean() || isBitVector() || isFloatingPoint()
           || isRoundingMode())
  {
    ret = CardinalityClass::FINITE;
  }
  else if (isString() || isRegExp() || isSequence() || isReal() || isBag())
  {
    ret = CardinalityClass::INFINITE;
  }
  else
  {
    // recursive case (this may be a parametric sort), we assume infinite for
    // the moment here to prevent infinite loops, which may occur when
    // computing the cardinality of datatype types with foreign types
    setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));

    if (isDatatype())
    {
      TypeNode tn = *this;
      const DType& dt = getDType();
      ret = dt.getCardinalityClass(tn);
    }
    else if (isArray())
    {
      ret = getArrayConstituentType().getCardinalityClass();
      if (ret == CardinalityClass::FINITE
          || ret == CardinalityClass::INTERPRETED_FINITE)
      {
        CardinalityClass cci = getArrayIndexType().getCardinalityClass();
        // arrays with both finite element types, we take the max with its
        // index type.
        ret = maxCardinalityClass(ret, cci);
      }
      // else, array types whose element type is INFINITE, ONE, or
      // INTERPRETED_ONE have the same cardinality class as their range.
    }
    else if (isSet())
    {
      CardinalityClass cc = getSetElementType().getCardinalityClass();
      if (cc == CardinalityClass::ONE)
      {
        // 1 -> 2
        ret = CardinalityClass::FINITE;
      }
      else if (ret == CardinalityClass::INTERPRETED_ONE)
      {
        // maybe 1 -> maybe finite
        ret = CardinalityClass::INTERPRETED_FINITE;
      }
      else
      {
        // finite or infinite is unchanged
        ret = cc;
      }
    }
    else if (isFunction())
    {
      ret = getRangeType().getCardinalityClass();
      if (ret == CardinalityClass::FINITE
          || ret == CardinalityClass::INTERPRETED_FINITE)
      {
        // we may have a larger cardinality class based on the
        // arguments of the function
        std::vector<TypeNode> argTypes = getArgTypes();
        for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
        {
          CardinalityClass cca = argTypes[i].getCardinalityClass();
          ret = maxCardinalityClass(ret, cca);
        }
      }
      // else, function types whose range type is INFINITE, ONE, or
      // INTERPRETED_ONE have the same cardinality class as their range.
    }
    else if (isConstructor())
    {
      // notice that we require computing the cardinality class of the
      // constructor type, which is equivalent to asking how many
      // constructor applications of the given constructor exist. This
      // is used in several places in the decision procedure for datatypes.
      // The cardinality starts with one.
      ret = CardinalityClass::ONE;
      // we may have a larger cardinality class based on the
      // arguments of the constructor
      std::vector<TypeNode> argTypes = getArgTypes();
      for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
      {
        CardinalityClass cca = argTypes[i].getCardinalityClass();
        ret = maxCardinalityClass(ret, cca);
      }
    }
    else
    {
      // all types we care about should be handled above
      Assert(false);
    }
  }
  setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));
  return ret;
}

/** Attribute true for types that are closed enumerable */
struct IsClosedEnumerableTag
{
};
struct IsClosedEnumerableComputedTag
{
};
typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
    IsClosedEnumerableComputedAttr;

bool TypeNode::isClosedEnumerable()
{
  // check it is already cached
  if (!getAttribute(IsClosedEnumerableComputedAttr()))
  {
    bool ret = true;
    if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp())
    {
      ret = false;
    }
    else if (isSet())
    {
      ret = getSetElementType().isClosedEnumerable();
    }
    else if (isSequence())
    {
      ret = getSequenceElementType().isClosedEnumerable();
    }
    else if (isDatatype())
    {
      // avoid infinite loops: initially set to true
      setAttribute(IsClosedEnumerableAttr(), ret);
      setAttribute(IsClosedEnumerableComputedAttr(), true);
      TypeNode tn = *this;
      const DType& dt = getDType();
      for (uint32_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
      {
        for (uint32_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
        {
          TypeNode ctn = dt[i][j].getRangeType();
          if (tn != ctn && !ctn.isClosedEnumerable())
          {
            ret = false;
            break;
          }
        }
        if (!ret)
        {
          break;
        }
      }
    }
    setAttribute(IsClosedEnumerableAttr(), ret);
    setAttribute(IsClosedEnumerableComputedAttr(), true);
    return ret;
  }
  return getAttribute(IsClosedEnumerableAttr());
}

bool TypeNode::isFirstClass() const
{
  return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
         && getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE
         && (getKind() != kind::TYPE_CONSTANT
             || (getConst<TypeConstant>() != REGEXP_TYPE
                 && getConst<TypeConstant>() != SEXPR_TYPE));
}

bool TypeNode::isWellFounded() const {
  return kind::isWellFounded(*this);
}

Node TypeNode::mkGroundTerm() const {
  return kind::mkGroundTerm(*this);
}

Node TypeNode::mkGroundValue() const
{
  theory::TypeEnumerator te(*this);
  return *te;
}

bool TypeNode::isStringLike() const { return isString() || isSequence(); }

bool TypeNode::isSubtypeOf(TypeNode t) const {
  if(*this == t) {
    return true;
  }
  if(getKind() == kind::TYPE_CONSTANT) {
    switch(getConst<TypeConstant>()) {
    case INTEGER_TYPE:
      return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
    default:
      return false;
    }
  }
  if (isFunction() && t.isFunction())
  {
    if (!isComparableTo(t))
    {
      // incomparable, not subtype
      return false;
    }
    return getRangeType().isSubtypeOf(t.getRangeType());
  }
  // this should only return true for types T1, T2 where we handle equalities between T1 and T2
  // (more cases go here, if we want to support such cases)
  return false;
}

bool TypeNode::isComparableTo(TypeNode t) const {
  if(*this == t) {
    return true;
  }
  if(isSubtypeOf(NodeManager::currentNM()->realType())) {
    return t.isSubtypeOf(NodeManager::currentNM()->realType());
  }
  if (isFunction() && t.isFunction())
  {
    // comparable if they have a common type node
    return !leastCommonTypeNode(*this, t).isNull();
  }
  return false;
}

TypeNode TypeNode::getTesterDomainType() const
{
  Assert(isTester());
  return (*this)[0];
}

TypeNode TypeNode::getSequenceElementType() const
{
  Assert(isSequence());
  return (*this)[0];
}

TypeNode TypeNode::getBaseType() const {
  TypeNode realt = NodeManager::currentNM()->realType();
  if (isSubtypeOf(realt)) {
    return realt;
  } else if (isParametricDatatype()) {
    std::vector<TypeNode> v;
    for(size_t i = 1; i < getNumChildren(); ++i) {
      v.push_back((*this)[i].getBaseType());
    }
    return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v);
  }
  return *this;
}

std::vector<TypeNode> TypeNode::getArgTypes() const {
  vector<TypeNode> args;
  if(isTester()) {
    Assert(getNumChildren() == 1);
    args.push_back((*this)[0]);
  } else {
    Assert(isFunction() || isConstructor() || isSelector());
    for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
      args.push_back((*this)[i]);
    }
  }
  return args;
}

std::vector<TypeNode> TypeNode::getParamTypes() const {
  vector<TypeNode> params;
  Assert(isParametricDatatype());
  for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
    params.push_back((*this)[i]);
  }
  return params;
}

bool TypeNode::isTuple() const
{
  return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
}

bool TypeNode::isRecord() const
{
  return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord());
}

size_t TypeNode::getTupleLength() const {
  Assert(isTuple());
  const DType& dt = getDType();
  Assert(dt.getNumConstructors() == 1);
  return dt[0].getNumArgs();
}

vector<TypeNode> TypeNode::getTupleTypes() const {
  Assert(isTuple());
  const DType& dt = getDType();
  Assert(dt.getNumConstructors() == 1);
  vector<TypeNode> types;
  for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
    types.push_back(dt[0][i].getRangeType());
  }
  return types;
}

/** Is this an instantiated datatype type */
bool TypeNode::isInstantiatedDatatype() const {
  if(getKind() == kind::DATATYPE_TYPE) {
    return true;
  }
  if(getKind() != kind::PARAMETRIC_DATATYPE) {
    return false;
  }
  const DType& dt = (*this)[0].getDType();
  unsigned n = dt.getNumParameters();
  Assert(n < getNumChildren());
  for(unsigned i = 0; i < n; ++i) {
    if (dt.getParameter(i) == (*this)[i + 1])
    {
      return false;
    }
  }
  return true;
}

TypeNode TypeNode::instantiateParametricDatatype(
    const std::vector<TypeNode>& params) const
{
  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
  AssertArgument(params.size() == getNumChildren() - 1, *this);
  NodeManager* nm = NodeManager::currentNM();
  TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>());
  std::vector<TypeNode> paramsNodes;
  paramsNodes.push_back(cons);
  for (const TypeNode& t : params)
  {
    paramsNodes.push_back(t);
  }
  return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
}

uint64_t TypeNode::getSortConstructorArity() const
{
  Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr()));
  return getAttribute(expr::SortArityAttr());
}

std::string TypeNode::getName() const
{
  Assert(isSort() || isSortConstructor());
  return getAttribute(expr::VarNameAttr());
}

TypeNode TypeNode::instantiateSortConstructor(
    const std::vector<TypeNode>& params) const
{
  Assert(isSortConstructor());
  return NodeManager::currentNM()->mkSort(*this, params);
}

/** Is this an instantiated datatype parameter */
bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
  AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
  const DType& dt = (*this)[0].getDType();
  AssertArgument(n < dt.getNumParameters(), *this);
  return dt.getParameter(n) != (*this)[n + 1];
}

TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
  return commonTypeNode( t0, t1, true );
}

TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
  return commonTypeNode( t0, t1, false );
}

TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
  Assert(!t0.isNull());
  Assert(!t1.isNull());

  if(__builtin_expect( (t0 == t1), true )) {
    return t0;
  }

  // t0 != t1 &&
  if(t0.getKind() == kind::TYPE_CONSTANT) {
    switch(t0.getConst<TypeConstant>()) {
    case INTEGER_TYPE:
      if(t1.isInteger()) {
        // t0 == IntegerType && t1.isInteger()
        return t0; //IntegerType
      } else if(t1.isReal()) {
        // t0 == IntegerType && t1.isReal() && !t1.isInteger()
        return isLeast ? t1 : t0; // RealType
      } else {
        return TypeNode(); // null type
      }
    case REAL_TYPE:
      if(t1.isReal()) {
        return isLeast ? t0 : t1; // RealType
      } else {
        return TypeNode(); // null type
      }
    default:
      return TypeNode(); // null type
    }
  } else if(t1.getKind() == kind::TYPE_CONSTANT) {
    return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
  }

  // t0 != t1 &&
  // t0.getKind() == kind::TYPE_CONSTANT &&
  // t1.getKind() == kind::TYPE_CONSTANT
  switch(t0.getKind()) {
    case kind::FUNCTION_TYPE:
    {
      if (t1.getKind() != kind::FUNCTION_TYPE)
      {
        return TypeNode();
      }
      // must have equal arguments
      std::vector<TypeNode> t0a = t0.getArgTypes();
      std::vector<TypeNode> t1a = t1.getArgTypes();
      if (t0a.size() != t1a.size())
      {
        // different arities
        return TypeNode();
      }
      for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++)
      {
        if (t0a[i] != t1a[i])
        {
          // an argument is different
          return TypeNode();
        }
      }
      TypeNode t0r = t0.getRangeType();
      TypeNode t1r = t1.getRangeType();
      TypeNode tr = commonTypeNode(t0r, t1r, isLeast);
      std::vector<TypeNode> ftypes;
      ftypes.insert(ftypes.end(), t0a.begin(), t0a.end());
      ftypes.push_back(tr);
      return NodeManager::currentNM()->mkFunctionType(ftypes);
    }
    break;
    case kind::BITVECTOR_TYPE:
    case kind::FLOATINGPOINT_TYPE:
    case kind::SORT_TYPE:
    case kind::CONSTRUCTOR_TYPE:
    case kind::SELECTOR_TYPE:
    case kind::TESTER_TYPE:
    case kind::ARRAY_TYPE:
    case kind::DATATYPE_TYPE:
    case kind::PARAMETRIC_DATATYPE:
    case kind::SEQUENCE_TYPE:
    case kind::SET_TYPE:
    case kind::BAG_TYPE:
    {
      // we don't support subtyping except for built in types Int and Real.
      return TypeNode();  // return null type
    }
    default:
      Unimplemented() << "don't have a commonType for types `" << t0
                      << "' and `" << t1 << "'";
  }
}

Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
  TypeNode ntn = n.getType();
  Assert(ntn.isComparableTo(tn));
  if( !ntn.isSubtypeOf( tn ) ){
    if( tn.isInteger() ){
      if( tn.isSubtypeOf( ntn ) ){
        return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
      }
    }else if( tn.isDatatype() && ntn.isDatatype() ){
      if( tn.isTuple() && ntn.isTuple() ){
        const DType& dt1 = tn.getDType();
        const DType& dt2 = ntn.getDType();
        NodeManager* nm = NodeManager::currentNM();
        if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
          std::vector< Node > conds;
          for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
            Node s = nm->mkNode(
                kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n);
            Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType());
            if( etc.isNull() ){
              return Node::null();
            }else{
              conds.push_back( etc );
            }
          }
          if( conds.empty() ){
            return nm->mkConst(true);
          }else if( conds.size()==1 ){
            return conds[0];
          }else{
            return nm->mkNode(kind::AND, conds);
          }
        }
      }
    }
    return Node::null();
  }else{
    return NodeManager::currentNM()->mkConst( true );
  }
}

/** Is this a sort kind */
bool TypeNode::isSort() const {
  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
}

/** Is this a sort constructor kind */
bool TypeNode::isSortConstructor() const {
  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
}

bool TypeNode::isFloatingPoint() const
{
  return getKind() == kind::FLOATINGPOINT_TYPE;
}

bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; }

bool TypeNode::isDatatype() const
{
  return getKind() == kind::DATATYPE_TYPE
         || getKind() == kind::PARAMETRIC_DATATYPE;
}

bool TypeNode::isParametricDatatype() const
{
  return getKind() == kind::PARAMETRIC_DATATYPE;
}

bool TypeNode::isConstructor() const
{
  return getKind() == kind::CONSTRUCTOR_TYPE;
}

bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; }

bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; }

bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; }

bool TypeNode::isCodatatype() const
{
  if (isDatatype())
  {
    return getDType().isCodatatype();
  }
  return false;
}

bool TypeNode::isSygusDatatype() const
{
  if (isDatatype())
  {
    return getDType().isSygus();
  }
  return false;
}

std::string TypeNode::toString() const {
  std::stringstream ss;
  Language outlang =
      (this == &s_null) ? Language::LANG_AUTO : options::outputLanguage();
  d_nv->toStream(ss, -1, 0, outlang);
  return ss.str();
}

const DType& TypeNode::getDType() const
{
  if (getKind() == kind::DATATYPE_TYPE)
  {
    DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
    return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex());
  }
  Assert(getKind() == kind::PARAMETRIC_DATATYPE);
  return (*this)[0].getDType();
}

bool TypeNode::isBag() const
{
  return getKind() == kind::BAG_TYPE;
}

TypeNode TypeNode::getBagElementType() const
{
  Assert(isBag());
  return (*this)[0];
}

bool TypeNode::isBitVector(unsigned size) const
{
  return (getKind() == kind::BITVECTOR_TYPE
          && getConst<BitVectorSize>() == size);
}

uint32_t TypeNode::getBitVectorSize() const
{
  Assert(isBitVector());
  return getConst<BitVectorSize>();
}

}  // namespace cvc5

namespace std {

size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const
{
  return tn.getId();
}

}  // namespace std


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Tim King
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		* Reference-counted encapsulation of a pointer to node information.
14		*/
15		#include "expr/type_node.h"
16
17		#include <vector>
18
19		#include "expr/datatype_index.h"
20		#include "expr/dtype_cons.h"
21		#include "expr/node_manager_attributes.h"
22		#include "expr/type_properties.h"
23		#include "options/base_options.h"
24		#include "options/quantifiers_options.h"
25		#include "theory/type_enumerator.h"
26		#include "util/bitvector.h"
27		#include "util/cardinality.h"
28
29		using namespace std;
30
31		namespace cvc5 {
32
33	7582	TypeNode TypeNode::s_null( &expr::NodeValue::null() );
34
35	2	TypeNode TypeNode::substitute(
36		const TypeNode& type,
37		const TypeNode& replacement,
38		std::unordered_map<TypeNode, TypeNode>& cache) const
39		{
40		// in cache?
41	2	std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
42	2	if(i != cache.end()) {
43		return (*i).second;
44		}
45
46		// otherwise compute
47	4	NodeBuilder nb(getKind());
48	2	if(getMetaKind() == kind::metakind::PARAMETERIZED) {
49		// push the operator
50		nb << TypeNode(d_nv->d_children[0]);
51		}
52	6	for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j)
53		{
54	4	if (*j == type)
55		{
56	4	nb << replacement;
57		}
58		else
59		{
60		(*j).substitute(type, replacement);
61		}
62		}
63
64		// put in cache
65	4	TypeNode tn = nb.constructTypeNode();
66	2	cache[*this] = tn;
67	2	return tn;
68		}
69
70	15830	Cardinality TypeNode::getCardinality() const {
71	15830	return kind::getCardinality(*this);
72		}
73
74		/** Attribute true for types that have cardinality one */
75		struct TypeCardinalityClassTag
76		{
77		};
78		typedef expr::Attribute<TypeCardinalityClassTag, uint64_t>
79		TypeCardinalityClassAttr;
80
81	3836184	CardinalityClass TypeNode::getCardinalityClass()
82		{
83		// check it is already cached
84	3836184	if (hasAttribute(TypeCardinalityClassAttr()))
85		{
86		return static_cast<CardinalityClass>(
87	3825846	getAttribute(TypeCardinalityClassAttr()));
88		}
89	10338	CardinalityClass ret = CardinalityClass::INFINITE;
90	10338	if (isSort())
91		{
92	974	ret = CardinalityClass::INTERPRETED_ONE;
93		}
94	27916	else if (isBoolean() \|\| isBitVector() \|\| isFloatingPoint()
95	15404	\|\| isRoundingMode())
96		{
97	3341	ret = CardinalityClass::FINITE;
98		}
99	6023	else if (isString() \|\| isRegExp() \|\| isSequence() \|\| isReal() \|\| isBag())
100		{
101	3200	ret = CardinalityClass::INFINITE;
102		}
103		else
104		{
105		// recursive case (this may be a parametric sort), we assume infinite for
106		// the moment here to prevent infinite loops, which may occur when
107		// computing the cardinality of datatype types with foreign types
108	2823	setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));
109
110	2823	if (isDatatype())
111		{
112	3220	TypeNode tn = *this;
113	1610	const DType& dt = getDType();
114	1610	ret = dt.getCardinalityClass(tn);
115		}
116	1213	else if (isArray())
117		{
118	374	ret = getArrayConstituentType().getCardinalityClass();
119	374	if (ret == CardinalityClass::FINITE
120	155	\|\| ret == CardinalityClass::INTERPRETED_FINITE)
121		{
122	219	CardinalityClass cci = getArrayIndexType().getCardinalityClass();
123		// arrays with both finite element types, we take the max with its
124		// index type.
125	219	ret = maxCardinalityClass(ret, cci);
126		}
127		// else, array types whose element type is INFINITE, ONE, or
128		// INTERPRETED_ONE have the same cardinality class as their range.
129		}
130	839	else if (isSet())
131		{
132	558	CardinalityClass cc = getSetElementType().getCardinalityClass();
133	558	if (cc == CardinalityClass::ONE)
134		{
135		// 1 -> 2
136	13	ret = CardinalityClass::FINITE;
137		}
138	545	else if (ret == CardinalityClass::INTERPRETED_ONE)
139		{
140		// maybe 1 -> maybe finite
141		ret = CardinalityClass::INTERPRETED_FINITE;
142		}
143		else
144		{
145		// finite or infinite is unchanged
146	545	ret = cc;
147		}
148		}
149	281	else if (isFunction())
150		{
151	278	ret = getRangeType().getCardinalityClass();
152	278	if (ret == CardinalityClass::FINITE
153	196	\|\| ret == CardinalityClass::INTERPRETED_FINITE)
154		{
155		// we may have a larger cardinality class based on the
156		// arguments of the function
157	164	std::vector<TypeNode> argTypes = getArgTypes();
158	215	for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
159		{
160	133	CardinalityClass cca = argTypes[i].getCardinalityClass();
161	133	ret = maxCardinalityClass(ret, cca);
162		}
163		}
164		// else, function types whose range type is INFINITE, ONE, or
165		// INTERPRETED_ONE have the same cardinality class as their range.
166		}
167	3	else if (isConstructor())
168		{
169		// notice that we require computing the cardinality class of the
170		// constructor type, which is equivalent to asking how many
171		// constructor applications of the given constructor exist. This
172		// is used in several places in the decision procedure for datatypes.
173		// The cardinality starts with one.
174	3	ret = CardinalityClass::ONE;
175		// we may have a larger cardinality class based on the
176		// arguments of the constructor
177	6	std::vector<TypeNode> argTypes = getArgTypes();
178	7	for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
179		{
180	4	CardinalityClass cca = argTypes[i].getCardinalityClass();
181	4	ret = maxCardinalityClass(ret, cca);
182		}
183		}
184		else
185		{
186		// all types we care about should be handled above
187		Assert(false);
188		}
189		}
190	10338	setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));
191	10338	return ret;
192		}
193
194		/** Attribute true for types that are closed enumerable */
195		struct IsClosedEnumerableTag
196		{
197		};
198		struct IsClosedEnumerableComputedTag
199		{
200		};
201		typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
202		typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
203		IsClosedEnumerableComputedAttr;
204
205	76253	bool TypeNode::isClosedEnumerable()
206		{
207		// check it is already cached
208	76253	if (!getAttribute(IsClosedEnumerableComputedAttr()))
209		{
210	1493	bool ret = true;
211	1493	if (isArray() \|\| isSort() \|\| isCodatatype() \|\| isFunction() \|\| isRegExp())
212		{
213	369	ret = false;
214		}
215	1124	else if (isSet())
216		{
217	7	ret = getSetElementType().isClosedEnumerable();
218		}
219	1117	else if (isSequence())
220		{
221		ret = getSequenceElementType().isClosedEnumerable();
222		}
223	1117	else if (isDatatype())
224		{
225		// avoid infinite loops: initially set to true
226	248	setAttribute(IsClosedEnumerableAttr(), ret);
227	248	setAttribute(IsClosedEnumerableComputedAttr(), true);
228	496	TypeNode tn = *this;
229	248	const DType& dt = getDType();
230	679	for (uint32_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
231		{
232	954	for (uint32_t j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
233		{
234	957	TypeNode ctn = dt[i][j].getRangeType();
235	523	if (tn != ctn && !ctn.isClosedEnumerable())
236		{
237	89	ret = false;
238	89	break;
239		}
240		}
241	520	if (!ret)
242		{
243	89	break;
244		}
245		}
246		}
247	1493	setAttribute(IsClosedEnumerableAttr(), ret);
248	1493	setAttribute(IsClosedEnumerableComputedAttr(), true);
249	1493	return ret;
250		}
251	74760	return getAttribute(IsClosedEnumerableAttr());
252		}
253
254	626537	bool TypeNode::isFirstClass() const
255		{
256	1253074	return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE
257	626537	&& getKind() != kind::TESTER_TYPE && getKind() != kind::UPDATER_TYPE
258	1878058	&& (getKind() != kind::TYPE_CONSTANT
259	294103	\|\| (getConst<TypeConstant>() != REGEXP_TYPE
260	919087	&& getConst<TypeConstant>() != SEXPR_TYPE));
261		}
262
263		bool TypeNode::isWellFounded() const {
264		return kind::isWellFounded(*this);
265		}
266
267	106802	Node TypeNode::mkGroundTerm() const {
268	106802	return kind::mkGroundTerm(*this);
269		}
270
271	107799	Node TypeNode::mkGroundValue() const
272		{
273	215598	theory::TypeEnumerator te(*this);
274	215598	return *te;
275		}
276
277	3473789	bool TypeNode::isStringLike() const { return isString() \|\| isSequence(); }
278
279	7778524	bool TypeNode::isSubtypeOf(TypeNode t) const {
280	7778524	if(*this == t) {
281	7415806	return true;
282		}
283	362718	if(getKind() == kind::TYPE_CONSTANT) {
284	166512	switch(getConst<TypeConstant>()) {
285	123937	case INTEGER_TYPE:
286	123937	return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
287	42575	default:
288	42575	return false;
289		}
290		}
291	196206	if (isFunction() && t.isFunction())
292		{
293	1	if (!isComparableTo(t))
294		{
295		// incomparable, not subtype
296		return false;
297		}
298	1	return getRangeType().isSubtypeOf(t.getRangeType());
299		}
300		// this should only return true for types T1, T2 where we handle equalities between T1 and T2
301		// (more cases go here, if we want to support such cases)
302	196205	return false;
303		}
304
305	2727421	bool TypeNode::isComparableTo(TypeNode t) const {
306	2727421	if(*this == t) {
307	2716668	return true;
308		}
309	10753	if(isSubtypeOf(NodeManager::currentNM()->realType())) {
310	9973	return t.isSubtypeOf(NodeManager::currentNM()->realType());
311		}
312	780	if (isFunction() && t.isFunction())
313		{
314		// comparable if they have a common type node
315	3	return !leastCommonTypeNode(*this, t).isNull();
316		}
317	777	return false;
318		}
319
320	28	TypeNode TypeNode::getTesterDomainType() const
321		{
322	28	Assert(isTester());
323	28	return (*this)[0];
324		}
325
326	4656	TypeNode TypeNode::getSequenceElementType() const
327		{
328	4656	Assert(isSequence());
329	4656	return (*this)[0];
330		}
331
332	348664	TypeNode TypeNode::getBaseType() const {
333	697328	TypeNode realt = NodeManager::currentNM()->realType();
334	348664	if (isSubtypeOf(realt)) {
335	115122	return realt;
336	233542	} else if (isParametricDatatype()) {
337	1654	std::vector<TypeNode> v;
338	1820	for(size_t i = 1; i < getNumChildren(); ++i) {
339	993	v.push_back((*this)[i].getBaseType());
340		}
341	827	return (*this)[0].getDType().getTypeNode().instantiateParametricDatatype(v);
342		}
343	232715	return *this;
344		}
345
346	8424	std::vector<TypeNode> TypeNode::getArgTypes() const {
347	8424	vector<TypeNode> args;
348	8424	if(isTester()) {
349		Assert(getNumChildren() == 1);
350		args.push_back((*this)[0]);
351		} else {
352	8424	Assert(isFunction() \|\| isConstructor() \|\| isSelector());
353	22654	for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
354	14230	args.push_back((*this)[i]);
355		}
356		}
357	8424	return args;
358		}
359
360	1461	std::vector<TypeNode> TypeNode::getParamTypes() const {
361	1461	vector<TypeNode> params;
362	1461	Assert(isParametricDatatype());
363	3282	for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
364	1821	params.push_back((*this)[i]);
365		}
366	1461	return params;
367		}
368
369	48297	bool TypeNode::isTuple() const
370		{
371	48297	return (getKind() == kind::DATATYPE_TYPE && getDType().isTuple());
372		}
373
374	4	bool TypeNode::isRecord() const
375		{
376	4	return (getKind() == kind::DATATYPE_TYPE && getDType().isRecord());
377		}
378
379	16282	size_t TypeNode::getTupleLength() const {
380	16282	Assert(isTuple());
381	16282	const DType& dt = getDType();
382	16282	Assert(dt.getNumConstructors() == 1);
383	16282	return dt[0].getNumArgs();
384		}
385
386	5660	vector<TypeNode> TypeNode::getTupleTypes() const {
387	5660	Assert(isTuple());
388	5660	const DType& dt = getDType();
389	5660	Assert(dt.getNumConstructors() == 1);
390	5660	vector<TypeNode> types;
391	17002	for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
392	11342	types.push_back(dt[0][i].getRangeType());
393		}
394	5660	return types;
395		}
396
397		/** Is this an instantiated datatype type */
398	1255	bool TypeNode::isInstantiatedDatatype() const {
399	1255	if(getKind() == kind::DATATYPE_TYPE) {
400	884	return true;
401		}
402	371	if(getKind() != kind::PARAMETRIC_DATATYPE) {
403		return false;
404		}
405	371	const DType& dt = (*this)[0].getDType();
406	371	unsigned n = dt.getNumParameters();
407	371	Assert(n < getNumChildren());
408	884	for(unsigned i = 0; i < n; ++i) {
409	513	if (dt.getParameter(i) == (*this)[i + 1])
410		{
411		return false;
412		}
413		}
414	371	return true;
415		}
416
417	1262	TypeNode TypeNode::instantiateParametricDatatype(
418		const std::vector<TypeNode>& params) const
419		{
420	1262	AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
421	1262	AssertArgument(params.size() == getNumChildren() - 1, *this);
422	1262	NodeManager* nm = NodeManager::currentNM();
423	2524	TypeNode cons = nm->mkTypeConst((*this)[0].getConst<DatatypeIndexConstant>());
424	2524	std::vector<TypeNode> paramsNodes;
425	1262	paramsNodes.push_back(cons);
426	2806	for (const TypeNode& t : params)
427		{
428	1544	paramsNodes.push_back(t);
429		}
430	2524	return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes);
431		}
432
433	50	uint64_t TypeNode::getSortConstructorArity() const
434		{
435	50	Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr()));
436	50	return getAttribute(expr::SortArityAttr());
437		}
438
439	4	std::string TypeNode::getName() const
440		{
441	4	Assert(isSort() \|\| isSortConstructor());
442	4	return getAttribute(expr::VarNameAttr());
443		}
444
445	46	TypeNode TypeNode::instantiateSortConstructor(
446		const std::vector<TypeNode>& params) const
447		{
448	46	Assert(isSortConstructor());
449	46	return NodeManager::currentNM()->mkSort(*this, params);
450		}
451
452		/** Is this an instantiated datatype parameter */
453	1648	bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
454	1648	AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
455	1648	const DType& dt = (*this)[0].getDType();
456	1648	AssertArgument(n < dt.getNumParameters(), *this);
457	1648	return dt.getParameter(n) != (*this)[n + 1];
458		}
459
460	3200076	TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
461	3200076	return commonTypeNode( t0, t1, true );
462		}
463
464	69608	TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
465	69608	return commonTypeNode( t0, t1, false );
466		}
467
468	3269710	TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
469	3269710	Assert(!t0.isNull());
470	3269710	Assert(!t1.isNull());
471
472	3269710	if(__builtin_expect( (t0 == t1), true )) {
473	3252249	return t0;
474		}
475
476		// t0 != t1 &&
477	17461	if(t0.getKind() == kind::TYPE_CONSTANT) {
478	17405	switch(t0.getConst<TypeConstant>()) {
479	3559	case INTEGER_TYPE:
480	3559	if(t1.isInteger()) {
481		// t0 == IntegerType && t1.isInteger()
482		return t0; //IntegerType
483	3559	} else if(t1.isReal()) {
484		// t0 == IntegerType && t1.isReal() && !t1.isInteger()
485	3527	return isLeast ? t1 : t0; // RealType
486		} else {
487	32	return TypeNode(); // null type
488		}
489	13786	case REAL_TYPE:
490	13786	if(t1.isReal()) {
491	13786	return isLeast ? t0 : t1; // RealType
492		} else {
493		return TypeNode(); // null type
494		}
495	60	default:
496	60	return TypeNode(); // null type
497		}
498	56	} else if(t1.getKind() == kind::TYPE_CONSTANT) {
499	22	return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
500		}
501
502		// t0 != t1 &&
503		// t0.getKind() == kind::TYPE_CONSTANT &&
504		// t1.getKind() == kind::TYPE_CONSTANT
505	34	switch(t0.getKind()) {
506	10	case kind::FUNCTION_TYPE:
507		{
508	10	if (t1.getKind() != kind::FUNCTION_TYPE)
509		{
510	4	return TypeNode();
511		}
512		// must have equal arguments
513	12	std::vector<TypeNode> t0a = t0.getArgTypes();
514	12	std::vector<TypeNode> t1a = t1.getArgTypes();
515	6	if (t0a.size() != t1a.size())
516		{
517		// different arities
518		return TypeNode();
519		}
520	10	for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++)
521		{
522	6	if (t0a[i] != t1a[i])
523		{
524		// an argument is different
525	2	return TypeNode();
526		}
527		}
528	8	TypeNode t0r = t0.getRangeType();
529	8	TypeNode t1r = t1.getRangeType();
530	8	TypeNode tr = commonTypeNode(t0r, t1r, isLeast);
531	8	std::vector<TypeNode> ftypes;
532	4	ftypes.insert(ftypes.end(), t0a.begin(), t0a.end());
533	4	ftypes.push_back(tr);
534	4	return NodeManager::currentNM()->mkFunctionType(ftypes);
535		}
536		break;
537	24	case kind::BITVECTOR_TYPE:
538		case kind::FLOATINGPOINT_TYPE:
539		case kind::SORT_TYPE:
540		case kind::CONSTRUCTOR_TYPE:
541		case kind::SELECTOR_TYPE:
542		case kind::TESTER_TYPE:
543		case kind::ARRAY_TYPE:
544		case kind::DATATYPE_TYPE:
545		case kind::PARAMETRIC_DATATYPE:
546		case kind::SEQUENCE_TYPE:
547		case kind::SET_TYPE:
548		case kind::BAG_TYPE:
549		{
550		// we don't support subtyping except for built in types Int and Real.
551	24	return TypeNode(); // return null type
552		}
553		default:
554		Unimplemented() << "don't have a commonType for types `" << t0
555		<< "' and `" << t1 << "'";
556		}
557		}
558
559		Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
560		TypeNode ntn = n.getType();
561		Assert(ntn.isComparableTo(tn));
562		if( !ntn.isSubtypeOf( tn ) ){
563		if( tn.isInteger() ){
564		if( tn.isSubtypeOf( ntn ) ){
565		return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
566		}
567		}else if( tn.isDatatype() && ntn.isDatatype() ){
568		if( tn.isTuple() && ntn.isTuple() ){
569		const DType& dt1 = tn.getDType();
570		const DType& dt2 = ntn.getDType();
571		NodeManager* nm = NodeManager::currentNM();
572		if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
573		std::vector< Node > conds;
574		for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
575		Node s = nm->mkNode(
576		kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n);
577		Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType());
578		if( etc.isNull() ){
579		return Node::null();
580		}else{
581		conds.push_back( etc );
582		}
583		}
584		if( conds.empty() ){
585		return nm->mkConst(true);
586		}else if( conds.size()==1 ){
587		return conds[0];
588		}else{
589		return nm->mkNode(kind::AND, conds);
590		}
591		}
592		}
593		}
594		return Node::null();
595		}else{
596		return NodeManager::currentNM()->mkConst( true );
597		}
598		}
599
600		/** Is this a sort kind */
601	1225658	bool TypeNode::isSort() const {
602	1225658	return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
603		}
604
605		/** Is this a sort constructor kind */
606	670	bool TypeNode::isSortConstructor() const {
607	670	return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
608		}
609
610	102934	bool TypeNode::isFloatingPoint() const
611		{
612	102934	return getKind() == kind::FLOATINGPOINT_TYPE;
613		}
614
615	5408659	bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; }
616
617	6271473	bool TypeNode::isDatatype() const
618		{
619	6271473	return getKind() == kind::DATATYPE_TYPE
620	6271473	\|\| getKind() == kind::PARAMETRIC_DATATYPE;
621		}
622
623	584491	bool TypeNode::isParametricDatatype() const
624		{
625	584491	return getKind() == kind::PARAMETRIC_DATATYPE;
626		}
627
628	6272941	bool TypeNode::isConstructor() const
629		{
630	6272941	return getKind() == kind::CONSTRUCTOR_TYPE;
631		}
632
633	1178914	bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; }
634
635	1738455	bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; }
636
637	61	bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; }
638
639	400228	bool TypeNode::isCodatatype() const
640		{
641	400228	if (isDatatype())
642		{
643	399348	return getDType().isCodatatype();
644		}
645	880	return false;
646		}
647
648	8542	bool TypeNode::isSygusDatatype() const
649		{
650	8542	if (isDatatype())
651		{
652	8070	return getDType().isSygus();
653		}
654	472	return false;
655		}
656
657	1940	std::string TypeNode::toString() const {
658	3880	std::stringstream ss;
659		Language outlang =
660	1940	(this == &s_null) ? Language::LANG_AUTO : options::outputLanguage();
661	1940	d_nv->toStream(ss, -1, 0, outlang);
662	3880	return ss.str();
663		}
664
665	3628311	const DType& TypeNode::getDType() const
666		{
667	3628311	if (getKind() == kind::DATATYPE_TYPE)
668		{
669	3624583	DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
670	3624583	return NodeManager::currentNM()->getDTypeForIndex(dic.getIndex());
671		}
672	3728	Assert(getKind() == kind::PARAMETRIC_DATATYPE);
673	3728	return (*this)[0].getDType();
674		}
675
676	32708	bool TypeNode::isBag() const
677		{
678	32708	return getKind() == kind::BAG_TYPE;
679		}
680
681	2353	TypeNode TypeNode::getBagElementType() const
682		{
683	2353	Assert(isBag());
684	2353	return (*this)[0];
685		}
686
687	1232	bool TypeNode::isBitVector(unsigned size) const
688		{
689	1232	return (getKind() == kind::BITVECTOR_TYPE
690	1232	&& getConst<BitVectorSize>() == size);
691		}
692
693	2637657	uint32_t TypeNode::getBitVectorSize() const
694		{
695	2637657	Assert(isBitVector());
696	2637657	return getConst<BitVectorSize>();
697		}
698
699		} // namespace cvc5
700
701		namespace std {
702
703	1863643	size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const
704		{
705	1863643	return tn.getId();
706		}
707
708	22746	} // namespace std