1 |
|
/********************* */ |
2 |
|
/*! \file lfsc_post_processor.h |
3 |
|
** \verbatim |
4 |
|
** Top contributors (to current version): |
5 |
|
** Andrew Reynolds |
6 |
|
** This file is part of the CVC4 project. |
7 |
|
** Copyright (c) 2009-2020 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.\endverbatim |
11 |
|
** |
12 |
|
** \brief The module for processing proof nodes into Lfsc proof nodes |
13 |
|
**/ |
14 |
|
|
15 |
|
#include "cvc5_private.h" |
16 |
|
|
17 |
|
#ifndef CVC4__PROOF__LFSC__LFSC_POST_PROCESSOR_H |
18 |
|
#define CVC4__PROOF__LFSC__LFSC_POST_PROCESSOR_H |
19 |
|
|
20 |
|
#include <map> |
21 |
|
#include <unordered_set> |
22 |
|
|
23 |
|
#include "proof/lfsc/lfsc_node_converter.h" |
24 |
|
#include "proof/lfsc/lfsc_util.h" |
25 |
|
#include "proof/proof_node_updater.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
|
29 |
|
class ProofChecker; |
30 |
|
|
31 |
|
namespace proof { |
32 |
|
|
33 |
|
/** |
34 |
|
* A callback class used by the Lfsc convereter for post-processing proof nodes |
35 |
|
* by replacing internal rules by the rules in the Lfsc calculus. |
36 |
|
*/ |
37 |
|
class LfscProofPostprocessCallback : public ProofNodeUpdaterCallback |
38 |
|
{ |
39 |
|
public: |
40 |
|
LfscProofPostprocessCallback(LfscNodeConverter& ltp, ProofNodeManager* pnm); |
41 |
|
/** |
42 |
|
* Initialize, called once for each new ProofNode to process. This initializes |
43 |
|
* static information to be used by successive calls to update. |
44 |
|
*/ |
45 |
|
void initializeUpdate(); |
46 |
|
/** Should update */ |
47 |
|
bool shouldUpdate(std::shared_ptr<ProofNode> pn, |
48 |
|
const std::vector<Node>& fa, |
49 |
|
bool& continueUpdate) override; |
50 |
|
/** Update the proof rule application. */ |
51 |
|
bool update(Node res, |
52 |
|
PfRule id, |
53 |
|
const std::vector<Node>& children, |
54 |
|
const std::vector<Node>& args, |
55 |
|
CDProof* cdp, |
56 |
|
bool& continueUpdate) override; |
57 |
|
|
58 |
|
private: |
59 |
|
/** The proof node manager */ |
60 |
|
ProofNodeManager* d_pnm; |
61 |
|
/** The proof checker of d_pnm **/ |
62 |
|
ProofChecker* d_pc; |
63 |
|
/** The term processor */ |
64 |
|
LfscNodeConverter& d_tproc; |
65 |
|
/** |
66 |
|
* Are we in the first call to update? This is to distinguish the top-most |
67 |
|
* SCOPE. |
68 |
|
*/ |
69 |
|
bool d_firstTime; |
70 |
|
/** Add LFSC rule to cdp with children, args, conc */ |
71 |
|
void addLfscRule(CDProof* cdp, |
72 |
|
Node conc, |
73 |
|
const std::vector<Node>& children, |
74 |
|
LfscRule lr, |
75 |
|
const std::vector<Node>& args); |
76 |
|
/** Make chained form of a term */ |
77 |
|
Node mkChain(Kind k, const std::vector<Node>& children); |
78 |
|
/** Make fresh dummy predicate */ |
79 |
|
static Node mkDummyPredicate(); |
80 |
|
}; |
81 |
|
|
82 |
|
/** |
83 |
|
* The proof postprocessor module. This postprocesses a proof node into one |
84 |
|
* using the rules from the Lfsc calculus. |
85 |
|
*/ |
86 |
|
class LfscProofPostprocess |
87 |
|
{ |
88 |
|
public: |
89 |
|
LfscProofPostprocess(LfscNodeConverter& ltp, ProofNodeManager* pnm); |
90 |
|
/** post-process */ |
91 |
|
void process(std::shared_ptr<ProofNode> pf); |
92 |
|
|
93 |
|
private: |
94 |
|
/** The post process callback */ |
95 |
|
std::unique_ptr<LfscProofPostprocessCallback> d_cb; |
96 |
|
/** The proof node manager */ |
97 |
|
ProofNodeManager* d_pnm; |
98 |
|
}; |
99 |
|
|
100 |
|
} // namespace proof |
101 |
|
} // namespace cvc5 |
102 |
|
|
103 |
|
#endif |