GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/ite_removal.cpp Lines: 23 24 95.8 %
Date: 2021-03-23 Branches: 31 88 35.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ite_removal.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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
 ** \brief Remove ITEs from the assertions
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "preprocessing/passes/ite_removal.h"
19
20
#include "options/smt_options.h"
21
#include "preprocessing/assertion_pipeline.h"
22
#include "preprocessing/preprocessing_pass_context.h"
23
#include "proof/proof_manager.h"
24
#include "prop/prop_engine.h"
25
#include "theory/rewriter.h"
26
#include "theory/theory_preprocessor.h"
27
28
namespace CVC4 {
29
namespace preprocessing {
30
namespace passes {
31
32
using namespace CVC4::theory;
33
34
// TODO (project #42): note this preprocessing pass is deprecated
35
8997
IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
36
8997
    : PreprocessingPass(preprocContext, "ite-removal")
37
{
38
8997
}
39
40
1
PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
41
{
42
1
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
43
44
1
  IteSkolemMap& imap = assertions->getIteSkolemMap();
45
  // Remove all of the ITE occurrences and normalize
46
1
  prop::PropEngine* pe = d_preprocContext->getPropEngine();
47
3
  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
48
  {
49
4
    Node assertion = (*assertions)[i];
50
4
    std::vector<theory::TrustNode> newAsserts;
51
4
    std::vector<Node> newSkolems;
52
4
    TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
53
2
    if (!trn.isNull())
54
    {
55
      // process
56
1
      assertions->replaceTrusted(i, trn);
57
    }
58
2
    Assert(newSkolems.size() == newAsserts.size());
59
326
    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
60
    {
61
324
      imap[assertions->size()] = newSkolems[j];
62
324
      assertions->pushBackTrusted(newAsserts[j]);
63
      // new assertions have a dependence on the node (old pf architecture)
64
32660399
      if (options::unsatCores() && !options::produceProofs())
65
      {
66
        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
67
                                                 assertion);
68
      }
69
    }
70
  }
71
327
  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
72
  {
73
326
    assertions->replace(i, Rewriter::rewrite((*assertions)[i]));
74
  }
75
76
1
  return PreprocessingPassResult::NO_CONFLICT;
77
}
78
79
80
}  // namespace passes
81
}  // namespace preprocessing
82
32686760
}  // namespace CVC4