GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/monomial.cpp Lines: 162 168 96.4 %
Date: 2021-03-23 Branches: 251 522 48.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Andres Noetzli
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 Implementation of utilities for monomials
13
 **/
14
15
#include "theory/arith/nl/ext/monomial.h"
16
17
#include "theory/arith/arith_utilities.h"
18
#include "theory/arith/nl/nl_lemma_utils.h"
19
#include "theory/rewriter.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
28
// Returns a[key] if key is in a or value otherwise.
29
93224
unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value)
30
{
31
93224
  NodeMultiset::const_iterator it = a.find(key);
32
93224
  return (it == a.end()) ? value : it->second;
33
}
34
// Given two multisets return the multiset difference a \ b.
35
6548
NodeMultiset diffMultiset(const NodeMultiset& a, const NodeMultiset& b)
36
{
37
6548
  NodeMultiset difference;
38
17488
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
39
  {
40
21880
    Node key = it_a->first;
41
10940
    const unsigned a_value = it_a->second;
42
10940
    const unsigned b_value = getCountWithDefault(b, key, 0);
43
10940
    if (a_value > b_value)
44
    {
45
8517
      difference[key] = a_value - b_value;
46
    }
47
  }
48
6548
  return difference;
49
}
50
51
// Return a vector containing a[key] repetitions of key in a multiset a.
52
6548
std::vector<Node> ExpandMultiset(const NodeMultiset& a)
53
{
54
6548
  std::vector<Node> expansion;
55
15065
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
56
  {
57
8517
    expansion.insert(expansion.end(), it_a->second, it_a->first);
58
  }
59
6548
  return expansion;
60
}
61
62
// status 0 : n equal, -1 : n superset, 1 : n subset
63
77099
void MonomialIndex::addTerm(Node n,
64
                            const std::vector<Node>& reps,
65
                            MonomialDb* nla,
66
                            int status,
67
                            unsigned argIndex)
68
{
69
77099
  if (status == 0)
70
  {
71
8652
    if (argIndex == reps.size())
72
    {
73
3992
      d_monos.push_back(n);
74
    }
75
    else
76
    {
77
4660
      d_data[reps[argIndex]].addTerm(n, reps, nla, status, argIndex + 1);
78
    }
79
  }
80
150264
  for (std::map<Node, MonomialIndex>::iterator it = d_data.begin();
81
150264
       it != d_data.end();
82
       ++it)
83
  {
84
73165
    if (status != 0 || argIndex == reps.size() || it->first != reps[argIndex])
85
    {
86
      // if we do not contain this variable, then if we were a superset,
87
      // fail (-2), otherwise we are subset.  if we do contain this
88
      // variable, then if we were equal, we are superset since variables
89
      // are ordered, otherwise we remain the same.
90
      int new_status =
91
137010
          std::find(reps.begin(), reps.end(), it->first) == reps.end()
92
70106
              ? (status >= 0 ? 1 : -2)
93
70106
              : (status == 0 ? -1 : status);
94
68505
      if (new_status != -2)
95
      {
96
68447
        it->second.addTerm(n, reps, nla, new_status, argIndex);
97
      }
98
    }
99
  }
100
  // compare for subsets
101
152500
  for (unsigned i = 0; i < d_monos.size(); i++)
102
  {
103
150802
    Node m = d_monos[i];
104
75401
    if (m != n)
105
    {
106
      // we are superset if we are equal and haven't traversed all variables
107
71409
      int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status;
108
142818
      Trace("nl-ext-mindex-debug") << "  compare " << n << " and " << m
109
71409
                                   << ", status = " << cstatus << std::endl;
110
71409
      if (cstatus <= 0 && nla->isMonomialSubset(m, n))
111
      {
112
3680
        nla->registerMonomialSubset(m, n);
113
3680
        Trace("nl-ext-mindex-debug") << "...success" << std::endl;
114
      }
115
67729
      else if (cstatus >= 0 && nla->isMonomialSubset(n, m))
116
      {
117
2868
        nla->registerMonomialSubset(n, m);
118
2868
        Trace("nl-ext-mindex-debug") << "...success (rev)" << std::endl;
119
      }
120
    }
121
  }
122
77099
}
123
124
4391
MonomialDb::MonomialDb()
125
{
126
4391
  d_one = NodeManager::currentNM()->mkConst(Rational(1));
127
4391
}
128
129
49242
void MonomialDb::registerMonomial(Node n)
130
{
131
49242
  if (std::find(d_monomials.begin(), d_monomials.end(), n) != d_monomials.end())
132
  {
133
45250
    return;
134
  }
135
3992
  d_monomials.push_back(n);
136
3992
  Trace("nl-ext-debug") << "Register monomial : " << n << std::endl;
137
3992
  Kind k = n.getKind();
138
3992
  if (k == NONLINEAR_MULT)
139
  {
140
    // get exponent count
141
1200
    unsigned nchild = n.getNumChildren();
142
4162
    for (unsigned i = 0; i < nchild; i++)
143
    {
144
2962
      d_m_exp[n][n[i]]++;
145
2962
      if (i == 0 || n[i] != n[i - 1])
146
      {
147
2273
        d_m_vlist[n].push_back(n[i]);
148
      }
149
    }
150
1200
    d_m_degree[n] = nchild;
151
  }
152
2792
  else if (n == d_one)
153
  {
154
405
    d_m_exp[n].clear();
155
405
    d_m_vlist[n].clear();
156
405
    d_m_degree[n] = 0;
157
  }
158
  else
159
  {
160
2387
    Assert(k != PLUS && k != MULT);
161
2387
    d_m_exp[n][n] = 1;
162
2387
    d_m_vlist[n].push_back(n);
163
2387
    d_m_degree[n] = 1;
164
  }
165
3992
  std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end());
166
3992
  Trace("nl-ext-mindex") << "Add monomial to index : " << n << std::endl;
167
3992
  d_m_index.addTerm(n, d_m_vlist[n], this);
168
}
169
170
6548
void MonomialDb::registerMonomialSubset(Node a, Node b)
171
{
172
6548
  Assert(isMonomialSubset(a, b));
173
174
6548
  const NodeMultiset& a_exponent_map = getMonomialExponentMap(a);
175
6548
  const NodeMultiset& b_exponent_map = getMonomialExponentMap(b);
176
177
  std::vector<Node> diff_children =
178
13096
      ExpandMultiset(diffMultiset(b_exponent_map, a_exponent_map));
179
6548
  Assert(!diff_children.empty());
180
181
6548
  d_m_contain_parent[a].push_back(b);
182
6548
  d_m_contain_children[b].push_back(a);
183
184
13096
  Node mult_term = safeConstructNary(MULT, diff_children);
185
13096
  Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children);
186
6548
  d_m_contain_mult[a][b] = mult_term;
187
6548
  d_m_contain_umult[a][b] = nlmult_term;
188
13096
  Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b
189
6548
                         << ", difference is " << mult_term << std::endl;
190
6548
}
191
192
78415
bool MonomialDb::isMonomialSubset(Node am, Node bm) const
193
{
194
78415
  const NodeMultiset& a = getMonomialExponentMap(am);
195
78415
  const NodeMultiset& b = getMonomialExponentMap(bm);
196
86702
  for (NodeMultiset::const_iterator it_a = a.begin(); it_a != a.end(); ++it_a)
197
  {
198
81893
    Node key = it_a->first;
199
73606
    const unsigned a_value = it_a->second;
200
73606
    const unsigned b_value = getCountWithDefault(b, key, 0);
201
73606
    if (a_value > b_value)
202
    {
203
65319
      return false;
204
    }
205
  }
206
13096
  return true;
207
}
208
209
213929
const NodeMultiset& MonomialDb::getMonomialExponentMap(Node monomial) const
210
{
211
213929
  MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
212
213929
  Assert(it != d_m_exp.end());
213
213929
  return it->second;
214
}
215
216
306604
unsigned MonomialDb::getExponent(Node monomial, Node v) const
217
{
218
306604
  MonomialExponentMap::const_iterator it = d_m_exp.find(monomial);
219
306604
  if (it == d_m_exp.end())
220
  {
221
    return 0;
222
  }
223
306604
  std::map<Node, unsigned>::const_iterator itv = it->second.find(v);
224
306604
  if (itv == it->second.end())
225
  {
226
    return 0;
227
  }
228
306604
  return itv->second;
229
}
230
231
540781
const std::vector<Node>& MonomialDb::getVariableList(Node monomial) const
232
{
233
  std::map<Node, std::vector<Node> >::const_iterator itvl =
234
540781
      d_m_vlist.find(monomial);
235
540781
  Assert(itvl != d_m_vlist.end());
236
540781
  return itvl->second;
237
}
238
239
19612
unsigned MonomialDb::getDegree(Node monomial) const
240
{
241
19612
  std::map<Node, unsigned>::const_iterator it = d_m_degree.find(monomial);
242
19612
  Assert(it != d_m_degree.end());
243
19612
  return it->second;
244
}
245
246
520
void MonomialDb::sortByDegree(std::vector<Node>& ms) const
247
{
248
520
  SortNonlinearDegree snlad(d_m_degree);
249
520
  std::sort(ms.begin(), ms.end(), snlad);
250
520
}
251
252
1535
void MonomialDb::sortVariablesByModel(std::vector<Node>& ms, NlModel& m)
253
{
254
1535
  SortNlModel smv;
255
1535
  smv.d_nlm = &m;
256
1535
  smv.d_isConcrete = false;
257
1535
  smv.d_isAbsolute = true;
258
1535
  smv.d_reverse_order = true;
259
10675
  for (const Node& msc : ms)
260
  {
261
9140
    std::sort(d_m_vlist[msc].begin(), d_m_vlist[msc].end(), smv);
262
  }
263
1535
}
264
265
15
const std::map<Node, std::vector<Node> >& MonomialDb::getContainsChildrenMap()
266
{
267
15
  return d_m_contain_children;
268
}
269
270
520
const std::map<Node, std::vector<Node> >& MonomialDb::getContainsParentMap()
271
{
272
520
  return d_m_contain_parent;
273
}
274
275
56063
Node MonomialDb::getContainsDiff(Node a, Node b) const
276
{
277
  std::map<Node, std::map<Node, Node> >::const_iterator it =
278
56063
      d_m_contain_mult.find(a);
279
56063
  if (it == d_m_contain_mult.end())
280
  {
281
    return Node::null();
282
  }
283
56063
  std::map<Node, Node>::const_iterator it2 = it->second.find(b);
284
56063
  if (it2 == it->second.end())
285
  {
286
    return Node::null();
287
  }
288
56063
  return it2->second;
289
}
290
291
38
Node MonomialDb::getContainsDiffNl(Node a, Node b) const
292
{
293
  std::map<Node, std::map<Node, Node> >::const_iterator it =
294
38
      d_m_contain_umult.find(a);
295
38
  if (it == d_m_contain_umult.end())
296
  {
297
    return Node::null();
298
  }
299
38
  std::map<Node, Node>::const_iterator it2 = it->second.find(b);
300
38
  if (it2 == it->second.end())
301
  {
302
    return Node::null();
303
  }
304
38
  return it2->second;
305
}
306
307
5300
Node MonomialDb::mkMonomialRemFactor(Node n,
308
                                     const NodeMultiset& n_exp_rem) const
309
{
310
10600
  std::vector<Node> children;
311
5300
  const NodeMultiset& exponent_map = getMonomialExponentMap(n);
312
13978
  for (NodeMultiset::const_iterator itme2 = exponent_map.begin();
313
13978
       itme2 != exponent_map.end();
314
       ++itme2)
315
  {
316
17356
    Node v = itme2->first;
317
8678
    unsigned inc = itme2->second;
318
17356
    Trace("nl-ext-mono-factor")
319
8678
        << "..." << inc << " factors of " << v << std::endl;
320
8678
    unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0);
321
8678
    Assert(count_in_n_exp_rem <= inc);
322
8678
    inc -= count_in_n_exp_rem;
323
17356
    Trace("nl-ext-mono-factor")
324
8678
        << "......rem, now " << inc << " factors of " << v << std::endl;
325
8678
    children.insert(children.end(), inc, v);
326
  }
327
5300
  Node ret = safeConstructNary(MULT, children);
328
5300
  ret = Rewriter::rewrite(ret);
329
5300
  Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
330
10600
  return ret;
331
}
332
333
}  // namespace nl
334
}  // namespace arith
335
}  // namespace theory
336
26685
}  // namespace CVC4