GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node_to_sexpr.cpp Lines: 65 82 79.3 %
Date: 2021-03-23 Branches: 96 288 33.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node_to_sexpr.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 to s-expression
13
 **/
14
15
#include "expr/proof_node_to_sexpr.h"
16
17
#include <iostream>
18
#include <sstream>
19
20
#include "expr/proof_node.h"
21
#include "options/proof_options.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
27
31366
ProofNodeToSExpr::ProofNodeToSExpr()
28
{
29
31366
  NodeManager* nm = NodeManager::currentNM();
30
62732
  std::vector<TypeNode> types;
31
31366
  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->mkSExprType(types));
32
31366
  d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types));
33
31366
}
34
35
31366
Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
36
{
37
31366
  NodeManager* nm = NodeManager::currentNM();
38
31366
  std::map<const ProofNode*, Node>::iterator it;
39
62732
  std::vector<const ProofNode*> visit;
40
62732
  std::vector<const ProofNode*> traversing;
41
  const ProofNode* cur;
42
31366
  visit.push_back(pn);
43
368016
  do
44
  {
45
399382
    cur = visit.back();
46
399382
    visit.pop_back();
47
399382
    it = d_pnMap.find(cur);
48
49
399382
    if (it == d_pnMap.end())
50
    {
51
199691
      d_pnMap[cur] = Node::null();
52
199691
      traversing.push_back(cur);
53
199691
      visit.push_back(cur);
54
199691
      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
55
368016
      for (const std::shared_ptr<ProofNode>& cp : pc)
56
      {
57
504975
        if (std::find(traversing.begin(), traversing.end(), cp.get())
58
504975
            != traversing.end())
59
        {
60
          Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
61
                         "--proof-eager-checking)"
62
                      << std::endl;
63
          return Node::null();
64
        }
65
168325
        visit.push_back(cp.get());
66
      }
67
    }
68
199691
    else if (it->second.isNull())
69
    {
70
199691
      Assert(!traversing.empty());
71
199691
      traversing.pop_back();
72
399382
      std::vector<Node> children;
73
      // add proof rule
74
199691
      children.push_back(getOrMkPfRuleVariable(cur->getRule()));
75
399382
      if (options::proofPrintConclusion())
76
      {
77
        children.push_back(d_conclusionMarker);
78
        children.push_back(cur->getResult());
79
      }
80
199691
      const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
81
368016
      for (const std::shared_ptr<ProofNode>& cp : pc)
82
      {
83
168325
        it = d_pnMap.find(cp.get());
84
168325
        Assert(it != d_pnMap.end());
85
168325
        Assert(!it->second.isNull());
86
168325
        children.push_back(it->second);
87
      }
88
      // add arguments
89
199691
      const std::vector<Node>& args = cur->getArguments();
90
199691
      if (!args.empty())
91
      {
92
183321
        children.push_back(d_argsMarker);
93
        // needed to ensure builtin operators are not treated as operators
94
        // this can be the case for CONG where d_args may contain a builtin
95
        // operator
96
366642
        std::vector<Node> argsSafe;
97
398020
        for (const Node& a : args)
98
        {
99
429398
          Node av = a;
100
429398
          if (a.getNumChildren() == 0
101
429398
              && NodeManager::operatorToKind(a) != UNDEFINED_KIND)
102
          {
103
            av = getOrMkNodeVariable(a);
104
          }
105
214699
          argsSafe.push_back(av);
106
        }
107
366642
        Node argsC = nm->mkNode(SEXPR, argsSafe);
108
183321
        children.push_back(argsC);
109
      }
110
199691
      d_pnMap[cur] = nm->mkNode(SEXPR, children);
111
    }
112
399382
  } while (!visit.empty());
113
31366
  Assert(d_pnMap.find(pn) != d_pnMap.end());
114
31366
  Assert(!d_pnMap.find(pn)->second.isNull());
115
31366
  return d_pnMap[pn];
116
}
117
118
199691
Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
119
{
120
199691
  std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
121
199691
  if (it != d_pfrMap.end())
122
  {
123
57558
    return it->second;
124
  }
125
284266
  std::stringstream ss;
126
142133
  ss << r;
127
142133
  NodeManager* nm = NodeManager::currentNM();
128
284266
  std::vector<TypeNode> types;
129
284266
  Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
130
142133
  d_pfrMap[r] = var;
131
142133
  return var;
132
}
133
134
Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
135
{
136
  std::map<Node, Node>::iterator it = d_nodeMap.find(n);
137
  if (it != d_nodeMap.end())
138
  {
139
    return it->second;
140
  }
141
  std::stringstream ss;
142
  ss << n;
143
  NodeManager* nm = NodeManager::currentNM();
144
  std::vector<TypeNode> types;
145
  Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
146
  d_nodeMap[n] = var;
147
  return var;
148
}
149
150
226376
}  // namespace CVC4