GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/process_assertions.cpp Lines: 173 186 93.0 %
Date: 2021-03-23 Branches: 381 770 49.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file process_assertions.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Yoni Zohar
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 module for processing assertions for an SMT engine.
13
 **/
14
15
#include "smt/process_assertions.h"
16
17
#include <utility>
18
19
#include "expr/node_manager_attributes.h"
20
#include "options/arith_options.h"
21
#include "options/base_options.h"
22
#include "options/bv_options.h"
23
#include "options/quantifiers_options.h"
24
#include "options/sep_options.h"
25
#include "options/smt_options.h"
26
#include "options/strings_options.h"
27
#include "options/uf_options.h"
28
#include "preprocessing/assertion_pipeline.h"
29
#include "preprocessing/preprocessing_pass.h"
30
#include "preprocessing/preprocessing_pass_registry.h"
31
#include "printer/printer.h"
32
#include "smt/assertions.h"
33
#include "smt/defined_function.h"
34
#include "smt/dump.h"
35
#include "smt/expand_definitions.h"
36
#include "smt/smt_engine.h"
37
#include "smt/smt_engine_stats.h"
38
#include "theory/logic_info.h"
39
#include "theory/theory_engine.h"
40
41
using namespace std;
42
using namespace CVC4::preprocessing;
43
using namespace CVC4::theory;
44
using namespace CVC4::kind;
45
46
namespace CVC4 {
47
namespace smt {
48
49
/** Useful for counting the number of recursive calls. */
50
class ScopeCounter
51
{
52
 public:
53
12033
  ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
54
12033
  ~ScopeCounter() { --d_depth; }
55
56
 private:
57
  unsigned& d_depth;
58
};
59
60
9621
ProcessAssertions::ProcessAssertions(SmtEngine& smt,
61
                                     ExpandDefs& exDefs,
62
                                     ResourceManager& rm,
63
9621
                                     SmtEngineStatistics& stats)
64
    : d_smt(smt),
65
      d_exDefs(exDefs),
66
      d_resourceManager(rm),
67
      d_smtStats(stats),
68
9621
      d_preprocessingPassContext(nullptr)
69
{
70
9621
  d_true = NodeManager::currentNM()->mkConst(true);
71
9621
}
72
73
9600
ProcessAssertions::~ProcessAssertions()
74
{
75
9600
}
76
77
8997
void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
78
{
79
8997
  Assert(d_preprocessingPassContext == nullptr);
80
8997
  d_preprocessingPassContext = pc;
81
82
8997
  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
83
  // TODO: this will likely change when we add support for actually assembling
84
  // preprocessing pipelines. For now, we just create an instance of each
85
  // available preprocessing pass.
86
17994
  std::vector<std::string> passNames = ppReg.getAvailablePasses();
87
314895
  for (const std::string& passName : passNames)
88
  {
89
305898
    d_passes[passName].reset(
90
        ppReg.createPass(d_preprocessingPassContext, passName));
91
  }
92
8997
}
93
94
9600
void ProcessAssertions::cleanup() { d_passes.clear(); }
95
96
11678
void ProcessAssertions::spendResource(ResourceManager::Resource r)
97
{
98
11678
  d_resourceManager.spendResource(r);
99
11678
}
100
101
11325
bool ProcessAssertions::apply(Assertions& as)
102
{
103
11325
  AssertionPipeline& assertions = as.getAssertionPipeline();
104
11325
  Assert(d_preprocessingPassContext != nullptr);
105
  // Dump the assertions
106
11325
  dumpAssertions("pre-everything", assertions);
107
108
11325
  Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
109
11325
  Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
110
111
11325
  Debug("smt") << "#Assertions : " << assertions.size() << endl;
112
11325
  Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
113
114
11325
  if (assertions.size() == 0)
115
  {
116
    // nothing to do
117
    return true;
118
  }
119
120
22650
  if (options::bvGaussElim())
121
  {
122
    d_passes["bv-gauss"]->apply(&assertions);
123
  }
124
125
  // Add dummy assertion in last position - to be used as a
126
  // placeholder for any new assertions to get added
127
11325
  assertions.push_back(d_true);
128
  // any assertions added beyond realAssertionsEnd must NOT affect the
129
  // equisatisfiability
130
11325
  assertions.updateRealAssertionsEnd();
131
132
  // Assertions are NOT guaranteed to be rewritten by this point
133
134
22650
  Trace("smt-proc")
135
11325
      << "ProcessAssertions::processAssertions() : pre-definition-expansion"
136
11325
      << endl;
137
11325
  dumpAssertions("pre-definition-expansion", assertions);
138
  // Expand definitions, which replaces defined functions with their definition
139
  // and does beta reduction. Notice we pass true as the second argument since
140
  // we do not want to call theories to expand definitions here, since we want
141
  // to give the opportunity to rewrite/preprocess terms before expansion.
142
11325
  d_exDefs.expandAssertions(assertions, true);
143
22650
  Trace("smt-proc")
144
11325
      << "ProcessAssertions::processAssertions() : post-definition-expansion"
145
11325
      << endl;
146
11325
  dumpAssertions("post-definition-expansion", assertions);
147
148
11325
  Debug("smt") << " assertions     : " << assertions.size() << endl;
149
150
48204
  if (options::globalNegate())
151
  {
152
    // global negation of the formula
153
4
    d_passes["global-negate"]->apply(&assertions);
154
4
    as.flipGlobalNegated();
155
  }
156
157
22660
  if (options::nlExtPurify())
158
  {
159
9
    d_passes["nl-ext-purify"]->apply(&assertions);
160
  }
161
162
35069
  if (options::solveRealAsInt())
163
  {
164
13
    d_passes["real-to-int"]->apply(&assertions);
165
  }
166
167
11325
  if (options::solveIntAsBV() > 0)
168
  {
169
7
    d_passes["int-to-bv"]->apply(&assertions);
170
  }
171
172
40709
  if (options::ackermann())
173
  {
174
43
    d_passes["ackermann"]->apply(&assertions);
175
  }
176
177
1705803
  if (options::bvAbstraction())
178
  {
179
3
    d_passes["bv-abstraction"]->apply(&assertions);
180
  }
181
182
11325
  Debug("smt") << " assertions     : " << assertions.size() << endl;
183
184
11325
  bool noConflict = true;
185
186
22684
  if (options::extRewPrep())
187
  {
188
22
    d_passes["ext-rew-pre"]->apply(&assertions);
189
  }
190
191
  // Unconstrained simplification
192
57242
  if (options::unconstrainedSimp())
193
  {
194
147
    d_passes["rewrite"]->apply(&assertions);
195
147
    d_passes["unconstrained-simplifier"]->apply(&assertions);
196
  }
197
198
24473
  if (options::bvIntroducePow2())
199
  {
200
2
    d_passes["bv-intro-pow2"]->apply(&assertions);
201
  }
202
203
  // Lift bit-vectors of size 1 to bool
204
24682
  if (options::bitvectorToBool())
205
  {
206
155
    d_passes["bv-to-bool"]->apply(&assertions);
207
  }
208
11325
  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
209
  {
210
147
    d_passes["bv-to-int"]->apply(&assertions);
211
  }
212
22654
  if (options::foreignTheoryRewrite())
213
  {
214
2
    d_passes["foreign-theory-rewrite"]->apply(&assertions);
215
  }
216
217
  // Since this pass is not robust for the information tracking necessary for
218
  // unsat cores, it's only applied if we are not doing unsat core computation
219
11327
  d_passes["apply-substs"]->apply(&assertions);
220
221
  // Assertions MUST BE guaranteed to be rewritten by this point
222
11323
  d_passes["rewrite"]->apply(&assertions);
223
224
  // Convert non-top-level Booleans to bit-vectors of size 1
225
11323
  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
226
  {
227
12
    d_passes["bool-to-bv"]->apply(&assertions);
228
  }
229
22648
  if (options::sepPreSkolemEmp())
230
  {
231
1
    d_passes["sep-skolem-emp"]->apply(&assertions);
232
  }
233
234
11323
  if (d_smt.getLogicInfo().isQuantified())
235
  {
236
    // remove rewrite rules, apply pre-skolemization to existential quantifiers
237
6432
    d_passes["quantifiers-preprocess"]->apply(&assertions);
238
15744
    if (options::macrosQuant())
239
    {
240
      // quantifiers macro expansion
241
36
      d_passes["quantifier-macros"]->apply(&assertions);
242
    }
243
244
    // fmf-fun : assume admissible functions, applying preprocessing reduction
245
    // to FMF
246
21969
    if (options::fmfFunWellDefined())
247
    {
248
106
      d_passes["fun-def-fmf"]->apply(&assertions);
249
    }
250
  }
251
31171
  if (!options::stringLazyPreproc())
252
  {
253
34
    d_passes["strings-eager-pp"]->apply(&assertions);
254
  }
255
11323
  if (options::sortInference() || options::ufssFairnessMonotone())
256
  {
257
16
    d_passes["sort-inference"]->apply(&assertions);
258
  }
259
260
24469
  if (options::pbRewrites())
261
  {
262
2
    d_passes["pseudo-boolean-processor"]->apply(&assertions);
263
  }
264
265
  // rephrasing normal inputs as sygus problems
266
11323
  if (!d_smt.isInternalSubsolver())
267
  {
268
26507
    if (options::sygusInference())
269
    {
270
62
      d_passes["sygus-infer"]->apply(&assertions);
271
    }
272
25112
    else if (options::sygusRewSynthInput())
273
    {
274
      // do candidate rewrite rule synthesis
275
      d_passes["synth-rr"]->apply(&assertions);
276
    }
277
  }
278
279
22646
  Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
280
11323
                    << endl;
281
11323
  dumpAssertions("pre-simplify", assertions);
282
11323
  Chat() << "simplifying assertions..." << endl;
283
11323
  noConflict = simplifyAssertions(assertions);
284
11323
  if (!noConflict)
285
  {
286
966
    ++(d_smtStats.d_simplifiedToFalse);
287
  }
288
22646
  Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
289
11323
                    << endl;
290
11323
  dumpAssertions("post-simplify", assertions);
291
292
22646
  if (options::doStaticLearning())
293
  {
294
11323
    d_passes["static-learning"]->apply(&assertions);
295
  }
296
11323
  Debug("smt") << " assertions     : " << assertions.size() << endl;
297
298
22648
  if (options::earlyIteRemoval())
299
  {
300
1
    d_smtStats.d_numAssertionsPre += assertions.size();
301
1
    d_passes["ite-removal"]->apply(&assertions);
302
    // This is needed because when solving incrementally, removeITEs may
303
    // introduce skolems that were solved for earlier and thus appear in the
304
    // substitution map.
305
1
    d_passes["apply-substs"]->apply(&assertions);
306
1
    d_smtStats.d_numAssertionsPost += assertions.size();
307
  }
308
309
11323
  dumpAssertions("pre-repeat-simplify", assertions);
310
53168
  if (options::repeatSimp())
311
  {
312
710
    Trace("smt-proc")
313
355
        << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
314
355
        << endl;
315
355
    Chat() << "re-simplifying assertions..." << endl;
316
710
    ScopeCounter depth(d_simplifyAssertionsDepth);
317
355
    noConflict &= simplifyAssertions(assertions);
318
710
    Trace("smt-proc")
319
355
        << "ProcessAssertions::processAssertions() : post-repeat-simplify"
320
355
        << endl;
321
  }
322
11323
  dumpAssertions("post-repeat-simplify", assertions);
323
324
11323
  if (options::ufHo())
325
  {
326
212
    d_passes["ho-elim"]->apply(&assertions);
327
  }
328
329
  // begin: INVARIANT to maintain: no reordering of assertions or
330
  // introducing new ones
331
332
11323
  Debug("smt") << " assertions     : " << assertions.size() << endl;
333
334
22646
  Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
335
11323
               << endl;
336
11323
  Debug("smt") << " assertions     : " << assertions.size() << endl;
337
338
  // ensure rewritten
339
11323
  d_passes["rewrite"]->apply(&assertions);
340
  // rewrite equalities based on theory-specific rewriting
341
11323
  d_passes["theory-rewrite-eq"]->apply(&assertions);
342
  // apply theory preprocess, which includes ITE removal
343
11330
  d_passes["theory-preprocess"]->apply(&assertions);
344
  // notice that we do not apply substitutions as a last step here, since
345
  // the range of substitutions is not theory-preprocessed.
346
347
11316
  if (options::bitblastMode() == options::BitblastMode::EAGER)
348
  {
349
41
    d_passes["bv-eager-atoms"]->apply(&assertions);
350
  }
351
352
11316
  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
353
11316
  dumpAssertions("post-everything", assertions);
354
355
11316
  return noConflict;
356
}
357
358
// returns false if simplification led to "false"
359
11678
bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
360
{
361
11678
  spendResource(ResourceManager::Resource::PreprocessStep);
362
  try
363
  {
364
22377
    ScopeCounter depth(d_simplifyAssertionsDepth);
365
366
11678
    Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
367
368
41942
    if (options::simplificationMode() != options::SimplificationMode::NONE)
369
    {
370
      // Perform non-clausal simplification
371
      PreprocessingPassResult res =
372
9681
          d_passes["non-clausal-simp"]->apply(&assertions);
373
9681
      if (res == PreprocessingPassResult::CONFLICT)
374
      {
375
971
        return false;
376
      }
377
378
      // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
379
      // do the miplib trick.
380
8710
      if (  // check that option is on
381
27970
          options::arithMLTrick() &&
382
          // only useful in arith
383
8718
          d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
384
          // we add new assertions and need this (in practice, this
385
          // restriction only disables miplib processing during
386
          // re-simplification, which we don't expect to be useful anyway)
387
8
          assertions.getRealAssertionsEnd() == assertions.size())
388
      {
389
8
        d_passes["miplib-trick"]->apply(&assertions);
390
      }
391
      else
392
      {
393
17404
        Trace("simplify") << "SmtEnginePrivate::simplify(): "
394
8702
                          << "skipping miplib pseudobooleans pass..." << endl;
395
      }
396
    }
397
398
10707
    Debug("smt") << " assertions     : " << assertions.size() << endl;
399
400
    // ITE simplification
401
42939
    if (options::doITESimp()
402
10707
        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
403
    {
404
1
      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
405
1
      if (res == PreprocessingPassResult::CONFLICT)
406
      {
407
        Chat() << "...ITE simplification found unsat..." << endl;
408
        return false;
409
      }
410
    }
411
412
10707
    Debug("smt") << " assertions     : " << assertions.size() << endl;
413
414
    // Unconstrained simplification
415
10707
    if (options::unconstrainedSimp())
416
    {
417
264
      d_passes["unconstrained-simplifier"]->apply(&assertions);
418
    }
419
420
21414
    if (options::repeatSimp()
421
10707
        && options::simplificationMode() != options::SimplificationMode::NONE)
422
    {
423
      PreprocessingPassResult res =
424
674
          d_passes["non-clausal-simp"]->apply(&assertions);
425
674
      if (res == PreprocessingPassResult::CONFLICT)
426
      {
427
8
        return false;
428
      }
429
    }
430
431
10699
    dumpAssertions("post-repeatsimp", assertions);
432
10699
    Trace("smt") << "POST repeatSimp" << endl;
433
10699
    Debug("smt") << " assertions     : " << assertions.size() << endl;
434
  }
435
  catch (TypeCheckingExceptionPrivate& tcep)
436
  {
437
    // Calls to this function should have already weeded out any
438
    // typechecking exceptions via (e.g.) ensureBoolean().  But a
439
    // theory could still create a new expression that isn't
440
    // well-typed, and we don't want the C++ runtime to abort our
441
    // process without any error notice.
442
    InternalError()
443
        << "A bad expression was produced.  Original exception follows:\n"
444
        << tcep;
445
  }
446
10699
  return true;
447
}
448
449
101282
void ProcessAssertions::dumpAssertions(const char* key,
450
                                       const AssertionPipeline& assertionList)
451
{
452
101282
  if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
453
  {
454
    // Push the simplified assertions to the dump output stream
455
    for (unsigned i = 0; i < assertionList.size(); ++i)
456
    {
457
      TNode n = assertionList[i];
458
      d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
459
          d_smt.getOutputManager().getDumpOut(), n);
460
    }
461
  }
462
101282
}
463
464
}  // namespace smt
465
2168189
}  // namespace CVC4