Head

GCC Code Coverage Report

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