Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/dtype_cons.cpp	Lines:	318	337	94.4 %
Date:	2021-09-29	Branches:	504	1296	38.9 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * A class representing a datatype definition.
 */
#include "expr/dtype_cons.h"

#include "expr/ascription_type.h"
#include "expr/dtype.h"
#include "expr/node_manager.h"
#include "expr/skolem_manager.h"
#include "expr/type_matcher.h"
#include "options/datatypes_options.h"

using namespace cvc5::kind;
using namespace cvc5::theory;

namespace cvc5 {

DTypeConstructor::DTypeConstructor(std::string name,
                                   unsigned weight)
    :  // We don't want to introduce a new data member, because eventually
       // we're going to be a constant stuffed inside a node.  So we stow
       // the tester name away inside the constructor name until
       // resolution.
      d_name(name),
      d_tester(),
      d_args(),
      d_weight(weight)
{
  Assert(name != "");
}

void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
{
  // We don't want to introduce a new data member, because eventually
  // we're going to be a constant stuffed inside a node.  So we stow
  // the selector type away inside a var until resolution (when we can
  // create the proper selector type)
  Assert(!isResolved());
  Assert(!selectorType.isNull());
  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
  Node sel = sm->mkDummySkolem(
      "unresolved_" + selectorName,
      selectorType,
      "is an unresolved selector type placeholder",
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
  // can use null updater for now
  Node nullNode;
  Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl;
  std::shared_ptr<DTypeSelector> a =
      std::make_shared<DTypeSelector>(selectorName, sel, nullNode);
  addArg(a);
}

void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
{
  d_args.push_back(a);
}

void DTypeConstructor::addArgSelf(std::string selectorName)
{
  Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
  Node nullNode;
  std::shared_ptr<DTypeSelector> a =
      std::make_shared<DTypeSelector>(selectorName + '\0', nullNode, nullNode);
  addArg(a);
}

const std::string& DTypeConstructor::getName() const { return d_name; }

Node DTypeConstructor::getConstructor() const
{
  Assert(isResolved());
  return d_constructor;
}

Node DTypeConstructor::getTester() const
{
  Assert(isResolved());
  return d_tester;
}

void DTypeConstructor::setSygus(Node op)
{
  Assert(!isResolved());
  d_sygusOp = op;
}

Node DTypeConstructor::getSygusOp() const
{
  Assert(isResolved());
  return d_sygusOp;
}

bool DTypeConstructor::isSygusIdFunc() const
{
  Assert(isResolved());
  return (d_sygusOp.getKind() == LAMBDA && d_sygusOp[0].getNumChildren() == 1
          && d_sygusOp[0][0] == d_sygusOp[1]);
}

unsigned DTypeConstructor::getWeight() const
{
  Assert(isResolved());
  return d_weight;
}

size_t DTypeConstructor::getNumArgs() const { return d_args.size(); }

TypeNode DTypeConstructor::getSpecializedConstructorType(
    TypeNode returnType) const
{
  Assert(isResolved());
  Assert(returnType.isDatatype())
      << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
         "got "
      << returnType;
  TypeNode ctn = d_constructor.getType();
  const DType& dt = DType::datatypeOf(d_constructor);
  if (!dt.isParametric())
  {
    // if the datatype is not parametric, then no specialization is needed
    return ctn;
  }
  TypeNode dtt = dt.getTypeNode();
  TypeMatcher m(dtt);
  m.doMatching(dtt, returnType);
  std::vector<TypeNode> subst;
  m.getMatches(subst);
  std::vector<TypeNode> params = dt.getParameters();
  return ctn.substitute(
      params.begin(), params.end(), subst.begin(), subst.end());
}

const std::vector<std::shared_ptr<DTypeSelector> >& DTypeConstructor::getArgs()
    const
{
  return d_args;
}

Cardinality DTypeConstructor::getCardinality(TypeNode t) const
{
  Assert(isResolved());

  Cardinality c = 1;

  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
  {
    c *= getArgType(i).getCardinality();
  }

  return c;
}

CardinalityClass DTypeConstructor::getCardinalityClass(TypeNode t) const
{
  std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
  return cinfo.first;
}

bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
{
  std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
  return cinfo.second;
}

std::pair<CardinalityClass, bool> DTypeConstructor::computeCardinalityInfo(
    TypeNode t) const
{
  std::map<TypeNode, std::pair<CardinalityClass, bool> >::iterator it =
      d_cardInfo.find(t);
  if (it != d_cardInfo.end())
  {
    return it->second;
  }
  std::pair<CardinalityClass, bool> ret(CardinalityClass::ONE, false);
  std::vector<TypeNode> instTypes;
  std::vector<TypeNode> paramTypes;
  bool isParam = t.isParametricDatatype();
  if (isParam)
  {
    paramTypes = t.getDType().getParameters();
    instTypes = t.getParamTypes();
  }
  for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    TypeNode tc = getArgType(i);
    if (isParam)
    {
      tc = tc.substitute(paramTypes.begin(),
                         paramTypes.end(),
                         instTypes.begin(),
                         instTypes.end());
    }
    // get the current cardinality class
    CardinalityClass cctc = tc.getCardinalityClass();
    // update ret.first to the max cardinality class
    ret.first = maxCardinalityClass(ret.first, cctc);
    if (cctc != CardinalityClass::INFINITE)
    {
      // if the argument is (interpreted) finite and external, set the flag
      // for indicating it has a finite external argument
      ret.second = ret.second || !tc.isDatatype();
    }
  }
  d_cardInfo[t] = ret;
  return ret;
}

bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }

const DTypeSelector& DTypeConstructor::operator[](size_t index) const
{
  Assert(index < getNumArgs());
  return *d_args[index];
}

TypeNode DTypeConstructor::getArgType(size_t index) const
{
  Assert(index < getNumArgs());
  return (*this)[index].getType().getSelectorRangeType();
}

Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
                                           size_t index) const
{
  Assert(isResolved());
  Assert(index < getNumArgs());
  if (options::dtSharedSelectors())
  {
    computeSharedSelectors(domainType);
    Assert(d_sharedSelectors[domainType].size() == getNumArgs());
    return d_sharedSelectors[domainType][index];
  }
  else
  {
    return d_args[index]->getSelector();
  }
}

int DTypeConstructor::getSelectorIndexInternal(Node sel) const
{
  Assert(isResolved());
  if (options::dtSharedSelectors())
  {
    Assert(sel.getType().isSelector());
    TypeNode domainType = sel.getType().getSelectorDomainType();
    computeSharedSelectors(domainType);
    std::map<Node, unsigned>::iterator its =
        d_sharedSelectorIndex[domainType].find(sel);
    if (its != d_sharedSelectorIndex[domainType].end())
    {
      return (int)its->second;
    }
  }
  else
  {
    unsigned sindex = DType::indexOf(sel);
    if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
    {
      return static_cast<int>(sindex);
    }
  }
  return -1;
}

int DTypeConstructor::getSelectorIndexForName(const std::string& name) const
{
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    if (d_args[i]->getName() == name)
    {
      return i;
    }
  }
  return -1;
}

bool DTypeConstructor::involvesExternalType() const
{
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    if (!getArgType(i).isDatatype())
    {
      return true;
    }
  }
  return false;
}

bool DTypeConstructor::involvesUninterpretedType() const
{
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    if (!getArgType(i).isSort())
    {
      return true;
    }
  }
  return false;
}

Cardinality DTypeConstructor::computeCardinality(
    TypeNode t, std::vector<TypeNode>& processing) const
{
  Cardinality c = 1;
  std::vector<TypeNode> instTypes;
  std::vector<TypeNode> paramTypes;
  bool isParam = t.isParametricDatatype();
  if (isParam)
  {
    paramTypes = t.getDType().getParameters();
    instTypes = t.getParamTypes();
  }
  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
  {
    TypeNode tc = getArgType(i);
    if (isParam)
    {
      tc = tc.substitute(paramTypes.begin(),
                         paramTypes.end(),
                         instTypes.begin(),
                         instTypes.end());
    }
    if (tc.isDatatype())
    {
      const DType& dt = tc.getDType();
      c *= dt.computeCardinality(t, processing);
    }
    else
    {
      c *= tc.getCardinality();
    }
  }
  return c;
}

bool DTypeConstructor::computeWellFounded(
    std::vector<TypeNode>& processing) const
{
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    TypeNode t = getArgType(i);
    if (t.isDatatype())
    {
      const DType& dt = t.getDType();
      if (!dt.computeWellFounded(processing))
      {
        return false;
      }
    }
  }
  return true;
}

Node DTypeConstructor::computeGroundTerm(TypeNode t,
                                         std::vector<TypeNode>& processing,
                                         std::map<TypeNode, Node>& gt,
                                         bool isValue) const
{
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> groundTerms;
  groundTerms.push_back(getConstructor());
  Trace("datatypes-init") << "cons " << d_constructor
                          << " computeGroundTerm, isValue = " << isValue
                          << std::endl;

  // for each selector, get a ground term
  std::vector<TypeNode> instTypes;
  std::vector<TypeNode> paramTypes;
  bool isParam = t.isParametricDatatype();
  if (isParam)
  {
    paramTypes = t.getDType().getParameters();
    instTypes = TypeNode(t).getParamTypes();
  }
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
  {
    TypeNode selType = getArgType(i);
    if (isParam)
    {
      selType = selType.substitute(paramTypes.begin(),
                                   paramTypes.end(),
                                   instTypes.begin(),
                                   instTypes.end());
    }
    Node arg;
    if (selType.isDatatype())
    {
      std::map<TypeNode, Node>::iterator itgt = gt.find(selType);
      if (itgt != gt.end())
      {
        arg = itgt->second;
      }
      else
      {
        const DType& dt = selType.getDType();
        arg = dt.computeGroundTerm(selType, processing, isValue);
      }
    }
    else
    {
      // call mkGroundValue or mkGroundTerm based on isValue
      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
    }
    if (arg.isNull())
    {
      Trace("datatypes-init") << "...unable to construct arg of "
                              << d_args[i]->getName() << std::endl;
      return Node();
    }
    else
    {
      Trace("datatypes-init")
          << "...constructed arg " << arg << " of type " << arg.getType()
          << ", isConst = " << arg.isConst() << std::endl;
      Assert(!isValue || arg.isConst())
          << "Expected non-constant constructor argument : " << arg
          << " of type " << arg.getType();
      groundTerms.push_back(arg);
    }
  }

  Node groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
  if (isParam)
  {
    Assert(DType::datatypeOf(d_constructor).isParametric());
    // type is parametric, must apply type ascription
    Trace("datatypes-init") << "ambiguous type for " << groundTerm
                            << ", ascribe to " << t << std::endl;
    groundTerms[0] = nm->mkNode(
        APPLY_TYPE_ASCRIPTION,
        nm->mkConst(AscriptionType(getSpecializedConstructorType(t))),
        groundTerms[0]);
    groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
  }
  Trace("datatypes-init") << "...return " << groundTerm << std::endl;
  Assert(!isValue || groundTerm.isConst()) << "Non-constant term " << groundTerm
                                           << " returned for computeGroundTerm";
  return groundTerm;
}

void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const
{
  if (d_sharedSelectors[domainType].size() < getNumArgs())
  {
    TypeNode ctype;
    if (domainType.isParametricDatatype())
    {
      ctype = getSpecializedConstructorType(domainType);
    }
    else
    {
      ctype = d_constructor.getType();
    }
    Assert(ctype.isConstructor());
    Assert(ctype.getNumChildren() - 1 == getNumArgs());
    // compute the shared selectors
    const DType& dt = DType::datatypeOf(d_constructor);
    std::map<TypeNode, unsigned> counter;
    for (size_t j = 0, jend = ctype.getNumChildren() - 1; j < jend; j++)
    {
      TypeNode t = ctype[j];
      Node ss = dt.getSharedSelector(domainType, t, counter[t]);
      d_sharedSelectors[domainType].push_back(ss);
      Assert(d_sharedSelectorIndex[domainType].find(ss)
             == d_sharedSelectorIndex[domainType].end());
      d_sharedSelectorIndex[domainType][ss] = j;
      counter[t]++;
    }
  }
}

bool DTypeConstructor::resolve(
    TypeNode self,
    const std::map<std::string, TypeNode>& resolutions,
    const std::vector<TypeNode>& placeholders,
    const std::vector<TypeNode>& replacements,
    const std::vector<TypeNode>& paramTypes,
    const std::vector<TypeNode>& paramReplacements,
    size_t cindex)
{
  if (isResolved())
  {
    // already resolved, fail
    return false;
  }
  Trace("datatypes") << "DTypeConstructor::resolve, self type is " << self
                     << std::endl;

  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  size_t index = 0;
  std::vector<TypeNode> argTypes;
  Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
  for (std::shared_ptr<DTypeSelector> arg : d_args)
  {
    std::string argName = arg->d_name;
    TypeNode range;
    if (arg->d_selector.isNull())
    {
      // the unresolved type wasn't created here; do name resolution
      std::string typeName = argName.substr(argName.find('\0') + 1);
      Trace("datatypes-init")
          << "  - selector, typeName is " << typeName << std::endl;
      argName.resize(argName.find('\0'));
      if (typeName == "")
      {
        Trace("datatypes-init") << "  ...self selector" << std::endl;
        range = self;
      }
      else
      {
        std::map<std::string, TypeNode>::const_iterator j =
            resolutions.find(typeName);
        if (j == resolutions.end())
        {
          Trace("datatypes-init")
              << "  ...failed to resolve selector" << std::endl;
          // failed to resolve selector
          return false;
        }
        else
        {
          Trace("datatypes-init") << "  ...resolved selector" << std::endl;
          range = (*j).second;
        }
      }
    }
    else
    {
      // the type for the selector already exists; may need
      // complex-type substitution
      range = arg->d_selector.getType();
      Trace("datatypes-init")
          << "  - null selector, range = " << range << std::endl;
      if (!placeholders.empty())
      {
        range = range.substitute(placeholders.begin(),
                                 placeholders.end(),
                                 replacements.begin(),
                                 replacements.end());
      }
      Trace("datatypes-init")
          << "  ...range after placeholder replacement " << range << std::endl;
      if (!paramTypes.empty())
      {
        range = doParametricSubstitution(range, paramTypes, paramReplacements);
      }
      Trace("datatypes-init")
          << "  ...range after parametric substitution " << range << std::endl;
    }
    // Internally, selectors (and updaters) are fresh internal skolems which
    // we constructor via mkDummySkolem.
    arg->d_selector = sm->mkDummySkolem(
        argName,
        nm->mkSelectorType(self, range),
        "is a selector",
        NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
    std::string updateName("update_" + argName);
    arg->d_updater = sm->mkDummySkolem(
        updateName,
        nm->mkDatatypeUpdateType(self, range),
        "is a selector",
        NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
    // must set indices to ensure datatypes::utils::indexOf works
    arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
    arg->d_selector.setAttribute(DTypeIndexAttr(), index);
    arg->d_updater.setAttribute(DTypeConsIndexAttr(), cindex);
    arg->d_updater.setAttribute(DTypeIndexAttr(), index);
    index = index + 1;
    arg->d_resolved = true;
    argTypes.push_back(range);
    // We use \0 as a distinguished marker for unresolved selectors for doing
    // name resolutions. We now can remove \0 from name if necessary.
    const size_t nul = arg->d_name.find('\0');
    if (nul != std::string::npos)
    {
      arg->d_name.resize(nul);
    }
  }

  Assert(index == getNumArgs());

  // Set constructor/tester last, since DTypeConstructor::isResolved()
  // returns true when d_tester is not the null Node.  If something
  // fails above, we want Constuctor::isResolved() to remain "false".
  // Further, mkConstructorType() iterates over the selectors, so
  // should get the results of any resolutions we did above.
  // The name of the tester variable does not matter, it is only used
  // internally.
  std::string testerName("is_" + d_name);
  d_tester = sm->mkDummySkolem(
      testerName,
      nm->mkTesterType(self),
      "is a tester",
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
  d_constructor = sm->mkDummySkolem(
      getName(),
      nm->mkConstructorType(argTypes, self),
      "is a constructor",
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
  Assert(d_constructor.getType().isConstructor());
  // associate constructor with all selectors
  for (std::shared_ptr<DTypeSelector> sel : d_args)
  {
    sel->d_constructor = d_constructor;
  }
  Assert(isResolved());
  return true;
}

TypeNode DTypeConstructor::doParametricSubstitution(
    TypeNode range,
    const std::vector<TypeNode>& paramTypes,
    const std::vector<TypeNode>& paramReplacements)
{
  if (range.getNumChildren() == 0)
  {
    return range;
  }
  std::vector<TypeNode> origChildren;
  std::vector<TypeNode> children;
  for (TypeNode::const_iterator i = range.begin(), iend = range.end();
       i != iend;
       ++i)
  {
    origChildren.push_back((*i));
    children.push_back(
        doParametricSubstitution((*i), paramTypes, paramReplacements));
  }
  for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
  {
    if (paramTypes[i].getSortConstructorArity() == origChildren.size())
    {
      TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
      if (range == tn)
      {
        TypeNode tret =
            paramReplacements[i].instantiateParametricDatatype(children);
        return tret;
      }
    }
  }
  NodeBuilder nb(range.getKind());
  for (size_t i = 0, csize = children.size(); i < csize; ++i)
  {
    nb << children[i];
  }
  TypeNode tn = nb.constructTypeNode();
  return tn;
}

void DTypeConstructor::toStream(std::ostream& out) const
{
  out << getName();

  unsigned nargs = getNumArgs();
  if (nargs == 0)
  {
    return;
  }
  out << "(";
  for (unsigned i = 0; i < nargs; i++)
  {
    out << *d_args[i];
    if (i + 1 < nargs)
    {
      out << ", ";
    }
  }
  out << ")";
}

std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
{
  ctor.toStream(os);
  return os;
}

}  // 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		* A class representing a datatype definition.
14		*/
15		#include "expr/dtype_cons.h"
16
17		#include "expr/ascription_type.h"
18		#include "expr/dtype.h"
19		#include "expr/node_manager.h"
20		#include "expr/skolem_manager.h"
21		#include "expr/type_matcher.h"
22		#include "options/datatypes_options.h"
23
24		using namespace cvc5::kind;
25		using namespace cvc5::theory;
26
27		namespace cvc5 {
28
29	13852	DTypeConstructor::DTypeConstructor(std::string name,
30	13852	unsigned weight)
31		: // We don't want to introduce a new data member, because eventually
32		// we're going to be a constant stuffed inside a node. So we stow
33		// the tester name away inside the constructor name until
34		// resolution.
35		d_name(name),
36		d_tester(),
37		d_args(),
38	13852	d_weight(weight)
39		{
40	13852	Assert(name != "");
41	13852	}
42
43	13789	void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
44		{
45		// We don't want to introduce a new data member, because eventually
46		// we're going to be a constant stuffed inside a node. So we stow
47		// the selector type away inside a var until resolution (when we can
48		// create the proper selector type)
49	13789	Assert(!isResolved());
50	13789	Assert(!selectorType.isNull());
51	13789	SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
52		Node sel = sm->mkDummySkolem(
53	27578	"unresolved_" + selectorName,
54		selectorType,
55		"is an unresolved selector type placeholder",
56	55156	NodeManager::SKOLEM_EXACT_NAME \| NodeManager::SKOLEM_NO_NOTIFY);
57		// can use null updater for now
58	27578	Node nullNode;
59	13789	Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl;
60		std::shared_ptr<DTypeSelector> a =
61	27578	std::make_shared<DTypeSelector>(selectorName, sel, nullNode);
62	13789	addArg(a);
63	13789	}
64
65	13857	void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
66		{
67	13857	d_args.push_back(a);
68	13857	}
69
70	68	void DTypeConstructor::addArgSelf(std::string selectorName)
71		{
72	68	Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
73	136	Node nullNode;
74		std::shared_ptr<DTypeSelector> a =
75	136	std::make_shared<DTypeSelector>(selectorName + '\0', nullNode, nullNode);
76	68	addArg(a);
77	68	}
78
79	29467	const std::string& DTypeConstructor::getName() const { return d_name; }
80
81	292822	Node DTypeConstructor::getConstructor() const
82		{
83	292822	Assert(isResolved());
84	292822	return d_constructor;
85		}
86
87	191800	Node DTypeConstructor::getTester() const
88		{
89	191800	Assert(isResolved());
90	191800	return d_tester;
91		}
92
93	10049	void DTypeConstructor::setSygus(Node op)
94		{
95	10049	Assert(!isResolved());
96	10049	d_sygusOp = op;
97	10049	}
98
99	1416759	Node DTypeConstructor::getSygusOp() const
100		{
101	1416759	Assert(isResolved());
102	1416759	return d_sygusOp;
103		}
104
105	686	bool DTypeConstructor::isSygusIdFunc() const
106		{
107	686	Assert(isResolved());
108	1655	return (d_sygusOp.getKind() == LAMBDA && d_sygusOp[0].getNumChildren() == 1
109	2158	&& d_sygusOp[0][0] == d_sygusOp[1]);
110		}
111
112	297338	unsigned DTypeConstructor::getWeight() const
113		{
114	297338	Assert(isResolved());
115	297338	return d_weight;
116		}
117
118	6651262	size_t DTypeConstructor::getNumArgs() const { return d_args.size(); }
119
120	1409	TypeNode DTypeConstructor::getSpecializedConstructorType(
121		TypeNode returnType) const
122		{
123	1409	Assert(isResolved());
124	1409	Assert(returnType.isDatatype())
125		<< "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
126		"got "
127		<< returnType;
128	2818	TypeNode ctn = d_constructor.getType();
129	1409	const DType& dt = DType::datatypeOf(d_constructor);
130	1409	if (!dt.isParametric())
131		{
132		// if the datatype is not parametric, then no specialization is needed
133	903	return ctn;
134		}
135	1012	TypeNode dtt = dt.getTypeNode();
136	1012	TypeMatcher m(dtt);
137	506	m.doMatching(dtt, returnType);
138	1012	std::vector<TypeNode> subst;
139	506	m.getMatches(subst);
140	1012	std::vector<TypeNode> params = dt.getParameters();
141		return ctn.substitute(
142	506	params.begin(), params.end(), subst.begin(), subst.end());
143		}
144
145	2138	const std::vector<std::shared_ptr<DTypeSelector> >& DTypeConstructor::getArgs()
146		const
147		{
148	2138	return d_args;
149		}
150
151		Cardinality DTypeConstructor::getCardinality(TypeNode t) const
152		{
153		Assert(isResolved());
154
155		Cardinality c = 1;
156
157		for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
158		{
159		c *= getArgType(i).getCardinality();
160		}
161
162		return c;
163		}
164
165	39371	CardinalityClass DTypeConstructor::getCardinalityClass(TypeNode t) const
166		{
167	39371	std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
168	39371	return cinfo.first;
169		}
170
171	90599	bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
172		{
173	90599	std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
174	90599	return cinfo.second;
175		}
176
177	129970	std::pair<CardinalityClass, bool> DTypeConstructor::computeCardinalityInfo(
178		TypeNode t) const
179		{
180		std::map<TypeNode, std::pair<CardinalityClass, bool> >::iterator it =
181	129970	d_cardInfo.find(t);
182	129970	if (it != d_cardInfo.end())
183		{
184	123538	return it->second;
185		}
186	6432	std::pair<CardinalityClass, bool> ret(CardinalityClass::ONE, false);
187	12864	std::vector<TypeNode> instTypes;
188	12864	std::vector<TypeNode> paramTypes;
189	6432	bool isParam = t.isParametricDatatype();
190	6432	if (isParam)
191		{
192	68	paramTypes = t.getDType().getParameters();
193	68	instTypes = t.getParamTypes();
194		}
195	13934	for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
196		{
197	15004	TypeNode tc = getArgType(i);
198	7502	if (isParam)
199		{
200	85	tc = tc.substitute(paramTypes.begin(),
201		paramTypes.end(),
202		instTypes.begin(),
203		instTypes.end());
204		}
205		// get the current cardinality class
206	7502	CardinalityClass cctc = tc.getCardinalityClass();
207		// update ret.first to the max cardinality class
208	7502	ret.first = maxCardinalityClass(ret.first, cctc);
209	7502	if (cctc != CardinalityClass::INFINITE)
210		{
211		// if the argument is (interpreted) finite and external, set the flag
212		// for indicating it has a finite external argument
213	987	ret.second = ret.second \|\| !tc.isDatatype();
214		}
215		}
216	6432	d_cardInfo[t] = ret;
217	6432	return ret;
218		}
219
220	2851397	bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }
221
222	1454037	const DTypeSelector& DTypeConstructor::operator[](size_t index) const
223		{
224	1454037	Assert(index < getNumArgs());
225	1454037	return *d_args[index];
226		}
227
228	594933	TypeNode DTypeConstructor::getArgType(size_t index) const
229		{
230	594933	Assert(index < getNumArgs());
231	594933	return (*this)[index].getType().getSelectorRangeType();
232		}
233
234	293441	Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
235		size_t index) const
236		{
237	293441	Assert(isResolved());
238	293441	Assert(index < getNumArgs());
239	293441	if (options::dtSharedSelectors())
240		{
241	235289	computeSharedSelectors(domainType);
242	235289	Assert(d_sharedSelectors[domainType].size() == getNumArgs());
243	235289	return d_sharedSelectors[domainType][index];
244		}
245		else
246		{
247	58152	return d_args[index]->getSelector();
248		}
249		}
250
251	274226	int DTypeConstructor::getSelectorIndexInternal(Node sel) const
252		{
253	274226	Assert(isResolved());
254	274226	if (options::dtSharedSelectors())
255		{
256	182836	Assert(sel.getType().isSelector());
257	280173	TypeNode domainType = sel.getType().getSelectorDomainType();
258	182836	computeSharedSelectors(domainType);
259		std::map<Node, unsigned>::iterator its =
260	182836	d_sharedSelectorIndex[domainType].find(sel);
261	182836	if (its != d_sharedSelectorIndex[domainType].end())
262		{
263	85499	return (int)its->second;
264		}
265		}
266		else
267		{
268	91390	unsigned sindex = DType::indexOf(sel);
269	91390	if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
270		{
271	27803	return static_cast<int>(sindex);
272		}
273		}
274	160924	return -1;
275		}
276
277	23	int DTypeConstructor::getSelectorIndexForName(const std::string& name) const
278		{
279	27	for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
280		{
281	23	if (d_args[i]->getName() == name)
282		{
283	19	return i;
284		}
285		}
286	4	return -1;
287		}
288
289	13852	bool DTypeConstructor::involvesExternalType() const
290		{
291	25904	for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
292		{
293	13018	if (!getArgType(i).isDatatype())
294		{
295	966	return true;
296		}
297		}
298	12886	return false;
299		}
300
301	13852	bool DTypeConstructor::involvesUninterpretedType() const
302		{
303	14145	for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
304		{
305	7272	if (!getArgType(i).isSort())
306		{
307	6979	return true;
308		}
309		}
310	6873	return false;
311		}
312
313	13891	Cardinality DTypeConstructor::computeCardinality(
314		TypeNode t, std::vector<TypeNode>& processing) const
315		{
316	13891	Cardinality c = 1;
317	27782	std::vector<TypeNode> instTypes;
318	27782	std::vector<TypeNode> paramTypes;
319	13891	bool isParam = t.isParametricDatatype();
320	13891	if (isParam)
321		{
322		paramTypes = t.getDType().getParameters();
323		instTypes = t.getParamTypes();
324		}
325	18961	for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
326		{
327	10140	TypeNode tc = getArgType(i);
328	5070	if (isParam)
329		{
330		tc = tc.substitute(paramTypes.begin(),
331		paramTypes.end(),
332		instTypes.begin(),
333		instTypes.end());
334		}
335	5070	if (tc.isDatatype())
336		{
337	4493	const DType& dt = tc.getDType();
338	4493	c *= dt.computeCardinality(t, processing);
339		}
340		else
341		{
342	577	c *= tc.getCardinality();
343		}
344		}
345	27782	return c;
346		}
347
348	4520	bool DTypeConstructor::computeWellFounded(
349		std::vector<TypeNode>& processing) const
350		{
351	8277	for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
352		{
353	8320	TypeNode t = getArgType(i);
354	4563	if (t.isDatatype())
355		{
356	2343	const DType& dt = t.getDType();
357	2343	if (!dt.computeWellFounded(processing))
358		{
359	806	return false;
360		}
361		}
362		}
363	3714	return true;
364		}
365
366	1640	Node DTypeConstructor::computeGroundTerm(TypeNode t,
367		std::vector<TypeNode>& processing,
368		std::map<TypeNode, Node>& gt,
369		bool isValue) const
370		{
371	1640	NodeManager* nm = NodeManager::currentNM();
372	3280	std::vector<Node> groundTerms;
373	1640	groundTerms.push_back(getConstructor());
374	3280	Trace("datatypes-init") << "cons " << d_constructor
375	1640	<< " computeGroundTerm, isValue = " << isValue
376	1640	<< std::endl;
377
378		// for each selector, get a ground term
379	3280	std::vector<TypeNode> instTypes;
380	3280	std::vector<TypeNode> paramTypes;
381	1640	bool isParam = t.isParametricDatatype();
382	1640	if (isParam)
383		{
384	27	paramTypes = t.getDType().getParameters();
385	27	instTypes = TypeNode(t).getParamTypes();
386		}
387	2382	for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
388		{
389	1560	TypeNode selType = getArgType(i);
390	818	if (isParam)
391		{
392	20	selType = selType.substitute(paramTypes.begin(),
393		paramTypes.end(),
394		instTypes.begin(),
395		instTypes.end());
396		}
397	1560	Node arg;
398	818	if (selType.isDatatype())
399		{
400	540	std::map<TypeNode, Node>::iterator itgt = gt.find(selType);
401	540	if (itgt != gt.end())
402		{
403	1	arg = itgt->second;
404		}
405		else
406		{
407	539	const DType& dt = selType.getDType();
408	539	arg = dt.computeGroundTerm(selType, processing, isValue);
409		}
410		}
411		else
412		{
413		// call mkGroundValue or mkGroundTerm based on isValue
414	278	arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
415		}
416	818	if (arg.isNull())
417		{
418	152	Trace("datatypes-init") << "...unable to construct arg of "
419	76	<< d_args[i]->getName() << std::endl;
420	76	return Node();
421		}
422		else
423		{
424	1484	Trace("datatypes-init")
425	1484	<< "...constructed arg " << arg << " of type " << arg.getType()
426	742	<< ", isConst = " << arg.isConst() << std::endl;
427	1484	Assert(!isValue \|\| arg.isConst())
428	742	<< "Expected non-constant constructor argument : " << arg
429	742	<< " of type " << arg.getType();
430	742	groundTerms.push_back(arg);
431		}
432		}
433
434	3128	Node groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
435	1564	if (isParam)
436		{
437	26	Assert(DType::datatypeOf(d_constructor).isParametric());
438		// type is parametric, must apply type ascription
439	52	Trace("datatypes-init") << "ambiguous type for " << groundTerm
440	26	<< ", ascribe to " << t << std::endl;
441	78	groundTerms[0] = nm->mkNode(
442		APPLY_TYPE_ASCRIPTION,
443	52	nm->mkConst(AscriptionType(getSpecializedConstructorType(t))),
444	26	groundTerms[0]);
445	26	groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
446		}
447	1564	Trace("datatypes-init") << "...return " << groundTerm << std::endl;
448	1564	Assert(!isValue \|\| groundTerm.isConst()) << "Non-constant term " << groundTerm
449		<< " returned for computeGroundTerm";
450	1564	return groundTerm;
451		}
452
453	418125	void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const
454		{
455	418125	if (d_sharedSelectors[domainType].size() < getNumArgs())
456		{
457	1380	TypeNode ctype;
458	690	if (domainType.isParametricDatatype())
459		{
460	2	ctype = getSpecializedConstructorType(domainType);
461		}
462		else
463		{
464	688	ctype = d_constructor.getType();
465		}
466	690	Assert(ctype.isConstructor());
467	690	Assert(ctype.getNumChildren() - 1 == getNumArgs());
468		// compute the shared selectors
469	690	const DType& dt = DType::datatypeOf(d_constructor);
470	1380	std::map<TypeNode, unsigned> counter;
471	2009	for (size_t j = 0, jend = ctype.getNumChildren() - 1; j < jend; j++)
472		{
473	2638	TypeNode t = ctype[j];
474	2638	Node ss = dt.getSharedSelector(domainType, t, counter[t]);
475	1319	d_sharedSelectors[domainType].push_back(ss);
476	1319	Assert(d_sharedSelectorIndex[domainType].find(ss)
477		== d_sharedSelectorIndex[domainType].end());
478	1319	d_sharedSelectorIndex[domainType][ss] = j;
479	1319	counter[t]++;
480		}
481		}
482	418125	}
483
484	13852	bool DTypeConstructor::resolve(
485		TypeNode self,
486		const std::map<std::string, TypeNode>& resolutions,
487		const std::vector<TypeNode>& placeholders,
488		const std::vector<TypeNode>& replacements,
489		const std::vector<TypeNode>& paramTypes,
490		const std::vector<TypeNode>& paramReplacements,
491		size_t cindex)
492		{
493	13852	if (isResolved())
494		{
495		// already resolved, fail
496		return false;
497		}
498	27704	Trace("datatypes") << "DTypeConstructor::resolve, self type is " << self
499	13852	<< std::endl;
500
501	13852	NodeManager* nm = NodeManager::currentNM();
502	13852	SkolemManager* sm = nm->getSkolemManager();
503	13852	size_t index = 0;
504	27704	std::vector<TypeNode> argTypes;
505	13852	Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
506	27709	for (std::shared_ptr<DTypeSelector> arg : d_args)
507		{
508	27714	std::string argName = arg->d_name;
509	27714	TypeNode range;
510	13857	if (arg->d_selector.isNull())
511		{
512		// the unresolved type wasn't created here; do name resolution
513	136	std::string typeName = argName.substr(argName.find('\0') + 1);
514	136	Trace("datatypes-init")
515	68	<< " - selector, typeName is " << typeName << std::endl;
516	68	argName.resize(argName.find('\0'));
517	68	if (typeName == "")
518		{
519	68	Trace("datatypes-init") << " ...self selector" << std::endl;
520	68	range = self;
521		}
522		else
523		{
524		std::map<std::string, TypeNode>::const_iterator j =
525		resolutions.find(typeName);
526		if (j == resolutions.end())
527		{
528		Trace("datatypes-init")
529		<< " ...failed to resolve selector" << std::endl;
530		// failed to resolve selector
531		return false;
532		}
533		else
534		{
535		Trace("datatypes-init") << " ...resolved selector" << std::endl;
536		range = (*j).second;
537		}
538		}
539		}
540		else
541		{
542		// the type for the selector already exists; may need
543		// complex-type substitution
544	13789	range = arg->d_selector.getType();
545	27578	Trace("datatypes-init")
546	13789	<< " - null selector, range = " << range << std::endl;
547	13789	if (!placeholders.empty())
548		{
549	12982	range = range.substitute(placeholders.begin(),
550		placeholders.end(),
551		replacements.begin(),
552		replacements.end());
553		}
554	27578	Trace("datatypes-init")
555	13789	<< " ...range after placeholder replacement " << range << std::endl;
556	13789	if (!paramTypes.empty())
557		{
558	94	range = doParametricSubstitution(range, paramTypes, paramReplacements);
559		}
560	27578	Trace("datatypes-init")
561	13789	<< " ...range after parametric substitution " << range << std::endl;
562		}
563		// Internally, selectors (and updaters) are fresh internal skolems which
564		// we constructor via mkDummySkolem.
565	55428	arg->d_selector = sm->mkDummySkolem(
566		argName,
567	27714	nm->mkSelectorType(self, range),
568		"is a selector",
569	13857	NodeManager::SKOLEM_EXACT_NAME \| NodeManager::SKOLEM_NO_NOTIFY);
570	27714	std::string updateName("update_" + argName);
571	55428	arg->d_updater = sm->mkDummySkolem(
572		updateName,
573	27714	nm->mkDatatypeUpdateType(self, range),
574		"is a selector",
575	13857	NodeManager::SKOLEM_EXACT_NAME \| NodeManager::SKOLEM_NO_NOTIFY);
576		// must set indices to ensure datatypes::utils::indexOf works
577	13857	arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
578	13857	arg->d_selector.setAttribute(DTypeIndexAttr(), index);
579	13857	arg->d_updater.setAttribute(DTypeConsIndexAttr(), cindex);
580	13857	arg->d_updater.setAttribute(DTypeIndexAttr(), index);
581	13857	index = index + 1;
582	13857	arg->d_resolved = true;
583	13857	argTypes.push_back(range);
584		// We use \0 as a distinguished marker for unresolved selectors for doing
585		// name resolutions. We now can remove \0 from name if necessary.
586	13857	const size_t nul = arg->d_name.find('\0');
587	13857	if (nul != std::string::npos)
588		{
589	68	arg->d_name.resize(nul);
590		}
591		}
592
593	13852	Assert(index == getNumArgs());
594
595		// Set constructor/tester last, since DTypeConstructor::isResolved()
596		// returns true when d_tester is not the null Node. If something
597		// fails above, we want Constuctor::isResolved() to remain "false".
598		// Further, mkConstructorType() iterates over the selectors, so
599		// should get the results of any resolutions we did above.
600		// The name of the tester variable does not matter, it is only used
601		// internally.
602	27704	std::string testerName("is_" + d_name);
603	55408	d_tester = sm->mkDummySkolem(
604		testerName,
605	27704	nm->mkTesterType(self),
606		"is a tester",
607	13852	NodeManager::SKOLEM_EXACT_NAME \| NodeManager::SKOLEM_NO_NOTIFY);
608	55408	d_constructor = sm->mkDummySkolem(
609		getName(),
610	27704	nm->mkConstructorType(argTypes, self),
611		"is a constructor",
612	13852	NodeManager::SKOLEM_EXACT_NAME \| NodeManager::SKOLEM_NO_NOTIFY);
613	13852	Assert(d_constructor.getType().isConstructor());
614		// associate constructor with all selectors
615	27709	for (std::shared_ptr<DTypeSelector> sel : d_args)
616		{
617	13857	sel->d_constructor = d_constructor;
618		}
619	13852	Assert(isResolved());
620	13852	return true;
621		}
622
623	138	TypeNode DTypeConstructor::doParametricSubstitution(
624		TypeNode range,
625		const std::vector<TypeNode>& paramTypes,
626		const std::vector<TypeNode>& paramReplacements)
627		{
628	138	if (range.getNumChildren() == 0)
629		{
630	98	return range;
631		}
632	80	std::vector<TypeNode> origChildren;
633	80	std::vector<TypeNode> children;
634	84	for (TypeNode::const_iterator i = range.begin(), iend = range.end();
635	84	i != iend;
636		++i)
637		{
638	44	origChildren.push_back((*i));
639	44	children.push_back(
640	88	doParametricSubstitution((*i), paramTypes, paramReplacements));
641		}
642	50	for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
643		{
644	48	if (paramTypes[i].getSortConstructorArity() == origChildren.size())
645		{
646	54	TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
647	46	if (range == tn)
648		{
649		TypeNode tret =
650	76	paramReplacements[i].instantiateParametricDatatype(children);
651	38	return tret;
652		}
653		}
654		}
655	4	NodeBuilder nb(range.getKind());
656	6	for (size_t i = 0, csize = children.size(); i < csize; ++i)
657		{
658	4	nb << children[i];
659		}
660	4	TypeNode tn = nb.constructTypeNode();
661	2	return tn;
662		}
663
664	38	void DTypeConstructor::toStream(std::ostream& out) const
665		{
666	38	out << getName();
667
668	38	unsigned nargs = getNumArgs();
669	38	if (nargs == 0)
670		{
671	18	return;
672		}
673	20	out << "(";
674	54	for (unsigned i = 0; i < nargs; i++)
675		{
676	34	out << *d_args[i];
677	34	if (i + 1 < nargs)
678		{
679	14	out << ", ";
680		}
681		}
682	20	out << ")";
683		}
684
685	38	std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
686		{
687	38	ctor.toStream(os);
688	38	return os;
689		}
690
691	22746	} // namespace cvc5