GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/extended_rewriter_pass.cpp Lines: 9 9 100.0 %
Date: 2021-03-23 Branches: 13 28 46.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file extended_rewriter_pass.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa
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 ExtRewPre preprocessing pass
13
 **
14
 ** Applies the extended rewriter to assertions
15
 **/
16
17
#include "preprocessing/passes/extended_rewriter_pass.h"
18
19
#include "options/smt_options.h"
20
#include "preprocessing/assertion_pipeline.h"
21
#include "preprocessing/preprocessing_pass_context.h"
22
#include "theory/quantifiers/extended_rewrite.h"
23
24
namespace CVC4 {
25
namespace preprocessing {
26
namespace passes {
27
28
8997
ExtRewPre::ExtRewPre(PreprocessingPassContext* preprocContext)
29
8997
    : PreprocessingPass(preprocContext, "ext-rew-pre"){};
30
31
22
PreprocessingPassResult ExtRewPre::applyInternal(
32
    AssertionPipeline* assertionsToPreprocess)
33
{
34
80
  theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
35
70
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
36
  {
37
48
    assertionsToPreprocess->replace(
38
96
        i, extr.extendedRewrite((*assertionsToPreprocess)[i]));
39
  }
40
44
  return PreprocessingPassResult::NO_CONFLICT;
41
}
42
43
44
}  // namespace passes
45
}  // namespace preprocessing
46
26721
}  // namespace CVC4