GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/non_clausal_simp.cpp Lines: 230 239 96.2 %
Date: 2021-03-22 Branches: 525 1280 41.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file non_clausal_simp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Gereon Kremer
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 Non-clausal simplification preprocessing pass.
13
 **
14
 ** Run the nonclausal solver and try to solve all assigned theory literals.
15
 **/
16
17
#include "preprocessing/passes/non_clausal_simp.h"
18
19
#include <vector>
20
21
#include "context/cdo.h"
22
#include "options/smt_options.h"
23
#include "preprocessing/assertion_pipeline.h"
24
#include "preprocessing/preprocessing_pass_context.h"
25
#include "smt/preprocess_proof_generator.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "theory/booleans/circuit_propagator.h"
28
#include "theory/theory.h"
29
#include "theory/theory_engine.h"
30
#include "theory/theory_model.h"
31
#include "theory/trust_substitutions.h"
32
33
using namespace CVC4;
34
using namespace CVC4::theory;
35
36
namespace CVC4 {
37
namespace preprocessing {
38
namespace passes {
39
40
/* -------------------------------------------------------------------------- */
41
42
8995
NonClausalSimp::Statistics::Statistics()
43
    : d_numConstantProps(
44
8995
          "preprocessing::passes::NonClausalSimp::NumConstantProps", 0)
45
{
46
8995
  smtStatisticsRegistry()->registerStat(&d_numConstantProps);
47
8995
}
48
49
17984
NonClausalSimp::Statistics::~Statistics()
50
{
51
8992
  smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
52
8992
}
53
54
/* -------------------------------------------------------------------------- */
55
56
8995
NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
57
    : PreprocessingPass(preprocContext, "non-clausal-simp"),
58
8995
      d_pnm(preprocContext->getProofNodeManager()),
59
8995
      d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
60
                         d_pnm,
61
962
                         preprocContext->getUserContext(),
62
962
                         "NonClausalSimp::llpg")
63
                   : nullptr),
64
8995
      d_llra(d_pnm ? new LazyCDProof(d_pnm,
65
                                     nullptr,
66
962
                                     preprocContext->getUserContext(),
67
962
                                     "NonClausalSimp::llra")
68
                   : nullptr),
69
39828
      d_tsubsList(preprocContext->getUserContext())
70
{
71
8995
}
72
73
10353
PreprocessingPassResult NonClausalSimp::applyInternal(
74
    AssertionPipeline* assertionsToPreprocess)
75
{
76
10353
  Assert(!options::unsatCores() || isProofEnabled())
77
      << "Unsat cores with non-clausal simp only supported with new proofs";
78
79
10353
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
80
81
  theory::booleans::CircuitPropagator* propagator =
82
10353
      d_preprocContext->getCircuitPropagator();
83
84
91571
  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
85
  {
86
162436
    Trace("non-clausal-simplify") << "Assertion #" << i << " : "
87
81218
                                  << (*assertionsToPreprocess)[i] << std::endl;
88
  }
89
90
10353
  if (propagator->getNeedsFinish())
91
  {
92
3633
    propagator->finish();
93
3633
    propagator->setNeedsFinish(false);
94
  }
95
10353
  propagator->initialize();
96
97
  // Assert all the assertions to the propagator
98
10353
  Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
99
91571
  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
100
  {
101
81218
    Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
102
           == (*assertionsToPreprocess)[i]);
103
    // Don't reprocess substitutions
104
81218
    if (assertionsToPreprocess->isSubstsIndex(i))
105
    {
106
2224
      continue;
107
    }
108
157988
    Trace("non-clausal-simplify")
109
78994
        << "asserting " << (*assertionsToPreprocess)[i] << std::endl;
110
157988
    Debug("cores") << "propagator->assertTrue: " << (*assertionsToPreprocess)[i]
111
78994
                   << std::endl;
112
78994
    propagator->assertTrue((*assertionsToPreprocess)[i]);
113
  }
114
115
10353
  Trace("non-clausal-simplify") << "propagating" << std::endl;
116
20706
  TrustNode conf = propagator->propagate();
117
10353
  if (!conf.isNull())
118
  {
119
    // If in conflict, just return false
120
1622
    Trace("non-clausal-simplify")
121
811
        << "conflict in non-clausal propagation" << std::endl;
122
811
    assertionsToPreprocess->clear();
123
811
    assertionsToPreprocess->pushBackTrusted(conf);
124
811
    propagator->setNeedsFinish(true);
125
811
    return PreprocessingPassResult::CONFLICT;
126
  }
127
128
19084
  Trace("non-clausal-simplify")
129
19084
      << "Iterate through " << propagator->getLearnedLiterals().size()
130
9542
      << " learned literals." << std::endl;
131
  // No conflict, go through the literals and solve them
132
9542
  context::Context* u = d_preprocContext->getUserContext();
133
9542
  TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
134
9542
  CVC4_UNUSED SubstitutionMap& top_level_substs = ttls.get();
135
  // constant propagations
136
  std::shared_ptr<TrustSubstitutionMap> constantPropagations =
137
      std::make_shared<TrustSubstitutionMap>(
138
19084
          u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA);
139
9542
  SubstitutionMap& cps = constantPropagations->get();
140
  // new substitutions
141
  std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
142
      std::make_shared<TrustSubstitutionMap>(
143
19084
          u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA);
144
9542
  SubstitutionMap& nss = newSubstitutions->get();
145
146
9542
  size_t j = 0;
147
9542
  std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals();
148
  // if proofs are enabled, we will need to track the proofs of learned literals
149
9542
  if (isProofEnabled())
150
  {
151
1615
    d_tsubsList.push_back(constantPropagations);
152
1615
    d_tsubsList.push_back(newSubstitutions);
153
25829
    for (const TrustNode& tll : learned_literals)
154
    {
155
24214
      d_llpg->notifyNewTrustedAssert(tll);
156
    }
157
  }
158
120970
  for (size_t i = 0, size = learned_literals.size(); i < size; ++i)
159
  {
160
    // Simplify the literal we learned wrt previous substitutions
161
222674
    Node learnedLiteral = learned_literals[i].getNode();
162
111596
    Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
163
111596
    Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
164
    // process the learned literal with substitutions and const propagations
165
111596
    learnedLiteral = processLearnedLit(
166
        learnedLiteral, newSubstitutions.get(), constantPropagations.get());
167
223192
    Trace("non-clausal-simplify")
168
111596
        << "Process learnedLiteral, after constProp : " << learnedLiteral
169
111596
        << std::endl;
170
    // It might just simplify to a constant
171
111596
    if (learnedLiteral.isConst())
172
    {
173
518
      if (learnedLiteral.getConst<bool>())
174
      {
175
        // If the learned literal simplifies to true, it's redundant
176
350
        continue;
177
      }
178
      else
179
      {
180
        // If the learned literal simplifies to false, we're in conflict
181
336
        Trace("non-clausal-simplify")
182
168
            << "conflict with " << learned_literals[i].getNode() << std::endl;
183
168
        assertionsToPreprocess->clear();
184
336
        Node n = NodeManager::currentNM()->mkConst<bool>(false);
185
168
        assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
186
168
        propagator->setNeedsFinish(true);
187
168
        return PreprocessingPassResult::CONFLICT;
188
      }
189
    }
190
191
    // Solve it with the corresponding theory, possibly adding new
192
    // substitutions to newSubstitutions
193
111078
    Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
194
195
    TrustNode tlearnedLiteral =
196
222156
        TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get());
197
    Theory::PPAssertStatus solveStatus =
198
333234
        d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
199
222156
                                                   *newSubstitutions.get());
200
201
111078
    switch (solveStatus)
202
    {
203
45907
      case Theory::PP_ASSERT_STATUS_SOLVED:
204
      {
205
        // The literal should rewrite to true
206
91814
        Trace("non-clausal-simplify")
207
45907
            << "solved " << learnedLiteral << std::endl;
208
45907
        Assert(Rewriter::rewrite(nss.apply(learnedLiteral)).isConst());
209
        // else fall through
210
45907
        break;
211
      }
212
      case Theory::PP_ASSERT_STATUS_CONFLICT:
213
      {
214
        // If in conflict, we return false
215
        Trace("non-clausal-simplify")
216
            << "conflict while solving " << learnedLiteral << std::endl;
217
        assertionsToPreprocess->clear();
218
        Node n = NodeManager::currentNM()->mkConst<bool>(false);
219
        assertionsToPreprocess->push_back(n);
220
        propagator->setNeedsFinish(true);
221
        return PreprocessingPassResult::CONFLICT;
222
      }
223
65171
      default:
224
130342
        if (learnedLiteral.getKind() == kind::EQUAL
225
130342
            && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst()))
226
        {
227
          // constant propagation
228
10248
          TNode t;
229
10248
          TNode c;
230
5124
          if (learnedLiteral[0].isConst())
231
          {
232
347
            t = learnedLiteral[1];
233
347
            c = learnedLiteral[0];
234
          }
235
          else
236
          {
237
4777
            t = learnedLiteral[0];
238
4777
            c = learnedLiteral[1];
239
          }
240
5124
          Assert(!t.isConst());
241
5124
          Assert(cps.apply(t, true) == t);
242
5124
          Assert(top_level_substs.apply(t) == t);
243
5124
          Assert(nss.apply(t) == t);
244
          // also add to learned literal
245
10248
          ProofGenerator* cpg = constantPropagations->addSubstitutionSolved(
246
5124
              t, c, tlearnedLiteral);
247
          // We need to justify (= t c) as a literal, since it is reasserted
248
          // to the assertion pipeline below. We do this with the proof
249
          // generator returned by the above call.
250
5124
          if (isProofEnabled())
251
          {
252
823
            d_llpg->notifyNewAssert(t.eqNode(c), cpg);
253
          }
254
        }
255
        else
256
        {
257
          // Keep the literal
258
60047
          learned_literals[j++] = learned_literals[i];
259
        }
260
65171
        break;
261
    }
262
  }
263
264
#ifdef CVC4_ASSERTIONS
265
  // NOTE: When debugging this code, consider moving this check inside of the
266
  // loop over propagator->getLearnedLiterals(). This check has been moved
267
  // outside because it is costly for certain inputs (see bug 508).
268
  //
269
  // Check data structure invariants:
270
  // 1. for each lhs of top_level_substs, does not appear anywhere in rhs of
271
  // top_level_substs or anywhere in constantPropagations
272
  // 2. each lhs of constantPropagations rewrites to itself
273
  // 3. if l -> r is a constant propagation and l is a subterm of l' with l' ->
274
  // r' another constant propagation, then l'[l/r] -> r' should be a
275
  //    constant propagation too
276
  // 4. each lhs of constantPropagations is different from each rhs
277
54858
  for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
278
  {
279
45484
    Assert((*pos).first.isVar());
280
45484
    Assert(top_level_substs.apply((*pos).first) == (*pos).first);
281
45484
    Assert(top_level_substs.apply((*pos).second) == (*pos).second);
282
90968
    Node app = nss.apply((*pos).second);
283
45484
    Assert(nss.apply(app) == app);
284
  }
285
14478
  for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
286
  {
287
5104
    Assert((*pos).second.isConst());
288
5104
    Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
289
5104
    Assert(cps.apply((*pos).second) == (*pos).second);
290
  }
291
#endif /* CVC4_ASSERTIONS */
292
293
  // Resize the learnt
294
18748
  Trace("non-clausal-simplify")
295
9374
      << "Resize non-clausal learned literals to " << j << std::endl;
296
9374
  learned_literals.resize(j);
297
298
18748
  std::unordered_set<TNode, TNodeHashFunction> s;
299
86133
  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
300
  {
301
153518
    Node assertion = (*assertionsToPreprocess)[i];
302
153518
    TrustNode assertionNew = newSubstitutions->apply(assertion);
303
76759
    Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
304
76759
    if (!assertionNew.isNull())
305
    {
306
56284
      Trace("non-clausal-simplify")
307
28142
          << "assertionNew = " << assertionNew.getNode() << std::endl;
308
28142
      assertionsToPreprocess->replaceTrusted(i, assertionNew);
309
28142
      assertion = assertionNew.getNode();
310
28142
      Assert(Rewriter::rewrite(assertion) == assertion);
311
    }
312
    for (;;)
313
    {
314
79015
      assertionNew = constantPropagations->apply(assertion);
315
77887
      if (assertionNew.isNull())
316
      {
317
76759
        break;
318
      }
319
1128
      Assert(assertionNew.getNode() != assertion);
320
1128
      assertionsToPreprocess->replaceTrusted(i, assertionNew);
321
1128
      assertion = assertionNew.getNode();
322
1128
      d_statistics.d_numConstantProps += 1;
323
2256
      Trace("non-clausal-simplify")
324
1128
          << "assertionNew = " << assertion << std::endl;
325
    }
326
76759
    s.insert(assertion);
327
153518
    Trace("non-clausal-simplify")
328
76759
        << "non-clausal preprocessed: " << assertion << std::endl;
329
  }
330
331
  // add substitutions to model, or as assertions if needed (when incremental)
332
9374
  TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
333
9374
  Assert(m != nullptr);
334
9374
  NodeManager* nm = NodeManager::currentNM();
335
54858
  for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
336
  {
337
90968
    Node lhs = (*pos).first;
338
90968
    TrustNode trhs = newSubstitutions->apply((*pos).second);
339
90968
    Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode();
340
    // If using incremental, we must check whether this variable has occurred
341
    // before now. If it hasn't we can add this as a substitution.
342
90968
    if (!assertionsToPreprocess->storeSubstsInAsserts()
343
50464
        || d_preprocContext->getSymsInAssertions().find(lhs)
344
50464
               == d_preprocContext->getSymsInAssertions().end())
345
    {
346
88560
      Trace("non-clausal-simplify")
347
44280
          << "substitute: " << lhs << " " << rhs << std::endl;
348
44280
      m->addSubstitution(lhs, rhs);
349
    }
350
    else
351
    {
352
      // if it has, the substitution becomes an assertion
353
2408
      Node eq = nm->mkNode(kind::EQUAL, lhs, rhs);
354
2408
      Trace("non-clausal-simplify")
355
1204
          << "substitute: will notify SAT layer of substitution: " << eq
356
1204
          << std::endl;
357
1204
       trhs = newSubstitutions->apply((*pos).first);
358
1204
       Assert(!trhs.isNull());
359
1204
       assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
360
       trhs.getGenerator());
361
    }
362
  }
363
364
9374
  Assert(assertionsToPreprocess->getRealAssertionsEnd()
365
         <= assertionsToPreprocess->size());
366
  // Learned literals to conjoin. If proofs are enabled, all these are
367
  // justified by d_llpg.
368
18748
  std::vector<Node> learnedLitsToConjoin;
369
370
68882
  for (size_t i = 0; i < learned_literals.size(); ++i)
371
  {
372
97320
    Node learned = learned_literals[i].getNode();
373
59508
    Assert(top_level_substs.apply(learned) == learned);
374
    // process learned literal
375
59508
    learned = processLearnedLit(
376
        learned, newSubstitutions.get(), constantPropagations.get());
377
59508
    if (s.find(learned) != s.end())
378
    {
379
21696
      continue;
380
    }
381
37812
    s.insert(learned);
382
37812
    learnedLitsToConjoin.push_back(learned);
383
75624
    Trace("non-clausal-simplify")
384
37812
        << "non-clausal learned : " << learned << std::endl;
385
  }
386
9374
  learned_literals.clear();
387
388
14478
  for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
389
  {
390
10117
    Node cProp = (*pos).first.eqNode((*pos).second);
391
5104
    Assert(top_level_substs.apply(cProp) == cProp);
392
    // process learned literal (substitutions only)
393
5104
    cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr);
394
5104
    if (s.find(cProp) != s.end())
395
    {
396
91
      continue;
397
    }
398
5013
    s.insert(cProp);
399
5013
    learnedLitsToConjoin.push_back(cProp);
400
10026
    Trace("non-clausal-simplify")
401
5013
        << "non-clausal constant propagation : " << cProp << std::endl;
402
  }
403
404
  // Add new substitutions to topLevelSubstitutions
405
  // Note that we don't have to keep rhs's in full solved form
406
  // because SubstitutionMap::apply does a fixed-point iteration when
407
  // substituting
408
9374
  ttls.addSubstitutions(*newSubstitutions.get());
409
410
9374
  if (!learnedLitsToConjoin.empty())
411
  {
412
2324
    size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
413
4648
    Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
414
4648
    Trace("non-clausal-simplify")
415
2324
        << "non-clausal simplification, reassert: " << newConj << std::endl;
416
2324
    ProofGenerator* pg = nullptr;
417
2324
    if (isProofEnabled())
418
    {
419
      // justify in d_llra
420
13685
      for (const Node& lit : learnedLitsToConjoin)
421
      {
422
13244
        d_llra->addLazyStep(lit, d_llpg.get());
423
      }
424
441
      if (learnedLitsToConjoin.size() > 1)
425
      {
426
343
        d_llra->addStep(newConj, PfRule::AND_INTRO, learnedLitsToConjoin, {});
427
343
        pg = d_llra.get();
428
      }
429
      else
430
      {
431
        // otherwise we ask the learned literal proof generator directly
432
98
        pg = d_llpg.get();
433
      }
434
    }
435
    // ------- from d_llpg    --------- from d_llpg
436
    //  conj[0]       ....    d_conj[n]
437
    // -------------------------------- AND_INTRO
438
    //  newConj
439
    // where newConj is conjoined at the given index
440
2324
    assertionsToPreprocess->conjoin(replIndex, newConj, pg);
441
  }
442
443
9374
  propagator->setNeedsFinish(true);
444
9374
  return PreprocessingPassResult::NO_CONFLICT;
445
}
446
447
53705
bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; }
448
449
176208
Node NonClausalSimp::processLearnedLit(Node lit,
450
                                       theory::TrustSubstitutionMap* subs,
451
                                       theory::TrustSubstitutionMap* cp)
452
{
453
352416
  TrustNode tlit;
454
176208
  if (subs != nullptr)
455
  {
456
176208
    tlit = subs->apply(lit);
457
176208
    if (!tlit.isNull())
458
    {
459
36563
      lit = processRewrittenLearnedLit(tlit);
460
    }
461
352416
    Trace("non-clausal-simplify")
462
176208
        << "Process learnedLiteral, after newSubs : " << lit << std::endl;
463
  }
464
  // apply to fixed point
465
176208
  if (cp != nullptr)
466
  {
467
    for (;;)
468
    {
469
171408
      tlit = cp->apply(lit);
470
171256
      if (tlit.isNull())
471
      {
472
171104
        break;
473
      }
474
152
      Assert(lit != tlit.getNode());
475
152
      lit = processRewrittenLearnedLit(tlit);
476
152
      d_statistics.d_numConstantProps += 1;
477
    }
478
  }
479
352416
  return lit;
480
}
481
482
36715
Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn)
483
{
484
36715
  if (isProofEnabled())
485
  {
486
10907
    d_llpg->notifyTrustedPreprocessed(trn);
487
  }
488
  // return the node
489
36715
  return trn.getNode();
490
}
491
492
}  // namespace passes
493
}  // namespace preprocessing
494
26676
}  // namespace CVC4