Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_canonize.cpp	Lines:	111	112	99.1 %
Date:	2021-11-07	Branches:	210	390	53.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, 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 term canonize.
 */

#include "expr/term_canonize.h"

#include <sstream>

// TODO #1216: move the code in this include
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace expr {

TermCanonize::TermCanonize(TypeClassCallback* tcc)
    : d_tcc(tcc), d_op_id_count(0), d_typ_id_count(0)
{
}

int TermCanonize::getIdForOperator(Node op)
{
  std::map<Node, int>::iterator it = d_op_id.find(op);
  if (it == d_op_id.end())
  {
    d_op_id[op] = d_op_id_count;
    d_op_id_count++;
    return d_op_id[op];
  }
  return it->second;
}

int TermCanonize::getIdForType(TypeNode t)
{
  std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
  if (it == d_typ_id.end())
  {
    d_typ_id[t] = d_typ_id_count;
    d_typ_id_count++;
    return d_typ_id[t];
  }
  return it->second;
}

bool TermCanonize::getTermOrder(Node a, Node b)
{
  if (a.getKind() == BOUND_VARIABLE)
  {
    if (b.getKind() == BOUND_VARIABLE)
    {
      return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
    }
    return true;
  }
  if (b.getKind() != BOUND_VARIABLE)
  {
    Node aop = a.hasOperator() ? a.getOperator() : a;
    Node bop = b.hasOperator() ? b.getOperator() : b;
    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
    if (aop == bop)
    {
      if (a.getNumChildren() == b.getNumChildren())
      {
        for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
        {
          if (a[i] != b[i])
          {
            // first distinct child determines the ordering
            return getTermOrder(a[i], b[i]);
          }
        }
      }
      else
      {
        return aop.getNumChildren() < bop.getNumChildren();
      }
    }
    else
    {
      return getIdForOperator(aop) < getIdForOperator(bop);
    }
  }
  return false;
}

Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc)
{
  Assert(!tn.isNull());
  NodeManager* nm = NodeManager::currentNM();
  std::pair<TypeNode, uint32_t> key(tn, tc);
  std::vector<Node>& tvars = d_cn_free_var[key];
  while (tvars.size() <= i)
  {
    std::stringstream oss;
    oss << tn;
    std::string typ_name = oss.str();
    while (typ_name[0] == '(')
    {
      typ_name.erase(typ_name.begin());
    }
    std::stringstream os;
    os << typ_name[0] << i;
    Node x = nm->mkBoundVar(os.str().c_str(), tn);
    d_fvIndex[x] = tvars.size();
    tvars.push_back(x);
  }
  return tvars[i];
}

uint32_t TermCanonize::getTypeClass(TNode v)
{
  return d_tcc == nullptr ? 0 : d_tcc->getTypeClass(v);
}

size_t TermCanonize::getIndexForFreeVariable(Node v) const
{
  std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
  if (it == d_fvIndex.end())
  {
    return 0;
  }
  return it->second;
}

struct sortTermOrder
{
  TermCanonize* d_tu;
  bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
};

Node TermCanonize::getCanonicalTerm(
    TNode n,
    bool apply_torder,
    bool doHoVar,
    std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
    std::map<TNode, Node>& visited)
{
  std::map<TNode, Node>::iterator it = visited.find(n);
  if (it != visited.end())
  {
    return it->second;
  }

  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
  if (n.getKind() == BOUND_VARIABLE)
  {
    uint32_t tc = getTypeClass(n);
    TypeNode tn = n.getType();
    std::pair<TypeNode, uint32_t> key(tn, tc);
    // allocate variable
    unsigned vn = var_count[key];
    var_count[key]++;
    Node fv = getCanonicalFreeVar(tn, vn, tc);
    visited[n] = fv;
    Trace("canon-term-debug") << "...allocate variable." << std::endl;
    return fv;
  }
  else if (n.getNumChildren() > 0)
  {
    // collect children
    Trace("canon-term-debug") << "Collect children" << std::endl;
    std::vector<Node> cchildren;
    for (const Node& cn : n)
    {
      cchildren.push_back(cn);
    }
    // if applicable, first sort by term order
    if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
    {
      Trace("canon-term-debug")
          << "Sort based on commutative operator " << n.getKind() << std::endl;
      sortTermOrder sto;
      sto.d_tu = this;
      std::sort(cchildren.begin(), cchildren.end(), sto);
    }
    // now make canonical
    Trace("canon-term-debug") << "Make canonical children" << std::endl;
    for (unsigned i = 0, size = cchildren.size(); i < size; i++)
    {
      cchildren[i] = getCanonicalTerm(
          cchildren[i], apply_torder, doHoVar, var_count, visited);
    }
    if (n.getMetaKind() == metakind::PARAMETERIZED)
    {
      Node op = n.getOperator();
      if (doHoVar)
      {
        op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
      }
      Trace("canon-term-debug") << "Insert operator " << op << std::endl;
      cchildren.insert(cchildren.begin(), op);
    }
    Trace("canon-term-debug")
        << "...constructing for " << n << "." << std::endl;
    Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
    Trace("canon-term-debug")
        << "...constructed " << ret << " for " << n << "." << std::endl;
    visited[n] = ret;
    return ret;
  }
  Trace("canon-term-debug") << "...return 0-child term." << std::endl;
  return n;
}

Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
{
  std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
  std::map<TNode, Node> visited;
  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
}

Node TermCanonize::getCanonicalTerm(TNode n,
                                    std::map<TNode, Node>& visited,
                                    bool apply_torder,
                                    bool doHoVar)
{
  std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, 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 term canonize.
14		*/
15
16		#include "expr/term_canonize.h"
17
18		#include <sstream>
19
20		// TODO #1216: move the code in this include
21		#include "theory/quantifiers/term_util.h"
22
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace expr {
27
28	12160	TermCanonize::TermCanonize(TypeClassCallback* tcc)
29	12160	: d_tcc(tcc), d_op_id_count(0), d_typ_id_count(0)
30		{
31	12160	}
32
33	316790	int TermCanonize::getIdForOperator(Node op)
34		{
35	316790	std::map<Node, int>::iterator it = d_op_id.find(op);
36	316790	if (it == d_op_id.end())
37		{
38	24953	d_op_id[op] = d_op_id_count;
39	24953	d_op_id_count++;
40	24953	return d_op_id[op];
41		}
42	291837	return it->second;
43		}
44
45	44972	int TermCanonize::getIdForType(TypeNode t)
46		{
47	44972	std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
48	44972	if (it == d_typ_id.end())
49		{
50	2102	d_typ_id[t] = d_typ_id_count;
51	2102	d_typ_id_count++;
52	2102	return d_typ_id[t];
53		}
54	42870	return it->second;
55		}
56
57	471381	bool TermCanonize::getTermOrder(Node a, Node b)
58		{
59	471381	if (a.getKind() == BOUND_VARIABLE)
60		{
61	57216	if (b.getKind() == BOUND_VARIABLE)
62		{
63	39140	return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
64		}
65	18076	return true;
66		}
67	414165	if (b.getKind() != BOUND_VARIABLE)
68		{
69	373502	Node aop = a.hasOperator() ? a.getOperator() : a;
70	373502	Node bop = b.hasOperator() ? b.getOperator() : b;
71	373315	Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
72	373315	Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
73	373315	if (aop == bop)
74		{
75	214920	if (a.getNumChildren() == b.getNumChildren())
76		{
77	268064	for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
78		{
79	267877	if (a[i] != b[i])
80		{
81		// first distinct child determines the ordering
82	208829	return getTermOrder(a[i], b[i]);
83		}
84		}
85		}
86		else
87		{
88	5904	return aop.getNumChildren() < bop.getNumChildren();
89		}
90		}
91		else
92		{
93	158395	return getIdForOperator(aop) < getIdForOperator(bop);
94		}
95		}
96	41037	return false;
97		}
98
99	115766	Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc)
100		{
101	115766	Assert(!tn.isNull());
102	115766	NodeManager* nm = NodeManager::currentNM();
103	231532	std::pair<TypeNode, uint32_t> key(tn, tc);
104	115766	std::vector<Node>& tvars = d_cn_free_var[key];
105	138982	while (tvars.size() <= i)
106		{
107	23216	std::stringstream oss;
108	11608	oss << tn;
109	23216	std::string typ_name = oss.str();
110	15876	while (typ_name[0] == '(')
111		{
112	2134	typ_name.erase(typ_name.begin());
113		}
114	23216	std::stringstream os;
115	11608	os << typ_name[0] << i;
116	23216	Node x = nm->mkBoundVar(os.str().c_str(), tn);
117	11608	d_fvIndex[x] = tvars.size();
118	11608	tvars.push_back(x);
119		}
120	231532	return tvars[i];
121		}
122
123	73786	uint32_t TermCanonize::getTypeClass(TNode v)
124		{
125	73786	return d_tcc == nullptr ? 0 : d_tcc->getTypeClass(v);
126		}
127
128	78280	size_t TermCanonize::getIndexForFreeVariable(Node v) const
129		{
130	78280	std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
131	78280	if (it == d_fvIndex.end())
132		{
133	78280	return 0;
134		}
135		return it->second;
136		}
137
138		struct sortTermOrder
139		{
140		TermCanonize* d_tu;
141	262552	bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
142		};
143
144	771337	Node TermCanonize::getCanonicalTerm(
145		TNode n,
146		bool apply_torder,
147		bool doHoVar,
148		std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
149		std::map<TNode, Node>& visited)
150		{
151	771337	std::map<TNode, Node>::iterator it = visited.find(n);
152	771337	if (it != visited.end())
153		{
154	168429	return it->second;
155		}
156
157	602908	Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
158	602908	if (n.getKind() == BOUND_VARIABLE)
159		{
160	73786	uint32_t tc = getTypeClass(n);
161	147572	TypeNode tn = n.getType();
162	147572	std::pair<TypeNode, uint32_t> key(tn, tc);
163		// allocate variable
164	73786	unsigned vn = var_count[key];
165	73786	var_count[key]++;
166	147572	Node fv = getCanonicalFreeVar(tn, vn, tc);
167	73786	visited[n] = fv;
168	73786	Trace("canon-term-debug") << "...allocate variable." << std::endl;
169	73786	return fv;
170		}
171	529122	else if (n.getNumChildren() > 0)
172		{
173		// collect children
174	300555	Trace("canon-term-debug") << "Collect children" << std::endl;
175	601110	std::vector<Node> cchildren;
176	923293	for (const Node& cn : n)
177		{
178	622738	cchildren.push_back(cn);
179		}
180		// if applicable, first sort by term order
181	300555	if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
182		{
183	202386	Trace("canon-term-debug")
184	101193	<< "Sort based on commutative operator " << n.getKind() << std::endl;
185		sortTermOrder sto;
186	101193	sto.d_tu = this;
187	101193	std::sort(cchildren.begin(), cchildren.end(), sto);
188		}
189		// now make canonical
190	300555	Trace("canon-term-debug") << "Make canonical children" << std::endl;
191	923293	for (unsigned i = 0, size = cchildren.size(); i < size; i++)
192		{
193	1245476	cchildren[i] = getCanonicalTerm(
194	622738	cchildren[i], apply_torder, doHoVar, var_count, visited);
195		}
196	300555	if (n.getMetaKind() == metakind::PARAMETERIZED)
197		{
198	241078	Node op = n.getOperator();
199	120539	if (doHoVar)
200		{
201	120539	op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
202		}
203	120539	Trace("canon-term-debug") << "Insert operator " << op << std::endl;
204	120539	cchildren.insert(cchildren.begin(), op);
205		}
206	601110	Trace("canon-term-debug")
207	300555	<< "...constructing for " << n << "." << std::endl;
208	601110	Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
209	601110	Trace("canon-term-debug")
210	300555	<< "...constructed " << ret << " for " << n << "." << std::endl;
211	300555	visited[n] = ret;
212	300555	return ret;
213		}
214	228567	Trace("canon-term-debug") << "...return 0-child term." << std::endl;
215	228567	return n;
216		}
217
218	12089	Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
219		{
220	24178	std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
221	24178	std::map<TNode, Node> visited;
222	24178	return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
223		}
224
225	15971	Node TermCanonize::getCanonicalTerm(TNode n,
226		std::map<TNode, Node>& visited,
227		bool apply_torder,
228		bool doHoVar)
229		{
230	31942	std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
231	31942	return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
232		}
233
234		} // namespace expr
235	31137	} // namespace cvc5