Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/theory_datatypes_type_rules.cpp	Lines:	217	279	77.8 %
Date:	2021-09-18	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/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);
}

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