GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/ite_simp.cpp Lines: 63 124 50.8 %
Date: 2021-03-23 Branches: 69 458 15.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ite_simp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Andrew Reynolds
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 ITE simplification preprocessing pass.
13
 **/
14
15
#include "preprocessing/passes/ite_simp.h"
16
17
#include <vector>
18
19
#include "options/smt_options.h"
20
#include "preprocessing/assertion_pipeline.h"
21
#include "preprocessing/preprocessing_pass_context.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "smt_util/nary_builder.h"
24
#include "theory/arith/arith_ite_utils.h"
25
#include "theory/rewriter.h"
26
#include "theory/theory_engine.h"
27
28
using namespace std;
29
using namespace CVC4;
30
using namespace CVC4::theory;
31
32
namespace CVC4 {
33
namespace preprocessing {
34
namespace passes {
35
36
/* -------------------------------------------------------------------------- */
37
38
namespace {
39
40
2
Node simpITE(util::ITEUtilities* ite_utils, TNode assertion)
41
{
42
2
  if (!ite_utils->containsTermITE(assertion))
43
  {
44
1
    return assertion;
45
  }
46
  else
47
  {
48
2
    Node result = ite_utils->simpITE(assertion);
49
2
    Node res_rewritten = Rewriter::rewrite(result);
50
51
17996
    if (options::simplifyWithCareEnabled())
52
    {
53
      Chat() << "starting simplifyWithCare()" << endl;
54
      Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
55
      Chat() << "ending simplifyWithCare()"
56
             << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
57
      result = Rewriter::rewrite(postSimpWithCare);
58
    }
59
    else
60
    {
61
1
      result = res_rewritten;
62
    }
63
1
    return result;
64
  }
65
}
66
67
/**
68
 * Ensures the assertions asserted after index 'before' now effectively come
69
 * before 'real_assertions_end'.
70
 */
71
1
void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess,
72
                                  size_t before)
73
{
74
1
  size_t cur_size = assertionsToPreprocess->size();
75
2
  if (before >= cur_size || assertionsToPreprocess->getRealAssertionsEnd() <= 0
76
2
      || assertionsToPreprocess->getRealAssertionsEnd() >= cur_size)
77
  {
78
    return;
79
  }
80
81
  // assertions
82
  // original: [0 ... assertionsToPreprocess.getRealAssertionsEnd())
83
  //  can be modified
84
  // ites skolems [assertionsToPreprocess.getRealAssertionsEnd(), before)
85
  //  cannot be moved
86
  // added [before, cur_size)
87
  //  can be modified
88
1
  Assert(0 < assertionsToPreprocess->getRealAssertionsEnd());
89
1
  Assert(assertionsToPreprocess->getRealAssertionsEnd() <= before);
90
1
  Assert(before < cur_size);
91
92
2
  std::vector<Node> intoConjunction;
93
1210
  for (size_t i = before; i < cur_size; ++i)
94
  {
95
1209
    intoConjunction.push_back((*assertionsToPreprocess)[i]);
96
  }
97
1
  assertionsToPreprocess->resize(before);
98
1
  size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1;
99
1
  intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]);
100
2
  Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
101
1
  assertionsToPreprocess->replace(lastBeforeItes, newLast);
102
1
  Assert(assertionsToPreprocess->size() == before);
103
}
104
105
}  // namespace
106
107
/* -------------------------------------------------------------------------- */
108
109
8997
ITESimp::Statistics::Statistics()
110
    : d_arithSubstitutionsAdded(
111
8997
          "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0)
112
{
113
8997
  smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
114
8997
}
115
116
17988
ITESimp::Statistics::~Statistics()
117
{
118
8994
  smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
119
8994
}
120
121
1
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
122
{
123
1
  Assert(!options::unsatCores());
124
1
  bool result = true;
125
1
  bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
126
1
  if (simpDidALotOfWork)
127
  {
128
4
    if (options::compressItes())
129
    {
130
1
      result = d_iteUtilities.compress(assertionsToPreprocess);
131
    }
132
133
1
    if (result)
134
    {
135
      // if false, don't bother to reclaim memory here.
136
1
      NodeManager* nm = NodeManager::currentNM();
137
2
      if (nm->poolSize() >= options::zombieHuntThreshold())
138
      {
139
        Chat() << "..ite simplifier did quite a bit of work.. "
140
               << nm->poolSize() << endl;
141
        Chat() << "....node manager contains " << nm->poolSize()
142
               << " nodes before cleanup" << endl;
143
        d_iteUtilities.clear();
144
        Rewriter::clearCaches();
145
        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
146
        Chat() << "....node manager contains " << nm->poolSize()
147
               << " nodes after cleanup" << endl;
148
      }
149
    }
150
  }
151
152
  // Do theory specific preprocessing passes
153
1
  TheoryEngine* theory_engine = d_preprocContext->getTheoryEngine();
154
2
  if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH)
155
1
      && !options::incrementalSolving())
156
  {
157
1
    if (!simpDidALotOfWork)
158
    {
159
      util::ContainsTermITEVisitor& contains =
160
          *(d_iteUtilities.getContainsVisitor());
161
      arith::ArithIteUtils aiteu(contains,
162
                                 d_preprocContext->getUserContext(),
163
                                 theory_engine->getModel());
164
      bool anyItes = false;
165
      for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
166
      {
167
        Node curr = (*assertionsToPreprocess)[i];
168
        if (contains.containsTermITE(curr))
169
        {
170
          anyItes = true;
171
          Node res = aiteu.reduceVariablesInItes(curr);
172
          Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl
173
                                   << "   ->" << res << endl;
174
          if (curr != res)
175
          {
176
            Node more = aiteu.reduceConstantIteByGCD(res);
177
            Debug("arith::ite::red") << "  gcd->" << more << endl;
178
            Node morer = Rewriter::rewrite(more);
179
            assertionsToPreprocess->replace(i, morer);
180
          }
181
        }
182
      }
183
      if (!anyItes)
184
      {
185
        unsigned prevSubCount = aiteu.getSubCount();
186
        aiteu.learnSubstitutions(assertionsToPreprocess->ref());
187
        if (prevSubCount < aiteu.getSubCount())
188
        {
189
          d_statistics.d_arithSubstitutionsAdded +=
190
              aiteu.getSubCount() - prevSubCount;
191
          bool anySuccess = false;
192
          for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
193
          {
194
            Node curr = (*assertionsToPreprocess)[i];
195
            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
196
            Node res = aiteu.reduceVariablesInItes(next);
197
            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
198
                                     << "   ->" << res << endl;
199
            Node more = aiteu.reduceConstantIteByGCD(res);
200
            Debug("arith::ite::red") << "  gcd->" << more << endl;
201
            if (more != next)
202
            {
203
              anySuccess = true;
204
              break;
205
            }
206
          }
207
          for (size_t i = 0, N = assertionsToPreprocess->size();
208
               anySuccess && i < N;
209
               ++i)
210
          {
211
            Node curr = (*assertionsToPreprocess)[i];
212
            Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
213
            Node res = aiteu.reduceVariablesInItes(next);
214
            Debug("arith::ite::red") << "@ " << i << " ... " << next << endl
215
                                     << "   ->" << res << endl;
216
            Node more = aiteu.reduceConstantIteByGCD(res);
217
            Debug("arith::ite::red") << "  gcd->" << more << endl;
218
            Node morer = Rewriter::rewrite(more);
219
            assertionsToPreprocess->replace(i, morer);
220
          }
221
        }
222
      }
223
    }
224
  }
225
1
  return result;
226
}
227
228
/* -------------------------------------------------------------------------- */
229
230
8997
ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
231
8997
    : PreprocessingPass(preprocContext, "ite-simp")
232
{
233
8997
}
234
235
1
PreprocessingPassResult ITESimp::applyInternal(
236
    AssertionPipeline* assertionsToPreprocess)
237
{
238
1
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
239
240
1
  size_t nasserts = assertionsToPreprocess->size();
241
3
  for (size_t i = 0; i < nasserts; ++i)
242
  {
243
2
    d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
244
4
    Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]);
245
2
    assertionsToPreprocess->replace(i, simp);
246
2
    if (simp.isConst() && !simp.getConst<bool>())
247
    {
248
      return PreprocessingPassResult::CONFLICT;
249
    }
250
  }
251
1
  bool done = doneSimpITE(assertionsToPreprocess);
252
1
  if (nasserts < assertionsToPreprocess->size())
253
  {
254
1
    compressBeforeRealAssertions(assertionsToPreprocess, nasserts);
255
  }
256
1
  return done ? PreprocessingPassResult::NO_CONFLICT
257
1
              : PreprocessingPassResult::CONFLICT;
258
}
259
260
261
/* -------------------------------------------------------------------------- */
262
263
}  // namespace passes
264
}  // namespace preprocessing
265
44680
}  // namespace CVC4