GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp Lines: 449 527 85.2 %
Date: 2021-03-23 Branches: 1172 2808 41.7 %

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