GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/monomial_bounds_check.cpp Lines: 168 294 57.1 %
Date: 2021-03-22 Branches: 353 1198 29.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial_bounds_check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Tim King
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 Check for monomial bound inference lemmas
13
 **/
14
15
#include "theory/arith/nl/ext/monomial_bounds_check.h"
16
17
#include "expr/node.h"
18
#include "expr/proof.h"
19
#include "options/arith_options.h"
20
#include "theory/arith/arith_msum.h"
21
#include "theory/arith/arith_utilities.h"
22
#include "theory/arith/inference_manager.h"
23
#include "theory/arith/nl/ext/ext_state.h"
24
#include "theory/arith/nl/nl_model.h"
25
#include "theory/rewriter.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace arith {
30
namespace nl {
31
32
namespace {
33
void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs)
34
{
35
  Node t = ArithMSum::mkCoeffTerm(coeff, x);
36
  Trace(c) << t << " " << type << " " << rhs;
37
}
38
39
2441
bool hasNewMonomials(Node n, const std::vector<Node>& existing)
40
{
41
4882
  std::set<Node> visited;
42
43
4882
  std::vector<Node> worklist;
44
2441
  worklist.push_back(n);
45
48953
  while (!worklist.empty())
46
  {
47
48332
    Node current = worklist.back();
48
25076
    worklist.pop_back();
49
25076
    if (visited.find(current) == visited.end())
50
    {
51
23217
      visited.insert(current);
52
23217
      if (current.getKind() == Kind::NONLINEAR_MULT)
53
      {
54
11343
        if (std::find(existing.begin(), existing.end(), current)
55
11343
            == existing.end())
56
        {
57
1820
          return true;
58
        }
59
      }
60
      else
61
      {
62
19436
        worklist.insert(worklist.end(), current.begin(), current.end());
63
      }
64
    }
65
  }
66
621
  return false;
67
}
68
}  // namespace
69
70
4389
MonomialBoundsCheck::MonomialBoundsCheck(ExtState* data)
71
4389
    : d_data(data), d_cdb(d_data->d_mdb)
72
{
73
4389
}
74
75
2742
void MonomialBoundsCheck::init()
76
{
77
2742
  d_ci.clear();
78
2742
  d_ci_exp.clear();
79
2742
  d_ci_max.clear();
80
2742
}
81
82
520
void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
83
                                      const std::vector<Node>& false_asserts)
84
{
85
  // sort monomials by degree
86
520
  Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl;
87
520
  d_data->d_mdb.sortByDegree(d_data->d_ms);
88
  // all monomials
89
2080
  d_data->d_mterms.insert(d_data->d_mterms.end(),
90
520
                          d_data->d_ms_vars.begin(),
91
2080
                          d_data->d_ms_vars.end());
92
1040
  d_data->d_mterms.insert(
93
1040
      d_data->d_mterms.end(), d_data->d_ms.begin(), d_data->d_ms.end());
94
95
  const std::map<Node, std::map<Node, ConstraintInfo> >& cim =
96
520
      d_cdb.getConstraints();
97
98
520
  NodeManager* nm = NodeManager::currentNM();
99
  // register constraints
100
520
  Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
101
35453
  for (const Node& lit : asserts)
102
  {
103
34933
    bool polarity = lit.getKind() != Kind::NOT;
104
69866
    Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
105
34933
    d_cdb.registerConstraint(atom);
106
    bool is_false_lit =
107
69866
        std::find(false_asserts.begin(), false_asserts.end(), lit)
108
104799
        != false_asserts.end();
109
    // add information about bounds to variables
110
    std::map<Node, std::map<Node, ConstraintInfo> >::const_iterator itc =
111
34933
        cim.find(atom);
112
34933
    if (itc == cim.end())
113
    {
114
      continue;
115
    }
116
98510
    for (const std::pair<const Node, ConstraintInfo>& itcc : itc->second)
117
    {
118
127154
      Node x = itcc.first;
119
127154
      Node coeff = itcc.second.d_coeff;
120
127154
      Node rhs = itcc.second.d_rhs;
121
63577
      Kind type = itcc.second.d_type;
122
127154
      Node exp = lit;
123
63577
      if (!polarity)
124
      {
125
        // reverse
126
37615
        if (type == Kind::EQUAL)
127
        {
128
          // we will take the strict inequality in the direction of the
129
          // model
130
29664
          Node lhs = ArithMSum::mkCoeffTerm(coeff, x);
131
29664
          Node query = nm->mkNode(Kind::GT, lhs, rhs);
132
29664
          Node query_mv = d_data->d_model.computeAbstractModelValue(query);
133
14832
          if (query_mv == d_data->d_true)
134
          {
135
9746
            exp = query;
136
9746
            type = Kind::GT;
137
          }
138
          else
139
          {
140
5086
            Assert(query_mv == d_data->d_false);
141
5086
            exp = nm->mkNode(Kind::LT, lhs, rhs);
142
5086
            type = Kind::LT;
143
          }
144
        }
145
        else
146
        {
147
22783
          type = negateKind(type);
148
        }
149
      }
150
      // add to status if maximal degree
151
63577
      d_ci_max[x][coeff][rhs] = d_cdb.isMaximal(atom, x);
152
63577
      if (Trace.isOn("nl-ext-bound-debug2"))
153
      {
154
        Node t = ArithMSum::mkCoeffTerm(coeff, x);
155
        Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " "
156
                                     << rhs << " by " << exp << std::endl;
157
      }
158
63577
      bool updated = true;
159
63577
      std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs);
160
63577
      if (its == d_ci[x][coeff].end())
161
      {
162
58542
        d_ci[x][coeff][rhs] = type;
163
58542
        d_ci_exp[x][coeff][rhs] = exp;
164
      }
165
5035
      else if (type != its->second)
166
      {
167
294
        Trace("nl-ext-bound-debug2")
168
147
            << "Joining kinds : " << type << " " << its->second << std::endl;
169
147
        Kind jk = joinKinds(type, its->second);
170
147
        if (jk == Kind::UNDEFINED_KIND)
171
        {
172
          updated = false;
173
        }
174
147
        else if (jk != its->second)
175
        {
176
119
          if (jk == type)
177
          {
178
119
            d_ci[x][coeff][rhs] = type;
179
119
            d_ci_exp[x][coeff][rhs] = exp;
180
          }
181
          else
182
          {
183
            d_ci[x][coeff][rhs] = jk;
184
            d_ci_exp[x][coeff][rhs] =
185
                nm->mkNode(Kind::AND, d_ci_exp[x][coeff][rhs], exp);
186
          }
187
        }
188
        else
189
        {
190
28
          updated = false;
191
        }
192
      }
193
63577
      if (Trace.isOn("nl-ext-bound"))
194
      {
195
        if (updated)
196
        {
197
          Trace("nl-ext-bound") << "Bound: ";
198
          debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs);
199
          Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs];
200
          if (d_ci_max[x][coeff][rhs])
201
          {
202
            Trace("nl-ext-bound") << ", is max degree";
203
          }
204
          Trace("nl-ext-bound") << std::endl;
205
        }
206
      }
207
      // compute if bound is not satisfied, and store what is required
208
      // for a possible refinement
209
63577
      if (options::nlExtTangentPlanes())
210
      {
211
11706
        if (is_false_lit)
212
        {
213
2043
          d_data->d_tplane_refine.insert(x);
214
        }
215
      }
216
    }
217
  }
218
  // reflexive constraints
219
1040
  Node null_coeff;
220
4772
  for (unsigned j = 0; j < d_data->d_mterms.size(); j++)
221
  {
222
8504
    Node n = d_data->d_mterms[j];
223
4252
    d_ci[n][null_coeff][n] = Kind::EQUAL;
224
4252
    d_ci_exp[n][null_coeff][n] = d_data->d_true;
225
4252
    d_ci_max[n][null_coeff][n] = false;
226
  }
227
228
520
  Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl;
229
  const std::map<Node, std::vector<Node> >& cpMap =
230
520
      d_data->d_mdb.getContainsParentMap();
231
4772
  for (unsigned k = 0; k < d_data->d_mterms.size(); k++)
232
  {
233
6302
    Node x = d_data->d_mterms[k];
234
8504
    Trace("nl-ext-bound-debug")
235
4252
        << "Process bounds for " << x << " : " << std::endl;
236
4252
    std::map<Node, std::vector<Node> >::const_iterator itm = cpMap.find(x);
237
6454
    if (itm == cpMap.end())
238
    {
239
2202
      Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl;
240
2202
      continue;
241
    }
242
4100
    Trace("nl-ext-bound-debug")
243
2050
        << "...has " << itm->second.size() << " parent monomials." << std::endl;
244
    // check derived bounds
245
    std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc =
246
2050
        d_ci.find(x);
247
2050
    if (itc == d_ci.end())
248
    {
249
      continue;
250
    }
251
2543
    for (std::map<Node, std::map<Node, Kind> >::iterator itcc =
252
2050
             itc->second.begin();
253
4593
         itcc != itc->second.end();
254
         ++itcc)
255
    {
256
5086
      Node coeff = itcc->first;
257
5086
      Node t = ArithMSum::mkCoeffTerm(coeff, x);
258
28535
      for (std::map<Node, Kind>::iterator itcr = itcc->second.begin();
259
28535
           itcr != itcc->second.end();
260
           ++itcr)
261
      {
262
39843
        Node rhs = itcr->first;
263
        // only consider this bound if maximal degree
264
25992
        if (!d_ci_max[x][coeff][rhs])
265
        {
266
12141
          continue;
267
        }
268
13851
        Kind type = itcr->second;
269
69914
        for (unsigned j = 0; j < itm->second.size(); j++)
270
        {
271
103082
          Node y = itm->second[j];
272
103082
          Node mult = d_data->d_mdb.getContainsDiff(x, y);
273
          // x <k> t => m*x <k'> t  where y = m*x
274
          // get the sign of mult
275
103082
          Node mmv = d_data->d_model.computeConcreteModelValue(mult);
276
112126
          Trace("nl-ext-bound-debug2")
277
56063
              << "Model value of " << mult << " is " << mmv << std::endl;
278
56279
          if (!mmv.isConst())
279
          {
280
432
            Trace("nl-ext-bound-debug")
281
216
                << "     ...coefficient " << mult
282
216
                << " is non-constant (probably transcendental)." << std::endl;
283
216
            continue;
284
          }
285
55847
          int mmv_sign = mmv.getConst<Rational>().sgn();
286
111694
          Trace("nl-ext-bound-debug2")
287
55847
              << "  sign of " << mmv << " is " << mmv_sign << std::endl;
288
64675
          if (mmv_sign == 0)
289
          {
290
17656
            Trace("nl-ext-bound-debug")
291
8828
                << "     ...coefficient " << mult << " is zero." << std::endl;
292
8828
            continue;
293
          }
294
94038
          Trace("nl-ext-bound-debug")
295
47019
              << "  from " << x << " * " << mult << " = " << y << " and " << t
296
47019
              << " " << type << " " << rhs << ", infer : " << std::endl;
297
47019
          Kind infer_type = mmv_sign == -1 ? reverseRelationKind(type) : type;
298
94038
          Node infer_lhs = nm->mkNode(Kind::MULT, mult, t);
299
94038
          Node infer_rhs = nm->mkNode(Kind::MULT, mult, rhs);
300
94038
          Node infer = nm->mkNode(infer_type, infer_lhs, infer_rhs);
301
47019
          Trace("nl-ext-bound-debug") << "     " << infer << std::endl;
302
94038
          Node infer_mv = d_data->d_model.computeAbstractModelValue(Rewriter::rewrite(infer));
303
94038
          Trace("nl-ext-bound-debug")
304
47019
              << "       ...infer model value is " << infer_mv << std::endl;
305
47019
          if (infer_mv == d_data->d_false)
306
          {
307
            Node exp = nm->mkNode(
308
                Kind::AND,
309
7323
                nm->mkNode(
310
4882
                    mmv_sign == 1 ? Kind::GT : Kind::LT, mult, d_data->d_zero),
311
9764
                d_ci_exp[x][coeff][rhs]);
312
4882
            Node iblem = nm->mkNode(Kind::IMPLIES, exp, infer);
313
4882
            Node iblem_rw = Rewriter::rewrite(iblem);
314
2441
            bool introNewTerms = hasNewMonomials(iblem_rw, d_data->d_ms);
315
4882
            Trace("nl-ext-bound-lemma")
316
2441
                << "*** Bound inference lemma : " << iblem_rw
317
2441
                << " (pre-rewrite : " << iblem << ")" << std::endl;
318
2441
            CDProof* proof = nullptr;
319
4882
            Node orig = d_ci_exp[x][coeff][rhs];
320
2441
            if (d_data->isProofEnabled())
321
            {
322
404
              proof = d_data->getProof();
323
              // this is iblem, but uses (type t rhs) instead of the original
324
              // variant (which is identical under rewriting)
325
              // we first infer the "clean" version of the lemma and then
326
              // use MACRO_SR_PRED_TRANSFORM to rewrite
327
              Node tmplem = nm->mkNode(
328
                  Kind::IMPLIES,
329
1616
                  nm->mkNode(Kind::AND,
330
808
                             nm->mkNode(mmv_sign == 1 ? Kind::GT : Kind::LT,
331
                                        mult,
332
404
                                        d_data->d_zero),
333
808
                             nm->mkNode(type, t, rhs)),
334
1616
                  infer);
335
1616
              proof->addStep(tmplem,
336
404
                             mmv_sign == 1 ? PfRule::ARITH_MULT_POS
337
                                           : PfRule::ARITH_MULT_NEG,
338
                             {},
339
808
                             {mult, nm->mkNode(type, t, rhs)});
340
1212
              proof->addStep(
341
808
                  iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem});
342
            }
343
2441
            d_data->d_im.addPendingLemma(iblem,
344
                                         InferenceId::ARITH_NL_INFER_BOUNDS_NT,
345
                                         proof,
346
                                         introNewTerms);
347
          }
348
        }
349
      }
350
    }
351
  }
352
520
}
353
354
void MonomialBoundsCheck::checkResBounds()
355
{
356
  NodeManager* nm = NodeManager::currentNM();
357
  Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..."
358
                  << std::endl;
359
  size_t nmterms = d_data->d_mterms.size();
360
  for (unsigned j = 0; j < nmterms; j++)
361
  {
362
    Node a = d_data->d_mterms[j];
363
    std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca =
364
        d_ci.find(a);
365
    if (itca == d_ci.end())
366
    {
367
      continue;
368
    }
369
    for (unsigned k = (j + 1); k < nmterms; k++)
370
    {
371
      Node b = d_data->d_mterms[k];
372
      std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itcb =
373
          d_ci.find(b);
374
      if (itcb == d_ci.end())
375
      {
376
        continue;
377
      }
378
      Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a
379
                                   << " and " << b << std::endl;
380
      // if they have common factors
381
      std::map<Node, Node>::iterator ita = d_data->d_mono_diff[a].find(b);
382
      if (ita == d_data->d_mono_diff[a].end())
383
      {
384
        continue;
385
      }
386
      Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a
387
                             << " vs [b] " << b << std::endl;
388
      std::map<Node, Node>::iterator itb = d_data->d_mono_diff[b].find(a);
389
      Assert(itb != d_data->d_mono_diff[b].end());
390
      Node mv_a = d_data->d_model.computeAbstractModelValue(ita->second);
391
      Assert(mv_a.isConst());
392
      int mv_a_sgn = mv_a.getConst<Rational>().sgn();
393
      if (mv_a_sgn == 0)
394
      {
395
        // we don't compare monomials whose current model value is zero
396
        continue;
397
      }
398
      Node mv_b = d_data->d_model.computeAbstractModelValue(itb->second);
399
      Assert(mv_b.isConst());
400
      int mv_b_sgn = mv_b.getConst<Rational>().sgn();
401
      if (mv_b_sgn == 0)
402
      {
403
        // we don't compare monomials whose current model value is zero
404
        continue;
405
      }
406
      Trace("nl-ext-rbound") << "  [a] factor is " << ita->second
407
                             << ", sign in model = " << mv_a_sgn << std::endl;
408
      Trace("nl-ext-rbound") << "  [b] factor is " << itb->second
409
                             << ", sign in model = " << mv_b_sgn << std::endl;
410
411
      std::vector<Node> exp;
412
      // bounds of a
413
      for (std::map<Node, std::map<Node, Kind> >::iterator itcac =
414
               itca->second.begin();
415
           itcac != itca->second.end();
416
           ++itcac)
417
      {
418
        Node coeff_a = itcac->first;
419
        for (std::map<Node, Kind>::iterator itcar = itcac->second.begin();
420
             itcar != itcac->second.end();
421
             ++itcar)
422
        {
423
          Node rhs_a = itcar->first;
424
          Node rhs_a_res_base = nm->mkNode(Kind::MULT, itb->second, rhs_a);
425
          rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base);
426
          if (hasNewMonomials(rhs_a_res_base, d_data->d_ms))
427
          {
428
            continue;
429
          }
430
          Kind type_a = itcar->second;
431
          exp.push_back(d_ci_exp[a][coeff_a][rhs_a]);
432
433
          // bounds of b
434
          for (std::map<Node, std::map<Node, Kind> >::iterator itcbc =
435
                   itcb->second.begin();
436
               itcbc != itcb->second.end();
437
               ++itcbc)
438
          {
439
            Node coeff_b = itcbc->first;
440
            Node rhs_a_res = ArithMSum::mkCoeffTerm(coeff_b, rhs_a_res_base);
441
            for (std::map<Node, Kind>::iterator itcbr = itcbc->second.begin();
442
                 itcbr != itcbc->second.end();
443
                 ++itcbr)
444
            {
445
              Node rhs_b = itcbr->first;
446
              Node rhs_b_res = nm->mkNode(Kind::MULT, ita->second, rhs_b);
447
              rhs_b_res = ArithMSum::mkCoeffTerm(coeff_a, rhs_b_res);
448
              rhs_b_res = Rewriter::rewrite(rhs_b_res);
449
              if (hasNewMonomials(rhs_b_res, d_data->d_ms))
450
              {
451
                continue;
452
              }
453
              Kind type_b = itcbr->second;
454
              exp.push_back(d_ci_exp[b][coeff_b][rhs_b]);
455
              if (Trace.isOn("nl-ext-rbound"))
456
              {
457
                Trace("nl-ext-rbound") << "* try bounds : ";
458
                debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a);
459
                Trace("nl-ext-rbound") << std::endl;
460
                Trace("nl-ext-rbound") << "               ";
461
                debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b);
462
                Trace("nl-ext-rbound") << std::endl;
463
              }
464
              Kind types[2];
465
              for (unsigned r = 0; r < 2; r++)
466
              {
467
                Node pivot_factor = r == 0 ? itb->second : ita->second;
468
                int pivot_factor_sign = r == 0 ? mv_b_sgn : mv_a_sgn;
469
                types[r] = r == 0 ? type_a : type_b;
470
                if (pivot_factor_sign == (r == 0 ? 1 : -1))
471
                {
472
                  types[r] = reverseRelationKind(types[r]);
473
                }
474
                if (pivot_factor_sign == 1)
475
                {
476
                  exp.push_back(
477
                      nm->mkNode(Kind::GT, pivot_factor, d_data->d_zero));
478
                }
479
                else
480
                {
481
                  exp.push_back(
482
                      nm->mkNode(Kind::LT, pivot_factor, d_data->d_zero));
483
                }
484
              }
485
              Kind jk = transKinds(types[0], types[1]);
486
              Trace("nl-ext-rbound-debug")
487
                  << "trans kind : " << types[0] << " + " << types[1] << " = "
488
                  << jk << std::endl;
489
              if (jk != Kind::UNDEFINED_KIND)
490
              {
491
                Node conc = nm->mkNode(jk, rhs_a_res, rhs_b_res);
492
                Node conc_mv = d_data->d_model.computeAbstractModelValue(conc);
493
                if (conc_mv == d_data->d_false)
494
                {
495
                  Node rblem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
496
                  Trace("nl-ext-rbound-lemma-debug")
497
                      << "Resolution bound lemma "
498
                         "(pre-rewrite) "
499
                         ": "
500
                      << rblem << std::endl;
501
                  rblem = Rewriter::rewrite(rblem);
502
                  Trace("nl-ext-rbound-lemma")
503
                      << "Resolution bound lemma : " << rblem << std::endl;
504
                  d_data->d_im.addPendingLemma(
505
                      rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS);
506
                }
507
              }
508
              exp.pop_back();
509
              exp.pop_back();
510
              exp.pop_back();
511
            }
512
          }
513
          exp.pop_back();
514
        }
515
      }
516
    }
517
  }
518
}
519
520
}  // namespace nl
521
}  // namespace arith
522
}  // namespace theory
523
26676
}  // namespace CVC4