GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/theory_preprocess.cpp Lines: 21 21 100.0 %
Date: 2021-03-22 Branches: 32 72 44.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_preprocess.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
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 TheoryPreprocess preprocessing pass
13
 **
14
 ** Calls Theory::preprocess(...) on every assertion of the formula.
15
 **/
16
17
#include "preprocessing/passes/theory_preprocess.h"
18
19
#include "options/smt_options.h"
20
#include "preprocessing/assertion_pipeline.h"
21
#include "preprocessing/preprocessing_pass_context.h"
22
#include "proof/proof_manager.h"
23
#include "prop/prop_engine.h"
24
#include "theory/rewriter.h"
25
#include "theory/theory_engine.h"
26
27
namespace CVC4 {
28
namespace preprocessing {
29
namespace passes {
30
31
using namespace CVC4::theory;
32
33
8995
TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
34
8995
    : PreprocessingPass(preprocContext, "theory-preprocess"){};
35
36
11321
PreprocessingPassResult TheoryPreprocess::applyInternal(
37
    AssertionPipeline* assertions)
38
{
39
11321
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
40
41
11321
  IteSkolemMap& imap = assertions->getIteSkolemMap();
42
11321
  prop::PropEngine* propEngine = d_preprocContext->getPropEngine();
43
  // Remove all of the ITE occurrences and normalize
44
103628
  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
45
  {
46
184628
    Node assertion = (*assertions)[i];
47
184628
    std::vector<theory::TrustNode> newAsserts;
48
184628
    std::vector<Node> newSkolems;
49
184628
    TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
50
92307
    if (!trn.isNull())
51
    {
52
      // process
53
2656
      assertions->replaceTrusted(i, trn);
54
    }
55
92307
    Assert(newSkolems.size() == newAsserts.size());
56
111527
    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
57
    {
58
19220
      imap[assertions->size()] = newSkolems[j];
59
19220
      assertions->pushBackTrusted(newAsserts[j]);
60
      // new assertions have a dependence on the node (old pf architecture)
61
19220
      if (options::unsatCores())
62
      {
63
6673
        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
64
                                                 assertion);
65
      }
66
    }
67
  }
68
69
11314
  return PreprocessingPassResult::NO_CONFLICT;
70
}
71
72
73
}  // namespace passes
74
}  // namespace preprocessing
75
26676
}  // namespace CVC4