GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/sep_skolem_emp.cpp Lines: 47 49 95.9 %
Date: 2021-03-23 Branches: 98 194 50.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sep_skolem_emp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, 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 sep-pre-skolem-emp preprocessing pass
13
 **
14
 **/
15
16
#include "preprocessing/passes/sep_skolem_emp.h"
17
18
#include <string>
19
#include <unordered_map>
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "preprocessing/assertion_pipeline.h"
24
#include "theory/quantifiers/quant_util.h"
25
#include "theory/rewriter.h"
26
#include "theory/theory.h"
27
28
namespace CVC4 {
29
namespace preprocessing {
30
namespace passes {
31
32
using namespace std;
33
using namespace CVC4::theory;
34
35
namespace {
36
37
3
Node preSkolemEmp(Node n,
38
                         bool pol,
39
                         std::map<bool, std::map<Node, Node>>& visited)
40
{
41
3
  std::map<Node, Node>::iterator it = visited[pol].find(n);
42
3
  if (it == visited[pol].end())
43
  {
44
6
    Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
45
3
                            << std::endl;
46
6
    Node ret = n;
47
3
    if (n.getKind() == kind::SEP_EMP)
48
    {
49
1
      if (!pol)
50
      {
51
2
        TypeNode tnx = n[0].getType();
52
2
        TypeNode tny = n[1].getType();
53
        Node x = NodeManager::currentNM()->mkSkolem(
54
2
            "ex", tnx, "skolem location for negated emp");
55
        Node y = NodeManager::currentNM()->mkSkolem(
56
2
            "ey", tny, "skolem data for negated emp");
57
        return NodeManager::currentNM()
58
5
            ->mkNode(kind::SEP_STAR,
59
2
                     NodeManager::currentNM()->mkNode(kind::SEP_PTO, x, y),
60
2
                     NodeManager::currentNM()->mkConst(true))
61
1
            .negate();
62
      }
63
    }
64
2
    else if (n.getKind() != kind::FORALL && n.getNumChildren() > 0)
65
    {
66
1
      std::vector<Node> children;
67
1
      bool childChanged = false;
68
1
      if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
69
      {
70
        children.push_back(n.getOperator());
71
      }
72
2
      for (unsigned i = 0; i < n.getNumChildren(); i++)
73
      {
74
        bool newPol, newHasPol;
75
1
        QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol);
76
2
        Node nc = n[i];
77
1
        if (newHasPol)
78
        {
79
1
          nc = preSkolemEmp(n[i], newPol, visited);
80
1
          childChanged = childChanged || nc != n[i];
81
        }
82
1
        children.push_back(nc);
83
      }
84
1
      if (childChanged)
85
      {
86
1
        return NodeManager::currentNM()->mkNode(n.getKind(), children);
87
      }
88
    }
89
1
    visited[pol][n] = ret;
90
1
    return n;
91
  }
92
  else
93
  {
94
    return it->second;
95
  }
96
}
97
98
}  // namespace
99
100
8997
SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
101
8997
    : PreprocessingPass(preprocContext, "sep-skolem-emp"){};
102
103
1
PreprocessingPassResult SepSkolemEmp::applyInternal(
104
    AssertionPipeline* assertionsToPreprocess)
105
{
106
2
  std::map<bool, std::map<Node, Node>> visited;
107
3
  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
108
  {
109
4
    Node prev = (*assertionsToPreprocess)[i];
110
2
    bool pol = true;
111
4
    Node next = preSkolemEmp(prev, pol, visited);
112
2
    if (next != prev)
113
    {
114
1
      assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
115
1
      Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
116
2
      Trace("sep-preprocess") << "   ...got " << (*assertionsToPreprocess)[i]
117
1
                              << endl;
118
    }
119
2
    visited.clear();
120
  }
121
2
  return PreprocessingPassResult::NO_CONFLICT;
122
}
123
124
125
}  // namespace passes
126
}  // namespace preprocessing
127
26685
}  // namespace CVC4