GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt_util/nary_builder.cpp Lines: 11 99 11.1 %
Date: 2021-03-22 Branches: 11 315 3.5 %

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