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 "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H |
19 |
|
#define CVC4__PROOF__LFSC__LFSC_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/lfsc/lfsc_util.h" |
27 |
|
#include "proof/proof_node.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace proof { |
31 |
|
|
32 |
|
/** |
33 |
|
* LFSC proofs are printed in two phases: the first phase computes the |
34 |
|
* letification of terms in the proof as well as other information that is |
35 |
|
* required for printing the preamble of the proof. The second phase prints the |
36 |
|
* proof to an output stream. This is the base class for these two phases. |
37 |
|
*/ |
38 |
|
class LfscPrintChannel |
39 |
|
{ |
40 |
|
public: |
41 |
|
LfscPrintChannel() {} |
42 |
|
virtual ~LfscPrintChannel() {} |
43 |
|
/** Print node n */ |
44 |
|
virtual void printNode(TNode n) {} |
45 |
|
/** Print type node n */ |
46 |
|
virtual void printTypeNode(TypeNode tn) {} |
47 |
|
/** Print a hole */ |
48 |
|
virtual void printHole() {} |
49 |
|
/** |
50 |
|
* Print an application of the trusting the result res, whose source is the |
51 |
|
* given proof rule. |
52 |
|
*/ |
53 |
|
virtual void printTrust(TNode res, PfRule src) {} |
54 |
|
/** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */ |
55 |
|
virtual void printOpenRule(const ProofNode* pn) {} |
56 |
|
/** Print the opening of LFSC rule lr, e.g. "(cong " */ |
57 |
|
virtual void printOpenLfscRule(LfscRule lr) {} |
58 |
|
/** Print the closing of # nparen proof rules */ |
59 |
|
virtual void printCloseRule(size_t nparen = 1) {} |
60 |
|
/** Print a letified proof with the given identifier */ |
61 |
|
virtual void printProofId(size_t id) {} |
62 |
|
/** Print a proof assumption with the given identifier */ |
63 |
|
virtual void printAssumeId(size_t id) {} |
64 |
|
/** Print an end line */ |
65 |
|
virtual void printEndLine() {} |
66 |
|
}; |
67 |
|
|
68 |
|
/** Prints the proof to output stream d_out */ |
69 |
|
class LfscPrintChannelOut : public LfscPrintChannel |
70 |
|
{ |
71 |
|
public: |
72 |
|
LfscPrintChannelOut(std::ostream& out); |
73 |
|
void printNode(TNode n) override; |
74 |
|
void printTypeNode(TypeNode tn) override; |
75 |
|
void printHole() override; |
76 |
|
void printTrust(TNode res, PfRule src) override; |
77 |
|
void printOpenRule(const ProofNode* pn) override; |
78 |
|
void printOpenLfscRule(LfscRule lr) override; |
79 |
|
void printCloseRule(size_t nparen = 1) override; |
80 |
|
void printProofId(size_t id) override; |
81 |
|
void printAssumeId(size_t id) override; |
82 |
|
void printEndLine() override; |
83 |
|
//------------------- helper methods |
84 |
|
/** |
85 |
|
* Print node to stream in the expected format of LFSC. |
86 |
|
*/ |
87 |
|
static void printNodeInternal(std::ostream& out, Node n); |
88 |
|
/** |
89 |
|
* Print type node to stream in the expected format of LFSC. |
90 |
|
*/ |
91 |
|
static void printTypeNodeInternal(std::ostream& out, TypeNode tn); |
92 |
|
static void printRule(std::ostream& out, const ProofNode* pn); |
93 |
|
static void printId(std::ostream& out, size_t id); |
94 |
|
static void printProofId(std::ostream& out, size_t id); |
95 |
|
static void printAssumeId(std::ostream& out, size_t id); |
96 |
|
//------------------- end helper methods |
97 |
|
private: |
98 |
|
/** |
99 |
|
* Replaces "(_ " with "(" to eliminate indexed symbols |
100 |
|
* Replaces "__LFSC_TMP" with "" |
101 |
|
*/ |
102 |
|
static void cleanSymbols(std::string& s); |
103 |
|
/** The output stream */ |
104 |
|
std::ostream& d_out; |
105 |
|
}; |
106 |
|
|
107 |
|
/** |
108 |
|
* Run on the proof before it is printed, and does two preparation steps: |
109 |
|
* - Computes the letification of nodes that appear in the proof. |
110 |
|
* - Computes the set of DSL rules that appear in the proof. |
111 |
|
*/ |
112 |
|
class LfscPrintChannelPre : public LfscPrintChannel |
113 |
|
{ |
114 |
|
public: |
115 |
|
LfscPrintChannelPre(LetBinding& lbind); |
116 |
|
void printNode(TNode n) override; |
117 |
|
void printTrust(TNode res, PfRule src) override; |
118 |
|
void printOpenRule(const ProofNode* pn) override; |
119 |
|
|
120 |
|
private: |
121 |
|
/** The let binding */ |
122 |
|
LetBinding& d_lbind; |
123 |
|
}; |
124 |
|
|
125 |
|
} // namespace proof |
126 |
|
} // namespace cvc5 |
127 |
|
|
128 |
|
#endif |