Head

GCC Code Coverage Report

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