GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/preprocessing_pass_context.cpp Lines: 19 19 100.0 %
Date: 2021-03-22 Branches: 15 28 53.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file preprocessing_pass_context.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, 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 The preprocessing pass context for passes
13
 **
14
 ** The preprocessing pass context for passes.
15
 **/
16
17
#include "preprocessing/preprocessing_pass_context.h"
18
19
#include "expr/node_algorithm.h"
20
21
namespace CVC4 {
22
namespace preprocessing {
23
24
8995
PreprocessingPassContext::PreprocessingPassContext(
25
    SmtEngine* smt,
26
    theory::booleans::CircuitPropagator* circuitPropagator,
27
8995
    ProofNodeManager* pnm)
28
    : d_smt(smt),
29
8995
      d_resourceManager(smt->getResourceManager()),
30
8995
      d_topLevelSubstitutions(smt->getUserContext(), pnm),
31
      d_circuitPropagator(circuitPropagator),
32
      d_pnm(pnm),
33
26985
      d_symsInAssertions(smt->getUserContext())
34
{
35
8995
}
36
37
theory::TrustSubstitutionMap&
38
20932
PreprocessingPassContext::getTopLevelSubstitutions()
39
{
40
20932
  return d_topLevelSubstitutions;
41
}
42
43
3946
void PreprocessingPassContext::recordSymbolsInAssertions(
44
    const std::vector<Node>& assertions)
45
{
46
7892
  std::unordered_set<TNode, TNodeHashFunction> visited;
47
7892
  std::unordered_set<Node, NodeHashFunction> syms;
48
20969
  for (TNode cn : assertions)
49
  {
50
17023
    expr::getSymbols(cn, syms, visited);
51
  }
52
29974
  for (const Node& s : syms)
53
  {
54
26028
    d_symsInAssertions.insert(s);
55
  }
56
3946
}
57
58
8995
ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
59
{
60
8995
  return d_pnm;
61
}
62
63
}  // namespace preprocessing
64
26676
}  // namespace CVC4