Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_canonize.cpp	Lines:	100	101	99.0 %
Date:	2021-05-24	Branches:	200	366	54.6 %


/******************************************************************************
 * 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() : 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)
{
  Assert(!tn.isNull());
  NodeManager* nm = NodeManager::currentNM();
  while (d_cn_free_var[tn].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] = d_cn_free_var[tn].size();
    d_cn_free_var[tn].push_back(x);
  }
  return d_cn_free_var[tn][i];
}

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<TypeNode, 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)
  {
    TypeNode tn = n.getType();
    // allocate variable
    unsigned vn = var_count[tn];
    var_count[tn]++;
    Node fv = getCanonicalFreeVar(tn, vn);
    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<TypeNode, unsigned> var_count;
  std::map<TNode, Node> visited;
  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	6423	TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
29
30	286946	int TermCanonize::getIdForOperator(Node op)
31		{
32	286946	std::map<Node, int>::iterator it = d_op_id.find(op);
33	286946	if (it == d_op_id.end())
34		{
35	21023	d_op_id[op] = d_op_id_count;
36	21023	d_op_id_count++;
37	21023	return d_op_id[op];
38		}
39	265923	return it->second;
40		}
41
42	44028	int TermCanonize::getIdForType(TypeNode t)
43		{
44	44028	std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
45	44028	if (it == d_typ_id.end())
46		{
47	1934	d_typ_id[t] = d_typ_id_count;
48	1934	d_typ_id_count++;
49	1934	return d_typ_id[t];
50		}
51	42094	return it->second;
52		}
53
54	426287	bool TermCanonize::getTermOrder(Node a, Node b)
55		{
56	426287	if (a.getKind() == BOUND_VARIABLE)
57		{
58	52210	if (b.getKind() == BOUND_VARIABLE)
59		{
60	35529	return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
61		}
62	16681	return true;
63		}
64	374077	if (b.getKind() != BOUND_VARIABLE)
65		{
66	338696	Node aop = a.hasOperator() ? a.getOperator() : a;
67	338696	Node bop = b.hasOperator() ? b.getOperator() : b;
68	338562	Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
69	338562	Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
70	338562	if (aop == bop)
71		{
72	195089	if (a.getNumChildren() == b.getNumChildren())
73		{
74	246363	for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
75		{
76	246229	if (a[i] != b[i])
77		{
78		// first distinct child determines the ordering
79	189653	return getTermOrder(a[i], b[i]);
80		}
81		}
82		}
83		else
84		{
85	5302	return aop.getNumChildren() < bop.getNumChildren();
86		}
87		}
88		else
89		{
90	143473	return getIdForOperator(aop) < getIdForOperator(bop);
91		}
92		}
93	35649	return false;
94		}
95
96	112406	Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i)
97		{
98	112406	Assert(!tn.isNull());
99	112406	NodeManager* nm = NodeManager::currentNM();
100	131308	while (d_cn_free_var[tn].size() <= i)
101		{
102	18902	std::stringstream oss;
103	9451	oss << tn;
104	18902	std::string typ_name = oss.str();
105	12837	while (typ_name[0] == '(')
106		{
107	1693	typ_name.erase(typ_name.begin());
108		}
109	18902	std::stringstream os;
110	9451	os << typ_name[0] << i;
111	18902	Node x = nm->mkBoundVar(os.str().c_str(), tn);
112	9451	d_fvIndex[x] = d_cn_free_var[tn].size();
113	9451	d_cn_free_var[tn].push_back(x);
114		}
115	112406	return d_cn_free_var[tn][i];
116		}
117
118	71058	size_t TermCanonize::getIndexForFreeVariable(Node v) const
119		{
120	71058	std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
121	71058	if (it == d_fvIndex.end())
122		{
123	71058	return 0;
124		}
125		return it->second;
126		}
127
128		struct sortTermOrder
129		{
130		TermCanonize* d_tu;
131	236634	bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
132		};
133
134	726955	Node TermCanonize::getCanonicalTerm(TNode n,
135		bool apply_torder,
136		bool doHoVar,
137		std::map<TypeNode, unsigned>& var_count,
138		std::map<TNode, Node>& visited)
139		{
140	726955	std::map<TNode, Node>::iterator it = visited.find(n);
141	726955	if (it != visited.end())
142		{
143	157365	return it->second;
144		}
145
146	569590	Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
147	569590	if (n.getKind() == BOUND_VARIABLE)
148		{
149	140852	TypeNode tn = n.getType();
150		// allocate variable
151	70426	unsigned vn = var_count[tn];
152	70426	var_count[tn]++;
153	140852	Node fv = getCanonicalFreeVar(tn, vn);
154	70426	visited[n] = fv;
155	70426	Trace("canon-term-debug") << "...allocate variable." << std::endl;
156	70426	return fv;
157		}
158	499164	else if (n.getNumChildren() > 0)
159		{
160		// collect children
161	280570	Trace("canon-term-debug") << "Collect children" << std::endl;
162	561140	std::vector<Node> cchildren;
163	862017	for (const Node& cn : n)
164		{
165	581447	cchildren.push_back(cn);
166		}
167		// if applicable, first sort by term order
168	280570	if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
169		{
170	187788	Trace("canon-term-debug")
171	93894	<< "Sort based on commutative operator " << n.getKind() << std::endl;
172		sortTermOrder sto;
173	93894	sto.d_tu = this;
174	93894	std::sort(cchildren.begin(), cchildren.end(), sto);
175		}
176		// now make canonical
177	280570	Trace("canon-term-debug") << "Make canonical children" << std::endl;
178	862017	for (unsigned i = 0, size = cchildren.size(); i < size; i++)
179		{
180	1162894	cchildren[i] = getCanonicalTerm(
181	581447	cchildren[i], apply_torder, doHoVar, var_count, visited);
182		}
183	280570	if (n.getMetaKind() == metakind::PARAMETERIZED)
184		{
185	236972	Node op = n.getOperator();
186	118486	if (doHoVar)
187		{
188	118486	op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
189		}
190	118486	Trace("canon-term-debug") << "Insert operator " << op << std::endl;
191	118486	cchildren.insert(cchildren.begin(), op);
192		}
193	561140	Trace("canon-term-debug")
194	280570	<< "...constructing for " << n << "." << std::endl;
195	561140	Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
196	561140	Trace("canon-term-debug")
197	280570	<< "...constructed " << ret << " for " << n << "." << std::endl;
198	280570	visited[n] = ret;
199	280570	return ret;
200		}
201	218594	Trace("canon-term-debug") << "...return 0-child term." << std::endl;
202	218594	return n;
203		}
204
205	27022	Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
206		{
207	54044	std::map<TypeNode, unsigned> var_count;
208	54044	std::map<TNode, Node> visited;
209	54044	return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
210		}
211
212		} // namespace expr
213	28191	} // namespace cvc5