GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node_algorithm.cpp Lines: 54 75 72.0 %
Date: 2021-03-22 Branches: 59 162 36.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node_algorithm.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 Implementation of proof node algorithm utilities
13
 **/
14
15
#include "expr/proof_node_algorithm.h"
16
17
#include "expr/proof_node.h"
18
19
namespace CVC4 {
20
namespace expr {
21
22
95375
void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
23
{
24
190750
  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
25
  std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
26
190750
      pn->getRule(), pn->getChildren(), pn->getArguments());
27
95375
  getFreeAssumptionsMap(spn, amap);
28
70427
  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
29
95375
       amap)
30
  {
31
70427
    assump.push_back(p.first);
32
  }
33
95375
}
34
35
327007
void getFreeAssumptionsMap(
36
    std::shared_ptr<ProofNode> pn,
37
    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
38
{
39
  // proof should not be cyclic
40
  // visited set false after preorder traversal, true after postorder traversal
41
654014
  std::unordered_map<ProofNode*, bool> visited;
42
327007
  std::unordered_map<ProofNode*, bool>::iterator it;
43
654014
  std::vector<std::shared_ptr<ProofNode>> visit;
44
654014
  std::vector<std::shared_ptr<ProofNode>> traversing;
45
  // Maps a bound assumption to the number of bindings it is under
46
  // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
47
  // (ASSUME x), and x would be mapped to 1.
48
  //
49
  // This map is used to track which nodes are in scope while traversing the
50
  // DAG. The in-scope assumptions are keys in the map. They're removed when
51
  // their binding count drops to zero. Let's annotate the above example to
52
  // serve as an illustration:
53
  //
54
  //   (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
55
  //
56
  // This is how the map changes during the traversal:
57
  //   after  previsiting SCOPE0: { y: 1 }
58
  //   after  previsiting SCOPE1: { y: 2, x: 1 }
59
  //   at                 ASSUME: { y: 2, x: 1 } (so x is in scope!)
60
  //   after postvisiting SCOPE1: { y: 1 }
61
  //   after postvisiting SCOPE2: {}
62
  //
63
654014
  std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
64
654014
  std::shared_ptr<ProofNode> cur;
65
327007
  visit.push_back(pn);
66
19634720
  do
67
  {
68
19961727
    cur = visit.back();
69
19961727
    visit.pop_back();
70
19961727
    it = visited.find(cur.get());
71
19961727
    const std::vector<Node>& cargs = cur->getArguments();
72
19961727
    if (it == visited.end())
73
    {
74
10618695
      PfRule id = cur->getRule();
75
10618695
      if (id == PfRule::ASSUME)
76
      {
77
3673139
        visited[cur.get()] = true;
78
3673139
        Assert(cargs.size() == 1);
79
7346278
        Node f = cargs[0];
80
3673139
        if (!scopeDepth.count(f))
81
        {
82
2360020
          amap[f].push_back(cur);
83
        }
84
      }
85
      else
86
      {
87
6945556
        if (id == PfRule::SCOPE)
88
        {
89
          // mark that its arguments are bound in the current scope
90
1109106
          for (const Node& a : cargs)
91
          {
92
915709
            scopeDepth[a] += 1;
93
          }
94
          // will need to unbind the variables below
95
        }
96
        // The following loop cannot be merged with the loop above because the
97
        // same subproof
98
6945556
        visited[cur.get()] = false;
99
6945556
        visit.push_back(cur);
100
6945556
        traversing.push_back(cur);
101
6945556
        const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
102
19634720
        for (const std::shared_ptr<ProofNode>& cp : cs)
103
        {
104
38067492
          if (std::find(traversing.begin(), traversing.end(), cp)
105
38067492
              != traversing.end())
106
          {
107
            Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
108
                           "--proof-eager-checking)"
109
                        << std::endl;
110
          }
111
12689164
          visit.push_back(cp);
112
        }
113
      }
114
    }
115
9343032
    else if (!it->second)
116
    {
117
6945556
      Assert(!traversing.empty());
118
6945556
      traversing.pop_back();
119
6945556
      visited[cur.get()] = true;
120
6945556
      if (cur->getRule() == PfRule::SCOPE)
121
      {
122
        // unbind its assumptions
123
1109106
        for (const Node& a : cargs)
124
        {
125
915709
          auto scopeCt = scopeDepth.find(a);
126
915709
          Assert(scopeCt != scopeDepth.end());
127
915709
          scopeCt->second -= 1;
128
915709
          if (scopeCt->second == 0)
129
          {
130
829271
            scopeDepth.erase(scopeCt);
131
          }
132
        }
133
      }
134
    }
135
19961727
  } while (!visit.empty());
136
327007
}
137
138
bool containsSubproof(ProofNode* pn, ProofNode* pnc)
139
{
140
  std::unordered_set<const ProofNode*> visited;
141
  return containsSubproof(pn, pnc, visited);
142
}
143
144
bool containsSubproof(ProofNode* pn,
145
                      ProofNode* pnc,
146
                      std::unordered_set<const ProofNode*>& visited)
147
{
148
  std::unordered_map<const ProofNode*, bool>::iterator it;
149
  std::vector<const ProofNode*> visit;
150
  visit.push_back(pn);
151
  const ProofNode* cur;
152
  while (!visit.empty())
153
  {
154
    cur = visit.back();
155
    visit.pop_back();
156
    if (visited.find(cur) == visited.end())
157
    {
158
      visited.insert(cur);
159
      if (cur == pnc)
160
      {
161
        return true;
162
      }
163
      const std::vector<std::shared_ptr<ProofNode>>& children =
164
          cur->getChildren();
165
      for (const std::shared_ptr<ProofNode>& cp : children)
166
      {
167
        visit.push_back(cp.get());
168
      }
169
    }
170
  }
171
  return false;
172
}
173
174
}  // namespace expr
175
26676
}  // namespace CVC4