Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Daniel Larraz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 ALF proofs.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__PROOF__ALF__ALF_PRINT_CHANNEL_H
19 : : #define CVC5__PROOF__ALF__ALF_PRINT_CHANNEL_H
20 : :
21 : : #include <iostream>
22 : : #include <map>
23 : :
24 : : #include "expr/node.h"
25 : : #include "printer/let_binding.h"
26 : : #include "proof/proof_node.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace proof {
30 : :
31 : : /**
32 : : * ALF proofs are printed in two phases: the first phase computes the
33 : : * letification of terms in the proof as well as other information that is
34 : : * required for printing the preamble of the proof. The second phase prints the
35 : : * proof to an output stream. This is the base class for these two phases.
36 : : */
37 : : class AlfPrintChannel
38 : : {
39 : : public:
40 : : AlfPrintChannel();
41 : : virtual ~AlfPrintChannel();
42 : : /** Print node n */
43 : : virtual void printNode(TNode n) = 0;
44 : : /** Print type node n */
45 : : virtual void printTypeNode(TypeNode tn) = 0;
46 : : /** Print assume */
47 : : virtual void printAssume(TNode n, size_t i, bool isPush = false) = 0;
48 : : /**
49 : : * Print step
50 : : * @param rname The rule name.
51 : : * @param n The (optional) conclusion.
52 : : * @param i The identifier for the step.
53 : : * @param premises The list of identifiers of premises
54 : : * @param args The arguments of the proof rule.
55 : : * @param isPop Whether this is a step-pop command.
56 : : */
57 : : virtual void printStep(const std::string& rname,
58 : : TNode n,
59 : : size_t i,
60 : : const std::vector<size_t>& premises,
61 : : const std::vector<Node>& args,
62 : : bool isPop = false) = 0;
63 : : /** Print trust step */
64 : : virtual void printTrustStep(ProofRule r,
65 : : TNode n,
66 : : size_t i,
67 : : const std::vector<size_t>& premises,
68 : : const std::vector<Node>& args,
69 : : TNode conc) = 0;
70 : : };
71 : :
72 : : /** Prints the proof to output stream d_out */
73 : : class AlfPrintChannelOut : public AlfPrintChannel
74 : : {
75 : : public:
76 : : AlfPrintChannelOut(std::ostream& out,
77 : : const LetBinding* lbind,
78 : : const std::string& tprefix,
79 : : bool trackWarn);
80 : : void printNode(TNode n) override;
81 : : void printTypeNode(TypeNode tn) override;
82 : : void printAssume(TNode n, size_t i, bool isPush) override;
83 : : void printStep(const std::string& rname,
84 : : TNode n,
85 : : size_t i,
86 : : const std::vector<size_t>& premises,
87 : : const std::vector<Node>& args,
88 : : bool isPop = false) override;
89 : : void printTrustStep(ProofRule r,
90 : : TNode n,
91 : : size_t i,
92 : : const std::vector<size_t>& premises,
93 : : const std::vector<Node>& args,
94 : : TNode conc) override;
95 : :
96 : : /**
97 : : * Print node to stream in the expected format of ALF.
98 : : */
99 : : void printNodeInternal(std::ostream& out, Node n);
100 : : /**
101 : : * Print type node to stream in the expected format of ALF.
102 : : */
103 : : void printTypeNodeInternal(std::ostream& out, TypeNode tn);
104 : 1620 : std::ostream& getOStream() { return d_out; }
105 : :
106 : : private:
107 : : /**
108 : : * Helper for print steps. We set reqPremises to true if we require printing
109 : : * premises even if empty.
110 : : */
111 : : void printStepInternal(const std::string& rname,
112 : : TNode n,
113 : : size_t i,
114 : : const std::vector<size_t>& premises,
115 : : const std::vector<Node>& args,
116 : : bool isPop,
117 : : bool reqPremises);
118 : : /** The output stream */
119 : : std::ostream& d_out;
120 : : /** The let binding */
121 : : const LetBinding* d_lbind;
122 : : /** term prefix */
123 : : std::string d_termLetPrefix;
124 : : /**
125 : : * The set of ProofRule that we have output a warning about, i.e. the rules
126 : : * associated with trusted steps.
127 : : */
128 : : std::unordered_set<ProofRule> d_warnedRules;
129 : : /** Are we tracking warned rules? */
130 : : bool d_trackWarn;
131 : : };
132 : :
133 : : /**
134 : : * Run on the proof before it is printed, and does two preparation steps:
135 : : * - Computes the letification of nodes that appear in the proof.
136 : : * - Computes the set of variables that appear in the proof.
137 : : */
138 : : class AlfPrintChannelPre : public AlfPrintChannel
139 : : {
140 : : public:
141 : : AlfPrintChannelPre(LetBinding* lbind);
142 : : void printNode(TNode n) override;
143 : : void printTypeNode(TypeNode tn) override;
144 : : void printAssume(TNode n, size_t i, bool isPush) override;
145 : : void printStep(const std::string& rname,
146 : : TNode n,
147 : : size_t i,
148 : : const std::vector<size_t>& premises,
149 : : const std::vector<Node>& args,
150 : : bool isPop = false) override;
151 : : void printTrustStep(ProofRule r,
152 : : TNode n,
153 : : size_t i,
154 : : const std::vector<size_t>& premises,
155 : : const std::vector<Node>& args,
156 : : TNode conc) override;
157 : :
158 : : private:
159 : : /** The let binding */
160 : : LetBinding* d_lbind;
161 : : /** For computing free variables */
162 : : std::unordered_set<Node> d_keep;
163 : : /** Process that we will print node n in the final proof */
164 : : void processInternal(const Node& n);
165 : : };
166 : :
167 : : } // namespace proof
168 : : } // namespace cvc5::internal
169 : :
170 : : #endif
|
