GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp Lines: 455 526 86.5 %
Date: 2021-11-05 Branches: 1173 2740 42.8 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Aina Niemetz, Andres Noetzli
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Arithmetic instantiator.
14
 */
15
16
#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
17
18
#include "expr/node_algorithm.h"
19
#include "options/quantifiers_options.h"
20
#include "theory/arith/arith_msum.h"
21
#include "theory/arith/partial_model.h"
22
#include "theory/arith/theory_arith.h"
23
#include "theory/arith/theory_arith_private.h"
24
#include "theory/quantifiers/term_util.h"
25
#include "theory/rewriter.h"
26
#include "util/random.h"
27
28
using namespace std;
29
using namespace cvc5::kind;
30
using namespace cvc5::context;
31
32
namespace cvc5 {
33
namespace theory {
34
namespace quantifiers {
35
36
2021
ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc)
37
2021
    : Instantiator(env, tn), d_vtc(vtc)
38
{
39
2021
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
40
2021
  d_one = NodeManager::currentNM()->mkConst(Rational(1));
41
2021
}
42
43
28294
void ArithInstantiator::reset(CegInstantiator* ci,
44
                              SolvedForm& sf,
45
                              Node pv,
46
                              CegInstEffort effort)
47
{
48
28294
  d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false);
49
28294
  d_vts_sym[1] = d_vtc->getVtsDelta(false, false);
50
84882
  for (unsigned i = 0; i < 2; i++)
51
  {
52
56588
    d_mbp_bounds[i].clear();
53
56588
    d_mbp_coeff[i].clear();
54
169764
    for (unsigned j = 0; j < 2; j++)
55
    {
56
113176
      d_mbp_vts_coeff[i][j].clear();
57
    }
58
56588
    d_mbp_lit[i].clear();
59
  }
60
28294
}
61
62
27936
bool ArithInstantiator::hasProcessEquality(CegInstantiator* ci,
63
                                           SolvedForm& sf,
64
                                           Node pv,
65
                                           CegInstEffort effort)
66
{
67
27936
  return true;
68
}
69
70
46107
bool ArithInstantiator::processEquality(CegInstantiator* ci,
71
                                        SolvedForm& sf,
72
                                        Node pv,
73
                                        std::vector<TermProperties>& term_props,
74
                                        std::vector<Node>& terms,
75
                                        CegInstEffort effort)
76
{
77
46107
  NodeManager* nm = NodeManager::currentNM();
78
92214
  Node eq_lhs = terms[0];
79
92214
  Node eq_rhs = terms[1];
80
92214
  Node lhs_coeff = term_props[0].d_coeff;
81
92214
  Node rhs_coeff = term_props[1].d_coeff;
82
  // make the same coefficient
83
46107
  if (rhs_coeff != lhs_coeff)
84
  {
85
    if (!rhs_coeff.isNull())
86
    {
87
      Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl;
88
      eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs);
89
    }
90
    if (!lhs_coeff.isNull())
91
    {
92
      Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl;
93
      eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs);
94
    }
95
  }
96
92214
  Node eq = eq_lhs.eqNode(eq_rhs);
97
46107
  eq = rewrite(eq);
98
92214
  Node val;
99
92214
  TermProperties pv_prop;
100
92214
  Node vts_coeff_inf;
101
92214
  Node vts_coeff_delta;
102
  // isolate pv in the equality
103
92214
  CegTermType ires = solve_arith(
104
46107
      ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta);
105
46107
  if (ires != CEG_TT_INVALID)
106
  {
107
13222
    pv_prop.d_type = CEG_TT_EQUAL;
108
13222
    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
109
    {
110
12440
      return true;
111
    }
112
  }
113
33667
  return false;
114
}
115
116
14714
bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
117
                                            SolvedForm& sf,
118
                                            Node pv,
119
                                            CegInstEffort effort)
120
{
121
14714
  return effort != CEG_INST_EFFORT_FULL;
122
}
123
124
419151
Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
125
                                            SolvedForm& sf,
126
                                            Node pv,
127
                                            Node lit,
128
                                            CegInstEffort effort)
129
{
130
838302
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
131
  // arithmetic inequalities and disequalities
132
838302
  if (atom.getKind() == GEQ
133
838302
      || (atom.getKind() == EQUAL && atom[0].getType().isReal()))
134
  {
135
419151
    return lit;
136
  }
137
  return Node::null();
138
}
139
140
11899
bool ArithInstantiator::processAssertion(CegInstantiator* ci,
141
                                         SolvedForm& sf,
142
                                         Node pv,
143
                                         Node lit,
144
                                         Node alit,
145
                                         CegInstEffort effort)
146
{
147
11899
  NodeManager* nm = NodeManager::currentNM();
148
23798
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
149
11899
  bool pol = lit.getKind() != NOT;
150
  // arithmetic inequalities and disequalities
151
11899
  Assert(atom.getKind() == GEQ
152
         || (atom.getKind() == EQUAL && atom[0].getType().isReal()));
153
  // get model value for pv
154
23798
  Node pv_value = ci->getModelValue(pv);
155
  // cannot contain infinity?
156
23798
  Node vts_coeff_inf;
157
23798
  Node vts_coeff_delta;
158
23798
  Node val;
159
23798
  TermProperties pv_prop;
160
  // isolate pv in the inequality
161
23798
  CegTermType ires = solve_arith(
162
11899
      ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta);
163
11899
  if (ires == CEG_TT_INVALID)
164
  {
165
719
    return false;
166
  }
167
  // compute how many bounds we will consider
168
11180
  unsigned rmax = 1;
169
11180
  if (atom.getKind() == EQUAL && (pol || !options().quantifiers.cegqiModel))
170
  {
171
    rmax = 2;
172
  }
173
22360
  for (unsigned r = 0; r < rmax; r++)
174
  {
175
11180
    CegTermType uires = ires;
176
22360
    Node uval = val;
177
11180
    if (atom.getKind() == GEQ)
178
    {
179
      // push negation downwards
180
7416
      if (!pol)
181
      {
182
3797
        uires = mkNegateCTT(ires);
183
3797
        if (d_type.isInteger())
184
        {
185
3431
          uval = nm->mkNode(
186
              PLUS,
187
              val,
188
6862
              nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
189
3431
          uval = rewrite(uval);
190
        }
191
        else
192
        {
193
366
          Assert(d_type.isReal());
194
          // now is strict inequality
195
366
          uires = mkStrictCTT(uires);
196
        }
197
      }
198
    }
199
3764
    else if (pol)
200
    {
201
      // equalities are both non-strict upper and lower bounds
202
      uires = r == 0 ? CEG_TT_UPPER : CEG_TT_LOWER;
203
    }
204
    else
205
    {
206
      // disequalities are either strict upper or lower bounds
207
      bool is_upper;
208
3764
      if (options().quantifiers.cegqiModel)
209
      {
210
        // disequality is a disjunction : only consider the bound in the
211
        // direction of the model
212
        // first check if there is an infinity...
213
3764
        if (!vts_coeff_inf.isNull())
214
        {
215
          // coefficient or val won't make a difference, just compare with zero
216
          Trace("cegqi-arith-debug") << "Disequality : check infinity polarity "
217
                                     << vts_coeff_inf << std::endl;
218
          Assert(vts_coeff_inf.isConst());
219
          is_upper = (vts_coeff_inf.getConst<Rational>().sgn() == 1);
220
        }
221
        else
222
        {
223
7528
          Node rhs_value = ci->getModelValue(val);
224
7528
          Node lhs_value = pv_prop.getModifiedTerm(pv_value);
225
3764
          if (!pv_prop.isBasic())
226
          {
227
14
            lhs_value = pv_prop.getModifiedTerm(pv_value);
228
14
            lhs_value = rewrite(lhs_value);
229
          }
230
7528
          Trace("cegqi-arith-debug")
231
3764
              << "Disequality : check model values " << lhs_value << " "
232
3764
              << rhs_value << std::endl;
233
          // it generally should be the case that lhs_value!=rhs_value
234
          // however, this assertion is violated e.g. if non-linear is enabled
235
          // since the quantifier-free arithmetic solver may pass full
236
          // effort with no lemmas even when we are not guaranteed to have a
237
          // model. By convention, we use GEQ to compare the values here.
238
          // It also may be the case that cmp is non-constant, in the case
239
          // where lhs or rhs contains a transcendental function. We consider
240
          // the bound to be an upper bound in this case.
241
7528
          Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value);
242
3764
          cmp = rewrite(cmp);
243
3764
          is_upper = !cmp.isConst() || !cmp.getConst<bool>();
244
        }
245
      }
246
      else
247
      {
248
        // since we are not using the model, we try both.
249
        is_upper = (r == 0);
250
      }
251
3764
      Assert(atom.getKind() == EQUAL && !pol);
252
3764
      if (d_type.isInteger())
253
      {
254
3654
        uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER;
255
3654
        uval = nm->mkNode(
256
7308
            PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
257
3654
        uval = rewrite(uval);
258
      }
259
      else
260
      {
261
110
        Assert(d_type.isReal());
262
110
        uires = is_upper ? CEG_TT_LOWER_STRICT : CEG_TT_UPPER_STRICT;
263
      }
264
    }
265
11180
    if (Trace.isOn("cegqi-arith-bound-inf"))
266
    {
267
      Node pvmod = pv_prop.getModifiedTerm(pv);
268
      Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : ";
269
      Trace("cegqi-arith-bound-inf")
270
          << pvmod << " -> " << uval << ", styp = " << uires << std::endl;
271
    }
272
    // take into account delta
273
11180
    if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT)
274
    {
275
476
      if (options().quantifiers.cegqiModel)
276
      {
277
        Node delta_coeff =
278
952
            nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
279
476
        if (vts_coeff_delta.isNull())
280
        {
281
468
          vts_coeff_delta = delta_coeff;
282
        }
283
        else
284
        {
285
8
          vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff);
286
8
          vts_coeff_delta = rewrite(vts_coeff_delta);
287
        }
288
      }
289
      else
290
      {
291
        Node delta = d_vtc->getVtsDelta();
292
        uval = nm->mkNode(
293
            uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta);
294
        uval = rewrite(uval);
295
      }
296
    }
297
11180
    if (options().quantifiers.cegqiModel)
298
    {
299
      // just store bounds, will choose based on tighest bound
300
11180
      unsigned index = isUpperBoundCTT(uires) ? 0 : 1;
301
11180
      d_mbp_bounds[index].push_back(uval);
302
11180
      d_mbp_coeff[index].push_back(pv_prop.d_coeff);
303
22360
      Trace("cegqi-arith-debug")
304
11180
          << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff
305
11180
          << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit
306
11180
          << std::endl;
307
33540
      for (unsigned t = 0; t < 2; t++)
308
      {
309
22360
        d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf
310
                                                   : vts_coeff_delta);
311
      }
312
11180
      d_mbp_lit[index].push_back(lit);
313
    }
314
    else
315
    {
316
      // try this bound
317
      pv_prop.d_type = isUpperBoundCTT(uires) ? CEG_TT_UPPER : CEG_TT_LOWER;
318
      if (ci->constructInstantiationInc(pv, uval, pv_prop, sf))
319
      {
320
        return true;
321
      }
322
    }
323
  }
324
11180
  return false;
325
}
326
327
14045
bool ArithInstantiator::processAssertions(CegInstantiator* ci,
328
                                          SolvedForm& sf,
329
                                          Node pv,
330
                                          CegInstEffort effort)
331
{
332
14045
  if (!options().quantifiers.cegqiModel)
333
  {
334
    return false;
335
  }
336
14045
  NodeManager* nm = NodeManager::currentNM();
337
14510
  bool use_inf = d_type.isInteger() ? options().quantifiers.cegqiUseInfInt
338
14510
                                    : options().quantifiers.cegqiUseInfReal;
339
14045
  bool upper_first = Random::getRandom().pickWithProb(0.5);
340
14045
  if (options().quantifiers.cegqiMinBounds)
341
  {
342
    upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
343
  }
344
  int best_used[2];
345
28090
  std::vector<Node> t_values[3];
346
28090
  Node pv_value = ci->getModelValue(pv);
347
  // try optimal bounds
348
33603
  for (unsigned r = 0; r < 2; r++)
349
  {
350
24678
    int rr = upper_first ? (1 - r) : r;
351
24678
    best_used[rr] = -1;
352
24678
    if (d_mbp_bounds[rr].empty())
353
    {
354
19620
      if (use_inf)
355
      {
356
304
        Trace("cegqi-arith-bound")
357
152
            << "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv
358
152
            << " (type=" << d_type << ")" << std::endl;
359
        // no bounds, we do +- infinity
360
152
        Node val = d_vtc->getVtsInfinity(d_type);
361
        // could get rho value for infinity here
362
152
        if (rr == 0)
363
        {
364
96
          val = nm->mkNode(UMINUS, val);
365
96
          val = rewrite(val);
366
        }
367
152
        TermProperties pv_prop_no_bound;
368
152
        if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
369
        {
370
152
          return true;
371
        }
372
        else if (!options().quantifiers.cegqiMultiInst)
373
        {
374
          return false;
375
        }
376
      }
377
    }
378
    else
379
    {
380
10116
      Trace("cegqi-arith-bound")
381
5058
          << (rr == 0 ? "Lower" : "Upper") << " bounds for " << pv
382
5058
          << " (type=" << d_type << ") : " << std::endl;
383
5058
      int best = -1;
384
20232
      Node best_bound_value[3];
385
13545
      for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
386
      {
387
16974
        Node value[3];
388
8487
        if (Trace.isOn("cegqi-arith-bound"))
389
        {
390
          Assert(!d_mbp_bounds[rr][j].isNull());
391
          Trace("cegqi-arith-bound")
392
              << "  " << j << ": " << d_mbp_bounds[rr][j];
393
          if (!d_mbp_vts_coeff[rr][0][j].isNull())
394
          {
395
            Trace("cegqi-arith-bound")
396
                << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)";
397
          }
398
          if (!d_mbp_vts_coeff[rr][1][j].isNull())
399
          {
400
            Trace("cegqi-arith-bound")
401
                << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)";
402
          }
403
          if (!d_mbp_coeff[rr][j].isNull())
404
          {
405
            Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")";
406
          }
407
          Trace("cegqi-arith-bound") << ", value = ";
408
        }
409
8487
        t_values[rr].push_back(Node::null());
410
        // check if it is better than the current best bound : lexicographic
411
        // order infinite/finite/infinitesimal parts
412
8487
        bool new_best_set = false;
413
8487
        bool new_best = true;
414
31971
        for (unsigned t = 0; t < 3; t++)
415
        {
416
          // get the value
417
24478
          if (t == 0)
418
          {
419
8487
            value[0] = d_mbp_vts_coeff[rr][0][j];
420
8487
            if (!value[0].isNull())
421
            {
422
              Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + ";
423
            }
424
            else
425
            {
426
8487
              value[0] = d_zero;
427
            }
428
          }
429
15991
          else if (t == 1)
430
          {
431
16974
            Node t_value = ci->getModelValue(d_mbp_bounds[rr][j]);
432
8487
            t_values[rr][j] = t_value;
433
8487
            value[1] = t_value;
434
8487
            Trace("cegqi-arith-bound") << value[1];
435
          }
436
          else
437
          {
438
7504
            value[2] = d_mbp_vts_coeff[rr][1][j];
439
7504
            if (!value[2].isNull())
440
            {
441
224
              Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )";
442
            }
443
            else
444
            {
445
7280
              value[2] = d_zero;
446
            }
447
          }
448
          // multiply by coefficient
449
24478
          if (value[t] != d_zero && !d_mbp_coeff[rr][j].isNull())
450
          {
451
150
            Assert(d_mbp_coeff[rr][j].isConst());
452
600
            value[t] = nm->mkNode(
453
                MULT,
454
600
                nm->mkConst(Rational(1)
455
450
                            / d_mbp_coeff[rr][j].getConst<Rational>()),
456
150
                value[t]);
457
150
            value[t] = rewrite(value[t]);
458
          }
459
          // check if new best, if we have not already set it.
460
24478
          if (best != -1 && !new_best_set)
461
          {
462
8613
            Assert(!value[t].isNull() && !best_bound_value[t].isNull());
463
8613
            if (value[t] != best_bound_value[t])
464
            {
465
1689
              Kind k = rr == 0 ? GEQ : LEQ;
466
2384
              Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]);
467
1689
              cmp_bound = rewrite(cmp_bound);
468
              // Should be comparing two constant values which should rewrite
469
              // to a constant. If a step failed, we assume that this is not
470
              // the new best bound. We might not be comparing constant
471
              // values (for instance if transcendental functions are
472
              // involved), in which case we do update the best bound value.
473
1689
              if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>())
474
              {
475
994
                new_best = false;
476
994
                break;
477
              }
478
              // indicate that the value of new_best is now established.
479
695
              new_best_set = true;
480
            }
481
          }
482
        }
483
8487
        Trace("cegqi-arith-bound") << std::endl;
484
8487
        if (new_best)
485
        {
486
29972
          for (unsigned t = 0; t < 3; t++)
487
          {
488
22479
            best_bound_value[t] = value[t];
489
          }
490
7493
          best = j;
491
        }
492
      }
493
5058
      if (best != -1)
494
      {
495
5058
        Trace("cegqi-arith-bound") << "...best bound is " << best << " : ";
496
5058
        if (best_bound_value[0] != d_zero)
497
        {
498
          Trace("cegqi-arith-bound")
499
              << "( " << best_bound_value[0] << " * INF ) + ";
500
        }
501
5058
        Trace("cegqi-arith-bound") << best_bound_value[1];
502
5058
        if (best_bound_value[2] != d_zero)
503
        {
504
338
          Trace("cegqi-arith-bound")
505
169
              << " + ( " << best_bound_value[2] << " * DELTA )";
506
        }
507
5058
        Trace("cegqi-arith-bound") << std::endl;
508
5058
        best_used[rr] = best;
509
        // if using cbqiMidpoint, only add the instance based on one bound if
510
        // the bound is non-strict
511
10894
        if (!options().quantifiers.cegqiMidpoint || d_type.isInteger()
512
5114
            || d_mbp_vts_coeff[rr][1][best].isNull())
513
        {
514
5048
          Node val = d_mbp_bounds[rr][best];
515
25040
          val = getModelBasedProjectionValue(ci,
516
                                             pv,
517
                                             val,
518
                                             rr == 0,
519
5008
                                             d_mbp_coeff[rr][best],
520
                                             pv_value,
521
5008
                                             t_values[rr][best],
522
10016
                                             sf.getTheta(),
523
5008
                                             d_mbp_vts_coeff[rr][0][best],
524
5008
                                             d_mbp_vts_coeff[rr][1][best]);
525
5008
          if (!val.isNull())
526
          {
527
5048
            TermProperties pv_prop_bound;
528
5008
            pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
529
5008
            pv_prop_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER;
530
5008
            if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf))
531
            {
532
4136
              return true;
533
            }
534
872
            else if (!options().quantifiers.cegqiMultiInst)
535
            {
536
832
              return false;
537
            }
538
          }
539
        }
540
      }
541
    }
542
  }
543
  // if not using infinity, use model value of zero
544
8925
  if (!use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty())
545
  {
546
8857
    Node val = d_zero;
547
8857
    TermProperties pv_prop_zero;
548
8857
    Node theta = sf.getTheta();
549
8857
    val = getModelBasedProjectionValue(ci,
550
                                       pv,
551
                                       val,
552
                                       true,
553
                                       pv_prop_zero.d_coeff,
554
                                       pv_value,
555
                                       d_zero,
556
17714
                                       sf.getTheta(),
557
17714
                                       Node::null(),
558
17714
                                       Node::null());
559
8857
    if (!val.isNull())
560
    {
561
8857
      if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf))
562
      {
563
8705
        return true;
564
      }
565
152
      else if (!options().quantifiers.cegqiMultiInst)
566
      {
567
152
        return false;
568
      }
569
    }
570
  }
571
68
  if (options().quantifiers.cegqiMidpoint && !d_type.isInteger())
572
  {
573
144
    Node vals[2];
574
48
    bool bothBounds = true;
575
48
    Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl;
576
144
    for (unsigned rr = 0; rr < 2; rr++)
577
    {
578
96
      int best = best_used[rr];
579
96
      if (best == -1)
580
      {
581
46
        bothBounds = false;
582
      }
583
      else
584
      {
585
50
        vals[rr] = d_mbp_bounds[rr][best];
586
300
        vals[rr] = getModelBasedProjectionValue(ci,
587
                                                pv,
588
                                                vals[rr],
589
                                                rr == 0,
590
100
                                                Node::null(),
591
                                                pv_value,
592
50
                                                t_values[rr][best],
593
100
                                                sf.getTheta(),
594
50
                                                d_mbp_vts_coeff[rr][0][best],
595
150
                                                Node::null());
596
      }
597
96
      Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl;
598
    }
599
48
    Node val;
600
48
    if (bothBounds)
601
    {
602
2
      Assert(!vals[0].isNull() && !vals[1].isNull());
603
2
      if (vals[0] == vals[1])
604
      {
605
        val = vals[0];
606
      }
607
      else
608
      {
609
6
        val = nm->mkNode(MULT,
610
4
                         nm->mkNode(PLUS, vals[0], vals[1]),
611
4
                         nm->mkConst(Rational(1) / Rational(2)));
612
2
        val = rewrite(val);
613
      }
614
    }
615
    else
616
    {
617
46
      if (!vals[0].isNull())
618
      {
619
20
        val = nm->mkNode(PLUS, vals[0], d_one);
620
20
        val = rewrite(val);
621
      }
622
26
      else if (!vals[1].isNull())
623
      {
624
26
        val = nm->mkNode(MINUS, vals[1], d_one);
625
26
        val = rewrite(val);
626
      }
627
    }
628
48
    Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
629
48
    if (!val.isNull())
630
    {
631
48
      TermProperties pv_prop_midpoint;
632
48
      if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf))
633
      {
634
36
        return true;
635
      }
636
12
      else if (!options().quantifiers.cegqiMultiInst)
637
      {
638
12
        return false;
639
      }
640
    }
641
  }
642
  // generally should not make it to this point, unless we are using a
643
  // non-monotonic selection function
644
645
20
  if (!options().quantifiers.cegqiNopt)
646
  {
647
    // if not trying non-optimal bounds, return
648
    return false;
649
  }
650
  // try non-optimal bounds (heuristic, may help when nested quantification) ?
651
20
  Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl;
652
60
  for (unsigned r = 0; r < 2; r++)
653
  {
654
40
    int rr = upper_first ? (1 - r) : r;
655
100
    for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
656
    {
657
120
      if ((int)j != best_used[rr]
658
80
          && (!options().quantifiers.cegqiMidpoint
659
              || d_mbp_vts_coeff[rr][1][j].isNull()))
660
      {
661
        Node val = getModelBasedProjectionValue(ci,
662
                                                pv,
663
20
                                                d_mbp_bounds[rr][j],
664
                                                rr == 0,
665
20
                                                d_mbp_coeff[rr][j],
666
                                                pv_value,
667
20
                                                t_values[rr][j],
668
40
                                                sf.getTheta(),
669
20
                                                d_mbp_vts_coeff[rr][0][j],
670
140
                                                d_mbp_vts_coeff[rr][1][j]);
671
20
        if (!val.isNull())
672
        {
673
40
          TermProperties pv_prop_nopt_bound;
674
20
          pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
675
20
          pv_prop_nopt_bound.d_type = rr == 0 ? CEG_TT_UPPER : CEG_TT_LOWER;
676
20
          if (ci->constructInstantiationInc(pv, val, pv_prop_nopt_bound, sf))
677
          {
678
            return true;
679
          }
680
20
          else if (!options().quantifiers.cegqiMultiInst)
681
          {
682
            return false;
683
          }
684
        }
685
      }
686
    }
687
  }
688
20
  return false;
689
}
690
691
28334
bool ArithInstantiator::needsPostProcessInstantiationForVariable(
692
    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
693
{
694
56668
  return std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv)
695
85002
         != sf.d_non_basic.end();
696
}
697
698
253
bool ArithInstantiator::postProcessInstantiationForVariable(
699
    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
700
{
701
253
  Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv)
702
         != sf.d_non_basic.end());
703
253
  Assert(std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) != sf.d_vars.end());
704
  unsigned index =
705
253
      std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) - sf.d_vars.begin();
706
253
  Assert(!sf.d_props[index].isBasic());
707
506
  Node eq_lhs = sf.d_props[index].getModifiedTerm(sf.d_vars[index]);
708
253
  if (Trace.isOn("cegqi-arith-debug"))
709
  {
710
    Trace("cegqi-arith-debug") << "Normalize substitution for ";
711
    Trace("cegqi-arith-debug")
712
        << eq_lhs << " = " << sf.d_subs[index] << std::endl;
713
  }
714
253
  Assert(sf.d_vars[index].getType().isInteger());
715
  // must ensure that divisibility constraints are met
716
  // solve updated rewritten equality for vars[index], if coefficient is one,
717
  // then we are successful
718
506
  Node eq_rhs = sf.d_subs[index];
719
506
  Node eq = eq_lhs.eqNode(eq_rhs);
720
253
  eq = rewrite(eq);
721
253
  Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
722
506
  std::map<Node, Node> msum;
723
253
  if (!ArithMSum::getMonomialSumLit(eq, msum))
724
  {
725
41
    Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl;
726
41
    return false;
727
  }
728
424
  Node veq;
729
212
  if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) == 0)
730
  {
731
    Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl;
732
    return false;
733
  }
734
424
  Node veq_c;
735
212
  if (veq[0] != sf.d_vars[index])
736
  {
737
172
    Node veq_v;
738
86
    if (ArithMSum::getMonomial(veq[0], veq_c, veq_v))
739
    {
740
86
      Assert(veq_v == sf.d_vars[index]);
741
    }
742
  }
743
212
  sf.d_subs[index] = veq[1];
744
212
  if (!veq_c.isNull())
745
  {
746
86
    NodeManager* nm = NodeManager::currentNM();
747
86
    sf.d_subs[index] = nm->mkNode(INTS_DIVISION_TOTAL, veq[1], veq_c);
748
172
    Trace("cegqi-arith-debug")
749
86
        << "...bound type is : " << sf.d_props[index].d_type << std::endl;
750
    // intger division rounding up if from a lower bound
751
172
    if (sf.d_props[index].d_type == CEG_TT_UPPER
752
86
        && options().quantifiers.cegqiRoundUpLowerLia)
753
    {
754
      sf.d_subs[index] = nm->mkNode(
755
          PLUS,
756
          sf.d_subs[index],
757
          nm->mkNode(
758
              ITE,
759
              nm->mkNode(
760
                  EQUAL, nm->mkNode(INTS_MODULUS_TOTAL, veq[1], veq_c), d_zero),
761
              d_zero,
762
              d_one));
763
    }
764
  }
765
424
  Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index]
766
212
                             << " -> " << sf.d_subs[index] << std::endl;
767
212
  return true;
768
}
769
770
58006
CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci,
771
                                           Node pv,
772
                                           Node atom,
773
                                           Node& veq_c,
774
                                           Node& val,
775
                                           Node& vts_coeff_inf,
776
                                           Node& vts_coeff_delta)
777
{
778
58006
  NodeManager* nm = NodeManager::currentNM();
779
116012
  Trace("cegqi-arith-debug")
780
58006
      << "isolate for " << pv << " in " << atom << std::endl;
781
116012
  std::map<Node, Node> msum;
782
58006
  if (!ArithMSum::getMonomialSumLit(atom, msum))
783
  {
784
63564
    Trace("cegqi-arith-debug")
785
31782
        << "fail : could not get monomial sum" << std::endl;
786
31782
    return CEG_TT_INVALID;
787
  }
788
26224
  Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl;
789
26224
  if (Trace.isOn("cegqi-arith-debug"))
790
  {
791
    ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug");
792
  }
793
52448
  TypeNode pvtn = pv.getType();
794
  // remove vts symbols from polynomial
795
52448
  Node vts_coeff[2];
796
78672
  for (unsigned t = 0; t < 2; t++)
797
  {
798
52448
    if (!d_vts_sym[t].isNull())
799
    {
800
714
      std::map<Node, Node>::iterator itminf = msum.find(d_vts_sym[t]);
801
714
      if (itminf != msum.end())
802
      {
803
50
        vts_coeff[t] = itminf->second;
804
50
        if (vts_coeff[t].isNull())
805
        {
806
6
          vts_coeff[t] = nm->mkConst(Rational(1));
807
        }
808
        // negate if coefficient on variable is positive
809
50
        std::map<Node, Node>::iterator itv = msum.find(pv);
810
50
        if (itv != msum.end())
811
        {
812
          // multiply by the coefficient we will isolate for
813
50
          if (itv->second.isNull())
814
          {
815
12
            vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
816
          }
817
          else
818
          {
819
38
            if (!pvtn.isInteger())
820
            {
821
32
              vts_coeff[t] = nm->mkNode(
822
                  MULT,
823
16
                  nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()),
824
16
                  vts_coeff[t]);
825
8
              vts_coeff[t] = rewrite(vts_coeff[t]);
826
            }
827
30
            else if (itv->second.getConst<Rational>().sgn() == 1)
828
            {
829
              vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
830
            }
831
          }
832
        }
833
100
        Trace("cegqi-arith-debug")
834
50
            << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
835
50
        msum.erase(d_vts_sym[t]);
836
      }
837
    }
838
  }
839
840
26224
  int ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
841
26224
  if (ires == 0)
842
  {
843
1318
    Trace("cegqi-arith-debug") << "fail : isolate" << std::endl;
844
1318
    return CEG_TT_INVALID;
845
  }
846
24906
  if (Trace.isOn("cegqi-arith-debug"))
847
  {
848
    Trace("cegqi-arith-debug") << "Isolate : ";
849
    if (!veq_c.isNull())
850
    {
851
      Trace("cegqi-arith-debug") << veq_c << " * ";
852
    }
853
    Trace("cegqi-arith-debug")
854
        << pv << " " << atom.getKind() << " " << val << std::endl;
855
  }
856
  // when not pure LIA/LRA, we must check whether the lhs contains pv
857
24906
  if (expr::hasSubterm(val, pv))
858
  {
859
504
    Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
860
504
    return CEG_TT_INVALID;
861
  }
862
  // if its type is integer but the substitution is not integer
863
48804
  if (pvtn.isInteger()
864
73257
      && ((!veq_c.isNull() && !veq_c.getType().isInteger())
865
47854
          || !val.getType().isInteger()))
866
  {
867
    // redo, split integer/non-integer parts
868
51
    bool useCoeff = false;
869
102
    Integer coeff(1);
870
171
    for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
871
         ++it)
872
    {
873
120
      if (it->first.isNull() || it->first.getType().isInteger())
874
      {
875
77
        if (!it->second.isNull())
876
        {
877
61
          coeff = coeff.lcm(it->second.getConst<Rational>().getDenominator());
878
61
          useCoeff = true;
879
        }
880
      }
881
    }
882
    // multiply everything by this coefficient
883
102
    Node rcoeff = nm->mkConst(Rational(coeff));
884
102
    std::vector<Node> real_part;
885
171
    for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
886
         ++it)
887
    {
888
120
      if (useCoeff)
889
      {
890
108
        if (it->second.isNull())
891
        {
892
43
          msum[it->first] = rcoeff;
893
        }
894
        else
895
        {
896
65
          msum[it->first] = rewrite(nm->mkNode(MULT, it->second, rcoeff));
897
        }
898
      }
899
120
      if (!it->first.isNull() && !it->first.getType().isInteger())
900
      {
901
86
        real_part.push_back(msum[it->first].isNull()
902
172
                                ? it->first
903
86
                                : nm->mkNode(MULT, msum[it->first], it->first));
904
      }
905
    }
906
    // remove delta
907
51
    vts_coeff[1] = Node::null();
908
    // multiply inf
909
51
    if (!vts_coeff[0].isNull())
910
    {
911
      vts_coeff[0] = rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0]));
912
    }
913
51
    Node realPart = real_part.empty()
914
                        ? d_zero
915
86
                        : (real_part.size() == 1 ? real_part[0]
916
188
                                                 : nm->mkNode(PLUS, real_part));
917
51
    Assert(ci->isEligibleForInstantiation(realPart));
918
    // re-isolate
919
51
    Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
920
51
    veq_c = Node::null();
921
51
    ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
922
102
    Trace("cegqi-arith-debug")
923
51
        << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " "
924
51
        << atom.getKind() << " " << val << std::endl;
925
102
    Trace("cegqi-arith-debug")
926
51
        << "                 real part : " << realPart << std::endl;
927
51
    if (ires != 0)
928
    {
929
      int ires_use =
930
51
          (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
931
51
                                                                          : -1;
932
102
      val = rewrite(
933
204
          nm->mkNode(ires_use == -1 ? PLUS : MINUS,
934
102
                     nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart),
935
102
                     nm->mkNode(TO_INTEGER, realPart)));
936
      // could round up for upper bounds here
937
51
      Trace("cegqi-arith-debug") << "result : " << val << std::endl;
938
51
      Assert(val.getType().isInteger());
939
    }
940
    else
941
    {
942
      return CEG_TT_INVALID;
943
    }
944
  }
945
24402
  vts_coeff_inf = vts_coeff[0];
946
24402
  vts_coeff_delta = vts_coeff[1];
947
48804
  Trace("cegqi-arith-debug")
948
48804
      << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " "
949
24402
      << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")"
950
24402
      << std::endl;
951
24402
  Assert(ires != 0);
952
24402
  if (atom.getKind() == EQUAL)
953
  {
954
16986
    return CEG_TT_EQUAL;
955
  }
956
7416
  return ires == 1 ? CEG_TT_UPPER : CEG_TT_LOWER;
957
}
958
959
13935
Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
960
                                                     Node e,
961
                                                     Node t,
962
                                                     bool isLower,
963
                                                     Node c,
964
                                                     Node me,
965
                                                     Node mt,
966
                                                     Node theta,
967
                                                     Node inf_coeff,
968
                                                     Node delta_coeff)
969
{
970
13935
  NodeManager* nm = NodeManager::currentNM();
971
13935
  Node val = t;
972
13935
  Trace("cegqi-arith-bound2") << "Value : " << val << std::endl;
973
13935
  Assert(!e.getType().isInteger() || t.getType().isInteger());
974
13935
  Assert(!e.getType().isInteger() || mt.getType().isInteger());
975
  // add rho value
976
  // get the value of c*e
977
27870
  Node ceValue = me;
978
27870
  Node new_theta = theta;
979
13935
  if (!c.isNull())
980
  {
981
124
    Assert(c.getType().isInteger());
982
124
    ceValue = nm->mkNode(MULT, ceValue, c);
983
124
    ceValue = rewrite(ceValue);
984
124
    if (new_theta.isNull())
985
    {
986
86
      new_theta = c;
987
    }
988
    else
989
    {
990
38
      new_theta = nm->mkNode(MULT, new_theta, c);
991
38
      new_theta = rewrite(new_theta);
992
    }
993
124
    Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl;
994
124
    Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl;
995
  }
996
13935
  if (!new_theta.isNull() && e.getType().isInteger())
997
  {
998
554
    Node rho;
999
277
    if (isLower)
1000
    {
1001
155
      rho = nm->mkNode(MINUS, ceValue, mt);
1002
    }
1003
    else
1004
    {
1005
122
      rho = nm->mkNode(MINUS, mt, ceValue);
1006
    }
1007
277
    rho = rewrite(rho);
1008
554
    Trace("cegqi-arith-bound2")
1009
277
        << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
1010
554
    Trace("cegqi-arith-bound2")
1011
277
        << "..." << rho << " mod " << new_theta << " = ";
1012
277
    rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
1013
277
    rho = rewrite(rho);
1014
277
    Trace("cegqi-arith-bound2") << rho << std::endl;
1015
277
    Kind rk = isLower ? PLUS : MINUS;
1016
277
    val = nm->mkNode(rk, val, rho);
1017
277
    val = rewrite(val);
1018
277
    Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
1019
  }
1020
13935
  if (!inf_coeff.isNull())
1021
  {
1022
    Assert(!d_vts_sym[0].isNull());
1023
    val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
1024
    val = rewrite(val);
1025
  }
1026
13935
  if (!delta_coeff.isNull())
1027
  {
1028
    // create delta here if necessary
1029
119
    val = nm->mkNode(
1030
238
        PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
1031
119
    val = rewrite(val);
1032
  }
1033
27870
  return val;
1034
}
1035
1036
}  // namespace quantifiers
1037
}  // namespace theory
1038
31125
}  // namespace cvc5