Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/theory_datatypes_type_rules.cpp	Lines:	219	281	77.9 %
Date:	2021-11-07	Branches:	445	1360	32.7 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Typing and cardinality rules for the theory of datatypes.
 */

#include "theory/datatypes/theory_datatypes_type_rules.h"

#include <sstream>

#include "expr/ascription_type.h"
#include "expr/codatatype_bound_variable.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/type_matcher.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/datatypes/tuple_project_op.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace datatypes {

TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager,
                                                  TNode n,
                                                  bool check)
{
  Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
  TypeNode consType = n.getOperator().getType(check);
  TypeNode t = consType.getConstructorRangeType();
  Assert(t.isDatatype());
  TNode::iterator child_it = n.begin();
  TNode::iterator child_it_end = n.end();
  TypeNode::iterator tchild_it = consType.begin();
  if ((t.isParametricDatatype() || check)
      && n.getNumChildren() != consType.getNumChildren() - 1)
  {
    throw TypeCheckingExceptionPrivate(
        n, "number of arguments does not match the constructor type");
  }
  if (t.isParametricDatatype())
  {
    Debug("typecheck-idt") << "typecheck parameterized datatype " << n
                           << std::endl;
    TypeMatcher m(t);
    for (; child_it != child_it_end; ++child_it, ++tchild_it)
    {
      TypeNode childType = (*child_it).getType(check);
      if (!m.doMatching(*tchild_it, childType))
      {
        throw TypeCheckingExceptionPrivate(
            n, "matching failed for parameterized constructor");
      }
    }
    std::vector<TypeNode> instTypes;
    m.getMatches(instTypes);
    TypeNode range = t.instantiateParametricDatatype(instTypes);
    Debug("typecheck-idt") << "Return " << range << std::endl;
    return range;
  }
  else
  {
    if (check)
    {
      Debug("typecheck-idt")
          << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl;
      Debug("typecheck-idt") << "cons type: " << consType << " "
                             << consType.getNumChildren() << std::endl;
      for (; child_it != child_it_end; ++child_it, ++tchild_it)
      {
        TypeNode childType = (*child_it).getType(check);
        Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
                               << (*tchild_it) << std::endl;
        TypeNode argumentType = *tchild_it;
        if (!childType.isSubtypeOf(argumentType))
        {
          std::stringstream ss;
          ss << "bad type for constructor argument:\n"
             << "child type:  " << childType << "\n"
             << "not subtype: " << argumentType << "\n"
             << "in term : " << n;
          throw TypeCheckingExceptionPrivate(n, ss.str());
        }
      }
    }
    return consType.getConstructorRangeType();
  }
}

bool DatatypeConstructorTypeRule::computeIsConst(NodeManager* nodeManager,
                                                 TNode n)
{
  Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
  for (TNode::const_iterator i = n.begin(); i != n.end(); ++i)
  {
    if (!(*i).isConst())
    {
      return false;
    }
  }
  return true;
}

TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager,
                                               TNode n,
                                               bool check)
{
  Assert(n.getKind() == kind::APPLY_SELECTOR
         || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
  TypeNode selType = n.getOperator().getType(check);
  TypeNode t = selType[0];
  Assert(t.isDatatype());
  if ((t.isParametricDatatype() || check) && n.getNumChildren() != 1)
  {
    throw TypeCheckingExceptionPrivate(
        n, "number of arguments does not match the selector type");
  }
  if (t.isParametricDatatype())
  {
    Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl;
    TypeMatcher m(t);
    TypeNode childType = n[0].getType(check);
    if (!childType.isInstantiatedDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "Datatype type not fully instantiated");
    }
    if (!m.doMatching(selType[0], childType))
    {
      throw TypeCheckingExceptionPrivate(
          n, "matching failed for selector argument of parameterized datatype");
    }
    std::vector<TypeNode> types, matches;
    m.getTypes(types);
    m.getMatches(matches);
    TypeNode range = selType[1];
    range = range.substitute(
        types.begin(), types.end(), matches.begin(), matches.end());
    Debug("typecheck-idt") << "Return " << range << std::endl;
    return range;
  }
  else
  {
    if (check)
    {
      Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
      Debug("typecheck-idt") << "sel type: " << selType << std::endl;
      TypeNode childType = n[0].getType(check);
      if (!selType[0].isComparableTo(childType))
      {
        Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " "
                               << childType.getKind() << std::endl;
        throw TypeCheckingExceptionPrivate(n, "bad type for selector argument");
      }
    }
    return selType[1];
  }
}

TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  Assert(n.getKind() == kind::APPLY_TESTER);
  if (check)
  {
    if (n.getNumChildren() != 1)
    {
      throw TypeCheckingExceptionPrivate(
          n, "number of arguments does not match the tester type");
    }
    TypeNode testType = n.getOperator().getType(check);
    TypeNode childType = n[0].getType(check);
    TypeNode t = testType[0];
    Assert(t.isDatatype());
    if (t.isParametricDatatype())
    {
      Debug("typecheck-idt")
          << "typecheck parameterized tester: " << n << std::endl;
      TypeMatcher m(t);
      if (!m.doMatching(testType[0], childType))
      {
        throw TypeCheckingExceptionPrivate(
            n, "matching failed for tester argument of parameterized datatype");
      }
    }
    else
    {
      Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
      Debug("typecheck-idt") << "test type: " << testType << std::endl;
      if (!testType[0].isComparableTo(childType))
      {
        throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
      }
    }
  }
  return nodeManager->booleanType();
}

TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  Assert(n.getKind() == kind::APPLY_UPDATER);
  TypeNode updType = n.getOperator().getType(check);
  Assert(updType.getNumChildren() == 2);
  if (check)
  {
    for (size_t i = 0; i < 2; i++)
    {
      TypeNode childType = n[i].getType(check);
      TypeNode t = updType[i];
      if (t.isParametricDatatype())
      {
        Debug("typecheck-idt")
            << "typecheck parameterized update: " << n << std::endl;
        TypeMatcher m(t);
        if (!m.doMatching(t, childType))
        {
          throw TypeCheckingExceptionPrivate(
              n,
              "matching failed for update argument of parameterized datatype");
        }
      }
      else
      {
        Debug("typecheck-idt") << "typecheck update: " << n << std::endl;
        Debug("typecheck-idt") << "test type: " << updType << std::endl;
        if (!t.isComparableTo(childType))
        {
          throw TypeCheckingExceptionPrivate(n, "bad type for update argument");
        }
      }
    }
  }
  // type is the first argument
  return updType[0];
}

TypeNode DatatypeAscriptionTypeRule::computeType(NodeManager* nodeManager,
                                                 TNode n,
                                                 bool check)
{
  Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl;
  Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION);
  TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
  if (check)
  {
    TypeNode childType = n[0].getType(check);

    TypeMatcher m;
    if (childType.getKind() == kind::CONSTRUCTOR_TYPE)
    {
      m.addTypesFromDatatype(childType.getConstructorRangeType());
    }
    else if (childType.getKind() == kind::DATATYPE_TYPE)
    {
      m.addTypesFromDatatype(childType);
    }
    if (!m.doMatching(childType, t))
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "matching failed for type "
                                         "ascription argument of "
                                         "parameterized datatype");
    }
  }
  return t;
}

Cardinality ConstructorProperties::computeCardinality(TypeNode type)
{
  // Constructors aren't exactly functions, they're like
  // parameterized ground terms.  So the cardinality is more like
  // that of a tuple than that of a function.
  AssertArgument(type.isConstructor(), type);
  Cardinality c = 1;
  for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i)
  {
    c *= type[i].getCardinality();
  }
  return c;
}

TypeNode DtSizeTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting datatype size term to have datatype argument.");
    }
  }
  return nodeManager->integerType();
}

TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager,
                                      TNode n,
                                      bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting datatype bound term to have datatype argument.");
    }
    if (n[1].getKind() != kind::CONST_RATIONAL)
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "datatype bound must be a constant");
    }
    if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "datatype bound must be non-negative");
    }
  }
  return nodeManager->booleanType();
}

TypeNode DtSygusBoundTypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  if (check)
  {
    if (!n[0].getType().isDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "datatype sygus bound takes a datatype");
    }
    if (n[1].getKind() != kind::CONST_RATIONAL)
    {
      throw TypeCheckingExceptionPrivate(
          n, "datatype sygus bound must be a constant");
    }
    if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
    {
      throw TypeCheckingExceptionPrivate(
          n, "datatype sygus bound must be non-negative");
    }
  }
  return nodeManager->booleanType();
}

TypeNode DtSyguEvalTypeRule::computeType(NodeManager* nodeManager,
                                         TNode n,
                                         bool check)
{
  TypeNode headType = n[0].getType(check);
  if (!headType.isDatatype())
  {
    throw TypeCheckingExceptionPrivate(
        n, "datatype sygus eval takes a datatype head");
  }
  const DType& dt = headType.getDType();
  if (!dt.isSygus())
  {
    throw TypeCheckingExceptionPrivate(
        n, "datatype sygus eval must have a datatype head that is sygus");
  }
  if (check)
  {
    Node svl = dt.getSygusVarList();
    if (svl.getNumChildren() + 1 != n.getNumChildren())
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "wrong number of arguments to a "
                                         "datatype sygus evaluation "
                                         "function");
    }
    for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
    {
      TypeNode vtype = svl[i].getType(check);
      TypeNode atype = n[i + 1].getType(check);
      if (!vtype.isComparableTo(atype))
      {
        throw TypeCheckingExceptionPrivate(
            n,
            "argument type mismatch in a datatype sygus evaluation function");
      }
    }
  }
  return dt.getSygusType();
}

TypeNode MatchTypeRule::computeType(NodeManager* nodeManager,
                                    TNode n,
                                    bool check)
{
  Assert(n.getKind() == kind::MATCH);

  TypeNode retType;

  TypeNode headType = n[0].getType(check);
  if (!headType.isDatatype())
  {
    throw TypeCheckingExceptionPrivate(n, "expecting datatype head in match");
  }
  const DType& hdt = headType.getDType();

  std::unordered_set<unsigned> patIndices;
  bool patHasVariable = false;
  // the type of a match case list is the least common type of its cases
  for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++)
  {
    Node nc = n[i];
    if (check)
    {
      Kind nck = nc.getKind();
      std::unordered_set<Node> bvs;
      if (nck == kind::MATCH_BIND_CASE)
      {
        for (const Node& v : nc[0])
        {
          Assert(v.getKind() == kind::BOUND_VARIABLE);
          bvs.insert(v);
        }
      }
      else if (nck != kind::MATCH_CASE)
      {
        throw TypeCheckingExceptionPrivate(
            n, "expected a match case in match expression");
      }
      // get the pattern type
      unsigned pindex = nck == kind::MATCH_CASE ? 0 : 1;
      TypeNode patType = nc[pindex].getType();
      // should be caught in the above call
      if (!patType.isDatatype())
      {
        throw TypeCheckingExceptionPrivate(
            n, "expecting datatype pattern in match");
      }
      Kind ncpk = nc[pindex].getKind();
      if (ncpk == kind::APPLY_CONSTRUCTOR)
      {
        for (const Node& arg : nc[pindex])
        {
          if (bvs.find(arg) == bvs.end())
          {
            throw TypeCheckingExceptionPrivate(
                n,
                "expecting distinct bound variable as argument to "
                "constructor in pattern of match");
          }
          bvs.erase(arg);
        }
        unsigned ci = utils::indexOf(nc[pindex].getOperator());
        patIndices.insert(ci);
      }
      else if (ncpk == kind::BOUND_VARIABLE)
      {
        patHasVariable = true;
      }
      else
      {
        throw TypeCheckingExceptionPrivate(
            n, "unexpected kind of term in pattern in match");
      }
      const DType& pdt = patType.getDType();
      // compare datatypes instead of the types to catch parametric case,
      // where the pattern has parametric type.
      if (hdt.getTypeNode() != pdt.getTypeNode())
      {
        std::stringstream ss;
        ss << "pattern of a match case does not match the head type in match";
        throw TypeCheckingExceptionPrivate(n, ss.str());
      }
    }
    TypeNode currType = nc.getType(check);
    if (i == 1)
    {
      retType = currType;
    }
    else
    {
      retType = TypeNode::leastCommonTypeNode(retType, currType);
      if (retType.isNull())
      {
        throw TypeCheckingExceptionPrivate(
            n, "incomparable types in match case list");
      }
    }
  }
  if (check)
  {
    if (!patHasVariable && patIndices.size() < hdt.getNumConstructors())
    {
      throw TypeCheckingExceptionPrivate(
          n, "cases for match term are not exhaustive");
    }
  }
  return retType;
}

TypeNode MatchCaseTypeRule::computeType(NodeManager* nodeManager,
                                        TNode n,
                                        bool check)
{
  Assert(n.getKind() == kind::MATCH_CASE);
  if (check)
  {
    TypeNode patType = n[0].getType(check);
    if (!patType.isDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting datatype pattern in match case");
    }
  }
  return n[1].getType(check);
}

TypeNode MatchBindCaseTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  Assert(n.getKind() == kind::MATCH_BIND_CASE);
  if (check)
  {
    if (n[0].getKind() != kind::BOUND_VAR_LIST)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expected a bound variable list in match bind case");
    }
    TypeNode patType = n[1].getType(check);
    if (!patType.isDatatype())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting datatype pattern in match bind case");
    }
  }
  return n[2].getType(check);
}

TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check)
{
  Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator()
         && n.getOperator().getKind() == kind::TUPLE_PROJECT_OP);
  TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
  const std::vector<uint32_t>& indices = op.getIndices();
  if (check)
  {
    if (n.getNumChildren() != 1)
    {
      std::stringstream ss;
      ss << "operands in term " << n << " are " << n.getNumChildren()
         << ", but TUPLE_PROJECT expects 1 operand.";
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
    TypeNode tupleType = n[0].getType(check);
    if (!tupleType.isTuple())
    {
      std::stringstream ss;
      ss << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found"
         << tupleType;
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }

    // make sure all indices are less than the length of the tuple type
    DType dType = tupleType.getDType();
    DTypeConstructor constructor = dType[0];
    size_t numArgs = constructor.getNumArgs();
    for (uint32_t index : indices)
    {
      std::stringstream ss;
      if (index >= numArgs)
      {
        ss << "Project index " << index << " in term " << n
           << " is >= " << numArgs << " which is the length of tuple " << n[0]
           << std::endl;
        throw TypeCheckingExceptionPrivate(n, ss.str());
      }
    }
  }
  TypeNode tupleType = n[0].getType(check);
  std::vector<TypeNode> types;
  DType dType = tupleType.getDType();
  DTypeConstructor constructor = dType[0];
  for (uint32_t index : indices)
  {
    types.push_back(constructor.getArgType(index));
  }
  return nm->mkTupleType(types);
}

TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager,
                                                      TNode n,
                                                      bool check)
{
  return n.getConst<CodatatypeBoundVariable>().getType();
}

}  // namespace datatypes
}  // namespace theory
}  // namespace cvc5


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		* Typing and cardinality rules for the theory of datatypes.
14		*/
15
16		#include "theory/datatypes/theory_datatypes_type_rules.h"
17
18		#include <sstream>
19
20		#include "expr/ascription_type.h"
21		#include "expr/codatatype_bound_variable.h"
22		#include "expr/dtype.h"
23		#include "expr/dtype_cons.h"
24		#include "expr/type_matcher.h"
25		#include "theory/datatypes/theory_datatypes_utils.h"
26		#include "theory/datatypes/tuple_project_op.h"
27		#include "util/rational.h"
28
29		namespace cvc5 {
30		namespace theory {
31		namespace datatypes {
32
33	167482	TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager,
34		TNode n,
35		bool check)
36		{
37	167482	Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
38	334964	TypeNode consType = n.getOperator().getType(check);
39	334964	TypeNode t = consType.getConstructorRangeType();
40	167482	Assert(t.isDatatype());
41	167482	TNode::iterator child_it = n.begin();
42	167482	TNode::iterator child_it_end = n.end();
43	167482	TypeNode::iterator tchild_it = consType.begin();
44	502086	if ((t.isParametricDatatype() \|\| check)
45	334964	&& n.getNumChildren() != consType.getNumChildren() - 1)
46		{
47		throw TypeCheckingExceptionPrivate(
48	6	n, "number of arguments does not match the constructor type");
49		}
50	167476	if (t.isParametricDatatype())
51		{
52	712	Debug("typecheck-idt") << "typecheck parameterized datatype " << n
53	356	<< std::endl;
54	712	TypeMatcher m(t);
55	1428	for (; child_it != child_it_end; ++child_it, ++tchild_it)
56		{
57	1072	TypeNode childType = (*child_it).getType(check);
58	536	if (!m.doMatching(*tchild_it, childType))
59		{
60		throw TypeCheckingExceptionPrivate(
61		n, "matching failed for parameterized constructor");
62		}
63		}
64	712	std::vector<TypeNode> instTypes;
65	356	m.getMatches(instTypes);
66	712	TypeNode range = t.instantiateParametricDatatype(instTypes);
67	356	Debug("typecheck-idt") << "Return " << range << std::endl;
68	356	return range;
69		}
70		else
71		{
72	167120	if (check)
73		{
74	334240	Debug("typecheck-idt")
75	167120	<< "typecheck cons: " << n << " " << n.getNumChildren() << std::endl;
76	334240	Debug("typecheck-idt") << "cons type: " << consType << " "
77	167120	<< consType.getNumChildren() << std::endl;
78	805848	for (; child_it != child_it_end; ++child_it, ++tchild_it)
79		{
80	638728	TypeNode childType = (*child_it).getType(check);
81	638728	Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
82	319364	<< (*tchild_it) << std::endl;
83	638728	TypeNode argumentType = *tchild_it;
84	319364	if (!childType.isSubtypeOf(argumentType))
85		{
86		std::stringstream ss;
87		ss << "bad type for constructor argument:\n"
88		<< "child type: " << childType << "\n"
89		<< "not subtype: " << argumentType << "\n"
90		<< "in term : " << n;
91		throw TypeCheckingExceptionPrivate(n, ss.str());
92		}
93		}
94		}
95	167120	return consType.getConstructorRangeType();
96		}
97		}
98
99	97230	bool DatatypeConstructorTypeRule::computeIsConst(NodeManager* nodeManager,
100		TNode n)
101		{
102	97230	Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
103	183496	for (TNode::const_iterator i = n.begin(); i != n.end(); ++i)
104		{
105	143835	if (!(*i).isConst())
106		{
107	57569	return false;
108		}
109		}
110	39661	return true;
111		}
112
113	74428	TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager,
114		TNode n,
115		bool check)
116		{
117	74428	Assert(n.getKind() == kind::APPLY_SELECTOR
118		\|\| n.getKind() == kind::APPLY_SELECTOR_TOTAL);
119	148856	TypeNode selType = n.getOperator().getType(check);
120	148856	TypeNode t = selType[0];
121	74428	Assert(t.isDatatype());
122	74428	if ((t.isParametricDatatype() \|\| check) && n.getNumChildren() != 1)
123		{
124		throw TypeCheckingExceptionPrivate(
125		n, "number of arguments does not match the selector type");
126		}
127	74428	if (t.isParametricDatatype())
128		{
129	541	Debug("typecheck-idt") << "typecheck parameterized sel: " << n << std::endl;
130	1082	TypeMatcher m(t);
131	1082	TypeNode childType = n[0].getType(check);
132	541	if (!childType.isInstantiatedDatatype())
133		{
134		throw TypeCheckingExceptionPrivate(
135		n, "Datatype type not fully instantiated");
136		}
137	541	if (!m.doMatching(selType[0], childType))
138		{
139		throw TypeCheckingExceptionPrivate(
140		n, "matching failed for selector argument of parameterized datatype");
141		}
142	1082	std::vector<TypeNode> types, matches;
143	541	m.getTypes(types);
144	541	m.getMatches(matches);
145	1082	TypeNode range = selType[1];
146	541	range = range.substitute(
147		types.begin(), types.end(), matches.begin(), matches.end());
148	541	Debug("typecheck-idt") << "Return " << range << std::endl;
149	541	return range;
150		}
151		else
152		{
153	73887	if (check)
154		{
155	73887	Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
156	73887	Debug("typecheck-idt") << "sel type: " << selType << std::endl;
157	147774	TypeNode childType = n[0].getType(check);
158	73887	if (!selType[0].isComparableTo(childType))
159		{
160		Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " "
161		<< childType.getKind() << std::endl;
162		throw TypeCheckingExceptionPrivate(n, "bad type for selector argument");
163		}
164		}
165	73887	return selType[1];
166		}
167		}
168
169	36262	TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager,
170		TNode n,
171		bool check)
172		{
173	36262	Assert(n.getKind() == kind::APPLY_TESTER);
174	36262	if (check)
175		{
176	36262	if (n.getNumChildren() != 1)
177		{
178		throw TypeCheckingExceptionPrivate(
179		n, "number of arguments does not match the tester type");
180		}
181	72524	TypeNode testType = n.getOperator().getType(check);
182	72524	TypeNode childType = n[0].getType(check);
183	72524	TypeNode t = testType[0];
184	36262	Assert(t.isDatatype());
185	36262	if (t.isParametricDatatype())
186		{
187	252	Debug("typecheck-idt")
188	126	<< "typecheck parameterized tester: " << n << std::endl;
189	252	TypeMatcher m(t);
190	126	if (!m.doMatching(testType[0], childType))
191		{
192		throw TypeCheckingExceptionPrivate(
193		n, "matching failed for tester argument of parameterized datatype");
194		}
195		}
196		else
197		{
198	36136	Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
199	36136	Debug("typecheck-idt") << "test type: " << testType << std::endl;
200	36136	if (!testType[0].isComparableTo(childType))
201		{
202		throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
203		}
204		}
205		}
206	36262	return nodeManager->booleanType();
207		}
208
209	49	TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
210		TNode n,
211		bool check)
212		{
213	49	Assert(n.getKind() == kind::APPLY_UPDATER);
214	98	TypeNode updType = n.getOperator().getType(check);
215	49	Assert(updType.getNumChildren() == 2);
216	49	if (check)
217		{
218	145	for (size_t i = 0; i < 2; i++)
219		{
220	196	TypeNode childType = n[i].getType(check);
221	196	TypeNode t = updType[i];
222	98	if (t.isParametricDatatype())
223		{
224		Debug("typecheck-idt")
225		<< "typecheck parameterized update: " << n << std::endl;
226		TypeMatcher m(t);
227		if (!m.doMatching(t, childType))
228		{
229		throw TypeCheckingExceptionPrivate(
230		n,
231		"matching failed for update argument of parameterized datatype");
232		}
233		}
234		else
235		{
236	98	Debug("typecheck-idt") << "typecheck update: " << n << std::endl;
237	98	Debug("typecheck-idt") << "test type: " << updType << std::endl;
238	98	if (!t.isComparableTo(childType))
239		{
240	2	throw TypeCheckingExceptionPrivate(n, "bad type for update argument");
241		}
242		}
243		}
244		}
245		// type is the first argument
246	94	return updType[0];
247		}
248
249	110	TypeNode DatatypeAscriptionTypeRule::computeType(NodeManager* nodeManager,
250		TNode n,
251		bool check)
252		{
253	110	Debug("typecheck-idt") << "typechecking ascription: " << n << std::endl;
254	110	Assert(n.getKind() == kind::APPLY_TYPE_ASCRIPTION);
255	110	TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
256	110	if (check)
257		{
258	220	TypeNode childType = n[0].getType(check);
259
260	220	TypeMatcher m;
261	110	if (childType.getKind() == kind::CONSTRUCTOR_TYPE)
262		{
263	102	m.addTypesFromDatatype(childType.getConstructorRangeType());
264		}
265	8	else if (childType.getKind() == kind::DATATYPE_TYPE)
266		{
267		m.addTypesFromDatatype(childType);
268		}
269	110	if (!m.doMatching(childType, t))
270		{
271		throw TypeCheckingExceptionPrivate(n,
272		"matching failed for type "
273		"ascription argument of "
274		"parameterized datatype");
275		}
276		}
277	110	return t;
278		}
279
280	2	Cardinality ConstructorProperties::computeCardinality(TypeNode type)
281		{
282		// Constructors aren't exactly functions, they're like
283		// parameterized ground terms. So the cardinality is more like
284		// that of a tuple than that of a function.
285	2	AssertArgument(type.isConstructor(), type);
286	2	Cardinality c = 1;
287	2	for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i)
288		{
289		c *= type[i].getCardinality();
290		}
291	2	return c;
292		}
293
294	22171	TypeNode DtSizeTypeRule::computeType(NodeManager* nodeManager,
295		TNode n,
296		bool check)
297		{
298	22171	if (check)
299		{
300	44342	TypeNode t = n[0].getType(check);
301	22171	if (!t.isDatatype())
302		{
303		throw TypeCheckingExceptionPrivate(
304		n, "expecting datatype size term to have datatype argument.");
305		}
306		}
307	22171	return nodeManager->integerType();
308		}
309
310		TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager,
311		TNode n,
312		bool check)
313		{
314		if (check)
315		{
316		TypeNode t = n[0].getType(check);
317		if (!t.isDatatype())
318		{
319		throw TypeCheckingExceptionPrivate(
320		n, "expecting datatype bound term to have datatype argument.");
321		}
322		if (n[1].getKind() != kind::CONST_RATIONAL)
323		{
324		throw TypeCheckingExceptionPrivate(n,
325		"datatype bound must be a constant");
326		}
327		if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
328		{
329		throw TypeCheckingExceptionPrivate(n,
330		"datatype bound must be non-negative");
331		}
332		}
333		return nodeManager->booleanType();
334		}
335
336	829	TypeNode DtSygusBoundTypeRule::computeType(NodeManager* nodeManager,
337		TNode n,
338		bool check)
339		{
340	829	if (check)
341		{
342	829	if (!n[0].getType().isDatatype())
343		{
344		throw TypeCheckingExceptionPrivate(
345		n, "datatype sygus bound takes a datatype");
346		}
347	829	if (n[1].getKind() != kind::CONST_RATIONAL)
348		{
349		throw TypeCheckingExceptionPrivate(
350		n, "datatype sygus bound must be a constant");
351		}
352	829	if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
353		{
354		throw TypeCheckingExceptionPrivate(
355		n, "datatype sygus bound must be non-negative");
356		}
357		}
358	829	return nodeManager->booleanType();
359		}
360
361	106526	TypeNode DtSyguEvalTypeRule::computeType(NodeManager* nodeManager,
362		TNode n,
363		bool check)
364		{
365	213052	TypeNode headType = n[0].getType(check);
366	106526	if (!headType.isDatatype())
367		{
368		throw TypeCheckingExceptionPrivate(
369		n, "datatype sygus eval takes a datatype head");
370		}
371	106526	const DType& dt = headType.getDType();
372	106526	if (!dt.isSygus())
373		{
374		throw TypeCheckingExceptionPrivate(
375		n, "datatype sygus eval must have a datatype head that is sygus");
376		}
377	106526	if (check)
378		{
379	213052	Node svl = dt.getSygusVarList();
380	106526	if (svl.getNumChildren() + 1 != n.getNumChildren())
381		{
382		throw TypeCheckingExceptionPrivate(n,
383		"wrong number of arguments to a "
384		"datatype sygus evaluation "
385		"function");
386		}
387	449626	for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++)
388		{
389	686200	TypeNode vtype = svl[i].getType(check);
390	686200	TypeNode atype = n[i + 1].getType(check);
391	343100	if (!vtype.isComparableTo(atype))
392		{
393		throw TypeCheckingExceptionPrivate(
394		n,
395		"argument type mismatch in a datatype sygus evaluation function");
396		}
397		}
398		}
399	213052	return dt.getSygusType();
400		}
401
402	20	TypeNode MatchTypeRule::computeType(NodeManager* nodeManager,
403		TNode n,
404		bool check)
405		{
406	20	Assert(n.getKind() == kind::MATCH);
407
408	20	TypeNode retType;
409
410	40	TypeNode headType = n[0].getType(check);
411	20	if (!headType.isDatatype())
412		{
413		throw TypeCheckingExceptionPrivate(n, "expecting datatype head in match");
414		}
415	20	const DType& hdt = headType.getDType();
416
417	40	std::unordered_set<unsigned> patIndices;
418	20	bool patHasVariable = false;
419		// the type of a match case list is the least common type of its cases
420	71	for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++)
421		{
422	102	Node nc = n[i];
423	51	if (check)
424		{
425	51	Kind nck = nc.getKind();
426	102	std::unordered_set<Node> bvs;
427	51	if (nck == kind::MATCH_BIND_CASE)
428		{
429	48	for (const Node& v : nc[0])
430		{
431	31	Assert(v.getKind() == kind::BOUND_VARIABLE);
432	31	bvs.insert(v);
433		}
434		}
435	34	else if (nck != kind::MATCH_CASE)
436		{
437		throw TypeCheckingExceptionPrivate(
438		n, "expected a match case in match expression");
439		}
440		// get the pattern type
441	51	unsigned pindex = nck == kind::MATCH_CASE ? 0 : 1;
442	102	TypeNode patType = nc[pindex].getType();
443		// should be caught in the above call
444	51	if (!patType.isDatatype())
445		{
446		throw TypeCheckingExceptionPrivate(
447		n, "expecting datatype pattern in match");
448		}
449	51	Kind ncpk = nc[pindex].getKind();
450	51	if (ncpk == kind::APPLY_CONSTRUCTOR)
451		{
452	76	for (const Node& arg : nc[pindex])
453		{
454	28	if (bvs.find(arg) == bvs.end())
455		{
456		throw TypeCheckingExceptionPrivate(
457		n,
458		"expecting distinct bound variable as argument to "
459		"constructor in pattern of match");
460		}
461	28	bvs.erase(arg);
462		}
463	48	unsigned ci = utils::indexOf(nc[pindex].getOperator());
464	48	patIndices.insert(ci);
465		}
466	3	else if (ncpk == kind::BOUND_VARIABLE)
467		{
468	3	patHasVariable = true;
469		}
470		else
471		{
472		throw TypeCheckingExceptionPrivate(
473		n, "unexpected kind of term in pattern in match");
474		}
475	51	const DType& pdt = patType.getDType();
476		// compare datatypes instead of the types to catch parametric case,
477		// where the pattern has parametric type.
478	51	if (hdt.getTypeNode() != pdt.getTypeNode())
479		{
480		std::stringstream ss;
481		ss << "pattern of a match case does not match the head type in match";
482		throw TypeCheckingExceptionPrivate(n, ss.str());
483		}
484		}
485	102	TypeNode currType = nc.getType(check);
486	51	if (i == 1)
487		{
488	20	retType = currType;
489		}
490		else
491		{
492	31	retType = TypeNode::leastCommonTypeNode(retType, currType);
493	31	if (retType.isNull())
494		{
495		throw TypeCheckingExceptionPrivate(
496		n, "incomparable types in match case list");
497		}
498		}
499		}
500	20	if (check)
501		{
502	20	if (!patHasVariable && patIndices.size() < hdt.getNumConstructors())
503		{
504		throw TypeCheckingExceptionPrivate(
505		n, "cases for match term are not exhaustive");
506		}
507		}
508	40	return retType;
509		}
510
511	34	TypeNode MatchCaseTypeRule::computeType(NodeManager* nodeManager,
512		TNode n,
513		bool check)
514		{
515	34	Assert(n.getKind() == kind::MATCH_CASE);
516	34	if (check)
517		{
518	68	TypeNode patType = n[0].getType(check);
519	34	if (!patType.isDatatype())
520		{
521		throw TypeCheckingExceptionPrivate(
522		n, "expecting datatype pattern in match case");
523		}
524		}
525	34	return n[1].getType(check);
526		}
527
528	15	TypeNode MatchBindCaseTypeRule::computeType(NodeManager* nodeManager,
529		TNode n,
530		bool check)
531		{
532	15	Assert(n.getKind() == kind::MATCH_BIND_CASE);
533	15	if (check)
534		{
535	15	if (n[0].getKind() != kind::BOUND_VAR_LIST)
536		{
537		throw TypeCheckingExceptionPrivate(
538		n, "expected a bound variable list in match bind case");
539		}
540	30	TypeNode patType = n[1].getType(check);
541	15	if (!patType.isDatatype())
542		{
543		throw TypeCheckingExceptionPrivate(
544		n, "expecting datatype pattern in match bind case");
545		}
546		}
547	15	return n[2].getType(check);
548		}
549
550	20	TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check)
551		{
552	20	Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator()
553		&& n.getOperator().getKind() == kind::TUPLE_PROJECT_OP);
554	40	TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
555	20	const std::vector<uint32_t>& indices = op.getIndices();
556	20	if (check)
557		{
558	20	if (n.getNumChildren() != 1)
559		{
560		std::stringstream ss;
561		ss << "operands in term " << n << " are " << n.getNumChildren()
562		<< ", but TUPLE_PROJECT expects 1 operand.";
563		throw TypeCheckingExceptionPrivate(n, ss.str());
564		}
565	40	TypeNode tupleType = n[0].getType(check);
566	20	if (!tupleType.isTuple())
567		{
568		std::stringstream ss;
569		ss << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found"
570		<< tupleType;
571		throw TypeCheckingExceptionPrivate(n, ss.str());
572		}
573
574		// make sure all indices are less than the length of the tuple type
575	40	DType dType = tupleType.getDType();
576	40	DTypeConstructor constructor = dType[0];
577	20	size_t numArgs = constructor.getNumArgs();
578	60	for (uint32_t index : indices)
579		{
580	88	std::stringstream ss;
581	44	if (index >= numArgs)
582		{
583	8	ss << "Project index " << index << " in term " << n
584	8	<< " is >= " << numArgs << " which is the length of tuple " << n[0]
585	4	<< std::endl;
586	4	throw TypeCheckingExceptionPrivate(n, ss.str());
587		}
588		}
589		}
590	32	TypeNode tupleType = n[0].getType(check);
591	32	std::vector<TypeNode> types;
592	32	DType dType = tupleType.getDType();
593	32	DTypeConstructor constructor = dType[0];
594	54	for (uint32_t index : indices)
595		{
596	38	types.push_back(constructor.getArgType(index));
597		}
598	32	return nm->mkTupleType(types);
599		}
600
601	326	TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager,
602		TNode n,
603		bool check)
604		{
605	326	return n.getConst<CodatatypeBoundVariable>().getType();
606		}
607
608		} // namespace datatypes
609		} // namespace theory
610	31137	} // namespace cvc5