GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/monomial_check.cpp Lines: 359 370 97.0 %
Date: 2021-03-22 Branches: 748 1484 50.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial_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 some monomial lemmas
13
 **/
14
15
#include "theory/arith/nl/ext/monomial_check.h"
16
17
#include "expr/node.h"
18
#include "expr/proof.h"
19
#include "theory/arith/arith_msum.h"
20
#include "theory/arith/inference_manager.h"
21
#include "theory/arith/nl/nl_model.h"
22
#include "theory/arith/nl/nl_lemma_utils.h"
23
#include "theory/arith/nl/ext/ext_state.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace arith {
28
namespace nl {
29
30
4389
MonomialCheck::MonomialCheck(ExtState* data) : d_data(data)
31
{
32
4389
  d_order_points.push_back(d_data->d_neg_one);
33
4389
  d_order_points.push_back(d_data->d_zero);
34
4389
  d_order_points.push_back(d_data->d_one);
35
4389
}
36
37
2742
void MonomialCheck::init(const std::vector<Node>& xts)
38
{
39
2742
  d_ms_proc.clear();
40
2742
  d_m_nconst_factor.clear();
41
42
23167
  for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
43
  {
44
40850
    Node a = xts[i];
45
20425
    if (a.getKind() == Kind::NONLINEAR_MULT)
46
    {
47
14043
      const std::vector<Node>& varList = d_data->d_mdb.getVariableList(a);
48
40649
      for (const Node& v : varList)
49
      {
50
53212
        Node mvk = d_data->d_model.computeAbstractModelValue(v);
51
26606
        if (!mvk.isConst())
52
        {
53
          d_m_nconst_factor[a] = true;
54
        }
55
      }
56
    }
57
  }
58
59
10968
  for (unsigned j = 0; j < d_order_points.size(); j++)
60
  {
61
16452
    Node c = d_order_points[j];
62
8226
    d_data->d_model.computeConcreteModelValue(c);
63
8226
    d_data->d_model.computeAbstractModelValue(c);
64
  }
65
2742
}
66
67
2359
void MonomialCheck::checkSign()
68
{
69
4718
  std::map<Node, int> signs;
70
2359
  Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl;
71
15512
  for (unsigned j = 0; j < d_data->d_ms.size(); j++)
72
  {
73
26306
    Node a = d_data->d_ms[j];
74
13153
    if (d_ms_proc.find(a) == d_ms_proc.end())
75
    {
76
26306
      std::vector<Node> exp;
77
13153
      if (Trace.isOn("nl-ext-debug"))
78
      {
79
        Node cmva = d_data->d_model.computeConcreteModelValue(a);
80
        Trace("nl-ext-debug")
81
            << "  process " << a << ", mv=" << cmva << "..." << std::endl;
82
      }
83
13153
      if (d_m_nconst_factor.find(a) == d_m_nconst_factor.end())
84
      {
85
13153
        signs[a] = compareSign(a, a, 0, 1, exp);
86
13153
        if (signs[a] == 0)
87
        {
88
2576
          d_ms_proc[a] = true;
89
5152
          Trace("nl-ext-debug")
90
2576
              << "...mark " << a << " reduced since its value is 0."
91
2576
              << std::endl;
92
        }
93
      }
94
      else
95
      {
96
        Trace("nl-ext-debug")
97
            << "...can't conclude sign lemma for " << a
98
            << " since model value of a factor is non-constant." << std::endl;
99
      }
100
    }
101
  }
102
2359
}
103
104
3420
void MonomialCheck::checkMagnitude(unsigned c)
105
{
106
  // ensure information is setup
107
3420
  if (c == 0)
108
  {
109
    // sort by absolute values of abstract model values
110
1535
    assignOrderIds(d_data->d_ms_vars, d_order_vars, false, true);
111
112
    // sort individual variable lists
113
1535
    Trace("nl-ext-proc") << "Assign order var lists..." << std::endl;
114
1535
    d_data->d_mdb.sortVariablesByModel(d_data->d_ms, d_data->d_model);
115
  }
116
117
3420
  unsigned r = 1;
118
6840
  std::vector<SimpleTheoryLemma> lemmas;
119
  // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
120
  // in lemmas
121
6840
  std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
122
6840
  Trace("nl-ext") << "Get monomial comparison lemmas (order=" << r
123
3420
                  << ", compare=" << c << ")..." << std::endl;
124
24559
  for (unsigned j = 0; j < d_data->d_ms.size(); j++)
125
  {
126
42278
    Node a = d_data->d_ms[j];
127
42278
    if (d_ms_proc.find(a) == d_ms_proc.end()
128
21139
        && d_m_nconst_factor.find(a) == d_m_nconst_factor.end())
129
    {
130
18785
      if (c == 0)
131
      {
132
        // compare magnitude against 1
133
16180
        std::vector<Node> exp;
134
16180
        NodeMultiset a_exp_proc;
135
16180
        NodeMultiset b_exp_proc;
136
16180
        compareMonomial(a,
137
                        a,
138
                        a_exp_proc,
139
8090
                        d_data->d_one,
140
8090
                        d_data->d_one,
141
                        b_exp_proc,
142
                        exp,
143
                        lemmas,
144
                        cmp_infers);
145
      }
146
      else
147
      {
148
10695
        const NodeMultiset& mea = d_data->d_mdb.getMonomialExponentMap(a);
149
10695
        if (c == 1)
150
        {
151
          // could compare not just against containing variables?
152
          // compare magnitude against variables
153
48886
          for (unsigned k = 0; k < d_data->d_ms_vars.size(); k++)
154
          {
155
85270
            Node v = d_data->d_ms_vars[k];
156
85270
            Node mvcv = d_data->d_model.computeConcreteModelValue(v);
157
42635
            if (mvcv.isConst())
158
            {
159
84866
              std::vector<Node> exp;
160
84866
              NodeMultiset a_exp_proc;
161
84866
              NodeMultiset b_exp_proc;
162
42433
              if (mea.find(v) != mea.end())
163
              {
164
10870
                a_exp_proc[v] = 1;
165
10870
                b_exp_proc[v] = 1;
166
10870
                setMonomialFactor(a, v, a_exp_proc);
167
10870
                setMonomialFactor(v, a, b_exp_proc);
168
10870
                compareMonomial(a,
169
                                a,
170
                                a_exp_proc,
171
                                v,
172
                                v,
173
                                b_exp_proc,
174
                                exp,
175
                                lemmas,
176
                                cmp_infers);
177
              }
178
            }
179
          }
180
        }
181
        else
182
        {
183
          // compare magnitude against other non-linear monomials
184
33924
          for (unsigned k = (j + 1); k < d_data->d_ms.size(); k++)
185
          {
186
58960
            Node b = d_data->d_ms[k];
187
            //(signs[a]==signs[b])==(r==0)
188
58960
            if (d_ms_proc.find(b) == d_ms_proc.end()
189
29480
                && d_m_nconst_factor.find(b) == d_m_nconst_factor.end())
190
            {
191
28008
              const NodeMultiset& meb = d_data->d_mdb.getMonomialExponentMap(b);
192
193
56016
              std::vector<Node> exp;
194
              // take common factors of monomials, set minimum of
195
              // common exponents as processed
196
56016
              NodeMultiset a_exp_proc;
197
56016
              NodeMultiset b_exp_proc;
198
78370
              for (NodeMultiset::const_iterator itmea2 = mea.begin();
199
78370
                   itmea2 != mea.end();
200
                   ++itmea2)
201
              {
202
50362
                NodeMultiset::const_iterator itmeb2 = meb.find(itmea2->first);
203
50362
                if (itmeb2 != meb.end())
204
                {
205
13785
                  unsigned min_exp = itmea2->second > itmeb2->second
206
25441
                                         ? itmeb2->second
207
25441
                                         : itmea2->second;
208
13785
                  a_exp_proc[itmea2->first] = min_exp;
209
13785
                  b_exp_proc[itmea2->first] = min_exp;
210
27570
                  Trace("nl-ext-comp") << "Common exponent : " << itmea2->first
211
13785
                                       << " : " << min_exp << std::endl;
212
                }
213
              }
214
28008
              if (!a_exp_proc.empty())
215
              {
216
13476
                setMonomialFactor(a, b, a_exp_proc);
217
13476
                setMonomialFactor(b, a, b_exp_proc);
218
              }
219
              /*
220
              if( !a_exp_proc.empty() ){
221
                //reduction based on common exponents a > 0 => ( a * b
222
              <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b
223
              !<> c )  ? }else{ compareMonomial( a, a, a_exp_proc, b,
224
              b, b_exp_proc, exp, lemmas );
225
              }
226
              */
227
28008
              compareMonomial(
228
                  a, a, a_exp_proc, b, b, b_exp_proc, exp, lemmas, cmp_infers);
229
            }
230
          }
231
        }
232
      }
233
    }
234
  }
235
  // remove redundant lemmas, e.g. if a > b, b > c, a > c were
236
  // inferred, discard lemma with conclusion a > c
237
6840
  Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
238
3420
                       << " lemmas." << std::endl;
239
  // naive
240
6840
  std::unordered_set<Node, NodeHashFunction> r_lemmas;
241
1110
  for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
242
3420
           cmp_infers.begin();
243
4530
       itb != cmp_infers.end();
244
       ++itb)
245
  {
246
1817
    for (std::map<Node, std::map<Node, Node> >::iterator itc =
247
1110
             itb->second.begin();
248
2927
         itc != itb->second.end();
249
         ++itc)
250
    {
251
4267
      for (std::map<Node, Node>::iterator itc2 = itc->second.begin();
252
4267
           itc2 != itc->second.end();
253
           ++itc2)
254
      {
255
4900
        std::map<Node, bool> visited;
256
6671
        for (std::map<Node, Node>::iterator itc3 = itc->second.begin();
257
6671
             itc3 != itc->second.end();
258
             ++itc3)
259
        {
260
4376
          if (itc3->first != itc2->first)
261
          {
262
3841
            std::vector<Node> exp;
263
1998
            if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited))
264
            {
265
155
              r_lemmas.insert(itc2->second);
266
310
              Trace("nl-ext-comp")
267
155
                  << "...inference of " << itc->first << " > " << itc2->first
268
155
                  << " was redundant." << std::endl;
269
155
              break;
270
            }
271
          }
272
        }
273
      }
274
    }
275
  }
276
5870
  for (unsigned i = 0; i < lemmas.size(); i++)
277
  {
278
2450
    if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end())
279
    {
280
2295
      d_data->d_im.addPendingLemma(lemmas[i]);
281
    }
282
  }
283
  // could only take maximal lower/minimial lower bounds?
284
3420
}
285
286
// show a <> 0 by inequalities between variables in monomial a w.r.t 0
287
34517
int MonomialCheck::compareSign(
288
    Node oa, Node a, unsigned a_index, int status, std::vector<Node>& exp)
289
{
290
69034
  Trace("nl-ext-debug") << "Process " << a << " at index " << a_index
291
34517
                        << ", status is " << status << std::endl;
292
34517
  NodeManager* nm = NodeManager::currentNM();
293
69034
  Node mvaoa = d_data->d_model.computeAbstractModelValue(oa);
294
34517
  const std::vector<Node>& vla = d_data->d_mdb.getVariableList(a);
295
34517
  if (a_index == vla.size())
296
  {
297
10577
    if (mvaoa.getConst<Rational>().sgn() != status)
298
    {
299
      Node lemma =
300
1758
          nm->mkAnd(exp).impNode(mkLit(oa, d_data->d_zero, status * 2));
301
879
      CDProof* proof = nullptr;
302
879
      if (d_data->isProofEnabled())
303
      {
304
174
        proof = d_data->getProof();
305
348
        std::vector<Node> args = exp;
306
174
        args.emplace_back(oa);
307
174
        proof->addStep(lemma, PfRule::ARITH_MULT_SIGN, {}, args);
308
      }
309
879
      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN, proof);
310
    }
311
10577
    return status;
312
  }
313
23940
  Assert(a_index < vla.size());
314
47880
  Node av = vla[a_index];
315
23940
  unsigned aexp = d_data->d_mdb.getExponent(a, av);
316
  // take current sign in model
317
47880
  Node mvaav = d_data->d_model.computeAbstractModelValue(av);
318
23940
  int sgn = mvaav.getConst<Rational>().sgn();
319
47880
  Trace("nl-ext-debug") << "Process var " << av << "^" << aexp
320
23940
                        << ", model sign = " << sgn << std::endl;
321
23940
  if (sgn == 0)
322
  {
323
2576
    if (mvaoa.getConst<Rational>().sgn() != 0)
324
    {
325
938
      Node prem = av.eqNode(d_data->d_zero);
326
938
      Node conc = oa.eqNode(d_data->d_zero);
327
938
      Node lemma = prem.impNode(conc);
328
469
      CDProof* proof = nullptr;
329
469
      if (d_data->isProofEnabled())
330
      {
331
67
        proof = d_data->getProof();
332
67
        proof->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {prem}, {conc});
333
67
        proof->addStep(lemma, PfRule::SCOPE, {conc}, {prem});
334
      }
335
469
      d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN, proof);
336
    }
337
2576
    return 0;
338
  }
339
21364
  if (aexp % 2 == 0)
340
  {
341
2924
    exp.push_back(av.eqNode(d_data->d_zero).negate());
342
2924
    return compareSign(oa, a, a_index + 1, status, exp);
343
  }
344
18440
  exp.push_back(nm->mkNode(sgn == 1 ? Kind::GT : Kind::LT, av, d_data->d_zero));
345
18440
  return compareSign(oa, a, a_index + 1, status * sgn, exp);
346
}
347
348
46968
bool MonomialCheck::compareMonomial(
349
    Node oa,
350
    Node a,
351
    NodeMultiset& a_exp_proc,
352
    Node ob,
353
    Node b,
354
    NodeMultiset& b_exp_proc,
355
    std::vector<Node>& exp,
356
    std::vector<SimpleTheoryLemma>& lem,
357
    std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
358
{
359
93936
  Trace("nl-ext-comp-debug")
360
46968
      << "Check |" << a << "| >= |" << b << "|" << std::endl;
361
46968
  unsigned pexp_size = exp.size();
362
46968
  if (compareMonomial(
363
          oa, a, 0, a_exp_proc, ob, b, 0, b_exp_proc, 0, exp, lem, cmp_infers))
364
  {
365
31426
    return true;
366
  }
367
15542
  exp.resize(pexp_size);
368
31084
  Trace("nl-ext-comp-debug")
369
15542
      << "Check |" << b << "| >= |" << a << "|" << std::endl;
370
15542
  if (compareMonomial(
371
          ob, b, 0, b_exp_proc, oa, a, 0, a_exp_proc, 0, exp, lem, cmp_infers))
372
  {
373
9332
    return true;
374
  }
375
6210
  return false;
376
}
377
378
// trying to show a ( >, = ) b   by inequalities between variables in
379
// monomials a,b
380
239089
bool MonomialCheck::compareMonomial(
381
    Node oa,
382
    Node a,
383
    unsigned a_index,
384
    NodeMultiset& a_exp_proc,
385
    Node ob,
386
    Node b,
387
    unsigned b_index,
388
    NodeMultiset& b_exp_proc,
389
    int status,
390
    std::vector<Node>& exp,
391
    std::vector<SimpleTheoryLemma>& lem,
392
    std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
393
{
394
478178
  Trace("nl-ext-comp-debug")
395
239089
      << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index
396
239089
      << " " << b_index << std::endl;
397
239089
  Assert(status == 0 || status == 2);
398
239089
  const std::vector<Node>& vla = d_data->d_mdb.getVariableList(a);
399
239089
  const std::vector<Node>& vlb = d_data->d_mdb.getVariableList(b);
400
239089
  if (a_index == vla.size() && b_index == vlb.size())
401
  {
402
    // finished, compare absolute value of abstract model values
403
40758
    int modelStatus = d_data->d_model.compare(oa, ob, false, true) * -2;
404
81516
    Trace("nl-ext-comp") << "...finished comparison with " << oa << " <"
405
40758
                         << status << "> " << ob
406
40758
                         << ", model status = " << modelStatus << std::endl;
407
40758
    if (status != modelStatus)
408
    {
409
4900
      Trace("nl-ext-comp-infer")
410
2450
          << "infer : " << oa << " <" << status << "> " << ob << std::endl;
411
2450
      if (status == 2)
412
      {
413
        // must state that all variables are non-zero
414
5515
        for (unsigned j = 0; j < vla.size(); j++)
415
        {
416
3449
          exp.push_back(vla[j].eqNode(d_data->d_zero).negate());
417
        }
418
      }
419
2450
      NodeManager* nm = NodeManager::currentNM();
420
      Node clem = nm->mkNode(
421
4900
          Kind::IMPLIES, nm->mkAnd(exp), mkLit(oa, ob, status, true));
422
2450
      Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
423
2450
      lem.emplace_back(
424
4900
          InferenceId::ARITH_NL_COMPARISON, clem, LemmaProperty::NONE, nullptr);
425
2450
      cmp_infers[status][oa][ob] = clem;
426
    }
427
40758
    return true;
428
  }
429
  // get a/b variable information
430
396662
  Node av;
431
198331
  unsigned aexp = 0;
432
198331
  unsigned avo = 0;
433
198331
  if (a_index < vla.size())
434
  {
435
170116
    av = vla[a_index];
436
170116
    unsigned aexpTotal = d_data->d_mdb.getExponent(a, av);
437
170116
    Assert(a_exp_proc[av] <= aexpTotal);
438
170116
    aexp = aexpTotal - a_exp_proc[av];
439
170116
    if (aexp == 0)
440
    {
441
116356
      return compareMonomial(oa,
442
                             a,
443
                             a_index + 1,
444
                             a_exp_proc,
445
                             ob,
446
                             b,
447
                             b_index,
448
                             b_exp_proc,
449
                             status,
450
                             exp,
451
                             lem,
452
58178
                             cmp_infers);
453
    }
454
111938
    Assert(d_order_vars.find(av) != d_order_vars.end());
455
111938
    avo = d_order_vars[av];
456
  }
457
280306
  Node bv;
458
140153
  unsigned bexp = 0;
459
140153
  unsigned bvo = 0;
460
140153
  if (b_index < vlb.size())
461
  {
462
112548
    bv = vlb[b_index];
463
112548
    unsigned bexpTotal = d_data->d_mdb.getExponent(b, bv);
464
112548
    Assert(b_exp_proc[bv] <= bexpTotal);
465
112548
    bexp = bexpTotal - b_exp_proc[bv];
466
112548
    if (bexp == 0)
467
    {
468
111070
      return compareMonomial(oa,
469
                             a,
470
                             a_index,
471
                             a_exp_proc,
472
                             ob,
473
                             b,
474
                             b_index + 1,
475
                             b_exp_proc,
476
                             status,
477
                             exp,
478
                             lem,
479
55535
                             cmp_infers);
480
    }
481
57013
    Assert(d_order_vars.find(bv) != d_order_vars.end());
482
57013
    bvo = d_order_vars[bv];
483
  }
484
  // get "one" information
485
84618
  Assert(d_order_vars.find(d_data->d_one) != d_order_vars.end());
486
84618
  unsigned ovo = d_order_vars[d_data->d_one];
487
169236
  Trace("nl-ext-comp-debug") << "....vars : " << av << "^" << aexp << " " << bv
488
84618
                             << "^" << bexp << std::endl;
489
490
  //--- cases
491
84618
  if (av.isNull())
492
  {
493
4538
    if (bvo <= ovo)
494
    {
495
2071
      Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl;
496
      // can multiply b by <=1
497
2071
      exp.push_back(mkLit(d_data->d_one, bv, bvo == ovo ? 0 : 2, true));
498
4142
      return compareMonomial(oa,
499
                             a,
500
                             a_index,
501
                             a_exp_proc,
502
                             ob,
503
                             b,
504
                             b_index + 1,
505
                             b_exp_proc,
506
                             bvo == ovo ? status : 2,
507
                             exp,
508
                             lem,
509
2071
                             cmp_infers);
510
    }
511
4934
    Trace("nl-ext-comp-debug")
512
2467
        << "...failure, unmatched |b|>1 component." << std::endl;
513
2467
    return false;
514
  }
515
80080
  else if (bv.isNull())
516
  {
517
27605
    if (avo >= ovo)
518
    {
519
25250
      Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl;
520
      // can multiply a by >=1
521
25250
      exp.push_back(mkLit(av, d_data->d_one, avo == ovo ? 0 : 2, true));
522
50500
      return compareMonomial(oa,
523
                             a,
524
                             a_index + 1,
525
                             a_exp_proc,
526
                             ob,
527
                             b,
528
                             b_index,
529
                             b_exp_proc,
530
                             avo == ovo ? status : 2,
531
                             exp,
532
                             lem,
533
25250
                             cmp_infers);
534
    }
535
4710
    Trace("nl-ext-comp-debug")
536
2355
        << "...failure, unmatched |a|<1 component." << std::endl;
537
2355
    return false;
538
  }
539
52475
  Assert(!av.isNull() && !bv.isNull());
540
52475
  if (avo >= bvo)
541
  {
542
35424
    if (bvo < ovo && avo >= ovo)
543
    {
544
274
      Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl;
545
      // do avo>=1 instead
546
274
      exp.push_back(mkLit(av, d_data->d_one, avo == ovo ? 0 : 2, true));
547
548
      return compareMonomial(oa,
548
                             a,
549
                             a_index + 1,
550
                             a_exp_proc,
551
                             ob,
552
                             b,
553
                             b_index,
554
                             b_exp_proc,
555
                             avo == ovo ? status : 2,
556
                             exp,
557
                             lem,
558
274
                             cmp_infers);
559
    }
560
35150
    unsigned min_exp = aexp > bexp ? bexp : aexp;
561
35150
    a_exp_proc[av] += min_exp;
562
35150
    b_exp_proc[bv] += min_exp;
563
70300
    Trace("nl-ext-comp-debug") << "...take leading " << min_exp << " from "
564
35150
                               << av << " and " << bv << std::endl;
565
35150
    exp.push_back(mkLit(av, bv, avo == bvo ? 0 : 2, true));
566
70300
    bool ret = compareMonomial(oa,
567
                               a,
568
                               a_index,
569
                               a_exp_proc,
570
                               ob,
571
                               b,
572
                               b_index,
573
                               b_exp_proc,
574
                               avo == bvo ? status : 2,
575
                               exp,
576
                               lem,
577
35150
                               cmp_infers);
578
35150
    a_exp_proc[av] -= min_exp;
579
35150
    b_exp_proc[bv] -= min_exp;
580
35150
    return ret;
581
  }
582
17051
  if (bvo <= ovo)
583
  {
584
121
    Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl;
585
    // try multiply b <= 1
586
121
    exp.push_back(mkLit(d_data->d_one, bv, bvo == ovo ? 0 : 2, true));
587
242
    return compareMonomial(oa,
588
                           a,
589
                           a_index,
590
                           a_exp_proc,
591
                           ob,
592
                           b,
593
                           b_index + 1,
594
                           b_exp_proc,
595
                           bvo == ovo ? status : 2,
596
                           exp,
597
                           lem,
598
121
                           cmp_infers);
599
  }
600
33860
  Trace("nl-ext-comp-debug")
601
16930
      << "...failure, leading |b|>|a|>1 component." << std::endl;
602
16930
  return false;
603
}
604
605
2550
bool MonomialCheck::cmp_holds(Node x,
606
                              Node y,
607
                              std::map<Node, std::map<Node, Node> >& cmp_infers,
608
                              std::vector<Node>& exp,
609
                              std::map<Node, bool>& visited)
610
{
611
2550
  if (x == y)
612
  {
613
155
    return true;
614
  }
615
2395
  else if (visited.find(x) != visited.end())
616
  {
617
363
    return false;
618
  }
619
2032
  visited[x] = true;
620
2032
  std::map<Node, std::map<Node, Node> >::iterator it = cmp_infers.find(x);
621
2032
  if (it != cmp_infers.end())
622
  {
623
741
    for (std::map<Node, Node>::iterator itc = it->second.begin();
624
741
         itc != it->second.end();
625
         ++itc)
626
    {
627
552
      exp.push_back(itc->second);
628
552
      if (cmp_holds(itc->first, y, cmp_infers, exp, visited))
629
      {
630
168
        return true;
631
      }
632
384
      exp.pop_back();
633
    }
634
  }
635
1864
  return false;
636
}
637
638
1535
void MonomialCheck::assignOrderIds(std::vector<Node>& vars,
639
                                   NodeMultiset& order,
640
                                   bool isConcrete,
641
                                   bool isAbsolute)
642
{
643
1535
  SortNlModel smv;
644
1535
  smv.d_nlm = &d_data->d_model;
645
1535
  smv.d_isConcrete = isConcrete;
646
1535
  smv.d_isAbsolute = isAbsolute;
647
1535
  smv.d_reverse_order = false;
648
1535
  std::sort(vars.begin(), vars.end(), smv);
649
650
1535
  order.clear();
651
  // assign ordering id's
652
1535
  unsigned counter = 0;
653
1535
  unsigned order_index = isConcrete ? 0 : 1;
654
3070
  Node prev;
655
8816
  for (unsigned j = 0; j < vars.size(); j++)
656
  {
657
14562
    Node x = vars[j];
658
14562
    Node v = d_data->d_model.computeModelValue(x, isConcrete);
659
7281
    if (!v.isConst())
660
    {
661
      Trace("nl-ext-mvo") << "..do not assign order to " << x << " : " << v
662
                          << std::endl;
663
      // don't assign for non-constant values (transcendental function apps)
664
      break;
665
    }
666
7281
    Trace("nl-ext-mvo") << "  order " << x << " : " << v << std::endl;
667
7281
    if (v != prev)
668
    {
669
      // builtin points
670
      bool success;
671
8064
      do
672
      {
673
8064
        success = false;
674
8064
        if (order_index < d_order_points.size())
675
        {
676
3646
          Node vv = d_data->d_model.computeModelValue(
677
7292
              d_order_points[order_index], isConcrete);
678
3646
          if (d_data->d_model.compareValue(v, vv, isAbsolute) <= 0)
679
          {
680
2777
            counter++;
681
5554
            Trace("nl-ext-mvo") << "O[" << d_order_points[order_index]
682
2777
                                << "] = " << counter << std::endl;
683
2777
            order[d_order_points[order_index]] = counter;
684
2777
            prev = vv;
685
2777
            order_index++;
686
2777
            success = true;
687
          }
688
        }
689
      } while (success);
690
    }
691
7281
    if (prev.isNull() || d_data->d_model.compareValue(v, prev, isAbsolute) != 0)
692
    {
693
3669
      counter++;
694
    }
695
7281
    Trace("nl-ext-mvo") << "O[" << x << "] = " << counter << std::endl;
696
7281
    order[x] = counter;
697
7281
    prev = v;
698
  }
699
2121
  while (order_index < d_order_points.size())
700
  {
701
293
    counter++;
702
586
    Trace("nl-ext-mvo") << "O[" << d_order_points[order_index]
703
293
                        << "] = " << counter << std::endl;
704
293
    order[d_order_points[order_index]] = counter;
705
293
    order_index++;
706
  }
707
1535
}
708
66526
Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
709
{
710
66526
  if (status == 0)
711
  {
712
11002
    Node a_eq_b = a.eqNode(b);
713
5501
    if (!isAbsolute)
714
    {
715
      return a_eq_b;
716
    }
717
11002
    Node negate_b = NodeManager::currentNM()->mkNode(Kind::UMINUS, b);
718
5501
    return a_eq_b.orNode(a.eqNode(negate_b));
719
  }
720
61025
  else if (status < 0)
721
  {
722
331
    return mkLit(b, a, -status);
723
  }
724
60694
  Assert(status == 1 || status == 2);
725
60694
  NodeManager* nm = NodeManager::currentNM();
726
60694
  Kind greater_op = status == 1 ? Kind::GEQ : Kind::GT;
727
60694
  if (!isAbsolute)
728
  {
729
879
    return nm->mkNode(greater_op, a, b);
730
  }
731
  // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) );
732
119630
  Node a_is_nonnegative = nm->mkNode(Kind::GEQ, a, d_data->d_zero);
733
119630
  Node b_is_nonnegative = nm->mkNode(Kind::GEQ, b, d_data->d_zero);
734
119630
  Node negate_a = nm->mkNode(Kind::UMINUS, a);
735
119630
  Node negate_b = nm->mkNode(Kind::UMINUS, b);
736
  return a_is_nonnegative.iteNode(
737
119630
      b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b),
738
119630
                               nm->mkNode(greater_op, a, negate_b)),
739
119630
      b_is_nonnegative.iteNode(nm->mkNode(greater_op, negate_a, b),
740
179445
                               nm->mkNode(greater_op, negate_a, negate_b)));
741
}
742
743
48692
void MonomialCheck::setMonomialFactor(Node a,
744
                                      Node b,
745
                                      const NodeMultiset& common)
746
{
747
  // Could not tell if this was being inserted intentionally or not.
748
48692
  std::map<Node, Node>& mono_diff_a = d_data->d_mono_diff[a];
749
48692
  if (mono_diff_a.find(b) == mono_diff_a.end())
750
  {
751
10600
    Trace("nl-ext-mono-factor")
752
5300
        << "Set monomial factor for " << a << "/" << b << std::endl;
753
5300
    mono_diff_a[b] = d_data->d_mdb.mkMonomialRemFactor(a, common);
754
  }
755
48692
}
756
757
}  // namespace nl
758
}  // namespace arith
759
}  // namespace theory
760
26676
}  // namespace CVC4