1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
/********************* */
/*! \file proof_node_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Proof node manager utility
**/
#include "cvc4_private.h"
#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H
#define CVC4__EXPR__PROOF_NODE_MANAGER_H
#include <vector>
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
namespace CVC4 {
/**
* A manager for proof node objects. This is a trusted interface for creating
* and updating ProofNode objects.
*
* In more detail, we say a ProofNode is "well-formed (with respect to checker
* X)" if its d_proven field is non-null, and corresponds to the formula that
* the ProofNode proves according to X. The ProofNodeManager class constructs
* and update nodes that are well-formed with respect to its underlying checker.
*
* If no checker is provided, then the ProofNodeManager assigns the d_proven
* field of ProofNode based on the provided "expected" argument in mkNode below,
* which must be provided in this case.
*
* The ProofNodeManager is used as a trusted way of updating ProofNode objects
* via updateNode below. In particular, this method leaves the d_proven field
* unchanged and updates (if possible) the remaining content of a given proof
* node.
*
* Notice that ProofNode objects are mutable, and hence this class does not
* cache the results of mkNode. A version of this class that caches
* immutable version of ProofNode objects could be built as an extension
* or layer on top of this class.
*/
class ProofNodeManager
{
public:
ProofNodeManager(ProofChecker* pc = nullptr);
~ProofNodeManager() {}
/**
* This constructs a ProofNode with the given arguments. The expected
* argument, when provided, indicates the formula that the returned node
* is expected to prove. If we find that it does not, based on the underlying
* checker, this method returns nullptr.
*
* @param id The id of the proof node.
* @param children The children of the proof node.
* @param args The arguments of the proof node.
* @param expected (Optional) the expected conclusion of the proof node.
* @return the proof node, or nullptr if the given arguments do not
* consistute a proof of the expected conclusion according to the underlying
* checker, if both are provided. It also returns nullptr if neither the
* checker nor the expected field is provided, since in this case the
* conclusion is unknown.
*/
std::shared_ptr<ProofNode> mkNode(
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
Node expected = Node::null());
/** Construct proof node, single child version */
std::shared_ptr<ProofNode> mkNode(PfRule id,
std::shared_ptr<ProofNode> child1,
const std::vector<Node>& args,
Node expected = Node::null());
/** Make assume */
std::shared_ptr<ProofNode> mkAssume(Node fact);
/** Make scope */
std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
std::vector<Node>& assumps,
bool ensureClosed = true
);
/**
* This method updates pn to be a proof of the form <id>( children, args ),
* while maintaining its d_proven field. This method returns false if this
* proof manager is using a checker, and we compute that the above proof
* is not a proof of the fact that pn previously proved.
*
* @param pn The proof node to update.
* @param id The updated id of the proof node.
* @param children The updated children of the proof node.
* @param args The updated arguments of the proof node.
* @return true if the update was successful.
*
* Notice that updateNode always returns true if there is no underlying
* checker.
*/
bool updateNode(ProofNode* pn,
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args);
/** Get the underlying proof checker */
ProofChecker* getChecker() const;
private:
/** The (optional) proof checker */
ProofChecker* d_checker;
/** Check internal
*
* This returns the result of proof checking a ProofNode with the provided
* arguments with an expected conclusion, which may not null if there is
* no expected conclusion.
*
* This throws an assertion error if we fail to check such a proof node, or
* if expected is provided (non-null) and is different what is proven by the
* other arguments.
*/
Node checkInternal(PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
Node expected);
};
} // namespace CVC4
#endif /* CVC4__EXPR__PROOF_NODE_H */
|
