Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/type_info.cpp	Lines:	203	240	84.6 %
Date:	2021-05-22	Branches:	336	818	41.1 %


/******************************************************************************
 * 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;
    }
  }
  // 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	1807	SygusTypeInfo::SygusTypeInfo()
33		: d_hasIte(false),
34		d_hasBoolConnective(false),
35		d_min_term_size(0),
36		d_sym_cons_any_constant(-1),
37	1807	d_has_subterm_sym_cons(false)
38		{
39	1807	}
40
41	1807	void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
42		{
43	1807	d_this = tn;
44	1807	Assert(tn.isDatatype());
45	1807	const DType& dt = tn.getDType();
46	1807	Assert(dt.isSygus());
47	1807	Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
48	3614	TypeNode btn = dt.getSygusType();
49	1807	d_btype = btn;
50	1807	Assert(!d_btype.isNull());
51		// get the sygus variable list
52	3614	Node var_list = dt.getSygusVarList();
53	1807	if (!var_list.isNull())
54		{
55	4340	for (unsigned j = 0; j < var_list.getNumChildren(); j++)
56		{
57	6214	Node sv = var_list[j];
58		SygusVarNumAttribute svna;
59	3107	sv.setAttribute(svna, j);
60	3107	d_var_list.push_back(sv);
61		}
62		}
63		else
64		{
65		// no arguments to synthesis functions
66	574	d_var_list.clear();
67		}
68
69		// compute min term size information: this must be computed before registering
70		// subfield types
71	1807	d_min_term_size = 1;
72	12305	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
73		{
74	10498	if (dt[i].getNumArgs() == 0)
75		{
76	4424	d_min_term_size = 0;
77		}
78		}
79
80		// register connected types
81	12305	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
82		{
83	22288	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
84		{
85	23580	TypeNode ctn = dt[i].getArgType(j);
86	11790	Trace("sygus-db") << " register subfield type " << ctn << std::endl;
87	11790	if (tds->registerSygusType(ctn))
88		{
89	11746	SygusTypeInfo& stic = tds->getTypeInfo(ctn);
90		// carry type attributes
91	11746	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	12305	for (unsigned i = 0; i < dt.getNumConstructors(); i++)
100		{
101	20996	Node sop = dt[i].getSygusOp();
102	10498	Assert(!sop.isNull());
103	10498	Trace("sygus-db") << " Operator #" << i << " : " << sop;
104	10498	Kind builtinKind = UNDEFINED_KIND;
105	10498	if (sop.getKind() == kind::BUILTIN)
106		{
107	3872	builtinKind = NodeManager::operatorToKind(sop);
108	3872	Trace("sygus-db") << ", kind = " << builtinKind;
109		}
110	6626	else if (sop.isConst() && dt[i].getNumArgs() == 0)
111		{
112	3076	Trace("sygus-db") << ", constant";
113	3076	d_consts[sop] = i;
114	3076	d_arg_const[i] = sop;
115		}
116	3550	else if (sop.getKind() == LAMBDA)
117		{
118		// do type checking
119	2078	Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
120	5990	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
121		{
122	7824	TypeNode ct = dt[i].getArgType(j);
123	7824	TypeNode cbt = tds->sygusToBuiltinType(ct);
124	7824	TypeNode lat = sop[0][j].getType();
125	7824	AlwaysAssert(cbt.isSubtypeOf(lat))
126	3912	<< "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	2078	if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED)
133		{
134	1703	size_t nchild = sop[0].getNumChildren();
135	1703	if (nchild == sop[1].getNumChildren())
136		{
137	1608	builtinKind = sop[1].getKind();
138	4753	for (size_t j = 0; j < nchild; j++)
139		{
140	3158	if (sop[0][j] != sop[1][j])
141		{
142		// arguments not in order
143	13	builtinKind = UNDEFINED_KIND;
144	13	break;
145		}
146		}
147		}
148		}
149		}
150	10498	if (builtinKind != UNDEFINED_KIND)
151		{
152	5467	d_kinds[builtinKind] = i;
153	5467	d_arg_kind[i] = builtinKind;
154		}
155		// symbolic constructors
156	10498	if (sop.getAttribute(SygusAnyConstAttribute()))
157		{
158	44	d_sym_cons_any_constant = i;
159	44	d_has_subterm_sym_cons = true;
160		}
161	10498	d_ops[sop] = i;
162	10498	d_arg_ops[i] = sop;
163	10498	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	20996	Node g = tds->mkGeneric(dt, i);
173	20996	TypeNode gtn = g.getType();
174	20996	AlwaysAssert(gtn.isSubtypeOf(btn))
175	10498	<< "Sygus datatype " << dt.getName()
176		<< " encodes terms that are not of type " << btn << std::endl;
177	10498	Trace("sygus-db") << "...done register Operator #" << i << std::endl;
178	10498	Kind gk = g.getKind();
179	10498	if (gk == ITE)
180		{
181		// mark that this type has an ITE
182	718	d_hasIte = true;
183	718	if (g.getType().isBoolean())
184		{
185	23	d_hasBoolConnective = true;
186		}
187		}
188	19083	else if (gk == AND \|\| gk == OR \|\| gk == IMPLIES \|\| gk == XOR
189	18599	\|\| (gk == EQUAL && g[0].getType().isBoolean()))
190		{
191	966	d_hasBoolConnective = true;
192		}
193		}
194		// compute minimum type depth information
195	1807	computeMinTypeDepthInternal(tn, 0);
196		// compute minimum term size information
197	1807	d_min_term_size = 1;
198	12305	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
199		{
200	10498	unsigned csize = 0;
201	10498	if (dt[i].getNumArgs() > 0)
202		{
203	6074	csize = 1;
204	17864	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
205		{
206	23580	TypeNode ct = dt[i].getArgType(j);
207	11790	if (ct == tn)
208		{
209	7714	csize += d_min_term_size;
210		}
211	4076	else if (tds->isRegistered(ct))
212		{
213	4032	SygusTypeInfo& stic = tds->getTypeInfo(ct);
214	4032	csize += stic.getMinTermSize();
215		}
216		else
217		{
218	44	Assert(!ct.isDatatype() \|\| !ct.getDType().isSygus());
219		}
220		}
221		}
222	10498	d_min_cons_term_size[i] = csize;
223		}
224	3614	Trace("sygus-db") << "Register type " << dt.getName() << " finished"
225	1807	<< std::endl;
226	1807	}
227
228	1	void SygusTypeInfo::initializeVarSubclasses()
229		{
230	1	if (d_var_list.empty())
231		{
232		// no variables
233		return;
234		}
235	1	if (!d_var_subclass_id.empty())
236		{
237		// already computed
238		return;
239		}
240		// compute variable subclasses
241	2	std::vector<TypeNode> sf_types;
242	1	getSubfieldTypes(sf_types);
243		// maps variables to the list of subfield types they occur in
244	2	std::map<Node, std::vector<TypeNode> > type_occurs;
245	3	for (const Node& v : d_var_list)
246		{
247	2	type_occurs[v].clear();
248		}
249		// for each type of subfield type of this enumerator
250	2	for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
251		{
252	2	std::vector<unsigned> rm_indices;
253	2	TypeNode stn = sf_types[i];
254	1	Assert(stn.isDatatype());
255	1	const DType& dt = stn.getDType();
256	4	for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
257		{
258	6	Node sopn = dt[j].getSygusOp();
259	3	Assert(!sopn.isNull());
260	3	if (type_occurs.find(sopn) != type_occurs.end())
261		{
262		// if it is a variable, store that it occurs in stn
263	2	type_occurs[sopn].push_back(stn);
264		}
265		}
266		}
267	2	TypeNodeIdTrie tnit;
268	3	for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
269		{
270	2	tnit.add(to.first, to.second);
271		}
272		// 0 is reserved for "no type class id"
273	1	unsigned typeIdCount = 1;
274	1	tnit.assignIds(d_var_subclass_id, typeIdCount);
275		// assign the list and reverse map to index
276	3	for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
277		{
278	4	Node v = to.first;
279	2	unsigned sc = d_var_subclass_id[v];
280	2	Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
281	2	d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
282	2	d_var_subclass_list[sc].push_back(v);
283		}
284		}
285
286	6640	TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }
287
288	129277	const std::vector<Node>& SygusTypeInfo::getVarList() const
289		{
290	129277	return d_var_list;
291		}
292
293	36011	void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
294		unsigned type_depth)
295		{
296	36011	std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
297	36011	if (it != d_min_type_depth.end() && type_depth >= it->second)
298		{
299		// no new information
300	62040	return;
301		}
302	5044	if (!tn.isDatatype())
303		{
304		// do not recurse to non-datatype types
305	106	return;
306		}
307	4938	const DType& dt = tn.getDType();
308	4938	if (!dt.isSygus())
309		{
310		// do not recurse to non-sygus datatype types
311		return;
312		}
313	4938	d_min_type_depth[tn] = type_depth;
314		// compute for connected types
315	33889	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
316		{
317	63155	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
318		{
319	68408	TypeNode at = dt[i].getArgType(j);
320	34204	computeMinTypeDepthInternal(at, type_depth + 1);
321		}
322		}
323		}
324
325		unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
326		{
327		std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
328		if (it != d_min_type_depth.end())
329		{
330		Assert(false);
331		return 0;
332		}
333		return it->second;
334		}
335
336	4032	unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }
337
338		unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
339		{
340		std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
341		if (it != d_min_cons_term_size.end())
342		{
343		return it->second;
344		}
345		Assert(false);
346		return 0;
347		}
348
349	477	void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
350		{
351	1491	for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
352		{
353	1014	sf_types.push_back(st.first);
354		}
355	477	}
356
357	16704	int SygusTypeInfo::getKindConsNum(Kind k) const
358		{
359	16704	std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
360	16704	if (it != d_kinds.end())
361		{
362	16499	return static_cast<int>(it->second);
363		}
364	205	return -1;
365		}
366
367	192	int SygusTypeInfo::getConstConsNum(Node n) const
368		{
369	192	std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
370	192	if (it != d_consts.end())
371		{
372	168	return static_cast<int>(it->second);
373		}
374	24	return -1;
375		}
376
377	6	int SygusTypeInfo::getOpConsNum(Node n) const
378		{
379	6	std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
380	6	if (it != d_ops.end())
381		{
382	6	return static_cast<int>(it->second);
383		}
384		return -1;
385		}
386
387	6827	bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
388	128	bool SygusTypeInfo::hasIte() const { return d_hasIte; }
389	88	bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; }
390	192	bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
391		bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
392
393		Node SygusTypeInfo::getConsNumOp(unsigned i) const
394		{
395		std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
396		if (itn != d_arg_ops.end())
397		{
398		return itn->second;
399		}
400		return Node::null();
401		}
402
403	2300	Node SygusTypeInfo::getConsNumConst(unsigned i) const
404		{
405	2300	std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
406	2300	if (itn != d_arg_const.end())
407		{
408	1250	return itn->second;
409		}
410	1050	return Node::null();
411		}
412
413	7819	Kind SygusTypeInfo::getConsNumKind(unsigned i) const
414		{
415	7819	std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
416	7819	if (itk != d_arg_kind.end())
417		{
418	4140	return itk->second;
419		}
420	3679	return UNDEFINED_KIND;
421		}
422
423		bool SygusTypeInfo::isKindArg(unsigned i) const
424		{
425		return getConsNumKind(i) != UNDEFINED_KIND;
426		}
427
428		bool SygusTypeInfo::isConstArg(unsigned i) const
429		{
430		return d_arg_const.find(i) != d_arg_const.end();
431		}
432
433	1710	int SygusTypeInfo::getAnyConstantConsNum() const
434		{
435	1710	return d_sym_cons_any_constant;
436		}
437
438	8220	bool SygusTypeInfo::hasSubtermSymbolicCons() const
439		{
440	8220	return d_has_subterm_sym_cons;
441		}
442
443	13	unsigned SygusTypeInfo::getSubclassForVar(Node n) const
444		{
445	13	std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
446	13	if (itcc == d_var_subclass_id.end())
447		{
448		Assert(false);
449		return 0;
450		}
451	13	return itcc->second;
452		}
453
454	8	unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
455		{
456		std::map<unsigned, std::vector<Node> >::const_iterator itvv =
457	8	d_var_subclass_list.find(sc);
458	8	if (itvv == d_var_subclass_list.end())
459		{
460		Assert(false);
461		return 0;
462		}
463	8	return itvv->second.size();
464		}
465	3	Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
466		{
467		std::map<unsigned, std::vector<Node> >::const_iterator itvv =
468	3	d_var_subclass_list.find(sc);
469	3	if (itvv == d_var_subclass_list.end() \|\| i >= itvv->second.size())
470		{
471		Assert(false);
472		return Node::null();
473		}
474	3	return itvv->second[i];
475		}
476
477	6	bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
478		{
479		std::map<Node, unsigned>::const_iterator itvv =
480	6	d_var_subclass_list_index.find(v);
481	6	if (itvv == d_var_subclass_list_index.end())
482		{
483		return false;
484		}
485	6	index = itvv->second;
486	6	return true;
487		}
488
489	1	bool SygusTypeInfo::isSubclassVarTrivial() const
490		{
491		for (const std::pair<const unsigned, std::vector<Node> >& p :
492	1	d_var_subclass_list)
493		{
494	1	if (p.second.size() > 1)
495		{
496	1	return false;
497		}
498		}
499		return true;
500		}
501
502		} // namespace quantifiers
503		} // namespace theory
504	28194	} // namespace cvc5