GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/static_learning.cpp Lines: 15 15 100.0 %
Date: 2021-03-22 Branches: 20 38 52.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file static_learning.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Gereon Kremer, Andrew Reynolds
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 static learning preprocessing pass
13
 **
14
 **/
15
16
#include "preprocessing/passes/static_learning.h"
17
18
#include <string>
19
20
#include "expr/node.h"
21
#include "preprocessing/assertion_pipeline.h"
22
#include "preprocessing/preprocessing_pass_context.h"
23
#include "theory/rewriter.h"
24
#include "theory/theory_engine.h"
25
26
namespace CVC4 {
27
namespace preprocessing {
28
namespace passes {
29
30
8995
StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext)
31
8995
    : PreprocessingPass(preprocContext, "static-learning"){};
32
33
11321
PreprocessingPassResult StaticLearning::applyInternal(
34
    AssertionPipeline* assertionsToPreprocess)
35
{
36
11321
  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
37
38
103319
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
39
  {
40
183996
    NodeBuilder<> learned(kind::AND);
41
91998
    learned << (*assertionsToPreprocess)[i];
42
183996
    d_preprocContext->getTheoryEngine()->ppStaticLearn(
43
91998
        (*assertionsToPreprocess)[i], learned);
44
91998
    if (learned.getNumChildren() == 1)
45
    {
46
91653
      learned.clear();
47
    }
48
    else
49
    {
50
345
      assertionsToPreprocess->replace(
51
690
          i, theory::Rewriter::rewrite(learned.constructNode()));
52
    }
53
  }
54
11321
  return PreprocessingPassResult::NO_CONFLICT;
55
}
56
57
58
}  // namespace passes
59
}  // namespace preprocessing
60
26676
}  // namespace CVC4