diff options
Diffstat (limited to 'src/expr/proof_node_manager.h')
| -rw-r--r-- | src/expr/proof_node_manager.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 9904a78ec..527f2562d 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -80,6 +80,11 @@ class ProofNodeManager 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 |