GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/arith_static_learner.cpp Lines: 130 155 83.9 %
Date: 2021-03-22 Branches: 355 915 38.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_static_learner.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Dejan Jovanovic, Morgan Deters
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
18
#include <vector>
19
20
#include "base/output.h"
21
#include "expr/node_algorithm.h"
22
#include "options/arith_options.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/arith/arith_static_learner.h"
25
#include "theory/arith/arith_utilities.h"
26
#include "theory/arith/normal_form.h"
27
#include "theory/rewriter.h"
28
29
using namespace std;
30
using namespace CVC4::kind;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace arith {
35
36
37
8995
ArithStaticLearner::ArithStaticLearner(context::Context* userContext) :
38
  d_minMap(userContext),
39
  d_maxMap(userContext),
40
8995
  d_statistics()
41
{
42
8995
}
43
44
8992
ArithStaticLearner::~ArithStaticLearner(){
45
8992
}
46
47
8995
ArithStaticLearner::Statistics::Statistics():
48
  d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
49
8995
  d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
50
{
51
8995
  smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications);
52
8995
  smtStatisticsRegistry()->registerStat(&d_iteConstantApplications);
53
8995
}
54
55
17984
ArithStaticLearner::Statistics::~Statistics(){
56
8992
  smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications);
57
8992
  smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
58
8992
}
59
60
91998
void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
61
62
183996
  vector<TNode> workList;
63
91998
  workList.push_back(n);
64
183996
  TNodeSet processed;
65
66
  //Contains an underapproximation of nodes that must hold.
67
183996
  TNodeSet defTrue;
68
69
91998
  defTrue.insert(n);
70
71
5731546
  while(!workList.empty()) {
72
2819774
    n = workList.back();
73
74
2819774
    bool unprocessedChildren = false;
75
8875758
    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
76
6055984
      if(processed.find(*i) == processed.end()) {
77
        // unprocessed child
78
1817847
        workList.push_back(*i);
79
1817847
        unprocessedChildren = true;
80
      }
81
    }
82
2819774
    if(n.getKind() == AND && defTrue.find(n) != defTrue.end() ){
83
826318
      for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
84
817210
        defTrue.insert(*i);
85
      }
86
    }
87
88
2819774
    if(unprocessedChildren) {
89
909929
      continue;
90
    }
91
92
1909845
    workList.pop_back();
93
    // has node n been processed in the meantime ?
94
1909845
    if(processed.find(n) != processed.end()) {
95
23099
      continue;
96
    }
97
1886746
    processed.insert(n);
98
99
1886746
    process(n,learned, defTrue);
100
101
  }
102
91998
}
103
104
105
1886746
void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
106
1886746
  Debug("arith::static") << "===================== looking at " << n << endl;
107
108
1886746
  switch(n.getKind()){
109
29942
  case ITE:
110
29942
    if (expr::hasBoundVar(n))
111
    {
112
      // Unsafe with non-ground ITEs; do nothing
113
9744
      Debug("arith::static")
114
4872
          << "(potentially) non-ground ITE, ignoring..." << endl;
115
4872
      break;
116
    }
117
118
85420
    if(n[0].getKind() != EQUAL &&
119
60350
       isRelationOperator(n[0].getKind())  ){
120
2101
      iteMinMax(n, learned);
121
    }
122
123
75210
    if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) ||
124
49810
       (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) {
125
1993
      iteConstant(n, learned);
126
    }
127
25070
    break;
128
129
91494
  case CONST_RATIONAL:
130
    // Mark constants as minmax
131
91494
    d_minMap.insert(n, n.getConst<Rational>());
132
91494
    d_maxMap.insert(n, n.getConst<Rational>());
133
91494
    break;
134
1765310
  default: // Do nothing
135
1765310
    break;
136
  }
137
1886746
}
138
139
2101
void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
140
2101
  Assert(n.getKind() == kind::ITE);
141
2101
  Assert(n[0].getKind() != EQUAL);
142
2101
  Assert(isRelationOperator(n[0].getKind()));
143
144
4202
  TNode c = n[0];
145
2101
  Kind k = oldSimplifiedKind(c);
146
4202
  TNode t = n[1];
147
4202
  TNode e = n[2];
148
4202
  TNode cleft = (c.getKind() == NOT) ? c[0][0] : c[0];
149
4202
  TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1];
150
151
2101
  if((t == cright) && (e == cleft)){
152
32
    TNode tmp = t;
153
16
    t = e;
154
16
    e = tmp;
155
16
    k = reverseRelationKind(k);
156
  }
157
  //(ite (< x y) x y)
158
  //(ite (x < y) x y)
159
  //(ite (x - y < 0) x y)
160
  // ----------------
161
  // (ite (x - y < -c) )
162
163
2101
  if(t == cleft && e == cright){
164
    // t == cleft && e == cright
165
16
    Assert(t == cleft);
166
16
    Assert(e == cright);
167
16
    switch(k){
168
16
    case LT:   // (ite (< x y) x y)
169
    case LEQ: { // (ite (<= x y) x y)
170
32
      Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
171
32
      Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
172
16
      Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
173
16
      learned << nLeqX << nLeqY;
174
16
      ++(d_statistics.d_iteMinMaxApplications);
175
16
      break;
176
    }
177
    case GT: // (ite (> x y) x y)
178
    case GEQ: { // (ite (>= x y) x y)
179
      Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
180
      Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
181
      Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
182
      learned << nGeqX << nGeqY;
183
      ++(d_statistics.d_iteMinMaxApplications);
184
      break;
185
    }
186
    default: Unreachable();
187
    }
188
  }
189
2101
}
190
191
1993
void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
192
1993
  Assert(n.getKind() == ITE);
193
194
1993
  Debug("arith::static") << "iteConstant(" << n << ")" << endl;
195
196
1993
  if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) {
197
3986
    const DeltaRational& first = d_minMap[n[1]];
198
3986
    const DeltaRational& second = d_minMap[n[2]];
199
3986
    DeltaRational min = std::min(first, second);
200
1993
    CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
201
1993
    if (minFind == d_minMap.end() || (*minFind).second < min) {
202
1679
      d_minMap.insert(n, min);
203
3358
      Node nGeqMin;
204
1679
      if (min.getInfinitesimalPart() == 0) {
205
1679
        nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
206
      } else {
207
        nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart());
208
      }
209
1679
      learned << nGeqMin;
210
1679
      Debug("arith::static") << n << " iteConstant"  << nGeqMin << endl;
211
1679
      ++(d_statistics.d_iteConstantApplications);
212
    }
213
  }
214
215
1993
  if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) {
216
3678
    const DeltaRational& first = d_maxMap[n[1]];
217
3678
    const DeltaRational& second = d_maxMap[n[2]];
218
3678
    DeltaRational max = std::max(first, second);
219
1839
    CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
220
1839
    if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
221
1549
      d_maxMap.insert(n, max);
222
3098
      Node nLeqMax;
223
1549
      if (max.getInfinitesimalPart() == 0) {
224
1549
        nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
225
      } else {
226
        nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart());
227
      }
228
1549
      learned << nLeqMax;
229
1549
      Debug("arith::static") << n << " iteConstant"  << nLeqMax << endl;
230
1549
      ++(d_statistics.d_iteConstantApplications);
231
    }
232
  }
233
1993
}
234
235
std::set<Node> listToSet(TNode l){
236
  std::set<Node> ret;
237
  while(l.getKind() == OR){
238
    Assert(l.getNumChildren() == 2);
239
    ret.insert(l[0]);
240
    l = l[1];
241
  }
242
  return ret;
243
}
244
245
2637
void ArithStaticLearner::addBound(TNode n) {
246
247
2637
  CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n[0]);
248
2637
  CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n[0]);
249
250
5274
  Rational constant = n[1].getConst<Rational>();
251
5274
  DeltaRational bound = constant;
252
253
2637
  switch(Kind k = n.getKind()) {
254
    case kind::LT: bound = DeltaRational(constant, -1); CVC4_FALLTHROUGH;
255
    case kind::LEQ:
256
      if (maxFind == d_maxMap.end() || (*maxFind).second > bound)
257
      {
258
        d_maxMap.insert(n[0], bound);
259
        Debug("arith::static") << "adding bound " << n << endl;
260
      }
261
      break;
262
    case kind::GT: bound = DeltaRational(constant, 1); CVC4_FALLTHROUGH;
263
2637
    case kind::GEQ:
264
2637
      if (minFind == d_minMap.end() || (*minFind).second < bound)
265
      {
266
2369
        d_minMap.insert(n[0], bound);
267
2369
        Debug("arith::static") << "adding bound " << n << endl;
268
      }
269
2637
      break;
270
    default: Unhandled() << k; break;
271
  }
272
2637
}
273
274
}/* CVC4::theory::arith namespace */
275
}/* CVC4::theory namespace */
276
26676
}/* CVC4 namespace */