GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/foreign_theory_rewrite.cpp Lines: 52 53 98.1 %
Date: 2021-03-22 Branches: 92 244 37.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file foreign_theory_rewrite.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar
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 foreign_theory_rewrite preprocessing pass
13
 **
14
 ** Simplifies nodes of one theory using rewrites from another.
15
 **/
16
17
#include "preprocessing/passes/foreign_theory_rewrite.h"
18
19
#include "expr/node_traversal.h"
20
#include "preprocessing/assertion_pipeline.h"
21
#include "preprocessing/preprocessing_pass_context.h"
22
#include "theory/rewriter.h"
23
#include "theory/strings/arith_entail.h"
24
25
namespace CVC4 {
26
namespace preprocessing {
27
namespace passes {
28
29
using namespace CVC4::theory;
30
8995
ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
31
    : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
32
8995
      d_cache(preprocContext->getUserContext()){};
33
34
4
Node ForeignTheoryRewrite::simplify(Node n)
35
{
36
8
  std::vector<Node> toVisit;
37
4
  n = Rewriter::rewrite(n);
38
4
  toVisit.push_back(n);
39
  // traverse n and rewrite until fixpoint
40
84
  while (!toVisit.empty())
41
  {
42
80
    Node current = toVisit.back();
43
    // split according to three cases:
44
    // 1. We have not visited this node
45
    // 2. We visited it but did not process it
46
    // 3. We already processed and cached the node
47
40
    if (d_cache.find(current) == d_cache.end())
48
    {
49
      // current is seen for the first time.
50
      // mark it by assigning a null node
51
      // and add its children to toVisit
52
16
      d_cache[current] = Node();
53
16
      toVisit.insert(toVisit.end(), current.begin(), current.end());
54
    }
55
24
    else if (d_cache[current].get().isNull())
56
    {
57
      // current was seen but was not processed.
58
      // (a) remove from toVisit
59
16
      toVisit.pop_back();
60
      // (b) Reconstruct it with processed children
61
32
      std::vector<Node> processedChildren;
62
32
      for (Node child : current)
63
      {
64
16
        Assert(d_cache.find(child) != d_cache.end());
65
16
        Assert(!d_cache[child].get().isNull());
66
16
        processedChildren.push_back(d_cache[child]);
67
      }
68
32
      Node reconstruction = reconstructNode(current, processedChildren);
69
      // (c) process the node and store the result in the cache
70
32
      Node result = foreignRewrite(reconstruction);
71
16
      d_cache[current] = result;
72
      // (d) add the result to toVisit, unless it is the same as current
73
16
      if (current != result)
74
      {
75
4
        toVisit.push_back(result);
76
      }
77
    }
78
    else
79
    {
80
      // current was already processed
81
      // remove from toVisit and skip
82
8
      toVisit.pop_back();
83
    }
84
  }
85
8
  return d_cache[n];
86
}
87
88
20
Node ForeignTheoryRewrite::foreignRewrite(Node n)
89
{
90
  // n is a rewritten node, and so GT, LT, LEQ
91
  // should have been eliminated
92
20
  Assert(n.getKind() != kind::GT);
93
20
  Assert(n.getKind() != kind::LT);
94
20
  Assert(n.getKind() != kind::LEQ);
95
  // apply rewrites according to the structure of n
96
20
  if (n.getKind() == kind::GEQ)
97
  {
98
6
    return rewriteStringsGeq(n);
99
  }
100
14
  return n;
101
}
102
103
6
Node ForeignTheoryRewrite::rewriteStringsGeq(Node n)
104
{
105
  // check if the node can be simplified to true
106
6
  if (theory::strings::ArithEntail::check(n[0], n[1], false))
107
  {
108
4
    return NodeManager::currentNM()->mkConst(true);
109
  }
110
2
  return n;
111
}
112
113
16
Node ForeignTheoryRewrite::reconstructNode(Node originalNode,
114
                                           std::vector<Node> newChildren)
115
{
116
  // Nodes with no children are reconstructed to themselves
117
16
  if (originalNode.getNumChildren() == 0)
118
  {
119
6
    Assert(newChildren.empty());
120
6
    return originalNode;
121
  }
122
  // re-build the node with the same kind and new children
123
10
  kind::Kind_t k = originalNode.getKind();
124
20
  NodeBuilder<> builder(k);
125
  // special case for parameterized nodes
126
10
  if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
127
  {
128
    builder << originalNode.getOperator();
129
  }
130
  // reconstruction
131
26
  for (Node child : newChildren)
132
  {
133
16
    builder << child;
134
  }
135
10
  return builder.constructNode();
136
}
137
138
2
PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
139
    AssertionPipeline* assertionsToPreprocess)
140
{
141
6
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
142
  {
143
4
    assertionsToPreprocess->replace(
144
8
        i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i])));
145
  }
146
147
2
  return PreprocessingPassResult::NO_CONFLICT;
148
}
149
150
}  // namespace passes
151
}  // namespace preprocessing
152
26676
}  // namespace CVC4