src/expr/type_node.cpp

   1 /*********************                                                        */
   2 /*! \file type_node.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Kshitij Bansal
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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.\endverbatim
  11  **
  12  ** \brief Reference-counted encapsulation of a pointer to node information.
  13  **
  14  ** Reference-counted encapsulation of a pointer to node information.
  15  **/
  16 #include "expr/type_node.h"
  17
  18 #include <vector>
  19
  20 #include "expr/node_manager_attributes.h"
  21 #include "expr/type_properties.h"
  22 #include "options/base_options.h"
  23 #include "options/expr_options.h"
  24 #include "options/quantifiers_options.h"
  25 #include "options/uf_options.h"
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30
  31 TypeNode TypeNode::s_null( &expr::NodeValue::null() );
  32
  33 TypeNode TypeNode::substitute(const TypeNode& type,
  34                               const TypeNode& replacement,
  35                               std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
  36   // in cache?
  37   std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
  38   if(i != cache.end()) {
  39     return (*i).second;
  40   }
  41
  42   // otherwise compute
  43   NodeBuilder<> nb(getKind());
  44   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
  45     // push the operator
  46     nb << TypeNode(d_nv->d_children[0]);
  47   }
  48   for(TypeNode::const_iterator i = begin(),
  49         iend = end();
  50       i != iend;
  51       ++i) {
  52     if(*i == type) {
  53       nb << replacement;
  54     } else {
  55       (*i).substitute(type, replacement);
  56     }
  57   }
  58
  59   // put in cache
  60   TypeNode tn = nb.constructTypeNode();
  61   cache[*this] = tn;
  62   return tn;
  63 }
  64
  65 Cardinality TypeNode::getCardinality() const {
  66   return kind::getCardinality(*this);
  67 }
  68
  69 bool TypeNode::isInterpretedFinite() const {
  70   if( getCardinality().isFinite() ){
  71     return true;
  72   }else{
  73     if( options::finiteModelFind() ){
  74       if( isSort() ){
  75         return true;
  76       }else if( isDatatype() ){
  77         TypeNode tn = *this;
  78         const Datatype& dt = getDatatype();
  79         return dt.isInterpretedFinite( tn.toType() );
  80       }else if( isArray() ){
  81         return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
  82       }else if( isSet() ) {
  83         return getSetElementType().isInterpretedFinite();
  84       }
  85       else if (isFunction())
  86       {
  87         if (!getRangeType().isInterpretedFinite())
  88         {
  89           return false;
  90         }
  91         std::vector<TypeNode> argTypes = getArgTypes();
  92         for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
  93         {
  94           if (!argTypes[i].isInterpretedFinite())
  95           {
  96             return false;
  97           }
  98         }
  99         return true;
 100       }
 101     }
 102     return false;
 103   }
 104 }
 105
 106 bool TypeNode::isFirstClass() const {
 107   return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) &&
 108          getKind() != kind::CONSTRUCTOR_TYPE &&
 109          getKind() != kind::SELECTOR_TYPE &&
 110          getKind() != kind::TESTER_TYPE &&
 111          getKind() != kind::SEXPR_TYPE &&
 112          ( getKind() != kind::TYPE_CONSTANT ||
 113            getConst<TypeConstant>() != REGEXP_TYPE );
 114 }
 115
 116 bool TypeNode::isWellFounded() const {
 117   return kind::isWellFounded(*this);
 118 }
 119
 120 Node TypeNode::mkGroundTerm() const {
 121   return kind::mkGroundTerm(*this);
 122 }
 123
 124 bool TypeNode::isSubtypeOf(TypeNode t) const {
 125   if(*this == t) {
 126     return true;
 127   }
 128   if(getKind() == kind::TYPE_CONSTANT) {
 129     switch(getConst<TypeConstant>()) {
 130     case INTEGER_TYPE:
 131       return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
 132     default:
 133       return false;
 134     }
 135   }
 136   if(isSet() && t.isSet()) {
 137     return getSetElementType().isSubtypeOf(t.getSetElementType());
 138   }
 139   // this should only return true for types T1, T2 where we handle equalities between T1 and T2
 140   // (more cases go here, if we want to support such cases)
 141   return false;
 142 }
 143
 144 bool TypeNode::isComparableTo(TypeNode t) const {
 145   if(*this == t) {
 146     return true;
 147   }
 148   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
 149     return t.isSubtypeOf(NodeManager::currentNM()->realType());
 150   }
 151   if(isSet() && t.isSet()) {
 152     return getSetElementType().isComparableTo(t.getSetElementType());
 153   }
 154   return false;
 155 }
 156
 157 TypeNode TypeNode::getBaseType() const {
 158   TypeNode realt = NodeManager::currentNM()->realType();
 159   if (isSubtypeOf(realt)) {
 160     return realt;
 161   } else if (isParametricDatatype()) {
 162     vector<Type> v;
 163     for(size_t i = 1; i < getNumChildren(); ++i) {
 164       v.push_back((*this)[i].getBaseType().toType());
 165     }
 166     TypeNode tn = TypeNode::fromType((*this)[0].getDatatype().getDatatypeType(v));
 167     return tn;
 168   }
 169   return *this;
 170 }
 171
 172 std::vector<TypeNode> TypeNode::getArgTypes() const {
 173   vector<TypeNode> args;
 174   if(isTester()) {
 175     Assert(getNumChildren() == 1);
 176     args.push_back((*this)[0]);
 177   } else {
 178     Assert(isFunction() || isConstructor() || isSelector());
 179     for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
 180       args.push_back((*this)[i]);
 181     }
 182   }
 183   return args;
 184 }
 185
 186 std::vector<TypeNode> TypeNode::getParamTypes() const {
 187   vector<TypeNode> params;
 188   Assert(isParametricDatatype());
 189   for(unsigned i = 1, i_end = getNumChildren(); i < i_end; ++i) {
 190     params.push_back((*this)[i]);
 191   }
 192   return params;
 193 }
 194
 195
 196 /** Is this a tuple type? */
 197 bool TypeNode::isTuple() const {
 198   return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() );
 199 }
 200
 201 /** Is this a record type? */
 202 bool TypeNode::isRecord() const {
 203   return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() );
 204 }
 205
 206 size_t TypeNode::getTupleLength() const {
 207   Assert(isTuple());
 208   const Datatype& dt = getDatatype();
 209   Assert(dt.getNumConstructors()==1);
 210   return dt[0].getNumArgs();
 211 }
 212
 213 vector<TypeNode> TypeNode::getTupleTypes() const {
 214   Assert(isTuple());
 215   const Datatype& dt = getDatatype();
 216   Assert(dt.getNumConstructors()==1);
 217   vector<TypeNode> types;
 218   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
 219     types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
 220   }
 221   return types;
 222 }
 223
 224 const Record& TypeNode::getRecord() const {
 225   Assert(isRecord());
 226   const Datatype & dt = getDatatype();
 227   return *(dt.getRecord());
 228   //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
 229 }
 230
 231 vector<TypeNode> TypeNode::getSExprTypes() const {
 232   Assert(isSExpr());
 233   vector<TypeNode> types;
 234   for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
 235     types.push_back((*this)[i]);
 236   }
 237   return types;
 238 }
 239
 240 /** Is this an instantiated datatype type */
 241 bool TypeNode::isInstantiatedDatatype() const {
 242   if(getKind() == kind::DATATYPE_TYPE) {
 243     return true;
 244   }
 245   if(getKind() != kind::PARAMETRIC_DATATYPE) {
 246     return false;
 247   }
 248   const Datatype& dt = (*this)[0].getDatatype();
 249   unsigned n = dt.getNumParameters();
 250   Assert(n < getNumChildren());
 251   for(unsigned i = 0; i < n; ++i) {
 252     if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) {
 253       return false;
 254     }
 255   }
 256   return true;
 257 }
 258
 259 /** Is this an instantiated datatype parameter */
 260 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
 261   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
 262   const Datatype& dt = (*this)[0].getDatatype();
 263   AssertArgument(n < dt.getNumParameters(), *this);
 264   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 265 }
 266
 267 TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
 268   return commonTypeNode( t0, t1, true );
 269 }
 270
 271 TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
 272   return commonTypeNode( t0, t1, false );
 273 }
 274
 275 TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
 276   Assert( NodeManager::currentNM() != NULL,
 277           "There is no current CVC4::NodeManager associated to this thread.\n"
 278           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 279
 280   Assert(!t0.isNull());
 281   Assert(!t1.isNull());
 282
 283   if(__builtin_expect( (t0 == t1), true )) {
 284     return t0;
 285   }
 286
 287   // t0 != t1 &&
 288   if(t0.getKind() == kind::TYPE_CONSTANT) {
 289     switch(t0.getConst<TypeConstant>()) {
 290     case INTEGER_TYPE:
 291       if(t1.isInteger()) {
 292         // t0 == IntegerType && t1.isInteger()
 293         return t0; //IntegerType
 294       } else if(t1.isReal()) {
 295         // t0 == IntegerType && t1.isReal() && !t1.isInteger()
 296         return isLeast ? t1 : t0; // RealType
 297       } else {
 298         return TypeNode(); // null type
 299       }
 300     case REAL_TYPE:
 301       if(t1.isReal()) {
 302         return isLeast ? t0 : t1; // RealType
 303       } else {
 304         return TypeNode(); // null type
 305       }
 306     default:
 307       return TypeNode(); // null type
 308     }
 309   } else if(t1.getKind() == kind::TYPE_CONSTANT) {
 310     return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
 311   }
 312
 313   // t0 != t1 &&
 314   // t0.getKind() == kind::TYPE_CONSTANT &&
 315   // t1.getKind() == kind::TYPE_CONSTANT
 316   switch(t0.getKind()) {
 317   case kind::BITVECTOR_TYPE:
 318   case kind::SORT_TYPE:
 319   case kind::CONSTRUCTOR_TYPE:
 320   case kind::SELECTOR_TYPE:
 321   case kind::TESTER_TYPE:
 322   case kind::FUNCTION_TYPE:
 323   case kind::ARRAY_TYPE:
 324   case kind::DATATYPE_TYPE:
 325   case kind::PARAMETRIC_DATATYPE:
 326     return TypeNode();
 327   case kind::SET_TYPE: {
 328     // take the least common subtype of element types
 329     TypeNode elementType;
 330     if(t1.isSet() && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull() ) {
 331       return NodeManager::currentNM()->mkSetType(elementType);
 332     } else {
 333       return TypeNode();
 334     }
 335   }
 336   case kind::SEXPR_TYPE:
 337     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
 338   default:
 339     Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
 340   }
 341 }
 342
 343 Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
 344   TypeNode ntn = n.getType();
 345   Assert( ntn.isComparableTo( tn ) );
 346   if( !ntn.isSubtypeOf( tn ) ){
 347     if( tn.isInteger() ){
 348       if( tn.isSubtypeOf( ntn ) ){
 349         return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n );
 350       }
 351     }else if( tn.isDatatype() && ntn.isDatatype() ){
 352       if( tn.isTuple() && ntn.isTuple() ){
 353         const Datatype& dt1 = tn.getDatatype();
 354         const Datatype& dt2 = ntn.getDatatype();
 355         if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
 356           std::vector< Node > conds;
 357           for( unsigned i=0; i<dt2[0].getNumArgs(); i++ ){
 358             Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt2[0][i].getSelector() ), n );
 359             Node etc = getEnsureTypeCondition( s, TypeNode::fromType( dt1[0][i].getRangeType() ) );
 360             if( etc.isNull() ){
 361               return Node::null();
 362             }else{
 363               conds.push_back( etc );
 364             }
 365           }
 366           if( conds.empty() ){
 367             return NodeManager::currentNM()->mkConst( true );
 368           }else if( conds.size()==1 ){
 369             return conds[0];
 370           }else{
 371             return NodeManager::currentNM()->mkNode( kind::AND, conds );
 372           }
 373         }
 374       }
 375     }
 376     return Node::null();
 377   }else{
 378     return NodeManager::currentNM()->mkConst( true );
 379   }
 380 }
 381
 382 /** Is this a sort kind */
 383 bool TypeNode::isSort() const {
 384   return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
 385 }
 386
 387 /** Is this a sort constructor kind */
 388 bool TypeNode::isSortConstructor() const {
 389   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 390 }
 391
 392 std::string TypeNode::toString() const {
 393   std::stringstream ss;
 394   OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
 395   d_nv->toStream(ss, -1, false, 0, outlang);
 396   return ss.str();
 397 }
 398
 399
 400 }/* CVC4 namespace */