Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt_util/nary_builder.cpp	Lines:	11	99	11.1 %
Date:	2021-05-21	Branches:	11	315	3.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Aina Niemetz, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */
#include "smt_util/nary_builder.h"

#include "expr/metakind.h"

using namespace std;

namespace cvc5 {
namespace util {

Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children)
{
  if (children.size() == 0)
  {
    return zeroArity(kind);
  }
  else if (children.size() == 1)
  {
    return children[0];
  }
  else
  {
    const uint32_t max = kind::metakind::getMaxArityForKind(kind);
    const uint32_t min = kind::metakind::getMinArityForKind(kind);

    Assert(min <= children.size());

    unsigned int numChildren = children.size();
    NodeManager* nm = NodeManager::currentNM();
    if( numChildren <= max ) {
      return nm->mkNode(kind,children);
    }

    typedef std::vector<Node>::const_iterator const_iterator;
    const_iterator it = children.begin() ;
    const_iterator end = children.end() ;

    /* The new top-level children and the children of each sub node */
    std::vector<Node> newChildren;
    std::vector<Node> subChildren;

    while( it != end && numChildren > max ) {
      /* Grab the next max children and make a node for them. */
      for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
        subChildren.push_back(*it);
      }
      Node subNode = nm->mkNode(kind,subChildren);
      newChildren.push_back(subNode);
      subChildren.clear();
    }

    /* If there's children left, "top off" the Expr. */
    if(numChildren > 0) {
      /* If the leftovers are too few, just copy them into newChildren;
       * otherwise make a new sub-node  */
      if(numChildren < min) {
        for(; it != end; ++it) {
          newChildren.push_back(*it);
        }
      } else {
        for(; it != end; ++it) {
          subChildren.push_back(*it);
        }
        Node subNode = nm->mkNode(kind, subChildren);
        newChildren.push_back(subNode);
      }
    }

    /* It's inconceivable we could have enough children for this to fail
     * (more than 2^32, in most cases?). */
    AlwaysAssert(newChildren.size() <= max)
        << "Too many new children in mkAssociative";

    /* It would be really weird if this happened (it would require
     * min > 2, for one thing), but let's make sure. */
    AlwaysAssert(newChildren.size() >= min)
        << "Too few new children in mkAssociative";

    return nm->mkNode(kind,newChildren);
  }
}

Node NaryBuilder::zeroArity(Kind k){
  using namespace kind;
  NodeManager* nm = NodeManager::currentNM();
  switch(k){
  case AND:
    return nm->mkConst(true);
  case OR:
    return nm->mkConst(false);
  case PLUS:
    return nm->mkConst(Rational(0));
  case MULT:
    return nm->mkConst(Rational(1));
  default:
    return Node::null();
  }
}


RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
  : d_cache()
{}
RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }

bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
  using namespace kind;
  switch(k){
  case BITVECTOR_CONCAT:
  case BITVECTOR_AND:
  case BITVECTOR_OR:
  case BITVECTOR_XOR:
  case BITVECTOR_MULT:
  case BITVECTOR_ADD:
  case DISTINCT:
  case PLUS:
  case MULT:
  case AND:
  case OR:
    return true;
  default:
    return false;
  }
}

Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
  if(d_cache.find(n) != d_cache.end()){
    return d_cache[n];
  }
  Node result =
    isAssociateCommutative(n.getKind()) ?
    case_assoccomm(n) : case_other(n);

  d_cache[n] = result;
  return result;
}

Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
  Kind k = n.getKind();
  Assert(isAssociateCommutative(k));
  Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
  unsigned N = n.getNumChildren();
  Assert(N >= 2);

  Node last = rePairAssocCommutativeOperators( n[N-1]);
  Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);

  NodeManager* nm = NodeManager::currentNM();
  Node last2 = nm->mkNode(k, nextToLast, last);

  if(N <= 2){
    return last2;
  } else{
    Assert(N > 2);
    Node prevRound = last2;
    for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
      unsigned currPos = prevPos-1;
      Node curr = rePairAssocCommutativeOperators(n[currPos]);
      Node round = nm->mkNode(k, curr, prevRound);
      prevRound = round;
    }
    return prevRound;
  }
}

Node RePairAssocCommutativeOperators::case_other(TNode n){
  if(n.isConst() || n.isVar()){
    return n;
  }

  NodeBuilder nb(n.getKind());

  if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
    nb << n.getOperator();
  }

  // Remove the ITEs from the children
  for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
    Node newChild = rePairAssocCommutativeOperators(*i);
    nb << newChild;
  }

  Node result = (Node)nb;
  return result;
}

}/* util namespace */
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Aina Niemetz, Mathias Preiner
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18		#include "smt_util/nary_builder.h"
19
20		#include "expr/metakind.h"
21
22		using namespace std;
23
24		namespace cvc5 {
25		namespace util {
26
27	2	Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children)
28		{
29	2	if (children.size() == 0)
30		{
31		return zeroArity(kind);
32		}
33	2	else if (children.size() == 1)
34		{
35		return children[0];
36		}
37		else
38		{
39	2	const uint32_t max = kind::metakind::getMaxArityForKind(kind);
40	2	const uint32_t min = kind::metakind::getMinArityForKind(kind);
41
42	2	Assert(min <= children.size());
43
44	2	unsigned int numChildren = children.size();
45	2	NodeManager* nm = NodeManager::currentNM();
46	2	if( numChildren <= max ) {
47	2	return nm->mkNode(kind,children);
48		}
49
50		typedef std::vector<Node>::const_iterator const_iterator;
51		const_iterator it = children.begin() ;
52		const_iterator end = children.end() ;
53
54		/* The new top-level children and the children of each sub node */
55		std::vector<Node> newChildren;
56		std::vector<Node> subChildren;
57
58		while( it != end && numChildren > max ) {
59		/* Grab the next max children and make a node for them. */
60		for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
61		subChildren.push_back(*it);
62		}
63		Node subNode = nm->mkNode(kind,subChildren);
64		newChildren.push_back(subNode);
65		subChildren.clear();
66		}
67
68		/* If there's children left, "top off" the Expr. */
69		if(numChildren > 0) {
70		/* If the leftovers are too few, just copy them into newChildren;
71		* otherwise make a new sub-node */
72		if(numChildren < min) {
73		for(; it != end; ++it) {
74		newChildren.push_back(*it);
75		}
76		} else {
77		for(; it != end; ++it) {
78		subChildren.push_back(*it);
79		}
80		Node subNode = nm->mkNode(kind, subChildren);
81		newChildren.push_back(subNode);
82		}
83		}
84
85		/* It's inconceivable we could have enough children for this to fail
86		* (more than 2^32, in most cases?). */
87		AlwaysAssert(newChildren.size() <= max)
88		<< "Too many new children in mkAssociative";
89
90		/* It would be really weird if this happened (it would require
91		* min > 2, for one thing), but let's make sure. */
92		AlwaysAssert(newChildren.size() >= min)
93		<< "Too few new children in mkAssociative";
94
95		return nm->mkNode(kind,newChildren);
96		}
97		}
98
99		Node NaryBuilder::zeroArity(Kind k){
100		using namespace kind;
101		NodeManager* nm = NodeManager::currentNM();
102		switch(k){
103		case AND:
104		return nm->mkConst(true);
105		case OR:
106		return nm->mkConst(false);
107		case PLUS:
108		return nm->mkConst(Rational(0));
109		case MULT:
110		return nm->mkConst(Rational(1));
111		default:
112		return Node::null();
113		}
114		}
115
116
117		RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
118		: d_cache()
119		{}
120		RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
121		size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
122		void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
123
124		bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
125		using namespace kind;
126		switch(k){
127		case BITVECTOR_CONCAT:
128		case BITVECTOR_AND:
129		case BITVECTOR_OR:
130		case BITVECTOR_XOR:
131		case BITVECTOR_MULT:
132		case BITVECTOR_ADD:
133		case DISTINCT:
134		case PLUS:
135		case MULT:
136		case AND:
137		case OR:
138		return true;
139		default:
140		return false;
141		}
142		}
143
144		Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
145		if(d_cache.find(n) != d_cache.end()){
146		return d_cache[n];
147		}
148		Node result =
149		isAssociateCommutative(n.getKind()) ?
150		case_assoccomm(n) : case_other(n);
151
152		d_cache[n] = result;
153		return result;
154		}
155
156		Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
157		Kind k = n.getKind();
158		Assert(isAssociateCommutative(k));
159		Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
160		unsigned N = n.getNumChildren();
161		Assert(N >= 2);
162
163		Node last = rePairAssocCommutativeOperators( n[N-1]);
164		Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
165
166		NodeManager* nm = NodeManager::currentNM();
167		Node last2 = nm->mkNode(k, nextToLast, last);
168
169		if(N <= 2){
170		return last2;
171		} else{
172		Assert(N > 2);
173		Node prevRound = last2;
174		for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
175		unsigned currPos = prevPos-1;
176		Node curr = rePairAssocCommutativeOperators(n[currPos]);
177		Node round = nm->mkNode(k, curr, prevRound);
178		prevRound = round;
179		}
180		return prevRound;
181		}
182		}
183
184		Node RePairAssocCommutativeOperators::case_other(TNode n){
185		if(n.isConst() \|\| n.isVar()){
186		return n;
187		}
188
189		NodeBuilder nb(n.getKind());
190
191		if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
192		nb << n.getOperator();
193		}
194
195		// Remove the ITEs from the children
196		for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
197		Node newChild = rePairAssocCommutativeOperators(*i);
198		nb << newChild;
199		}
200
201		Node result = (Node)nb;
202		return result;
203		}
204
205		}/* util namespace */
206	27735	} // namespace cvc5