GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/quantifiers_preprocess.cpp Lines: 15 15 100.0 %
Date: 2021-03-22 Branches: 26 50 52.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_preprocess.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Caleb Donovick, Andrew Reynolds, Gereon Kremer
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 Remove rewrite rules, apply pre-skolemization to existential
13
 *quantifiers
14
 **
15
 **
16
 ** Calls the quantifier rewriter, removing rewrite rules and applying
17
 ** pre-skolemization to existential quantifiers
18
 **/
19
20
#include "preprocessing/passes/quantifiers_preprocess.h"
21
22
#include "base/output.h"
23
#include "preprocessing/assertion_pipeline.h"
24
#include "theory/quantifiers/quantifiers_rewriter.h"
25
#include "theory/rewriter.h"
26
27
namespace CVC4 {
28
namespace preprocessing {
29
namespace passes {
30
31
using namespace std;
32
using namespace CVC4::theory;
33
34
8995
QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext)
35
8995
    : PreprocessingPass(preprocContext, "quantifiers-preprocess"){};
36
37
6430
PreprocessingPassResult QuantifiersPreprocess::applyInternal(
38
    AssertionPipeline* assertionsToPreprocess)
39
{
40
6430
  size_t size = assertionsToPreprocess->size();
41
49684
  for (size_t i = 0; i < size; ++i)
42
  {
43
86508
    Node prev = (*assertionsToPreprocess)[i];
44
86508
    TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev);
45
43254
    if (!trn.isNull())
46
    {
47
26
      Node next = trn.getNode();
48
13
      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
49
13
      Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
50
26
      Trace("quantifiers-preprocess")
51
13
          << "   ...got " << (*assertionsToPreprocess)[i] << endl;
52
    }
53
  }
54
55
6430
  return PreprocessingPassResult::NO_CONFLICT;
56
}
57
58
59
}  // namespace passes
60
}  // namespace preprocessing
61
26676
}  // namespace CVC4