GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/nl_ext_purify.cpp Lines: 55 56 98.2 %
Date: 2021-03-22 Branches: 107 190 56.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file nl_ext_purify.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, 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 The NlExtPurify preprocessing pass
13
 **
14
 ** Purifies non-linear terms
15
 **/
16
17
#include "preprocessing/passes/nl_ext_purify.h"
18
19
#include "preprocessing/assertion_pipeline.h"
20
#include "theory/rewriter.h"
21
22
namespace CVC4 {
23
namespace preprocessing {
24
namespace passes {
25
26
using namespace std;
27
using namespace CVC4::theory;
28
29
410
Node NlExtPurify::purifyNlTerms(TNode n,
30
                                NodeMap& cache,
31
                                NodeMap& bcache,
32
                                std::vector<Node>& var_eq,
33
                                bool beneathMult)
34
{
35
410
  if (beneathMult)
36
  {
37
64
    NodeMap::iterator find = bcache.find(n);
38
64
    if (find != bcache.end())
39
    {
40
62
      return (*find).second;
41
    }
42
  }
43
  else
44
  {
45
346
    NodeMap::iterator find = cache.find(n);
46
346
    if (find != cache.end())
47
    {
48
129
      return (*find).second;
49
    }
50
  }
51
219
  if (n.isClosure())
52
  {
53
    // don't traverse quantified formulas
54
3
    return n;
55
  }
56
432
  Node ret = n;
57
216
  if (n.getNumChildren() > 0)
58
  {
59
122
    if (beneathMult
60
122
        && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
61
    {
62
      // don't do it if it rewrites to a constant
63
4
      Node nr = Rewriter::rewrite(n);
64
2
      if (nr.isConst())
65
      {
66
        // return the rewritten constant
67
        ret = nr;
68
      }
69
      else
70
      {
71
        // new variable
72
6
        ret = NodeManager::currentNM()->mkSkolem(
73
            "__purifyNl_var",
74
4
            n.getType(),
75
            "Variable introduced in purifyNl pass");
76
4
        Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
77
2
        var_eq.push_back(np.eqNode(ret));
78
4
        Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
79
2
                               << std::endl;
80
      }
81
    }
82
    else
83
    {
84
120
      bool beneathMultNew = beneathMult || n.getKind() == kind::MULT;
85
120
      bool childChanged = false;
86
240
      std::vector<Node> children;
87
480
      for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
88
      {
89
720
        Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew);
90
360
        childChanged = childChanged || nc != n[i];
91
360
        children.push_back(nc);
92
      }
93
120
      if (childChanged)
94
      {
95
10
        ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
96
      }
97
    }
98
  }
99
216
  if (beneathMult)
100
  {
101
2
    bcache[n] = ret;
102
  }
103
  else
104
  {
105
214
    cache[n] = ret;
106
  }
107
216
  return ret;
108
}
109
110
8995
NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext)
111
8995
    : PreprocessingPass(preprocContext, "nl-ext-purify"){};
112
113
9
PreprocessingPassResult NlExtPurify::applyInternal(
114
    AssertionPipeline* assertionsToPreprocess)
115
{
116
18
  unordered_map<Node, Node, NodeHashFunction> cache;
117
18
  unordered_map<Node, Node, NodeHashFunction> bcache;
118
18
  std::vector<Node> var_eq;
119
9
  unsigned size = assertionsToPreprocess->size();
120
57
  for (unsigned i = 0; i < size; ++i)
121
  {
122
96
    Node a = (*assertionsToPreprocess)[i];
123
96
    Node ap = purifyNlTerms(a, cache, bcache, var_eq);
124
48
    if (a != ap)
125
    {
126
2
      assertionsToPreprocess->replace(i, ap);
127
4
      Trace("nl-ext-purify")
128
2
          << "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n";
129
    }
130
  }
131
9
  if (!var_eq.empty())
132
  {
133
2
    unsigned lastIndex = size - 1;
134
4
    Node veq = NodeManager::currentNM()->mkAnd(var_eq);
135
2
    assertionsToPreprocess->conjoin(lastIndex, veq);
136
  }
137
18
  return PreprocessingPassResult::NO_CONFLICT;
138
}
139
140
141
}  // namespace passes
142
}  // namespace preprocessing
143
26676
}  // namespace CVC4