GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/strings_eager_pp.cpp Lines: 19 19 100.0 %
Date: 2021-03-22 Branches: 24 44 54.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strings_eager_pp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 strings eager preprocess utility
13
 **/
14
15
#include "preprocessing/passes/strings_eager_pp.h"
16
17
#include "preprocessing/assertion_pipeline.h"
18
#include "theory/rewriter.h"
19
#include "theory/strings/theory_strings_preprocess.h"
20
21
using namespace CVC4::theory;
22
23
namespace CVC4 {
24
namespace preprocessing {
25
namespace passes {
26
27
8995
StringsEagerPp::StringsEagerPp(PreprocessingPassContext* preprocContext)
28
8995
    : PreprocessingPass(preprocContext, "strings-eager-pp"){};
29
30
34
PreprocessingPassResult StringsEagerPp::applyInternal(
31
    AssertionPipeline* assertionsToPreprocess)
32
{
33
34
  NodeManager* nm = NodeManager::currentNM();
34
68
  theory::strings::SkolemCache skc(false);
35
68
  theory::strings::StringsPreprocess pp(&skc);
36
115
  for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
37
       ++i)
38
  {
39
162
    Node prev = (*assertionsToPreprocess)[i];
40
162
    std::vector<Node> asserts;
41
162
    Node rew = pp.processAssertion(prev, asserts);
42
81
    if (!asserts.empty())
43
    {
44
54
      std::vector<Node> conj;
45
27
      conj.push_back(rew);
46
27
      conj.insert(conj.end(), asserts.begin(), asserts.end());
47
27
      rew = nm->mkAnd(conj);
48
    }
49
81
    if (prev != rew)
50
    {
51
27
      assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew));
52
    }
53
  }
54
55
68
  return PreprocessingPassResult::NO_CONFLICT;
56
}
57
58
}  // namespace passes
59
}  // namespace preprocessing
60
26676
}  // namespace CVC4