Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/nary_term_util.cpp	Lines:	1	135	0.7 %
Date:	2021-08-16	Branches:	2	445	0.4 %


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

#include "expr/nary_term_util.h"

#include "expr/attribute.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/strings/word.h"
#include "util/bitvector.h"
#include "util/rational.h"
#include "util/regexp.h"
#include "util/string.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace expr {

struct IsListTag
{
};
using IsListAttr = expr::Attribute<IsListTag, bool>;

void markListVar(TNode fv)
{
  Assert(fv.getKind() == BOUND_VARIABLE);
  fv.setAttribute(IsListAttr(), true);
}

bool isListVar(TNode fv) { return fv.getAttribute(IsListAttr()); }

bool hasListVar(TNode n)
{
  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited.insert(cur);
      if (isListVar(cur))
      {
        return true;
      }
      visit.insert(visit.end(), cur.begin(), cur.end());
    }
  } while (!visit.empty());
  return false;
}

bool getListVarContext(TNode n, std::map<Node, Kind>& context)
{
  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::map<Node, Kind>::iterator itc;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      visited.insert(cur);
      if (isListVar(cur))
      {
        // top-level list variable, undefined
        return false;
      }
      for (const Node& cn : cur)
      {
        if (isListVar(cn))
        {
          itc = context.find(cn);
          if (itc == context.end())
          {
            context[cn] = cur.getKind();
          }
          else if (itc->second != cur.getKind())
          {
            return false;
          }
          continue;
        }
        visit.push_back(cn);
      }
    }
  } while (!visit.empty());
  return true;
}

Node getNullTerminator(Kind k, TypeNode tn)
{
  NodeManager* nm = NodeManager::currentNM();
  Node nullTerm;
  switch (k)
  {
    case OR: nullTerm = nm->mkConst(false); break;
    case AND:
    case SEP_STAR: nullTerm = nm->mkConst(true); break;
    case PLUS: nullTerm = nm->mkConst(Rational(0)); break;
    case MULT:
    case NONLINEAR_MULT: nullTerm = nm->mkConst(Rational(1)); break;
    case STRING_CONCAT:
      // handles strings and sequences
      nullTerm = theory::strings::Word::mkEmptyWord(tn);
      break;
    case REGEXP_CONCAT:
      // the language containing only the empty string
      nullTerm = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
      break;
    case BITVECTOR_AND:
      nullTerm = theory::bv::utils::mkOnes(tn.getBitVectorSize());
      break;
    case BITVECTOR_OR:
    case BITVECTOR_ADD:
    case BITVECTOR_XOR:
      nullTerm = theory::bv::utils::mkZero(tn.getBitVectorSize());
      break;
    case BITVECTOR_MULT:
      nullTerm = theory::bv::utils::mkOne(tn.getBitVectorSize());
      break;
    default:
      // not handled as null-terminated
      break;
  }
  return nullTerm;
}

Node narySubstitute(Node src,
                    const std::vector<Node>& vars,
                    const std::vector<Node>& subs)
{
  // assumes all variables are list variables
  NodeManager* nm = NodeManager::currentNM();
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  std::vector<Node>::const_iterator itv;
  TNode cur;
  visit.push_back(src);
  do
  {
    cur = visit.back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      // if it is a non-list variable, do the replacement
      itv = std::find(vars.begin(), vars.end(), cur);
      if (itv != vars.end())
      {
        size_t d = std::distance(vars.begin(), itv);
        if (!isListVar(vars[d]))
        {
          visited[cur] = subs[d];
          continue;
        }
      }
      visited[cur] = Node::null();
      visit.insert(visit.end(), cur.begin(), cur.end());
      continue;
    }
    visit.pop_back();
    if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      for (const Node& cn : cur)
      {
        // if it is a list variable, insert the corresponding list as children;
        itv = std::find(vars.begin(), vars.end(), cn);
        if (itv != vars.end())
        {
          childChanged = true;
          size_t d = std::distance(vars.begin(), itv);
          Assert(d < subs.size());
          Node sd = subs[d];
          if (isListVar(vars[d]))
          {
            Assert(sd.getKind() == SEXPR);
            // add its children
            children.insert(children.end(), sd.begin(), sd.end());
          }
          else
          {
            children.push_back(sd);
          }
          continue;
        }
        it = visited.find(cn);
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cn != it->second;
        children.push_back(it->second);
      }
      if (childChanged)
      {
        if (children.size() != cur.getNumChildren())
        {
          // n-ary operators cannot be parameterized
          Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
          ret = children.empty()
                    ? getNullTerminator(cur.getKind(), cur.getType())
                    : (children.size() == 1
                           ? children[0]
                           : nm->mkNode(cur.getKind(), children));
        }
        else
        {
          if (cur.getMetaKind() == metakind::PARAMETERIZED)
          {
            children.insert(children.begin(), cur.getOperator());
          }
          ret = nm->mkNode(cur.getKind(), children);
        }
      }
      visited[cur] = ret;
    }

  } while (!visit.empty());
  Assert(visited.find(src) != visited.end());
  Assert(!visited.find(src)->second.isNull());
  return visited[src];
}

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Rewrite database
14		*/
15
16		#include "expr/nary_term_util.h"
17
18		#include "expr/attribute.h"
19		#include "theory/bv/theory_bv_utils.h"
20		#include "theory/strings/word.h"
21		#include "util/bitvector.h"
22		#include "util/rational.h"
23		#include "util/regexp.h"
24		#include "util/string.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace expr {
30
31		struct IsListTag
32		{
33		};
34		using IsListAttr = expr::Attribute<IsListTag, bool>;
35
36		void markListVar(TNode fv)
37		{
38		Assert(fv.getKind() == BOUND_VARIABLE);
39		fv.setAttribute(IsListAttr(), true);
40		}
41
42		bool isListVar(TNode fv) { return fv.getAttribute(IsListAttr()); }
43
44		bool hasListVar(TNode n)
45		{
46		std::unordered_set<TNode> visited;
47		std::unordered_set<TNode>::iterator it;
48		std::vector<TNode> visit;
49		TNode cur;
50		visit.push_back(n);
51		do
52		{
53		cur = visit.back();
54		visit.pop_back();
55		it = visited.find(cur);
56
57		if (it == visited.end())
58		{
59		visited.insert(cur);
60		if (isListVar(cur))
61		{
62		return true;
63		}
64		visit.insert(visit.end(), cur.begin(), cur.end());
65		}
66		} while (!visit.empty());
67		return false;
68		}
69
70		bool getListVarContext(TNode n, std::map<Node, Kind>& context)
71		{
72		std::unordered_set<TNode> visited;
73		std::unordered_set<TNode>::iterator it;
74		std::map<Node, Kind>::iterator itc;
75		std::vector<TNode> visit;
76		TNode cur;
77		visit.push_back(n);
78		do
79		{
80		cur = visit.back();
81		visit.pop_back();
82		it = visited.find(cur);
83		if (it == visited.end())
84		{
85		visited.insert(cur);
86		if (isListVar(cur))
87		{
88		// top-level list variable, undefined
89		return false;
90		}
91		for (const Node& cn : cur)
92		{
93		if (isListVar(cn))
94		{
95		itc = context.find(cn);
96		if (itc == context.end())
97		{
98		context[cn] = cur.getKind();
99		}
100		else if (itc->second != cur.getKind())
101		{
102		return false;
103		}
104		continue;
105		}
106		visit.push_back(cn);
107		}
108		}
109		} while (!visit.empty());
110		return true;
111		}
112
113		Node getNullTerminator(Kind k, TypeNode tn)
114		{
115		NodeManager* nm = NodeManager::currentNM();
116		Node nullTerm;
117		switch (k)
118		{
119		case OR: nullTerm = nm->mkConst(false); break;
120		case AND:
121		case SEP_STAR: nullTerm = nm->mkConst(true); break;
122		case PLUS: nullTerm = nm->mkConst(Rational(0)); break;
123		case MULT:
124		case NONLINEAR_MULT: nullTerm = nm->mkConst(Rational(1)); break;
125		case STRING_CONCAT:
126		// handles strings and sequences
127		nullTerm = theory::strings::Word::mkEmptyWord(tn);
128		break;
129		case REGEXP_CONCAT:
130		// the language containing only the empty string
131		nullTerm = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
132		break;
133		case BITVECTOR_AND:
134		nullTerm = theory::bv::utils::mkOnes(tn.getBitVectorSize());
135		break;
136		case BITVECTOR_OR:
137		case BITVECTOR_ADD:
138		case BITVECTOR_XOR:
139		nullTerm = theory::bv::utils::mkZero(tn.getBitVectorSize());
140		break;
141		case BITVECTOR_MULT:
142		nullTerm = theory::bv::utils::mkOne(tn.getBitVectorSize());
143		break;
144		default:
145		// not handled as null-terminated
146		break;
147		}
148		return nullTerm;
149		}
150
151		Node narySubstitute(Node src,
152		const std::vector<Node>& vars,
153		const std::vector<Node>& subs)
154		{
155		// assumes all variables are list variables
156		NodeManager* nm = NodeManager::currentNM();
157		std::unordered_map<TNode, Node> visited;
158		std::unordered_map<TNode, Node>::iterator it;
159		std::vector<TNode> visit;
160		std::vector<Node>::const_iterator itv;
161		TNode cur;
162		visit.push_back(src);
163		do
164		{
165		cur = visit.back();
166		it = visited.find(cur);
167		if (it == visited.end())
168		{
169		// if it is a non-list variable, do the replacement
170		itv = std::find(vars.begin(), vars.end(), cur);
171		if (itv != vars.end())
172		{
173		size_t d = std::distance(vars.begin(), itv);
174		if (!isListVar(vars[d]))
175		{
176		visited[cur] = subs[d];
177		continue;
178		}
179		}
180		visited[cur] = Node::null();
181		visit.insert(visit.end(), cur.begin(), cur.end());
182		continue;
183		}
184		visit.pop_back();
185		if (it->second.isNull())
186		{
187		Node ret = cur;
188		bool childChanged = false;
189		std::vector<Node> children;
190		for (const Node& cn : cur)
191		{
192		// if it is a list variable, insert the corresponding list as children;
193		itv = std::find(vars.begin(), vars.end(), cn);
194		if (itv != vars.end())
195		{
196		childChanged = true;
197		size_t d = std::distance(vars.begin(), itv);
198		Assert(d < subs.size());
199		Node sd = subs[d];
200		if (isListVar(vars[d]))
201		{
202		Assert(sd.getKind() == SEXPR);
203		// add its children
204		children.insert(children.end(), sd.begin(), sd.end());
205		}
206		else
207		{
208		children.push_back(sd);
209		}
210		continue;
211		}
212		it = visited.find(cn);
213		Assert(it != visited.end());
214		Assert(!it->second.isNull());
215		childChanged = childChanged \|\| cn != it->second;
216		children.push_back(it->second);
217		}
218		if (childChanged)
219		{
220		if (children.size() != cur.getNumChildren())
221		{
222		// n-ary operators cannot be parameterized
223		Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
224		ret = children.empty()
225		? getNullTerminator(cur.getKind(), cur.getType())
226		: (children.size() == 1
227		? children[0]
228		: nm->mkNode(cur.getKind(), children));
229		}
230		else
231		{
232		if (cur.getMetaKind() == metakind::PARAMETERIZED)
233		{
234		children.insert(children.begin(), cur.getOperator());
235		}
236		ret = nm->mkNode(cur.getKind(), children);
237		}
238		}
239		visited[cur] = ret;
240		}
241
242		} while (!visit.empty());
243		Assert(visited.find(src) != visited.end());
244		Assert(!visited.find(src)->second.isNull());
245		return visited[src];
246		}
247
248		} // namespace expr
249	29340	} // namespace cvc5