GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/learned_literal_manager.cpp Lines: 18 18 100.0 %
Date: 2021-09-29 Branches: 27 52 51.9 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Learned literal manager
14
 */
15
16
#include "preprocessing/learned_literal_manager.h"
17
18
#include "theory/rewriter.h"
19
20
namespace cvc5 {
21
namespace preprocessing {
22
23
6345
LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
24
                                             context::UserContext* u,
25
6345
                                             ProofNodeManager* pnm)
26
6345
    : d_topLevelSubs(tls), d_learnedLits(u)
27
{
28
6345
}
29
30
39013
void LearnedLiteralManager::notifyLearnedLiteral(TNode lit)
31
{
32
39013
  d_learnedLits.insert(lit);
33
39013
  Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl;
34
39013
}
35
36
1
std::vector<Node> LearnedLiteralManager::getLearnedLiterals() const
37
{
38
1
  std::vector<Node> currLearnedLits;
39
5
  for (const auto& lit: d_learnedLits)
40
  {
41
    // update based on substitutions
42
8
    Node tlsNode = d_topLevelSubs.get().apply(lit);
43
4
    tlsNode = theory::Rewriter::rewrite(tlsNode);
44
4
    currLearnedLits.push_back(tlsNode);
45
8
    Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit
46
4
                    << std::endl;
47
  }
48
1
  return currLearnedLits;
49
}
50
51
}  // namespace preprocessing
52
22746
}  // namespace cvc5