Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/type_info.cpp	Lines:	204	247	82.6 %
Date:	2021-09-16	Branches:	339	854	39.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of sygus type info class.
 */

#include "theory/quantifiers/sygus/type_info.h"

#include "base/check.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/sygus_datatype.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/sygus/type_node_id_trie.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

SygusTypeInfo::SygusTypeInfo()
    : d_hasIte(false),
      d_hasBoolConnective(false),
      d_min_term_size(0),
      d_sym_cons_any_constant(-1),
      d_has_subterm_sym_cons(false)
{
}

void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
{
  d_this = tn;
  Assert(tn.isDatatype());
  const DType& dt = tn.getDType();
  Assert(dt.isSygus());
  Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
  TypeNode btn = dt.getSygusType();
  d_btype = btn;
  Assert(!d_btype.isNull());
  // get the sygus variable list
  Node var_list = dt.getSygusVarList();
  if (!var_list.isNull())
  {
    for (unsigned j = 0; j < var_list.getNumChildren(); j++)
    {
      Node sv = var_list[j];
      SygusVarNumAttribute svna;
      sv.setAttribute(svna, j);
      d_var_list.push_back(sv);
    }
  }
  else
  {
    // no arguments to synthesis functions
    d_var_list.clear();
  }

  // compute min term size information: this must be computed before registering
  // subfield types
  d_min_term_size = 1;
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    if (dt[i].getNumArgs() == 0)
    {
      d_min_term_size = 0;
    }
  }

  // register connected types
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
    {
      TypeNode ctn = dt[i].getArgType(j);
      Trace("sygus-db") << "  register subfield type " << ctn << std::endl;
      if (tds->registerSygusType(ctn))
      {
        SygusTypeInfo& stic = tds->getTypeInfo(ctn);
        // carry type attributes
        if (stic.d_has_subterm_sym_cons)
        {
          d_has_subterm_sym_cons = true;
        }
      }
    }
  }
  // iterate over constructors
  for (unsigned i = 0; i < dt.getNumConstructors(); i++)
  {
    Node sop = dt[i].getSygusOp();
    Assert(!sop.isNull());
    Trace("sygus-db") << "  Operator #" << i << " : " << sop;
    Kind builtinKind = UNDEFINED_KIND;
    if (sop.getKind() == kind::BUILTIN)
    {
      builtinKind = NodeManager::operatorToKind(sop);
      Trace("sygus-db") << ", kind = " << builtinKind;
    }
    else if (sop.isConst() && dt[i].getNumArgs() == 0)
    {
      Trace("sygus-db") << ", constant";
      d_consts[sop] = i;
      d_arg_const[i] = sop;
    }
    else if (sop.getKind() == LAMBDA)
    {
      // do type checking
      Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
      {
        TypeNode ct = dt[i].getArgType(j);
        TypeNode cbt = tds->sygusToBuiltinType(ct);
        TypeNode lat = sop[0][j].getType();
        AlwaysAssert(cbt.isSubtypeOf(lat))
            << "In sygus datatype " << dt.getName()
            << ", argument to a lambda constructor is not " << lat << std::endl;
      }
      // See if it is a builtin kind, possible if the operator is of the form:
      // lambda x1 ... xn. f( x1, ..., xn ) and f is not a parameterized kind
      // (e.g. APPLY_UF is a parameterized kind).
      if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED)
      {
        size_t nchild = sop[0].getNumChildren();
        if (nchild == sop[1].getNumChildren())
        {
          builtinKind = sop[1].getKind();
          for (size_t j = 0; j < nchild; j++)
          {
            if (sop[0][j] != sop[1][j])
            {
              // arguments not in order
              builtinKind = UNDEFINED_KIND;
              break;
            }
          }
        }
      }
    }
    if (builtinKind != UNDEFINED_KIND)
    {
      d_kinds[builtinKind] = i;
      d_arg_kind[i] = builtinKind;
    }
    // symbolic constructors
    if (sop.getAttribute(SygusAnyConstAttribute()))
    {
      d_sym_cons_any_constant = i;
      d_has_subterm_sym_cons = true;
    }
    d_ops[sop] = i;
    d_arg_ops[i] = sop;
    Trace("sygus-db") << std::endl;
    // We must properly catch type errors in sygus grammars for arguments of
    // builtin operators. The challenge is that we easily ask for expected
    // argument types of builtin operators e.g. PLUS. Hence we use a call to
    // mkGeneric below. This ensures that terms that this constructor encodes
    // are of the type specified in the datatype. This will fail if
    // e.g. bitvector-and is a constructor of an integer grammar. Our (version
    // 2) SyGuS parser ensures that sygus constructors are built from well-typed
    // terms, so the term created by mkGeneric will also be well-typed here.
    Node g = tds->mkGeneric(dt, i);
    TypeNode gtn = g.getType();
    AlwaysAssert(gtn.isSubtypeOf(btn))
        << "Sygus datatype " << dt.getName()
        << " encodes terms that are not of type " << btn << std::endl;
    Trace("sygus-db") << "...done register Operator #" << i << std::endl;
    Kind gk = g.getKind();
    if (gk == ITE)
    {
      // mark that this type has an ITE
      d_hasIte = true;
      if (g.getType().isBoolean())
      {
        d_hasBoolConnective = true;
      }
    }
    else if (gk == AND || gk == OR || gk == IMPLIES || gk == XOR
             || (gk == EQUAL && g[0].getType().isBoolean()))
    {
      d_hasBoolConnective = true;
    }
    if (Trace.isOn("sygus-db"))
    {
      Node eop = datatypes::utils::getExpandedDefinitionForm(sop);
      Trace("sygus-db") << "Expanded form: ";
      if (eop == sop)
      {
        Trace("sygus-db") << "same";
      }
      else
      {
        Trace("sygus-db") << eop;
      }
      Trace("sygus-db") << std::endl;
    }
  }
  // compute minimum type depth information
  computeMinTypeDepthInternal(tn, 0);
  // compute minimum term size information
  d_min_term_size = 1;
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    unsigned csize = 0;
    if (dt[i].getNumArgs() > 0)
    {
      csize = 1;
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
      {
        TypeNode ct = dt[i].getArgType(j);
        if (ct == tn)
        {
          csize += d_min_term_size;
        }
        else if (tds->isRegistered(ct))
        {
          SygusTypeInfo& stic = tds->getTypeInfo(ct);
          csize += stic.getMinTermSize();
        }
        else
        {
          Assert(!ct.isDatatype() || !ct.getDType().isSygus());
        }
      }
    }
    d_min_cons_term_size[i] = csize;
  }
  Trace("sygus-db") << "Register type " << dt.getName() << " finished"
                    << std::endl;
}

void SygusTypeInfo::initializeVarSubclasses()
{
  if (d_var_list.empty())
  {
    // no variables
    return;
  }
  if (!d_var_subclass_id.empty())
  {
    // already computed
    return;
  }
  // compute variable subclasses
  std::vector<TypeNode> sf_types;
  getSubfieldTypes(sf_types);
  // maps variables to the list of subfield types they occur in
  std::map<Node, std::vector<TypeNode> > type_occurs;
  for (const Node& v : d_var_list)
  {
    type_occurs[v].clear();
  }
  // for each type of subfield type of this enumerator
  for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
  {
    std::vector<unsigned> rm_indices;
    TypeNode stn = sf_types[i];
    Assert(stn.isDatatype());
    const DType& dt = stn.getDType();
    for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
    {
      Node sopn = dt[j].getSygusOp();
      Assert(!sopn.isNull());
      if (type_occurs.find(sopn) != type_occurs.end())
      {
        // if it is a variable, store that it occurs in stn
        type_occurs[sopn].push_back(stn);
      }
    }
  }
  TypeNodeIdTrie tnit;
  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
  {
    tnit.add(to.first, to.second);
  }
  // 0 is reserved for "no type class id"
  unsigned typeIdCount = 1;
  tnit.assignIds(d_var_subclass_id, typeIdCount);
  // assign the list and reverse map to index
  for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
  {
    Node v = to.first;
    unsigned sc = d_var_subclass_id[v];
    Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
    d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
    d_var_subclass_list[sc].push_back(v);
  }
}

TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }

const std::vector<Node>& SygusTypeInfo::getVarList() const
{
  return d_var_list;
}

void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
                                                unsigned type_depth)
{
  std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
  if (it != d_min_type_depth.end() && type_depth >= it->second)
  {
    // no new information
    return;
  }
  if (!tn.isDatatype())
  {
    // do not recurse to non-datatype types
    return;
  }
  const DType& dt = tn.getDType();
  if (!dt.isSygus())
  {
    // do not recurse to non-sygus datatype types
    return;
  }
  d_min_type_depth[tn] = type_depth;
  // compute for connected types
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
    {
      TypeNode at = dt[i].getArgType(j);
      computeMinTypeDepthInternal(at, type_depth + 1);
    }
  }
}

unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
{
  std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
  if (it != d_min_type_depth.end())
  {
    Assert(false);
    return 0;
  }
  return it->second;
}

unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }

unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
{
  std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
  if (it != d_min_cons_term_size.end())
  {
    return it->second;
  }
  Assert(false);
  return 0;
}

void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
{
  for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
  {
    sf_types.push_back(st.first);
  }
}

int SygusTypeInfo::getKindConsNum(Kind k) const
{
  std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
  if (it != d_kinds.end())
  {
    return static_cast<int>(it->second);
  }
  return -1;
}

int SygusTypeInfo::getConstConsNum(Node n) const
{
  std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
  if (it != d_consts.end())
  {
    return static_cast<int>(it->second);
  }
  return -1;
}

int SygusTypeInfo::getOpConsNum(Node n) const
{
  std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
  if (it != d_ops.end())
  {
    return static_cast<int>(it->second);
  }
  return -1;
}

bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
bool SygusTypeInfo::hasIte() const { return d_hasIte; }
bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; }
bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }

Node SygusTypeInfo::getConsNumOp(unsigned i) const
{
  std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
  if (itn != d_arg_ops.end())
  {
    return itn->second;
  }
  return Node::null();
}

Node SygusTypeInfo::getConsNumConst(unsigned i) const
{
  std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
  if (itn != d_arg_const.end())
  {
    return itn->second;
  }
  return Node::null();
}

Kind SygusTypeInfo::getConsNumKind(unsigned i) const
{
  std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
  if (itk != d_arg_kind.end())
  {
    return itk->second;
  }
  return UNDEFINED_KIND;
}

bool SygusTypeInfo::isKindArg(unsigned i) const
{
  return getConsNumKind(i) != UNDEFINED_KIND;
}

bool SygusTypeInfo::isConstArg(unsigned i) const
{
  return d_arg_const.find(i) != d_arg_const.end();
}

int SygusTypeInfo::getAnyConstantConsNum() const
{
  return d_sym_cons_any_constant;
}

bool SygusTypeInfo::hasSubtermSymbolicCons() const
{
  return d_has_subterm_sym_cons;
}

unsigned SygusTypeInfo::getSubclassForVar(Node n) const
{
  std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
  if (itcc == d_var_subclass_id.end())
  {
    Assert(false);
    return 0;
  }
  return itcc->second;
}

unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
{
  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
      d_var_subclass_list.find(sc);
  if (itvv == d_var_subclass_list.end())
  {
    Assert(false);
    return 0;
  }
  return itvv->second.size();
}
Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
{
  std::map<unsigned, std::vector<Node> >::const_iterator itvv =
      d_var_subclass_list.find(sc);
  if (itvv == d_var_subclass_list.end() || i >= itvv->second.size())
  {
    Assert(false);
    return Node::null();
  }
  return itvv->second[i];
}

bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
{
  std::map<Node, unsigned>::const_iterator itvv =
      d_var_subclass_list_index.find(v);
  if (itvv == d_var_subclass_list_index.end())
  {
    return false;
  }
  index = itvv->second;
  return true;
}

bool SygusTypeInfo::isSubclassVarTrivial() const
{
  for (const std::pair<const unsigned, std::vector<Node> >& p :
       d_var_subclass_list)
  {
    if (p.second.size() > 1)
    {
      return false;
    }
  }
  return true;
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
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		* Implementation of sygus type info class.
14		*/
15
16		#include "theory/quantifiers/sygus/type_info.h"
17
18		#include "base/check.h"
19		#include "expr/dtype.h"
20		#include "expr/dtype_cons.h"
21		#include "expr/sygus_datatype.h"
22		#include "theory/datatypes/sygus_datatype_utils.h"
23		#include "theory/quantifiers/sygus/term_database_sygus.h"
24		#include "theory/quantifiers/sygus/type_node_id_trie.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32	1983	SygusTypeInfo::SygusTypeInfo()
33		: d_hasIte(false),
34		d_hasBoolConnective(false),
35		d_min_term_size(0),
36		d_sym_cons_any_constant(-1),
37	1983	d_has_subterm_sym_cons(false)
38		{
39	1983	}
40
41	1983	void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
42		{
43	1983	d_this = tn;
44	1983	Assert(tn.isDatatype());
45	1983	const DType& dt = tn.getDType();
46	1983	Assert(dt.isSygus());
47	1983	Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
48	3966	TypeNode btn = dt.getSygusType();
49	1983	d_btype = btn;
50	1983	Assert(!d_btype.isNull());
51		// get the sygus variable list
52	3966	Node var_list = dt.getSygusVarList();
53	1983	if (!var_list.isNull())
54		{
55	4984	for (unsigned j = 0; j < var_list.getNumChildren(); j++)
56		{
57	7232	Node sv = var_list[j];
58		SygusVarNumAttribute svna;
59	3616	sv.setAttribute(svna, j);
60	3616	d_var_list.push_back(sv);
61		}
62		}
63		else
64		{
65		// no arguments to synthesis functions
66	615	d_var_list.clear();
67		}
68
69		// compute min term size information: this must be computed before registering
70		// subfield types
71	1983	d_min_term_size = 1;
72	13821	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
73		{
74	11838	if (dt[i].getNumArgs() == 0)
75		{
76	5080	d_min_term_size = 0;
77		}
78		}
79
80		// register connected types
81	13821	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
82		{
83	24979	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
84		{
85	26282	TypeNode ctn = dt[i].getArgType(j);
86	13141	Trace("sygus-db") << " register subfield type " << ctn << std::endl;
87	13141	if (tds->registerSygusType(ctn))
88		{
89	13097	SygusTypeInfo& stic = tds->getTypeInfo(ctn);
90		// carry type attributes
91	13097	if (stic.d_has_subterm_sym_cons)
92		{
93	222	d_has_subterm_sym_cons = true;
94		}
95		}
96		}
97		}
98		// iterate over constructors
99	13821	for (unsigned i = 0; i < dt.getNumConstructors(); i++)
100		{
101	23676	Node sop = dt[i].getSygusOp();
102	11838	Assert(!sop.isNull());
103	11838	Trace("sygus-db") << " Operator #" << i << " : " << sop;
104	11838	Kind builtinKind = UNDEFINED_KIND;
105	11838	if (sop.getKind() == kind::BUILTIN)
106		{
107	4535	builtinKind = NodeManager::operatorToKind(sop);
108	4535	Trace("sygus-db") << ", kind = " << builtinKind;
109		}
110	7303	else if (sop.isConst() && dt[i].getNumArgs() == 0)
111		{
112	3447	Trace("sygus-db") << ", constant";
113	3447	d_consts[sop] = i;
114	3447	d_arg_const[i] = sop;
115		}
116	3856	else if (sop.getKind() == LAMBDA)
117		{
118		// do type checking
119	2064	Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
120	5946	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
121		{
122	7764	TypeNode ct = dt[i].getArgType(j);
123	7764	TypeNode cbt = tds->sygusToBuiltinType(ct);
124	7764	TypeNode lat = sop[0][j].getType();
125	7764	AlwaysAssert(cbt.isSubtypeOf(lat))
126	3882	<< "In sygus datatype " << dt.getName()
127		<< ", argument to a lambda constructor is not " << lat << std::endl;
128		}
129		// See if it is a builtin kind, possible if the operator is of the form:
130		// lambda x1 ... xn. f( x1, ..., xn ) and f is not a parameterized kind
131		// (e.g. APPLY_UF is a parameterized kind).
132	2064	if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED)
133		{
134	1721	size_t nchild = sop[0].getNumChildren();
135	1721	if (nchild == sop[1].getNumChildren())
136		{
137	1622	builtinKind = sop[1].getKind();
138	4789	for (size_t j = 0; j < nchild; j++)
139		{
140	3184	if (sop[0][j] != sop[1][j])
141		{
142		// arguments not in order
143	17	builtinKind = UNDEFINED_KIND;
144	17	break;
145		}
146		}
147		}
148		}
149		}
150	11838	if (builtinKind != UNDEFINED_KIND)
151		{
152	6140	d_kinds[builtinKind] = i;
153	6140	d_arg_kind[i] = builtinKind;
154		}
155		// symbolic constructors
156	11838	if (sop.getAttribute(SygusAnyConstAttribute()))
157		{
158	44	d_sym_cons_any_constant = i;
159	44	d_has_subterm_sym_cons = true;
160		}
161	11838	d_ops[sop] = i;
162	11838	d_arg_ops[i] = sop;
163	11838	Trace("sygus-db") << std::endl;
164		// We must properly catch type errors in sygus grammars for arguments of
165		// builtin operators. The challenge is that we easily ask for expected
166		// argument types of builtin operators e.g. PLUS. Hence we use a call to
167		// mkGeneric below. This ensures that terms that this constructor encodes
168		// are of the type specified in the datatype. This will fail if
169		// e.g. bitvector-and is a constructor of an integer grammar. Our (version
170		// 2) SyGuS parser ensures that sygus constructors are built from well-typed
171		// terms, so the term created by mkGeneric will also be well-typed here.
172	23676	Node g = tds->mkGeneric(dt, i);
173	23676	TypeNode gtn = g.getType();
174	23676	AlwaysAssert(gtn.isSubtypeOf(btn))
175	11838	<< "Sygus datatype " << dt.getName()
176		<< " encodes terms that are not of type " << btn << std::endl;
177	11838	Trace("sygus-db") << "...done register Operator #" << i << std::endl;
178	11838	Kind gk = g.getKind();
179	11838	if (gk == ITE)
180		{
181		// mark that this type has an ITE
182	820	d_hasIte = true;
183	820	if (g.getType().isBoolean())
184		{
185	29	d_hasBoolConnective = true;
186		}
187		}
188	21476	else if (gk == AND \|\| gk == OR \|\| gk == IMPLIES \|\| gk == XOR
189	20913	\|\| (gk == EQUAL && g[0].getType().isBoolean()))
190		{
191	1126	d_hasBoolConnective = true;
192		}
193	11838	if (Trace.isOn("sygus-db"))
194		{
195		Node eop = datatypes::utils::getExpandedDefinitionForm(sop);
196		Trace("sygus-db") << "Expanded form: ";
197		if (eop == sop)
198		{
199		Trace("sygus-db") << "same";
200		}
201		else
202		{
203		Trace("sygus-db") << eop;
204		}
205		Trace("sygus-db") << std::endl;
206		}
207		}
208		// compute minimum type depth information
209	1983	computeMinTypeDepthInternal(tn, 0);
210		// compute minimum term size information
211	1983	d_min_term_size = 1;
212	13821	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
213		{
214	11838	unsigned csize = 0;
215	11838	if (dt[i].getNumArgs() > 0)
216		{
217	6758	csize = 1;
218	19899	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
219		{
220	26282	TypeNode ct = dt[i].getArgType(j);
221	13141	if (ct == tn)
222		{
223	8588	csize += d_min_term_size;
224		}
225	4553	else if (tds->isRegistered(ct))
226		{
227	4509	SygusTypeInfo& stic = tds->getTypeInfo(ct);
228	4509	csize += stic.getMinTermSize();
229		}
230		else
231		{
232	44	Assert(!ct.isDatatype() \|\| !ct.getDType().isSygus());
233		}
234		}
235		}
236	11838	d_min_cons_term_size[i] = csize;
237		}
238	3966	Trace("sygus-db") << "Register type " << dt.getName() << " finished"
239	1983	<< std::endl;
240	1983	}
241
242	1	void SygusTypeInfo::initializeVarSubclasses()
243		{
244	1	if (d_var_list.empty())
245		{
246		// no variables
247		return;
248		}
249	1	if (!d_var_subclass_id.empty())
250		{
251		// already computed
252		return;
253		}
254		// compute variable subclasses
255	2	std::vector<TypeNode> sf_types;
256	1	getSubfieldTypes(sf_types);
257		// maps variables to the list of subfield types they occur in
258	2	std::map<Node, std::vector<TypeNode> > type_occurs;
259	3	for (const Node& v : d_var_list)
260		{
261	2	type_occurs[v].clear();
262		}
263		// for each type of subfield type of this enumerator
264	2	for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
265		{
266	2	std::vector<unsigned> rm_indices;
267	2	TypeNode stn = sf_types[i];
268	1	Assert(stn.isDatatype());
269	1	const DType& dt = stn.getDType();
270	4	for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
271		{
272	6	Node sopn = dt[j].getSygusOp();
273	3	Assert(!sopn.isNull());
274	3	if (type_occurs.find(sopn) != type_occurs.end())
275		{
276		// if it is a variable, store that it occurs in stn
277	2	type_occurs[sopn].push_back(stn);
278		}
279		}
280		}
281	2	TypeNodeIdTrie tnit;
282	3	for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
283		{
284	2	tnit.add(to.first, to.second);
285		}
286		// 0 is reserved for "no type class id"
287	1	unsigned typeIdCount = 1;
288	1	tnit.assignIds(d_var_subclass_id, typeIdCount);
289		// assign the list and reverse map to index
290	3	for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
291		{
292	4	Node v = to.first;
293	2	unsigned sc = d_var_subclass_id[v];
294	2	Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
295	2	d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
296	2	d_var_subclass_list[sc].push_back(v);
297		}
298		}
299
300	6664	TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }
301
302	129085	const std::vector<Node>& SygusTypeInfo::getVarList() const
303		{
304	129085	return d_var_list;
305		}
306
307	40892	void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
308		unsigned type_depth)
309		{
310	40892	std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
311	40892	if (it != d_min_type_depth.end() && type_depth >= it->second)
312		{
313		// no new information
314	70668	return;
315		}
316	5611	if (!tn.isDatatype())
317		{
318		// do not recurse to non-datatype types
319	106	return;
320		}
321	5505	const DType& dt = tn.getDType();
322	5505	if (!dt.isSygus())
323		{
324		// do not recurse to non-sygus datatype types
325		return;
326		}
327	5505	d_min_type_depth[tn] = type_depth;
328		// compute for connected types
329	38483	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
330		{
331	71887	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
332		{
333	77818	TypeNode at = dt[i].getArgType(j);
334	38909	computeMinTypeDepthInternal(at, type_depth + 1);
335		}
336		}
337		}
338
339		unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
340		{
341		std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
342		if (it != d_min_type_depth.end())
343		{
344		Assert(false);
345		return 0;
346		}
347		return it->second;
348		}
349
350	4509	unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }
351
352		unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
353		{
354		std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
355		if (it != d_min_cons_term_size.end())
356		{
357		return it->second;
358		}
359		Assert(false);
360		return 0;
361		}
362
363	504	void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
364		{
365	1575	for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
366		{
367	1071	sf_types.push_back(st.first);
368		}
369	504	}
370
371	15299	int SygusTypeInfo::getKindConsNum(Kind k) const
372		{
373	15299	std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
374	15299	if (it != d_kinds.end())
375		{
376	15090	return static_cast<int>(it->second);
377		}
378	209	return -1;
379		}
380
381	178	int SygusTypeInfo::getConstConsNum(Node n) const
382		{
383	178	std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
384	178	if (it != d_consts.end())
385		{
386	155	return static_cast<int>(it->second);
387		}
388	23	return -1;
389		}
390
391	6	int SygusTypeInfo::getOpConsNum(Node n) const
392		{
393	6	std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
394	6	if (it != d_ops.end())
395		{
396	6	return static_cast<int>(it->second);
397		}
398		return -1;
399		}
400
401	6151	bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
402	134	bool SygusTypeInfo::hasIte() const { return d_hasIte; }
403	91	bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; }
404	178	bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
405		bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
406
407		Node SygusTypeInfo::getConsNumOp(unsigned i) const
408		{
409		std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
410		if (itn != d_arg_ops.end())
411		{
412		return itn->second;
413		}
414		return Node::null();
415		}
416
417	2262	Node SygusTypeInfo::getConsNumConst(unsigned i) const
418		{
419	2262	std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
420	2262	if (itn != d_arg_const.end())
421		{
422	1226	return itn->second;
423		}
424	1036	return Node::null();
425		}
426
427	7501	Kind SygusTypeInfo::getConsNumKind(unsigned i) const
428		{
429	7501	std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
430	7501	if (itk != d_arg_kind.end())
431		{
432	3828	return itk->second;
433		}
434	3673	return UNDEFINED_KIND;
435		}
436
437		bool SygusTypeInfo::isKindArg(unsigned i) const
438		{
439		return getConsNumKind(i) != UNDEFINED_KIND;
440		}
441
442		bool SygusTypeInfo::isConstArg(unsigned i) const
443		{
444		return d_arg_const.find(i) != d_arg_const.end();
445		}
446
447	1755	int SygusTypeInfo::getAnyConstantConsNum() const
448		{
449	1755	return d_sym_cons_any_constant;
450		}
451
452	8545	bool SygusTypeInfo::hasSubtermSymbolicCons() const
453		{
454	8545	return d_has_subterm_sym_cons;
455		}
456
457	13	unsigned SygusTypeInfo::getSubclassForVar(Node n) const
458		{
459	13	std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
460	13	if (itcc == d_var_subclass_id.end())
461		{
462		Assert(false);
463		return 0;
464		}
465	13	return itcc->second;
466		}
467
468	8	unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
469		{
470		std::map<unsigned, std::vector<Node> >::const_iterator itvv =
471	8	d_var_subclass_list.find(sc);
472	8	if (itvv == d_var_subclass_list.end())
473		{
474		Assert(false);
475		return 0;
476		}
477	8	return itvv->second.size();
478		}
479	3	Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
480		{
481		std::map<unsigned, std::vector<Node> >::const_iterator itvv =
482	3	d_var_subclass_list.find(sc);
483	3	if (itvv == d_var_subclass_list.end() \|\| i >= itvv->second.size())
484		{
485		Assert(false);
486		return Node::null();
487		}
488	3	return itvv->second[i];
489		}
490
491	6	bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
492		{
493		std::map<Node, unsigned>::const_iterator itvv =
494	6	d_var_subclass_list_index.find(v);
495	6	if (itvv == d_var_subclass_list_index.end())
496		{
497		return false;
498		}
499	6	index = itvv->second;
500	6	return true;
501		}
502
503	1	bool SygusTypeInfo::isSubclassVarTrivial() const
504		{
505		for (const std::pair<const unsigned, std::vector<Node> >& p :
506	1	d_var_subclass_list)
507		{
508	1	if (p.second.size() > 1)
509		{
510	1	return false;
511		}
512		}
513		return true;
514		}
515
516		} // namespace quantifiers
517		} // namespace theory
518	29577	} // namespace cvc5