Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Print channels for Eunoia proofs.
11 : : */
12 : :
13 : : #include "proof/eo/eo_print_channel.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/node_algorithm.h"
18 : : #include "expr/skolem_manager.h"
19 : : #include "printer/printer.h"
20 : : #include "proof/trust_id.h"
21 : : #include "rewriter/rewrite_db.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace proof {
25 : :
26 : 3958 : EoPrintChannel::EoPrintChannel() {}
27 : :
28 : 3958 : EoPrintChannel::~EoPrintChannel() {}
29 : :
30 : 1979 : EoPrintChannelOut::EoPrintChannelOut(std::ostream& out,
31 : : const LetBinding* lbind,
32 : : const std::string& tprefix,
33 : 1979 : bool trackWarn)
34 : 1979 : : d_out(out),
35 : 1979 : d_lbind(lbind),
36 : 1979 : d_termLetPrefix(tprefix),
37 : 1979 : d_trackWarn(trackWarn)
38 : : {
39 : 1979 : }
40 : :
41 : 499068 : void EoPrintChannelOut::printNode(TNode n)
42 : : {
43 : 499068 : d_out << " ";
44 : 499068 : printNodeInternal(d_out, n);
45 : 499068 : }
46 : :
47 : 0 : void EoPrintChannelOut::printTypeNode(TypeNode tn)
48 : : {
49 : 0 : d_out << " ";
50 : 0 : printTypeNodeInternal(d_out, tn);
51 : 0 : }
52 : :
53 : 499068 : void EoPrintChannelOut::printAssume(TNode n, size_t i, bool isPush)
54 : : {
55 [ - + ][ - + ]: 499068 : Assert(!n.isNull());
[ - - ]
56 [ + + ]: 499068 : d_out << "(" << (isPush ? "assume-push" : "assume") << " @p" << i;
57 : 499068 : printNode(n);
58 : 499068 : d_out << ")" << std::endl;
59 : 499068 : }
60 : :
61 : 2517063 : void EoPrintChannelOut::printStep(const std::string& rname,
62 : : TNode n,
63 : : size_t i,
64 : : const std::vector<size_t>& premises,
65 : : const std::vector<Node>& args,
66 : : bool isPop)
67 : : {
68 : 2517063 : printStepInternal(rname, n, i, premises, args, isPop, false);
69 : 2517063 : }
70 : :
71 : 2518873 : void EoPrintChannelOut::printStepInternal(const std::string& rname,
72 : : TNode n,
73 : : size_t i,
74 : : const std::vector<size_t>& premises,
75 : : const std::vector<Node>& args,
76 : : bool isPop,
77 : : bool reqPremises)
78 : : {
79 [ + + ]: 2518873 : d_out << "(" << (isPop ? "step-pop" : "step") << " @p" << i;
80 [ + + ]: 2518873 : if (!n.isNull())
81 : : {
82 : 2018232 : d_out << " ";
83 : 2018232 : printNodeInternal(d_out, n);
84 : : }
85 : 2518873 : d_out << " :rule " << rname;
86 : 2518873 : bool firstTime = true;
87 : : // if reqPremises is true, we print even if empty
88 [ + + ][ + + ]: 2518873 : if (!premises.empty() || reqPremises)
[ + + ]
89 : : {
90 : 1943755 : d_out << " :premises (";
91 [ + + ]: 6911194 : for (size_t p : premises)
92 : : {
93 [ + + ]: 4967439 : if (firstTime)
94 : : {
95 : 1942140 : firstTime = false;
96 : : }
97 : : else
98 : : {
99 : 3025299 : d_out << " ";
100 : : }
101 : 4967439 : d_out << "@p" << p;
102 : : }
103 : 1943755 : d_out << ")";
104 : : }
105 [ + + ]: 2518873 : if (!args.empty())
106 : : {
107 : 1269241 : d_out << " :args (";
108 : 1269241 : firstTime = true;
109 [ + + ]: 2830735 : for (const Node& a : args)
110 : : {
111 [ + + ]: 1561494 : if (firstTime)
112 : : {
113 : 1269241 : firstTime = false;
114 : : }
115 : : else
116 : : {
117 : 292253 : d_out << " ";
118 : : }
119 : 1561494 : printNodeInternal(d_out, a);
120 : : }
121 : 1269241 : d_out << ")";
122 : : }
123 : 2518873 : d_out << ")" << std::endl;
124 : 2518873 : }
125 : :
126 : 1810 : void EoPrintChannelOut::printTrustStep(ProofRule r,
127 : : TNode n,
128 : : size_t i,
129 : : const std::vector<size_t>& premises,
130 : : const std::vector<Node>& args,
131 : : TNode nc)
132 : : {
133 [ - + ][ - + ]: 1810 : Assert(!nc.isNull());
[ - - ]
134 [ + - ]: 1810 : if (d_trackWarn)
135 : : {
136 [ + + ]: 1810 : if (d_warnedRules.find(r) == d_warnedRules.end())
137 : : {
138 : 534 : d_out << "; WARNING: add trust step for " << r << std::endl;
139 : 534 : d_warnedRules.insert(r);
140 : : }
141 : : }
142 : 1810 : d_out << "; trust " << r;
143 [ - + ]: 1810 : if (r == ProofRule::DSL_REWRITE)
144 : : {
145 : : ProofRewriteRule di;
146 [ - - ]: 0 : if (rewriter::getRewriteRule(args[0], di))
147 : : {
148 : 0 : d_out << " " << di;
149 : : }
150 : : }
151 [ + + ]: 1810 : else if (r == ProofRule::THEORY_REWRITE)
152 : : {
153 : : ProofRewriteRule di;
154 [ + - ]: 27 : if (rewriter::getRewriteRule(args[0], di))
155 : : {
156 : 27 : d_out << " " << di;
157 : : }
158 : : }
159 [ + + ]: 1783 : else if (r == ProofRule::TRUST)
160 : : {
161 : : TrustId tid;
162 [ + - ]: 1496 : if (getTrustId(args[0], tid))
163 : : {
164 : 1496 : d_out << " " << tid;
165 : : }
166 : : }
167 : 1810 : d_out << std::endl;
168 : : // trust takes a premise-list which must be specified even if empty
169 : 3620 : printStepInternal("trust", n, i, premises, {nc}, false, true);
170 : 1810 : }
171 : :
172 : 4078794 : void EoPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
173 : : {
174 [ + - ]: 4078794 : if (d_lbind)
175 : : {
176 : : // use the toStream with custom letification method
177 : 4078794 : Printer::getPrinter(out)->toStream(out, n, d_lbind, true);
178 : : }
179 : : else
180 : : {
181 : : // just use default print
182 : 0 : Printer::getPrinter(out)->toStream(out, n);
183 : : }
184 : 4078794 : }
185 : :
186 : 0 : void EoPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
187 : : {
188 : 0 : tn.toStream(out);
189 : 0 : }
190 : :
191 : 1979 : EoPrintChannelPre::EoPrintChannelPre(LetBinding* lbind) : d_lbind(lbind) {}
192 : :
193 : 0 : void EoPrintChannelPre::printNode(TNode n)
194 : : {
195 [ - - ]: 0 : if (d_lbind)
196 : : {
197 : 0 : d_lbind->process(n);
198 : : }
199 : 0 : }
200 : :
201 : 0 : void EoPrintChannelPre::printTypeNode(CVC5_UNUSED TypeNode tn)
202 : : {
203 : : // current do nothing
204 : 0 : }
205 : :
206 : 504906 : void EoPrintChannelPre::printAssume(TNode n,
207 : : CVC5_UNUSED size_t i,
208 : : CVC5_UNUSED bool isPush)
209 : : {
210 : 504906 : processInternal(n);
211 : 504906 : }
212 : :
213 : 2559113 : void EoPrintChannelPre::printStep(
214 : : CVC5_UNUSED const std::string& rname,
215 : : TNode n,
216 : : CVC5_UNUSED size_t i,
217 : : CVC5_UNUSED const std::vector<size_t>& premises,
218 : : const std::vector<Node>& args,
219 : : CVC5_UNUSED bool isPop)
220 : : {
221 [ + + ]: 2559113 : if (!n.isNull())
222 : : {
223 : 2052635 : processInternal(n);
224 : : }
225 [ + + ]: 4140583 : for (const Node& a : args)
226 : : {
227 : 1581470 : processInternal(a);
228 : : }
229 : 2559113 : }
230 : :
231 : 1810 : void EoPrintChannelPre::printTrustStep(
232 : : CVC5_UNUSED ProofRule r,
233 : : CVC5_UNUSED TNode n,
234 : : CVC5_UNUSED size_t i,
235 : : CVC5_UNUSED const std::vector<size_t>& premises,
236 : : CVC5_UNUSED const std::vector<Node>& args,
237 : : TNode nc)
238 : : {
239 [ - + ][ - + ]: 1810 : Assert(!nc.isNull());
[ - - ]
240 : 1810 : processInternal(nc);
241 : 1810 : }
242 : :
243 : 4140821 : void EoPrintChannelPre::processInternal(const Node& n)
244 : : {
245 [ + - ]: 4140821 : if (d_lbind)
246 : : {
247 : 4140821 : d_lbind->process(n);
248 : : }
249 : 4140821 : d_keep.insert(n); // probably not necessary
250 : 4140821 : }
251 : :
252 : : } // namespace proof
253 : : } // namespace cvc5::internal
|
