Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/theory_datatypes_type_rules.cpp	Lines:	218	280	77.9 %
Date:	2021-05-22	Branches:	447	1366	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/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/type_matcher.h"
#include "theory/datatypes/theory_datatypes_utils.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);
  NodeManagerScope nms(nodeManager);
  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);
}

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