1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
/********************* */
/*! \file nary_builder.cpp
** \verbatim
** Top contributors (to current version):
** Tim King, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2016 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.\endverbatim
**
** \brief [[ 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 CVC4 {
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 unsigned int max = kind::metakind::getUpperBoundForKind(kind);
const unsigned int min = kind::metakind::getLowerBoundForKind(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_PLUS:
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 */
}/* CVC4 namespace */
|
