blob: 2dbb2a873b0bacb833e397872707744d0c61a248 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/********************* */
/*! \file proof_node_to_sexpr.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of proof node to s-expression
**/
#include "expr/proof_node_to_sexpr.h"
#include <iostream>
using namespace CVC4::kind;
namespace CVC4 {
ProofNodeToSExpr::ProofNodeToSExpr()
{
NodeManager* nm = NodeManager::currentNM();
std::vector<TypeNode> types;
d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types));
}
Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
{
NodeManager* nm = NodeManager::currentNM();
std::map<const ProofNode*, Node>::iterator it;
std::vector<const ProofNode*> visit;
std::vector<const ProofNode*> traversing;
const ProofNode* cur;
visit.push_back(pn);
do
{
cur = visit.back();
visit.pop_back();
it = d_pnMap.find(cur);
if (it == d_pnMap.end())
{
d_pnMap[cur] = Node::null();
traversing.push_back(cur);
visit.push_back(cur);
const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
for (const std::shared_ptr<ProofNode>& cp : pc)
{
if (std::find(traversing.begin(), traversing.end(), cp.get())
!= traversing.end())
{
Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
"--proof-new-eager-checking)"
<< std::endl;
return Node::null();
}
visit.push_back(cp.get());
}
}
else if (it->second.isNull())
{
Assert(!traversing.empty());
traversing.pop_back();
std::vector<Node> children;
// add proof rule
children.push_back(getOrMkPfRuleVariable(cur->getRule()));
const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
for (const std::shared_ptr<ProofNode>& cp : pc)
{
it = d_pnMap.find(cp.get());
Assert(it != d_pnMap.end());
Assert(!it->second.isNull());
children.push_back(it->second);
}
// add arguments
const std::vector<Node>& args = cur->getArguments();
if (!args.empty())
{
children.push_back(d_argsMarker);
// needed to ensure builtin operators are not treated as operators
// this can be the case for CONG where d_args may contain a builtin
// operator
std::vector<Node> argsSafe;
for (const Node& a : args)
{
Node av = a;
if (a.getNumChildren() == 0
&& NodeManager::operatorToKind(a) != UNDEFINED_KIND)
{
av = getOrMkNodeVariable(a);
}
argsSafe.push_back(av);
}
Node argsC = nm->mkNode(SEXPR, argsSafe);
children.push_back(argsC);
}
d_pnMap[cur] = nm->mkNode(SEXPR, children);
}
} while (!visit.empty());
Assert(d_pnMap.find(pn) != d_pnMap.end());
Assert(!d_pnMap.find(pn)->second.isNull());
return d_pnMap[pn];
}
Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r)
{
std::map<PfRule, Node>::iterator it = d_pfrMap.find(r);
if (it != d_pfrMap.end())
{
return it->second;
}
std::stringstream ss;
ss << r;
NodeManager* nm = NodeManager::currentNM();
std::vector<TypeNode> types;
Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
d_pfrMap[r] = var;
return var;
}
Node ProofNodeToSExpr::getOrMkNodeVariable(Node n)
{
std::map<Node, Node>::iterator it = d_nodeMap.find(n);
if (it != d_nodeMap.end())
{
return it->second;
}
std::stringstream ss;
ss << n;
NodeManager* nm = NodeManager::currentNM();
std::vector<TypeNode> types;
Node var = nm->mkBoundVar(ss.str(), nm->mkSExprType(types));
d_nodeMap[n] = var;
return var;
}
} // namespace CVC4
|
