1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Print channels for LFSC proofs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/lfsc/lfsc_print_channel.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "proof/lfsc/lfsc_util.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace proof { |
24 |
|
|
25 |
1 |
LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {} |
26 |
16 |
void LfscPrintChannelOut::printNode(TNode n) |
27 |
|
{ |
28 |
16 |
d_out << " "; |
29 |
16 |
printNodeInternal(d_out, n); |
30 |
16 |
} |
31 |
|
|
32 |
|
void LfscPrintChannelOut::printTypeNode(TypeNode tn) |
33 |
|
{ |
34 |
|
d_out << " "; |
35 |
|
printTypeNodeInternal(d_out, tn); |
36 |
|
} |
37 |
|
|
38 |
91 |
void LfscPrintChannelOut::printHole() { d_out << " _ "; } |
39 |
3 |
void LfscPrintChannelOut::printTrust(TNode res, PfRule src) |
40 |
|
{ |
41 |
3 |
d_out << std::endl << "(trust "; |
42 |
3 |
printNodeInternal(d_out, res); |
43 |
3 |
d_out << ") ; from " << src << std::endl; |
44 |
3 |
} |
45 |
|
|
46 |
36 |
void LfscPrintChannelOut::printOpenRule(const ProofNode* pn) |
47 |
|
{ |
48 |
36 |
d_out << std::endl << "("; |
49 |
36 |
printRule(d_out, pn); |
50 |
36 |
} |
51 |
|
|
52 |
6 |
void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr) |
53 |
|
{ |
54 |
6 |
d_out << std::endl << "(" << lr; |
55 |
6 |
} |
56 |
|
|
57 |
37 |
void LfscPrintChannelOut::printCloseRule(size_t nparen) |
58 |
|
{ |
59 |
79 |
for (size_t i = 0; i < nparen; i++) |
60 |
|
{ |
61 |
42 |
d_out << ")"; |
62 |
|
} |
63 |
37 |
} |
64 |
|
|
65 |
11 |
void LfscPrintChannelOut::printProofId(size_t id) |
66 |
|
{ |
67 |
11 |
d_out << " "; |
68 |
11 |
printProofId(d_out, id); |
69 |
11 |
} |
70 |
3 |
void LfscPrintChannelOut::printAssumeId(size_t id) |
71 |
|
{ |
72 |
3 |
d_out << " "; |
73 |
3 |
printAssumeId(d_out, id); |
74 |
3 |
} |
75 |
|
|
76 |
7 |
void LfscPrintChannelOut::printEndLine() { d_out << std::endl; } |
77 |
|
|
78 |
30 |
void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) |
79 |
|
{ |
80 |
|
// due to use of special names in the node converter, we must clean symbols |
81 |
60 |
std::stringstream ss; |
82 |
30 |
n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6); |
83 |
60 |
std::string s = ss.str(); |
84 |
30 |
cleanSymbols(s); |
85 |
30 |
out << s; |
86 |
30 |
} |
87 |
|
|
88 |
6 |
void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) |
89 |
|
{ |
90 |
|
// due to use of special names in the node converter, we must clean symbols |
91 |
12 |
std::stringstream ss; |
92 |
6 |
tn.toStream(ss, Language::LANG_SMTLIB_V2_6); |
93 |
12 |
std::string s = ss.str(); |
94 |
6 |
cleanSymbols(s); |
95 |
6 |
out << s; |
96 |
6 |
} |
97 |
|
|
98 |
36 |
void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn) |
99 |
|
{ |
100 |
36 |
if (pn->getRule() == PfRule::LFSC_RULE) |
101 |
|
{ |
102 |
18 |
const std::vector<Node>& args = pn->getArguments(); |
103 |
18 |
out << getLfscRule(args[0]); |
104 |
36 |
return; |
105 |
|
} |
106 |
|
// Otherwise, convert to lower case |
107 |
36 |
std::stringstream ss; |
108 |
18 |
ss << pn->getRule(); |
109 |
36 |
std::string rname = ss.str(); |
110 |
18 |
std::transform( |
111 |
95 |
rname.begin(), rname.end(), rname.begin(), [](unsigned char c) { |
112 |
95 |
return std::tolower(c); |
113 |
113 |
}); |
114 |
18 |
out << rname; |
115 |
|
} |
116 |
|
|
117 |
8 |
void LfscPrintChannelOut::printId(std::ostream& out, size_t id) |
118 |
|
{ |
119 |
8 |
out << "__t" << id; |
120 |
8 |
} |
121 |
|
|
122 |
11 |
void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id) |
123 |
|
{ |
124 |
11 |
out << "__p" << id; |
125 |
11 |
} |
126 |
|
|
127 |
6 |
void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id) |
128 |
|
{ |
129 |
6 |
out << "__a" << id; |
130 |
6 |
} |
131 |
|
|
132 |
36 |
void LfscPrintChannelOut::cleanSymbols(std::string& s) |
133 |
|
{ |
134 |
36 |
size_t start_pos = 0; |
135 |
36 |
while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos) |
136 |
|
{ |
137 |
|
s.replace(start_pos, 3, "("); |
138 |
|
start_pos += 1; |
139 |
|
} |
140 |
36 |
start_pos = 0; |
141 |
36 |
while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos) |
142 |
|
{ |
143 |
|
s.replace(start_pos, 10, ""); |
144 |
|
} |
145 |
36 |
} |
146 |
|
|
147 |
1 |
LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {} |
148 |
|
|
149 |
16 |
void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); } |
150 |
3 |
void LfscPrintChannelPre::printTrust(TNode res, PfRule src) |
151 |
|
{ |
152 |
3 |
d_lbind.process(res); |
153 |
3 |
} |
154 |
|
|
155 |
36 |
void LfscPrintChannelPre::printOpenRule(const ProofNode* pn) |
156 |
|
{ |
157 |
|
|
158 |
36 |
} |
159 |
|
|
160 |
|
} // namespace proof |
161 |
31125 |
} // namespace cvc5 |