GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/preprocessing_pass.cpp Lines: 29 29 100.0 %
Date: 2021-03-22 Branches: 51 92 55.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file preprocessing_pass.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Justin Xu, Abdalrhman Mohamed, 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 preprocessing pass super class
13
 **
14
 ** Preprocessing pass super class.
15
 **/
16
17
#include "preprocessing/preprocessing_pass.h"
18
19
#include "preprocessing/assertion_pipeline.h"
20
#include "preprocessing/preprocessing_pass_context.h"
21
#include "printer/printer.h"
22
#include "smt/dump.h"
23
#include "smt/output_manager.h"
24
#include "smt/smt_engine_scope.h"
25
#include "smt/smt_statistics_registry.h"
26
27
namespace CVC4 {
28
namespace preprocessing {
29
30
86209
PreprocessingPassResult PreprocessingPass::apply(
31
    AssertionPipeline* assertionsToPreprocess) {
32
172418
  TimerStat::CodeTimer codeTimer(d_timer);
33
86209
  Trace("preprocessing") << "PRE " << d_name << std::endl;
34
86209
  Chat() << d_name << "..." << std::endl;
35
86209
  dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
36
86209
  PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
37
86200
  dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess);
38
86200
  Trace("preprocessing") << "POST " << d_name << std::endl;
39
172400
  return result;
40
}
41
42
172409
void PreprocessingPass::dumpAssertions(const char* key,
43
                                       const AssertionPipeline& assertionList) {
44
172409
  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
45
  {
46
    // Push the simplified assertions to the dump output stream
47
1
    OutputManager& outMgr = d_preprocContext->getSmt()->getOutputManager();
48
1
    const Printer& printer = outMgr.getPrinter();
49
1
    std::ostream& out = outMgr.getDumpOut();
50
51
5
    for (const auto& n : assertionList)
52
    {
53
4
      printer.toStreamCmdAssert(out, n);
54
    }
55
  }
56
172409
}
57
58
305836
PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
59
305836
                                     const std::string& name)
60
305836
    : d_name(name), d_timer("preprocessing::" + name) {
61
305836
  d_preprocContext = preprocContext;
62
305836
  smtStatisticsRegistry()->registerStat(&d_timer);
63
305836
}
64
65
611468
PreprocessingPass::~PreprocessingPass() {
66
305734
  Assert(smt::smtEngineInScope());
67
305734
  if (smtStatisticsRegistry() != nullptr) {
68
305734
    smtStatisticsRegistry()->unregisterStat(&d_timer);
69
  }
70
305734
}
71
72
}  // namespace preprocessing
73
26676
}  // namespace CVC4