GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/miplib_trick.cpp Lines: 45 367 12.3 %
Date: 2021-03-23 Branches: 51 1882 2.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file miplib_trick.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Andrew Reynolds, Morgan Deters
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 The MIPLIB trick preprocessing pass
13
 **
14
 **/
15
16
#include "preprocessing/passes/miplib_trick.h"
17
18
#include <sstream>
19
#include <vector>
20
21
#include "expr/node_self_iterator.h"
22
#include "options/arith_options.h"
23
#include "options/smt_options.h"
24
#include "preprocessing/assertion_pipeline.h"
25
#include "preprocessing/preprocessing_pass_context.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "smt_util/boolean_simplification.h"
28
#include "theory/booleans/circuit_propagator.h"
29
#include "theory/theory_engine.h"
30
#include "theory/theory_model.h"
31
#include "theory/trust_substitutions.h"
32
33
namespace CVC4 {
34
namespace preprocessing {
35
namespace passes {
36
37
using namespace std;
38
using namespace CVC4::theory;
39
40
namespace {
41
42
/**
43
 * Remove conjuncts in toRemove from conjunction n. Return # of removed
44
 * conjuncts.
45
 */
46
size_t removeFromConjunction(Node& n,
47
                             const std::unordered_set<unsigned long>& toRemove)
48
{
49
  Assert(n.getKind() == kind::AND);
50
  Node trueNode = NodeManager::currentNM()->mkConst(true);
51
  size_t removals = 0;
52
  for (Node::iterator j = n.begin(); j != n.end(); ++j)
53
  {
54
    size_t subremovals = 0;
55
    Node sub = *j;
56
    if (toRemove.find(sub.getId()) != toRemove.end()
57
        || (sub.getKind() == kind::AND
58
            && (subremovals = removeFromConjunction(sub, toRemove)) > 0))
59
    {
60
      NodeBuilder<> b(kind::AND);
61
      b.append(n.begin(), j);
62
      if (subremovals > 0)
63
      {
64
        removals += subremovals;
65
        b << sub;
66
      }
67
      else
68
      {
69
        ++removals;
70
      }
71
      for (++j; j != n.end(); ++j)
72
      {
73
        if (toRemove.find((*j).getId()) != toRemove.end())
74
        {
75
          ++removals;
76
        }
77
        else if ((*j).getKind() == kind::AND)
78
        {
79
          sub = *j;
80
          if ((subremovals = removeFromConjunction(sub, toRemove)) > 0)
81
          {
82
            removals += subremovals;
83
            b << sub;
84
          }
85
          else
86
          {
87
            b << *j;
88
          }
89
        }
90
        else
91
        {
92
          b << *j;
93
        }
94
      }
95
      if (b.getNumChildren() == 0)
96
      {
97
        n = trueNode;
98
        b.clear();
99
      }
100
      else if (b.getNumChildren() == 1)
101
      {
102
        n = b[0];
103
        b.clear();
104
      }
105
      else
106
      {
107
        n = b;
108
      }
109
      n = Rewriter::rewrite(n);
110
      return removals;
111
    }
112
  }
113
114
  Assert(removals == 0);
115
  return 0;
116
}
117
118
/**
119
 * Trace nodes back to their assertions using CircuitPropagator's
120
 * BackEdgesMap.
121
 */
122
void traceBackToAssertions(booleans::CircuitPropagator* propagator,
123
                           const std::vector<Node>& nodes,
124
                           std::vector<TNode>& assertions)
125
{
126
  const booleans::CircuitPropagator::BackEdgesMap& backEdges =
127
      propagator->getBackEdges();
128
  for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
129
  {
130
    booleans::CircuitPropagator::BackEdgesMap::const_iterator j =
131
        backEdges.find(*i);
132
    // term must appear in map, otherwise how did we get here?!
133
    Assert(j != backEdges.end());
134
    // if term maps to empty, that means it's a top-level assertion
135
    if (!(*j).second.empty())
136
    {
137
      traceBackToAssertions(propagator, (*j).second, assertions);
138
    }
139
    else
140
    {
141
      assertions.push_back(*i);
142
    }
143
  }
144
}
145
146
}  // namespace
147
148
8997
MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
149
8997
    : PreprocessingPass(preprocContext, "miplib-trick")
150
{
151
8997
  if (!options::incrementalSolving())
152
  {
153
7468
    NodeManager::currentNM()->subscribeEvents(this);
154
  }
155
8997
}
156
157
26982
MipLibTrick::~MipLibTrick()
158
{
159
8994
  if (!options::incrementalSolving())
160
  {
161
7465
    NodeManager::currentNM()->unsubscribeEvents(this);
162
  }
163
17988
}
164
165
22521
void MipLibTrick::nmNotifyNewVar(TNode n)
166
{
167
22521
  if (n.getType().isBoolean())
168
  {
169
598
    d_boolVars.push_back(n);
170
  }
171
22521
}
172
173
83374
void MipLibTrick::nmNotifyNewSkolem(TNode n,
174
                                    const std::string& comment,
175
                                    uint32_t flags)
176
{
177
83374
  if (n.getType().isBoolean())
178
  {
179
8020
    d_boolVars.push_back(n);
180
  }
181
83374
}
182
183
8
PreprocessingPassResult MipLibTrick::applyInternal(
184
    AssertionPipeline* assertionsToPreprocess)
185
{
186
8
  Assert(assertionsToPreprocess->getRealAssertionsEnd()
187
         == assertionsToPreprocess->size());
188
8
  Assert(!options::incrementalSolving());
189
8
  Assert(!options::unsatCores());
190
191
16
  context::Context fakeContext;
192
8
  TheoryEngine* te = d_preprocContext->getTheoryEngine();
193
  booleans::CircuitPropagator* propagator =
194
8
      d_preprocContext->getCircuitPropagator();
195
  const booleans::CircuitPropagator::BackEdgesMap& backEdges =
196
8
      propagator->getBackEdges();
197
16
  unordered_set<unsigned long> removeAssertions;
198
199
  theory::TrustSubstitutionMap& tlsm =
200
8
      d_preprocContext->getTopLevelSubstitutions();
201
8
  SubstitutionMap& top_level_substs = tlsm.get();
202
203
8
  NodeManager* nm = NodeManager::currentNM();
204
16
  Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
205
16
  Node trueNode = nm->mkConst(true);
206
207
16
  unordered_map<TNode, Node, TNodeHashFunction> intVars;
208
8
  for (TNode v0 : d_boolVars)
209
  {
210
    if (propagator->isAssigned(v0))
211
    {
212
      Debug("miplib") << "ineligible: " << v0 << " because assigned "
213
                      << propagator->getAssignment(v0) << endl;
214
      continue;
215
    }
216
217
    vector<TNode> assertions;
218
    booleans::CircuitPropagator::BackEdgesMap::const_iterator j0 =
219
        backEdges.find(v0);
220
    // if not in back edges map, the bool var is unconstrained, showing up in no
221
    // assertions. if maps to an empty vector, that means the bool var was
222
    // asserted itself.
223
    if (j0 != backEdges.end())
224
    {
225
      if (!(*j0).second.empty())
226
      {
227
        traceBackToAssertions(propagator, (*j0).second, assertions);
228
      }
229
      else
230
      {
231
        assertions.push_back(v0);
232
      }
233
    }
234
    Debug("miplib") << "for " << v0 << endl;
235
    bool eligible = true;
236
    map<pair<Node, Node>, uint64_t> marks;
237
    map<pair<Node, Node>, vector<Rational> > coef;
238
    map<pair<Node, Node>, vector<Rational> > checks;
239
    map<pair<Node, Node>, vector<TNode> > asserts;
240
    for (vector<TNode>::const_iterator j1 = assertions.begin();
241
         j1 != assertions.end();
242
         ++j1)
243
    {
244
      Debug("miplib") << "  found: " << *j1 << endl;
245
      if ((*j1).getKind() != kind::IMPLIES)
246
      {
247
        eligible = false;
248
        Debug("miplib") << "  -- INELIGIBLE -- (not =>)" << endl;
249
        break;
250
      }
251
      Node conj = BooleanSimplification::simplify((*j1)[0]);
252
      if (conj.getKind() == kind::AND && conj.getNumChildren() > 6)
253
      {
254
        eligible = false;
255
        Debug("miplib") << "  -- INELIGIBLE -- (N-ary /\\ too big)" << endl;
256
        break;
257
      }
258
      if (conj.getKind() != kind::AND && !conj.isVar()
259
          && !(conj.getKind() == kind::NOT && conj[0].isVar()))
260
      {
261
        eligible = false;
262
        Debug("miplib") << "  -- INELIGIBLE -- (not /\\ or literal)" << endl;
263
        break;
264
      }
265
      if ((*j1)[1].getKind() != kind::EQUAL
266
          || !(((*j1)[1][0].isVar()
267
                && (*j1)[1][1].getKind() == kind::CONST_RATIONAL)
268
               || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL
269
                   && (*j1)[1][1].isVar())))
270
      {
271
        eligible = false;
272
        Debug("miplib") << "  -- INELIGIBLE -- (=> (and X X) X)" << endl;
273
        break;
274
      }
275
      if (conj.getKind() == kind::AND)
276
      {
277
        vector<Node> posv;
278
        bool found_x = false;
279
        map<TNode, bool> neg;
280
        for (Node::iterator ii = conj.begin(); ii != conj.end(); ++ii)
281
        {
282
          if ((*ii).isVar())
283
          {
284
            posv.push_back(*ii);
285
            neg[*ii] = false;
286
            found_x = found_x || v0 == *ii;
287
          }
288
          else if ((*ii).getKind() == kind::NOT && (*ii)[0].isVar())
289
          {
290
            posv.push_back((*ii)[0]);
291
            neg[(*ii)[0]] = true;
292
            found_x = found_x || v0 == (*ii)[0];
293
          }
294
          else
295
          {
296
            eligible = false;
297
            Debug("miplib")
298
                << "  -- INELIGIBLE -- (non-var: " << *ii << ")" << endl;
299
            break;
300
          }
301
          if (propagator->isAssigned(posv.back()))
302
          {
303
            eligible = false;
304
            Debug("miplib") << "  -- INELIGIBLE -- (" << posv.back()
305
                            << " asserted)" << endl;
306
            break;
307
          }
308
        }
309
        if (!eligible)
310
        {
311
          break;
312
        }
313
        if (!found_x)
314
        {
315
          eligible = false;
316
          Debug("miplib") << "  --INELIGIBLE -- (couldn't find " << v0
317
                          << " in conjunction)" << endl;
318
          break;
319
        }
320
        sort(posv.begin(), posv.end());
321
        const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv);
322
        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
323
                              ? (*j1)[1][1]
324
                              : (*j1)[1][0];
325
        const pair<Node, Node> pos_var(pos, var);
326
        const Rational& constant =
327
            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
328
                ? (*j1)[1][0].getConst<Rational>()
329
                : (*j1)[1][1].getConst<Rational>();
330
        uint64_t mark = 0;
331
        unsigned countneg = 0, thepos = 0;
332
        for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii)
333
        {
334
          if (neg[pos[ii]])
335
          {
336
            ++countneg;
337
          }
338
          else
339
          {
340
            thepos = ii;
341
            mark |= (0x1 << ii);
342
          }
343
        }
344
        if ((marks[pos_var] & (1lu << mark)) != 0)
345
        {
346
          eligible = false;
347
          Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
348
          break;
349
        }
350
        Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark)
351
                        << endl;
352
        marks[pos_var] |= (1lu << mark);
353
        Debug("miplib") << "marks[" << pos << "," << var << "] now "
354
                        << marks[pos_var] << endl;
355
        if (countneg == pos.getNumChildren())
356
        {
357
          if (constant != 0)
358
          {
359
            eligible = false;
360
            Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
361
            break;
362
          }
363
        }
364
        else if (countneg == pos.getNumChildren() - 1)
365
        {
366
          Assert(coef[pos_var].size() <= 6 && thepos < 6);
367
          if (coef[pos_var].size() <= thepos)
368
          {
369
            coef[pos_var].resize(thepos + 1);
370
          }
371
          coef[pos_var][thepos] = constant;
372
        }
373
        else
374
        {
375
          if (checks[pos_var].size() <= mark)
376
          {
377
            checks[pos_var].resize(mark + 1);
378
          }
379
          checks[pos_var][mark] = constant;
380
        }
381
        asserts[pos_var].push_back(*j1);
382
      }
383
      else
384
      {
385
        TNode x = conj;
386
        if (x != v0 && x != (v0).notNode())
387
        {
388
          eligible = false;
389
          Debug("miplib")
390
              << "  -- INELIGIBLE -- (x not present where I expect it)" << endl;
391
          break;
392
        }
393
        const bool xneg = (x.getKind() == kind::NOT);
394
        x = xneg ? x[0] : x;
395
        Debug("miplib") << "  x:" << x << "  " << xneg << endl;
396
        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
397
                              ? (*j1)[1][1]
398
                              : (*j1)[1][0];
399
        const pair<Node, Node> x_var(x, var);
400
        const Rational& constant =
401
            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
402
                ? (*j1)[1][0].getConst<Rational>()
403
                : (*j1)[1][1].getConst<Rational>();
404
        unsigned mark = (xneg ? 0 : 1);
405
        if ((marks[x_var] & (1u << mark)) != 0)
406
        {
407
          eligible = false;
408
          Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
409
          break;
410
        }
411
        marks[x_var] |= (1u << mark);
412
        if (xneg)
413
        {
414
          if (constant != 0)
415
          {
416
            eligible = false;
417
            Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
418
            break;
419
          }
420
        }
421
        else
422
        {
423
          Assert(coef[x_var].size() <= 6);
424
          coef[x_var].resize(6);
425
          coef[x_var][0] = constant;
426
        }
427
        asserts[x_var].push_back(*j1);
428
      }
429
    }
430
    if (eligible)
431
    {
432
      for (map<pair<Node, Node>, uint64_t>::const_iterator j = marks.begin();
433
           j != marks.end();
434
           ++j)
435
      {
436
        const TNode pos = (*j).first.first;
437
        const TNode var = (*j).first.second;
438
        const pair<Node, Node>& pos_var = (*j).first;
439
        const uint64_t mark = (*j).second;
440
        const unsigned numVars =
441
            pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
442
        uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
443
        expected = (expected == 0) ? -1 : expected;  // fix for overflow
444
        Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect "
445
                        << expected << dec << endl;
446
        Assert(pos.getKind() == kind::AND || pos.isVar());
447
        if (mark != expected)
448
        {
449
          Debug("miplib") << "  -- INELIGIBLE " << pos
450
                          << " -- (insufficiently marked, got " << mark
451
                          << " for " << numVars << " vars, expected "
452
                          << expected << endl;
453
        }
454
        else
455
        {
456
          if (mark != 3)
457
          {  // exclude single-var case; nothing to check there
458
            uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
459
            sz = (sz == 0) ? -1 : sz;  // fix for overflow
460
            Assert(sz == mark) << "expected size " << sz << " == mark " << mark;
461
            for (size_t k = 0; k < checks[pos_var].size(); ++k)
462
            {
463
              if ((k & (k - 1)) != 0)
464
              {
465
                Rational sum = 0;
466
                Debug("miplib") << k << " => " << checks[pos_var][k] << endl;
467
                for (size_t v1 = 1, kk = k; kk != 0; ++v1, kk >>= 1)
468
                {
469
                  if ((kk & 0x1) == 1)
470
                  {
471
                    Assert(pos.getKind() == kind::AND);
472
                    Debug("miplib")
473
                        << "var " << v1 << " : " << pos[v1 - 1]
474
                        << " coef:" << coef[pos_var][v1 - 1] << endl;
475
                    sum += coef[pos_var][v1 - 1];
476
                  }
477
                }
478
                Debug("miplib") << "checkSum is " << sum << " input says "
479
                                << checks[pos_var][k] << endl;
480
                if (sum != checks[pos_var][k])
481
                {
482
                  eligible = false;
483
                  Debug("miplib") << "  -- INELIGIBLE " << pos
484
                                  << " -- (nonlinear combination)" << endl;
485
                  break;
486
                }
487
              }
488
              else
489
              {
490
                Assert(checks[pos_var][k] == 0)
491
                    << "checks[(" << pos << "," << var << ")][" << k
492
                    << "] should be 0, but it's "
493
                    << checks[pos_var]
494
                             [k];  // we never set for single-positive-var
495
              }
496
            }
497
          }
498
          if (!eligible)
499
          {
500
            eligible = true;  // next is still eligible
501
            continue;
502
          }
503
504
          Debug("miplib") << "  -- ELIGIBLE " << v0 << " , " << pos << " --"
505
                          << endl;
506
          vector<Node> newVars;
507
          expr::NodeSelfIterator ii, iiend;
508
          if (pos.getKind() == kind::AND)
509
          {
510
            ii = pos.begin();
511
            iiend = pos.end();
512
          }
513
          else
514
          {
515
            ii = expr::NodeSelfIterator::self(pos);
516
            iiend = expr::NodeSelfIterator::selfEnd(pos);
517
          }
518
          for (; ii != iiend; ++ii)
519
          {
520
            Node& varRef = intVars[*ii];
521
            if (varRef.isNull())
522
            {
523
              stringstream ss;
524
              ss << "mipvar_" << *ii;
525
              Node newVar = nm->mkSkolem(
526
                  ss.str(),
527
                  nm->integerType(),
528
                  "a variable introduced due to scrubbing a miplib encoding",
529
                  NodeManager::SKOLEM_EXACT_NAME);
530
              Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
531
              Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
532
              TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
533
              TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr);
534
535
              Node n = Rewriter::rewrite(geq.andNode(leq));
536
              assertionsToPreprocess->push_back(n);
537
              TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
538
              CVC4_UNUSED SubstitutionMap& nullMap = tnullMap.get();
539
              Theory::PPAssertStatus status CVC4_UNUSED;  // just for assertions
540
              status = te->solve(tgeq, tnullMap);
541
              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
542
                  << "unexpected solution from arith's ppAssert()";
543
              Assert(nullMap.empty())
544
                  << "unexpected substitution from arith's ppAssert()";
545
              status = te->solve(tleq, tnullMap);
546
              Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED)
547
                  << "unexpected solution from arith's ppAssert()";
548
              Assert(nullMap.empty())
549
                  << "unexpected substitution from arith's ppAssert()";
550
              te->getModel()->addSubstitution(*ii, newVar.eqNode(one));
551
              newVars.push_back(newVar);
552
              varRef = newVar;
553
            }
554
            else
555
            {
556
              newVars.push_back(varRef);
557
            }
558
          }
559
          Node sum;
560
          if (pos.getKind() == kind::AND)
561
          {
562
            NodeBuilder<> sumb(kind::PLUS);
563
            for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
564
            {
565
              sumb << nm->mkNode(
566
                  kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]);
567
            }
568
            sum = sumb;
569
          }
570
          else
571
          {
572
            sum = nm->mkNode(
573
                kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]);
574
          }
575
          Debug("miplib") << "vars[] " << var << endl
576
                          << "    eq " << Rewriter::rewrite(sum) << endl;
577
          Node newAssertion = var.eqNode(Rewriter::rewrite(sum));
578
          if (top_level_substs.hasSubstitution(newAssertion[0]))
579
          {
580
            // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
581
            // Warning() << "REPLACE         " << newAssertion[1] << endl;
582
            // Warning() << "ORIG            " <<
583
            // top_level_substs.getSubstitution(newAssertion[0]) << endl;
584
            Assert(top_level_substs.getSubstitution(newAssertion[0])
585
                   == newAssertion[1]);
586
          }
587
          else if (pos.getNumChildren() <= options::arithMLTrickSubstitutions())
588
          {
589
            top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]);
590
            Debug("miplib") << "addSubs: " << newAssertion[0] << " to "
591
                            << newAssertion[1] << endl;
592
          }
593
          else
594
          {
595
            Debug("miplib")
596
                << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1]
597
                << " (threshold is " << options::arithMLTrickSubstitutions()
598
                << ")" << endl;
599
          }
600
          newAssertion = Rewriter::rewrite(newAssertion);
601
          Debug("miplib") << "  " << newAssertion << endl;
602
603
          assertionsToPreprocess->push_back(newAssertion);
604
          Debug("miplib") << "  assertions to remove: " << endl;
605
          for (vector<TNode>::const_iterator k = asserts[pos_var].begin(),
606
                                             k_end = asserts[pos_var].end();
607
               k != k_end;
608
               ++k)
609
          {
610
            Debug("miplib") << "    " << *k << endl;
611
            removeAssertions.insert((*k).getId());
612
          }
613
        }
614
      }
615
    }
616
  }
617
8
  if (!removeAssertions.empty())
618
  {
619
    Debug("miplib") << " scrubbing miplib encoding..." << endl;
620
    for (size_t i = 0, size = assertionsToPreprocess->getRealAssertionsEnd();
621
         i < size;
622
         ++i)
623
    {
624
      Node assertion = (*assertionsToPreprocess)[i];
625
      if (removeAssertions.find(assertion.getId()) != removeAssertions.end())
626
      {
627
        Debug("miplib") << " - removing " << assertion << endl;
628
        assertionsToPreprocess->replace(i, trueNode);
629
        ++d_statistics.d_numMiplibAssertionsRemoved;
630
      }
631
      else if (assertion.getKind() == kind::AND)
632
      {
633
        size_t removals = removeFromConjunction(assertion, removeAssertions);
634
        if (removals > 0)
635
        {
636
          Debug("miplib") << " - reduced " << assertion << endl;
637
          Debug("miplib") << " -      by " << removals << " conjuncts" << endl;
638
          d_statistics.d_numMiplibAssertionsRemoved += removals;
639
        }
640
      }
641
      Debug("miplib") << "had: " << assertion[i] << endl;
642
      assertionsToPreprocess->replace(
643
          i, Rewriter::rewrite(top_level_substs.apply(assertion)));
644
      Debug("miplib") << "now: " << assertion << endl;
645
    }
646
  }
647
  else
648
  {
649
8
    Debug("miplib") << " miplib pass found nothing." << endl;
650
  }
651
8
  assertionsToPreprocess->updateRealAssertionsEnd();
652
16
  return PreprocessingPassResult::NO_CONFLICT;
653
}
654
655
8997
MipLibTrick::Statistics::Statistics()
656
    : d_numMiplibAssertionsRemoved(
657
8997
          "preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved", 0)
658
{
659
8997
  smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
660
8997
}
661
662
17988
MipLibTrick::Statistics::~Statistics()
663
{
664
8994
  smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
665
8994
}
666
667
668
}  // namespace passes
669
}  // namespace preprocessing
670
26685
}  // namespace CVC4