GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp Lines: 299 350 85.4 %
Date: 2021-03-22 Branches: 671 1718 39.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_bv_instantiator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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_bv_instantiator
13
 **/
14
15
#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
16
17
#include <stack>
18
#include "options/quantifiers_options.h"
19
#include "theory/bv/theory_bv_utils.h"
20
#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
21
#include "theory/quantifiers_engine.h"
22
#include "theory/rewriter.h"
23
#include "util/bitvector.h"
24
#include "util/random.h"
25
26
using namespace std;
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
// this class can be used to query the model value through the CegInstaniator
34
// class
35
class CegInstantiatorBvInverterQuery : public BvInverterQuery
36
{
37
 public:
38
2913
  CegInstantiatorBvInverterQuery(CegInstantiator* ci)
39
2913
      : BvInverterQuery(), d_ci(ci)
40
  {
41
2913
  }
42
2913
  ~CegInstantiatorBvInverterQuery() {}
43
  /** return the model value of n */
44
  Node getModelValue(Node n) override { return d_ci->getModelValue(n); }
45
  /** get bound variable of type tn */
46
1112
  Node getBoundVariable(TypeNode tn) override
47
  {
48
1112
    return d_ci->getBoundVariable(tn);
49
  }
50
51
 protected:
52
  // pointer to class that is able to query model values
53
  CegInstantiator* d_ci;
54
};
55
56
1198
BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv)
57
1198
    : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0)
58
{
59
  // The inverter utility d_inverter is global to all BvInstantiator classes.
60
  // This must be global since we need to:
61
  // * process Skolem functions properly across multiple variables within the
62
  // same quantifier
63
  // * cache Skolem variables uniformly across multiple quantified formulas
64
1198
}
65
66
2396
BvInstantiator::~BvInstantiator() {}
67
4337
void BvInstantiator::reset(CegInstantiator* ci,
68
                           SolvedForm& sf,
69
                           Node pv,
70
                           CegInstEffort effort)
71
{
72
4337
  d_inst_id_counter = 0;
73
4337
  d_var_to_inst_id.clear();
74
4337
  d_inst_id_to_term.clear();
75
4337
  d_inst_id_to_alit.clear();
76
4337
  d_var_to_curr_inst_id.clear();
77
4337
  d_alit_to_model_slack.clear();
78
4337
}
79
80
3184
void BvInstantiator::processLiteral(CegInstantiator* ci,
81
                                    SolvedForm& sf,
82
                                    Node pv,
83
                                    Node lit,
84
                                    Node alit,
85
                                    CegInstEffort effort)
86
{
87
3184
  Assert(d_inverter != NULL);
88
  // find path to pv
89
6368
  std::vector<unsigned> path;
90
6368
  Node sv = d_inverter->getSolveVariable(pv.getType());
91
6368
  Node pvs = ci->getModelValue(pv);
92
3184
  Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
93
  Node slit =
94
9552
      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl());
95
3184
  if (!slit.isNull())
96
  {
97
5826
    CegInstantiatorBvInverterQuery m(ci);
98
2913
    unsigned iid = d_inst_id_counter;
99
2913
    Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
100
5826
    Node inst = d_inverter->solveBvLit(sv, slit, path, &m);
101
2913
    if (!inst.isNull())
102
    {
103
1893
      inst = Rewriter::rewrite(inst);
104
1893
      if (inst.isConst() || !ci->hasNestedQuantification())
105
      {
106
1857
        Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
107
        // store information for id and increment
108
1857
        d_var_to_inst_id[pv].push_back(iid);
109
1857
        d_inst_id_to_term[iid] = inst;
110
1857
        d_inst_id_to_alit[iid] = alit;
111
1857
        d_inst_id_counter++;
112
      }
113
    }
114
    else
115
    {
116
1020
      Trace("cegqi-bv") << "...failed to solve." << std::endl;
117
    }
118
  }
119
  else
120
  {
121
271
    Trace("cegqi-bv") << "...no path." << std::endl;
122
  }
123
3184
}
124
125
3710
bool BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
126
                                         SolvedForm& sf,
127
                                         Node pv,
128
                                         CegInstEffort effort)
129
{
130
3710
  return true;
131
}
132
133
7815
Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
134
                                         SolvedForm& sf,
135
                                         Node pv,
136
                                         Node lit,
137
                                         CegInstEffort effort)
138
{
139
7815
  if (effort == CEG_INST_EFFORT_FULL)
140
  {
141
    // always use model values at full effort
142
1198
    return Node::null();
143
  }
144
13234
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
145
6617
  bool pol = lit.getKind() != NOT;
146
6617
  Kind k = atom.getKind();
147
6617
  if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT)
148
  {
149
    // others are unhandled
150
    return Node::null();
151
  }
152
6617
  else if (!atom[0].getType().isBitVector())
153
  {
154
    return Node::null();
155
  }
156
23245
  else if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::KEEP
157
6617
           || (pol && k == EQUAL))
158
  {
159
3387
    return lit;
160
  }
161
3230
  NodeManager* nm = NodeManager::currentNM();
162
6460
  Node s = atom[0];
163
6460
  Node t = atom[1];
164
165
6460
  Node sm = ci->getModelValue(s);
166
6460
  Node tm = ci->getModelValue(t);
167
3230
  Assert(!sm.isNull() && sm.isConst());
168
3230
  Assert(!tm.isNull() && tm.isConst());
169
3230
  Trace("cegqi-bv") << "Model value: " << std::endl;
170
6460
  Trace("cegqi-bv") << "   " << s << " " << k << " " << t << " is "
171
3230
                    << std::endl;
172
3230
  Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
173
174
6460
  Node ret;
175
3230
  if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::EQ_SLACK)
176
  {
177
    // if using slack, we convert constraints to a positive equality based on
178
    // the current model M, e.g.:
179
    //   (not) s ~ t  --->  s = t + ( s^M - t^M )
180
    if (sm != tm)
181
    {
182
      Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm));
183
      Assert(slack.isConst());
184
      // remember the slack value for the asserted literal
185
      d_alit_to_model_slack[lit] = slack;
186
      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
187
      Trace("cegqi-bv") << "Slack is " << slack << std::endl;
188
    }
189
    else
190
    {
191
      ret = s.eqNode(t);
192
    }
193
  }
194
  else
195
  {
196
    // turn disequality into an inequality
197
    // e.g. s != t becomes s < t or t < s
198
3230
    if (k == EQUAL)
199
    {
200
1570
      if (Random::getRandom().pickWithProb(0.5))
201
      {
202
725
        std::swap(s, t);
203
      }
204
1570
      pol = true;
205
    }
206
    // otherwise, we optimistically solve for the boundary point of an
207
    // inequality, for example:
208
    //   for s < t, we solve s+1 = t
209
    //   for ~( s < t ), we solve s = t
210
    // notice that this equality does not necessarily hold in the model, and
211
    // hence the corresponding instantiation strategy is not guaranteed to be
212
    // monotonic.
213
3230
    if (!pol)
214
    {
215
987
      ret = s.eqNode(t);
216
    }
217
    else
218
    {
219
4486
      Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
220
2243
      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
221
    }
222
  }
223
3230
  Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
224
3230
  return ret;
225
}
226
227
4182
bool BvInstantiator::processAssertion(CegInstantiator* ci,
228
                                      SolvedForm& sf,
229
                                      Node pv,
230
                                      Node lit,
231
                                      Node alit,
232
                                      CegInstEffort effort)
233
{
234
  // if option enabled, use approach for word-level inversion for BV
235
  // instantiation
236
4182
  if (options::cegqiBv())
237
  {
238
    // get the best rewritten form of lit for solving for pv
239
    //   this should remove instances of non-invertible operators, and
240
    //   "linearize" lit with respect to pv as much as possible
241
6368
    Node rlit = rewriteAssertionForSolvePv(ci, pv, lit);
242
3184
    if (Trace.isOn("cegqi-bv"))
243
    {
244
      Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv
245
                        << " in " << lit << std::endl;
246
      if (lit != rlit)
247
      {
248
        Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
249
      }
250
    }
251
3184
    if (!rlit.isNull())
252
    {
253
3184
      processLiteral(ci, sf, pv, rlit, alit, effort);
254
    }
255
  }
256
4182
  return false;
257
}
258
259
2756
bool BvInstantiator::useModelValue(CegInstantiator* ci,
260
                                   SolvedForm& sf,
261
                                   Node pv,
262
                                   CegInstEffort effort)
263
{
264
2756
  return effort < CEG_INST_EFFORT_FULL || options::cegqiFullEffort();
265
}
266
267
3710
bool BvInstantiator::processAssertions(CegInstantiator* ci,
268
                                       SolvedForm& sf,
269
                                       Node pv,
270
                                       CegInstEffort effort)
271
{
272
  std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::iterator
273
3710
      iti = d_var_to_inst_id.find(pv);
274
3710
  if (iti == d_var_to_inst_id.end())
275
  {
276
    // no bounds
277
2129
    return false;
278
  }
279
3162
  Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv
280
1581
                    << std::endl;
281
  // if interleaving, do not do inversion half the time
282
3162
  if (options::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
283
  {
284
    Trace("cegqi-bv") << "...do not do instantiation for " << pv
285
                      << " (skip, based on heuristic)" << std::endl;
286
  }
287
1581
  bool firstVar = sf.empty();
288
  // get inst id list
289
1581
  if (Trace.isOn("cegqi-bv"))
290
  {
291
    Trace("cegqi-bv") << "  " << iti->second.size()
292
                      << " candidate instantiations for " << pv << " : "
293
                      << std::endl;
294
    if (firstVar)
295
    {
296
      Trace("cegqi-bv") << "  ...this is the first variable" << std::endl;
297
    }
298
  }
299
  // until we have a model-preserving selection function for BV, this must
300
  // be heuristic (we only pick one literal)
301
  // hence we randomize the list
302
  // this helps robustness, since picking the same literal every time may
303
  // lead to a stream of value instantiations, whereas with randomization
304
  // we may find an invertible literal that leads to a useful instantiation.
305
1581
  std::shuffle(iti->second.begin(), iti->second.end(), Random::getRandom());
306
307
1581
  if (Trace.isOn("cegqi-bv"))
308
  {
309
    for (unsigned j = 0, size = iti->second.size(); j < size; j++)
310
    {
311
      unsigned inst_id = iti->second[j];
312
      Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
313
      Node inst_term = d_inst_id_to_term[inst_id];
314
      Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
315
      Node alit = d_inst_id_to_alit[inst_id];
316
317
      // get the slack value introduced for the asserted literal
318
      Node curr_slack_val;
319
      std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
320
          d_alit_to_model_slack.find(alit);
321
      if (itms != d_alit_to_model_slack.end())
322
      {
323
        curr_slack_val = itms->second;
324
      }
325
326
      // debug printing
327
      Trace("cegqi-bv") << "   [" << j << "] : ";
328
      Trace("cegqi-bv") << inst_term << std::endl;
329
      if (!curr_slack_val.isNull())
330
      {
331
        Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
332
                          << std::endl;
333
      }
334
      Trace("cegqi-bv-debug") << "   ...from : " << alit << std::endl;
335
      Trace("cegqi-bv") << std::endl;
336
    }
337
  }
338
339
  // Now, try all instantiation ids we want to try
340
  // Typically we try only one, otherwise worst-case performance
341
  // for constructing instantiations is exponential on the number of
342
  // variables in this quantifier prefix.
343
1581
  bool ret = false;
344
1581
  bool tryMultipleInst = firstVar && options::cegqiMultiInst();
345
1581
  bool revertOnSuccess = tryMultipleInst;
346
1581
  for (unsigned j = 0, size = iti->second.size(); j < size; j++)
347
  {
348
1581
    unsigned inst_id = iti->second[j];
349
1581
    Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
350
1581
    Node inst_term = d_inst_id_to_term[inst_id];
351
1581
    Node alit = d_inst_id_to_alit[inst_id];
352
    // try instantiation pv -> inst_term
353
1581
    TermProperties pv_prop_bv;
354
1581
    Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl;
355
1581
    d_var_to_curr_inst_id[pv] = inst_id;
356
1581
    ci->markSolved(alit);
357
1581
    if (ci->constructInstantiationInc(
358
            pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
359
    {
360
895
      ret = true;
361
    }
362
1581
    ci->markSolved(alit, false);
363
    // we are done unless we try multiple instances
364
1581
    if (!tryMultipleInst)
365
    {
366
1581
      break;
367
    }
368
  }
369
1581
  if (ret)
370
  {
371
895
    return true;
372
  }
373
686
  Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl;
374
686
  d_var_to_curr_inst_id.erase(pv);
375
376
686
  return false;
377
}
378
379
3184
Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
380
                                                Node pv,
381
                                                Node lit)
382
{
383
  // result of rewriting the visited term
384
6368
  std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
385
3184
  visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
386
  // whether the visited term contains pv
387
6368
  std::unordered_map<Node, bool, NodeHashFunction> visited_contains_pv;
388
3184
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
389
6368
  std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
390
6368
  std::stack<std::stack<TNode> > visit;
391
6368
  TNode cur;
392
3184
  visit.push(std::stack<TNode>());
393
3184
  visit.top().push(lit);
394
82123
  do
395
  {
396
85307
    cur = visit.top().top();
397
85307
    visit.top().pop();
398
85307
    it = visited.top().find(cur);
399
400
85307
    if (it == visited.top().end())
401
    {
402
      std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc =
403
34458
          curr_subs.find(cur);
404
34458
      if (itc != curr_subs.end())
405
      {
406
112
        visited.top()[cur] = itc->second;
407
      }
408
      else
409
      {
410
34346
        if (cur.getKind() == WITNESS)
411
        {
412
          // must replace variables of choice functions
413
          // with new variables to avoid variable
414
          // capture when considering substitutions
415
          // with multiple literals.
416
224
          Node bv = ci->getBoundVariable(cur[0][0].getType());
417
          // should not have captured variables
418
112
          Assert(curr_subs.find(cur[0][0]) == curr_subs.end());
419
112
          curr_subs[cur[0][0]] = bv;
420
          // we cannot cache the results of subterms
421
          // of this witness expression since we are
422
          // now in the context { cur[0][0] -> bv },
423
          // hence we push a context here
424
112
          visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
425
112
          visit.push(std::stack<TNode>());
426
        }
427
34346
        visited.top()[cur] = Node::null();
428
34346
        visit.top().push(cur);
429
82123
        for (unsigned i = 0; i < cur.getNumChildren(); i++)
430
        {
431
47777
          visit.top().push(cur[i]);
432
        }
433
      }
434
    }
435
50849
    else if (it->second.isNull())
436
    {
437
68692
      Node ret;
438
34346
      bool childChanged = false;
439
68692
      std::vector<Node> children;
440
34346
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
441
      {
442
3595
        children.push_back(cur.getOperator());
443
      }
444
34346
      bool contains_pv = (cur == pv);
445
82123
      for (unsigned i = 0; i < cur.getNumChildren(); i++)
446
      {
447
47777
        it = visited.top().find(cur[i]);
448
47777
        Assert(it != visited.top().end());
449
47777
        Assert(!it->second.isNull());
450
47777
        childChanged = childChanged || cur[i] != it->second;
451
47777
        children.push_back(it->second);
452
47777
        contains_pv = contains_pv || visited_contains_pv[cur[i]];
453
      }
454
      // careful that rewrites above do not affect whether this term contains pv
455
34346
      visited_contains_pv[cur] = contains_pv;
456
457
      // rewrite the term
458
34346
      ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv);
459
460
      // return original if the above function does not produce a result
461
34346
      if (ret.isNull())
462
      {
463
33853
        if (childChanged)
464
        {
465
2314
          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
466
        }
467
        else
468
        {
469
31539
          ret = cur;
470
        }
471
      }
472
473
      /* We need to update contains_pv also for rewritten nodes, since
474
       * the normalizePv* functions rely on the information if pv occurs in a
475
       * rewritten node or not. */
476
34346
      if (ret != cur)
477
      {
478
2653
        contains_pv = (ret == pv);
479
8960
        for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i)
480
        {
481
6307
          contains_pv = contains_pv || visited_contains_pv[ret[i]];
482
        }
483
2653
        visited_contains_pv[ret] = contains_pv;
484
      }
485
486
      // if was witness, pop context
487
34346
      if (cur.getKind() == WITNESS)
488
      {
489
112
        Assert(curr_subs.find(cur[0][0]) != curr_subs.end());
490
112
        curr_subs.erase(cur[0][0]);
491
112
        visited.pop();
492
112
        visit.pop();
493
112
        Assert(visited.size() == visit.size());
494
112
        Assert(!visit.empty());
495
      }
496
497
34346
      visited.top()[cur] = ret;
498
    }
499
85307
  } while (!visit.top().empty());
500
3184
  Assert(visited.size() == 1);
501
3184
  Assert(visited.top().find(lit) != visited.top().end());
502
3184
  Assert(!visited.top().find(lit)->second.isNull());
503
504
3184
  Node result = visited.top()[lit];
505
506
3184
  if (Trace.isOn("cegqi-bv-nl"))
507
  {
508
    std::vector<TNode> trace_visit;
509
    std::unordered_set<TNode, TNodeHashFunction> trace_visited;
510
511
    trace_visit.push_back(result);
512
    do
513
    {
514
      cur = trace_visit.back();
515
      trace_visit.pop_back();
516
517
      if (trace_visited.find(cur) == trace_visited.end())
518
      {
519
        trace_visited.insert(cur);
520
        trace_visit.insert(trace_visit.end(), cur.begin(), cur.end());
521
      }
522
      else if (cur == pv)
523
      {
524
        Trace("cegqi-bv-nl")
525
            << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl;
526
      }
527
    } while (!trace_visit.empty());
528
  }
529
530
6368
  return result;
531
}
532
533
34346
Node BvInstantiator::rewriteTermForSolvePv(
534
    Node pv,
535
    Node n,
536
    std::vector<Node>& children,
537
    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
538
{
539
34346
  NodeManager* nm = NodeManager::currentNM();
540
541
  // [1] rewrite cases of non-invertible operators
542
543
34346
  if (n.getKind() == EQUAL)
544
  {
545
13716
    TNode lhs = children[0];
546
13716
    TNode rhs = children[1];
547
548
    /* rewrite: x * x = x -> x < 2 */
549
14132
    if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv
550
6942
         && rhs[1] == pv)
551
27772
        || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv
552
6950
            && lhs[1] == pv))
553
    {
554
      return nm->mkNode(
555
          BITVECTOR_ULT,
556
          pv,
557
4
          bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
558
    }
559
560
16668
    if (options::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
561
    {
562
328
      Node result = utils::normalizePvEqual(pv, children, contains_pv);
563
164
      if (!result.isNull())
564
      {
565
8
        Trace("cegqi-bv-nl")
566
4
            << "Normalize " << n << " to " << result << std::endl;
567
      }
568
      else
569
      {
570
320
        Trace("cegqi-bv-nl")
571
160
            << "Nonlinear " << n.getKind() << " " << n << std::endl;
572
      }
573
164
      return result;
574
    }
575
  }
576
27404
  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
577
  {
578
2792
    if (options::cegqiBvLinearize() && contains_pv[n])
579
    {
580
1885
      Node result;
581
1185
      if (n.getKind() == BITVECTOR_MULT)
582
      {
583
246
        result = utils::normalizePvMult(pv, children, contains_pv);
584
      }
585
      else
586
      {
587
939
        result = utils::normalizePvPlus(pv, children, contains_pv);
588
      }
589
1185
      if (!result.isNull())
590
      {
591
970
        Trace("cegqi-bv-nl")
592
485
            << "Normalize " << n << " to " << result << std::endl;
593
485
        return result;
594
      }
595
      else
596
      {
597
1400
        Trace("cegqi-bv-nl")
598
700
            << "Nonlinear " << n.getKind() << " " << n << std::endl;
599
      }
600
    }
601
  }
602
603
  // [2] try to rewrite non-linear literals -> linear literals
604
605
33693
  return Node::null();
606
}
607
608
/** sort bv extract interval
609
 *
610
 * This sorts lists of bitvector extract terms where
611
 * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
612
 * if i1>j1 or i1=j1 and i2>j2.
613
 */
614
struct SortBvExtractInterval
615
{
616
118
  bool operator()(Node i, Node j)
617
  {
618
118
    Assert(i.getKind() == BITVECTOR_EXTRACT);
619
118
    Assert(j.getKind() == BITVECTOR_EXTRACT);
620
118
    BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
621
118
    BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
622
118
    if (ie.d_high > je.d_high)
623
    {
624
114
      return true;
625
    }
626
4
    else if (ie.d_high == je.d_high)
627
    {
628
2
      Assert(ie.d_low != je.d_low);
629
2
      return ie.d_low > je.d_low;
630
    }
631
2
    return false;
632
  }
633
};
634
635
714
void BvInstantiatorPreprocess::registerCounterexampleLemma(
636
    Node lem, std::vector<Node>& ceVars, std::vector<Node>& auxLems)
637
{
638
  // new variables
639
1428
  std::vector<Node> vars;
640
  // new lemmas
641
1428
  std::vector<Node> new_lems;
642
643
1432
  if (options::cegqiBvRmExtract())
644
  {
645
714
    NodeManager* nm = NodeManager::currentNM();
646
714
    Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
647
    // map from terms to bitvector extracts applied to that term
648
1428
    std::map<Node, std::vector<Node> > extract_map;
649
1428
    std::unordered_set<TNode, TNodeHashFunction> visited;
650
714
    Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl;
651
714
    collectExtracts(lem, extract_map, visited);
652
852
    for (std::pair<const Node, std::vector<Node> >& es : extract_map)
653
    {
654
      // sort based on the extract start position
655
138
      std::vector<Node>& curr_vec = es.second;
656
657
      SortBvExtractInterval sbei;
658
138
      std::sort(curr_vec.begin(), curr_vec.end(), sbei);
659
660
138
      unsigned width = es.first.getType().getBitVectorSize();
661
662
      // list of points b such that:
663
      //   b>0 and we must start a segment at (b-1)  or  b==0
664
276
      std::vector<unsigned> boundaries;
665
138
      boundaries.push_back(width);
666
138
      boundaries.push_back(0);
667
668
138
      Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
669
392
      for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
670
      {
671
254
        Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
672
        BitVectorExtract e =
673
254
            curr_vec[i].getOperator().getConst<BitVectorExtract>();
674
762
        if (std::find(boundaries.begin(), boundaries.end(), e.d_high + 1)
675
762
            == boundaries.end())
676
        {
677
22
          boundaries.push_back(e.d_high + 1);
678
        }
679
762
        if (std::find(boundaries.begin(), boundaries.end(), e.d_low)
680
762
            == boundaries.end())
681
        {
682
118
          boundaries.push_back(e.d_low);
683
        }
684
      }
685
138
      std::sort(boundaries.rbegin(), boundaries.rend());
686
687
      // make the extract variables
688
276
      std::vector<Node> children;
689
416
      for (unsigned i = 1; i < boundaries.size(); i++)
690
      {
691
278
        Assert(boundaries[i - 1] > 0);
692
        Node ex = bv::utils::mkExtract(
693
556
            es.first, boundaries[i - 1] - 1, boundaries[i]);
694
        Node var =
695
            nm->mkSkolem("ek",
696
556
                         ex.getType(),
697
1112
                         "variable to represent disjoint extract region");
698
278
        children.push_back(var);
699
278
        vars.push_back(var);
700
      }
701
702
276
      Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
703
138
      Assert(conc.getType() == es.first.getType());
704
276
      Node eq_lem = conc.eqNode(es.first);
705
138
      Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
706
138
      new_lems.push_back(eq_lem);
707
276
      Trace("cegqi-bv-pp") << "...finished processing extracts for term "
708
138
                           << es.first << std::endl;
709
    }
710
714
    Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
711
  }
712
713
714
  if (!vars.empty())
714
  {
715
    // could try applying subs -> vars here
716
    // in practice, this led to worse performance
717
718
148
    Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
719
74
                         << std::endl;
720
74
    auxLems.insert(auxLems.end(), new_lems.begin(), new_lems.end());
721
148
    Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
722
74
                         << std::endl;
723
74
    ceVars.insert(ceVars.end(), vars.begin(), vars.end());
724
  }
725
714
}
726
727
714
void BvInstantiatorPreprocess::collectExtracts(
728
    Node lem,
729
    std::map<Node, std::vector<Node> >& extract_map,
730
    std::unordered_set<TNode, TNodeHashFunction>& visited)
731
{
732
1428
  std::vector<TNode> visit;
733
1428
  TNode cur;
734
714
  visit.push_back(lem);
735
9089
  do
736
  {
737
9803
    cur = visit.back();
738
9803
    visit.pop_back();
739
9803
    if (visited.find(cur) == visited.end())
740
    {
741
8343
      visited.insert(cur);
742
8343
      if (cur.getKind() != FORALL)
743
      {
744
8335
        if (cur.getKind() == BITVECTOR_EXTRACT)
745
        {
746
337
          if (cur[0].getKind() == INST_CONSTANT)
747
          {
748
254
            extract_map[cur[0]].push_back(cur);
749
          }
750
        }
751
752
17424
        for (const Node& nc : cur)
753
        {
754
9089
          visit.push_back(nc);
755
        }
756
      }
757
    }
758
9803
  } while (!visit.empty());
759
714
}
760
761
}  // namespace quantifiers
762
}  // namespace theory
763
51900
}  // namespace CVC4