GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/apply_substs.cpp Lines: 21 21 100.0 %
Date: 2021-03-22 Branches: 30 54 55.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file apply_substs.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, 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 Apply substitutions preprocessing pass.
13
 **
14
 ** Apply top level substitutions to assertions, rewrite, and store back into
15
 ** assertions.
16
 **/
17
18
#include "preprocessing/passes/apply_substs.h"
19
20
#include "context/cdo.h"
21
#include "preprocessing/assertion_pipeline.h"
22
#include "preprocessing/preprocessing_pass_context.h"
23
#include "theory/rewriter.h"
24
#include "theory/substitutions.h"
25
26
namespace CVC4 {
27
namespace preprocessing {
28
namespace passes {
29
30
8995
ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
31
8995
    : PreprocessingPass(preprocContext, "apply-substs")
32
{
33
8995
}
34
35
11324
PreprocessingPassResult ApplySubsts::applyInternal(
36
    AssertionPipeline* assertionsToPreprocess)
37
{
38
11324
  Chat() << "applying substitutions..." << std::endl;
39
22648
  Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): "
40
11324
                        << "applying substitutions" << std::endl;
41
  // TODO(#1255): Substitutions in incremental mode should be managed with a
42
  // proper data structure.
43
44
  theory::TrustSubstitutionMap& tlsm =
45
11324
      d_preprocContext->getTopLevelSubstitutions();
46
11324
  unsigned size = assertionsToPreprocess->size();
47
107127
  for (unsigned i = 0; i < size; ++i)
48
  {
49
95805
    if (assertionsToPreprocess->isSubstsIndex(i))
50
    {
51
2323
      continue;
52
    }
53
186964
    Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
54
93482
                          << std::endl;
55
93482
    d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
56
93480
    assertionsToPreprocess->replaceTrusted(
57
186962
        i, tlsm.apply((*assertionsToPreprocess)[i]));
58
186960
    Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
59
93480
                          << std::endl;
60
  }
61
11322
  return PreprocessingPassResult::NO_CONFLICT;
62
}
63
64
}  // namespace passes
65
}  // namespace preprocessing
66
26676
}  // namespace CVC4