GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/abstraction.cpp Lines: 173 631 27.4 %
Date: 2021-03-23 Branches: 275 2758 10.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file abstraction.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Aina Niemetz, Mathias Preiner
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
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
#include "theory/bv/abstraction.h"
16
17
#include "options/bv_options.h"
18
#include "printer/printer.h"
19
#include "smt/dump.h"
20
#include "smt/smt_engine.h"
21
#include "smt/smt_engine_scope.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "theory/bv/theory_bv_utils.h"
24
#include "theory/rewriter.h"
25
26
using namespace CVC4;
27
using namespace CVC4::theory;
28
using namespace CVC4::theory::bv;
29
using namespace CVC4::context;
30
31
using namespace std;
32
using namespace CVC4::theory::bv::utils;
33
34
3
bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
35
                                         std::vector<Node>& new_assertions)
36
{
37
3
  Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n";
38
39
6
  TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime);
40
41
6
  TNodeSet seen;
42
11
  for (unsigned i = 0; i < assertions.size(); ++i)
43
  {
44
8
    if (assertions[i].getKind() == kind::OR)
45
    {
46
19
      for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j)
47
      {
48
14
        if (!isConjunctionOfAtoms(assertions[i][j], seen))
49
        {
50
2
          continue;
51
        }
52
24
        Node signature = computeSignature(assertions[i][j]);
53
12
        storeSignature(signature, assertions[i][j]);
54
12
        Debug("bv-abstraction") << "   assertion: " << assertions[i][j] << "\n";
55
12
        Debug("bv-abstraction") << "   signature: " << signature << "\n";
56
      }
57
    }
58
  }
59
3
  finalizeSignatures();
60
61
11
  for (unsigned i = 0; i < assertions.size(); ++i)
62
  {
63
16
    if (assertions[i].getKind() == kind::OR
64
16
        && assertions[i][0].getKind() == kind::AND)
65
    {
66
2
      std::vector<Node> new_children;
67
3
      for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j)
68
      {
69
2
        if (hasSignature(assertions[i][j]))
70
        {
71
          new_children.push_back(abstractSignatures(assertions[i][j]));
72
        }
73
        else
74
        {
75
2
          new_children.push_back(assertions[i][j]);
76
        }
77
      }
78
1
      new_assertions.push_back(utils::mkOr(new_children));
79
    }
80
    else
81
    {
82
      // assertions that are not changed
83
7
      new_assertions.push_back(assertions[i]);
84
    }
85
  }
86
87
6
  if (options::skolemizeArguments())
88
  {
89
    skolemizeArguments(new_assertions);
90
  }
91
92
  // if we are using the eager solver reverse the abstraction
93
3
  if (options::bitblastMode() == options::BitblastMode::EAGER)
94
  {
95
1
    if (d_funcToSignature.size() == 0)
96
    {
97
      // we did not change anything
98
1
      return false;
99
    }
100
    NodeNodeMap seen_rev;
101
    for (unsigned i = 0; i < new_assertions.size(); ++i)
102
    {
103
      new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev);
104
    }
105
    // we undo the abstraction functions so the logic is QF_BV still
106
    return true;
107
  }
108
109
  // return true if we have created new function symbols for the problem
110
2
  return d_funcToSignature.size() != 0;
111
}
112
113
16
bool AbstractionModule::isConjunctionOfAtoms(TNode node, TNodeSet& seen)
114
{
115
16
  if (seen.find(node)!= seen.end())
116
    return true;
117
118
16
  if (!node.getType().isBitVector() && node.getKind() != kind::AND)
119
  {
120
14
    return utils::isBVPredicate(node);
121
  }
122
123
2
  if (node.getNumChildren() == 0)
124
    return true;
125
126
2
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
127
2
    if (!isConjunctionOfAtoms(node[i], seen))
128
    {
129
2
      return false;
130
    }
131
  }
132
  seen.insert(node);
133
  return true;
134
}
135
136
137
Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
138
139
  if (seen.find(assertion) != seen.end())
140
    return seen[assertion];
141
142
  if (isAbstraction(assertion)) {
143
    Node interp =  getInterpretation(assertion);
144
    seen[assertion] = interp;
145
    Assert(interp.getType() == assertion.getType());
146
    return interp;
147
  }
148
149
  if (assertion.getNumChildren() == 0) {
150
    seen[assertion] = assertion;
151
    return assertion;
152
  }
153
154
  NodeBuilder<> result(assertion.getKind());
155
  if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
156
    result << assertion.getOperator();
157
  }
158
159
  for (unsigned i = 0; i < assertion.getNumChildren(); ++i) {
160
    result << reverseAbstraction(assertion[i], seen);
161
  }
162
  Node res = result;
163
  seen[assertion] = res;
164
  return res;
165
}
166
167
void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
168
{
169
  NodeManager* nm = NodeManager::currentNM();
170
  for (unsigned i = 0; i < assertions.size(); ++i)
171
  {
172
    TNode assertion = assertions[i];
173
    if (assertion.getKind() != kind::OR) continue;
174
175
    bool is_skolemizable = true;
176
    for (unsigned k = 0; k < assertion.getNumChildren(); ++k)
177
    {
178
      if (assertion[k].getKind() != kind::EQUAL
179
          || assertion[k][0].getKind() != kind::APPLY_UF
180
          || assertion[k][1].getKind() != kind::CONST_BITVECTOR
181
          || assertion[k][1].getConst<BitVector>() != BitVector(1, 1u))
182
      {
183
        is_skolemizable = false;
184
        break;
185
      }
186
    }
187
188
    if (!is_skolemizable) continue;
189
190
    ArgsTable assertion_table;
191
192
    // collect function symbols and their arguments
193
    for (unsigned j = 0; j < assertion.getNumChildren(); ++j)
194
    {
195
      TNode current = assertion[j];
196
      Assert(current.getKind() == kind::EQUAL
197
             && current[0].getKind() == kind::APPLY_UF);
198
      TNode func = current[0];
199
      ArgsVec args;
200
      for (unsigned k = 0; k < func.getNumChildren(); ++k)
201
      {
202
        args.push_back(func[k]);
203
      }
204
      assertion_table.addEntry(func.getOperator(), args);
205
    }
206
207
    NodeBuilder<> assertion_builder(kind::OR);
208
    // construct skolemized assertion
209
    for (ArgsTable::iterator it = assertion_table.begin();
210
         it != assertion_table.end();
211
         ++it)
212
    {
213
      // for each function symbol
214
      ++(d_statistics.d_numArgsSkolemized);
215
      TNode func = it->first;
216
      ArgsTableEntry& args = it->second;
217
      NodeBuilder<> skolem_func(kind::APPLY_UF);
218
      skolem_func << func;
219
      std::vector<Node> skolem_args;
220
221
      for (unsigned j = 0; j < args.getArity(); ++j)
222
      {
223
        bool all_same = true;
224
        for (unsigned k = 1; k < args.getNumEntries(); ++k)
225
        {
226
          if (args.getEntry(k)[j] != args.getEntry(0)[j]) all_same = false;
227
        }
228
        Node new_arg = all_same
229
                           ? (Node)args.getEntry(0)[j]
230
                           : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
231
        skolem_args.push_back(new_arg);
232
        skolem_func << new_arg;
233
      }
234
235
      Node skolem_func_eq1 =
236
          nm->mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
237
238
      // enumerate arguments assignments
239
      std::vector<Node> or_assignments;
240
      for (const ArgsVec& av : args)
241
      // for (ArgsTableEntry::iterator it = args.begin(); it != args.end();
242
      // ++it)
243
      {
244
        NodeBuilder<> arg_assignment(kind::AND);
245
        // ArgsVec& args = *it;
246
        for (unsigned k = 0; k < av.size(); ++k)
247
        {
248
          Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]);
249
          arg_assignment << eq;
250
        }
251
        or_assignments.push_back(arg_assignment);
252
      }
253
254
      Node new_func_def =
255
        utils::mkAnd(skolem_func_eq1, utils::mkOr(or_assignments));
256
      assertion_builder << new_func_def;
257
    }
258
    Node new_assertion = assertion_builder;
259
    Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments "
260
                                << assertions[i] << " => \n";
261
    Debug("bv-abstraction-dbg") << "    " << new_assertion;
262
    assertions[i] = new_assertion;
263
  }
264
}
265
266
12
void AbstractionModule::storeSignature(Node signature, TNode assertion) {
267
12
  if(d_signatures.find(signature) == d_signatures.end()) {
268
4
    d_signatures[signature] = 0;
269
  }
270
12
  d_signatures[signature] = d_signatures[signature] + 1;
271
12
  d_assertionToSignature[assertion] = signature;
272
12
}
273
274
12
Node AbstractionModule::computeSignature(TNode node) {
275
12
  resetSignatureIndex();
276
24
  NodeNodeMap cache;
277
12
  Node sig = computeSignatureRec(node, cache);
278
24
  return sig;
279
}
280
281
36
Node AbstractionModule::getSignatureSkolem(TNode node)
282
{
283
36
  Assert(node.getMetaKind() == kind::metakind::VARIABLE);
284
36
  NodeManager* nm = NodeManager::currentNM();
285
36
  unsigned bitwidth = utils::getSize(node);
286
36
  if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end())
287
  {
288
2
    d_signatureSkolems[bitwidth] = vector<Node>();
289
  }
290
291
36
  vector<Node>& skolems = d_signatureSkolems[bitwidth];
292
  // get the index of bv variables of this size
293
36
  unsigned index = getBitwidthIndex(bitwidth);
294
36
  Assert(skolems.size() + 1 >= index);
295
36
  if (skolems.size() == index)
296
  {
297
12
    ostringstream os;
298
6
    os << "sig_" << bitwidth << "_" << index;
299
18
    skolems.push_back(nm->mkSkolem(os.str(),
300
12
                                   nm->mkBitVectorType(bitwidth),
301
                                   "skolem for computing signatures"));
302
  }
303
36
  ++(d_signatureIndices[bitwidth]);
304
36
  return skolems[index];
305
}
306
307
36
unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) {
308
36
  if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) {
309
2
    d_signatureIndices[bitwidth] = 0;
310
  }
311
36
  return d_signatureIndices[bitwidth];
312
}
313
314
12
void AbstractionModule::resetSignatureIndex() {
315
22
  for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) {
316
10
    it->second = 0;
317
  }
318
12
}
319
320
2
bool AbstractionModule::hasSignature(Node node) {
321
2
  return d_assertionToSignature.find(node) != d_assertionToSignature.end();
322
}
323
324
Node AbstractionModule::getGeneralizedSignature(Node node) {
325
  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
326
  Assert(it != d_assertionToSignature.end());
327
  Node generalized_signature = getGeneralization(it->second);
328
  return generalized_signature;
329
}
330
331
108
Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
332
108
  if (cache.find(node) != cache.end()) {
333
    return cache.find(node)->second;
334
  }
335
336
108
  if (node.getNumChildren() == 0) {
337
60
    if (node.getKind() == kind::CONST_BITVECTOR)
338
24
      return node;
339
340
72
    Node sig = getSignatureSkolem(node);
341
36
    cache[node] = sig;
342
36
    return sig;
343
  }
344
345
96
  NodeBuilder<> builder(node.getKind());
346
48
  if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
347
    builder << node.getOperator();
348
  }
349
144
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
350
192
    Node converted = computeSignatureRec(node[i], cache);
351
96
    builder << converted;
352
  }
353
96
  Node result = builder;
354
48
  cache[node] = result;
355
48
  return result;
356
}
357
358
/**
359
 * Returns 0, if the two are equal,
360
 * 1 if s is a generalization of t
361
 * 2 if t is a generalization of s
362
 * -1 if the two cannot be unified
363
 *
364
 * @param s
365
 * @param t
366
 *
367
 * @return
368
 */
369
8
int AbstractionModule::comparePatterns(TNode s, TNode t) {
370
10
  if (s.getKind() == kind::SKOLEM &&
371
2
      t.getKind() == kind::SKOLEM) {
372
2
    return 0;
373
  }
374
375
6
  if (s.getKind() == kind::CONST_BITVECTOR &&
376
      t.getKind() == kind::CONST_BITVECTOR) {
377
    if (s == t) {
378
      return 0;
379
    } else {
380
      return -1;
381
    }
382
  }
383
384
6
  if (s.getKind() == kind::SKOLEM &&
385
      t.getKind() == kind::CONST_BITVECTOR) {
386
    return 1;
387
  }
388
389
6
  if (s.getKind() == kind::CONST_BITVECTOR &&
390
      t.getKind() == kind::SKOLEM) {
391
    return 2;
392
  }
393
394
12
  if (s.getNumChildren() != t.getNumChildren() ||
395
6
      s.getKind() != t.getKind())
396
2
    return -1;
397
398
4
  int unify = 0;
399
6
  for (unsigned i = 0; i < s.getNumChildren(); ++i) {
400
6
    int unify_i = comparePatterns(s[i], t[i]);
401
6
    if (unify_i < 0)
402
4
      return -1;
403
2
    if (unify == 0) {
404
2
      unify = unify_i;
405
    } else if (unify != unify_i && unify_i != 0) {
406
      return -1;
407
    }
408
  }
409
  return unify;
410
}
411
412
16
TNode AbstractionModule::getGeneralization(TNode term) {
413
16
  NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
414
  // if not in the map we add it
415
16
  if (it == d_sigToGeneralization.end()) {
416
4
    d_sigToGeneralization[term] = term;
417
4
    return term;
418
  }
419
  // doesn't have a generalization
420
12
  if (it->second == term)
421
12
    return term;
422
423
  TNode generalization = getGeneralization(it->second);
424
  Assert(generalization != term);
425
  d_sigToGeneralization[term] = generalization;
426
  return generalization;
427
}
428
429
void AbstractionModule::storeGeneralization(TNode s, TNode t) {
430
  Assert(s == getGeneralization(s));
431
  Assert(t == getGeneralization(t));
432
  d_sigToGeneralization[s] = t;
433
}
434
435
3
void AbstractionModule::finalizeSignatures()
436
{
437
3
  NodeManager* nm = NodeManager::currentNM();
438
6
  Debug("bv-abstraction")
439
3
      << "AbstractionModule::finalizeSignatures num signatures = "
440
3
      << d_signatures.size() << "\n";
441
6
  TNodeSet new_signatures;
442
443
  // "unify" signatures
444
7
  for (SignatureMap::const_iterator ss = d_signatures.begin();
445
7
       ss != d_signatures.end();
446
       ++ss)
447
  {
448
10
    for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt)
449
    {
450
10
      TNode t = getGeneralization(tt->first);
451
10
      TNode s = getGeneralization(ss->first);
452
453
6
      if (t != s)
454
      {
455
2
        int status = comparePatterns(s, t);
456
2
        Assert(status);
457
2
        if (status < 0) continue;
458
        if (status == 1)
459
        {
460
          storeGeneralization(t, s);
461
        }
462
        else
463
        {
464
          storeGeneralization(s, t);
465
        }
466
      }
467
    }
468
  }
469
  // keep only most general signatures
470
7
  for (SignatureMap::iterator it = d_signatures.begin();
471
7
       it != d_signatures.end();)
472
  {
473
8
    TNode sig = it->first;
474
8
    TNode gen = getGeneralization(sig);
475
4
    if (sig != gen)
476
    {
477
      Assert(d_signatures.find(gen) != d_signatures.end());
478
      // update the count
479
      d_signatures[gen] += d_signatures[sig];
480
      d_signatures.erase(it++);
481
    }
482
    else
483
    {
484
4
      ++it;
485
    }
486
  }
487
488
  // remove signatures that are not frequent enough
489
7
  for (SignatureMap::iterator it = d_signatures.begin();
490
7
       it != d_signatures.end();)
491
  {
492
4
    if (it->second <= 7)
493
    {
494
4
      d_signatures.erase(it++);
495
    }
496
    else
497
    {
498
      ++it;
499
    }
500
  }
501
502
3
  for (SignatureMap::const_iterator it = d_signatures.begin();
503
3
       it != d_signatures.end();
504
       ++it)
505
  {
506
    TNode signature = it->first;
507
    // we already processed this signature
508
    Assert(d_signatureToFunc.find(signature) == d_signatureToFunc.end());
509
510
    Debug("bv-abstraction") << "Processing signature " << signature << " count "
511
                            << it->second << "\n";
512
    std::vector<TypeNode> arg_types;
513
    TNodeSet seen;
514
    collectArgumentTypes(signature, arg_types, seen);
515
    Assert(signature.getType().isBoolean());
516
    // make function return a bitvector of size 1
517
    // Node bv_function = nm->mkNode(kind::ITE, signature, utils::mkConst(1,
518
    // 1u), utils::mkConst(1, 0u));
519
    TypeNode range = nm->mkBitVectorType(1);
520
521
    TypeNode abs_type = nm->mkFunctionType(arg_types, range);
522
    Node abs_func =
523
        nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
524
    Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
525
526
    // NOTE: signature expression type is BOOLEAN
527
    d_signatureToFunc[signature] = abs_func;
528
    d_funcToSignature[abs_func] = signature;
529
  }
530
531
3
  d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
532
533
6
  Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
534
3
                          << d_signatureToFunc.size() << " signatures. \n";
535
3
}
536
537
void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) {
538
  if (seen.find(sig) != seen.end())
539
    return;
540
541
  if (sig.getKind() == kind::SKOLEM) {
542
    types.push_back(sig.getType());
543
    seen.insert(sig);
544
    return;
545
  }
546
547
  for (unsigned i = 0; i < sig.getNumChildren(); ++i) {
548
    collectArgumentTypes(sig[i], types, seen);
549
    seen.insert(sig);
550
  }
551
}
552
553
void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) {
554
  if (seen.find(node)!= seen.end())
555
    return;
556
557
  if (node.getMetaKind() == kind::metakind::VARIABLE
558
      || node.getKind() == kind::CONST_BITVECTOR)
559
  {
560
    // a constant in the node can either map to an argument of the abstraction
561
    // or can be hard-coded and part of the abstraction
562
    if (signature.getKind() == kind::SKOLEM) {
563
      args.push_back(node);
564
      seen.insert(node);
565
    } else {
566
      Assert(signature.getKind() == kind::CONST_BITVECTOR);
567
    }
568
    //
569
    return;
570
  }
571
  Assert(node.getKind() == signature.getKind()
572
         && node.getNumChildren() == signature.getNumChildren());
573
574
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
575
    collectArguments(node[i], signature[i], args, seen);
576
    seen.insert(node);
577
  }
578
}
579
580
Node AbstractionModule::abstractSignatures(TNode assertion)
581
{
582
  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "
583
                          << assertion << "\n";
584
  NodeManager* nm = NodeManager::currentNM();
585
  // assume the assertion has been fully abstracted
586
  Node signature = getGeneralizedSignature(assertion);
587
588
  Debug("bv-abstraction") << "   with sig " << signature << "\n";
589
  NodeNodeMap::iterator it = d_signatureToFunc.find(signature);
590
  if (it != d_signatureToFunc.end())
591
  {
592
    std::vector<Node> args;
593
    TNode func = it->second;
594
    // pushing the function symbol
595
    args.push_back(func);
596
    TNodeSet seen;
597
    collectArguments(assertion, signature, args, seen);
598
    std::vector<TNode> real_args;
599
    for (unsigned i = 1; i < args.size(); ++i)
600
    {
601
      real_args.push_back(args[i]);
602
    }
603
    d_argsTable.addEntry(func, real_args);
604
    Node result = nm->mkNode(
605
        kind::EQUAL,
606
        nm->mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u));
607
    Debug("bv-abstraction") << "=>   " << result << "\n";
608
    Assert(result.getType() == assertion.getType());
609
    return result;
610
  }
611
  return assertion;
612
}
613
614
12
bool AbstractionModule::isAbstraction(TNode node) {
615
12
  if (node.getKind() != kind::EQUAL)
616
    return false;
617
36
  if ((node[0].getKind() != kind::CONST_BITVECTOR ||
618
84
       node[1].getKind() != kind::APPLY_UF) &&
619
36
      (node[1].getKind() != kind::CONST_BITVECTOR ||
620
12
       node[0].getKind() != kind::APPLY_UF))
621
12
    return false;
622
623
  TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1];
624
  TNode func = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1];
625
  Assert(constant.getKind() == kind::CONST_BITVECTOR
626
         && func.getKind() == kind::APPLY_UF);
627
  if (utils::getSize(constant) != 1)
628
    return false;
629
  if (constant != utils::mkConst(1, 1u))
630
    return false;
631
632
  TNode func_symbol = func.getOperator();
633
  if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end())
634
    return false;
635
636
  return true;
637
}
638
639
Node AbstractionModule::getInterpretation(TNode node) {
640
  Assert(isAbstraction(node));
641
  TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1];
642
  TNode apply = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1];
643
  Assert(constant.getKind() == kind::CONST_BITVECTOR
644
         && apply.getKind() == kind::APPLY_UF);
645
646
  Node func = apply.getOperator();
647
  Assert(d_funcToSignature.find(func) != d_funcToSignature.end());
648
649
  Node sig = d_funcToSignature[func];
650
651
  // substitute arguments in signature
652
  TNodeTNodeMap seen;
653
  unsigned index = 0;
654
  Node result = substituteArguments(sig, apply, index, seen);
655
  Assert(result.getType().isBoolean());
656
  Assert(index == apply.getNumChildren());
657
  // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
658
  // Debug("bv-abstraction") << "    => " << result << "\n";
659
  return result;
660
}
661
662
Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
663
  if (seen.find(signature) != seen.end()) {
664
    return seen[signature];
665
  }
666
667
  if (signature.getKind() == kind::SKOLEM) {
668
    // return corresponding argument and increment counter
669
    seen[signature] = apply[index];
670
    return apply[index++];
671
  }
672
673
  if (signature.getNumChildren() == 0) {
674
    Assert(signature.getMetaKind() != kind::metakind::VARIABLE);
675
    seen[signature] = signature;
676
    return signature;
677
  }
678
679
  NodeBuilder<> builder(signature.getKind());
680
  if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
681
    builder << signature.getOperator();
682
  }
683
684
  for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
685
    Node child = substituteArguments(signature[i], apply, index, seen);
686
    builder << child;
687
  }
688
689
  Node result = builder;
690
  seen[signature]= result;
691
692
  return result;
693
}
694
695
Node AbstractionModule::simplifyConflict(TNode conflict) {
696
  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
697
  if (conflict.getKind() != kind::AND)
698
    return conflict;
699
700
  std::vector<Node> conjuncts;
701
  for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
702
    conjuncts.push_back(conflict[i]);
703
704
  theory::SubstitutionMap subst(new context::Context());
705
  for (unsigned i = 0; i < conjuncts.size(); ++i) {
706
    TNode conjunct = conjuncts[i];
707
    // substitute s -> t
708
    Node s, t;
709
710
    if (conjunct.getKind() == kind::EQUAL) {
711
      if (conjunct[0].getMetaKind() == kind::metakind::VARIABLE &&
712
          conjunct[1].getKind() == kind::CONST_BITVECTOR) {
713
        s = conjunct[0];
714
        t = conjunct[1];
715
      }
716
      else if (conjunct[1].getMetaKind() == kind::metakind::VARIABLE &&
717
               conjunct[0].getKind() == kind::CONST_BITVECTOR) {
718
        s = conjunct[1];
719
        t = conjunct[0];
720
      } else {
721
        continue;
722
      }
723
724
      Assert(!subst.hasSubstitution(s));
725
      Assert(!t.isNull() && !s.isNull() && s != t);
726
      subst.addSubstitution(s, t);
727
728
      for (unsigned k = 0; k < conjuncts.size(); k++) {
729
        conjuncts[k] = subst.apply(conjuncts[k]);
730
      }
731
    }
732
  }
733
  Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts));
734
735
  Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
736
  Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
737
738
  return new_conflict;
739
}
740
741
void DebugPrintInstantiations(
742
    const std::vector<std::vector<ArgsVec> >& instantiations,
743
    const std::vector<TNode>& functions)
744
{
745
  // print header
746
  Debug("bv-abstraction-dbg") <<"[ ";
747
  for (unsigned i = 0; i < functions.size(); ++i) {
748
    for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) {
749
      Debug("bv-abstraction-dgb") << functions[i][j] <<" ";
750
    }
751
    Debug("bv-abstraction-dgb") << " || ";
752
  }
753
  Debug("bv-abstraction-dbg") <<"]\n";
754
755
  for (unsigned i = 0; i < instantiations.size(); ++i) {
756
    Debug("bv-abstraction-dbg") <<"[";
757
    const std::vector<ArgsVec>& inst = instantiations[i];
758
    for (unsigned j = 0; j < inst.size(); ++j) {
759
      for (unsigned k = 0; k < inst[j].size(); ++k) {
760
        Debug("bv-abstraction-dbg") << inst[j][k] << " ";
761
      }
762
      Debug("bv-abstraction-dbg") << " || ";
763
    }
764
    Debug("bv-abstraction-dbg") <<"]\n";
765
  }
766
}
767
768
void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) {
769
  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
770
  std::vector<TNode> functions;
771
772
  // collect abstract functions
773
  if (conflict.getKind() != kind::AND) {
774
    if (isAbstraction(conflict)) {
775
      Assert(conflict[0].getKind() == kind::APPLY_UF);
776
      functions.push_back(conflict[0]);
777
    }
778
  } else {
779
    for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
780
      TNode conjunct = conflict[i];
781
      if (isAbstraction(conjunct)) {
782
        Assert(conjunct[0].getKind() == kind::APPLY_UF);
783
        functions.push_back(conjunct[0]);
784
      }
785
    }
786
  }
787
788
  // if (functions.size() >= 3) {
789
  //   // dump conflict
790
  //   NodeNodeMap seen;
791
  //   Node reversed = reverseAbstraction(conflict, seen);
792
  //   std::cout << "CONFLICT " << reversed << "\n";
793
  // }
794
795
796
  if (functions.size() == 0 || functions.size() > options::bvNumFunc()) {
797
    return;
798
  }
799
800
801
  // Skolemize function arguments to avoid confusion in pattern matching
802
  SubstitutionMap skolem_subst(new context::Context());
803
  SubstitutionMap reverse_skolem(new context::Context());
804
  makeFreshSkolems(conflict, skolem_subst, reverse_skolem);
805
806
  Node skolemized_conflict = skolem_subst.apply(conflict);
807
  for (unsigned i = 0; i < functions.size(); ++i) {
808
    functions[i] = skolem_subst.apply(functions[i]);
809
  }
810
811
  conflict = skolem_subst.apply(conflict);
812
813
  LemmaInstantiatior inst(functions, d_argsTable, conflict);
814
  std::vector<Node> new_lemmas;
815
  inst.generateInstantiations(new_lemmas);
816
  for (unsigned i = 0; i < new_lemmas.size(); ++i) {
817
    TNode lemma = reverse_skolem.apply(new_lemmas[i]);
818
    if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) {
819
      lemmas.push_back(lemma);
820
      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
821
      storeLemma(lemma);
822
    }
823
  }
824
}
825
826
int AbstractionModule::LemmaInstantiatior::next(int val, int index) {
827
  if (val < d_maxMatch[index]  - 1)
828
    return val + 1;
829
  return -1;
830
}
831
832
/**
833
 * Assumes the stack without top is consistent, and checks that the
834
 * full stack is consistent
835
 *
836
 * @param stack
837
 *
838
 * @return
839
 */
840
bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) {
841
  if (stack.empty())
842
    return true;
843
844
  unsigned current = stack.size() - 1;
845
  TNode func = d_functions[current];
846
  ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
847
  ArgsVec& args = matches.getEntry(stack[current]);
848
  Assert(args.size() == func.getNumChildren());
849
  for (unsigned k = 0; k < args.size(); ++k) {
850
    TNode s = func[k];
851
    TNode t = args[k];
852
853
    TNode s0 = s;
854
    while (d_subst.hasSubstitution(s0)) {
855
      s0 = d_subst.getSubstitution(s0);
856
    }
857
858
    TNode t0 = t;
859
    while (d_subst.hasSubstitution(t0)) {
860
      t0 = d_subst.getSubstitution(t0);
861
    }
862
863
    if (s0.isConst() && t0.isConst()) {
864
      if (s0 != t0)
865
        return false; // fail
866
      else
867
        continue;
868
    }
869
870
    if(s0.getMetaKind() == kind::metakind::VARIABLE &&
871
       t0.isConst()) {
872
      d_subst.addSubstitution(s0, t0);
873
      continue;
874
    }
875
876
    if (s0.isConst() &&
877
        t0.getMetaKind() == kind::metakind::VARIABLE) {
878
      d_subst.addSubstitution(t0, s0);
879
      continue;
880
    }
881
882
    Assert(s0.getMetaKind() == kind::metakind::VARIABLE
883
           && t0.getMetaKind() == kind::metakind::VARIABLE);
884
885
    if (s0 != t0) {
886
      d_subst.addSubstitution(s0, t0);
887
    }
888
  }
889
  return true;
890
}
891
892
bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
893
  return stack.size() == d_functions.size();
894
}
895
896
void AbstractionModule::LemmaInstantiatior::mkLemma() {
897
  Node lemma = d_subst.apply(d_conflict);
898
  // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n";
899
  d_lemmas.push_back(lemma);
900
}
901
902
void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
903
  if (!isConsistent(stack))
904
    return;
905
906
  if (accept(stack)) {
907
    mkLemma();
908
    return;
909
  }
910
911
  int x = 0;
912
  while (x != -1) {
913
    d_ctx->push();
914
    stack.push_back(x);
915
    backtrack(stack);
916
917
    d_ctx->pop();
918
    stack.pop_back();
919
    x = next(x, stack.size());
920
  }
921
}
922
923
924
void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) {
925
  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
926
927
  std::vector<int> stack;
928
  backtrack(stack);
929
  Assert(d_ctx->getLevel() == 0);
930
  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
931
  lemmas.swap(d_lemmas);
932
}
933
934
void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) {
935
  if (map.hasSubstitution(node)) {
936
    return;
937
  }
938
  if (node.getMetaKind() == kind::metakind::VARIABLE) {
939
    Node skolem = utils::mkVar(utils::getSize(node));
940
    map.addSubstitution(node, skolem);
941
    reverse_map.addSubstitution(skolem, node);
942
    return;
943
  }
944
  if (node.isConst())
945
    return;
946
947
  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
948
    makeFreshSkolems(node[i], map, reverse_map);
949
  }
950
}
951
952
void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
953
  Assert(fresh_args.size() == 0);
954
  Assert(func.getKind() == kind::APPLY_UF);
955
  TNodeNodeMap d_map;
956
  for (unsigned i = 0; i < func.getNumChildren(); ++i) {
957
    TNode arg = func[i];
958
    if (arg.isConst()) {
959
      fresh_args.push_back(arg);
960
      continue;
961
    }
962
    Assert(arg.getMetaKind() == kind::metakind::VARIABLE);
963
    TNodeNodeMap::iterator it = d_map.find(arg);
964
    if (it != d_map.end()) {
965
      fresh_args.push_back(it->second);
966
    } else {
967
      Node skolem = utils::mkVar(utils::getSize(arg));
968
      d_map[arg] = skolem;
969
      fresh_args.push_back(skolem);
970
    }
971
  }
972
  Assert(fresh_args.size() == func.getNumChildren());
973
}
974
975
Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict) {
976
  Assert(ss.size() == tt.size());
977
978
  Debug("bv-abstraction-dbg") << "AbstractionModule::tryMatching conflict = " << conflict << "\n";
979
  if (Debug.isOn("bv-abstraction-dbg")) {
980
    Debug("bv-abstraction-dbg") << "  Match: ";
981
    for (unsigned i = 0; i < ss.size(); ++i) {
982
      Debug("bv-abstraction-dbg") << ss[i] <<" ";
983
984
    }
985
    Debug("bv-abstraction-dbg") << "\n  To: ";
986
    for (unsigned i = 0; i < tt.size(); ++i) {
987
      Debug("bv-abstraction-dbg") << tt[i] <<" ";
988
    }
989
    Debug("bv-abstraction-dbg") <<"\n";
990
  }
991
992
993
  SubstitutionMap subst(new context::Context());
994
995
  for (unsigned i = 0; i < ss.size(); ++i) {
996
    TNode s = ss[i];
997
    TNode t = tt[i];
998
999
    TNode s0 = subst.hasSubstitution(s) ? subst.getSubstitution(s) : s;
1000
    TNode t0 = subst.hasSubstitution(t) ? subst.getSubstitution(t) : t;
1001
1002
    if (s0.isConst() && t0.isConst()) {
1003
      if (s0 != t0)
1004
        return Node(); // fail
1005
      else
1006
        continue;
1007
    }
1008
1009
    if(s0.getMetaKind() == kind::metakind::VARIABLE &&
1010
       t0.isConst()) {
1011
      subst.addSubstitution(s0, t0);
1012
      continue;
1013
    }
1014
1015
    if (s0.isConst() &&
1016
        t0.getMetaKind() == kind::metakind::VARIABLE) {
1017
      subst.addSubstitution(t0, s0);
1018
      continue;
1019
    }
1020
1021
    Assert(s0.getMetaKind() == kind::metakind::VARIABLE
1022
           && t0.getMetaKind() == kind::metakind::VARIABLE);
1023
1024
    Assert(s0 != t0);
1025
    subst.addSubstitution(s0, t0);
1026
  }
1027
1028
  Node res = subst.apply(conflict);
1029
  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n";
1030
  return res;
1031
}
1032
1033
void AbstractionModule::storeLemma(TNode lemma) {
1034
  d_addedLemmas.insert(lemma);
1035
  if (lemma.getKind() == kind::AND) {
1036
    for (unsigned i = 0; i < lemma.getNumChildren(); i++) {
1037
      TNode atom = lemma[i];
1038
      atom = atom.getKind() == kind::NOT ? atom[0] : atom;
1039
      Assert(atom.getKind() != kind::NOT);
1040
      Assert(utils::isBVPredicate(atom));
1041
      d_lemmaAtoms.insert(atom);
1042
    }
1043
  } else {
1044
    lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
1045
    Assert(utils::isBVPredicate(lemma));
1046
    d_lemmaAtoms.insert(lemma);
1047
  }
1048
}
1049
1050
1051
16
bool AbstractionModule::isLemmaAtom(TNode node) const {
1052
16
  Assert(node.getType().isBoolean());
1053
16
  node = node.getKind() == kind::NOT? node[0] : node;
1054
1055
32
  return d_inputAtoms.find(node) == d_inputAtoms.end() &&
1056
32
    d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
1057
}
1058
1059
12
void AbstractionModule::addInputAtom(TNode atom) {
1060
12
  if (options::bitblastMode() == options::BitblastMode::LAZY)
1061
  {
1062
12
    d_inputAtoms.insert(atom);
1063
  }
1064
12
}
1065
1066
void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
1067
  Assert(args.size() == d_arity);
1068
  d_data.push_back(args);
1069
}
1070
1071
void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) {
1072
  if (d_data.find(signature) == d_data.end()) {
1073
    d_data[signature] = ArgsTableEntry(args.size());
1074
  }
1075
  ArgsTableEntry& entry = d_data[signature];
1076
  entry.addArguments(args);
1077
}
1078
1079
1080
bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
1081
  return d_data.find(signature) != d_data.end();
1082
}
1083
1084
AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
1085
  Assert(hasEntry(signature));
1086
  return d_data.find(signature)->second;
1087
}
1088
1089
8987
AbstractionModule::Statistics::Statistics(const std::string& name)
1090
17974
    : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
1091
                               0),
1092
17974
      d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
1093
44935
      d_abstractionTime(name + "::abstraction::AbstractionTime")
1094
{
1095
8987
  smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
1096
8987
  smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
1097
8987
  smtStatisticsRegistry()->registerStat(&d_abstractionTime);
1098
8987
}
1099
1100
17968
AbstractionModule::Statistics::~Statistics() {
1101
8984
  smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted);
1102
8984
  smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized);
1103
8984
  smtStatisticsRegistry()->unregisterStat(&d_abstractionTime);
1104
35672
}